(* Comme en ML *) Inductive letter : Set := a | b. Definition int_of_letter (x:letter) := match x with | a => 0 | b => 1 end. Fixpoint f (n:nat) : nat := match n with | O => 1 | (S n) => f n + f n end. Eval compute in (f 3). (* Plus fort que ML *) Section sec. Variable A B: Prop. Fixpoint fl (n:nat) : Prop := match n with | O => A | (S n) => A -> fl n end. Eval compute in (fl 3). Lemma correct : forall n, fl (S n). induction n; simpl in * |- * . trivial. trivial. Qed. Lemma test1 : A -> A -> A -> A -> A -> A -> A. change (fl 6). apply correct. Qed. Print test1. Definition prop_of x := match x with | a => A | b => B end. Require Import List. Definition word := list letter. Fixpoint decode (l: word) (y: letter) {struct l} : Prop := match l with | nil => prop_of y | x :: l => prop_of x -> decode l y end. Eval compute in (decode (a :: b :: a :: b :: nil) b). Lemma weaken_decode : forall l y, prop_of y -> decode l y. induction l; simpl; auto. Defined. (* *) Definition eqlb x y : bool := match x, y with | a, a => true | b, b => true | _, _ => false end. Fixpoint inb (l: word) (y: letter) {struct l} : bool := match l with | nil => false | x :: l => if (eqlb x y) then true else (inb l y) end. Eval compute in (inb (a :: a :: a :: a :: nil) b). Theorem correctness : forall l y, inb l y = true -> decode l y. induction l as [|x l IHl]; simpl. intros y F. discriminate F. intros y. destruct x; destruct y; intro e; simpl in e |- . apply weaken_decode. intro; apply IHl; auto. intro; apply IHl; auto. apply weaken_decode. Defined. Lemma test3 : A -> B -> A -> A -> B. change (decode (a :: b :: a :: a :: nil) b). apply correctness. reflexivity. Defined. Print test3. Lemma test4 : A -> B -> A -> A -> B. auto. Show Proof. Defined. Goal test3 = test4. reflexivity. Qed. (* *) Coercion is_true (b:bool) : Prop := if b then True else False. Definition inP l y := is_true (inb l y). Eval compute in (inP (a :: b :: a :: b :: nil) b). (* En logique minimale *) Definition eqPK x y P : Prop := match x, y with | a, a => True | b, b => True | _, _ => P end. Fixpoint inPK (l: word) (y: letter) (P: Prop) {struct l} : Prop := match l with | nil => P | x :: l => eqPK x y (inPK l y P) end. Eval compute in (inPK (a :: b :: a :: a :: nil) b (a=b)). Theorem correctnessPK : forall (P:Prop) y l, (P -> decode l y) -> inPK l y P -> decode l y. induction l as [|x l IHl]; simpl. intros py; exact py. destruct y; destruct x. intros. apply weaken_decode. trivial. simpl. intros. apply IHl; auto. simpl. intros. apply IHl; auto. intros. apply weaken_decode. trivial. Defined. Theorem correctnessP1 : forall y l, inPK l y (decode l y) -> decode l y. intros y l. apply (correctnessPK (decode l y)). trivial. Qed. Lemma testPK : A -> B -> A -> A -> B. change (decode (a :: b :: a :: a :: nil) b). apply correctnessP1. simpl. trivial. Qed. Print testPK. Lemma failP : A -> A -> A -> A -> B. change (decode (a :: a :: a :: a :: nil) b). apply correctnessP1. simpl. Abort.