Add Rec LoadPath "." as ALEA.

Require Export Probas.

Definition Mif (A:Type) (b:distr bool) (m1 m2: distr A)
    := Mlet b (fun x:bool => if x then m1 else m2).

Lemma Mif_le_compat : forall (A:Type) (b1 b2:distr bool) (m1 m2 n1 n2: distr A),
    b1 <= b2 -> m1 <= m2 -> n1 <= n2 -> Mif b1 m1 n1 <= Mif b2 m2 n2.

Hint Resolve Mif_le_compat.

Instance Mif_mon2 : forall (A:Type) b, monotonic2 (Mif (A:=A) b).
Save.

Definition MIf : forall (A:Type), distr bool -m> distr A -m> distr A -m> distr A.
Defined.

Lemma MIf_simpl : forall A b d1 d2, MIf A b d1 d2 = Mif b d1 d2.

Instance if_mon : forall `{o:ord A} (b:bool), monotonic2 (fun (x y:A) => if b then x else y).
Save.

Definition If `{o:ord A} (b:bool) : A -m> A -m> A := mon2 (fun (x y:A) => if b then x else y).

Instance Mif_continuous2 : forall (A:Type) b, continuous2 (MIf A b).
Save.

Hint Resolve Mif_continuous2.

Instance Mif_cond_continuous : forall (A:Type), continuous (MIf A).
Save.

Hint Resolve Mif_cond_continuous.

Add Parametric Morphism (A:Type) : (Mif (A:=A))
  with signature Oeq ==> Oeq ==> Oeq ==> Oeq
as Mif_eq_compat.
Save.
Hint Immediate Mif_eq_compat.

Add Parametric Morphism (A:Type) : (Mif (A:=A))
  with signature Ole ==> Ole ==> Ole ==> Ole
as Mif_le_compat_morph.
Save.

Lemma Mif_lub_eq_left : forall (A:Type) b h (d: distr A),
    Mif b (lub h) d == lub (MIf _ b @ h) d.

Lemma Mif_lub_eq_right : forall (A:Type) b h (d: distr A),
    Mif b d (lub h) == lub (MIf _ b d @ h).

Lemma Mif_lub_eq2 : forall (A:Type) b (h1 h2 : nat -m> distr A),
    Mif b (lub h1) (lub h2) == lub ((MIf _ b @2 h1) h2).

Instance Mif_term : forall (A:Type) b (d1 d2:distr A)
     {Tb : Term b} {T1:Term d1} {T2:Term d2}, Term (Mif b d1 d2).
Save.
Hint Resolve Mif_term.

Definition pchoice : forall A, U -> M A -> M A -> M A.
Defined.

Lemma pchoice_simpl : forall A p (m1 m2:M A) f,
      pchoice p m1 m2 f = p * m1 f + [1-]p * m2 f.

Definition Mchoice (A:Type) (p:U) (m1 m2: distr A) : distr A.
Defined.

Lemma Mchoice_simpl : forall A p (m1 m2:distr A) f,
      mu (Mchoice p m1 m2) f = p * mu m1 f + [1-]p * mu m2 f.

Lemma Mchoice_le_compat : forall (A:Type) (p:U) (m1 m2 n1 n2: distr A),
        m1<=m2 -> n1<=n2 -> Mchoice p m1 n1 <= Mchoice p m2 n2.
Hint Resolve Mchoice_le_compat.

Add Parametric Morphism (A:Type) : (Mchoice (A:=A))
  with signature Oeq ==> Oeq ==> Oeq ==> Oeq
as Mchoice_eq_compat.
Save.
Hint Immediate Mchoice_eq_compat.

Instance Mchoice_mon2 : forall (A:Type) (p:U), monotonic2 (Mchoice (A:=A) p).
Save.

Definition MChoice A (p:U) : distr A -m> distr A -m> distr A :=
               mon2 (Mchoice (A:=A) p).

Lemma MChoice_simpl : forall A (p:U) (m1 m2 : distr A),
MChoice A p m1 m2 = Mchoice p m1 m2.

