Require Export Probas.
Set Implicit Arguments.

Module Rules (Univ:Universe).
Module PP := (Proba Univ).

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

Lemma Mif_mon : forall (A:Type) (b b':distr bool) (m1 m2 m1' m2': distr A),
    le_distr b b' -> le_distr m1 m1' -> le_distr m2 m2'
    -> le_distr (Mif b m1 m2) (Mif b' m1' m2').
intros; unfold Mif; apply Mlet_mon; auto.
destruct x; auto.
Save.

Section Fixpoints.

Variables A B : Type.

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

Hypothesis F_mon : forall f g : A -> distr B,
  (forall x, le_distr (f x) (g x)) -> forall x, le_distr (F f x) (F g x).

Fixpoint iter (n:nat) : A -> (distr B)
:= match n with | O => fun x => (distr_null B)
                | S n => fun x => F (iter n) x
   end.

Definition Flift (dn:A->nat->distr B)(x:A)(n:nat):(distr B)
      := F (fun y => dn y n) x.

Lemma Flift_mon : forall dn : A -> nat -> distr B,
(forall (x:A) (n m:nat), (n <= m)%nat ->le_distr (dn x n) (dn x m))
 -> forall (x:A) (n m:nat), (n <= m)%nat ->le_distr (Flift dn x n) (Flift dn x m).
unfold Flift; red; intros.
apply F_mon; auto.
Save.

Hypothesis F_continuous : forall (dn:A->nat->distr B)
  (dnmon : forall x n m,(n <= m)%nat ->le_distr (dn x n) (dn x m))
  (x:A),
  (le_distr (F (fun y => mu_lub (dn y) (dnmon y)) x)
               (mu_lub (Flift dn x) (Flift_mon dn dnmon x))).

Let muf (x:A) (n:nat) := (iter n x).

Lemma muf_mon_succ : forall (n:nat) (x:A), le_distr (muf x n) (muf x (S n)).
induction n; unfold muf, le_distr; simpl; intros.
auto.
apply F_mon; auto.
Save.

Lemma muf_mon : forall (x:A) (n m:nat), (n <= m)%nat -> le_distr (muf x n) (muf x m).
induction 1; auto.
apply le_distr_trans with (muf x m); auto.
apply muf_mon_succ.
Save.

Definition Mfix (x:A) := mu_lub (fun n => iter n x) (muf_mon x).

Lemma Mfix_le_iter : forall (x : A) (n:nat), le_distr (iter n x) (Mfix x).
red; intros; unfold Mfix.
apply mu_lub_le with (muf:=fun n0:nat => iter n0 x); trivial.
Save.
Hint Resolve Mfix_le_iter.

Lemma Mfix_iter_le : forall (m:A->distr B),
              (forall (x : A) (n:nat), le_distr (iter n x) (m x)) -> forall x, le_distr (Mfix x) (m x).
red; intros; unfold Mfix.
apply mu_lub_sup with (muf:=fun n0:nat => iter n0 x); trivial.
Save.
Hint Resolve Mfix_iter_le.

Lemma Mfix_le : forall x : A, le_distr (Mfix x) (F Mfix x).
unfold Mfix at 1; red; intros.
apply mu_lub_sup; trivial.
destruct n; simpl; auto.
Save.

Lemma Mfix_sup : forall x : A, le_distr (F Mfix x) (Mfix x).
unfold Mfix.
intro x.
pose (dn:=fun (x0:A) (n:nat) => iter n x0).
apply le_distr_trans with
  (mu_lub (Flift dn x) (Flift_mon dn muf_mon x)).
apply F_continuous with
 (dn:=fun (x0:A) (n:nat) => iter n x0) (dnmon:=muf_mon) (x:=x).
red; auto.
unfold Flift, dn.
intros; apply mu_lub_sup; intros.
apply le_distr_trans with (iter (S n) x); auto.
red; simpl; intros.
apply F_mon; auto.
apply mu_lub_le with (muf:=fun n0:nat => iter n0 x); auto.
Save.

Lemma Mfix_eq : forall x : A, eq_distr (Mfix x) (F Mfix x).
red; intros; apply Ule_antisym.
apply Mfix_le; trivial.
apply Mfix_sup; trivial.
Save.

End Fixpoints.

Lemma Mfix_le_stable : forall (A B:Type) F G
        (Fmon:forall f g : A -> distr B, (forall x : A, le_distr (f x) (g x)) ->
                                                        forall x : A, le_distr (F f x) (F g x))
        (Gmon:forall f g : A -> distr B, (forall x : A, le_distr (f x) (g x)) ->
                                                        forall x : A, le_distr (G f x) (G g x)),
        (forall f x, le_distr (F f x) (G f x)) -> forall x, le_distr (Mfix F Fmon x) (Mfix G Gmon x).
intros.
apply Mfix_iter_le with (m:=Mfix G Gmon); intros.
apply le_distr_trans with (iter G n x0).
generalize x0; clear x0; induction n; simpl; intros; auto.
apply le_distr_trans with (G (iter F n) x0); auto.
apply Mfix_le_iter.
Save.

Section Continuity.

Variables A B:Type.
Variable mun : nat -> distr A.
Hypothesis mun_incr : forall n m, ((n <= m)%nat) -> le_distr (mun n) (mun m).
Hypothesis mun_cont : forall n, continuous (mu (mun n)).
Variable Mn : A -> nat -> distr B.
Hypothesis Mn_incr : forall x n m, ((n <= m)%nat) -> le_distr (Mn x n) (Mn x m).
Lemma Mlet_incr :
             forall n m,(n <= m)%nat ->
             le_distr (Mlet (mun n) (fun x => Mn x n)) (Mlet (mun m) (fun x => Mn x m)).
intros; apply Mlet_mon; auto.
Save.

Lemma Mlet_continuous :
             le_distr (Mlet (mu_lub mun mun_incr) (fun x => mu_lub (Mn x) (Mn_incr x)))
                          (mu_lub (fun n => Mlet (mun n) (fun x => Mn x n)) Mlet_incr).
red; simpl; unfold mu_lub_, star; intro.
apply Ule_trans with
 (lub (fun n : nat => lub (fun n0 => mu (mun n) (fun x => mu (Mn x n0) f)))).
apply lub_le_stable; intro.
apply (mun_cont n (fn:=fun n0 x => mu (Mn x n0) f)).
repeat red; intros.
apply Mn_incr; auto with arith.
rewrite (double_lub_simpl
            (fun n m => mu (mun n) (fun x : A => mu (Mn x m) f))); auto.
intros; apply (@mun_incr n (S n)) with (f:=fun x : A => mu (Mn x m) f); auto with arith.
intros; apply mu_monotonic; repeat red; intros; auto.
apply (@Mn_incr x m (S m)) with (f:=f); auto with arith.
Save.

Variable Fn : nat -> (A -> distr B) -> A -> distr B.

Hypothesis Fn_mon : forall n (f g : A -> distr B),
  (forall x, le_distr (f x) (g x)) -> forall x, le_distr (Fn n f x) (Fn n g x).

Hypothesis Fn_incr : forall f x n m, (n <= m)%nat ->le_distr (Fn n f x) (Fn m f x).

Hypothesis Fn_continuous : forall n (dn:A->nat->distr B)
  (dnmon : forall x n m,(n <= m)%nat -> le_distr (dn x n) (dn x m))
  (x:A),
  (le_distr (Fn n (fun y => mu_lub (dn y) (dnmon y)) x)
               (mu_lub (Flift (Fn n) dn x) (Flift_mon (Fn n) (Fn_mon n) dn dnmon x))).

Lemma Mfix_incr : forall x,
             forall n m,(n <= m)%nat ->
             le_distr (Mfix (Fn n) (Fn_mon n) x) (Mfix (Fn m) (Fn_mon m) x).
intros; apply Mfix_le_stable; auto.
Save.

Lemma mu_lub_mon :
             forall (f g : A -> distr B), (forall x, le_distr (f x) (g x))
             -> forall x, le_distr (mu_lub (fun n => Fn n f x) (Fn_incr f x))
                                           (mu_lub (fun n => Fn n g x) (Fn_incr g x)).
repeat red; intros.
simpl; unfold mu_lub_.
apply lub_le_stable;intros.
apply (Fn_mon n f g) with (x:=x); auto.
Save.

Lemma iter_incr : forall k x,
             forall n m,(n <= m)%nat ->
             le_distr (iter (Fn n) k x) (iter (Fn m) k x).
induction k; intros; simpl; auto.
apply le_distr_trans with (Fn m (iter (Fn n) k) x); auto.
Save.
Hint Resolve iter_incr.

Lemma iter_continuous :
       forall k x, le_distr (iter (fun f x => mu_lub (fun n => Fn n f x) (Fn_incr f x)) k x)
                                   (mu_lub (fun n => iter (Fn n) k x) (iter_incr k x)).
induction k; simpl; intros; auto.
red; simpl; unfold mu_lub_; intros.
apply Ule_trans with
 (lub (fun n => mu (Fn n (fun x => mu_lub (fun n : nat => iter (Fn n) k x) (iter_incr k x)) x) f)).
apply lub_le_stable; intros.
apply (Fn_mon n); auto with arith.
pose (dn:=fun (x0:A) (n0:nat) => iter (Fn n0) k x0).
pose (dnmon:= iter_incr k).
apply Ule_trans with
 (lub (fun n : nat =>
         mu (mu_lub (Flift (Fn n) dn x)
                            (Flift_mon (Fn n) (Fn_mon n) dn dnmon x)) f)).
apply lub_le_stable; intro.
apply (Fn_continuous n dn dnmon x f).
unfold dn; simpl; unfold mu_lub_,Flift.
rewrite (double_lub_simpl (fun n m => mu (Fn n (fun y : A => iter (Fn m) k y) x) f)); auto.
apply lub_le_stable; intro.
apply (@Fn_mon n (fun y : A => iter (Fn n) k y) (iter (Fn n) k)); auto.
intros; apply (@Fn_incr (fun y : A => iter (Fn m) k y) x n (S n)); auto with arith.
intros; apply (@Fn_mon n (fun y : A => iter (Fn m) k y) (fun y : A => iter (Fn (S m)) k y)); auto.
Save.
Hint Resolve iter_continuous.

Lemma MFix_continuous :
       forall x,
       le_distr (Mfix (fun f x => mu_lub (fun n => Fn n f x) (Fn_incr f x)) mu_lub_mon x)
                   (mu_lub (fun n => Mfix (Fn n) (Fn_mon n) x) (Mfix_incr x)).
red; intros.
simpl; unfold mu_lub_.
apply Ule_trans with
 (lub (fun n : nat =>
            mu (mu_lub (fun m => iter (Fn m) n x) (iter_incr n x)) f)).
apply lub_le_stable; intros; apply iter_continuous.
simpl; unfold mu_lub_; auto.
Save.

End Continuity.

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 -> fle q q' -> ok p e q -> ok p' e q'.
unfold ok; intros.
apply Ule_trans with p; auto.
apply Ule_trans with (mu e q); auto.
apply (mu_monotonic e); auto.
Save.

Lemma ok_eq_compat : forall (A:Type) (p p':U) (e e':distr A) (q q':A->U),
    p' == p -> (feq q q') -> eq_distr e e' -> ok p e q -> ok p' e' q'.
unfold ok; intros.
apply Ule_trans with p; auto.
apply Ule_trans with (mu e q); auto.
apply Ule_trans with (mu e' q); auto.
apply (mu_monotonic e'); auto.
Save.

Lemma okfun_le_compat : forall (A B:Type) (p p':A -> U) (e:A -> distr B) (q q':A->B->U),
    fle p' p -> (forall x,fle (q x) (q' x)) -> okfun p e q -> okfun p' e q'.
unfold okfun; intros.
apply ok_le_compat with (p x) (q x); auto.
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).
unfold ok; intros A k p e f oka.
rewrite (mu_stable_mult e k f).
apply Umult_le_compat_right; trivial.
Save.

Lemma ok_inv : forall (A:Type)(p:U)(e:distr A)(f : A -> U), ok p e f -> mu e (finv f) <= [1-]p.
unfold ok; intros A p e f oka.
apply Ule_trans with ([1-](mu e f)); auto.
Save.

Lemma okup_le_compat : forall (A:Type) (p p':U) (e:distr A) (q q':A->U),
    p <= p' -> fle q' q -> okup p e q -> okup p' e q'.
unfold okup; intros.
apply Ule_trans with p; auto.
apply Ule_trans with (mu e q); auto.
apply (mu_monotonic e); auto.
Save.

Lemma okup_eq_compat : forall (A:Type) (p p':U) (e e':distr A) (q q':A->U),
    p == p' -> (feq q q') -> eq_distr e e' -> okup p e q -> okup p' e' q'.
unfold okup; intros.
apply Ule_trans with p; auto.
apply Ule_trans with (mu e q); auto.
apply Ule_trans with (mu e' q); auto.
apply (mu_monotonic e'); auto.
Save.

Lemma upfun_le_compat : forall (A B:Type) (p p':A -> U) (e:A -> distr B) (q q':A->B->U),
    fle p p' -> (forall x,fle (q' x) (q x)) -> upfun p e q -> upfun p' e q'.
unfold upfun; intros.
apply okup_le_compat with (p x) (q x); auto.
Save.

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).
unfold okup; intros A k p e f oka.
rewrite (mu_stable_mult e k f).
apply Umult_le_compat_right; trivial.
Save.

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.
unfold ok,okfun,Mlet; simpl; intros.
apply Ule_trans with (mu a p); auto.
unfold star.
apply mu_monotonic; red; auto.
Save.

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.
unfold okup,upfun,Mlet; simpl; intros.
apply Ule_trans with (mu a p); auto.
unfold star.
apply mu_monotonic; red; auto.
Save.

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.
trivial.
Save.

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.
trivial.
Save.

