Set Implicit Arguments.

(** * Monades *)
(** ** Exceptions *)
Inductive tree : Type := 
     Leaf : nat -> tree | Node : tree -> tree -> tree.

Fixpoint multe (t:tree) : option nat := 
   match t with Leaf 0 => None | Leaf n => Some n 
       | Node t1 t2 => 
            match multe t1, multe t2 with 
              Some n1,  Some n2 => Some (n1 * n2) 
            | _,_ => None
            end
   end.

Definition mult (t:tree) : nat := 
   match multe t with Some n => n | None => 0 end.

Section Exception.
Definition M A := option A.
Definition unit : forall A, A -> M A := fun A x => Some x.
Definition bind : forall A B, M A -> (A -> M B) -> M B := 
     fun A B a f => match a with Some x => f x | None => None end.
Definition raise : forall A, M A := @None.
Definition try : forall A, M A -> A -> A 
    := fun A a z => match a with Some x => x | _ => z end.

Fixpoint multe2 (t:tree) : M nat := 
   match t with Leaf 0 => raise nat | Leaf n => unit n 
       | Node t1 t2 => 
            bind (multe2 t1)
             (fun n1 => bind (multe2 t2) 
                                     (fun n2 => unit (n1 * n2)))
   end.

Definition mult2 (t:tree) : nat := try (multe2 t) 0.
End Exception.

(** ** Non determinisme *)
Module NonDeterminisme.
Require Export List.
Open Scope list_scope.
Definition M A := list A.
Definition unit : forall A, A -> M A := fun A x => x::nil.
Definition bind : forall A B, M A -> (A -> M B) -> M B := 
     fun A B a f => fold_left (fun l ai => (f ai ++ l)) a nil.
Definition par : forall A, M A -> M A -> M A := fun A a b => a++b.

(** * Preuve par reflexion *)

(** * Modules *)

(** ** Sp\u00e9cification *)
Module Type Order.
Variable A:Type.
Variable leb:A->A->bool.
Hypothesis leb_refl : forall x, leb x x = true.
Hypothesis leb_trans : forall x y z, 
     leb x y = true -> leb y z = true -> leb x z = true.
Hint Resolve leb_refl.
End Order.

Module Type FinSet.
Declare Module O:Order.
Import O.
Variable t:Type.
Variable empty:t.
Variable ins : A->t->bool.
Variable add: A -> t -> t.
Variable rem : A -> t -> t.
Definition eqb x y : bool :=andb (leb x y) (leb y x).
Hypothesis in_empty : forall x, ins x empty=false.
Hypothesis in_add : forall a l x, 
     ins x (add a l) =true <-> ins x l = true \/ eqb a x = true.
Hypothesis in_rem : forall a l x, 
     ins x (rem a l) =true <-> ins x l = true /\ eqb a x = false.                                             
End FinSet.

(** ** Implantation par des listes non tri\u00e9es avec r\u00e9p\u00e9tition *)
Require Export List.
Module FSetList (O:Order) <: FinSet.
Module O:=O.
Import O.
Definition t := list A.
Definition empty:t :=nil.
Definition add: A -> t -> t:= cons (A:=A).

Definition eqb x y : bool :=andb (leb x y) (leb y x).

Lemma eqb_sym : forall x y, eqb x y = eqb y x.
unfold eqb; intros; case (leb x y); case (leb y x); simpl; auto.
Save.

Lemma eqb_elim_true 
     : forall x y, eqb x y = true -> leb x y = true /\ leb y x = true.
unfold eqb; intros x y; case (leb x y); intuition.
Save.

Lemma eqb_elim_false 
     : forall x y, eqb x y = false -> leb x y = false \/ leb y x = false.
unfold eqb; intros x y; case (leb x y); intuition.
Save.

Lemma eqb_trans 
  : forall x y z, eqb x y = true -> eqb x z = eqb y z.
unfold eqb; intros x y z H; case (eqb_elim_true x y H); intros.
case_eq (leb x z); simpl; intuition.
rewrite (leb_trans H1 H2); simpl.
case_eq (leb z x); simpl; intuition.
rewrite (leb_trans H3 H0); simpl; trivial.

case_eq (leb y z); simpl; intuition.
case_eq (leb z x); simpl; intuition.

rewrite (leb_sym z x); rewrite (leb_sym z y); rewrite H; auto.
rewrite (leb_trans H H2); simpl.
apply leb_trans with y; auto.
Save.

Fixpoint ins (a: A) (l:t) {struct l}: bool := match l with 
      nil => false 
  | cons b m => if eqb b a then true else ins a m 
   end.

Fixpoint rem (a: A) (l:t) {struct l}: t := match l with 
      nil => nil 
  | cons b m => if eqb b a then rem a m else cons b (rem a m) 
   end.

Lemma in_empty : forall x, ins x empty=false.
trivial.
Save.

Lemma in_add : forall a l x, 
     ins x (add a l) =true <-> ins x l = true \/ eqb x a = true.
simpl; intros.
rewrite eqb_sym.
case (eqb x a); simpl; intuition.
Save.

Lemma in_rem : forall a l x, 
     ins x (rem a l) =true <-> ins x l = true /\ eqb x a = false.  
intros; elim l; simpl; intros.
intuition.
discriminate.
case_eq (eqb a0 a); simpl; intros.
rewrite H.
case_eq (eqb x a); simpl; intros.
intuition discriminate.
replace (eqb a0 x) with false.
intuition.




Definition 

End FSetList.