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.