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 e-mail hotline coq@pauillac.inria.fr and and moderated mailing-list coq-club@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 home-page (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 on-line 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:A|P}.

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 non-computational version of the division.

This document was translated from L^AT_EX by H^EV^EA.