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
The bar
The (actual) goal
A1 -> ... -> Am
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

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


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.


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.