Lemma combiok : forall (A:Type) p q (f1 f2 : A -> U), p <= [1-]q -> fplusok (fmult p f1) (fmult q f2).
unfold fplusok, fmult, fle, finv; intros.
apply Ule_trans with p; auto.
apply Ule_trans with ([1-]q); auto.
Save.
Hint Resolve combiok.

Lemma fmult_fplusok : forall (A:Type) p q (f1 f2 : A -> U), fplusok f1 f2 -> fplusok (fmult p f1) (fmult q f2).
unfold fplusok, fmult, fle, finv; intros.
apply Ule_trans with (f1 x); auto.
apply Ule_trans with ([1-]f2 x); auto.
Save.
Hint Resolve fmult_fplusok.

Lemma ifok : forall f1 f2, fplusok (fmult f1 ctrue) (fmult f2 cfalse).
intros; apply fmult_fplusok; unfold fplusok,ctrue,cfalse,finv; auto.
Save.
Hint Resolve ifok.

Lemma Mif_eq : forall (A:Type)(b:(distr bool))(f1 f2:distr A)(q:A->U),
        (mu (Mif b f1 f2) q) == (mu f1 q) * (mu b ctrue) + (mu f2 q) * (mu b cfalse).
intros.
apply Ueq_trans with (mu b (fplus (fmult (mu f1 q) ctrue) (fmult (mu f2 q) cfalse))).
intros; unfold Mif,Mlet,star; simpl.
apply (mu_stable_eq b); red; intro.
unfold fplus,fmult;destruct x; simpl.
setoid_rewrite (Umult_one_right (mu f1 q));
setoid_rewrite (Umult_zero_right (mu f2 q));
auto.
setoid_rewrite (Umult_zero_right (mu f1 q));
setoid_rewrite (Umult_one_right (mu f2 q));
auto.
setoid_rewrite (mu_stable_plus b (f:=(fmult (mu f1 q) ctrue))
                                (g:=(fmult (mu f2 q) cfalse))
                (ifok (mu f1 q) (mu f2 q))).