Lemma Mchoice_sym_le : forall (A:Type) (p:U) (m1 m2: distr A),
            Mchoice p m1 m2 <= Mchoice ([1-]p) m2 m1.
Hint Resolve Mchoice_sym_le.

Lemma Mchoice_sym : forall (A:Type) (p:U) (m1 m2: distr A),
            Mchoice p m1 m2 == Mchoice ([1-]p) m2 m1.

Lemma Mchoice_continuous_right
    : forall (A:Type) (p:U) (m: distr A), continuous (D1:=distr A) (D2:=distr A) (MChoice A p m).
Hint Resolve Mchoice_continuous_right.

Lemma Mchoice_continuous_left : forall (A:Type) (p:U),
    continuous (D1:=distr A) (D2:=distr A -m> distr A) (MChoice A p).

Lemma Mchoice_continuous :
forall (A:Type) (p:U), continuous2 (D1:=distr A) (D2:=distr A) (D3:=distr A) (MChoice A p).

Instance Mchoice_term : forall A p (d1 d2:distr A) {T1:Term d1} {T2:Term d2},
     Term (Mchoice p d1 d2).
Save.
Hint Resolve Mchoice_term.

Definition im_distr (A B : Type) (f:A -> B) (m:distr A) : distr B :=
    Mlet m (fun a => Munit (f a)).

Lemma im_distr_simpl : forall A B (f:A -> B) (m:distr A)(h:B -> U),
     mu (im_distr f m) h = mu m (fun a => h (f a)).

Add Parametric Morphism (A B : Type) : (im_distr (A:=A) (B:=B))
  with signature (feq (A:=A) (B:=B)) ==> Oeq ==> Oeq
  as im_distr_eq_compat.
Save.

Lemma im_distr_comp : forall A B C (f:A -> B) (g:B -> C) (m:distr A),
            im_distr g (im_distr f m) == im_distr (fun a => g (f a)) m.

Lemma im_distr_id : forall A (f:A -> A) (m:distr A), (forall x, f x = x) ->
            im_distr f m == m.

Instance im_distr_term : forall A B (f:A->B)(d:distr A){T:Term d},
              Term (im_distr f d).
Save.
Hint Resolve im_distr_term.

Definition prod_distr (A B : Type)(d1:distr A)(d2:distr B) : distr (A*B) :=
                Mlet d1 (fun x => Mlet d2 (fun y => Munit (x,y))).

Add Parametric Morphism (A B : Type) : (prod_distr (A:=A) (B:=B))
with signature Ole ++> Ole ++> Ole
as prod_distr_le_compat.
Save.
Hint Resolve prod_distr_le_compat.

Add Parametric Morphism (A B : Type) : (prod_distr (A:=A) (B:=B))
with signature Oeq ==> Oeq ==> Oeq
as prod_distr_eq_compat.
Save.
Hint Immediate prod_distr_eq_compat.

Instance prod_distr_mon2 : forall (A B :Type), monotonic2 (prod_distr (A:=A) (B:=B)).
Save.

Definition Prod_distr (A B :Type): distr A -m> distr B -m> distr (A*B) :=
     mon2 (prod_distr (A:=A) (B:=B)).

Lemma Prod_distr_simpl : forall (A B:Type)(d1: distr A) (d2:distr B),
     Prod_distr A B d1 d2 = prod_distr d1 d2.

Lemma prod_distr_rect : forall (A B : Type) (d1: distr A) (d2:distr B) (f:A -> U)(g:B -> U),
         mu (prod_distr d1 d2) (fun xy => f (fst xy) * g (snd xy)) == mu d1 f * mu d2 g.

Lemma prod_distr_fst : forall (A B : Type) (d1: distr A) (d2:distr B) (f:A -> U),
             mu (prod_distr d1 d2) (fun xy => f (fst xy)) == pone d2 * mu d1 f.

Lemma prod_distr_snd : forall (A B : Type) (d1: distr A) (d2:distr B) (g:B -> U),
             mu (prod_distr d1 d2) (fun xy => g (snd xy)) == pone d1 * mu d2 g.

