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 : ∀ (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 : ∀ (A:Type) b, monotonic2 (Mif (A:=A) b).
Save.

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

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

Instance if_mon : ∀ `{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 : ∀ (A:Type) b, continuous2 (MIf A b).
Save.

Hint Resolve Mif_continuous2.

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

Hint Resolve Mif_cond_continuous.

Definition pchoice : ∀ A, U → M A → M A → M A.
Defined.

Lemma pchoice_simpl : ∀ 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 : ∀ A p (m1 m2:distr A) f,
      μ (Mchoice p m1 m2) f = p * μ m1 f + [1-]p * μ m2 f.

Lemma Mchoice_le_compat : ∀ (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 : ∀ (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 : ∀ A (p:U) (m1 m2 : distr A),
MChoice A p m1 m2 = Mchoice p m1 m2.

Lemma Mchoice_sym_le : ∀ (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 : ∀ (A:Type) (p:U) (m1 m2: distr A),
            Mchoice p m1 m2 ≈ Mchoice ([1-]p) m2 m1.

Lemma Mchoice_continuous_right
    : ∀ (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 : ∀ (A:Type) (p:U),
    continuous (D1:=distr A) (D2:=distr A -m> distr A) (MChoice A p).

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

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 : ∀ A B (f:A → B) (m:distr A)(h:B → U),
     μ (im_distr f m) h = μ 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 : ∀ 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 : ∀ A (f:A → A) (m:distr A), (∀ x, f x = x) →
            im_distr f m ≈ m.

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 : ∀ (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 : ∀ (A B:Type)(d1: distr A) (d2:distr B),
     Prod_distr A B d1 d2 = prod_distr d1 d2.

Lemma prod_distr_rect : ∀ (A B : Type) (d1: distr A) (d2:distr B) (f:A → U)(g:B → U),
         μ (prod_distr d1 d2) (fun xy ⇒ f (fst xy) * g (snd xy)) ≈ μ d1 f * μ d2 g.

Lemma prod_distr_fst : ∀ (A B : Type) (d1: distr A) (d2:distr B) (f:A → U),
             μ (prod_distr d1 d2) (fun xy ⇒ f (fst xy)) ≈ pone d2 * μ d1 f.

Lemma prod_distr_snd : ∀ (A B : Type) (d1: distr A) (d2:distr B) (g:B → U),
             μ (prod_distr d1 d2) (fun xy ⇒ g (snd xy)) ≈ pone d1 * μ d2 g.

Lemma prod_distr_fst_eq : ∀ (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 : ∀ (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 : ∀ 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)) :=
      μ (prod_distr d1 d2) f ≈ μ (prod_distr d2 d1) (arg_swap f).

Lemma prod_distr_com_eq_compat : ∀ 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 : ∀ (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 : ∀ (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 : ∀ (A B : Type) (d1: distr A) (d2:distr B),
         prod_distr_com d1 d2 (fone (A*B)).

Lemma prod_distr_com_plus : ∀ (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 : ∀ (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 : ∀ (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 : ∀ (A B : Type) (d1: distr A) (d2:distr B) (f:nat -m> MF (A*B)),
         (∀ n, prod_distr_com d1 d2 (f n)) → prod_distr_com d1 d2 (lub f).

Lemma prod_distr_com_sym : ∀ 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 : ∀ 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: ∀ 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)).

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 : ∀ A B (m1:distr A) (m2:distr B),
           fst_distr (prod_distr m1 m2) ≈ distr_scale (pone m2) m1.

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

Lemma pone_prod : ∀ A B (m1:distr A) (m2:distr B),
          pone (prod_distr m1 m2) ≈ pone m1 * pone m2.

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 : ∀ 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
   : ∀ A B (m:distr (A*B)), prod_indep m →
                     ∀ (f1 : MF A) (f2:MF B),
                     pone m * μ m (fun p ⇒ f1 (fst p) * f2 (snd p)) ≈
                     μ (fst_distr m) f1 * μ (snd_distr m) f2.

Definition range A (P:A → Prop) (d: distr A) :=
   ∀ f, (∀ x, P x → 0 ≈ f x) → 0 ≈ μ d f.

Lemma range_le : ∀ A (P:A → Prop) (d:distr A), range P d →
       ∀ f g, (∀ a, P a → f a ≤ g a) → μ d f ≤ μ d g.

Lemma range_eq : ∀ A (P:A → Prop) (d:distr A), range P d →
       ∀ f g, (∀ a, P a → f a ≈ g a) → μ d f ≈ μ d g.

Definition ok (A:Type) (p:U) (e:distr A) (q:A → U) := p ≤ μ e q.

Definition okfun (A B:Type)(p:A → U)(e:A → distr B)(q:A → B → U)
  := ∀ x:A, ok (p x) (e x) (q x).

Definition okup (A:Type) (p:U) (e:distr A) (q:A → U) := μ e q ≤ p.

Definition upfun (A B:Type)(p:A → U)(e:A → distr B)(q:A → B → U)
  := ∀ x:A, okup (p x) (e x) (q x).

Lemma ok_le_compat : ∀ (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 : ∀ (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 :
∀ (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 :
∀ (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 : ∀ (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 : ∀ (A:Type)(p:U)(e:distr A)(f : A → U),
             ok p e f → μ e (finv f) ≤ [1-]p.

Lemma okup_le_compat : ∀ (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 : ∀ (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 : ∀ (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 : ∀ (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 : ∀ (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 : ∀ (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 : ∀ (A B:Type)(f:A → distr B)(p:A → U)(q:A → B → U),
   (∀ x:A, ok (p x) (f x) (q x)) → okfun p f q.

Lemma okup_lambda_rule : ∀ (A B:Type)(f:A → distr B)(p:A → U)(q:A → B → U),
   (∀ x:A, okup (p x) (f x) (q x)) → upfun p f q.

Lemma combiok : ∀ (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 : ∀ (A:Type) p q (f1 f2 : A → U), fplusok f1 f2 → fplusok (fmult p f1) (fmult q f2).
Hint Resolve fmult_fplusok.

Lemma ifok : ∀ f1 f2, fplusok (fmult f1 ctrue) (fmult f2 cfalse).
Hint Resolve ifok.

Lemma Mif_eq : ∀ (A:Type)(b:(distr bool))(f1 f2:distr A)(q:MF A),
        μ (Mif b f1 f2) q ≈ (μ f1 q) * (μ b ctrue) + (μ f2 q) * (μ b cfalse).

Lemma Mif_eq2 : ∀ (A : Type) (b : distr bool) (f1 f2 : distr A) (q : MF A),
  μ (Mif b f1 f2) q ≈ μ b ctrue * μ f1 q + μ b cfalse * μ f2 q.

Lemma ifrule :
  ∀ (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 * (μ b ctrue) + p2 * (μ b cfalse)) (Mif b f1 f2) q.

Lemma okup_ifrule :
  ∀ (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 * (μ b ctrue) + p2 * (μ b cfalse)) (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 : ∀ (p : A → nat → U),
   (∀ x:A, p x O ≈ 0)->
   (∀ (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 : ∀ (p : A → nat -m> U),
   (∀ x:A, p x O ≈ 0)->
   (∀ (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 : ∀ (p : A → nat → U),
   (∀ (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 : ∀ (p : A → nat -m> U),
   (∀ (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 :
   ∀ p : A → nat -m→ U,
   (∀ (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 : ∀ (p : A → U) (q : A → B → U),
   (∀ (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 ∧ ∀ 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 :=
  ∀ f x, f ≤ Mfix F → μ (F f x) (q x) ≤ muF (fun y ⇒ μ (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 : ∀ x, μ (Mfix F x) (q x) ≤ mufix muF x.
Hint Resolve mu_mufix_le.

Lemma muF_le : ∀ f, muF f ≤ f
      → ∀ x, μ (Mfix F x) (q x) ≤ f x.

Hypothesis muF_F_le :
    ∀ f x, f ≤ Mfix F → muF (fun y ⇒ μ (f y) (q y)) x ≤ μ (F f x) (q x).

Lemma mufix_mu_le : ∀ x, mufix muF x ≤ μ (Mfix F x) (q x).

End F_muF_results.
Hint Resolve mu_mufix_le mufix_mu_le.

Lemma mufix_mu :
   (∀ f x, f ≤ Mfix F → μ (F f x) (q x) ≈ muF (fun y ⇒ μ (f y) (q y)) x)
   → ∀ x, mufix muF x ≈ μ (Mfix F x) (q x).
Hint Resolve mufix_mu.
End Fix_muF.

Section Fix_Term.

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

Hypothesis F_muF_eq_one :
  ∀ f x, f ≤ Mfix F → μ (F f x) (fone B) ≈ muFone (fun y ⇒ μ (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 : ∀ f, muFqinv (finv f) ≤ finv f →
    ∀ x, f x & pterm x ≤ μ (Mfix F x) (q x).

Lemma muF_le_term_minus :
∀ f, f ≤ pterm → muFqinv (fminus pterm f) ≤ fminus pterm f →
    ∀ x, f x ≤ μ (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 : ∀ f, muFq f ≤ f → muFqinv (finv f) ≤ finv f →
    ∀ x, pterm x ≈ 1 → μ (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 :
    ∀ f x, Loop f x = μ (stop x) (fun b ⇒ if b then a else μ (step x) f).

Definition loop := mufix Loop.

Lemma Mfixvar :
  (∀ (f:A → distr B),
      okfun (fun x ⇒ Loop (fun y ⇒ μ (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 :
  (∀ (f:A → distr B),
      upfun (fun x ⇒ Loop (fun y ⇒ μ (f y) (q y)) x) (fun x ⇒ F f x) q)
 → upfun up_loop (Mfix F) q.

End LoopRule.

End Fixrule.

Definition Imu : ∀ A:Type, distr A → (A → IU) → IU.
Defined.

Lemma low_Imu : ∀ (A:Type) (e:distr A) (F: A → IU),
             low (Imu e F) = μ e (fun x ⇒ low (F x)).

Lemma up_Imu : ∀ (A:Type) (e:distr A) (F: A → IU),
             up (Imu e F) = μ e (fun x ⇒ up (F x)).

Lemma Imu_monotonic : ∀ (A:Type) (e:distr A) (F G : A → IU),
            (∀ x, Iincl (F x) (G x)) → Iincl (Imu e F) (Imu e G).

Lemma Imu_stable_eq : ∀ (A:Type) (e:distr A) (F G : A → IU),
            (∀ x, Ieq (F x) (G x)) → Ieq (Imu e F) (Imu e G).
Hint Resolve Imu_monotonic Imu_stable_eq.

Lemma Imu_singl : ∀ (A:Type) (e:distr A) (f:A → U),
           Ieq (Imu e (fun x ⇒ singl (f x))) (singl (μ e f)).

Lemma Imu_inf : ∀ (A:Type) (e:distr A) (f:A → U),
           Ieq (Imu e (fun x ⇒ inf (f x))) (inf (μ e f)).

Lemma Imu_sup : ∀ (A:Type) (e:distr A) (f:A → U),
           Iincl (Imu e (fun x ⇒ sup (f x))) (sup (μ e f)).

Lemma Iin_mu_Imu :
   ∀ (A:Type) (e:distr A) (F:A → IU) (f:A → U),
           (∀ x, Iin (f x) (F x)) → Iin (μ e f) (Imu e F).
Hint Resolve Iin_mu_Imu.

Definition Iok (A:Type) (I:IU) (e:distr A) (F:A → IU) := Iincl (Imu e F) I.
Definition Iokfun (A B:Type)(I:A → IU) (e:A → distr B) (F:A → B → IU)
               := ∀ x, Iok (I x) (e x) (F x).

Lemma Iin_mu_Iok :
   ∀ (A:Type) (I:IU) (e:distr A) (F:A → IU) (f:A → U),
           (∀ x, Iin (f x) (F x)) → Iok I e F → Iin (μ e f) I.

Lemma Iok_le_compat : ∀ (A:Type) (I J:IU) (e:distr A) (F G:A → IU),
   Iincl I J → (∀ x, Iincl (G x) (F x)) → Iok I e F → Iok J e G.

Lemma Iokfun_le_compat : ∀ (A B:Type) (I J:A → IU) (e:A → distr B) (F G:A → B → IU),
   (∀ x, Iincl (I x) (J x)) → (∀ x y, Iincl (G x y) (F x y)) → Iokfun I e F → Iokfun J e G.

Lemma Iunit_eq : ∀ (A: Type) (a:A) (F:A → IU), Ieq (Imu (Munit a) F) (F a).

Lemma Ilet_eq : ∀ (A B : Type) (a:distr A) (f:A → distr B)(I:IU)(G:B → IU),
   Ieq (Imu (Mlet a f) G) (Imu a (fun x ⇒ Imu (f x) G)).
Hint Resolve Ilet_eq.

Lemma Iapply_rule : ∀ (A B : Type) (a:distr A) (f:A → distr B)(I:IU)(F:A → IU)(G:B → IU),
    Iok I a F → Iokfun F f (fun x ⇒ G) → Iok I (Mlet a f) G.

Lemma Ilambda_rule : ∀ (A B:Type)(f:A → distr B)(F:A → IU)(G:A → B → IU),
   (∀ x:A, Iok (F x) (f x) (G x)) → Iokfun F f G.

Lemma Imu_Mif_eq : ∀ (A:Type)(b:distr bool)(f1 f2:distr A)(F:A → IU),
 Ieq (Imu (Mif b f1 f2) F) (Iplus (Imultk (μ b ctrue) (Imu f1 F)) (Imultk (μ b cfalse) (Imu f2 F))).

Lemma Iifrule :
  ∀ (A:Type)(b:(distr bool))(f1 f2:distr A)(I1 I2:IU)(F:A → IU),
       Iok I1 f1 F → Iok I2 f2 F
       → Iok (Iplus (Imultk (μ b ctrue) I1) (Imultk (μ b cfalse) I2)) (Mif b f1 f2) F.

Section IFixrule.
Variables A B : Type.

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

Section IRuleseq.
Variable Q : A → B → IU.

Variable I : A → nat -m> IU.

Lemma Ifixrule :
   (∀ x:A, Iin 0 (I x O)) →
   (∀ (i:nat) (f:A → distr B),
      (Iokfun (fun x ⇒ I x i) f Q) → Iokfun (fun x ⇒ I x (S i)) (fun x ⇒ F f x) Q)
   → Iokfun (fun x ⇒ Ilim (I x)) (Mfix F) Q.
End IRuleseq.

Section ITransformFix.

Section IFix_muF.
Variable Q : A → B → IU.
Variable ImuF : (A → IU) -m> (A → IU).

Lemma ImuF_stable : ∀ I J, I ≈ J → ImuF I ≈ ImuF J.

Section IF_muF_results.
Hypothesis Iincl_F_ImuF :
    ∀ f x, f ≤ Mfix F →
                      Iincl (Imu (F f x) (Q x)) (ImuF (fun y ⇒ Imu (f y) (Q y)) x).

Lemma Iincl_fix_ifix : ∀ x, Iincl (Imu (Mfix F x) (Q x)) (fixp (D:=A → IU) ImuF x).
Hint Resolve Iincl_fix_ifix.

End IF_muF_results.

End IFix_muF.
End ITransformFix.
End IFixrule.

Lemma Flip_ctrue : μ Flip ctrue ≈ ½.

Lemma Flip_cfalse : μ Flip cfalse ≈ ½.

Lemma ok_Flip : ∀ q : bool → U, ok (½ * q true + ½ * q false) Flip q.

Lemma okup_Flip : ∀ q : bool → U, okup (½ * q true + ½ * q false) Flip q.

Hint Resolve ok_Flip okup_Flip Flip_ctrue Flip_cfalse.

Lemma Flip_eq : ∀ q : bool → U, μ Flip q ≈ ½ * q true + ½ * q false.
Hint Resolve Flip_eq.

Lemma IFlip_eq : ∀ Q : bool → IU, Ieq (Imu Flip Q) (Iplus (Imultk ½ (Q true)) (Imultk ½ (Q false))).
Hint Resolve IFlip_eq.

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

Definition WfFix : A → distr B := Fix Rwf (fun _ ⇒ distr B) F.

Hypothesis Fext : ∀ x f g, (∀ y (p:R y x), f y p ≈ g y p) → F f ≈ F g.

Lemma Acc_iter_distr :
   ∀ x, ∀ r s : Acc R x, Acc_iter (fun _⇒ distr B) F r ≈ Acc_iter (fun _⇒ distr B) F s.

Lemma WfFix_eq : ∀ x, WfFix x ≈ F (fun (y:A) (p:R y x) ⇒ WfFix y).

Variable P : distr B → Prop.
Hypothesis Pext : ∀ m1 m2, m1 ≈ m2 → P m1 → P m2.

Lemma WfFix_ind :
     (∀ x f, (∀ y (p:R y x), P (f y p)) → P (F f))
  → ∀ x, P (WfFix x).

End Wellfounded.

Ltac distrsimpl := match goal with
 | |- (Ole (fmont (μ ?d1) ?f) (fmont (μ ?d2) ?g)) ⇒ apply (mu_le_compat (m1:=d1) (m2:=d2) (Ole_refl d1) (f:=f) (g:=g)); intro
 | |- (Oeq (fmont (μ ?d1) ?f) (fmont (μ ?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 (μ (Mlet ?m ?M)) ?f)] ⇒ rewrite (Mlet_simpl m M f)
 | |- context [(fmont (μ (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 (μ Flip) ?f)] ⇒ rewrite (Flip_simpl f)
 | |- context [(fmont (μ (Discrete ?d)) ?f)] ⇒ rewrite (Discrete_simpl d);
                                                           rewrite (discrete_simpl (coeff d) (points d) f)
 | |- context [(fmont (μ (Random ?n)) ?f)] ⇒ rewrite (Random_simpl n);
                                                           rewrite (random_simpl n f)
 | |- context [(fmont (μ (Mif ?b ?f ?g)) ?h)] ⇒ unfold Mif
 | |- context [(fmont (μ (Mchoice ?p ?m1 ?m2)) ?f)] ⇒ rewrite (Mchoice_simpl p m1 m2 f)
 | |- context [(fmont (μ (im_distr ?f ?m)) ?h)] ⇒ rewrite (im_distr_simpl f m h)
 | |- context [(fmont (μ (prod_distr ?m1 ?m2)) ?h)] ⇒ unfold prod_distr
 | |- context [((mon ?f (fmonotonic:=?mf)) ?x)] ⇒ rewrite (mon_simpl f (mf:=mf) x)
end.