``` ```

# Prog.v: Composition of distributions

``` Require Export Probas. Set Implicit Arguments. Module Rules (Univ:Universe). Module PP := (Proba Univ). ```

## Conditional

``` 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) (b1 b2:Distr bool) (m1 m2 n1 n2: Distr A),     b1 <= b2 -> m1 <= m2 -> n1 <= n2 -> Mif b1 m1 n1 <= Mif b2 m2 n2. intros; unfold Mif. apply Mlet_le_compat ; auto. intro x; destruct x; auto. Save. Definition MIf : forall (A:Type), Distr bool -m> Distr A -m> Distr A -m> Distr A. intro A; exists (fun b => le_stable2_mon (fun m1 m2 n1 n2 (H1:m1 <= m2) (H2:n1<=n2) =>                                                                     Mif_mon (Ole_refl b) H1 H2)). red; simpl; intros; auto. Defined. ```

## Probabilistic choice

``` ```

### The distribution associated to `pchoice p` is

``` Definition pchoice : forall A, U -> M A -> M A -> M A. intros A p m1 m2;      exists (fun (f : A -> U) => p * m1 f + [1-]p * m2 f). red; intros; simpl. apply Uplus_le_compat; auto. Defined. Lemma pchoice_simpl : forall A p (m1 m2:M A) f,       pchoice p m1 m2 f = p * m1 f + [1-]p * m2 f. trivial. Save. Definition Mchoice (A:Type) (p:U) (m1 m2: Distr A) : Distr A. intros A p m1 m2; exists (pchoice p (mu m1) (mu m2)). red; intros; repeat (rewrite pchoice_simpl). apply Ole_trans with  (p * [1-]mu m1 f + [1-] p * [1-]mu m2 f); auto. apply Uplus_le_compat; repeat Usimpl; auto. red; intros; repeat (rewrite pchoice_simpl). rewrite (mu_stable_plus m1 H); rewrite (mu_stable_plus m2 H). rewrite Udistr_plus_left; auto. rewrite Udistr_plus_left; auto. repeat norm_assoc_left; repeat Usimpl. repeat norm_assoc_right; repeat Usimpl; auto. red; intros; repeat (rewrite pchoice_simpl). rewrite (mu_stable_mult m1 k f); rewrite (mu_stable_mult m2 k f). rewrite Udistr_plus_left; auto. red; intros; rewrite pchoice_simpl. apply Ole_trans with     (p * lub (mu m1 @ h) + [1-] p * lub (mu m2 @ h)). apply Uplus_le_compat; repeat Usimpl; auto. repeat rewrite <- lub_eq_mult. rewrite <- lub_eq_plus; auto. 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. trivial. Save. Lemma Mchoice_mon : forall (A:Type) (p:U) (m1 m2 n1 n2: Distr A),         m1<=m2 -> n1<=n2 -> Mchoice p m1 n1 <= Mchoice p m2 n2. simpl; intros. apply Uplus_le_compat; repeat Usimpl; auto. Save. Add Morphism Mchoice with signature Oeq ==> Oeq ==> Oeq ==> Oeq as Mchoice_eq_compat. intros; apply eq_distr_intro; simpl; intros. rewrite H; apply Uplus_eq_compat; repeat Usimpl; auto. Save. Hint Immediate Mchoice_eq_compat. Definition MChoice A (p:U) : Distr A -m> Distr A -m> Distr A :=                le_stable2_mon (Mchoice_mon (A:=A) p). Lemma MChoice_simpl : forall A (p:U) (m1 m2 : Distr A), MChoice A p m1 m2 = Mchoice p m1 m2. trivial. Save. Lemma Mchoice_sym_le : forall (A:Type) (p:U) (m1 m2: Distr A),             Mchoice p m1 m2 <= Mchoice ([1-]p) m2 m1. simpl; intros. rewrite Uplus_sym; repeat Usimpl; auto. Save. 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. intros; apply Ole_antisym; auto. apply Ole_trans with (Mchoice ([1-][1-]p) m1 m2); auto. Save. Lemma Mchoice_continuous_right     : forall (A:Type) (p:U) (m: Distr A), continuous (D1:=cDistr A) (D2:=cDistr A) (MChoice A p m). red; intros; intro f. rewrite (MChoice_simpl p m). rewrite (Mchoice_simpl p m). simpl mu at 2. rewrite lub_fun_eq. rewrite <- (lub_eq_mult ([1-]p) ((Mu A @ h) <_> f)). rewrite <- lub_eq_plus_cte_left; auto. Save. Hint Resolve Mchoice_continuous_right. Lemma Mchoice_continuous_left     : forall (A:Type) (p:U) (m: Distr A), continuous (D1:=cDistr A) (D2:=cDistr A) (MChoice A p <_> m). red; intros. rewrite fmon_app_simpl. rewrite (MChoice_simpl (A:=A) p). rewrite Mchoice_sym. apply Ole_trans with (lub (c:=cDistr A) ((MChoice A ([1-] p) m)@h)). apply (Mchoice_continuous_right ([1-]p) m h). apply lub_le_stable; intros; intro f; simpl; auto. Save. Lemma Mchoice_continuous : forall (A:Type) (p:U), continuous2 (D1:=cDistr A) (D2:=cDistr A) (D3:=cDistr A) (MChoice A p). intros; apply continuous_continuous2; intros. apply (Mchoice_continuous_right (A:=A) p). apply (Mchoice_continuous_left (A:=A) p). Save. ```

