Set Implicit Arguments.
Require Import Setoid.

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

(** * Modules *)

(** ** Specification *)
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 x a = true.
Hypothesis in_rem : forall a l x, 
     ins x (rem a l) = true <-> ins x l = true /\ eqb x a = false.

End FinSet.

(** ** Implementation by unordered lists and repetition *)
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.
Qed.

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.
Qed.

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.
Qed.

Lemma eqb_trans :
  forall x y z, eqb x y = true -> eqb x z = eqb y z.
unfold eqb; intros x y z eqxy.
apply eqb_elim_true in eqxy; destruct eqxy as (lexy,leyx).
case_eq (leb y z); simpl; [intro leyz|intro nleyz].
 rewrite (leb_trans lexy leyz); simpl.
 case_eq (leb z y); simpl; [intro lezy|intro nlezy].
  apply leb_trans with y; trivial.

  case_eq (leb z x); trivial; intro lezx.
  rewrite (leb_trans lezx lexy) in nlezy; discriminate.

 case_eq (leb x z); simpl; trivial; intro lexz.
 rewrite (leb_trans leyx lexz) in nleyz; discriminate.
Qed.

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.
Qed.

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.
Qed.

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.
  rewrite eqb_trans with (1:=H0).
  rewrite (eqb_sym a x).
  split; intros.
   destruct H1.
   rewrite H2; auto.

   destruct H1.
   rewrite H2 in H1; auto.

  split; intros.
   case_eq (eqb a0 x); intros.
    rewrite eqb_trans with (1:=H2) in H0; auto.

    rewrite H2 in H1.
    rewrite H in H1; trivial.

   case_eq (eqb a0 x); trivial; intro.
   rewrite H.
   rewrite H2 in H1; trivial. 
Qed.

End FSetList.