Lemma prod_distr_fst_eq : forall (A B : Type) (d1: distr A) (d2:distr B),
     pone d2 == 1 -> im_distr (fst (A:=A) (B:=B)) (prod_distr d1 d2) == d1.

Lemma prod_distr_snd_eq : forall (A B : Type) (d1: distr A) (d2:distr B),
       pone d1 == 1 -> im_distr (snd (A:=A) (B:=B)) (prod_distr d1 d2) == d2.

Definition swap A B (x:A*B) : B * A := (snd x,fst x).

Definition arg_swap A B (f : MF (A*B)) : MF (B*A) := fun z => f (swap z).

Definition Arg_swap A B : MF (A*B) -m> MF (B*A).
Defined.

Lemma Arg_swap_simpl : forall A B f, Arg_swap A B f = arg_swap f.

Definition prod_distr_com A B (d1: distr A) (d2:distr B) (f : MF (A * B)) :=
      mu (prod_distr d1 d2) f == mu (prod_distr d2 d1) (arg_swap f).

Lemma prod_distr_com_eq_compat : forall A B (d1: distr A) (d2:distr B) (f g: MF (A * B)),
  f == g -> prod_distr_com d1 d2 f -> prod_distr_com d1 d2 g.

Lemma prod_distr_com_rect : forall (A B : Type) (d1: distr A) (d2:distr B) (f:A -> U)(g:B -> U),
         prod_distr_com d1 d2 (fun xy => f (fst xy) * g (snd xy)).

Lemma prod_distr_com_cte : forall (A B : Type) (d1: distr A) (d2:distr B) (c:U),
         prod_distr_com d1 d2 (fcte (A*B) c).

Lemma prod_distr_com_one : forall (A B : Type) (d1: distr A) (d2:distr B),
         prod_distr_com d1 d2 (fone (A*B)).

Lemma prod_distr_com_plus : forall (A B : Type) (d1: distr A) (d2:distr B) (f g:MF (A*B)),
         fplusok f g ->
         prod_distr_com d1 d2 f -> prod_distr_com d1 d2 g ->
         prod_distr_com d1 d2 (fplus f g).

Lemma prod_distr_com_mult : forall (A B : Type) (d1: distr A) (d2:distr B) (k:U)(f:MF (A*B)),
         prod_distr_com d1 d2 f -> prod_distr_com d1 d2 (fmult k f).

Lemma prod_distr_com_inv : forall (A B : Type) (d1: distr A) (d2:distr B) (f:MF (A*B)),
         prod_distr_com d1 d2 f -> prod_distr_com d1 d2 (finv f).

Lemma prod_distr_com_lub : forall (A B : Type) (d1: distr A) (d2:distr B) (f:nat -m> MF (A*B)),
         (forall n, prod_distr_com d1 d2 (f n)) -> prod_distr_com d1 d2 (lub f).

Lemma prod_distr_com_sym : forall A B (d1:distr A) (d2:distr B) (f:MF (A*B)),
     prod_distr_com d1 d2 f -> prod_distr_com d2 d1 (arg_swap f).

Lemma discrete_commute : forall A B (d1:distr A) (d2:distr B) (f:MF (A*B)),
    is_discrete d1 -> prod_distr_com d1 d2 f.

Lemma is_discrete_swap: forall A B C (d1:distr A) (d2:distr B) (f:A -> B -> distr C),
   is_discrete d1 ->
   Mlet d1 (fun x => Mlet d2 (fun y => f x y)) == Mlet d2 (fun y => Mlet d1 (fun x => f x y)).

Lemma is_discrete_swap_mu : forall A B (d1:distr A) (d2:distr B) (f:A -> B -> U),
   is_discrete d1 ->
   mu d1 (fun x : A => mu d2 (fun y : B => f x y)) ==
   mu d2 (fun y : B => mu d1 (fun x : A => f x y)).

Definition fst_distr A B (m : distr (A*B)) : distr A := im_distr (fst (B:=B)) m.
Definition snd_distr A B (m : distr (A*B)) : distr B := im_distr (snd (B:=B)) m.