## Fixpoints

``` Definition Mfix (A B:Type) (F: (A -d> cDistr B) -m> A -d> cDistr B) : A-d>cDistr B := fixp F. Definition MFix (A B:Type) : ((A -d> cDistr B) -m> A -d> cDistr B) -m> A-d>cDistr B            := Fixp (A -d> cDistr B). Lemma Mfix_le : forall (A B:Type) (F: (A -d> cDistr B) -m> A -d> cDistr B) (x :A),             Mfix F x <= F (Mfix F) x. intros; unfold Mfix; apply (fixp_le F x). Save. Lemma Mfix_eq : forall (A B:Type) (F: (A -d> cDistr B) -m> A -d> cDistr B), continuous F -> forall (x :A), Mfix F x == F (Mfix F) x. intros; unfold Mfix; apply ford_eq_elim with (n:=x). apply (fixp_eq H). Save. Hint Resolve Mfix_le Mfix_eq. Lemma Mfix_le_stable : forall (A B:Type) (F G : (A-d>cDistr B)-m>A-d>cDistr B),         F <= G -> Mfix F <= Mfix G. intros; unfold Mfix; auto. Save. Definition Miter (A B:Type) := Cpo.iter (D:=A -d> cDistr B). Lemma Mfix_le_iter : forall (A B:Type) (F:(A -d> cDistr B)-m> A -d> cDistr B) (n:nat),      Miter F n <= Mfix F. unfold Miter,Mfix,fixp; auto. Save. ```

## Continuity

``` Section Continuity. Variables A B:Type. Lemma Mlet_continuous_left     : forall a:Distr A, continuous (D1:=A-d>cDistr B) (D2:=cDistr B) (MLet A B a). red; intros; intro f. rewrite (MLet_simpl (A:=A) (B:=B)). apply Ole_trans with (mu a (fun x:A => lub ((Mu B @ (h <o> x)) <_> f))); auto. apply Ole_trans with (mu a (lub (c:=A-d>U) (ford_shift (fun x:A => ((Mu B @ (h <o> x)) <_> f))))); auto. apply Ole_trans with (1 := mu_continuous a (ford_shift (fun x : A => (Mu B @ (h <o> x)) <_> f))); auto. Save. Lemma Mlet_continuous_right     : forall F:A->Distr B, continuous (D1:=cDistr A) (D2:=cDistr B) (MLet A B <_> F). red; intros; intro f. rewrite fmon_app_simpl. rewrite (MLet_simpl (A:=A) (B:=B)). simpl; auto. Save. Hint Resolve Mlet_continuous_right Mlet_continuous_left. Lemma Mlet_continuous2 : continuous2 (D1:=cDistr A) (D2:= A-d>cDistr B) (D3:=cDistr B) (MLet A B). intros; apply continuous_continuous2; auto. Save. Hint Resolve Mlet_continuous2. Lemma Mlet_lub_le : forall (mun:natO-m>cDistr A) (Mn : natO-m>(A-d>cDistr B)),             Mlet (lub mun) (lub Mn) <= lub (c:=cDistr B) ((MLet A B @2 mun) Mn). intros; apply Mlet_continuous2 with (f:=mun) (g:=Mn). Save. Lemma Mfix_continuous :      forall (Fn : natO -m> (A -d> cDistr B) -c> A -d> cDistr B),      (forall n, continuous (Fn n)) ->      Mfix (lub Fn) <= lub (MFix A B @ Fn). unfold Mfix, MFix; intros; apply fixp_continuous; auto. Save. End Continuity. ```