setoid_rewrite (mu_stable_mult b (mu f1 q) ctrue).
setoid_rewrite (mu_stable_mult b (mu f2 q) cfalse); trivial.
Save.

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 ctrue) + p2 * (mu b cfalse)) (Mif b f1 f2) q.
unfold ok; intros.
setoid_rewrite (Mif_eq b f1 f2 q).
apply Uplus_le_compat.
apply Umult_le_compat_left; auto.
apply Umult_le_compat_left; auto.
Save.

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 ctrue) + p2 * (mu b cfalse)) (Mif b f1 f2) q.
unfold okup; intros.
setoid_rewrite (Mif_eq b f1 f2 q).
apply Uplus_le_compat.
apply Umult_le_compat_left; auto.
apply Umult_le_compat_left; auto.
Save.

Section Fixrule.
Variables A B : Type.

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

Hypothesis F_mon : forall f g : A -> (distr B),
  (forall x, le_distr (f x) (g x)) -> forall x, le_distr (F f x) (F g x).

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

Lemma fixrule :
   (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 F_mon) q.
red; intros p0 Hrec.
assert (forall n:nat,
        (okfun (fun x => (p x n)) (fun x => iter F n x) q)).
induction n; simpl; auto.
repeat red; intros; auto.
red; intros.
apply lub_le; auto.
intro n; apply Ule_trans with (mu (iter F n x) (q x)).
apply (H n).
apply Mfix_le_iter; auto.
Save.

