Commit edcca26a authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

solution td5 + demo5

parent d3a8628a
(** * A few words about the inversion tactics *)
(* Already seen : injection and discriminate :
injection H where H : S x = S y gives x = y
injection H where H : x::l = x'::l' gives both x=x' and l=l'
discriminate H where H : O = S x conludes the goal
(since this case is impossible)
*)
(* The tactic inversion is a generalization of both,
trying to recover from an inductive predicate
what situations may have lead to this concrete predicate.
*)
Inductive even : nat -> Prop :=
| even_O : even O
| even_SS n : even n -> even (S (S n)).
Lemma even_2 : even 2.
Proof.
apply even_SS.
apply even_O.
Qed.
Lemma even_plus4 : forall n, even n -> even (4+n).
Proof.
intros.
apply even_SS.
apply even_SS.
assumption.
Qed.
(* Up to now, even_2 and even_plus4 are direct proofs,
no need for inversion *)
Lemma not_even_one : ~even 1.
Proof.
intro.
(* Here, destruct H (or induction H) would forget that our number is 1 :-(
Before destruct H, we need to save all details ourselves
(for instance via "remember"). *)
remember 1 as m.
destruct H.
- discriminate.
- discriminate.
Qed.
(* inversion is here nicer than this remember + destruct,
and way more general *)
Lemma not_even_one_bis : ~even 1.
Proof.
intro.
inversion H.
Qed.
Lemma even_plus3 n : even (3+n) -> even (1+n).
Proof.
intro H.
inversion H. (* subst. (* if you want to get rid of remaining equations *)*)
assumption.
Qed.
(* Since equality is also an inductive predicate, inversion also works
on equality hypothesis (and subsumes injection and discriminate). *)
Lemma test_inj x : S x = 0 -> False.
Proof.
intro H.
inversion H.
Qed.
(** * Impredicative encodings *)
(* Note that we can quantify on all propositions and get a new proposition.
That's impredicativity. In Coq that's specific to Prop : the Type universe
is predicative (i.e. not impredicative).
*)
Definition FalseBis : Prop := forall (P:Prop), P.
Lemma False_equiv : False <-> FalseBis.
Proof.
split.
- destruct 1.
- intro H. unfold FalseBis in *.
apply H.
Qed.
(* Alternative disjunction *)
Definition OrBis (P Q : Prop) : Prop :=
forall R:Prop, (P -> R) -> (Q -> R) -> R.
Lemma or_equiv P Q : P \/ Q <-> OrBis P Q.
Proof.
split.
- destruct 1.
+ unfold OrBis. intros R pr qr. apply pr, H.
+ intros R pr qr. apply qr, H.
- intro H. unfold OrBis in H. apply H.
+ now left.
+ now right.
Qed.
(* Alternative definition for exists *)
Definition ExistsBis {X}(P:X->Prop)
:= forall Q:Prop, (forall x, P x -> Q) -> Q.
Lemma Exists_equiv {X}(P:X->Prop) :
(exists x, P x) <-> ExistsBis P.
Proof.
split.
- intros (w,H). unfold ExistsBis.
intros Q H'. apply (H' w), H.
- intro H. unfold ExistsBis in H. apply H.
intros w Hw.
exists w. auto.
Qed.
(* Alternative conjunction *)
Definition AndBis (P Q : Prop) : Prop :=
forall R:Prop, (P -> Q -> R) -> R.
Lemma and_equiv P Q : P /\ Q <-> AndBis P Q.
Proof.
split.
- destruct 1. intros R pqr. apply pqr; auto.
- intro H. apply H. split; auto.
Qed.
Require Import List.
Import ListNotations.
Inductive alpha := M | I | U.
Definition word := list alpha.
Inductive lang : word -> Prop :=
| axiom : lang [M;I]
| rule1 x : lang (x ++ [I]) -> lang (x ++ [I;U])
| rule2 x : lang ([M] ++ x) -> lang ([M] ++ x ++ x)
| rule3 x y : lang (x ++ [I;I;I] ++ y) -> lang (x ++ [U] ++ y)
| rule4 x y : lang (x ++ [U;U] ++ y) -> lang (x ++ y).
Lemma starts_with_M w :
lang w -> match w with
| letter :: _ => letter = M
| [] => False
end.
Proof.
induction 1. (* the first unnamed hyp, i.e. (lang w) *)
- reflexivity.
- destruct x; simpl in *; auto.
- simpl; reflexivity.
- destruct x; simpl in *. discriminate.
auto.
- destruct x; simpl in *. discriminate.
auto.
Qed.
(* other possible style for the "match" *)
Lemma starts_with_M_bis w :
lang w -> match w with
| M :: _ => True
| _ => False
end.
Proof.
induction 1; auto; destruct x; simpl in *; easy.
Qed.
(* Statement via exists. Equivalent with the previous "match" statements,
but much harder to prove directly (need to exhibit all the witnesses,
hence all the rest of the words). *)
Lemma starts_with_M_ter w : lang w -> exists v, w = M :: v.
Proof.
intros H.
apply starts_with_M in H. destruct w.
- destruct H.
- exists w. rewrite H. auto.
Qed.
Inductive Z3 := Z0 | Z1 | Z2.
Notation "0" := Z0.
Notation "1" := Z1.
Notation "2" := Z2.
Definition succ z :=
match z with
| 0 => 1
| 1 => 2
| 2 => 0
end.
Definition add z z' :=
match z with
| 0 => z'
| 1 => succ z'
| 2 => succ (succ z')
end.
Infix "+" := add.
Compute 2 + 2.
Lemma succ3 : forall x, succ (succ (succ x)) = x.
Proof.
now destruct x.
Qed.
Lemma add_comm : forall x y, x+y = y+x.
Proof.
now destruct x, y.
Qed.
Lemma add_assoc : forall x y z, x+(y+z) = (x+y)+z.
Proof.
now destruct x, y, z.
Qed.
Lemma add_0 x : 0+x = x.
Proof.
reflexivity.
Qed.
Lemma add_succ x y : succ (x+y) = succ x + y.
Proof.
now destruct x, y.
Qed.
Lemma twice_nonzero x : x<>0 -> x+x<>0.
Proof.
now destruct x.
Qed.
Fixpoint occurI3 w : Z3 :=
match w with
| [] => 0
| I::w' => succ (occurI3 w')
| _::w' => occurI3 w'
end.
Lemma occurI3_app v w : occurI3 (v ++ w) = occurI3 v + occurI3 w.
Proof.
induction v; simpl.
- reflexivity.
- destruct a; auto.
rewrite IHv.
apply add_succ.
Qed.
Lemma lang_occurI3_nonzero w : lang w -> occurI3 w <> 0.
Proof.
induction 1; simpl in *; rewrite ?occurI3_app in *; simpl in *; try easy.
- now apply twice_nonzero.
- now rewrite succ3 in *.
Qed.
Lemma mu_puzzle : ~(lang [M;U]).
Proof.
intro H.
apply lang_occurI3_nonzero in H. simpl in H. easy.
Qed.
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