# Prog.v: Axiomatic semantics

``` ```

## Definition of correctness judgements

is defined as is defined as
``` 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). ```

## Stability properties

``` Lemma ok_le_compat : forall (A:Type) (p p':U) (e:Distr A) (q q':A-o>U),     p' <= p -> q <= q' -> ok p e q -> ok p' e q'. unfold ok; intros. apply Ole_trans with p; auto. apply Ole_trans with (mu e q); auto. Save. Lemma ok_eq_compat : forall (A:Type) (p p':U) (e e':Distr A) (q q':A-o>U),     p' == p -> q == q' -> e == e' -> ok p e q -> ok p' e' q'. unfold ok; intros. apply Ole_trans with p; auto. apply Ole_trans with (mu e q); auto. apply Ole_trans with (mu e' q); auto. Save. Lemma okfun_le_compat : forall (A B:Type) (p p':A -o> U) (e:A -o> Distr B) (q q':A-o>B-o>U),     p' <= p -> q <= q' -> 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 -o> 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 Ole_trans with ([1-](mu e f)); auto. Save. Lemma okup_le_compat : forall (A:Type) (p p':U) (e:Distr A) (q q':A-o>U),     p <= p' -> q' <= q -> okup p e q -> okup p' e q'. unfold okup; intros. apply Ole_trans with p; auto. apply Ole_trans with (mu e q); auto. Save. Lemma okup_eq_compat : forall (A:Type) (p p':U) (e e':Distr A) (q q':A-o>U),     p == p' -> q == q' -> e == e' -> okup p e q -> okup p' e' q'. unfold okup; intros. apply Ole_trans with p; auto. apply Ole_trans with (mu e q); auto. apply Ole_trans with (mu e' q); auto. Save. Lemma upfun_le_compat : forall (A B:Type) (p p':A -o> U) (e:A -o> Distr B)     (q q':A-o>B-o>U),     p <= p' -> q'<=q -> 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 -o> 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. ```

## Basic rules

``` ```

### Rules for application

``` 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 Ole_trans with (mu a p); 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 Ole_trans with (mu a p); auto. Save. ```

### Rules for abstraction

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

### Rule for conditional

``` 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; intro x. apply Ole_trans with p; auto. apply Ole_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; intro x. apply Ole_trans with (f1 x); auto. apply Ole_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; intro x; case x; auto. Save. 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 ctrue) + (mu f2 q) * (mu b cfalse). intros. apply Oeq_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); simpl; apply ford_eq_intro; intro x. unfold fplus,fmult;destruct x; simpl. rewrite (Umult_one_right (mu f1 q)); rewrite (Umult_zero_right (mu f2 q)); auto. rewrite (Umult_zero_right (mu f1 q)); rewrite (Umult_one_right (mu f2 q)); auto. rewrite (mu_stable_plus b (f:=(fmult (mu f1 q) ctrue))                                 (g:=(fmult (mu f2 q) cfalse))                 (ifok (mu f1 q) (mu f2 q))). rewrite (mu_stable_mult b (mu f1 q) ctrue). 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. 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. rewrite (Mif_eq b f1 f2 q). apply Uplus_le_compat. apply Umult_le_compat_left; auto. apply Umult_le_compat_left; auto. Save. ```

### Rule for fixpoints

with , an increasing sequence of functions starting from

``` Section Fixrule. Variables A B : Type. Variable F : (A -o> Distr B) -m> A -o> Distr B. Section Ruleseq. Variable q : A -> B -> U. Lemma fixrule_Ulub : forall (p : A -> natO -> 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. red; intros p p0 Hrec. assert (forall n:nat,         (okfun (fun x => (p x n)) (fun x => Miter F n x) q)). induction n; simpl; auto. red; red; intros; auto. red; intros. apply Ulub_le; auto. intro n; apply Ole_trans with (mu (Miter F n x) (q x)). apply (H n). apply Mfix_le_iter; auto. Save. Lemma fixrule : forall (p : A -> natO -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. red; red; intros. rewrite <- Ulub_lub. apply (fixrule_Ulub p H H0 x). Save. Lemma fixrule_up_Ulub : forall (p : A -> natO -> 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. red; red; intros. unfold Mfix; simpl. apply Ole_trans with (Ulub ((Mu B @ (Miter F <o> x)) <_> q x)); auto. apply Ulub_le_stable. intro n; generalize x; induction n; simpl; intros; auto. apply (H n (Miter F n) IHn x0). Save. Lemma fixrule_up_lub : forall (p : A -> natO -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. red; red; intros. rewrite <- Ulub_lub. apply (fixrule_up_Ulub p H x). Save. Lemma okup_fixrule_glb :    forall p : A -> natO -m> UI,    (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. red; intros p Hrec x. assert (forall n:nat,         (upfun (fun x => (p x n))         (fun x => (Miter F n x)) q)). induction n; simpl; auto. red; red; intros; auto. red; intros. unfold Mfix, fixp; simpl. apply lub_glb_le; auto. intro n; exact (H n x). Save. 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. unfold upfun, okup; intros. unfold Mfix; simpl. apply lub_le. intro n; generalize x; induction n; simpl; auto. Save. ```

