summaryrefslogtreecommitdiff
path: root/doc/RecTutorial/RecTutorial.v
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-10-14 17:51:11 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-10-14 17:51:11 +0200
commit3e96002677226c0cdaa8f355938a76cfb37a722a (patch)
tree3ca96e142fdb68e464d2f5f403f315282b94f922 /doc/RecTutorial/RecTutorial.v
parentf18e6146f4fd6ed5b8ded10a3e602f5f64f919f4 (diff)
Imported Upstream version 8.3upstream/8.3
Diffstat (limited to 'doc/RecTutorial/RecTutorial.v')
-rw-r--r--doc/RecTutorial/RecTutorial.v1232
1 files changed, 1232 insertions, 0 deletions
diff --git a/doc/RecTutorial/RecTutorial.v b/doc/RecTutorial/RecTutorial.v
new file mode 100644
index 00000000..28aaf752
--- /dev/null
+++ b/doc/RecTutorial/RecTutorial.v
@@ -0,0 +1,1232 @@
+Check (forall A:Type, (exists x:A, forall (y:A), x <> y) -> 2 = 3).
+
+
+
+Inductive nat : Set :=
+ | O : nat
+ | S : nat->nat.
+Check nat.
+Check O.
+Check S.
+
+Reset nat.
+Print nat.
+
+
+Print le.
+
+Theorem zero_leq_three: 0 <= 3.
+
+Proof.
+ constructor 2.
+ constructor 2.
+ constructor 2.
+ constructor 1.
+
+Qed.
+
+Print zero_leq_three.
+
+
+Lemma zero_leq_three': 0 <= 3.
+ repeat constructor.
+Qed.
+
+
+Lemma zero_lt_three : 0 < 3.
+Proof.
+ repeat constructor.
+Qed.
+
+Print zero_lt_three.
+
+Inductive le'(n:nat):nat -> Prop :=
+ | le'_n : le' n n
+ | le'_S : forall p, le' (S n) p -> le' n p.
+
+Hint Constructors le'.
+
+
+Require Import List.
+
+Print list.
+
+Check list.
+
+Check (nil (A:=nat)).
+
+Check (nil (A:= nat -> nat)).
+
+Check (fun A: Type => (cons (A:=A))).
+
+Check (cons 3 (cons 2 nil)).
+
+Check (nat :: bool ::nil).
+
+Check ((3<=4) :: True ::nil).
+
+Check (Prop::Set::nil).
+
+Require Import Bvector.
+
+Print vector.
+
+Check (Vnil nat).
+
+Check (fun (A:Type)(a:A)=> Vcons _ a _ (Vnil _)).
+
+Check (Vcons _ 5 _ (Vcons _ 3 _ (Vnil _))).
+
+Lemma eq_3_3 : 2 + 1 = 3.
+Proof.
+ reflexivity.
+Qed.
+Print eq_3_3.
+
+Lemma eq_proof_proof : refl_equal (2*6) = refl_equal (3*4).
+Proof.
+ reflexivity.
+Qed.
+Print eq_proof_proof.
+
+Lemma eq_lt_le : ( 2 < 4) = (3 <= 4).
+Proof.
+ reflexivity.
+Qed.
+
+Lemma eq_nat_nat : nat = nat.
+Proof.
+ reflexivity.
+Qed.
+
+Lemma eq_Set_Set : Set = Set.
+Proof.
+ reflexivity.
+Qed.
+
+Lemma eq_Type_Type : Type = Type.
+Proof.
+ reflexivity.
+Qed.
+
+
+Check (2 + 1 = 3).
+
+
+Check (Type = Type).
+
+Goal Type = Type.
+reflexivity.
+Qed.
+
+
+Print or.
+
+Print and.
+
+
+Print sumbool.
+
+Print ex.
+
+Require Import ZArith.
+Require Import Compare_dec.
+
+Check le_lt_dec.
+
+Definition max (n p :nat) := match le_lt_dec n p with
+ | left _ => p
+ | right _ => n
+ end.
+
+Theorem le_max : forall n p, n <= p -> max n p = p.
+Proof.
+ intros n p ; unfold max ; case (le_lt_dec n p); simpl.
+ trivial.
+ intros; absurd (p < p); eauto with arith.
+Qed.
+
+Extraction max.
+
+
+
+
+
+
+Inductive tree(A:Type) : Type :=
+ node : A -> forest A -> tree A
+with
+ forest (A: Type) : Type :=
+ nochild : forest A |
+ addchild : tree A -> forest A -> forest A.
+
+
+
+
+
+Inductive
+ even : nat->Prop :=
+ evenO : even O |
+ evenS : forall n, odd n -> even (S n)
+with
+ odd : nat->Prop :=
+ oddS : forall n, even n -> odd (S n).
+
+Lemma odd_49 : odd (7 * 7).
+ simpl; repeat constructor.
+Qed.
+
+
+
+Definition nat_case :=
+ fun (Q : Type)(g0 : Q)(g1 : nat -> Q)(n:nat) =>
+ match n return Q with
+ | 0 => g0
+ | S p => g1 p
+ end.
+
+Eval simpl in (nat_case nat 0 (fun p => p) 34).
+
+Eval simpl in (fun g0 g1 => nat_case nat g0 g1 34).
+
+Eval simpl in (fun g0 g1 => nat_case nat g0 g1 0).
+
+
+Definition pred (n:nat) := match n with O => O | S m => m end.
+
+Eval simpl in pred 56.
+
+Eval simpl in pred 0.
+
+Eval simpl in fun p => pred (S p).
+
+
+Definition xorb (b1 b2:bool) :=
+match b1, b2 with
+ | false, true => true
+ | true, false => true
+ | _ , _ => false
+end.
+
+
+ Definition pred_spec (n:nat) := {m:nat | n=0 /\ m=0 \/ n = S m}.
+
+
+ Definition predecessor : forall n:nat, pred_spec n.
+ intro n;case n.
+ unfold pred_spec;exists 0;auto.
+ unfold pred_spec; intro n0;exists n0; auto.
+ Defined.
+
+Print predecessor.
+
+Extraction predecessor.
+
+Theorem nat_expand :
+ forall n:nat, n = match n with 0 => 0 | S p => S p end.
+ intro n;case n;simpl;auto.
+Qed.
+
+Check (fun p:False => match p return 2=3 with end).
+
+Theorem fromFalse : False -> 0=1.
+ intro absurd.
+ contradiction.
+Qed.
+
+Section equality_elimination.
+ Variables (A: Type)
+ (a b : A)
+ (p : a = b)
+ (Q : A -> Type).
+ Check (fun H : Q a =>
+ match p in (eq _ y) return Q y with
+ refl_equal => H
+ end).
+
+End equality_elimination.
+
+
+Theorem trans : forall n m p:nat, n=m -> m=p -> n=p.
+Proof.
+ intros n m p eqnm.
+ case eqnm.
+ trivial.
+Qed.
+
+Lemma Rw : forall x y: nat, y = y * x -> y * x * x = y.
+ intros x y e; do 2 rewrite <- e.
+ reflexivity.
+Qed.
+
+
+Require Import Arith.
+
+Check mult_1_l.
+(*
+mult_1_l
+ : forall n : nat, 1 * n = n
+*)
+
+Check mult_plus_distr_r.
+(*
+mult_plus_distr_r
+ : forall n m p : nat, (n + m) * p = n * p + m * p
+
+*)
+
+Lemma mult_distr_S : forall n p : nat, n * p + p = (S n)* p.
+ simpl;auto with arith.
+Qed.
+
+Lemma four_n : forall n:nat, n+n+n+n = 4*n.
+ intro n;rewrite <- (mult_1_l n).
+
+ Undo.
+ intro n; pattern n at 1.
+
+
+ rewrite <- mult_1_l.
+ repeat rewrite mult_distr_S.
+ trivial.
+Qed.
+
+
+Section Le_case_analysis.
+ Variables (n p : nat)
+ (H : n <= p)
+ (Q : nat -> Prop)
+ (H0 : Q n)
+ (HS : forall m, n <= m -> Q (S m)).
+ Check (
+ match H in (_ <= q) return (Q q) with
+ | le_n => H0
+ | le_S m Hm => HS m Hm
+ end
+ ).
+
+
+End Le_case_analysis.
+
+
+Lemma predecessor_of_positive : forall n, 1 <= n -> exists p:nat, n = S p.
+Proof.
+ intros n H; case H.
+ exists 0; trivial.
+ intros m Hm; exists m;trivial.
+Qed.
+
+Definition Vtail_total
+ (A : Type) (n : nat) (v : vector A n) : vector A (pred n):=
+match v in (vector _ n0) return (vector A (pred n0)) with
+| Vnil => Vnil A
+| Vcons _ n0 v0 => v0
+end.
+
+Definition Vtail' (A:Type)(n:nat)(v:vector A n) : vector A (pred n).
+ intros A n v; case v.
+ simpl.
+ exact (Vnil A).
+ simpl.
+ auto.
+Defined.
+
+(*
+Inductive Lambda : Set :=
+ lambda : (Lambda -> False) -> Lambda.
+
+
+Error: Non strictly positive occurrence of "Lambda" in
+ "(Lambda -> False) -> Lambda"
+
+*)
+
+Section Paradox.
+ Variable Lambda : Set.
+ Variable lambda : (Lambda -> False) ->Lambda.
+
+ Variable matchL : Lambda -> forall Q:Prop, ((Lambda ->False) -> Q) -> Q.
+ (*
+ understand matchL Q l (fun h : Lambda -> False => t)
+
+ as match l return Q with lambda h => t end
+ *)
+
+ Definition application (f x: Lambda) :False :=
+ matchL f False (fun h => h x).
+
+ Definition Delta : Lambda := lambda (fun x : Lambda => application x x).
+
+ Definition loop : False := application Delta Delta.
+
+ Theorem two_is_three : 2 = 3.
+ Proof.
+ elim loop.
+ Qed.
+
+End Paradox.
+
+
+Require Import ZArith.
+
+
+
+Inductive itree : Set :=
+| ileaf : itree
+| inode : Z-> (nat -> itree) -> itree.
+
+Definition isingle l := inode l (fun i => ileaf).
+
+Definition t1 := inode 0 (fun n => isingle (Z_of_nat (2*n))).
+
+Definition t2 := inode 0
+ (fun n : nat =>
+ inode (Z_of_nat n)
+ (fun p => isingle (Z_of_nat (n*p)))).
+
+
+Inductive itree_le : itree-> itree -> Prop :=
+ | le_leaf : forall t, itree_le ileaf t
+ | le_node : forall l l' s s',
+ Zle l l' ->
+ (forall i, exists j:nat, itree_le (s i) (s' j)) ->
+ itree_le (inode l s) (inode l' s').
+
+
+Theorem itree_le_trans :
+ forall t t', itree_le t t' ->
+ forall t'', itree_le t' t'' -> itree_le t t''.
+ induction t.
+ constructor 1.
+
+ intros t'; case t'.
+ inversion 1.
+ intros z0 i0 H0.
+ intro t'';case t''.
+ inversion 1.
+ intros.
+ inversion_clear H1.
+ constructor 2.
+ inversion_clear H0;eauto with zarith.
+ inversion_clear H0.
+ intro i2; case (H4 i2).
+ intros.
+ generalize (H i2 _ H0).
+ intros.
+ case (H3 x);intros.
+ generalize (H5 _ H6).
+ exists x0;auto.
+Qed.
+
+
+
+Inductive itree_le' : itree-> itree -> Prop :=
+ | le_leaf' : forall t, itree_le' ileaf t
+ | le_node' : forall l l' s s' g,
+ Zle l l' ->
+ (forall i, itree_le' (s i) (s' (g i))) ->
+ itree_le' (inode l s) (inode l' s').
+
+
+
+
+
+Lemma t1_le_t2 : itree_le t1 t2.
+ unfold t1, t2.
+ constructor.
+ auto with zarith.
+ intro i; exists (2 * i).
+ unfold isingle.
+ constructor.
+ auto with zarith.
+ exists i;constructor.
+Qed.
+
+
+
+Lemma t1_le'_t2 : itree_le' t1 t2.
+ unfold t1, t2.
+ constructor 2 with (fun i : nat => 2 * i).
+ auto with zarith.
+ unfold isingle;
+ intro i ; constructor 2 with (fun i :nat => i).
+ auto with zarith.
+ constructor .
+Qed.
+
+
+Require Import List.
+
+Inductive ltree (A:Set) : Set :=
+ lnode : A -> list (ltree A) -> ltree A.
+
+Inductive prop : Prop :=
+ prop_intro : Prop -> prop.
+
+Check (prop_intro prop).
+
+Inductive ex_Prop (P : Prop -> Prop) : Prop :=
+ exP_intro : forall X : Prop, P X -> ex_Prop P.
+
+Lemma ex_Prop_inhabitant : ex_Prop (fun P => P -> P).
+Proof.
+ exists (ex_Prop (fun P => P -> P)).
+ trivial.
+Qed.
+
+
+
+
+(*
+
+Check (fun (P:Prop->Prop)(p: ex_Prop P) =>
+ match p with exP_intro X HX => X end).
+Error:
+Incorrect elimination of "p" in the inductive type
+"ex_Prop", the return type has sort "Type" while it should be
+"Prop"
+
+Elimination of an inductive object of sort "Prop"
+is not allowed on a predicate in sort "Type"
+because proofs can be eliminated only to build proofs
+
+*)
+
+
+Inductive typ : Type :=
+ typ_intro : Type -> typ.
+
+Definition typ_inject: typ.
+split.
+exact typ.
+(*
+Defined.
+
+Error: Universe Inconsistency.
+*)
+Abort.
+(*
+
+Inductive aSet : Set :=
+ aSet_intro: Set -> aSet.
+
+
+User error: Large non-propositional inductive types must be in Type
+
+*)
+
+Inductive ex_Set (P : Set -> Prop) : Type :=
+ exS_intro : forall X : Set, P X -> ex_Set P.
+
+
+Inductive comes_from_the_left (P Q:Prop): P \/ Q -> Prop :=
+ c1 : forall p, comes_from_the_left P Q (or_introl (A:=P) Q p).
+
+Goal (comes_from_the_left _ _ (or_introl True I)).
+split.
+Qed.
+
+Goal ~(comes_from_the_left _ _ (or_intror True I)).
+ red;inversion 1.
+ (* discriminate H0.
+ *)
+Abort.
+
+Reset comes_from_the_left.
+
+(*
+
+
+
+
+
+
+ Definition comes_from_the_left (P Q:Prop)(H:P \/ Q): Prop :=
+ match H with
+ | or_introl p => True
+ | or_intror q => False
+ end.
+
+Error:
+Incorrect elimination of "H" in the inductive type
+"or", the return type has sort "Type" while it should be
+"Prop"
+
+Elimination of an inductive object of sort "Prop"
+is not allowed on a predicate in sort "Type"
+because proofs can be eliminated only to build proofs
+
+*)
+
+Definition comes_from_the_left_sumbool
+ (P Q:Prop)(x:{P}+{Q}): Prop :=
+ match x with
+ | left p => True
+ | right q => False
+ end.
+
+
+
+
+Close Scope Z_scope.
+
+
+
+
+
+Theorem S_is_not_O : forall n, S n <> 0.
+
+Definition Is_zero (x:nat):= match x with
+ | 0 => True
+ | _ => False
+ end.
+ Lemma O_is_zero : forall m, m = 0 -> Is_zero m.
+ Proof.
+ intros m H; subst m.
+ (*
+ ============================
+ Is_zero 0
+ *)
+ simpl;trivial.
+ Qed.
+
+ red; intros n Hn.
+ apply O_is_zero with (m := S n).
+ assumption.
+Qed.
+
+Theorem disc2 : forall n, S (S n) <> 1.
+Proof.
+ intros n Hn; discriminate.
+Qed.
+
+
+Theorem disc3 : forall n, S (S n) = 0 -> forall Q:Prop, Q.
+Proof.
+ intros n Hn Q.
+ discriminate.
+Qed.
+
+
+
+Theorem inj_succ : forall n m, S n = S m -> n = m.
+Proof.
+
+
+Lemma inj_pred : forall n m, n = m -> pred n = pred m.
+Proof.
+ intros n m eq_n_m.
+ rewrite eq_n_m.
+ trivial.
+Qed.
+
+ intros n m eq_Sn_Sm.
+ apply inj_pred with (n:= S n) (m := S m); assumption.
+Qed.
+
+Lemma list_inject : forall (A:Type)(a b :A)(l l':list A),
+ a :: b :: l = b :: a :: l' -> a = b /\ l = l'.
+Proof.
+ intros A a b l l' e.
+ injection e.
+ auto.
+Qed.
+
+
+Theorem not_le_Sn_0 : forall n:nat, ~ (S n <= 0).
+Proof.
+ red; intros n H.
+ case H.
+Undo.
+
+Lemma not_le_Sn_0_with_constraints :
+ forall n p , S n <= p -> p = 0 -> False.
+Proof.
+ intros n p H; case H ;
+ intros; discriminate.
+Qed.
+
+eapply not_le_Sn_0_with_constraints; eauto.
+Qed.
+
+
+Theorem not_le_Sn_0' : forall n:nat, ~ (S n <= 0).
+Proof.
+ red; intros n H ; inversion H.
+Qed.
+
+Derive Inversion le_Sn_0_inv with (forall n :nat, S n <= 0).
+Check le_Sn_0_inv.
+
+Theorem le_Sn_0'' : forall n p : nat, ~ S n <= 0 .
+Proof.
+ intros n p H;
+ inversion H using le_Sn_0_inv.
+Qed.
+
+Derive Inversion_clear le_Sn_0_inv' with (forall n :nat, S n <= 0).
+Check le_Sn_0_inv'.
+
+
+Theorem le_reverse_rules :
+ forall n m:nat, n <= m ->
+ n = m \/
+ exists p, n <= p /\ m = S p.
+Proof.
+ intros n m H; inversion H.
+ left;trivial.
+ right; exists m0; split; trivial.
+Restart.
+ intros n m H; inversion_clear H.
+ left;trivial.
+ right; exists m0; split; trivial.
+Qed.
+
+Inductive ArithExp : Set :=
+ Zero : ArithExp
+ | Succ : ArithExp -> ArithExp
+ | Plus : ArithExp -> ArithExp -> ArithExp.
+
+Inductive RewriteRel : ArithExp -> ArithExp -> Prop :=
+ RewSucc : forall e1 e2 :ArithExp,
+ RewriteRel e1 e2 -> RewriteRel (Succ e1) (Succ e2)
+ | RewPlus0 : forall e:ArithExp,
+ RewriteRel (Plus Zero e) e
+ | RewPlusS : forall e1 e2:ArithExp,
+ RewriteRel e1 e2 ->
+ RewriteRel (Plus (Succ e1) e2) (Succ (Plus e1 e2)).
+
+
+
+Fixpoint plus (n p:nat) {struct n} : nat :=
+ match n with
+ | 0 => p
+ | S m => S (plus m p)
+ end.
+
+Fixpoint plus' (n p:nat) {struct p} : nat :=
+ match p with
+ | 0 => n
+ | S q => S (plus' n q)
+ end.
+
+Fixpoint plus'' (n p:nat) {struct n} : nat :=
+ match n with
+ | 0 => p
+ | S m => plus'' m (S p)
+ end.
+
+
+Fixpoint even_test (n:nat) : bool :=
+ match n
+ with 0 => true
+ | 1 => false
+ | S (S p) => even_test p
+ end.
+
+
+Reset even_test.
+
+Fixpoint even_test (n:nat) : bool :=
+ match n
+ with
+ | 0 => true
+ | S p => odd_test p
+ end
+with odd_test (n:nat) : bool :=
+ match n
+ with
+ | 0 => false
+ | S p => even_test p
+ end.
+
+
+
+Eval simpl in even_test.
+
+
+
+Eval simpl in (fun x : nat => even_test x).
+
+Eval simpl in (fun x : nat => plus 5 x).
+Eval simpl in (fun x : nat => even_test (plus 5 x)).
+
+Eval simpl in (fun x : nat => even_test (plus x 5)).
+
+
+Section Principle_of_Induction.
+Variable P : nat -> Prop.
+Hypothesis base_case : P 0.
+Hypothesis inductive_step : forall n:nat, P n -> P (S n).
+Fixpoint nat_ind (n:nat) : (P n) :=
+ match n return P n with
+ | 0 => base_case
+ | S m => inductive_step m (nat_ind m)
+ end.
+
+End Principle_of_Induction.
+
+Scheme Even_induction := Minimality for even Sort Prop
+with Odd_induction := Minimality for odd Sort Prop.
+
+Theorem even_plus_four : forall n:nat, even n -> even (4+n).
+Proof.
+ intros n H.
+ elim H using Even_induction with (P0 := fun n => odd (4+n));
+ simpl;repeat constructor;assumption.
+Qed.
+
+
+Section Principle_of_Double_Induction.
+Variable P : nat -> nat ->Prop.
+Hypothesis base_case1 : forall x:nat, P 0 x.
+Hypothesis base_case2 : forall x:nat, P (S x) 0.
+Hypothesis inductive_step : forall n m:nat, P n m -> P (S n) (S m).
+Fixpoint nat_double_ind (n m:nat){struct n} : P n m :=
+ match n, m return P n m with
+ | 0 , x => base_case1 x
+ | (S x), 0 => base_case2 x
+ | (S x), (S y) => inductive_step x y (nat_double_ind x y)
+ end.
+End Principle_of_Double_Induction.
+
+Section Principle_of_Double_Recursion.
+Variable P : nat -> nat -> Type.
+Hypothesis base_case1 : forall x:nat, P 0 x.
+Hypothesis base_case2 : forall x:nat, P (S x) 0.
+Hypothesis inductive_step : forall n m:nat, P n m -> P (S n) (S m).
+Fixpoint nat_double_rect (n m:nat){struct n} : P n m :=
+ match n, m return P n m with
+ | 0 , x => base_case1 x
+ | (S x), 0 => base_case2 x
+ | (S x), (S y) => inductive_step x y (nat_double_rect x y)
+ end.
+End Principle_of_Double_Recursion.
+
+Definition min : nat -> nat -> nat :=
+ nat_double_rect (fun (x y:nat) => nat)
+ (fun (x:nat) => 0)
+ (fun (y:nat) => 0)
+ (fun (x y r:nat) => S r).
+
+Eval compute in (min 5 8).
+Eval compute in (min 8 5).
+
+
+
+Lemma not_circular : forall n:nat, n <> S n.
+Proof.
+ intro n.
+ apply nat_ind with (P:= fun n => n <> S n).
+ discriminate.
+ red; intros n0 Hn0 eqn0Sn0;injection eqn0Sn0;trivial.
+Qed.
+
+Definition eq_nat_dec : forall n p:nat , {n=p}+{n <> p}.
+Proof.
+ intros n p.
+ apply nat_double_rect with (P:= fun (n q:nat) => {q=p}+{q <> p}).
+Undo.
+ pattern p,n.
+ elim n using nat_double_rect.
+ destruct x; auto.
+ destruct x; auto.
+ intros n0 m H; case H.
+ intro eq; rewrite eq ; auto.
+ intro neg; right; red ; injection 1; auto.
+Defined.
+
+Definition eq_nat_dec' : forall n p:nat, {n=p}+{n <> p}.
+ decide equality.
+Defined.
+
+
+
+Require Import Le.
+Lemma le'_le : forall n p, le' n p -> n <= p.
+Proof.
+ induction 1;auto with arith.
+Qed.
+
+Lemma le'_n_Sp : forall n p, le' n p -> le' n (S p).
+Proof.
+ induction 1;auto.
+Qed.
+
+Hint Resolve le'_n_Sp.
+
+
+Lemma le_le' : forall n p, n<=p -> le' n p.
+Proof.
+ induction 1;auto with arith.
+Qed.
+
+
+Print Acc.
+
+
+Require Import Minus.
+
+(*
+Fixpoint div (x y:nat){struct x}: nat :=
+ if eq_nat_dec x 0
+ then 0
+ else if eq_nat_dec y 0
+ then x
+ else S (div (x-y) y).
+
+Error:
+Recursive definition of div is ill-formed.
+In environment
+div : nat -> nat -> nat
+x : nat
+y : nat
+_ : x <> 0
+_ : y <> 0
+
+Recursive call to div has principal argument equal to
+"x - y"
+instead of a subterm of x
+
+*)
+
+Lemma minus_smaller_S: forall x y:nat, x - y < S x.
+Proof.
+ intros x y; pattern y, x;
+ elim x using nat_double_ind.
+ destruct x0; auto with arith.
+ simpl; auto with arith.
+ simpl; auto with arith.
+Qed.
+
+Lemma minus_smaller_positive : forall x y:nat, x <>0 -> y <> 0 ->
+ x - y < x.
+Proof.
+ destruct x; destruct y;
+ ( simpl;intros; apply minus_smaller_S ||
+ intros; absurd (0=0); auto).
+Qed.
+
+Definition minus_decrease : forall x y:nat, Acc lt x ->
+ x <> 0 ->
+ y <> 0 ->
+ Acc lt (x-y).
+Proof.
+ intros x y H; case H.
+ intros Hz posz posy.
+ apply Hz; apply minus_smaller_positive; assumption.
+Defined.
+
+Print minus_decrease.
+
+
+
+Definition div_aux (x y:nat)(H: Acc lt x):nat.
+ fix 3.
+ intros.
+ refine (if eq_nat_dec x 0
+ then 0
+ else if eq_nat_dec y 0
+ then y
+ else div_aux (x-y) y _).
+ apply (minus_decrease x y H);assumption.
+Defined.
+
+
+Print div_aux.
+(*
+div_aux =
+(fix div_aux (x y : nat) (H : Acc lt x) {struct H} : nat :=
+ match eq_nat_dec x 0 with
+ | left _ => 0
+ | right _ =>
+ match eq_nat_dec y 0 with
+ | left _ => y
+ | right _0 => div_aux (x - y) y (minus_decrease x y H _ _0)
+ end
+ end)
+ : forall x : nat, nat -> Acc lt x -> nat
+*)
+
+Require Import Wf_nat.
+Definition div x y := div_aux x y (lt_wf x).
+
+Extraction div.
+(*
+let div x y =
+ div_aux x y
+*)
+
+Extraction div_aux.
+
+(*
+let rec div_aux x y =
+ match eq_nat_dec x O with
+ | Left -> O
+ | Right ->
+ (match eq_nat_dec y O with
+ | Left -> y
+ | Right -> div_aux (minus x y) y)
+*)
+
+Lemma vector0_is_vnil : forall (A:Type)(v:vector A 0), v = Vnil A.
+Proof.
+ intros A v;inversion v.
+Abort.
+
+(*
+ Lemma vector0_is_vnil_aux : forall (A:Type)(n:nat)(v:vector A n),
+ n= 0 -> v = Vnil A.
+
+Toplevel input, characters 40281-40287
+> Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:vector A n), n= 0 -> v = Vnil A.
+> ^^^^^^
+Error: In environment
+A : Set
+n : nat
+v : vector A n
+e : n = 0
+The term "Vnil A" has type "vector A 0" while it is expected to have type
+ "vector A n"
+*)
+ Require Import JMeq.
+
+
+(* On devrait changer Set en Type ? *)
+
+Lemma vector0_is_vnil_aux : forall (A:Type)(n:nat)(v:vector A n),
+ n= 0 -> JMeq v (Vnil A).
+Proof.
+ destruct v.
+ auto.
+ intro; discriminate.
+Qed.
+
+Lemma vector0_is_vnil : forall (A:Type)(v:vector A 0), v = Vnil A.
+Proof.
+ intros a v;apply JMeq_eq.
+ apply vector0_is_vnil_aux.
+ trivial.
+Qed.
+
+
+Implicit Arguments Vcons [A n].
+Implicit Arguments Vnil [A].
+Implicit Arguments Vhead [A n].
+Implicit Arguments Vtail [A n].
+
+Definition Vid : forall (A : Type)(n:nat), vector A n -> vector A n.
+Proof.
+ destruct n; intro v.
+ exact Vnil.
+ exact (Vcons (Vhead v) (Vtail v)).
+Defined.
+
+Eval simpl in (fun (A:Type)(v:vector A 0) => (Vid _ _ v)).
+
+Eval simpl in (fun (A:Type)(v:vector A 0) => v).
+
+
+
+Lemma Vid_eq : forall (n:nat) (A:Type)(v:vector A n), v=(Vid _ n v).
+Proof.
+ destruct v.
+ reflexivity.
+ reflexivity.
+Defined.
+
+Theorem zero_nil : forall A (v:vector A 0), v = Vnil.
+Proof.
+ intros.
+ change (Vnil (A:=A)) with (Vid _ 0 v).
+ apply Vid_eq.
+Defined.
+
+
+Theorem decomp :
+ forall (A : Type) (n : nat) (v : vector A (S n)),
+ v = Vcons (Vhead v) (Vtail v).
+Proof.
+ intros.
+ change (Vcons (Vhead v) (Vtail v)) with (Vid _ (S n) v).
+ apply Vid_eq.
+Defined.
+
+
+
+Definition vector_double_rect :
+ forall (A:Type) (P: forall (n:nat),(vector A n)->(vector A n) -> Type),
+ P 0 Vnil Vnil ->
+ (forall n (v1 v2 : vector A n) a b, P n v1 v2 ->
+ P (S n) (Vcons a v1) (Vcons b v2)) ->
+ forall n (v1 v2 : vector A n), P n v1 v2.
+ induction n.
+ intros; rewrite (zero_nil _ v1); rewrite (zero_nil _ v2).
+ auto.
+ intros v1 v2; rewrite (decomp _ _ v1);rewrite (decomp _ _ v2).
+ apply X0; auto.
+Defined.
+
+Require Import Bool.
+
+Definition bitwise_or n v1 v2 : vector bool n :=
+ vector_double_rect bool (fun n v1 v2 => vector bool n)
+ Vnil
+ (fun n v1 v2 a b r => Vcons (orb a b) r) n v1 v2.
+
+
+Fixpoint vector_nth (A:Type)(n:nat)(p:nat)(v:vector A p){struct v}
+ : option A :=
+ match n,v with
+ _ , Vnil => None
+ | 0 , Vcons b _ _ => Some b
+ | S n', Vcons _ p' v' => vector_nth A n' p' v'
+ end.
+
+Implicit Arguments vector_nth [A p].
+
+
+Lemma nth_bitwise : forall (n:nat) (v1 v2: vector bool n) i a b,
+ vector_nth i v1 = Some a ->
+ vector_nth i v2 = Some b ->
+ vector_nth i (bitwise_or _ v1 v2) = Some (orb a b).
+Proof.
+ intros n v1 v2; pattern n,v1,v2.
+ apply vector_double_rect.
+ simpl.
+ destruct i; discriminate 1.
+ destruct i; simpl;auto.
+ injection 1; injection 2;intros; subst a; subst b; auto.
+Qed.
+
+ Set Implicit Arguments.
+
+ CoInductive Stream (A:Type) : Type :=
+ | Cons : A -> Stream A -> Stream A.
+
+ CoInductive LList (A: Type) : Type :=
+ | LNil : LList A
+ | LCons : A -> LList A -> LList A.
+
+
+
+
+
+ Definition head (A:Type)(s : Stream A) := match s with Cons a s' => a end.
+
+ Definition tail (A : Type)(s : Stream A) :=
+ match s with Cons a s' => s' end.
+
+ CoFixpoint repeat (A:Type)(a:A) : Stream A := Cons a (repeat a).
+
+ CoFixpoint iterate (A: Type)(f: A -> A)(a : A) : Stream A:=
+ Cons a (iterate f (f a)).
+
+ CoFixpoint map (A B:Type)(f: A -> B)(s : Stream A) : Stream B:=
+ match s with Cons a tl => Cons (f a) (map f tl) end.
+
+Eval simpl in (fun (A:Type)(a:A) => repeat a).
+
+Eval simpl in (fun (A:Type)(a:A) => head (repeat a)).
+
+
+CoInductive EqSt (A: Type) : Stream A -> Stream A -> Prop :=
+ eqst : forall s1 s2: Stream A,
+ head s1 = head s2 ->
+ EqSt (tail s1) (tail s2) ->
+ EqSt s1 s2.
+
+
+Section Parks_Principle.
+Variable A : Type.
+Variable R : Stream A -> Stream A -> Prop.
+Hypothesis bisim1 : forall s1 s2:Stream A, R s1 s2 ->
+ head s1 = head s2.
+Hypothesis bisim2 : forall s1 s2:Stream A, R s1 s2 ->
+ R (tail s1) (tail s2).
+
+CoFixpoint park_ppl : forall s1 s2:Stream A, R s1 s2 ->
+ EqSt s1 s2 :=
+ fun s1 s2 (p : R s1 s2) =>
+ eqst s1 s2 (bisim1 p)
+ (park_ppl (bisim2 p)).
+End Parks_Principle.
+
+
+Theorem map_iterate : forall (A:Type)(f:A->A)(x:A),
+ EqSt (iterate f (f x)) (map f (iterate f x)).
+Proof.
+ intros A f x.
+ apply park_ppl with
+ (R:= fun s1 s2 => exists x: A,
+ s1 = iterate f (f x) /\ s2 = map f (iterate f x)).
+
+ intros s1 s2 (x0,(eqs1,eqs2));rewrite eqs1;rewrite eqs2;reflexivity.
+ intros s1 s2 (x0,(eqs1,eqs2)).
+ exists (f x0);split;[rewrite eqs1|rewrite eqs2]; reflexivity.
+ exists x;split; reflexivity.
+Qed.
+
+Ltac infiniteproof f :=
+ cofix f; constructor; [clear f| simpl; try (apply f; clear f)].
+
+
+Theorem map_iterate' : forall (A:Type)(f:A->A)(x:A),
+ EqSt (iterate f (f x)) (map f (iterate f x)).
+infiniteproof map_iterate'.
+ reflexivity.
+Qed.
+
+
+Implicit Arguments LNil [A].
+
+Lemma Lnil_not_Lcons : forall (A:Type)(a:A)(l:LList A),
+ LNil <> (LCons a l).
+ intros;discriminate.
+Qed.
+
+Lemma injection_demo : forall (A:Type)(a b : A)(l l': LList A),
+ LCons a (LCons b l) = LCons b (LCons a l') ->
+ a = b /\ l = l'.
+Proof.
+ intros A a b l l' e; injection e; auto.
+Qed.
+
+
+Inductive Finite (A:Type) : LList A -> Prop :=
+| Lnil_fin : Finite (LNil (A:=A))
+| Lcons_fin : forall a l, Finite l -> Finite (LCons a l).
+
+CoInductive Infinite (A:Type) : LList A -> Prop :=
+| LCons_inf : forall a l, Infinite l -> Infinite (LCons a l).
+
+Lemma LNil_not_Infinite : forall (A:Type), ~ Infinite (LNil (A:=A)).
+Proof.
+ intros A H;inversion H.
+Qed.
+
+Lemma Finite_not_Infinite : forall (A:Type)(l:LList A),
+ Finite l -> ~ Infinite l.
+Proof.
+ intros A l H; elim H.
+ apply LNil_not_Infinite.
+ intros a l0 F0 I0' I1.
+ case I0'; inversion_clear I1.
+ trivial.
+Qed.
+
+Lemma Not_Finite_Infinite : forall (A:Type)(l:LList A),
+ ~ Finite l -> Infinite l.
+Proof.
+ cofix H.
+ destruct l.
+ intro; absurd (Finite (LNil (A:=A)));[auto|constructor].
+ constructor.
+ apply H.
+ red; intro H1;case H0.
+ constructor.
+ trivial.
+Qed.
+
+
+