Bookkeeping

Having seen the basics, let's see how Ssreflect can make your life easier as a proof developer.

Open the file bookkeeping.v in Proof General.

Examples

The first example shows how to stack and unstack, and combine these operations. We start seeing a general pattern for our commands:

tactic [:h0...hn] [=> h0'...hm'] [=> //]

where only tactic is mandatory, and which is interpreted as follows:

First, :h0...hn (if present) loads items from the context onto the stack
(using parentheses around the labels, e.g. (h0), will keep a copy of the items in the context).
Second, tactic is applied; it will usually act on either
- the head of the stack (apply, case)
- the conclusion (split, left, right)
Third, => h0'...hm' (if present) unloads items from the stack to the context (using _ instead of a label will discard an item completely), while => // tries to automatically solve as many goals as tactic has generated.

Notes for the acute observer:

In the above pattern, notice that move is the tactic that does nothing. It's the : h0...hn and => h0'...hm' that do the moving about.
apply:h. does the same thing as move:h. apply.

The second example shows how to combine commands as written above, so that Coq executes them in one step, rather than several.

The third example shows how to reach your goal by proving a lemma first. This is called a forward-reasoning step: see below why.

Finally, it's time to give you Coq+Ssreflect's basic cheat sheet.

Exercise

Finish the proof of bk4.

First, do it with forward-reasoning: the next 2 commands you write should result in your having the extra hypothesis h2 : B, the next two should provide the extra hypothesis h3 : C, the next two h4 : D, the next two h5 : E; then from

        i1 : A → B
	i2 : B → C
	i3 : C → D
	i4 : D → E
	h1 : A
	h2 : B
	h3 : C
	h4 : D
	h5 : E

you can finish with done.

Second, do it with backward-reasoning: the next command you write should result in your having to prove D in the same context, the next one should result in your having to prove C, the next one should result in your having to prove B, and the next command you send should finish the proof. The context should never change.

Useful tip

When you have proved a theorem in Coq, you can re-use the result in your future proofs!

In fact, all of your previously proved theorems are invisibly part of your context. Therefore, if you have proved

Theorem mytheorem:A
Proof.
...
Qed.

then in your future proofs you can invoke that theorem with commands such as apply:mytheorem or case:mytheorem, as if mytheorem:A was a visible item of your context.