Exercices for Coq
Benjamin Werner
Giens, 1999
Abstract: This text is meant to be viewed through a browser like netscape. It is
the possible to copy and paste from it into your Coq window.
1 Pointers
The system is freely available by ftp. It can be found, together
with various information, on
http://coq.inria.fr
There is an email hotline coq@pauillac.inria.fr
and and
moderated mailinglist coqclub@pauillac.inria.fr
.
For people looking about more theoretical references about program
extraction (for functional programs), they can have a look at a paper
by Christine Paulin and myself (Journal of Symbolic Computation,
1993); go to my homepage (coq.inria.fr/~werner/
) look for the
pointer ``some publications'' and then some file with JSC in the name...
2 Other documentation
The user's manual is available online
here
for the machines
provided by the school, or somewhere else if you have installed Coq on
your machine.
3 Propositional tautologies
3.1 (A>B>C)>A>(A>B)>C
We launch this goal by:
Variable A,B,C:Prop.
Lemma Ex1 : (A>B>C)>A>(A>B)>C.
There are various ways to prove it. One is use the automated tactic
Tauto. Another automated tactic is Auto, which is often
usefull. It does systematicaly Intros and the tries to apply all
the local hypotheses as well as the lemmas of the Hint
database. A lemma L is added to the database by:
Hints Resolve L.
If Auto manages to solve this goal, it is because this can be
done only with introductions and local Apply's:
Intros c a b.
Apply c. (* generates two subgoals *)
Exact a.
Apply b. (* we start solving the secong goal *)
Exact a.
A more primitive way is, in this case, quite easy to give the direct proof of
this proposition.
Exact [c,a,b](c a (b a)).
Notice that we here do not have to provide the types of a,b and
c in the abstractions, since they can obviously be infered. The
explicit proof would be:
Exact [c:A>B>C][a:A][b:A>B](c a (b a)).
3.2 Reminder
 Save and Qed save the solved goal in the
environement under its current name. Savename allows you
to change the name.
 Restart restarts the proof of the current lemma from
scratch.
 Abort discards the current proof and goal.
3.3 conjunctions: (A>B>C)/\A/\(A>B)>(C/\A)
This hypothesis in this proposition are obviously equivalent to the
previous ones, but we
have to deal with the conjunctions. Conjunctions in hypotheses are
broken appart with Elim. Here we actually have two nested
conjunctions:
Intros h1.
Elim h1.
Intros h2 h3.
Elim h3.
Intros h4 h5.
To prove the conjunction, we prove separately its two components by
Split.
Split.
(* The first part is similar to the previous example *)
Apply h2.
Exact h4.
Apply h5; Exact h4.
(* the last goal *)
Exact h4.
3.4 disjunctions:A>(B\/(A>C))>(C\/B)
Again, in the hypotheses disjunctions are eliminated by Elim. You the get two cases corresponding to the two branches of the
disjunction.
Intros a d.
Elim d.
To prove a disjunction, one can use Left and Right to
chose the branch to be proven.
(* first case: B is true *)
Intros b.
Right.
Exact b.
(* second case: A>C *)
Intros c.
Left.
Apply c; Exact a.
4 Proofs by induction
The principles are the same as before, but elimination over natural
numbers yields an induction hypothesis, since the latter is a
recursive data type.
We want to prove that addition is commutative. Let us recall its
definition:
Fixpoint plus [n:nat] : nat > nat :=
[m:nat]
Cases m of
O => m
 (S p) => (S (plus n m))
end.
Because of its definition, addition verifies two congruences, namely:
(plus O n) 
> 
n 
(plus (S n) m) 
> 
(S (plus n m))