### Rules using commutation properties

``` Section TransformFix. Section Fix_muF. Variable q : A -> B -> U. Variable muF : Mcpo A -m> Mcpo A. Lemma muF_stable : stable muF. auto. Save. 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. intros; unfold mufix,Mfix,mu_lub; simpl. apply lub_le_stable; intros. intro n; generalize x; induction n; simpl; intros; auto. apply Ole_trans with (muF (fun y => mu (Miter F n y) (q y)) x0). apply F_muF_le. unfold Mfix,fixp; intros. apply le_lub. apply (fmonotonic muF); auto. Save. Hint Resolve mu_mufix_le. Lemma muF_le : forall f, muF f <= f       -> forall x, mu (Mfix F x) (q x) <= f x. intros; apply Ole_trans with (mufix muF x); auto. apply mufix_inv; auto. Save. 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). intros; unfold mufix,Mfix; simpl. apply lub_le_stable; intros. intro n; generalize x; induction n; simpl; intros; auto. apply Ole_trans with (muF (fun y => mu (Miter F n y) (q y)) x0). apply (fmonotonic muF); auto. apply muF_F_le. intro y; unfold Mfix,fixp; simpl; intros f. apply le_lub with (c:=U) (f:=(Mu B @ (Cpo.iter (D:=A -d> cDistr B) F <o> y)) <_> f) (n:=n). Save. 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). intros; apply Ole_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 : Mcpo A := fun (x:A) => mu (Mfix F x) (fone B). Variable muFone : Mcpo A -m> Mcpo 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. apply feq_intro; intro x; unfold pterm. rewrite <- (mufix_mu (fun (x:A) => fone B) muFone F_muF_eq_one x). apply Oeq_trans with (muFone (mufix muFone) x); auto. apply (feq_elim (A:=A)); apply mufix_eq; auto. apply (feq_elim (A:=A)). red; apply muF_stable; auto. apply feq_intro; intro; auto. apply (mufix_mu (fun (x:A) => fone B) muFone 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 : Mcpo A -m> Mcpo 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). intros; apply Ole_trans with (mu (Mfix F x) (fesp (q x) (fone B))). apply Ole_trans with ([1-] mu (Mfix F 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,fone; repeat Usimpl; auto. Save. 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). intros; apply Ole_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 Ole_trans with (muFqinv (fminus pterm f)). apply (fmonotonic muFqinv); unfold fminus, finv; intro y. apply Uinv_le_perm_left; auto. apply Ole_trans with (fminus pterm f); auto. unfold fminus, Uminus, finv; intro y; auto. Save. Variable muFq : Mcpo A -m> Mcpo 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. intros; apply Ole_antisym. apply muF_le with (muF:=muFq); auto. apply Ole_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 : Mcpo A -m> Mcpo A. exists (fun f (x:A) => mu (stop x) (fun b => if b then a else mu (step x) f)). red; simpl; intros. apply (mu_monotonic (stop x0)); intro b; case b; auto. Defined. Lemma Loop_eq :     forall f x, Loop f x = mu (stop x) (fun b => if b then a else mu (step x) f). trivial. Save. 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. intros; unfold loop,mufix,fixp. apply okfun_le_compat with (fun x => Ulub (fun n => Cpo.iter Loop n x)) q; auto. apply fixrule_Ulub with (p:=fun x n => Cpo.iter Loop n x); simpl; intros;auto. unfold okfun,ok in *|-*. intro x; apply Ole_trans with (2:=H f x). rewrite Loop_eq; apply (mu_monotonic (stop x)); intros. intro b; case b; auto. Save. 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. intros; unfold up_loop,nufix; simpl. apply okup_fixrule_glb with (p:=fun x => (Cpo.iter (G Loop)) <o> x); simpl; intros;intro; auto. unfold upfun,okup in *|-*. red; apply Ole_trans with (1:=H f x). rewrite Loop_eq. apply (mu_monotonic (stop x)); intro x0. case x0; auto. Save. End LoopRule. End Fixrule. ```

