Commit 392bf3c9 authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

demo2 and solution/td2 and some extra questions in td2

parent 06b204be
(** M2 LMFI : Internals of Coq basic logic *)
(* The only primitive stuff in Coq : universes and forall *)
(* the arrow (implication) is a notation for a non-dependent forall *)
Definition test (A B : Prop) := A -> B.
(*
Unset Printing Notations.
Print test.
*)
(* Logical constants : True *)
Print True.
(* Inductive True : Prop := I : True *)
Check I.
Lemma obvious : True.
exact I.
(*trivial.
Show Proof.*)
(* constructor.
Show Proof. *)
Qed.
Lemma attempt : True -> True.
Proof.
intros H.
destruct H. (* no interesting elimination of H:True *)
Show Proof.
Abort.
(* False *)
Print False.
(* Inductive FalseBis : Prop := . *)
Print False_rect. (* elimination of False : a match with no branches
providing anything you want *)
Lemma false_elim : False -> 0 = 1.
Proof.
intro H.
destruct H.
Show Proof.
Qed.
(* Negation : ~A shortcut A->False *)
(* Connectors : /\ and \/ *)
Print prod. (* or * in the type_scope *)
Check (0,1).
Print and.
(*Inductive and (A B : Prop) : Prop := conj : A -> B -> and A B.
Print and_ind. *)
Lemma conj_intro : True /\ True.
Proof.
split.
Show Proof. (* introduction is using constructor conj *)
trivial.
trivial.
Show Proof.
Qed.
Lemma conj_sym (A B : Prop) : A /\ B -> B /\ A.
Proof.
(*
intuition.
Show Proof. (* an and_ind instead of a match, but that's equivalent *)
*)
intros H.
destruct H. Show Proof.
auto.
Show Proof.
Qed.
(* disjonction : two constructors ! *)
Print or.
Check or.
Check or_introl. (* forall A B : Prop, A -> A \/ B *)
Check or_intror. (* forall A B : Prop, A -> A \/ B *)
Fail Check or_rect. (* no elimination on Type :
usually, no proofs can influence a program *)
(* Said again, the Prop world normally doesn't impact the program world
: "proofs can be eliminated only to build proofs". *)
Fail Definition evade (p : True \/ True) : bool :=
match p with
| or_introl _ => true
| or_intror _ => false
end. (* Refused *)
Check or_ind. (* forall A B P : Prop, (A -> P) -> (B -> P) -> A \/ B -> P *)
Print or_ind. (* a match on the proof of (A\/B) *)
(* the "left" tactic : applying the or_introl constructor *)
(* right or_intror *)
(* destruct on a H:A\/B hypothesis : match H with ...*)
(* iff : A<->B shortcut for (A->B)/\(B->A) *)
Lemma or_sym A B : A\/B -> B\/A.
Proof.
intros [a|b]. (* same as intro H. destruct H. *)
constructor. trivial. (* bad luck: tactic constructor takes the first
that fits. solution : constructor 2, or rather
left and right*)
Abort.
About "/\".
Locate "/\".
(* exists *)
Locate "exists". (* the underlying definition is called ex *)
(* exists x:A, P x <-------> ex A P *)
Print ex.
(*
Inductive ex (A : Type) (P : A -> Prop) : Prop :=
ex_intro : forall (x : A)(p : P x), ex A P.
*)
Print and.
(* Recall : Logical pair :
Inductive and (A B : Prop) : Prop :=
conj : forall (a:A) (b:B), and A B.
*)
(* in fact, ex is same, with a dependency on B (which becomes P ...)
ex is a dependent pair (sigma type)
: it groups a witness x and a proof of the property of x
introduce : tactic called "exists ..." : internally apply of ex_intro
elimination : destruct H when H:exists x,P x : that's a
match H with
| ex_intro x p => ...
end.
*)
(* instead of exists, you could try econstructor (leave the witness
undecided for the moment). See eexists also. Existential tactics
(manipulating existential variables. *)
Lemma test_ex : exists n:nat, n = n.
Proof.
eexists. (* ?n = ?n *)
Abort.
(* eq *)
Print eq.
(* Syntactic equality : only x is equal to x *)
(*Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : eq A x x. *)
(* constructor is the reflexivity rule. tactic "reflexivity" *)
Lemma compute_equal : 2+2 = 4.
Proof.
simpl.
reflexivity.
Qed.
Check eq_ind.
(* The Leibniz principle, or the rewrite principle :
eq_ind
: forall (A : Type) (x : A) (P : A -> Prop),
P x -> forall y : A, x = y -> P y
*)
(* match on a equality is a form of rewrite
the rewrite tactic proceed by a match on the equality *)
Print eq_ind.
Lemma eq_sym A (x y : A) : x = y -> y = x.
Proof.
intro H. destruct H. reflexivity.
Qed.
Print eq_sym.
(* nat and induction *)
Print nat.
Check nat_ind.
Print nat_ind. (* fixpoint + match *)
Lemma test_induction : forall n:nat, n=n.
induction n.
Show Proof.
Abort.
Print "+".
(*
2+2 = Nat.add (S (S 0)) 2.
= match S (S 0) with
| 0 => m
| S p => S (add p 2)
(* unfold rule for fixpoint : a fixpoint applied to a constructor can
unfold once *)
= S (add (S 0) 2)
= ...
= 4
*)
Compute 2+2.
Require Import Arith.
Check Nat.add_succ_l.
Lemma non_compute_proof : 2+2 = 4.
Proof.
rewrite Nat.add_succ_l.
rewrite Nat.add_succ_l.
rewrite Nat.add_0_l.
reflexivity.
Qed.
Print non_compute_proof.
Print Nat.add_succ_l.
Lemma compute_proof : 2+2 = 4.
(* in coq, most of the time we're modulo computation :
2+2 just the same as 4 *)
simpl. (* force a computation *)
reflexivity.
Set Printing Implicit.
Show Proof.
Check (@eq_refl nat 4).
(* 2+2=4 and 4=4 are the *same* statement (modulo computation) :
(what we call *convertible* )
they can be proved by the *same* proof term *)
Qed.
Lemma compute_proof' : 2+2 = 4.
reflexivity.
Qed.
Definition compute_proof'' : 2+2 = 4 := eq_refl.
(* or more precisely @eq_refl nat 4 *)
(* To be confirmed on recent Coq : issue with 8.12.0 ? *)
(* sig and sumbool : See later *)
Print sig. (* existential with output universe Type instead of Prop *)
Print sumbool. (* disjunction with output type in Type *)
......@@ -61,10 +61,12 @@ 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.
Lemma notexistsnot : ~(exists e, ~P e) <-> forall e, P e.
Proof.
intros H e.
apply not_not_elim. intro. apply H. exists e. assumption.
split.
- intros H e.
apply not_not_elim. intro. apply H. exists e. assumption.
- intros H (e,H'). apply H'. apply H.
Qed.
Lemma DrinkerLemma : exists e, P e -> (forall y, P y).
......
(* Exercise 1 *)
Lemma add_0_l : forall n, 0 + n = n.
Proof.
intro. (* optional step *)
simpl. (* optional step *)
reflexivity.
Qed.
Lemma add_succ_l : forall n m, S n + m = S (n + m).
Proof.
intros.
simpl.
reflexivity.
Qed.
Lemma add_0_r : forall n, n + 0 = n.
Proof.
simpl. (* nothing, internally n+... = ... match n with ... *)
induction n.
- simpl. reflexivity.
- simpl. f_equal. (* back to the initial statement, for n-1. *)
(* with induction n instead of destruct n,
now we have an extra IHn induction hypothesis *)
apply IHn.
Qed.
Lemma add_succ_r : forall n m, n + S m = S (n + m).
Proof.
induction n; simpl. (* induction and then simpl on both subgoals *)
- reflexivity.
- intros. f_equal. apply IHn. (* or "rewrite IHn" instead of the f_equal. *)
Qed.
Lemma add_assoc : forall n m p, (n + m) + p = n + (m + p).
Proof.
induction n; simpl. (* avoid induction on m or p, that would not help
(less computations triggered). *)
- reflexivity.
- intros. f_equal. apply IHn.
Qed.
Lemma add_comm : forall n m, n + m = m + n.
Proof.
induction m; simpl. (* For once, induction m is ok (symmetrical statement)
Compared with induction n, it even leads to
sub-equations in the right direction. *)
- apply add_0_r.
- rewrite add_succ_r. f_equal. apply IHm.
Qed.
Lemma add_comm' : forall n m, n + m = m + n.
Proof.
(* rewrite ?foo will rewrite equation foo as more as possible, possibly
0 times *)
induction n; simpl; intros; rewrite ?add_0_r, ?add_succ_r, ?IHn; reflexivity.
Qed.
(* Exercise 2 *)
Lemma mul_0_l : forall n, 0 * n = 0.
Proof.
reflexivity. (* definitional equality *)
Qed.
Lemma mul_succ_l : forall n m, S n * m = m + n * m.
Proof.
reflexivity. (* same *)
Qed.
Lemma mul_0_r : forall n, n * 0 = 0.
Proof.
induction n; simpl.
- reflexivity.
- apply IHn.
Qed. (* could be shortened in induction n; simpl; trivial. *)
Require Import Setoid.
Lemma mul_succ_r : forall n m, n * S m = n + n * m.
Proof.
induction n; simpl; intros.
- reflexivity.
- f_equal. rewrite IHn. rewrite <- 2 add_assoc. (* reverse rewrite two times *)
(* To answer a question by Enrique : rewrite (add_comm n)
for controling where add_comm is used. *)
f_equal. apply add_comm.
Qed.
Lemma mul_distr : forall n m p, (n + m) * p = n * p + m * p.
Proof.
induction n; simpl; intros.
- reflexivity.
- rewrite add_assoc. f_equal. apply IHn.
Qed.
(* Just to illustrate a bit of the tactic language, we can define
out own tactics (here an alias for a longer sequence of tactics *)
Ltac induct n := induction n; simpl; intros.
Lemma mul_assoc : forall n m p, (n * m) * p = n * (m * p).
Proof.
induct n. (* Same as induction n; simpl; intros. *)
- reflexivity.
- rewrite mul_distr. f_equal. apply IHn.
Qed.
Lemma mul_comm : forall n m, n * m = m * n.
Proof.
induction m; simpl. (* just as for add, induction n is also ok here *)
- apply mul_0_r.
- rewrite mul_succ_r. f_equal. apply IHm.
Qed.
(* Exercise 3 *)
Definition le (n m : nat) := exists p, n + p = m.
Infix "<=" := le : alt_le_scope.
Open Scope alt_le_scope.
Lemma le_refl : forall n, n <= n.
Proof.
unfold le. (* not mandatory, but convenient to understand what's going on*)
intros. exists 0. apply add_0_r.
Qed.
Lemma le_trans : forall n m p, n <= m -> m <= p -> n <= p.
Proof.
unfold le.
intros n m p (q,Hq) (r,Hr). exists (q+r).
rewrite <- add_assoc. rewrite Hq, Hr. reflexivity.
Qed.
Lemma add_more_0 : forall n m, n+m = n -> m = 0.
Proof.
induction n; simpl; intros. (* ; auto finishes directly :-) *)
- assumption.
- injection H. apply IHn.
Qed.
Lemma add_0_left_0 : forall n m, n+m = 0 -> n = 0.
induction n; simpl; intros. (* ; easy finishes directly :-) *)
- reflexivity.
- discriminate.
Qed.
Lemma le_antisym : forall n m, n <= m -> m <= n -> n = m.
Proof.
unfold le.
intros n m (q,Hq) (r,Hr). rewrite <- Hq in Hr.
rewrite add_assoc in Hr.
assert (q+r = 0).
{ apply (add_more_0 n). assumption. }
assert (q = 0).
{ apply (add_0_left_0 q r). assumption. }
rewrite H0 in Hq. rewrite add_0_r in Hq. assumption.
Qed.
(* another style : apply ... in ... *)
Lemma le_antisym' : forall n m, n <= m -> m <= n -> n = m.
Proof.
unfold le.
intros n m (q,Hq) (r,Hr). rewrite <- Hq in Hr.
rewrite add_assoc in Hr.
apply add_more_0 in Hr.
apply add_0_left_0 in Hr.
rewrite Hr in Hq. rewrite add_0_r in Hq. assumption.
Qed.
(* Bonus proofs : *)
Lemma le_succ : forall n m, n <= m -> n <= S m.
Proof.
Admitted.
Lemma le_total : forall n m, n <= m \/ m <= n.
Proof.
Admitted.
Close Scope alt_le_scope.
Locate "<=". (* Now <= is back to the default definition of Coq *)
Print Peano.le. (* The one of Coq : an inductive definition *)
Lemma le_equiv : forall n m, n <= m <-> le n m.
Proof.
split.
- intros H; induction H. (* induction on a inductive proof ! *)
+ admit. (* TODO *)
+ admit. (* TODO *)
- admit. (* TODO *)
Admitted.
......@@ -109,7 +109,14 @@ 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.
Also show the following statements:
```coq
Lemma le_succ : forall n m, n <= m -> n <= S m.
Lemma le_total : forall n m, n <= m \/ m <= n.
```
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 these two definitions are equivalent, you could even try to already prove that. Hint : a proof using a `<=` of Coq (internal name `Peano.le`) can be done by induction over this hypothesis.
### Epilogue ###
......
......@@ -86,8 +86,6 @@ On peut définir l'ordre large sur les entiers ainsi:
Definition le (n m : nat) := exists p, n + p = m.
Infix "<=" := le.
```
Notez que cette définition n'est pas celle de la libraire standard de Coq (cf. [Init/Peano.v](https://coq.inria.fr/stdlib/Coq.Init.Peano.html)), basée elle sur un prédicat inductif. Mais vous
pourrez montrer par la suite que ces deux définitions sont bien équivalentes.
Montrer que notre prédicat `le` est bien une relation d'ordre:
```
......@@ -96,6 +94,15 @@ 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.
```
Montrer également les énoncés suivants :
```coq
Lemma le_succ : forall n m, n <= m -> n <= S m.
Lemma le_total : forall n m, n <= m \/ m <= n.
```
Notez que cette définition n'est pas celle de la libraire standard de Coq (cf. [Init/Peano.v](https://coq.inria.fr/stdlib/Coq.Init.Peano.html)), basée elle sur un prédicat inductif. Mais ces deux définitions sont équivalentes, vous pouvez même essayer de le montrer dès maintenant. Indice : une preuve utilisant un `<=` de Coq (nom interne `Peano.le`) peut se faire par récurrence sur cette hypothèse.
### Epilogue ###
Au lancement de Coq, la définition des entiers `nat` est directement disponible, ainsi que les opérations correspondante, en version *qualifiées*, par exemple `Nat.add` qui correspond au signe `+`. Il existe aussi d'anciens noms pour ces opérations : `plus`, `mult`, mais ils sont considérés comme obsolètes. Les preuves concernant les entiers et leurs opérations ne sont pas toutes disponibles initialement, elles sont à charger via `Require Import Arith`. Ceci donnera accès par exemple à `Nat.add_assoc` et à la plupart des lemmes de ce TP. La commande `Search` permettra d'en savoir plus sur les résultats disponibles. Enfin, d'autres tactiques plus puissantes aideront grandement par la suite, par exemple `auto`, `omega` et `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