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 proofscript language. Let's see how it works.
The context  x1:H1 ... xn:Hn 

The bar  ======================= 

The (actual) goal 

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.
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.D
=A>B>C
and E
=(A>B)>(A>C)
.
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
.
A
is trivial, use done
: it closes the present subgoal and you are now left with one remaining subgoal, having to prove B
.
B
, use another Modus Ponens: apply:h2
will use hypothesis h2:A→B
and result in your having to prove A
.
done
.
move => h1 h2 h3.
You now know the basic tactics to manipulate implication when it is below the bar or above the bar.
~B
is an abbreviation of B>False
.
That's why, when reaching
h1 : A ============================ ¬¬Ain 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
.
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.
left
to decide to prove a disjunction by proving its lefthand side.
Look at the proof of A11, and the (re)use of tactic case
to use a disjunction when it is above the bar.
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.