## Rules for intervals

``` ```
Distributions operates on intervals
``` 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 e); intro x; case (H x); auto. apply (mu_monotonic e); intro x; case (H x); auto. 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 e); simpl; apply ford_eq_intro; intro x; case (H x); auto. apply (mu_stable_eq e); simpl; apply ford_eq_intro; intro x; case (H x); auto. 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 e); simpl; apply ford_eq_intro; intro x; auto. apply (mu_stable_eq e); simpl; apply ford_eq_intro; intro x; auto. 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 e); simpl; apply ford_eq_intro; intro x; auto. 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. 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 e); intro x; case (H x); auto. apply (mu_monotonic e); intro x; case (H x); auto. 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. ```

### Stability

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

### Rule for values

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

### Rule for application

``` 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) G0)); auto. apply Iincl_trans with (Imu a F); auto. Save. ```

### Rule for abstraction

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

### Rule for conditional

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

### Rule for fixpoints

with , an decreasing sequence of intervals functions () such that contains for all .

``` Section IFixrule. Variables A B : Type. Variable F : (A -o> Distr B) -m> A -o> Distr B. Section IRuleseq. Variable Q : A -> B -> IU. Variable I : A -> natO -m> IUord. 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 => Ilim (I x)) (Mfix F) Q. red; intros p0 Hrec. assert (forall n:nat,         (Iokfun (fun x => (I x n)) (fun x => Miter F n x) Q)). induction n; simpl; auto. split. rewrite low_lim; rewrite low_Imu. apply lub_le; auto. intro n; apply Ole_trans with (low (Imu (Miter 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; simpl. apply lub_glb_le; intros. case (H n x); auto. Save. End IRuleseq. Section ITransformFix. Section IFix_muF. Variable Q : A -> B -> IU. Variable ImuF : (A -o> IUord) -m> A -o> IUord. Lemma ImuF_stable : forall I J, I==J -> ImuF I == ImuF J. intros; apply monotonic_stable; auto. Save. Section IF_muF_results. Hypothesis Iincl_F_ImuF :     forall 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 : forall x, Iincl (Imu (Mfix F x) (Q x)) (fixp (D:=A-d>IUcpo) ImuF x). assert (forall n x, Iincl (Imu (Miter F n x) (Q x)) (Cpo.iter (D:=A-d>IUcpo) ImuF n x)). induction n; simpl; intros; auto. apply Iincl_trans with (ImuF (fun y => Imu (Miter F n y) (Q y)) x). apply Iincl_F_ImuF. intro y; unfold Mfix, fixp. intro f; simpl. apply le_lub with (f:=(Mu B @ (Cpo.iter (D:=A -d> cDistr B) F <o> y)) <_> f) (n:=n); auto. apply (fmonotonic ImuF); auto. intros; unfold Iincl, Imu,Mfix,fixp; simpl; split. apply lub_le_stable; intros. intro n; case (H n x); intros. apply Ole_trans with (low (Imu (Miter F n x) (Q x))); auto. apply lub_glb_le; intros; auto. case (H n x); intros. apply Ole_trans with (up (Imu (Miter F n x) (Q x))); auto. Save. Hint Resolve Iincl_fix_ifix. End IF_muF_results. End IFix_muF. End ITransformFix. End IFixrule. ```

## Rules for `Flip`

``` 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 Ole_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. ```

## Rules for total (well-founded) fixpoints

``` 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. intros x r; elim r using Acc_inv_dep; simpl; intros. case s; simpl; intros. apply Fext; auto. Save. Lemma WfFix_eq : forall x, WfFix x == F (fun (y:A) (p:R y x) => WfFix y). intro x; unfold WfFix,Fix. case (Rwf x); simpl; intros. apply Fext; intros. apply Acc_iter_distr. Save. 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). intros; pattern x; apply well_founded_ind with (R:=R); trivial; intros. apply Pext with (m1:= F (fun (y:A) (p:R y x0) => WfFix y)). apply Oeq_sym; apply WfFix_eq. apply H; auto. Save. End Wellfounded. End Rules. ```
 Global Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (109 entries) Lemma Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (85 entries) Definition Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (22 entries) Module Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (1 entry) Library Index A B C D E F G H I J K L M N O P Q R S T U V W X Y Z _ (1 entry)