Add Rec LoadPath "." as ALEA.

Set Implicit Arguments.
Require Export Uprop.
Require Export Arith.
Require Export Omega.


Open Local Scope U_scope.

Record IU : Type := mk_IU {low:U; up:U; proper:low <= up}.

Hint Resolve proper.

Definition full := mk_IU 0 1 (Upos 1).

Definition singl (x:U) := mk_IU x x (Ole_refl x).

Definition inf (x:U) := mk_IU 0 x (Upos x).

Definition sup (x:U) := mk_IU x 1 (Unit x).

Definition Iin (x:U) (I:IU) := low I <= x /\ x <= up I.

Definition Iincl I J := low J <= low I /\ up I <= up J.

Definition Ieq I J := low I == low J /\ up I == up J.
Hint Unfold Iin Iincl Ieq.

Lemma Iin_low : forall I, Iin (low I) I.

Lemma Iin_up : forall I, Iin (up I) I.

Hint Resolve Iin_low Iin_up.

Lemma Iin_singl_elim : forall x y, Iin x (singl y) -> x == y.

Lemma Iin_inf_elim : forall x y, Iin x (inf y) -> x <= y.

Lemma Iin_sup_elim : forall x y, Iin x (sup y) -> y <= x.

Lemma Iin_singl_intro : forall x y, x == y -> Iin x (singl y).

Lemma Iin_inf_intro : forall x y, x <= y -> Iin x (inf y).

Lemma Iin_sup_intro : forall x y, y <= x -> Iin x (sup y).

Hint Immediate Iin_inf_elim Iin_sup_elim Iin_singl_elim.
Hint Resolve Iin_inf_intro Iin_sup_intro Iin_singl_intro.

Lemma Iin_class : forall I x, class (Iin x I).

Lemma Iincl_class : forall I J, class (Iincl I J).

Lemma Ieq_class : forall I J, class (Ieq I J).
Hint Resolve Iin_class Iincl_class Ieq_class.

Lemma Iincl_in : forall I J, Iincl I J -> forall x, Iin x I -> Iin x J.

Lemma Iincl_low : forall I J, Iincl I J -> low J <= low I.

Lemma Iincl_up : forall I J, Iincl I J -> up I <= up J.

Hint Immediate Iincl_low Iincl_up.

Lemma Iincl_refl : forall I, Iincl I I.
Hint Resolve Iincl_refl.

Lemma Iincl_trans : forall I J K, Iincl I J -> Iincl J K -> Iincl I K.

Instance IUord : ord IU := {Oeq := fun I J => Ieq I J; Ole := fun I J => Iincl J I}.
Defined.

Lemma low_le_compat : forall I J:IU, I <= J -> low I <= low J.

Lemma up_le_compat : forall I J : IU, I <= J -> up J <= up I.

Instance low_mon : monotonic low.
Save.

Definition Low : IU -m> U := mon low.

Instance up_mon : monotonic (o2:=Iord U) up.
Save.

Definition Up : IU -m-> U := mon (o2:=Iord U) up.

Lemma Ieq_incl : forall I J, Ieq I J -> Iincl I J.

Lemma Ieq_incl_sym : forall I J, Ieq I J -> Iincl J I.
Hint Immediate Ieq_incl Ieq_incl_sym.

Lemma lincl_eq_compat : forall I J K L,
     Ieq I J -> Iincl J K -> Ieq K L -> Iincl I L.

Lemma lincl_eq_trans : forall I J K,
     Iincl I J -> Ieq J K -> Iincl I K.

Lemma Ieq_incl_trans : forall I J K,
     Ieq I J -> Iincl J K -> Iincl I K.

Lemma Iincl_antisym : forall I J, Iincl I J -> Iincl J I -> Ieq I J.
Hint Immediate Iincl_antisym.

Lemma Ieq_refl : forall I, Ieq I I.
Hint Resolve Ieq_refl.

Lemma Ieq_sym : forall I J, Ieq I J -> Ieq J I.
Hint Immediate Ieq_sym.

Lemma Ieq_trans : forall I J K, Ieq I J -> Ieq J K -> Ieq I K.

Lemma Isingl_eq : forall x y, Iincl (singl x) (singl y) -> x==y.
Hint Immediate Isingl_eq.

Lemma Iincl_full : forall I, Iincl I full.
Hint Resolve Iincl_full.

Definition Iplus I J := mk_IU (low I + low J) (up I + up J)
                                           (Uplus_le_compat _ _ _ _ (proper I) (proper J)).

Lemma low_Iplus : forall I J, low (Iplus I J)=low I + low J.

Lemma up_Iplus : forall I J, up (Iplus I J)=up I + up J.

Lemma Iplus_in : forall I J x y, Iin x I -> Iin y J -> Iin (x+y) (Iplus I J).

Lemma lplus_in_elim :
forall I J z, low I <= [1-]up J -> Iin z (Iplus I J)
                -> exc (fun x => Iin x I /\
                                                   exc (fun y => Iin y J /\ z==x+y)).

Definition Imult I J := mk_IU (low I * low J) (up I * up J)
                                            (Umult_le_compat _ _ _ _ (proper I) (proper J)).

Lemma low_Imult : forall I J, low (Imult I J) = low I * low J.

Lemma up_Imult : forall I J, up (Imult I J) = up I * up J.

Definition Imultk p I := mk_IU (p * low I) (p * up I) (Umult_le_compat_right p _ _ (proper I)).

Lemma low_Imultk : forall p I, low (Imultk p I) = p * low I.

Lemma up_Imultk : forall p I, up (Imultk p I) = p * up I.

Lemma Imult_in : forall I J x y, Iin x I -> Iin y J -> Iin (x*y) (Imult I J).

Lemma Imultk_in : forall p I x , Iin x I -> Iin (p*x) (Imultk p I).

Definition Ilim : forall I: nat -m> IU, IU.
Defined.

Lemma low_lim : forall (I:nat -m> IU), low (Ilim I) = lub (Low @ I).

Lemma up_lim : forall (I:nat -m> IU), up (Ilim I) = glb (Up @ I).

Lemma lim_Iincl : forall (I:nat -m> IU) n, Iincl (Ilim I) (I n).
Hint Resolve lim_Iincl.

Lemma Iincl_lim : forall J (I:nat -m>IU), (forall n, Iincl J (I n)) -> Iincl J (Ilim I).

Lemma IIim_incl_stable : forall (I J:nat -m> IU), (forall n, Iincl (I n) (J n)) -> Iincl (Ilim I) (Ilim J).
Hint Resolve IIim_incl_stable.

Instance IUcpo : cpo IU := {D0:=full; lub:=Ilim}.
Defined.