Lemma fixrule_up_lub :
   (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 F_mon) q.
repeat red; intros.
unfold Mfix,mu_lub,mu_lub_; simpl.
apply lub_le_stable.
intro n; generalize x; induction n; simpl; intros; auto.
apply (H n (iter F n) IHn x0).
Save.

Lemma okup_fixrule_glb :
   (forall (x:A) n, p x (S n) <= p x n)->
   (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 F_mon) q.
red; intros pdecr Hrec x.
assert (forall n:nat,
        (upfun (fun x => (p x n))
        (fun x => (iter F n x)) q)).
induction n; simpl; auto.
repeat red; intros; auto.
red; intros.
unfold Mfix; simpl.
unfold mu_lub_.
apply lub_glb_le; auto.
intros; apply (@muf_mon_succ A B F F_mon n x); auto.
intro n; apply (H n).
Save.
End Ruleseq.

Lemma okup_fixrule_inv :
   forall (q : A -> B -> U) (p : A -> U),
   (forall (f:A->distr B), upfun p f q -> upfun p (fun x => F f x) q)
           -> upfun p (Mfix F F_mon) q.
unfold upfun, okup; intros.
unfold Mfix; simpl; unfold mu_lub_.
apply lub_le.
intro n; generalize x; induction n; simpl; auto.
Save.

