Module OptionMonad

Require Export Setoid.
Require Export Relation_Definitions.
Require Export Morphisms.
Require Export Bool.
Require Export Sumbool.
Require Import Debugging.

Open Scope lazy_bool_scope.


Definition wte {A} (k: option A) (P: A -> Prop) (Q: Prop) :=
     match k with
     | Some a => P a
     | None => Q
     end.

Definition ifprop (k: bool) (P Q: Prop) :=
 if k then P else Q.


Bind Scope option_scope with option.
Delimit Scope option_scope with option.
Open Scope option.

Notation "'TRY' x '<-' k 'IN' f 'CATCH' opt" := (match k with Some x => f | None => opt end)
    (at level 55, k at level 53, right associativity): option_scope.

Notation "'SOME' x '<-' k1 '-;' k2" := (TRY x <- k1 IN k2 CATCH None)
    (at level 55, k1 at level 53, right associativity): option_scope.

Notation "k1 '-;' k2" := (SOME tt <- k1 -; k2)
  (at level 55, right associativity): option_scope.

Notation "'WHEN' x '<-' k 'THEN' R" := (wte k (fun x => R) True)
    (at level 73, R at level 95, right associativity): option_scope.

Notation "'WHEN' k 'THEN' R" := (wte k (fun _: unit => R) True)
    (at level 73, R at level 95, right associativity): option_scope.

Notation "'FAILS' k" := (wte k (fun _ => False) True)
    (at level 73): option_scope.

Notation "'EXISTS' x '<-' k 'SUCH' R" := (wte k (fun x => R) False)
    (at level 73, R at level 95, right associativity): option_scope.

Notation "'If' k 'THEN' R" := (ifprop k R True)
    (at level 73, R at level 95, right associativity): option_scope.


Definition check (b:bool) : option unit :=
  if b then Some tt else None.
Extraction Inline check.


Lemma ifprop_monotone (k:bool) (P1 P2 Q1 Q2: Prop):
        ifprop k P1 Q1
        -> (k=true -> P1 -> P2)
        -> (k=false -> Q1 -> Q2)
        -> ifprop k P2 Q2.

Lemma wte_monotone A (k:option A) (P1 P2: A -> Prop) (Q1 Q2: Prop):
        wte k P1 Q1
        -> (forall a, k=Some a -> P1 a -> P2 a)
        -> (k=None -> Q1 -> Q2)
        -> wte k P2 Q2.

Add Parametric Morphism (A:Type): ifprop with
  signature Logic.eq ==> iff ==> iff ==> iff
  as ifprop_compat.

Add Parametric Morphism (A:Type): (@wte A) with
  signature Logic.eq ==> (pointwise_relation A iff) ==> iff ==> iff
  as wte_compat.

Lemma if_decomp {A} (b:bool) (k1 k2: A) (P: A -> Prop):
    (ifprop b (P k1) (P k2))
    -> P (if b then k1 else k2).

Lemma if_decomp_ifprop (b:bool) (k1 k2: bool) (P Q: Prop):
    (ifprop b (ifprop k1 P Q) (ifprop k2 P Q))
    -> ifprop (if b then k1 else k2) P Q.

Lemma if_decomp_wte {A} (b:bool) (k1 k2: option A) (P: A -> Prop) (Q: Prop):
    (ifprop b (wte k1 P Q) (wte k2 P Q))
    -> wte (if b then k1 else k2) P Q.

Lemma try_catch_decomp A B (k: option A) f opt (P:B -> Prop):
         (wte k (fun x => P (f x)) (P opt)) -> P (TRY x <- k IN (f x) CATCH opt).

Lemma try_catch_decomp_ifprop A (k: option A) f opt (P Q:Prop):
         (wte k (fun x => ifprop (f x) P Q) (ifprop opt P Q)) -> ifprop (TRY x <- k IN (f x) CATCH opt) P Q.

Lemma try_catch_decomp_wte A B (k: option A) f opt (P:B -> Prop) (Q:Prop):
         (wte k (fun x => wte (f x) P Q) (wte opt P Q)) -> wte (TRY x <- k IN (f x) CATCH opt) P Q.


Lemma sumbool_decomp A (P Q: Prop) (k: {P}+{Q}) (k1 k2: A) (F: A -> Prop):
    (forall pf: P, k=(left pf) -> F k1)
     -> (forall pf: Q, k=(right pf) -> F k2)
        -> F (if k then k1 else k2).

