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

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