Section TransformFix.

Section Fix_muF.
Variable q : A -> B -> U.
Variable muF : (A -> U) -> A -> U.
Hypothesis muF_mon : Fmonotonic muF.

Lemma muF_stable : Fstable muF.
auto.
Save.

Definition mu_muF_commute_le :=
  forall f x, (forall y, le_distr (f y) (Mfix F F_mon y)) ->
                         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 F_mon x) (q x) <= mufix muF x.
intros; unfold mufix,Mfix,mu_lub; simpl.
unfold mu_lub_.
apply lub_le_stable; intros.
generalize x; induction n; simpl; intros; auto.
apply Ule_trans with (muF (fun y => mu (iter F n y) (q y)) x0).
apply F_muF_le.
repeat red; intros; unfold Mfix, mu_lub,mu_lub_;simpl.
apply le_lub with (f:=fun n => mu (iter F n y) f); auto.
apply muF_mon; auto.
Save.
Hint Resolve mu_mufix_le.

Lemma muF_le : forall f, (fle (muF f) f)
      -> forall x, mu (Mfix F F_mon x) (q x) <= f x.
intros; apply Ule_trans with (mufix muF x); auto.
apply mufix_inv; auto.
Save.

Hypothesis muF_F_le :
    forall f x, (forall y, le_distr (f y) (Mfix F F_mon y)) ->
                        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 F_mon x) (q x).
intros; unfold mufix,Mfix,mu_lub; simpl.
unfold mu_lub_.
apply lub_le_stable; intros.
generalize x; induction n; simpl; intros; auto.
apply Ule_trans with (muF (fun y => mu (iter F n y) (q y)) x0).
apply muF_mon; auto.
apply muF_F_le.
repeat red; intros; unfold Mfix, mu_lub,mu_lub_;simpl.
apply le_lub with (f:=fun n => mu (iter F n y) f); auto.
Save.

End F_muF_results.
Hint Resolve mu_mufix_le mufix_mu_le.

Lemma mufix_mu :
   (forall f x, (forall y, le_distr (f y) (Mfix F F_mon y))
          -> mu (F f x) (q x) == muF (fun y => mu (f y) (q y)) x)
   -> forall x, mufix muF x == mu (Mfix F F_mon x) (q x).
intros; apply Ule_antisym; auto.
apply mufix_mu_le; intros; auto.
rewrite (H f x0); auto.
Save.
Hint Resolve mufix_mu.
End Fix_muF.

Section Fix_Term.

Definition pterm (x:A) := mu (Mfix F F_mon x) (f_one B).
Variable muFone : (A -> U) -> A -> U.

Hypothesis muF_mon : Fmonotonic muFone.

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

Hypothesis muF_cont : Fcontlub muFone.

Lemma muF_pterm : feq pterm (muFone pterm).
red; intros; unfold pterm.
rewrite <- (mufix_mu (fun (x:A) => f_one B) muF_mon F_muF_eq_one x).
rewrite mufix_eq; auto.
apply muF_stable; auto.
red; intros; auto.
apply (mufix_mu (fun (x:A) => f_one B) muF_mon F_muF_eq_one x0).
Save.
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 : (A -> U) -> A -> U.

Hypothesis muF_mon_inv : Fmonotonic muFqinv.

Hypothesis F_muF_le_inv : mu_muF_commute_le qinv muFqinv.

Lemma muF_le_term : forall f, fle (muFqinv (finv f)) (finv f) ->
    forall x, f x & pterm x <= mu (Mfix F F_mon x) (q x).
