(* 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.