Coq for SSFT'2018 - Type Theory exercises - Level 2
Crash course in Coq


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.


The first example shows how to stack and unstack, and combine these operations. We start seeing a general pattern for our commands:
tactic [] [=> h0''] [=> //]
where only tactic is mandatory, and which is interpreted as follows: Notes for the acute observer:

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.


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
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.