intros; apply Ule_trans with (mu (Mfix F F_mon x) (fesp (q x) (f_one B))).
apply Ule_trans with ([1-] mu (Mfix F F_mon x) (qinv x) & pterm x).
apply Uesp_le_compat; auto.
apply Uinv_le_perm_right.
apply muF_le with (muF:=muFqinv) (q:=qinv) (f:=finv f) (x:=x); auto.
unfold pterm; replace (qinv x) with (finv (q x)); auto.
apply mu_monotonic; intro; unfold fesp,f_one; repeat Usimpl; auto.
Save.

Lemma muF_le_term_minus :
forall f, fle f pterm -> fle (muFqinv (fminus pterm f)) (fminus pterm f) ->
    forall x, f x <= mu (Mfix F F_mon x) (q x).
intros; apply Ule_trans with ((f x + [1-]pterm x) & pterm x).
red in H; rewrite Uplus_inv_esp_simpl; auto.
apply muF_le_term with (f:=fun y => f y + [1-]pterm y); auto.
apply fle_trans with (muFqinv (fminus pterm f)).
apply muF_mon_inv; unfold fle, fminus, finv; auto.
apply fle_trans with (fminus pterm f); auto.
unfold fle, fminus, Uminus, finv; auto.
Save.

Variable muFq : (A -> U) -> A -> U.

Hypothesis muF_mon : Fmonotonic muFq.

Hypothesis F_muF_le : mu_muF_commute_le q muFq.

Lemma muF_eq : forall f, fle (muFq f) f -> fle (muFqinv (finv f)) (finv f)->
    forall x, pterm x == 1 -> mu (Mfix F F_mon x) (q x) == f x.
intros; apply Ule_antisym.
apply muF_le with (muF:=muFq); auto.
apply Ule_trans with (f x & pterm x).
rewrite H1; auto.
apply muF_le_term; auto.
Save.

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 (f:A->U) (x:A) : U:=
     mu (stop x) (fun b => if b then a else mu (step x) f).

Fixpoint loopn (n:nat)(x:A){struct n} : U :=
    match n with O => 0
                       | S p => Loop (loopn p) x
    end.

Definition loop (x:A) : U := lub (fun n => loopn n x).

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 F_mon) q.
intros; unfold loop; simpl.
apply fixrule with (p:=fun x n => loopn n x); simpl; intros;auto.
unfold okfun,ok in *|-*.
intro x; apply Ule_trans with (2:=H f x).
unfold Loop; simpl; auto.
apply (mu_monotonic (stop x)); red; intros.
case x0; auto.
apply (mu_monotonic (step x)); red; auto.
Save.

Fixpoint up_loopn (n:nat)(x:A){struct n} : U :=
    match n with O => 1
                       | S p => Loop (up_loopn p) x
    end.

Definition up_loop (x:A) : U := glb (fun n => up_loopn n x).

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 F_mon) q.
intros; unfold up_loop; simpl.
apply okup_fixrule_glb with (p:=fun x n => up_loopn n x); simpl; intros;auto.
unfold upfun,okup in *|-*.
generalize x; induction n; simpl; intros; auto.
unfold Loop; simpl; auto.
apply mu_monotonic.
red; intros.
destruct x1; auto.
apply mu_monotonic; auto.
intro x.
red; apply Ule_trans with (1:=H f x).
unfold Loop; simpl; auto.
apply (mu_monotonic (stop x)); red; intros.
case x0; auto.
apply (mu_monotonic (step x)); red; auto.
Save.

End LoopRule.

End Fixrule.

Definition Imu : forall A:Type, distr A-> (A->IU) -> IU.
intros A m F; exists (mu m (fun x => low (F x))) (mu m (fun x => up (F x))).
apply mu_monotonic; auto.
Defined.

Lemma low_Imu : forall (A:Type) (e:distr A) (F: A -> IU),
             low (Imu e F) = mu e (fun x => low (F x)).
trivial.
Save.

Lemma up_Imu : forall (A:Type) (e:distr A) (F: A -> IU),
             up (Imu e F) = mu e (fun x => up (F x)).
trivial.
Save.

Lemma Imu_monotonic : forall (A:Type) (e:distr A) (F G : A -> IU),
            (forall x, Iincl (F x) (G x)) -> Iincl (Imu e F) (Imu e G).
unfold Iincl,Imu; simpl; intuition.
apply mu_monotonic; firstorder.
apply mu_monotonic; firstorder.
Save.

Lemma Imu_stable_eq : forall (A:Type) (e:distr A) (F G : A -> IU),
            (forall x, Ieq (F x) (G x)) -> Ieq (Imu e F) (Imu e G).