Add Parametric Morphism (A B : Type) : (fst_distr (A:=A) (B:=B))
   with signature Oeq ==> Oeq as fst_distr_eq_compat.
Save.

Add Parametric Morphism (A B : Type) : (snd_distr (A:=A) (B:=B))
   with signature Oeq ==> Oeq as snd_distr_eq_compat.
Save.

Lemma fst_prod_distr : forall A B (m1:distr A) (m2:distr B),
           fst_distr (prod_distr m1 m2) == distr_scale (pone m2) m1.

Lemma snd_prod_distr : forall A B (m1:distr A) (m2:distr B),
          snd_distr (prod_distr m1 m2) == distr_scale (pone m1) m2.

Lemma pone_prod : forall A B (m1:distr A) (m2:distr B),
          pone (prod_distr m1 m2) == pone m1 * pone m2.

Instance prod_distr_term : forall A B (d1:distr A) (d2:distr B)
     {T1:Term d1} {T2:Term d2}, Term (prod_distr d1 d2).
Save.
Hint Resolve prod_distr_term.

Lemma fst_prod_distr_term : forall A B (d1:distr A) (d2:distr B) {T2:Term d2},
           fst_distr (prod_distr d1 d2) == d1.

Lemma snd_prod_distr_term : forall A B (d1:distr A) (d2:distr B) {T1:Term d1},
           snd_distr (prod_distr d1 d2) == d2.
Hint Resolve fst_prod_distr_term snd_prod_distr_term.

Definition prod_indep A B (m:distr (A*B)) :=
        distr_scale (pone m) m == prod_distr (fst_distr m) (snd_distr m).

Lemma prod_distr_indep : forall A B (m1:distr A) (m2:distr B), prod_indep (prod_distr m1 m2).

Add Parametric Morphism A B : (prod_indep (A:=A) (B:=B))
   with signature Oeq ==> Basics.impl
   as prod_indep_eq_compat.
Save.
Hint Resolve prod_indep_eq_compat.

Lemma distr_indep_mult
   : forall A B (m:distr (A*B)), prod_indep m ->
                     forall (f1 : MF A) (f2:MF B),
                     pone m * mu m (fun p => f1 (fst p) * f2 (snd p)) ==
                     mu (fst_distr m) f1 * mu (snd_distr m) f2.

Definition range A (P:A -> Prop) (d: distr A) :=
   forall f, (forall x, P x -> 0 == f x) -> 0 == mu d f.

Lemma range_le : forall A (P: A -> Prop) (d:distr A), range P d ->
       forall f g, (forall a, P a -> f a <= g a) -> mu d f <= mu d g.

Lemma range_eq : forall A (P: A -> Prop) (d:distr A), range P d ->
       forall f g, (forall a, P a -> f a == g a) -> mu d f == mu d g.

Lemma im_range A B (f : A -> B) :
    forall (d : distr A) (P : B -> Prop),
    range (fun x => P (f x)) d -> range P (im_distr f d).
Hint Resolve im_range.

Lemma range_impl A (P Q : A -> Prop) :
  forall (d:distr A), (forall x, P x -> Q x)
    -> range P d -> range Q d.

Lemma im_range_map A B (f : A -> B) :
    forall (d : distr A) (P : B -> Prop) (Q:A -> Prop),
    (forall x, Q x -> P (f x)) ->
    range Q d -> range P (im_distr f d).

Lemma im_range_prop A B (f : A -> B) :
    forall (d : distr A) (P : B -> Prop),
    (forall x, P (f x)) -> range P (im_distr f d).

Lemma range_le_compat : forall A (P : A -> Prop) (d1 d2 : distr A),
    d1 <= d2 -> range P d2 -> range P d1.

Add Parametric Morphism A (P : A -> Prop) : (range P)
    with signature Oeq ==> iff as range_distr_morph.
Save.

Definition ok (A:Type) (p:U) (e:distr A) (q:A -> U) := p <= mu e q.