Lemma sumbool_decomp_ifprop (P Q: Prop) (k: {P}+{Q}) (k1 k2: bool) (FP FQ:Prop):
    (forall pf: P, k=(left pf) -> ifprop k1 FP FQ)
     -> (forall pf: Q, k=(right pf) -> ifprop k2 FP FQ)
        -> ifprop (if k then k1 else k2) FP FQ.

Lemma sumbool_decomp_wte A (P Q: Prop) (k: {P}+{Q}) (k1 k2: option A) (FP: A -> Prop) (FQ:Prop):
    (forall pf: P, k=(left pf) -> wte k1 FP FQ)
     -> (forall pf: Q, k=(right pf) -> wte k2 FP FQ)
        -> wte (if k then k1 else k2) FP FQ.



Lemma prod_decomp (A B C: Type) (p: A*B) (f: A -> B -> C) (P: C -> Prop):
  (P (f (fst p) (snd p)))
    -> (P (let (x,y):=p in (f x y))).

Lemma prod_decomp_ifprop (A B: Type) (p: A*B) (f: A -> B -> bool) (P Q: Prop):
  (ifprop (f (fst p) (snd p)) P Q)
    -> (ifprop (let (x,y):=p in (f x y)) P Q).

Lemma prod_decomp_wte (A B C: Type) (p: A*B) (f: A -> B -> option C) (P: C -> Prop) (Q: Prop):
  (wte (f (fst p) (snd p)) P Q)
    -> (wte (let (x,y):=p in (f x y)) P Q).


Lemma wte_decomp A (k: option A) (P: A -> Prop) (Q: Prop):
  (forall a, k = Some a -> P a) -> (k = None -> Q) -> wte k P Q.

Lemma ifprop_decomp (b:bool) (P Q: Prop):
    (b=true -> P)
     -> (b=false -> Q)
        -> (ifprop b P Q).



Lemma EXISTS_simpl {A} {k: option A} {P: A -> Prop}:
   (EXISTS x <- k SUCH P x) -> exists x, k=Some x /\ P x.


Lemma WHENTHEN_simpl {A} {k: option A} {P: A -> Prop}:
   (WHEN x <- k THEN P x) -> forall x, k=Some x -> P x.


Lemma IfTHEN_simpl {b:bool} {P:Prop}: (If b THEN P) -> b=true -> P.

Lemma wte_simpl {A} {k: option A} {P: A -> Prop} {Q: Prop} :
   wte k P Q -> { v | k=Some v & P v } + { k=None /\ Q }.

Lemma SOME_assoc {A B C} (k1: option A) (k2: A -> option B) (k3: B -> option C):
  SOME y <- (SOME x <- k1 -; k2 x) -; k3 y
  = SOME x <- k1 -;
    SOME y <- k2 x -;
    k3 y.
  




Ltac intro_rewrite := let H:= fresh "Heq_simplified" in intro H; try (rewrite !H in * |- *; simpl in * |- *).


Ltac wte_decompose :=
      apply prod_decomp_wte
   || apply try_catch_decomp_wte
   || (apply sumbool_decomp_wte; intro; intro_rewrite)
   || apply if_decomp_wte.

Ltac apply_wte_hint hint :=
    eapply wte_monotone;
      [ hint; fail | idtac | idtac ] ;
      simpl;
      [ intro | idtac ]; intro_rewrite.

Ltac ifprop_decompose :=
      apply prod_decomp_ifprop
   || apply try_catch_decomp_ifprop
   || (apply sumbool_decomp_ifprop; intro; intro_rewrite)
   || apply if_decomp_ifprop.

Ltac apply_ifprop_hint hint :=
    eapply ifprop_monotone;
     [ hint; fail | idtac | idtac ] ;
     intro_rewrite.

Ltac default_simplify :=
      apply prod_decomp
   || apply try_catch_decomp
   || apply if_decomp.

Ltac xstep hint :=
 match goal with
 | |- (wte _ _ _) => wte_decompose
                || apply_wte_hint ltac:hint
                || (apply wte_decomp; [ intro | idtac]; intro_rewrite)
 | |- (ifprop _ _ _) => ifprop_decompose
                || apply_ifprop_hint ltac:hint
                || (apply ifprop_decomp; intro_rewrite)
 | |- _ => default_simplify
 end.

 
Ltac xsimplify hint :=
 repeat (intros; xstep hint ; simpl; (tauto || hint)).