unfold Ieq,Imu; simpl; intuition.
apply mu_stable_eq; firstorder.
apply mu_stable_eq; firstorder.
Save.
Hint Resolve Imu_monotonic Imu_stable_eq.

Lemma Imu_singl : forall (A:Type) (e:distr A) (f:A->U),
           Ieq (Imu e (fun x => singl (f x))) (singl (mu e f)).
unfold Ieq,Imu,singl; simpl; intuition.
apply mu_stable_eq; firstorder.
apply mu_stable_eq; firstorder.
Save.

Lemma Imu_inf : forall (A:Type) (e:distr A) (f:A->U),
           Ieq (Imu e (fun x => inf (f x))) (inf (mu e f)).
unfold Ieq,Imu,inf; simpl; intuition.
exact (mu_zero e).
apply mu_stable_eq; firstorder.
Save.

Lemma Imu_sup : forall (A:Type) (e:distr A) (f:A->U),
           Iincl (Imu e (fun x => sup (f x))) (sup (mu e f)).
unfold Iincl,Imu,inf; simpl; intuition.
apply mu_monotonic; firstorder.
Save.

Lemma Iin_mu_Imu :
   forall (A:Type) (e:distr A) (F:A->IU) (f:A->U),
           (forall x, Iin (f x) (F x)) -> Iin (mu e f) (Imu e F).
unfold Iin,Imu; simpl; split.
apply mu_monotonic; firstorder.
apply mu_monotonic; firstorder.
Save.
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)
               := forall x, Iok (I x) (e x) (F x).

Lemma Iin_mu_Iok :
   forall (A:Type) (I:IU) (e:distr A) (F:A->IU) (f:A->U),
           (forall x, Iin (f x) (F x)) -> Iok I e F -> Iin (mu e f) I.
intros; apply Iincl_in with (Imu e F); auto.
Save.

Lemma Iok_le_compat : forall (A:Type) (I J:IU) (e:distr A) (F G:A->IU),
   Iincl I J -> (forall x, Iincl (G x) (F x)) -> Iok I e F -> Iok J e G.
unfold Iok; intros; apply Iincl_trans with I; auto.
apply Iincl_trans with (Imu e F); auto.
Save.

Lemma Iokfun_le_compat : forall (A B:Type) (I J:A->IU) (e:A->distr B) (F G:A->B->IU),
   (forall x, Iincl (I x) (J x)) -> (forall x y, Iincl (G x y) (F x y)) -> Iokfun I e F -> Iokfun J e G.
unfold Iokfun; intros; apply Iok_le_compat with (I x) (F x); auto.
Save.

Lemma Iunit_eq : forall (A: Type) (a:A) (F:A->IU), Ieq (Imu (Munit a) F) (F a).
intros; unfold Ieq,Imu,Munit; simpl; auto.
Save.

Lemma Ilet_eq : forall (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)).
unfold Ieq,Imu,Mlet,Iincl; simpl; intuition.
Save.
Hint Resolve Ilet_eq.

Lemma Iapply_rule : forall (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.
unfold Iokfun,Iok;intros.
apply Ieq_incl_trans with (Imu a (fun x => Imu (f x) G)); auto.
apply Iincl_trans with (Imu a F); auto.
Save.

Lemma Ilambda_rule : forall (A B:Type)(f:A->distr B)(F:A->IU)(G:A -> B->IU),
   (forall x:A, Iok (F x) (f x) (G x)) -> Iokfun F f G.
trivial.
Save.

Lemma Imu_Mif_eq : forall (A:Type)(b:distr bool)(f1 f2:distr A)(F:A->IU),
 Ieq (Imu (Mif b f1 f2) F) (Iplus (Imultk (mu b ctrue) (Imu f1 F)) (Imultk (mu b cfalse) (Imu f2 F))).
red; intros.
rewrite low_Imu; rewrite up_Imu.
repeat rewrite Mif_eq.
repeat rewrite low_Iplus; repeat rewrite low_Imultk.
repeat rewrite up_Iplus; repeat rewrite up_Imultk.
repeat rewrite low_Imu; repeat rewrite up_Imu; auto.
Save.

Lemma Iifrule :
  forall (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 (mu b ctrue) I1) (Imultk (mu b cfalse) I2)) (Mif b f1 f2) F.
unfold Iok; intros.
apply Ieq_incl_trans with (1:=Imu_Mif_eq b f1 f2 F).
split.
repeat rewrite low_Iplus; repeat rewrite low_Imultk.
apply Uplus_le_compat; auto.
repeat rewrite up_Iplus; repeat rewrite up_Imultk.
apply Uplus_le_compat; auto.
Save.

