How to step through semicolons separated tactics sequence in coqide?

Question

when constructing proof in coqide, I didn't find a way to step though

T1; T2; T3; ...; Tn.

one tactic by one tactic. So it became very difficult to construct correct proof like the code above. So my question is

• Is there a way to step through the code above or
• How do you construct proof like the code above?

Forward one Command or go to cursor aren't work.

Wooer

Answer 1

t1 ; t2 is not the same as doing first t1 then t2. If you want to do this you can do t1. t2. and this is the way to step through them.

The semicolon serves three purposes, stated for t1 ; t2:

• It applies t2 in all of the subgoals generated by t1;
• and it allows backtracking, if t2 were to fail, it would try a different success for t1 and apply t2 again on the generated subgoals;
• third, it's the simplest way to write down a tactic that represents a succession of tactics.

If you're lucky and this is the first or third case, then you can modify the script by replacing

t1 ; t2

by

t1. all: t2.

using goal selectors. This way the first step will allow you to see the goals generated by t1 and the second will show you how t2 affects them. If you need more precision you can also focus one of the subgoals to see t2 in action.

When backtracking is involved it becomes much harder to understand what is going on, but I believe it can be avoided at first, or limited to simple cases. You could for instance say that the goal can be closed by applying an introduction rule (constructor) and that then it should be easy. If multiple intro-rules/constructors apply doing

constructor. easy.

might result in failure, while

constructor ; easy.

might succeed. Indeed, if easy fails on the first constructor, coq will try the second and so on.

To answer your question about how one would write them, I suppose it can be the result of trial and error, and can mostly stem from factorisation or automation of proof scripts. Say you have the following proof script:

split.
- constructor.
  + assumption.
  + eassumption.
- constructor. eassumption.

You might want to summarise it as follows:

split ; constructor ; eassumption.

I personally don't necessarily recommend it because it becomes harder to maintain and harder to read for other users because of the issue of not being able to step through. I would limit this to cases where the proof is principled (like applying a constructor and be done with it), and resort to goal selectors for factorisation.

Leoraleos

Thanks for your detailed answer. I understand why it can't be step through now. But do people often write proof manual first and then summarize it to a more compact one? Or, do they just write down proof script and fix error until it passes? Or, do they only write such undebugable script when it's obviously right? – Wooer

If you find my answer satisfactory you can mark it as accepted. This is a question of style I think now. I think people do go step by step before getting the hang of it and going for a more concise version. Again, more concise doesn't necessarily mean better. If if makes it harder to maintain or less accessible, I don't think you should do it. And yeah unfortunately, some people write undebuggable stuff even when they shouldn't (to my mind). – Knapweed