Definition okfun (A B:Type)(p:A -> U)(e:A -> distr B)(q:A -> B -> U)
  := forall x:A, ok (p x) (e x) (q x).

Definition okup (A:Type) (p:U) (e:distr A) (q:A -> U) := mu e q <= p.

Definition upfun (A B:Type)(p:A -> U)(e:A -> distr B)(q:A -> B -> U)
  := forall x:A, okup (p x) (e x) (q x).

Lemma ok_le_compat : forall (A:Type) (p p':U) (e:distr A) (q q':A -> U),
    p' <= p -> q <= q' -> ok p e q -> ok p' e q'.

Lemma ok_eq_compat : forall (A:Type) (p p':U) (e e':distr A) (q q':A -> U),
    p' == p -> q == q' -> e == e' -> ok p e q -> ok p' e' q'.

Add Parametric Morphism (A:Type) : (@ok A)
  with signature Ole --> Oeq ==> Ole ==> Basics.impl
  as ok_le_morphism.
Save.

Add Parametric Morphism (A:Type) : (@ok A)
  with signature Oeq --> Oeq ==> Oeq ==> iff
  as ok_eq_morphism.
Save.

Lemma okfun_le_compat :
forall (A B:Type) (p p':A -> U) (e:A -> distr B) (q q':A -> B -> U),
    p' <= p -> q <= q' -> okfun p e q -> okfun p' e q'.

Lemma okfun_eq_compat :
forall (A B:Type) (p p':A -> U) (e e':A -> distr B) (q q':A -> B -> U),
    p' == p -> q == q' -> e == e' -> okfun p e q -> okfun p' e' q'.

Add Parametric Morphism (A B:Type) : (@okfun A B)
  with signature Ole --> Oeq ==> Ole ==> Basics.impl
  as okfun_le_morphism.
Save.

Add Parametric Morphism (A B:Type) : (@okfun A B)
  with signature Oeq --> Oeq ==> Oeq ==> iff
  as okfun_eq_morphism.
Save.

Lemma ok_mult : forall (A:Type)(k p:U)(e:distr A)(f : A -> U),
                           ok p e f -> ok (k*p) e (fmult k f).

Lemma ok_inv : forall (A:Type)(p:U)(e:distr A)(f : A -> U),
             ok p e f -> mu e (finv f) <= [1-]p.

Lemma okup_le_compat : forall (A:Type) (p p':U) (e:distr A) (q q':A -> U),
    p <= p' -> q' <= q -> okup p e q -> okup p' e q'.

Lemma okup_eq_compat : forall (A:Type) (p p':U) (e e':distr A) (q q':A -> U),
    p == p' -> q == q' -> e == e' -> okup p e q -> okup p' e' q'.

Lemma upfun_le_compat : forall (A B:Type) (p p':A -> U) (e:A -> distr B)
    (q q':A -> B -> U),
    p <= p' -> q'<=q -> upfun p e q -> upfun p' e q'.

Lemma okup_mult : forall (A:Type)(k p:U)(e:distr A)(f : A -> U), okup p e f -> okup (k*p) e (fmult k f).

Lemma apply_rule : forall (A B:Type)(a:(distr A))(f:A -> distr B)(r:U)(p:A -> U)(q:B -> U),
    ok r a p -> okfun p f (fun x => q) -> ok r (Mlet a f) q.

Lemma okup_apply_rule : forall (A B:Type)(a:distr A)(f:A -> distr B)(r:U)(p:A -> U)(q:B -> U),
    okup r a p -> upfun p f (fun x => q) -> okup r (Mlet a f) q.

Lemma lambda_rule : forall (A B:Type)(f:A -> distr B)(p:A -> U)(q:A -> B -> U),
   (forall x:A, ok (p x) (f x) (q x)) -> okfun p f q.

Lemma okup_lambda_rule : forall (A B:Type)(f:A -> distr B)(p:A -> U)(q:A -> B -> U),
   (forall x:A, okup (p x) (f x) (q x)) -> upfun p f q.

Lemma combiok : forall (A:Type) p q (f1 f2 : A -> U), p <= [1-]q -> fplusok (fmult p f1) (fmult q f2).
Hint Extern 1 => apply combiok.

Lemma fmult_fplusok : forall (A:Type) p q (f1 f2 : A -> U), fplusok f1 f2 -> fplusok (fmult p f1) (fmult q f2).
Hint Resolve fmult_fplusok.

Lemma ifok : forall f1 f2, fplusok (fmult f1 B2U) (fmult f2 NB2U).
Hint Resolve ifok.

Lemma Mif_eq : forall (A:Type)(b:(distr bool))(f1 f2:distr A)(q:MF A),
        mu (Mif b f1 f2) q == (mu f1 q) * (mu b B2U) + (mu f2 q) * (mu b NB2U).

Lemma Mif_eq2 : forall (A : Type) (b : distr bool) (f1 f2 : distr A) (q : MF A),
  mu (Mif b f1 f2) q == mu b B2U * mu f1 q + mu b NB2U * mu f2 q.

Lemma ifrule :
  forall (A:Type)(b:(distr bool))(f1 f2:distr A)(p1 p2:U)(q:A -> U),
       ok p1 f1 q -> ok p2 f2 q
       -> ok (p1 * (mu b B2U) + p2 * (mu b NB2U)) (Mif b f1 f2) q.

Lemma okup_ifrule :
  forall (A:Type)(b:(distr bool))(f1 f2:distr A)(p1 p2:U)(q:A -> U),
       okup p1 f1 q -> okup p2 f2 q
       -> okup (p1 * (mu b B2U) + p2 * (mu b NB2U)) (Mif b f1 f2) q.

Section Fixrule.
Variables A B : Type.

Variable F : (A -> distr B) -m> (A -> distr B).

Section Ruleseq.
Variable q : A -> B -> U.

Lemma fixrule_Ulub : forall (p : A -> nat -> U),
   (forall x:A, p x O == 0)->
   (forall (i:nat) (f:A -> distr B),
      (okfun (fun x => p x i) f q) -> okfun (fun x => p x (S i)) (fun x => F f x) q)
   -> okfun (fun x => Ulub (p x)) (Mfix F) q.

Lemma fixrule : forall (p : A -> nat -m> U),
   (forall x:A, p x O == 0)->
   (forall (i:nat) (f:A -> distr B),
      (okfun (fun x => p x i) f q) -> okfun (fun x => p x (S i)) (fun x => F f x) q)
   -> okfun (fun x => lub (p x)) (Mfix F) q.

Lemma fixrule_up_Ulub : forall (p : A -> nat -> U),
   (forall (i:nat) (f:A -> distr B),
      (upfun (fun x => p x i) f q) -> upfun (fun x => p x (S i)) (fun x => F f x) q)
   -> upfun (fun x => Ulub (p x)) (Mfix F) q.

Lemma fixrule_up_lub : forall (p : A -> nat -m> U),
   (forall (i:nat) (f:A -> distr B),
      (upfun (fun x => p x i) f q) -> upfun (fun x => p x (S i)) (fun x => F f x) q)
   -> upfun (fun x => lub (p x)) (Mfix F) q.

Lemma okup_fixrule_glb :
   forall p : A -> nat -m-> U,
   (forall (i:nat) (f:A -> distr B),
       (upfun (fun x => p x i) f q) -> upfun (fun x => p x (S i)) (fun x => F f x) q)
   -> upfun (fun x => glb (p x)) (Mfix F) q.
End Ruleseq.

Lemma okup_fixrule_inv : forall (p : A -> U) (q : A -> B -> U),
   (forall (f:A -> distr B), upfun p f q -> upfun p (fun x => F f x) q)
           -> upfun p (Mfix F) q.

Section TransformFix.

Section Fix_muF.
Variable q : A -> B -> U.
Variable muF : MF A -m> MF A.

Definition admissible (P:(A -> distr B) -> Prop) := P 0 /\ forall f, P f -> P (F f).

Lemma admissible_true : admissible (fun f => True).

Lemma admissible_le_fix :
  continuous (D1:=A -> distr B) (D2:=A -> distr B) F -> admissible (fun f => f <= Mfix F).

Lemma muF_stable : stable muF.

Definition mu_muF_commute_le :=
  forall f x, f <= Mfix F -> mu (F f x) (q x) <= muF (fun y => mu (f y) (q y)) x.
Hint Unfold mu_muF_commute_le.

Section F_muF_results.
Hypothesis F_muF_le : mu_muF_commute_le.

Lemma mu_mufix_le : forall x, mu (Mfix F x) (q x) <= mufix muF x.
Hint Resolve mu_mufix_le.

Lemma muF_le : forall f, muF f <= f
      -> forall x, mu (Mfix F x) (q x) <= f x.

Hypothesis muF_F_le :
    forall f x, f <= Mfix F -> muF (fun y => mu (f y) (q y)) x <= mu (F f x) (q x).

Lemma mufix_mu_le : forall x, mufix muF x <= mu (Mfix F x) (q x).

End F_muF_results.
Hint Resolve mu_mufix_le mufix_mu_le.

Lemma mufix_mu :
   (forall f x, f <= Mfix F -> mu (F f x) (q x) == muF (fun y => mu (f y) (q y)) x)
   -> forall x, mufix muF x == mu (Mfix F x) (q x).
Hint Resolve mufix_mu.
End Fix_muF.

Section Fix_Term.

Definition pterm : MF A := fun (x:A) => mu (Mfix F x) (fone B).
Variable muFone : MF A -m> MF A.

Hypothesis F_muF_eq_one :
  forall f x, f <= Mfix F -> mu (F f x) (fone B) == muFone (fun y => mu (f y) (fone B)) x.

Hypothesis muF_cont : continuous muFone.

Lemma muF_pterm : pterm == muFone pterm.
Hint Resolve muF_pterm.
End Fix_Term.

Section Fix_muF_Term.

Variable q : A -> B -> U.
Definition qinv x y := [1-]q x y.

Variable muFqinv : MF A -m> MF A.

Hypothesis F_muF_le_inv : mu_muF_commute_le qinv muFqinv.

Lemma muF_le_term : forall f, muFqinv (finv f) <= finv f ->
    forall x, f x & pterm x <= mu (Mfix F x) (q x).

Lemma muF_le_term_minus :
forall f, f <= pterm -> muFqinv (fminus pterm f) <= fminus pterm f ->
    forall x, f x <= mu (Mfix F x) (q x).

Variable muFq : MF A -m> MF A.

Hypothesis F_muF_le : mu_muF_commute_le q muFq.

Lemma muF_eq : forall f, muFq f <= f -> muFqinv (finv f) <= finv f ->
    forall x, pterm x == 1 -> mu (Mfix F x) (q x) == f x.

End Fix_muF_Term.
End TransformFix.

Section LoopRule.
Variable q : A -> B -> U.
Variable stop : A -> distr bool.
Variable step : A -> distr A.
Variable a : U.

Definition Loop : MF A -m> MF A.
Defined.

Lemma Loop_eq :
    forall f x, Loop f x = mu (stop x) (fun b => if b then a else mu (step x) f).

Definition loop := mufix Loop.

Lemma Mfixvar :
  (forall (f:A -> distr B),
      okfun (fun x => Loop (fun y => mu (f y) (q y)) x) (fun x => F f x) q)
 -> okfun loop (Mfix F) q.

Definition up_loop : MF A := nufix Loop.

Lemma Mfixvar_up :
  (forall (f:A -> distr B),
      upfun (fun x => Loop (fun y => mu (f y) (q y)) x) (fun x => F f x) q)
 -> upfun up_loop (Mfix F) q.

End LoopRule.

End Fixrule.

Lemma Flip_true : mu Flip B2U == [1/2].

Lemma Flip_false : mu Flip NB2U == [1/2].

Lemma ok_Flip : forall q : bool -> U, ok ([1/2] * q true + [1/2] * q false) Flip q.

Lemma okup_Flip : forall q : bool -> U, okup ([1/2] * q true + [1/2] * q false) Flip q.

Hint Resolve ok_Flip okup_Flip Flip_true Flip_false.

Lemma Flip_eq : forall q : bool -> U, mu Flip q == [1/2] * q true + [1/2] * q false.
Hint Resolve Flip_eq.

Section Wellfounded.
Variables A B : Type.
Variable R : A -> A -> Prop.
Hypothesis Rwf : well_founded R.
Variable F : forall x, (forall y, R y x -> distr B) -> distr B.

Definition WfFix : A -> distr B := Fix Rwf (fun _ => distr B) F.

Hypothesis Fext : forall x f g, (forall y (p:R y x), f y p == g y p) -> F f == F g.

Lemma Acc_iter_distr :
   forall x, forall r s : Acc R x, Acc_iter (fun _=> distr B) F r == Acc_iter (fun _=> distr B) F s.

Lemma WfFix_eq : forall x, WfFix x == F (fun (y:A) (p:R y x) => WfFix y).

Variable P : distr B -> Prop.
Hypothesis Pext : forall m1 m2, m1 == m2 -> P m1 -> P m2.

Lemma WfFix_ind :
     (forall x f, (forall y (p:R y x), P (f y p)) -> P (F f))
  -> forall x, P (WfFix x).

End Wellfounded.

Ltac distrsimpl := match goal with
 | |- (Ole (fmont (mu ?d1) ?f) (fmont (mu ?d2) ?g)) => apply (mu_le_compat (m1:=d1) (m2:=d2) (Ole_refl d1) (f:=f) (g:=g)); intro
 | |- (Oeq (fmont (mu ?d1) ?f) (fmont (mu ?d2) ?g)) => apply (mu_eq_compat (m1:=d1) (m2:=d2) (Oeq_refl d1) (f:=f) (g:=g)); intro
 | |- (Oeq (Munit ?x) (Munit ?y)) => apply (Munit_eq_compat x y)
 | |- (Oeq (Mlet ?x1 ?f) (Mlet ?x2 ?g))
              => apply (Mlet_eq_compat (m1:=x1) (m2:=x2) (M1:=f) (M2:=g) (Oeq_refl x1)); intro
 | |- (Ole (Mlet ?x1 ?f) (Mlet ?x2 ?g))
              => apply (Mlet_le_compat (m1:=x1) (m2:=x2) (M1:=f) (M2:=g) (Ole_refl x1)); intro
 | |- context [(fmont (mu (Mlet ?m ?M)) ?f)] => rewrite (Mlet_simpl m M f)
 | |- context [(fmont (mu (Munit ?x)) ?f)] => rewrite (Munit_simpl f x)
 | |- context [(Mlet (Mlet ?m ?M) ?f)] => rewrite (Mlet_assoc m M f)
 | |- context [(Mlet (Munit ?x) ?f)] => rewrite (Mlet_unit x f)
 | |- context [(fmont (mu Flip) ?f)] => rewrite (Flip_simpl f)
 | |- context [(fmont (mu (Discrete ?d)) ?f)] => rewrite (Discrete_simpl d);
                                                           rewrite (discrete_simpl (coeff d) (points d) f)
 | |- context [(fmont (mu (Random ?n)) ?f)] => rewrite (Random_simpl n);
                                                           rewrite (random_simpl n f)
 | |- context [(fmont (mu (Mif ?b ?f ?g)) ?h)] => unfold Mif
 | |- context [(fmont (mu (Mchoice ?p ?m1 ?m2)) ?f)] => rewrite (Mchoice_simpl p m1 m2 f)
 | |- context [(fmont (mu (im_distr ?f ?m)) ?h)] => rewrite (im_distr_simpl f m h)
 | |- context [(fmont (mu (prod_distr ?m1 ?m2)) ?h)] => unfold prod_distr
 | |- context [((mon ?f (fmonotonic:=?mf)) ?x)] => rewrite (mon_simpl f (mf:=mf) x)
end.