Commit 3484609c authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

td2, english version

parent 54475039
......@@ -61,6 +61,96 @@ Parameter P : E -> Prop.
(* Predicate telling if somebody drinks *)
Parameter e0 : E. (* the name of a person in the room *)
Lemma notexistsnot : ~(exists e, ~P e) -> forall e, P e.
Proof.
intros H e.
apply not_not_elim. intro. apply H. exists e. assumption.
Qed.
Lemma DrinkerLemma : exists e, P e -> (forall y, P y).
Proof.
(* To be continued... *)
destruct (EM (exists e, ~P e)).
- (* there is a non-drinker : it's our witness ! *)
destruct H as (x,Hx).
exists x. intros Hx'. destruct Hx. assumption.
- (* everybody drinks : any witness works, in particular e0 *)
exists e0. intros _. apply notexistsnot. assumption.
Qed.
End Exercise2.
Module Exercise3.
Parameter E:Type.
Definition sets := E -> Prop.
Definition subset (A B : sets) : Prop :=
forall x:E, A x -> B x.
Lemma subset_refl : forall A, subset A A.
Proof.
unfold subset; intros; assumption.
Qed.
Lemma subset_trans : forall A B C, subset A B -> subset B C -> subset A C.
Proof.
unfold subset; intros.
apply H0; apply H; assumption.
Qed.
Definition eq (A B : sets) : Prop :=
forall x:E, A x <-> B x.
Lemma eq_refl : forall A, eq A A.
Proof.
split; intros; assumption.
Qed.
Lemma eq_sym : forall A B, eq A B -> eq B A.
Proof.
unfold eq. intros. split; intros; apply H; assumption.
Qed.
Lemma eq_trans : forall A B C, eq A B -> eq B C -> eq A C.
Proof.
unfold eq. intros. split; intros.
- apply H0, H; assumption.
- apply H, H0; assumption.
Qed.
Lemma subset_antisym : forall A B, subset A B /\ subset B A <-> eq A B.
Proof.
split.
- intros (H,H'). intros x. split. apply H. apply H'.
- intros H. split; intro; apply H.
Qed.
Definition union (A B:sets) := fun x => A x \/ B x.
Definition inter (A B:sets) := fun x => A x /\ B x.
Lemma union_com A B : eq (union A B) (union B A).
Proof.
unfold eq, union.
firstorder. (* see td1 for a pedestrian proof. *)
Qed.
Lemma inter_com A B : eq (inter A B) (inter B A).
Proof.
firstorder.
Qed.
Lemma union_idem A : eq (union A A) A.
Proof.
firstorder.
Qed.
Lemma inter_idem A : eq (inter A A) A.
Proof.
firstorder.
Qed.
Lemma distr A B C : eq (inter A (union B C)) (union (inter A B) (inter A C)).
Proof.
firstorder.
Qed.
TD2 : Arithmetical Proofs in Coq
================================
M2 LMFI
Pierre Letouzey (from A. Miquel)
### Revision : the inductive type of natural numbers ###
In Coq, a new data type can be introduced via the mecanism of *inductive definition* (very similar to the algebraic types in OCaml). For instance, the type `nat` of natural numbers is introduced in the Coq standard library (cf. file [Init/Datatypes.v](https://coq.inria.fr/stdlib/Coq.Init.Datatypes.html)) via the following inductive definition:
```coq
Inductive nat : Set :=
| O : nat
| S : nat -> nat.
```
This definition adds to the current environment three new constants:
- the type `nat : Set` (where `Set` is an alias for the lowest of `Type` universes);
- the constructor `O : nat`
- the constructor `S : nat -> nat`
Beware, the constructor for zero is `O` internally (the letter O), even if the system also accepts later numerical notations : `0` for `O`, `1` for `(S O)`, `2` for `(S (S O))`, etc.
### Induction principles ###
The former inductive definition also generates automatically a few induction principles. In practice, the mostly used is :
```coq
nat_ind :
forall P : nat -> Prop,
P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P
```
which is used internally by the `induction` tactic.
Other handy tactics on such an inductive type :
- `simpl` : applies computation rules.
- `rewrite` : see [td1bis.md](td1bis.md).
- `injection` : all inductive constructors are injective, from `H : S x = S y` then `injection H` provides `x = y`.
- `discriminate` : all inductive constructors are orthogonal, from `H : S x = O` then `discriminate H` or just `discriminate` proves `False` (hence anything).
- `f_equal` : proves a goal `f x = f y`, as long as sub-goal `x = y` could then be proved. Sort of dual to `injection`, except that it works for any function `f`, not only for inductive constructors.
### Exercise 1 : Addition ###
In Coq, the addition of natural numbers is defined via a `Fixpoint` (similar to the `let rec` of OCaml). See [Init/Nat.v](https://coq.inria.fr/stdlib/Coq.Init.Nat.html) :
```coq
Fixpoint add (n m:nat) : nat :=
match n with
| O => m
| S p => S (add p m)
end.
```
Note that the recursive call is done here on a first argument `p` which is stricly lower than `n`. Only such a *structural decrease* is allowed, Coq will refuse the definitions where it cannot verify this property, in order to avoid non-terminating computations.
The system uses the notation `n + m` to shorten the term `Nat.add n m`.
Show the following lemmas on addtion (basic equalities, then associativity and commutativity). Which egalities are "definitional" (obtained by mere computation and reflexivity, tactics `simpl` and `reflexivity`) ? For the other equalities, proceed by induction over `n`, thanks to the `induction` tactic.
```coq
Lemma add_0_l : forall n, 0 + n = n.
Lemma add_succ_l : forall n m, S n + m = S (n + m).
Lemma add_0_r : forall n, n + 0 = n.
Lemma add_succ_r : forall n m, n + S m = S (n + m).
Lemma add_assoc : forall n m p, (n + m) + p = n + (m + p).
Lemma add_comm : forall n m, n + m = m + n.
```
### Exercise 2 : Multiplication ###
In Coq, the multiplication is defined by :
```coq
Fixpoint mul (n m:nat) : nat :=
match n with
| O => O
| S p => m + mul p m
end.
```
The system uses the notation `n * m` to shorten `mul n m`.
Just as for addition, prove the following lemmas:
```coq
Lemma mul_0_l : forall n, 0 * n = 0.
Lemma mul_succ_l : forall n m, S n * m = m + n * m.
Lemma mul_0_r : forall n, n * 0 = 0.
Lemma mul_succ_r : forall n m, n * S m = n + n * m.
Lemma mul_distr : forall n m p, (n + m) * p = n * p + m * p.
Lemma mul_assoc : forall n m p, (n * m) * p = n * (m * p).
Lemma mul_comm : forall n m, n * m = m * n.
```
### Exercise 3 : an order relation on numbers ###
Here is one possible way to define the large inequality on `nat` numbers:
```coq
Definition le (n m : nat) := exists p, n + p = m.
Infix "<=" := le.
```
Show that this predicate `le` is indeed an order relation:
```coq
Lemma le_refl : forall n, n <= n.
Lemma le_trans : forall n m p, n <= m -> m <= p -> n <= p.
Lemma le_antisym : forall n m, n <= m -> m <= n -> n = m.
```
Note : this `le` definition is not the one used in the Coq standard library (cf. [Init/Peano.v](https://coq.inria.fr/stdlib/Coq.Init.Peano.html)), which is based on an inductive predicate. But we could prove later than these two definitions are equivalent.
### Epilogue ###
When launching Coq, the definition of `nat` numbers is directly available, as well as the previous operations in *qualified* version, for instance `Nat.add` for `+`. Some older names are also available : `plus`, `mult` but they are considered deprecated. The proofs about `nat` numbers and their operations are not available initially, they should be loaded via `Require Import Arith`. This command provides for instance `Nat.add_assoc` and many other proofs, including many lemmas of this TP. The `Search` command allows to search through all these available lemmas. Moreover, some other powerful tactics may help later, for instance `auto`, `lia` (formerly `omega`) or `ring`.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment