Library ALEA.Prog_Intervals

Prog_Intervals.v: Rules for distributions and intervals

Add Rec LoadPath "." as ALEA.

Require Export Prog.
Require Export Intervals.

Distributions operates on intervals

Definition Imu : forall A:Type, distr A -> (A -> IU) -> IU.

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

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

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

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

Lemma Imu_inf : forall (A:Type) (e:distr A) (f:A -> U),
           Ieq (Imu e (fun x => inf (f x))) (inf (mu e f)).

Lemma Imu_sup : forall (A:Type) (e:distr A) (f:A -> U),
           Iincl (Imu e (fun x => sup (f x))) (sup (mu e f)).

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


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.

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.

Rule for values

Lemma Iunit_eq : forall (A: Type) (a:A) (F:A -> IU), Ieq (Imu (Munit a) F) (F a).

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

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.

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 B2U) (Imu f1 F)) (Imultk (mu b NB2U) (Imu f2 F))).

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 B2U) I1) (Imultk (mu b NB2U) I2)) (Mif b f1 f2) F.

Rule for fixpoints

with phi x = F phi x , p a decreasing sequence of intervals functions ( p (i+1) x is a bubset of (p i x) such that (p 0 x) contains 0 for all x.
forall f i, (forall x, iok (p i x) f (q x)) => forall x, iok (p (i+1) x) (F f x) (q x) implies forall x, iok (lub p x) (phi x) (q x)
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 :
   (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.
End IRuleseq.

Section ITransformFix.

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

Lemma ImuF_stable : forall I J, I==J -> ImuF I == ImuF J.

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 -> IU) ImuF x).
Hint Resolve Iincl_fix_ifix.

End IF_muF_results.

End IFix_muF.
End ITransformFix.
End IFixrule.

Lemma IFlip_eq : forall Q : bool -> IU, Ieq (Imu Flip Q) (Iplus (Imultk [1/2] (Q true)) (Imultk [1/2] (Q false))).
Hint Resolve IFlip_eq.