Library Prog

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)
This page has been generated by coqdoc