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

Propositional logic

We now show that Coq integrates reasoning in propositional logic.

Open the file `propositional.v` in Proof General.

Feeding the commands to Coq, you will see the different axioms for propositional logic being proven. Coq manages the first axiom with `done`. But it needs more guidance for the second: the proof is made of several steps, described in the Ssreflect proof-script language. Let's see how it works.

The goal display

Looking at the evolution of subgoal(s) while proving the second axiom, we can see that subgoals are displayed in the shape of what is known as a sequent:
The context
```x1:H1
...
xn:Hn```
The bar
`=======================`
The (actual) goal
 `A1 -> ... -> Am` `->` `C` The stack The conclusion
This corresponds to what is often denoted `H1,...,Hn |- A1 -> ... -> Am -> C`, i.e. "there is a proof of `A1 -> ... -> Am -> C` from hypotheses `H1,...,Hn`". Or at least that's what you are supposed to show. Note that in Coq, hypotheses are labeled (`x1,...,xn` in this example) so you can easily refer to them.

The proof script for A2: manipulating implication

• `move => h1` moves the head element of the stack to the context, using the property that if `H1,...,Hn,D |- E` then `H1,...,Hn |- D -> E`. So if you look for a proof of `H1,...,Hn |- D -> E`, it is sufficient to prove `H1,...,Hn,D |- E`.
`D` is given the label `h1` which we specified in the script.
Here we use that script for `D`=`A->B->C` and `E`=`(A->B)->(A->C)`.
• We do the same thing for the other elements of the stack until it is empty.
• `apply:h1` tells Coq that, using hypothesis `h1:A→B→C` (and two Modus Ponens steps), you get a proof of `C` provided that you can build a proof of `A` and a proof of `B`. Correspondingly, Coq's answer is to now ask you to prove `A` and, as subgoal number 2, to prove `B`.
• Proving `A` is trivial, use `done`: it closes the present subgoal and you are now left with one remaining subgoal, having to prove `B`.
• To prove `B`, use another Modus Ponens: `apply:h2` will use hypothesis `h2:A→B` and result in your having to prove `A`.
• This is trivially done with `done`.
Note that Ssreflect offers very efficient ways of compacting your proof-scripts.
For instance, you can compact the first three lines of the script by
`move => h1 h2 h3.`

You now know the basic tactics to manipulate implication when it is below the bar or above the bar.

Negation (and False)

Negation in Coq is not primitive: `~B` is an abbreviation of `B->False`. That's why, when reaching
```h1 : A
============================
¬¬A```
in the proof of A3, you can use `move => h2`. Then there is just one Modus Ponens to do to conclude the proof.

But `False` is not just any formula, look at A4 and its trivial proof to see its property called `ex falso quodlibet`.

Now exercise: prove Theorem A5.

Conjunction

Look at the proof of A6, and the use of tactic `split` to split your goal, when it is a conjunction, into two goals.

Look at the proof of A7, and the use of tactic `case` to use a conjunction when it is above the bar.

Exercise: prove A8.

Disjunction

Look at the proof of A9, and the use of tactic `left` to decide to prove a disjunction by proving its left-hand side.

Exercise: guess the proof of A10.

Look at the proof of A11, and the (re-)use of tactic `case` to use a disjunction when it is above the bar.

Do it yourself

Complete the exercises at the end of propositional.v.

At some point, you will see that you need to use a hypothesis twice. For this, using `apply:(h)` instead of `apply:h` will keep a copy of `h` in the context instead of consuming it.