Section IFixrule.
Variables A B : Type.

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

Hypothesis F_mon : forall f g : A -> (distr B),
  (forall x, le_distr (f x) (g x)) -> forall x, le_distr (F f x) (F g x).

Section IRuleseq.
Variable Q : A -> B -> IU.

Variable I : A -> nat -> IU.
Hypothesis decrp : forall x n, Iincl (I x (S n)) (I x n).

Lemma Ifixrule :
   (forall x:A, Iin 0 (I x O)) ->
   (forall (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 => lim (I x) (decrp x)) (Mfix F F_mon) Q.
red; intros p0 Hrec.
assert (forall n:nat,
        (Iokfun (fun x => (I x n)) (fun x => iter F n x) Q)).
induction n; simpl; auto.
split.
rewrite low_lim; rewrite low_Imu.
apply lub_le; auto.
intro n; apply Ule_trans with (low (Imu (iter F n x) (Q x))).
case (H n x); auto.
rewrite low_Imu; apply Mfix_le_iter; auto.
rewrite up_lim; rewrite up_Imu.
unfold Mfix,mu_lub,mu_lub_; simpl.
apply lub_glb_le; intros; auto.
apply (@muf_mon_succ A B F F_mon n x); auto.
case (H n x); auto.
Save.
End IRuleseq.

Section ITransformFix.

Section IFix_muF.
Variable Q : A -> B -> IU.
Variable ImuF : (A -> IU) -> A -> IU.
Hypothesis ImuF_mon : forall I J,
      (forall x, Iincl (I x) (J x)) -> forall x, Iincl (ImuF I x) (ImuF J x).

Lemma ImuF_stable : forall I J,
      (forall x, Ieq (I x) (J x)) -> forall x, Ieq (ImuF I x) (ImuF J x).
intros; apply Iincl_antisym; auto.
Save.

Section IF_muF_results.
Hypothesis Iincl_F_ImuF :
    forall f x, (forall y, le_distr (f y) (Mfix F F_mon y)) ->
                      Iincl (Imu (F f x) (Q x)) (ImuF (fun y => Imu (f y) (Q y)) x).

Lemma Iincl_fix_ifix : forall x, Iincl (Imu (Mfix F F_mon x) (Q x)) (Ifix ImuF ImuF_mon x).
assert (forall n x, Iincl (Imu (iter F n x) (Q x)) (Iiter ImuF n x)).
induction n; simpl; intros; auto.
apply Iincl_trans with (ImuF (fun y => Imu (iter F n y) (Q y)) x).
apply Iincl_F_ImuF.
repeat red; intros; unfold Mfix, mu_lub,mu_lub_;simpl.
apply le_lub with (f:=fun n => mu (iter F n y) f); auto.
apply ImuF_mon; auto.
intros; unfold Iincl, Ifix,Imu,Mfix,mu_lub; simpl.
unfold mu_lub_; split.
apply lub_le_stable; intros.
case (H n x); intros.
apply Ule_trans with (low (Imu (iter F n x) (Q x))); auto.
apply lub_glb_le; intros; auto.
apply (@muf_mon_succ A B F F_mon n x).
case (Iiter_decr ImuF ImuF_mon x n); auto.
case (H n x); intros.
apply Ule_trans with (up (Imu (iter F n x) (Q x))); auto.
Save.
Hint Resolve Iincl_fix_ifix.

End IF_muF_results.

End IFix_muF.
End ITransformFix.
End IFixrule.

Lemma Flip_ctrue : mu Flip ctrue == [1/2].
unfold Flip; auto.
Save.

Lemma Flip_cfalse : mu Flip cfalse == [1/2].
unfold Flip; auto.
Save.

Lemma ok_Flip : forall q : bool -> U, ok ([1/2] * q true + [1/2] * q false) Flip q.
red; unfold Flip, flip; simpl; auto.
Save.

Lemma okup_Flip : forall q : bool -> U, okup ([1/2] * q true + [1/2] * q false) Flip q.
red; unfold Flip, flip; simpl; auto.
Save.

Hint Resolve ok_Flip okup_Flip Flip_ctrue Flip_cfalse.

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

Lemma IFlip_eq : forall Q : bool -> IU, Ieq (Imu Flip Q) (Iplus (Imultk [1/2] (Q true)) (Imultk [1/2] (Q false))).
red; unfold Flip, flip; simpl; auto.
Save.
Hint Resolve IFlip_eq.