We reasoning by induction to prove that the same equalities hold with
respect to the second argument.
4.1 (n:nat)(plus n O)=n
This is done by induction over n. The tactic to use equalities in
order to change the current goal is Rewrite, a possible tactic
to prove reflexive equalities is Trivial.
Lemma p0 : (n:nat)(plus n O)=n.
Intro n; Elim n.
(* we now have two cases. The base case is trivial. *)
Simpl.
Trivial.
(* The second case is n=(S p) *)
Intros p IH.
Simpl. (* uses the reduction *)
Rewrite IH.
Trivial.
Save.
4.2 (n,m:nat)(plus n (S m))=(S (plus n m))
Again, an induction over n.
Lemma pS : (n,m:nat)(plus n (S m))=(S (plus n m)).
Intros n m.
Elim n.
Simpl; Trivial.
(* the recursive case *)
Intros p IH.
Rewrite IH.
Trivial.
Save.
4.3 commutativity
Using these two lemmas, try to prove the commutativity.
4.4 transitivity of <
Prov that le is transitive. This is an induction over the proof
of a recursive predicate.
5 Euclidean division
In order to avoid the condition d¹ 0 a possible way is to state:
(a,b:nat)(EX q  (EX r  a=(plus (mult (S b) q) r) /\ (le r b))).
The nice point is that the proof really reflects Euclid's algorithm
(since we are in constructive logic). The proof is by induction over
a. Think of the algorithm to understand how to do the proof !
At some point, we will need to decide which one of two natural numbers
is greater. Logicaly, this corresponds to a proof of:
(a,b:nat)(le a b)\/(lt b a)
or some equivalent proposition. When a proof of this disjunction is
eliminated, we are left with two cases, one corresponding to the case
a<= b and the other one to b >a.
To find this lemma without having to prove it, load the arithmetic
library:
Require Arith.
and look for the lemmas ending by a disjunction:
Search or.
6 Program extraction
Here are just a few words about extraction of functional programs. The
computational version of the existential quantifier is written
{x:AP}
.
For instance, the proposition
(a,b:nat){r:nat  (EX q  a=(plus (mult (S b) q) r) /\ (le r b))}
is the specification of the mod function, computing the reminder
of the division of a by (S b). The quotient q will
not appear in the extracted program, allthough its existence is part
of the specification.
Below is a proof of this specification and how the ML program can be
extracted.
Lemma mod : (a,b:nat)
{r:nat  (EX q:nat  a=(plus (mult (S b) q) r)/\(le r b))}.
Induction a.
Intros; Split with O; Split with O; Simpl.
Split.
Replace (plus (mult b (0)) (0)) with (mult b O); Auto.
Apply le_O_n.
Intros a' ha b.
Elim (ha b).
Intros r.
Intros h2.
Elim (le_or_le_S b r).
Intros.
Split with O.
Elim h2; Intros q hq.
Split with (S q).
Elim hq; Intros hq1 hq2.
Split.
Simpl.
Rewrite hq1.
Replace (plus (mult (S b) q) r) with (plus q (mult b (S q))).
Auto.
Replace b with r; Simpl.
Replace (plus (plus q (mult r q)) r) with (plus q (plus r (mult r q))).
Replace (mult r (S q)) with (plus r (mult r q)).
Auto.
Replace (mult r q) with (mult q r).
Replace (mult r (S q)) with (mult (S q) r).
Simpl.
Auto.
Apply mult_sym.
Apply mult_sym.
Replace (plus (plus q (mult r q)) r) with (plus q (plus (mult r q) r)).
Replace (plus r (mult r q)) with (plus (mult r q) r).
Auto.
Apply plus_sym.
Apply plus_assoc_l.
Apply le_antisym; Auto.
Apply le_O_n.
Intros; Split with (S r).
Elim h2; Intros q hq; Split with q.
Elim hq; Intros hq1 hq2; Split; Auto.
Rewrite hq1; Auto.
Save.
Finaly, we can extract the corresponding ML program.
Require Extraction.
Write Caml File "modulo" [mod].
which produces the file modulo.ml
6.1 full division
If we want to extract the program yielding the reminder r and the quotient q, the best is to define ourselves the double
existential quantification.
Inductive eucl_ex [a,b:nat] : Set :=
eucl_intro :
(r,q:nat) a=(plus (mult (S b) q) r)>(le r b)>
(eucl_ex a b).
The specification is then:
Lemma eucl_div : (a,b:nat)(eucl_ex a b).
and is proven in a similar way to the noncomputational version of the
division.
This document was translated from L^{A}T_{E}X by H^{E}V^{E}A.