Library Cpo
Require Export Setoid.
Require Export Arith.
Require Export Omega.
Open Scope nat_scope.
Record ord : Type := mk_ord
{tord:>Type; Ole:tord->tord->Prop; Ole_refl : forall x :tord, Ole x x;
Ole_trans : forall x y z:tord, Ole x y -> Ole y z -> Ole x z}.
Hint Resolve Ole_refl Ole_trans.
Hint Extern 2 (Ole (o:=?X1) ?X2 ?X3 ) => simpl Ole.
Delimit Scope O_scope with tord.
Infix "<=" := Ole : O_scope.
Open Scope O_scope.
Definition Oeq (O:ord) (x y : O) := x <= y /\ y <= x.
Infix "==" := Oeq (at level 70) : O_scope.
Lemma Ole_refl_eq : forall (O:ord) (x y:O), x=y -> x <= y.
Hint Resolve Ole_refl_eq.
Lemma Ole_antisym : forall (O:ord) (x y:O), x<=y -> y <=x -> x==y.
Hint Immediate Ole_antisym.
Lemma Oeq_refl : forall (O:ord) (x:O), x == x.
Hint Resolve Oeq_refl.
Lemma Oeq_refl_eq : forall (O:ord) (x y:O), x=y -> x == y.
Hint Resolve Oeq_refl_eq.
Lemma Oeq_sym : forall (O:ord) (x y:O), x == y -> y == x.
Lemma Oeq_le : forall (O:ord) (x y:O), x == y -> x <= y.
Lemma Oeq_le_sym : forall (O:ord) (x y:O), x == y -> y <= x.
Hint Resolve Oeq_le.
Hint Immediate Oeq_sym Oeq_le_sym.
Lemma Oeq_trans : forall (O:ord) (x y z:O), x == y -> y == z -> x == z.
Hint Resolve Oeq_trans.
Add Relation tord Oeq
reflexivity proved by Oeq_refl symmetry proved by Oeq_sym
transitivity proved by Oeq_trans as Oeq_Relation.
Add Relation tord Ole
reflexivity proved by Ole_refl
transitivity proved by Ole_trans as Ole_Relation.
Add Morphism Ole with signature Oeq ==> Oeq ==> iff as Ole_eq_compat_iff.
Lemma Ole_eq_compat :
forall (O : ord) (x1 x2 : O),
x1 == x2 -> forall x3 x4 : O, x3 == x4 -> x1 <= x3 -> x2 <= x4.
Lemma Ole_eq_right : forall (O : ord) (x y z: O),
x <= y -> y==z -> x<=z.
Lemma Ole_eq_left : forall (O : ord) (x y z: O),
x == y -> y<=z -> x<=z.
Definition Iord (O:ord):ord.
Definition ford (A:Type) (O:ord) : ord.
Infix "-o>" := ford (right associativity, at level 30) : O_scope .
Lemma ford_le_elim : forall A (O:ord) (f g:A -o> O), f <= g ->forall n, f n <= g n.
Hint Immediate ford_le_elim.
Lemma ford_le_intro : forall A (O:ord) (f g:A-o>O), (forall n, f n <= g n) -> f <= g.
Hint Resolve ford_le_intro.
Lemma ford_eq_elim : forall A (O:ord) (f g:A -o> O), f == g ->forall n, f n == g n.
Hint Immediate ford_eq_elim.
Lemma ford_eq_intro : forall A (O:ord) (f g:A -o> O), (forall n, f n == g n) -> f == g.
Hint Resolve ford_eq_intro.
Hint Extern 2 (Ole (o:=ford ?X1 ?X2) ?X3 ?X4) => intro.
Definition monotonic (O1 O2:ord) (f : O1 -> O2) := forall x y, x <= y -> f x <= f y.
Hint Unfold monotonic.
Definition stable (O1 O2:ord) (f : O1 -> O2) := forall x y, x == y -> f x == f y.
Hint Unfold stable.
Lemma monotonic_stable : forall (O1 O2 : ord) (f:O1 -> O2),
monotonic f -> stable f.
Hint Resolve monotonic_stable.
Record fmono (O1 O2:ord) : Type := mk_fmono
{fmonot :> O1->O2; fmonotonic: monotonic fmonot}.
Hint Resolve fmonotonic.
Definition fmon (O1 O2:ord) : ord.
Infix "-m>" := fmon (at level 30, right associativity) : O_scope.
Lemma fmon_stable : forall (O1 O2:ord) (f:O1-m>O2), stable f.
Hint Resolve fmon_stable.
Lemma fmon_le_elim : forall (O1 O2:ord) (f g:O1 -m> O2), f <= g ->forall n, f n <= g n.
Hint Immediate fmon_le_elim.
Lemma fmon_le_intro : forall (O1 O2:ord) (f g:O1 -m> O2), (forall n, f n <= g n) -> f <= g.
Hint Resolve fmon_le_intro.
Lemma fmon_eq_elim : forall (O1 O2:ord) (f g:O1 -m> O2), f == g ->forall n, f n == g n.
Hint Immediate fmon_eq_elim.
Lemma fmon_eq_intro : forall (O1 O2:ord) (f g:O1 -m> O2), (forall n, f n == g n) -> f == g.
Hint Resolve fmon_eq_intro.
Hint Extern 2 (Ole (o:=fmon ?X1 ?X2) ?X3 ?X4) => intro.
Definition Imon : forall O1 O2, (O1-m>O2) -> Iord O1 -m> Iord O2.
Definition Imon2 : forall O1 O2 O3, (O1-m>O2-m>O3) -> Iord O1 -m> Iord O2 -m> Iord O3.
Definition le_compat2_mon : forall (O1 O2 O3:ord)(f:O1 -> O2 -> O3),
(forall (x y:O1) (z t:O2), x<=y -> z <= t -> f x z <= f y t) -> (O1-m>O2-m>O3).
Definition natO : ord.
Definition fnatO_intro : forall (O:ord) (f:nat -> O), (forall n, f n <= f (S n)) -> natO-m>O.
Lemma fnatO_elim : forall (O:ord) (f:natO -m> O) (n:nat), f n <= f (S n).
Hint Resolve fnatO_elim.
- (mseq_lift_left f n) k = f (n+k)
Definition mseq_lift_left : forall (O:ord) (f:natO -m> O) (n:nat), natO -m> O.
Lemma mseq_lift_left_le_compat : forall (O:ord) (f g:natO -m> O) (n:nat),
f <= g -> mseq_lift_left f n <= mseq_lift_left g n.
Hint Resolve mseq_lift_left_le_compat.
Add Morphism mseq_lift_left with signature Oeq ==> eq ==> Oeq
as mseq_lift_left_eq_compat.
Hint Resolve mseq_lift_left_eq_compat.
- (mseq_lift_left f n) k = f (k+n)
Definition mseq_lift_right : forall (O:ord) (f:natO -m> O) (n:nat), natO -m> O.
Lemma mseq_lift_right_le_compat : forall (O:ord) (f g:natO -m> O) (n:nat),
f <= g -> mseq_lift_right f n <= mseq_lift_right g n.
Hint Resolve mseq_lift_right_le_compat.
Add Morphism mseq_lift_right with signature Oeq ==> eq ==> Oeq
as mseq_lift_right_eq_compat.
Lemma mseq_lift_right_left : forall (O:ord) (f:natO -m> O) n,
mseq_lift_left f n == mseq_lift_right f n.
- (ford_app f x) n = f n x
Definition ford_app : forall (A:Type)(O1 O2:ord)(f:O1 -m> (A -o> O2))(x:A), O1 -m> O2.
Infix "<o>" := ford_app (at level 30, no associativity) : O_scope.
Lemma ford_app_simpl : forall (A:Type)(O1 O2:ord) (f : O1 -m> A -o> O2) (x:A)(y:O1),
(f <o> x) y = f y x.
Lemma ford_app_le_compat : forall (A:Type)(O1 O2:ord) (f g:O1 -m> A -o> O2) (x:A),
f <= g -> f <o> x <= g <o> x.
Hint Resolve ford_app_le_compat.
Add Morphism ford_app with signature Oeq ==> eq ==> Oeq
as ford_app_eq_compat.
- ford_shift f x y == f y x
Definition ford_shift : forall (A:Type)(O1 O2:ord)(f:A -o> (O1 -m> O2)), O1 -m> (A-o>O2).
Lemma ford_shift_le_compat : forall (A:Type)(O1 O2:ord) (f g: A -o> (O1 -m> O2)),
f <= g -> ford_shift f <= ford_shift g.
Hint Resolve ford_shift_le_compat.
Add Morphism ford_shift with signature Oeq ==> Oeq
as ford_shift_eq_compat.
- (fmon_app f x) n = f n x
Definition fmon_app : forall (O1 O2 O3:ord)(f:O1 -m> O2 -m> O3)(x:O2), O1 -m> O3.
Infix "<_>" := fmon_app (at level 35, no associativity) : O_scope.
Lemma fmon_app_simpl : forall (O1 O2 O3:ord)(f:O1 -m> O2 -m> O3)(x:O2)(y:O1),
(f <_> x) y = f y x.
Lemma fmon_app_le_compat : forall (O1 O2 O3:ord) (f g:O1 -m> (O2 -m> O3)) (x y:O2),
f <= g -> x <= y -> f <_> x <= g <_> y.
Hint Resolve fmon_app_le_compat.
Add Morphism fmon_app with signature Oeq ==> Oeq ==> Oeq
as fmon_app_eq_compat.
- fmon_id c = c
Definition fmon_id : forall (O:ord), O -m> O.
Lemma fmon_id_simpl : forall (O:ord) (x:O), fmon_id O x = x.
- (fmon_cte c) n = c
Definition fmon_cte : forall (O1 O2:ord)(c:O2), O1 -m> O2.
Lemma fmon_cte_simpl : forall (O1 O2:ord)(c:O2)(c:O2) (x:O1), fmon_cte O1 c x = c.
Definition mseq_cte : forall O:ord, O -> natO-m>O := fmon_cte natO.
Lemma fmon_cte_le_compat : forall (O1 O2:ord) (c1 c2:O2),
c1 <= c2 -> fmon_cte O1 c1 <= fmon_cte O1 c2.
Add Morphism fmon_cte with signature Oeq ==> Oeq
as fmon_cte_eq_compat.
- (fmon_diag h) n = h n n
Definition fmon_diag : forall (O1 O2:ord)(h:O1 -m> (O1 -m> O2)), O1 -m> O2.
Lemma fmon_diag_le_compat : forall (O1 O2:ord) (f g:O1 -m> (O1 -m> O2)),
f <= g -> fmon_diag f <= fmon_diag g.
Hint Resolve fmon_diag_le_compat.
Lemma fmon_diag_simpl : forall (O1 O2:ord) (f:O1 -m> (O1 -m> O2)) (x:O1),
fmon_diag f x = f x x.
Add Morphism fmon_diag with signature Oeq ==> Oeq
as fmon_diag_eq_compat.
- (fmon_shift h) n m = h m n
Definition fmon_shift : forall (O1 O2 O3:ord)(h:O1 -m> O2 -m> O3), O2 -m> O1 -m> O3.
Lemma fmon_shift_simpl : forall (O1 O2 O3:ord)(h:O1 -m> O2 -m> O3) (x : O2) (y:O1),
fmon_shift h x y = h y x.
Lemma fmon_shift_le_compat : forall (O1 O2 O3:ord) (f g:O1 -m> O2 -m> O3),
f <= g -> fmon_shift f <= fmon_shift g.
Hint Resolve fmon_shift_le_compat.
Add Morphism fmon_shift with signature Oeq ==> Oeq
as fmon_shift_eq_compat.
Lemma fmon_shift_shift_eq : forall (O1 O2 O3:ord) (h : O1 -m> O2 -m> O3),
fmon_shift (fmon_shift h) == h.
- (f@g) x = f (g x)
Definition fmon_comp : forall O1 O2 O3:ord, (O2 -m> O3) -> (O1 -m> O2) -> O1 -m> O3.
Infix "@" := fmon_comp (at level 35) : O_scope.
Lemma fmon_comp_simpl : forall (O1 O2 O3:ord) (f :O2 -m> O3) (g:O1 -m> O2) (x:O1),
(f @ g) x = f (g x).
- (f@2 g) h x = f (g x) (h x)
Definition fmon_comp2 :
forall O1 O2 O3 O4:ord, (O2 -m> O3 -m> O4) -> (O1 -m> O2) -> (O1 -m> O3) -> O1-m>O4.
Infix "@2" := fmon_comp2 (at level 70) : O_scope.
Lemma fmon_comp2_simpl :
forall (O1 O2 O3 O4:ord) (f:O2 -m> O3 -m> O4) (g:O1 -m> O2) (h:O1 -m> O3) (x:O1),
(f @2 g) h x = f (g x) (h x).
Add Morphism fmon_comp with signature Ole ++> Ole ++> Ole as fmon_comp_le_compat_morph.
Lemma fmon_comp_le_compat :
forall (O1 O2 O3:ord) (f1 f2: O2 -m> O3) (g1 g2:O1 -m> O2),
f1 <= f2 -> g1<= g2 -> f1 @ g1 <= f2 @ g2.
Hint Immediate fmon_comp_le_compat.
Add Morphism fmon_comp with signature Oeq ==> Oeq ==> Oeq as fmon_comp_eq_compat.
Hint Immediate fmon_comp_eq_compat.
Lemma fmon_comp_monotonic2 :
forall (O1 O2 O3:ord) (f: O2 -m> O3) (g1 g2:O1 -m> O2),
g1<= g2 -> f @ g1 <= f @ g2.
Hint Resolve fmon_comp_monotonic2.
Lemma fmon_comp_monotonic1 :
forall (O1 O2 O3:ord) (f1 f2: O2 -m> O3) (g:O1 -m> O2),
f1<= f2 -> f1 @ g <= f2 @ g.
Hint Resolve fmon_comp_monotonic1.
Definition fcomp : forall O1 O2 O3:ord, (O2 -m> O3) -m> (O1 -m> O2) -m> (O1 -m> O3).
Lemma fmon_le_compat : forall (O1 O2:ord) (f: O1 -m> O2) (x y:O1), x<=y -> f x <= f y.
Hint Resolve fmon_le_compat.
Lemma fmon_le_compat2 : forall (O1 O2 O3:ord) (f: O1 -m> O2 -m> O3) (x y:O1) (z t:O2),
x<=y -> z <=t -> f x z <= f y t.
Hint Resolve fmon_le_compat2.
Lemma fmon_cte_comp : forall (O1 O2 O3:ord)(c:O3)(f:O1-m>O2),
fmon_cte O2 c @ f == fmon_cte O1 c.
- Constant :
- lub : limit of monotonic sequences
Record cpo : Type := mk_cpo
{tcpo:>ord; D0 : tcpo; lub: (natO -m> tcpo) -> tcpo;
Dbot : forall x:tcpo, D0 <= x;
le_lub : forall (f : natO -m> tcpo) (n:nat), f n <= lub f;
lub_le : forall (f : natO -m> tcpo) (x:tcpo), (forall n, f n <= x) -> lub f <= x}.
Implicit Arguments D0 [c].
Notation "0" := D0 : O_scope.
Hint Resolve Dbot le_lub lub_le.
Add Morphism lub with signature Ole ++> Ole as lub_le_compat_morph.
Hint Resolve lub_le_compat_morph.
Lemma lub_le_compat : forall (D:cpo) (f g:natO -m> D), f <= g -> lub f <= lub g.
Hint Resolve lub_le_compat.
Definition Lub : forall (D:cpo), (natO -m> D) -m> D.
Add Morphism lub with signature Oeq ==> Oeq as lub_eq_compat.
Hint Resolve lub_eq_compat.
Lemma lub_cte : forall (D:cpo) (c:D), lub (fmon_cte natO c) == c.
Hint Resolve lub_cte.
Lemma lub_lift_right : forall (D:cpo) (f:natO -m> D) n, lub f == lub (mseq_lift_right f n).
Hint Resolve lub_lift_right.
Lemma lub_lift_left : forall (D:cpo) (f:natO -m> D) n, lub f == lub (mseq_lift_left f n).
Hint Resolve lub_lift_left.
Lemma lub_le_lift : forall (D:cpo) (f g:natO -m> D) (n:natO),
(forall k, n <= k -> f k <= g k) -> lub f <= lub g.
Lemma lub_eq_lift : forall (D:cpo) (f g:natO -m> D) (n:natO),
(forall k, n <= k -> f k == g k) -> lub f == lub g.
- (lub_fun h) x = lub_n (h n x)
Definition lub_fun : forall (O:ord) (D:cpo) (h : natO -m> O -m> D), O -m> D.
Lemma lub_fun_eq : forall (O:ord) (D:cpo) (h : natO -m> O -m> D) (x:O),
lub_fun h x == lub (h <_> x).
Lemma lub_fun_shift : forall (D:cpo) (h : natO -m> (natO -m> D)),
lub_fun h == Lub D @ (fmon_shift h).
Lemma double_lub_simpl : forall (D:cpo) (h : natO -m> natO -m> D),
lub (Lub D @ h) == lub (fmon_diag h).
Lemma lub_exch_le : forall (D:cpo) (h : natO -m> (natO -m> D)),
lub (Lub D @ h) <= lub (lub_fun h).
Hint Resolve lub_exch_le.
Lemma lub_exch_eq : forall (D:cpo) (h : natO -m> (natO -m> D)),
lub (Lub D @ h) == lub (lub_fun h).
Hint Resolve lub_exch_eq.
Definition fcpo : Type -> cpo -> cpo.
Infix "-O->" := fcpo (right associativity, at level 30) : O_scope.
Lemma fcpo_lub_simpl : forall A (D:cpo) (h:natO-m> A-O->D)(x:A),
(lub h) x = lub(c:=D) (h<o> x).
Lemma lub_comp_le :
forall (D1 D2 : cpo) (f:D1 -m> D2) (h : natO -m> D1), lub (f @ h) <= f (lub h).
Hint Resolve lub_comp_le.
Lemma lub_comp2_le : forall (D1 D2 D3: cpo) (F:D1 -m> D2-m>D3) (f : natO -m> D1) (g: natO -m> D2),
lub ((F @2 f) g) <= F (lub f) (lub g).
Hint Resolve lub_comp2_le.
Definition continuous (D1 D2 : cpo) (f:D1 -m> D2)
:= forall h : natO -m> D1, f (lub h) <= lub (f @ h).
Lemma continuous_eq_compat : forall (D1 D2 : cpo) (f g:D1 -m> D2),
f==g -> continuous f -> continuous g.
Add Morphism continuous with signature Oeq ==> iff as continuous_eq_compat_iff.
Lemma lub_comp_eq :
forall (D1 D2 : cpo) (f:D1 -m> D2) (h : natO -m> D1), continuous f -> f (lub h) == lub (f @ h).
Hint Resolve lub_comp_eq.
- mon0 x == 0
Definition mon0 (O1:ord) (D2 : cpo) : O1 -m> D2 := fmon_cte O1 (0:D2).
Lemma cont0 : forall (D1 D2 : cpo), continuous (mon0 D1 D2).
Implicit Arguments cont0 [].
- double_app f g n m = f m (g n)
Definition double_app (O1 O2 O3 O4: ord) (f:O1 -m> O3 -m> O4) (g:O2 -m> O3)
: O2 -m> (O1 -m> O4) := (fmon_shift f) @ g.
Definition fmon_cpo : forall (O:ord) (D:cpo), cpo.
Infix "-M->" := fmon_cpo (at level 30, right associativity) : O_scope.
Lemma fmon_lub_simpl : forall (O:ord) (D:cpo) (h:natO-m>O-M->D) (x:O),
(lub h) x = lub (h <_> x).
Lemma double_lub_diag : forall (D:cpo) (h:natO-m>natO-M->D),
lub (lub h) == lub (fmon_diag h).
Definition continuous2 (D1 D2 D3: cpo) (F:D1 -m> D2 -m> D3)
:= forall (f : natO-m>D1) (g :natO-m>D2), F (lub f) (lub g) <= lub ((F @2 f) g).
Lemma continuous2_app : forall (D1 D2 D3:cpo) (F : D1-m>D2-m>D3),
continuous2 F -> forall k, continuous (F k).
Lemma continuous2_continuous : forall (D1 D2 D3:cpo) (F : D1-m>D2-M->D3),
continuous2 F -> continuous F.
Lemma continuous2_left : forall (D1 D2 D3:cpo) (F : D1-m>D2-M->D3) (h:natO-m>D1) (x:D2),
continuous2 F -> F (lub h) x <= lub ((F <_> x) @h).
Lemma continuous2_right : forall (D1 D2 D3:cpo) (F : D1-m>D2-M->D3) (x:D1)(h:natO-m>D2),
continuous2 F -> F x (lub h) <= lub (F x @h).
Lemma continuous_continuous2 : forall (D1 D2 D3:cpo) (F : D1-m>D2-M->D3),
(forall k:D1, continuous (F k)) -> continuous F -> continuous2 F.
Hint Resolve continuous2_app continuous2_continuous continuous_continuous2.
Lemma lub_comp2_eq : forall (D1 D2 D3:cpo) (F : D1 -m> D2 -M-> D3),
(forall k:D1, continuous (F k)) -> continuous F ->
forall (f : natO-m>D1) (g :natO-m>D2),
F (lub f) (lub g) == lub ((F@2 f) g).
Lemma continuous_sym : forall (D1 D2:cpo) (F : D1-m> D1 -M-> D2),
(forall x y, F x y == F y x) -> (forall k:D1, continuous (F k)) -> continuous F.
Lemma continuous2_sym : forall (D1 D2:cpo) (F : D1-m>D1-m>D2),
(forall x y, F x y == F y x) -> (forall k, continuous (F k)) -> continuous2 F.
Hint Resolve continuous2_sym.
- continuity is preserved by composition
Lemma continuous_comp : forall (D1 D2 D3:cpo) (f:D2-m>D3)(g:D1-m>D2),
continuous f -> continuous g -> continuous (f@g).
Hint Resolve continuous_comp.
Lemma cont_lub : forall (D1 D2 : cpo) (f:natO -m> (D1 -m> D2)),
(forall n, continuous (f n)) ->
continuous (lub (c:=D1-M->D2) f).
Record fconti (D1 D2:cpo): Type
:= mk_fconti {fcontit : D1 -m> D2; fcontinuous : continuous fcontit}.
Hint Resolve fcontinuous.
Definition fconti_fun (D1 D2 :cpo) (f:fconti D1 D2) : D1-> D2 :=fun x => fcontit f x.
Coercion fconti_fun : fconti >-> Funclass.
Definition fcont_ord : cpo -> cpo -> ord.
Infix "-c>" := fcont_ord (at level 30, right associativity) : O_scope.
Lemma fcont_le_intro : forall (D1 D2:cpo) (f g : D1 -c> D2), (forall x, f x <= g x) -> f <= g.
Lemma fcont_le_elim : forall (D1 D2:cpo) (f g : D1 -c> D2), f <= g -> forall x, f x <= g x.
Lemma fcont_eq_intro : forall (D1 D2:cpo) (f g : D1 -c> D2), (forall x, f x == g x) -> f == g.
Lemma fcont_eq_elim : forall (D1 D2:cpo) (f g : D1 -c> D2), f == g -> forall x, f x == g x.
Lemma fcont_monotonic : forall (D1 D2:cpo) (f : D1 -c> D2) (x y : D1),
x <= y -> f x <= f y.
Hint Resolve fcont_monotonic.
Lemma fcont_stable : forall (D1 D2:cpo) (f : D1 -c> D2) (x y : D1),
x == y -> f x == f y.
Hint Resolve fcont_monotonic.
Definition fcont0 (D1 D2:cpo) : D1 -c> D2 := mk_fconti (cont0 D1 D2).
Definition Fcontit (D1 D2:cpo) : (D1 -c> D2) -m> D1-m> D2.
Definition fcont_lub (D1 D2:cpo) : (natO -m> D1 -c> D2) -> D1 -c> D2.
Definition fcont_cpo : cpo -> cpo -> cpo.
Infix "-C->" := fcont_cpo (at level 30, right associativity) : O_scope.
Definition fcont_app (O:ord) (D1 D2:cpo) (f: O -m> D1-c> D2) (x:D1) : O -m> D2
:= Fcontit D1 D2 @ f <_> x.
Infix "<__>" := fcont_app (at level 70) : O_scope.
Lemma fcont_app_simpl : forall (O:ord) (D1 D2:cpo) (f: O -m> D1-c> D2) (x:D1)(y:O),
(f <__> x) y = f y x.
Definition ford_fcont_shift (A:Type) (D1 D2:cpo) (f: A -o> (D1-c> D2)) : D1 -c> A -O-> D2.
Definition fmon_fcont_shift (O:ord) (D1 D2:cpo) (f: O -m> D1-c> D2) : D1 -c> O -M-> D2.
Lemma fcont_app_continuous :
forall (O:ord) (D1 D2:cpo) (f: O -m> D1-c> D2) (h:natO-m>D1),
f <__> (lub h) <= lub (c:=O-M->D2) (fcontit (fmon_fcont_shift f) @ h).
Lemma fcont_lub_simpl : forall (D1 D2:cpo) (h:natO-m>D1-C->D2)(x:D1),
lub h x = lub (h <__> x).
Definition continuous2_cont_app : forall (D1 D2 D3 :cpo) (f:D1-m> D2 -M-> D3),
(forall k, continuous (f k)) -> D1 -m> (D2 -C-> D3).
Lemma continuous2_cont_app_simpl :
forall (D1 D2 D3 :cpo) (f:D1-m> D2 -M-> D3)(H:forall k, continuous (f k))
(k:D1), continuous2_cont_app H k = mk_fconti (H k).
Lemma continuous2_cont : forall (D1 D2 D3 :cpo) (f:D1-m> D2 -M-> D3),
continuous2 f -> D1 -c> (D2 -C-> D3).
Lemma Fcontit_cont : forall D1 D2, continuous (D1:=D1-C->D2) (D2:=D1-M->D2) (Fcontit D1 D2).
Hint Resolve Fcontit_cont.
Definition fcont_comp : forall (D1 D2 D3:cpo), (D2 -c> D3) -> (D1-c> D2) -> D1 -c> D3.
Infix "@_" := fcont_comp (at level 35) : O_scope.
Lemma fcont_comp_simpl : forall (D1 D2 D3:cpo)(f:D2 -c> D3)(g:D1-c> D2) (x:D1),
(f @_ g) x = f (g x).
Lemma fcontit_comp_simpl : forall (D1 D2 D3:cpo)(f:D2 -c> D3)(g:D1-c> D2) (x:D1),
fcontit (f @_ g) = fcontit f @ fcontit g.
Lemma fcont_comp_le_compat : forall (D1 D2 D3:cpo) (f g : D2 -c> D3) (k l :D1-c> D2),
f <= g -> k <= l -> f @_ k <= g @_ l.
Hint Resolve fcont_comp_le_compat.
Add Morphism fcont_comp with signature Ole ++> Ole ++> Ole as fcont_comp_le_morph.
Add Morphism fcont_comp with signature Oeq ==> Oeq ==> Oeq as fcont_comp_eq_compat.
Definition fcont_Comp (D1 D2 D3:cpo) : (D2 -C-> D3) -m> (D1-C-> D2) -m> D1 -C-> D3
:= le_compat2_mon (fcont_comp_le_compat (D1:=D1) (D2:=D2) (D3:=D3)).
Lemma fcont_Comp_simpl : forall (D1 D2 D3:cpo) (f:D2 -c> D3) (g:D1-c> D2),
fcont_Comp D1 D2 D3 f g = f @_ g.
Lemma fcont_Comp_continuous2 : forall (D1 D2 D3:cpo), continuous2 (fcont_Comp D1 D2 D3).
Definition fcont_COMP (D1 D2 D3:cpo) : (D2 -C-> D3) -c> (D1-C-> D2) -C-> D1 -C-> D3
:= continuous2_cont (fcont_Comp_continuous2 (D1:=D1) (D2:=D2) (D3:=D3)).
Lemma fcont_COMP_simpl : forall (D1 D2 D3:cpo) (f: D2 -C-> D3) (g:D1-C-> D2),
fcont_COMP D1 D2 D3 f g = f @_ g.
Definition fcont2_COMP (D1 D2 D3 D4:cpo) : (D3 -C-> D4) -c> (D1-C-> D2-C->D3) -C-> D1 -C-> D2 -C-> D4 :=
(fcont_COMP D1 (D2-C->D3) (D2 -C-> D4)) @_ (fcont_COMP D2 D3 D4).
Definition fcont2_comp (D1 D2 D3 D4:cpo) (f:D3 -C-> D4)(F:D1-C-> D2-C->D3) := fcont2_COMP D1 D2 D3 D4 f F.
Infix "@@_" := fcont2_comp (at level 35) : O_scope.
Lemma fcont2_comp_simpl : forall (D1 D2 D3 D4:cpo) (f:D3 -C-> D4)(F:D1-C-> D2-C->D3)(x:D1)(y:D2),
(f @@_ F) x y = f (F x y).
Lemma fcont_le_compat2 : forall (D1 D2 D3:cpo) (f : D1-c>D2-C->D3)
(x y : D1) (z t : D2), x <= y -> z <= t -> f x z <= f y t.
Hint Resolve fcont_le_compat2.
Lemma fcont_eq_compat2 : forall (D1 D2 D3:cpo) (f : D1-c>D2-C->D3)
(x y : D1) (z t : D2), x == y -> z == t -> f x z == f y t.
Hint Resolve fcont_eq_compat2.
Lemma fcont_continuous : forall (D1 D2 : cpo) (f:D1 -c> D2)(h:natO-m>D1),
f (lub h) <= lub (fcontit f @ h).
Hint Resolve fcont_continuous.
Lemma fcont_continuous2 : forall (D1 D2 D3:cpo) (f:D1-c>(D2-C->D3)),
continuous2 (Fcontit D2 D3 @ fcontit f).
Hint Resolve fcont_continuous2.
Definition fcont_shift (D1 D2 D3 : cpo) (f:D1-c>D2-C->D3) : D2-c>D1-C->D3.
Lemma fcont_shift_simpl : forall (D1 D2 D3 : cpo) (f:D1-c>D2-C->D3) (x:D2) (y:D1),
fcont_shift f x y = f y x.
Definition fcont_SEQ (D1 D2 D3:cpo) : (D1-C-> D2) -C-> (D2 -C-> D3) -C-> D1 -C-> D3
:= fcont_shift (fcont_COMP D1 D2 D3).
Lemma fcont_SEQ_simpl : forall (D1 D2 D3:cpo) (f: D1 -C-> D2) (g:D2-C-> D3),
fcont_SEQ D1 D2 D3 f g = g @_ f.
Definition fcont_comp2 : forall (D1 D2 D3 D4:cpo),
(D2 -c> D3 -C->D4) -> (D1-c> D2) -> (D1 -c> D3) -> D1-c>D4.
Infix "@2_" := fcont_comp2 (at level 35, right associativity) : O_scope.
Lemma fcont_comp2_simpl : forall (D1 D2 D3 D4:cpo)
(F:D2 -c> D3 -C->D4) (f:D1-c> D2) (g:D1 -c> D3) (x:D1), (F@2_ f) g x = F (f x) (g x).
Add Morphism fcont_comp2 with signature Ole++>Ole ++> Ole ++> Ole
as fcont_comp2_le_morph.
Add Morphism fcont_comp2 with signature Oeq ==> Oeq ==> Oeq ==> Oeq as fcont_comp2_eq_compat.
- Identity function is continuous
Definition Id : forall O:ord, O-m>O.
Definition ID : forall D:cpo, D-c>D.
Lemma Id_simpl : forall O x, Id O x = x.
Lemma ID_simpl : forall D x, ID D x = Id D x.
Definition AP (D1 D2:cpo) : (D1-C->D2)-c>D1-C->D2:=ID (D1-C->D2).
Lemma AP_simpl : forall (D1 D2:cpo) (f : D1-C->D2) (x:D1), AP D1 D2 f x = f x.
Definition fcont_comp3 (D1 D2 D3 D4 D5:cpo)
(F:D2 -c> D3 -C->D4-C->D5)(f:D1-c> D2)(g:D1 -c> D3)(h:D1-c>D4): D1-c>D5
:= (AP D4 D5 @2_ ((F @2_ f) g)) h.
Infix "@3_" := fcont_comp3 (at level 35, right associativity) : O_scope.
Lemma fcont_comp3_simpl : forall (D1 D2 D3 D4 D5:cpo)
(F:D2 -c> D3 -C->D4-C->D5) (f:D1-c> D2) (g:D1 -c> D3) (h:D1-c>D4) (x:D1),
(F@3_ f) g h x = F (f x) (g x) (h x).
Definition Oprod : ord -> ord -> ord.
Definition Fst (O1 O2 : ord) : Oprod O1 O2 -m> O1.
Definition Snd (O1 O2 : ord) : Oprod O1 O2 -m> O2.
Definition Pairr (O1 O2 : ord) : O1 -> O2 -m> Oprod O1 O2.
Definition Pair (O1 O2 : ord) : O1 -m> O2 -m> Oprod O1 O2.
Lemma Fst_simpl : forall (O1 O2 : ord) (p:Oprod O1 O2), Fst O1 O2 p = fst p.
Lemma Snd_simpl : forall (O1 O2 : ord) (p:Oprod O1 O2), Snd O1 O2 p = snd p.
Lemma Pair_simpl : forall (O1 O2 : ord) (x:O1)(y:O2), Pair O1 O2 x y = (x,y).
Definition prod0 (D1 D2:cpo) : Oprod D1 D2 := (0: D1,0: D2).
Definition prod_lub (D1 D2:cpo) (f : natO -m> Oprod D1 D2) := (lub (Fst D1 D2@f), lub (Snd D1 D2@f)).
Definition Dprod : cpo -> cpo -> cpo.
Lemma Dprod_eq_intro : forall (D1 D2:cpo) (p1 p2: Dprod D1 D2),
fst p1 == fst p2 -> snd p1 == snd p2 -> p1 == p2.
Hint Resolve Dprod_eq_intro.
Lemma Dprod_eq_pair : forall (D1 D2:cpo) (x1 y1:D1) (x2 y2:D2),
x1==y1 -> x2==y2 -> ((x1,x2):Dprod D1 D2) == (y1,y2).
Hint Resolve Dprod_eq_pair.
Lemma Dprod_eq_elim_fst : forall (D1 D2:cpo) (p1 p2: Dprod D1 D2),
p1==p2 -> fst p1 == fst p2.
Hint Immediate Dprod_eq_elim_fst.
Lemma Dprod_eq_elim_snd : forall (D1 D2:cpo) (p1 p2: Dprod D1 D2),
p1==p2 -> snd p1 == snd p2.
Hint Immediate Dprod_eq_elim_snd.
Definition FST (D1 D2:cpo) : Dprod D1 D2 -c> D1.
Definition SND (D1 D2:cpo) : Dprod D1 D2 -c> D2.
Lemma Pair_continuous2 : forall (D1 D2:cpo), continuous2 (D3:=Dprod D1 D2) (Pair D1 D2).
Definition PAIR (D1 D2:cpo) : D1 -c> D2 -C-> Dprod D1 D2
:= continuous2_cont (Pair_continuous2 (D1:=D1) (D2:=D2)).
Lemma FST_simpl : forall (D1 D2 :cpo) (p:Dprod D1 D2), FST D1 D2 p = Fst D1 D2 p.
Lemma SND_simpl : forall (D1 D2 :cpo) (p:Dprod D1 D2), SND D1 D2 p = Snd D1 D2 p.
Lemma PAIR_simpl : forall (D1 D2 :cpo) (p1:D1) (p2:D2), PAIR D1 D2 p1 p2 = Pair D1 D2 p1 p2.
Lemma FST_PAIR_simpl : forall (D1 D2 :cpo) (p1:D1) (p2:D2),
FST D1 D2 (PAIR D1 D2 p1 p2) = p1.
Lemma SND_PAIR_simpl : forall (D1 D2 :cpo) (p1:D1) (p2:D2),
SND D1 D2 (PAIR D1 D2 p1 p2) = p2.
Definition Prod_map : forall (D1 D2 D3 D4:cpo)(f:D1-m>D3)(g:D2-m>D4) ,
Dprod D1 D2 -m> Dprod D3 D4.
Lemma Prod_map_simpl : forall (D1 D2 D3 D4:cpo)(f:D1-m>D3)(g:D2-m>D4) (p:Dprod D1 D2),
Prod_map f g p = pair (f (fst p)) (g (snd p)).
Definition PROD_map : forall (D1 D2 D3 D4:cpo)(f:D1-c>D3)(g:D2-c>D4) ,
Dprod D1 D2 -c> Dprod D3 D4.
Lemma PROD_map_simpl : forall (D1 D2 D3 D4:cpo)(f:D1-c>D3)(g:D2-c>D4)(p:Dprod D1 D2),
PROD_map f g p = pair (f (fst p)) (g (snd p)).
Definition curry (D1 D2 D3 : cpo) (f:Dprod D1 D2 -c> D3) : D1 -c> (D2-C->D3) :=
fcont_COMP D1 (D2-C->Dprod D1 D2) (D2-C->D3)
(fcont_COMP D2 (Dprod D1 D2) D3 f) (PAIR D1 D2).
Definition Curry : forall (D1 D2 D3 : cpo), (Dprod D1 D2 -c> D3) -m> D1 -c> (D2-C->D3).
Lemma Curry_simpl : forall (D1 D2 D3 : cpo) (f:Dprod D1 D2 -C-> D3) (x:D1) (y:D2),
Curry D1 D2 D3 f x y = f (x,y).
Definition CURRY : forall (D1 D2 D3 : cpo), (Dprod D1 D2 -C-> D3) -c> D1 -C-> (D2-C->D3).
Lemma CURRY_simpl : forall (D1 D2 D3 : cpo) (f:Dprod D1 D2 -C-> D3),
CURRY D1 D2 D3 f = Curry D1 D2 D3 f.
Definition uncurry (D1 D2 D3 : cpo) (f:D1 -c> (D2-C->D3)) : Dprod D1 D2 -c> D3
:= (f @2_ (FST D1 D2)) (SND D1 D2).
Definition Uncurry : forall (D1 D2 D3 : cpo), (D1 -c> (D2-C->D3)) -m> Dprod D1 D2 -c> D3.
Lemma Uncurry_simpl : forall (D1 D2 D3 : cpo) (f:D1 -c> (D2-C->D3)) (p:Dprod D1 D2),
Uncurry D1 D2 D3 f p = f (fst p) (snd p).
Definition UNCURRY : forall (D1 D2 D3 : cpo), (D1 -C-> (D2-C->D3)) -c> Dprod D1 D2 -C-> D3.
Lemma UNCURRY_simpl : forall (D1 D2 D3 : cpo) (f:D1 -c> (D2-C->D3)),
UNCURRY D1 D2 D3 f = Uncurry D1 D2 D3 f.
Definition Oprodi (I:Type)(O:I->ord) : ord.
Lemma Oprodi_eq_intro : forall (I:Type)(O:I->ord) (p q : Oprodi O), (forall i, p i == q i) -> p==q.
Lemma Oprodi_eq_elim : forall (I:Type)(O:I->ord) (p q : Oprodi O), p==q -> forall i, p i == q i.
Definition Proj (I:Type)(O:I->ord) (i:I) : Oprodi O -m> O i.
Lemma Proj_simpl : forall (I:Type)(O:I->ord) (i:I) (x:Oprodi O),
Proj O i x = x i.
Definition Dprodi (I:Type)(D:I->cpo) : cpo.
Lemma Dprodi_lub_simpl : forall (I:Type)(Di:I->cpo)(h:natO-m>Dprodi Di)(i:I),
lub h i = lub (c:=Di i) (Proj Di i @ h).
Lemma Dprodi_continuous : forall (D:cpo)(I:Type)(Di:I->cpo)
(f:D -m> Dprodi Di), (forall i, continuous (Proj Di i @ f)) ->
continuous f.
Definition Dprodi_lift : forall (I J:Type)(Di:I->cpo)(f:J->I),
Dprodi Di -m> Dprodi (fun j => Di (f j)).
Lemma Dprodi_lift_simpl : forall (I J:Type)(Di:I->cpo)(f:J->I)(p:Dprodi Di),
Dprodi_lift Di f p = fun j => p (f j).
Lemma Dprodi_lift_cont : forall (I J:Type)(Di:I->cpo)(f:J->I),
continuous (Dprodi_lift Di f).
Definition DLIFTi (I J:Type)(Di:I->cpo)(f:J->I) : Dprodi Di -c> Dprodi (fun j => Di (f j))
:= mk_fconti (Dprodi_lift_cont (Di:=Di) f).
Definition Dmapi : forall (I:Type)(Di Dj:I->cpo)(f:forall i, Di i -m> Dj i),
Dprodi Di -m> Dprodi Dj.
Lemma Dmapi_simpl : forall (I:Type)(Di Dj:I->cpo)(f:forall i, Di i -m> Dj i) (p:Dprodi Di) (i:I),
Dmapi f p i = f i (p i).
Lemma DMAPi : forall (I:Type)(Di Dj:I->cpo)(f:forall i, Di i -c> Dj i),
Dprodi Di -c> Dprodi Dj.
Lemma DMAPi_simpl : forall (I:Type)(Di Dj:I->cpo)(f:forall i, Di i -c> Dj i) (p:Dprodi Di) (i:I),
DMAPi f p i = f i (p i).
Lemma Proj_cont : forall (I:Type)(Di:I->cpo) (i:I),
continuous (D1:=Dprodi Di) (D2:=Di i) (Proj Di i).
Definition PROJ (I:Type)(Di:I->cpo) (i:I) : Dprodi Di -c> Di i :=
mk_fconti (Proj_cont (Di:=Di) i).
Lemma PROJ_simpl : forall (I:Type)(Di:I->cpo) (i:I)(d:Dprodi Di),
PROJ Di i d = d i.
Section Product2.
Definition I2 := bool.
Variable DI2 : bool -> cpo.
Definition DP1 := DI2 true.
Definition DP2 := DI2 false.
Definition PI1 : Dprodi DI2 -c> DP1 := PROJ DI2 true.
Definition pi1 (d:Dprodi DI2) := PI1 d.
Definition PI2 : Dprodi DI2 -c> DP2 := PROJ DI2 false.
Definition pi2 (d:Dprodi DI2) := PI2 d.
Definition pair2 (d1:DP1) (d2:DP2) : Dprodi DI2 := bool_rect DI2 d1 d2.
Lemma pair2_le_compat : forall (d1 d'1:DP1) (d2 d'2:DP2), d1 <= d'1 -> d2 <= d'2
-> pair2 d1 d2 <= pair2 d'1 d'2.
Definition Pair2 : DP1 -m> DP2 -m> Dprodi DI2 := le_compat2_mon pair2_le_compat.
Definition PAIR2 : DP1 -c> DP2 -C-> Dprodi DI2.
Lemma PAIR2_simpl : forall (d1:DP1) (d2:DP2), PAIR2 d1 d2 = Pair2 d1 d2.
Lemma Pair2_simpl : forall (d1:DP1) (d2:DP2), Pair2 d1 d2 = pair2 d1 d2.
Lemma pi1_simpl : forall (d1: DP1) (d2:DP2), pi1 (pair2 d1 d2) = d1.
Lemma pi2_simpl : forall (d1: DP1) (d2:DP2), pi2 (pair2 d1 d2) = d2.
Definition DI2_map (f1 : DP1 -c> DP1) (f2:DP2 -c> DP2)
: Dprodi DI2 -c> Dprodi DI2 :=
DMAPi (bool_rect (fun b:bool => DI2 b -c>DI2 b) f1 f2).
Lemma Dl2_map_eq : forall (f1 : DP1 -c> DP1) (f2:DP2 -c> DP2) (d:Dprodi DI2),
DI2_map f1 f2 d == pair2 (f1 (pi1 d)) (f2 (pi2 d)).
End Product2.
Hint Resolve Dl2_map_eq.
Section Product1.
Definition I1 := unit.
Variable D : cpo.
Definition DI1 (_:unit) := D.
Definition PI : Dprodi DI1 -c> D := PROJ DI1 tt.
Definition pi (d:Dprodi DI1) := PI d.
Definition pair1 (d:D) : Dprodi DI1 := unit_rect DI1 d.
Definition pair1_simpl : forall (d:D) (x:unit), pair1 d x = d.
Definition Pair1 : D -m> Dprodi DI1.
Lemma Pair1_simpl : forall (d:D), Pair1 d = pair1 d.
Definition PAIR1 : D -c> Dprodi DI1.
Lemma pi_simpl : forall (d:D), pi (pair1 d) = d.
Definition DI1_map (f : D -c> D)
: Dprodi DI1 -c> Dprodi DI1 :=
DMAPi (fun t:unit => f).
Lemma DI1_map_eq : forall (f : D -c> D) (d:Dprodi DI1),
DI1_map f d == pair1 (f (pi d)).
End Product1.
Hint Resolve DI1_map_eq.
Section Fixpoints.
Variable D: cpo.
Variable f : D -m>D.
Hypothesis fcont : continuous f.
Fixpoint iter_ n : D := match n with O => 0 | S m => f (iter_ m) end.
Lemma iter_incr : forall n, iter_ n <= f (iter_ n).
Hint Resolve iter_incr.
Definition iter : natO -m> D.
Definition fixp : D := lub iter.
Lemma fixp_le : fixp <= f fixp.
Hint Resolve fixp_le.
Lemma fixp_eq : fixp == f fixp.
Lemma fixp_inv : forall g, f g <= g -> fixp <= g.
End Fixpoints.
Hint Resolve fixp_le fixp_eq fixp_inv.
Definition fixp_cte : forall (D:cpo) (d:D), fixp (fmon_cte D d) == d.
Hint Resolve fixp_cte.
Lemma fixp_le_compat : forall (D:cpo) (f g : D-m>D), f<=g -> fixp f <= fixp g.
Hint Resolve fixp_le_compat.
Add Morphism fixp with signature Oeq ==> Oeq as fixp_eq_compat.
Hint Resolve fixp_eq_compat.
Definition Fixp : forall (D:cpo), (D-m>D) -m> D.
Lemma Fixp_simpl : forall (D:cpo) (f:D-m>D), Fixp D f = fixp f.
Definition Iter : forall D:cpo, (D-M->D) -m> (natO -M->D).
Lemma IterS_simpl : forall (D:cpo) f n, Iter D f (S n) = f (Iter D f n).
Lemma iterS_simpl : forall (D:cpo) f n, iter f (S n) = f (iter (D:=D) f n).
Lemma iter_continuous : forall (D:cpo),
forall h : natO -m> (D-M->D), (forall n, continuous (h n)) ->
iter (lub h) <= lub (Iter D @ h).
Hint Resolve iter_continuous.
Lemma iter_continuous_eq : forall (D:cpo),
forall h : natO -m> (D-M->D), (forall n, continuous (h n)) ->
iter (lub h) == lub (Iter D @ h).
Lemma fixp_continuous : forall (D:cpo) (h : natO -m> (D-M->D)),
(forall n, continuous (h n)) -> fixp (lub h) <= lub (Fixp D @ h).
Hint Resolve fixp_continuous.
Lemma fixp_continuous_eq : forall (D:cpo) (h : natO -m> (D -M-> D)),
(forall n, continuous (h n)) -> fixp (lub h) == lub (Fixp D @ h).
Definition FIXP : forall (D:cpo), (D-C->D) -c> D.
Lemma FIXP_simpl : forall (D:cpo) (f:D-c>D), FIXP D f = Fixp D (fcontit f).
Lemma FIXP_le_compat : forall (D:cpo) (f g : D-C->D),
f <= g -> FIXP D f <= FIXP D g.
Hint Resolve FIXP_le_compat.
Lemma FIXP_eq_compat : forall (D:cpo) (f g : D-C->D),
f == g -> FIXP D f == FIXP D g.
Hint Resolve FIXP_eq_compat.
Lemma FIXP_eq : forall (D:cpo) (f:D-c>D), FIXP D f == f (FIXP D f).
Hint Resolve FIXP_eq.
Lemma FIXP_inv : forall (D:cpo) (f:D-c>D)(g : D), f g <= g -> FIXP D f <= g.
Lemma FIXP_comp_com : forall (D:cpo) (f g:D-c>D),
g @_ f <= f @_ g-> FIXP D g <= f (FIXP D g).
Lemma FIXP_comp : forall (D:cpo) (f g:D-c>D),
g @_ f <= f @_ g -> f (FIXP D g) <= FIXP D g -> FIXP D (f @_ g) == FIXP D g.
Fixpoint fcont_compn (D:cpo)(f:D-c>D) (n:nat) {struct n} : D-c>D :=
match n with O => f | S p => fcont_compn f p @_ f end.
Lemma fcont_compn_com : forall (D:cpo)(f:D-c>D) (n:nat),
f @_ (fcont_compn f n) <= fcont_compn f n @_ f.
Lemma FIXP_compn :
forall (D:cpo) (f:D-c>D) (n:nat), FIXP D (fcont_compn f n) == FIXP D f.
Lemma fixp_double : forall (D:cpo) (f:D-c>D), FIXP D (f @_ f) == FIXP D f.
Lemma FIXP_proj : forall (I:Type)(DI: I -> cpo) (F:Dprodi DI -c>Dprodi DI) (i:I) (fi : DI i -c> DI i),
(forall X : Dprodi DI, F X i == fi (X i)) -> FIXP (Dprodi DI) F i == FIXP (DI i) fi.
Definition admissible (D:cpo)(P:D->Type) :=
forall f : natO -m> D, (forall n, P (f n)) -> P (lub f).
Lemma fixp_ind : forall (D:cpo)(F:D -m> D)(P:D->Type),
admissible P -> P 0 -> (forall x, P x -> P (F x)) -> P (fixp F).
Record dcpo : Type := mk_dcpo
{tdcpo:>ord; dlub: (natO -m> tdcpo) -> tdcpo;
le_dlub : forall (f : natO -m> tdcpo) (n:nat), f n <= dlub f;
dlub_le : forall (f : natO -m> tdcpo) (x:tdcpo), (forall n, f n <= x) -> dlub f <= x}.
Hint Resolve le_dlub dlub_le.
Lemma dlub_le_compat : forall (D:dcpo)(f1 f2 : natO -m> D), f1 <= f2 -> dlub f1 <= dlub f2.
Hint Resolve dlub_le_compat.
Lemma dlub_eq_compat : forall (D:dcpo)(f1 f2 : natO -m> D), f1 == f2 -> dlub f1 == dlub f2.
Hint Resolve dlub_eq_compat.
Lemma dlub_lift_right : forall (D:dcpo) (f:natO-m>D) n, dlub f == dlub (mseq_lift_right f n).
Hint Resolve dlub_lift_right.
Lemma dlub_cte : forall (D:dcpo) (c:D), dlub (mseq_cte c) == c.
Definition cpo_dcpo : cpo -> dcpo.
Record setoid : Type := mk_setoid
{tset:>Type; Seq:tset->tset->Prop; Seq_refl : forall x :tset, Seq x x;
Seq_sym : forall x y:tset, Seq x y -> Seq y x;
Seq_trans : forall x y z:tset, Seq x y -> Seq y z -> Seq x z}.
Hint Resolve Seq_refl.
Hint Immediate Seq_sym.
Definition setoid_ord : setoid -> ord.
Definition ord_setoid : ord -> setoid.
Definition type_ord (X:Type) : ord.
Definition type_setoid (X:Type) : setoid.
Definition lub_eq (S:setoid) (f:natO-m>setoid_ord S) := f O.
Lemma le_lub_eq : forall (S:setoid) (f:natO-m>setoid_ord S) (n:nat), f n <= lub_eq f.
Lemma lub_eq_le : forall (S:setoid) (f:natO-m>setoid_ord S)(x:setoid_ord S),
(forall (n:nat), f n <= x) -> lub_eq f <= x.
Hint Resolve le_lub_eq lub_eq_le.
Definition setoid_dcpo : setoid -> dcpo.
Cpo of arrays seen as functions from nat to D with a bound n
Definition lek (O:ord) (k:nat) (f g : nat -> O) := forall n, n < k -> f n <= g n.
Hint Unfold lek.
Lemma lek_refl : forall (O:ord) k (f:nat -> O), lek k f f.
Hint Resolve lek_refl.
Lemma lek_trans : forall (O:ord) (k:nat) (f g h: nat -> O), lek k f g -> lek k g h -> lek k f h.
Definition natk_ord : ord -> nat -> ord.
Definition norm (O:ord) (x:O) (k:nat) (f: natk_ord O k) : natk_ord O k :=
fun n => if le_lt_dec k n then x else f n.
Lemma norm_simpl_lt : forall (O:ord) (x:O) (k:nat) (f: natk_ord O k) (n:nat),
n < k -> norm x f n = f n.
Lemma norm_simpl_le : forall (O:ord) (x:O) (k:nat) (f: natk_ord O k) (n:nat),
(k <= n)%nat -> norm x f n = x.
Definition natk_mon_shift : forall (O1 O2 : ord)(x:O2) (k:nat),
(O1 -m> natk_ord O2 k) -> natk_ord (O1 -m> O2) k.
Lemma natk_mon_shift_simpl
: forall (O1 O2 : ord)(x:O2) (k:nat)(f:O1 -m> natk_ord O2 k) (n:nat) (y:O1),
natk_mon_shift x f n y = norm x (f y) n.
Definition natk_shift_mon : forall (O1 O2 : ord)(k:nat),
(natk_ord (O1 -m> O2) k) -> O1 -m> natk_ord O2 k.
Lemma natk_shift_mon_simpl
: forall (O1 O2 : ord)(k:nat)(f:natk_ord (O1 -m> O2) k) (x:O1)(n:nat),
natk_shift_mon f x n = f n x.
Definition natk0 (D:cpo) (k:nat) : natk_ord D k := fun n : nat => (0:D).
Definition natklub (D:cpo) (k:nat) (h:natO-m>natk_ord D k) : natk_ord D k :=
fun n => lub (natk_mon_shift (0:D) h n).
Lemma natklub_less : forall (D:cpo) (k:nat) (h:natO-m>natk_ord D k) (n:nat),
h n <= natklub h.
Lemma natklub_least : forall (D:cpo) (k:nat) (h:natO-m>natk_ord D k) (p:natk_ord D k),
(forall n:nat, h n <= p) -> natklub h <= p.
Definition Dnatk : forall (D:cpo) (k:nat), cpo.
Notation "k --> D" := (Dnatk D k) (at level 30, right associativity) : O_scope.
Definition natk_shift_cont : forall (D1 D2 : cpo)(k:nat),
(k --> (D1-C->D2)) -> D1 -c> (k --> D2).
Lemma natk_shift_cont_simpl
: forall (D1 D2:cpo)(k:nat)(f:k --> (D1-C->D2)) (n:nat) (x:D1),
natk_shift_cont f x n = f n x.
Lemma natklub_simpl : forall (D:cpo) (k:nat) (h:natO -m> k --> D) (n:nat),
lub h n = lub (natk_mon_shift (0:D) h n).
Library Equations
Require Export Arith.
Require Export Omega.
Definition dec (P:nat->Prop) := forall n, {P n} + {~ P n}.
Record Dec : Type := mk_Dec {prop :> nat -> Prop; is_dec : dec prop}.
Definition PS : Dec -> Dec.
Definition ord (P Q:Dec) := forall n, Q n -> exists m, m < n /\ P m.
Lemma ord_eq_compat : forall (P1 P2 Q1 Q2:Dec),
(forall n, P1 n -> P2 n) -> (forall n, Q2 n -> Q1 n)
-> ord P1 Q1 -> ord P2 Q2.
Lemma ord_not_0 : forall P Q : Dec, ord P Q -> ~Q 0.
Lemma ord_0 : forall P Q : Dec, P 0 -> ~Q 0 -> ord P Q.
- first elt of P then Q
Definition PP : Dec -> Dec -> Dec.
Lemma PP_PS : forall (P:Dec) n, PP P (PS P) n <-> P n.
Lemma PS_PP : forall (P Q:Dec) n, PS (PP P Q) n <-> Q n.
Lemma ord_PS : forall P : Dec, ~ P 0 -> ord (PS P) P.
Lemma ord_PP : forall (P Q: Dec), ~ P 0 -> ord Q (PP P Q).
Lemma ord_PS_PS : forall P Q : Dec, ord P Q -> ~P 0 -> ord (PS P) (PS Q).
Lemma Acc_ord_equiv : forall P Q : Dec, (forall n, P n <-> Q n) -> Acc ord P -> Acc ord Q.
Lemma Acc_ord_0 : forall P : Dec, P 0 -> Acc ord P.
Hint Immediate Acc_ord_0.
Lemma Acc_ord_PP : forall (P Q:Dec), Acc ord Q -> Acc ord (PP P Q).
Lemma Acc_ord_PS : forall (P:Dec), Acc ord (PS P) -> Acc ord P.
Lemma Acc_ord : forall (P:Dec), (exists n,P n) -> Acc ord P.
Fixpoint min_acc (P:Dec) (a:Acc ord P) {struct a} : nat :=
match is_dec P 0 with
left _ => 0 | right H => S (min_acc (Acc_inv a (PS P) (ord_PS P H))) end.
Definition minimize (P:Dec) (e:exists n, P n) : nat := min_acc (Acc_ord P e).
Lemma minimize_P : forall (P:Dec) (e:exists n, P n), P (minimize P e).
Lemma minimize_min : forall (P:Dec) (e:exists n, P n) (m:nat), m < minimize P e -> ~ P m.
Lemma minimize_incr : forall (P Q:Dec)(e:exists n, P n)(f:exists n, Q n),
(forall n, P n -> Q n) -> minimize Q f <= minimize P e.
Require Export Cpo.
Section Terms.
Variables F : Type.
Hypothesis decF : forall f g : F, {f=g}+{~f=g}.
Variable Ar : F -> nat.
Record ind (f:F) : Type := mk_ind {val :> nat ; val_less : val < Ar f}.
Inductive term : Type := X | Ap : F -> (nat -> term) -> term.
Implicit Arguments Ap [].
Inductive le_term : term -> term -> Prop :=
le_X : forall t : term, le_term X t
| le_Ap : forall (f:F) (st1 st2: nat -> term),
(forall (i:nat), (i < Ar f) -> le_term (st1 i) (st2 i))
-> le_term (Ap f st1) (Ap f st2).
Hint Constructors le_term.
Lemma le_term_refl : forall t : term, le_term t t.
Lemma le_term_trans : forall t1 t2 t3 : term, le_term t1 t2 -> le_term t2 t3 -> le_term t1 t3.
Lemma not_le_term_Ap_X : forall f st, ~ le_term (Ap f st) X.
Hint Resolve not_le_term_Ap_X.
Lemma not_le_term_Ap_diff : forall f g st1 st2, ~ f=g -> ~ le_term (Ap f st1) (Ap g st2).
Hint Resolve not_le_term_Ap_diff.
Lemma not_le_term_Ap_st : forall f st1 st2 (n:nat),
n < Ar f -> ~ le_term (st1 n) (st2 n) -> ~ le_term (Ap f st1) (Ap f st2).
Lemma dec_finite : forall P:nat->Prop, dec P -> forall n,
{forall i, i < n -> P i} + {exists i, i < n /\ ~P i}.
Definition le_term_dec : forall t u, {le_term t u}+{~ le_term t u}.
Definition term_ord : ord.
Fixpoint substX (t u:term_ord) {struct t} : term_ord :=
match t with X => u | Ap f st => Ap f (fun i => substX (st i) u) end.
Lemma substX_le : forall (t u:term_ord), t <= substX t u.
Section InterpTerm.
Variable D : cpo.
Variable Finterp : forall f:F, (Ar f --> D) -c> D.
Fixpoint interp_term (t:term) : D -c> D :=
match t with X => ID D
| Ap f st => Finterp f @_
natk_shift_cont (fun i => interp_term (st i))
end.
Lemma interp_term_X : forall x:D, interp_term X x=x.
Lemma interp_term_Ap : forall (f:F) (st : nat -> term) (x:D),
interp_term (Ap f st) x = Finterp f (fun i => interp_term (st i) x).
Definition interp_equation (t:term) : D := FIXP D (interp_term t).
Lemma interp_equa_eq : forall (t:term), interp_equation t == interp_term t (interp_equation t).
End InterpTerm.
Hint Resolve interp_term_X interp_term_Ap interp_equa_eq.
Definition TU := natO -m> term_ord.
Definition TUle (T T' : TU) := forall n, exists m, n<m /\ T n <= T' m.
Lemma TUle_refl : forall T : TU, TUle T T.
Lemma TUle_trans : forall T1 T2 T3 : TU, TUle T1 T2 -> TUle T2 T3 -> TUle T1 T3.
Definition TU_ord : ord.
Definition TU0 : TU_ord := mseq_cte (X:term_ord).
Lemma TU0_less : forall T : TU_ord, TU0 <= T.
- find the smallest m greater than n such that T n <= T' m
Definition le_term_next : forall (T T' : TU_ord) (n:nat), Dec.
Definition TUle_next (T T' : TU_ord) (n:nat) (p: T <= T'):= minimize (le_term_next T T' n) (p n).
Lemma TUle_next_le_term : forall (T T' : TU_ord) (p: T <= T') (n:nat),
T n <= T' (TUle_next n p).
Lemma TUle_next_le : forall (T T' : TU_ord) (p: T <= T') (n:nat),
(n < TUle_next n p)%nat.
Lemma TUle_next_incr : forall (T T' : TU_ord) (p q: T <= T') (n m:nat),
(n <= m)%nat -> (TUle_next n p <= TUle_next m q)%nat.
- lub T 0 = T 0 0,
- lub T i = T i j with T k l <= lub T i for k <= i, l <= i,
- i <= j, lub T i <= lub T (i+1)
- find the apropriate index in T n starting from T 0 k
Fixpoint lub_index (T : natO-m>TU_ord) (k:nat) (n:nat) {struct n} : nat :=
match n with O => k
| S p => TUle_next (lub_index T k p) (fnatO_elim T p)
end.
Lemma lub_index_S : forall (T : natO-m>TU_ord) (k:nat) (n:nat),
lub_index T k (S n) = TUle_next (lub_index T k n) (fnatO_elim T n).
Lemma lub_index_incr : forall (T : natO-m>TU_ord) (k l:nat) (n:nat),
(k <= l) % nat -> (lub_index T k n <= lub_index T l n)%nat.
Hint Resolve lub_index_incr.
Lemma lub_index_le_term_S : forall (T : natO-m>TU_ord) (k:nat) (n:nat),
T n (lub_index T k n) <= T (S n) (lub_index T k (S n)).
Hint Resolve lub_index_le_term_S.
Lemma lub_index_le_term : forall (T : natO-m>TU_ord) (k:nat) (n m:nat),
(n <= m)%nat -> T n (lub_index T k n) <= T m (lub_index T k m).
Hint Resolve lub_index_le_term.
Lemma lub_index_le : forall (T : natO-m>TU_ord) (k:nat) (n:nat),
(n+k <= lub_index T k n)%nat.
Hint Resolve lub_index_le.
Definition TUlub : (natO-m>TU_ord) -> TU_ord.
Lemma TUlub_simpl : forall T n, TUlub T n = T n (lub_index T n n).
Lemma TUlub_le_term : forall (T : natO-m>TU_ord) (k l n : nat),
(k <= n)%nat -> (l<=n)%nat -> T k l <= TUlub T n.
Hint Resolve TUlub_le_term.
Lemma TUlub_less : forall T : natO-m>TU_ord, forall n, T n <= TUlub T.
Lemma TUlub_least : forall (T : natO-m>TU_ord) (T':TU_ord),
(forall n, T n <= T') -> TUlub T <= T'.
Definition DTU : cpo.
Fixpoint maxk (f:nat -> nat) (k:nat) (def:nat) {struct k}: nat :=
match k with O => def | S p => let m:=maxk f p def in
let a:= f p in
if le_lt_dec m a then a else m
end.
Lemma maxk_le : forall (f:nat -> nat) (k:nat) (def:nat),
forall p, p < k -> (f p <= maxk f k def)%nat.
Lemma maxk_le_def : forall (f:nat -> nat) (k:nat) (def:nat),
(def<= maxk f k def)%nat.
Definition TUcte (t:term) : DTU := mseq_cte (O:=term_ord) t.
Definition DTUAp : forall (f:F) (ST: Ar f --> DTU), DTU.
Lemma DTUAp_simpl
: forall (f:F) (ST: Ar f --> DTU)(n:nat), DTUAp ST n = Ap f (fun i => ST i n).
Definition DTUAp_mon : forall (f:F), (Ar f --> DTU) -m> DTU.
Lemma DTUAp_mon_simpl :
forall (f:F) (ST: Ar f --> DTU)(n:nat), DTUAp_mon f ST n = Ap f (fun i => ST i n).
Definition TUAp : forall (f:F), (Ar f --> DTU) -c> DTU.
Fixpoint DTUfix (T:term) (n:nat) {struct n}: term_ord
:= match n with O => X | S p => substX (DTUfix T p) T end.
Definition TUfix (T:term) : DTU.
Lemma TUfix_simplS : forall (T:term) n, TUfix T (S n) = substX (TUfix T n) T.
Lemma TUfix_simpl0 : forall (T:term) , TUfix T O = X.
End Terms.
Library Cpo_flat
Require Export Cpo.
Require Export Arith.
Require Export ZArith.
Section Flat_cpo.
Variable D : Type.
CoInductive Dflat : Type := Eps : Dflat -> Dflat | Val : D -> Dflat.
Lemma DF_inv : forall d, d = match d with Eps x => Eps x | Val d => Val d end.
Hint Resolve DF_inv.
Definition pred d : Dflat := match d with Eps x => x | Val _ => d end.
Fixpoint pred_nth (d:Dflat) (n:nat) {struct n} : Dflat :=
match n with 0 => d
|S m => match d with Eps x => pred_nth x m
| Val _ => d
end
end.
Lemma pred_nth_val : forall x n, pred_nth (Val x) n = Val x.
Hint Resolve pred_nth_val.
Lemma pred_nth_Sn_acc : forall n d, pred_nth d (S n) = pred_nth (pred d) n.
Lemma pred_nth_Sn : forall n d, pred_nth d (S n) = pred (pred_nth d n).
CoInductive DFle : Dflat -> Dflat -> Prop :=
DFleEps : forall x y, DFle x y -> DFle (Eps x) (Eps y)
| DFleEpsVal : forall x d, DFle x (Val d) -> DFle (Eps x) (Val d)
| DFleVal : forall d n y, pred_nth y n = Val d -> DFle (Val d) y.
Hint Constructors DFle.
Lemma DFle_rec : forall R : Dflat -> Dflat -> Prop,
(forall x y, R (Eps x) (Eps y) -> R x y) ->
(forall x d, R (Eps x) (Val d) -> R x (Val d)) ->
(forall d y, R (Val d) y -> exists n, pred_nth y n = Val d)
-> forall x y, R x y -> DFle x y.
Lemma DFle_refl : forall x, DFle x x.
Hint Resolve DFle_refl.
Lemma DFleEps_right : forall x y, DFle x y -> DFle x (Eps y).
Hint Resolve DFleEps_right.
Lemma DFleEps_left : forall x y, DFle x y -> DFle (Eps x) y.
Hint Resolve DFleEps_left.
Lemma DFle_pred_left : forall x y, DFle x y -> DFle (pred x) y.
Lemma DFle_pred_right : forall x y, DFle x y -> DFle x (pred y).
Hint Resolve DFle_pred_left DFle_pred_right.
Lemma DFle_pred : forall x y, DFle x y -> DFle (pred x) (pred y).
Hint Resolve DFle_pred.
Lemma DFle_pred_nth_left : forall n x y, DFle x y -> DFle (pred_nth x n) y.
Lemma DFle_pred_nth_right : forall n x y,
DFle x y -> DFle x (pred_nth y n).
Hint Resolve DFle_pred_nth_left DFle_pred_nth_right.
Lemma DFleVal_eq : forall x y, DFle (Val x) (Val y) -> x=y.
Hint Immediate DFleVal_eq.
Lemma DFleVal_sym : forall x y, DFle (Val x) y -> DFle y (Val x).
Lemma DFle_trans : forall x y z, DFle x y -> DFle y z -> DFle x z.
Definition DF_ord : ord.
Lemma eq_Eps : forall x:DF_ord, x == Eps x.
Hint Resolve eq_Eps.
CoFixpoint DF_bot : DF_ord := Eps DF_bot.
Lemma DF_bot_eq : DF_bot = Eps DF_bot.
Lemma DF_bot_least : forall x:DF_ord, DF_bot <= x.
Lemma DFle_eq : forall x (y:DF_ord), (Val x:DF_ord) <= y -> (Val x:DF_ord) == y.
Lemma DFle_Val_exists_pred :
forall (x:DF_ord) d, (Val d:DF_ord) <= x -> exists k, pred_nth x k = Val d.
Lemma Val_exists_pred_le :
forall (x:DF_ord) d, (exists k, pred_nth x k = Val d) -> (Val d:DF_ord) <= x.
Hint Immediate DFle_Val_exists_pred Val_exists_pred_le.
Lemma Val_exists_pred_eq :
forall (x:DF_ord) d, (exists k, pred_nth x k = Val d) -> (Val d:DF_ord) == x.
Definition isEps (x:DF_ord) := match x with Eps _ => True | _ => False end.
Lemma isEps_Eps : forall x:DF_ord, isEps (Eps x).
Lemma not_isEpsVal : forall d, ~ (isEps (Val d)).
Hint Resolve isEps_Eps not_isEpsVal.
Lemma isEps_dec : forall (x:DF_ord) , {d:D|x=Val d}+{isEps x}.
Lemma fVal : forall (c:natO -m> DF_ord) (n:nat),
{d:D | exists k, k<n /\ c k = Val d} + {forall k, k<n -> isEps (c k)}.
Definition cpred (c:natO -m> DF_ord) : natO-m>DF_ord.
CoFixpoint DF_lubn (c:natO-m> DF_ord) (n:nat) : DF_ord :=
match fVal c n with inleft (exist d _) => Val d
| inright _ => Eps (DF_lubn (cpred c) (S n))
end.
Lemma DF_lubn_inv : forall (c:natO-m> DF_ord) (n:nat), DF_lubn c n =
match fVal c n with inleft (exist d _) => Val d
| inright _ => Eps (DF_lubn (cpred c) (S n))
end.
Lemma chain_Val_eq : forall (c:natO-m> DF_ord) (n n':nat) d d',
(Val d : DF_ord) <= c n -> (Val d' : DF_ord) <= c n' -> d=d'.
Lemma pred_lubn_Val : forall (d:D)(n k p:nat) (c:natO-m> DF_ord),
(n <k+p)%nat -> pred_nth (c n) k = Val d
-> pred_nth (DF_lubn c p) k = Val d.
Lemma pred_lubn_Val_inv : forall (d:D)(k p:nat) (c:natO-m> DF_ord),
pred_nth (DF_lubn c p) k = Val d
-> exists n, (n <k+p)%nat /\ pred_nth (c n) k = Val d.
Definition DF_lub (c:natO-m> DF_ord) := DF_lubn c 1.
Lemma pred_lub_Val : forall (d:D)(n:nat) (c:natO-m> DF_ord),
(Val d:DF_ord) <= (c n) -> (Val d:DF_ord) <= DF_lub c.
Lemma pred_lub_Val_inv : forall (d:D)(c:natO-m> DF_ord),
(Val d:DF_ord) <= DF_lub c -> exists n, (Val d:DF_ord) <= (c n).
Lemma DF_lub_upper : forall c:natO-m> DF_ord, forall n, c n <= DF_lub c.
Lemma DF_lub_least : forall (c:natO-m> DF_ord) a,
(forall n, c n <= a) -> DF_lub c <= a.
Definition DF : cpo.
End Flat_cpo.
Inductive DTriv : Type := DTbot : DTriv.
Definition DT_ord : ord.
Definition DT : cpo.
Lemma DT_eqBot : forall x : DT, x = DTbot.
Library Cpo_streams_type
Require List.
Require Export Cpo.
CoInductive DStr (D:Type) : Type
:= Eps : DStr D -> DStr D | Con : D -> DStr D -> DStr D.
Lemma DS_inv : forall (D:Type) (d:DStr D),
d = match d with Eps x => Eps x | Con a s => Con a s end.
Hint Resolve DS_inv.
- Extraction of a finite list from the n first constructors of a stream
Fixpoint DS_to_list (D:Type)(d:DStr D) (n : nat) {struct n}: List.list D :=
match n with O => List.nil
| S p => match d with Eps d' => DS_to_list d' p
| Con a d' => List.cons a (DS_to_list d' p)
end
end.
Definition pred (D:Type) d : DStr D := match d with Eps x => x | Con _ _ => d end.
Inductive isCon (D:Type) : DStr D -> Prop :=
isConEps : forall x, isCon x -> isCon (Eps x)
| isConCon : forall a s, isCon (Con a s).
Hint Constructors isCon.
Lemma isCon_pred : forall D (x:DStr D), isCon x -> isCon (pred x).
Hint Resolve isCon_pred.
Definition isEps (D:Type) (x:DStr D) := match x with Eps _ => True | _ => False end.
Less general than isCon_pred but the result is a subterm of
the argument (isCon x), used in uncons
Lemma isConEps_inv : forall D (x:DStr D), isCon x -> isEps x -> isCon (pred x).
Lemma isCon_intro : forall D (x:DStr D), isCon (pred x) -> isCon x.
Hint Resolve isCon_intro.
Fixpoint pred_nth D (x:DStr D) (n:nat) {struct n} : DStr D :=
match n with 0 => x
| S m => pred_nth (pred x) m
end.
Lemma pred_nth_switch : forall D k (x:DStr D), pred_nth (pred x) k = pred (pred_nth x k).
Hint Resolve pred_nth_switch .
Lemma pred_nthS : forall D k (x:DStr D), pred_nth x (S k) = pred (pred_nth x k).
Hint Resolve pred_nthS.
Lemma pred_nthCon : forall D a (s:DStr D) n, pred_nth (Con a s) n = (Con a s).
Hint Resolve pred_nthCon.
Definition decomp D (a:D) (s x:DStr D) : Prop := exists k, pred_nth x k = Con a s.
Hint Unfold decomp.
Lemma decomp_isCon : forall D a (s x:DStr D), decomp a s x -> isCon x.
Lemma decompCon : forall D a (s:DStr D), decomp a s (Con a s).
Hint Resolve decompCon.
Lemma decompCon_eq :
forall D a b (s t:DStr D), decomp a s (Con b t) -> Con a s = Con b t.
Hint Immediate decompCon_eq.
Lemma decompEps : forall D a (s x:DStr D), decomp a s x -> decomp a s (Eps x).
Hint Resolve decompEps.
Lemma decompEps_pred : forall D a (s x:DStr D), decomp a s x -> decomp a s (pred x).
Lemma decompEps_pred_sym : forall D a (s x:DStr D), decomp a s (pred x) -> decomp a s x.
Hint Immediate decompEps_pred_sym decompEps_pred.
Lemma decomp_ind : forall D a (s:DStr D) (P : DStr D-> Prop),
(forall x, P x -> decomp a s x -> P (Eps x))
-> P (Con a s) -> forall x, decomp a s x -> P x.
Lemma DStr_match : forall D (x:DStr D), {a:D & {s:DStr D | x = Con a s}}+{isEps x}.
Lemma uncons : forall D (x:DStr D), isCon x ->{a:D & {s:DStr D| decomp a s x}}.
CoInductive DSle (D:Type) : DStr D -> DStr D -> Prop :=
DSleEps : forall x y, DSle x y -> DSle (Eps x) y
| DSleCon : forall a s t y, decomp a t y -> DSle s t -> DSle (Con a s) y.
Hint Constructors DSle.
Lemma DSle_pred_eq : forall D (x y:DStr D), forall n, x=pred_nth y n -> DSle x y.
Lemma DSle_refl : forall D (x:DStr D), DSle x x.
Hint Resolve DSle_refl.
Lemma DSle_pred_right : forall D (x y:DStr D), DSle x y -> DSle x (pred y).
Lemma DSleEps_right_elim : forall D (x y:DStr D), DSle x (Eps y) -> DSle x y.
Lemma DSle_pred_right_elim : forall D (x y:DStr D), DSle x (pred y) -> DSle x y.
Lemma DSle_pred_left : forall D (x y:DStr D), DSle x y -> DSle (pred x) y.
Hint Resolve DSle_pred_left DSle_pred_right.
Lemma DSle_pred : forall D (x y:DStr D), DSle x y -> DSle (pred x) (pred y).
Hint Resolve DSle_pred.
Lemma DSle_pred_left_elim : forall D (x y:DStr D), DSle (pred x) y -> DSle x y.
Lemma DSle_decomp : forall D a (s x y:DStr D),
decomp a s x -> DSle x y -> exists t, decomp a t y /\ DSle s t.
Lemma DSle_trans : forall D (x y z:DStr D), DSle x y -> DSle y z -> DSle x z.
Definition DS_ord (D:Type) : ord := mk_ord (DSle_refl (D:=D)) (DSle_trans (D:=D)).
Lemma DSleEps_right : forall (D:Type) (x y : DS_ord D), x <= y -> x <= Eps y.
Hint Resolve DSleEps_right.
Lemma DSleEps_left : forall D (x y : DS_ord D), x <= y -> (Eps x:DS_ord D) <= y.
Hint Resolve DSleEps_left.
Lemma DSeq_pred : forall D (x:DS_ord D), x == pred x.
Hint Resolve DSeq_pred.
Lemma pred_nth_eq : forall D n (x:DS_ord D), x == pred_nth x n.
Hint Resolve pred_nth_eq.
Lemma DSleCon0 :
forall D a (s t:DS_ord D), s <= t -> (Con a s:DS_ord D) <= Con a t.
Hint Resolve DSleCon0.
Lemma Con_compat :
forall D a (s t:DS_ord D), s == t -> (Con a s:DS_ord D) == Con a t.
Hint Resolve Con_compat.
Lemma DSleCon_hd : forall (D:Type) a b (s t:DS_ord D),
(Con a s:DS_ord D) <= Con b t-> a = b.
Lemma Con_hd_simpl : forall D a b (s t : DS_ord D), (Con a s:DS_ord D) == Con b t-> a = b.
Lemma DSleCon_tl : forall D a b (s t:DS_ord D), (Con a s:DS_ord D) <= Con b t -> (s:DS_ord D) <= t.
Lemma Con_tl_simpl : forall D a b (s t:DS_ord D), (Con a s:DS_ord D) == Con b t -> (s:DS_ord D) == t.
Lemma eqEps : forall D (x:DS_ord D), x == Eps x.
Hint Resolve eqEps.
Lemma decomp_eqCon : forall D a s (x:DS_ord D), decomp a s x -> x == Con a s.
Hint Immediate decomp_eqCon.
Lemma decomp_DSleCon : forall D a s (x:DS_ord D), decomp a s x -> x <= Con a s.
Lemma decomp_DSleCon_sym :
forall D a s (x:DS_ord D), decomp a s x -> (Con a s:DS_ord D)<=x.
Hint Immediate decomp_DSleCon decomp_DSleCon_sym.
Lemma DSleCon_exists_decomp :
forall D (x:DS_ord D) a (s:DS_ord D), (Con a s:DS_ord D) <= x
-> exists b, exists t, decomp b t x /\ a = b /\ s <= t.
Lemma Con_exists_decompDSle :
forall D (x:DS_ord D) a (s:DS_ord D),
(exists t, decomp a t x /\ s <= t) -> (Con a s:DS_ord D) <= x.
Hint Immediate DSleCon_exists_decomp Con_exists_decompDSle.
Lemma DSle_isCon : forall D a (s x : DS_ord D), (Con a s : DS_ord D) <= x -> isCon x.
Lemma DSle_uncons :
forall D (x:DS_ord D) a (s:DS_ord D), (Con a s:DS_ord D) <= x
-> { t : DS_ord D | decomp a t x /\ s <= t}.
Lemma DSle_rec : forall D (R : DStr D -> DStr D -> Prop),
(forall x y, R (Eps x) y -> R x y) ->
(forall a s y, R (Con a s) y -> exists t, decomp a t y /\ R s t)
-> forall x y : DS_ord D, R x y -> x <= y.
Lemma isEps_Eps : forall D (x:DS_ord D), isEps (Eps x).
Lemma not_isEpsCon : forall D a (s:DS_ord D), ~ isEps (Con a s).
Hint Resolve isEps_Eps not_isEpsCon.
Lemma isCon_le : forall D (x y : DS_ord D), isCon x -> x <= y -> isCon y.
Lemma decomp_eq : forall D a (s x:DS_ord D),
x == Con a s -> exists t, decomp a t x /\ s==t.
Lemma DSle_rec_eq : forall D (R : DStr D -> DStr D -> Prop),
(forall x1 x2 y1 y2:DS_ord D, R x1 y1 -> x1==x2 -> y1==y2 -> R x2 y2) ->
(forall a s (y:DS_ord D), R (Con a s) y -> exists t, y==Con a t /\ R s t)
-> forall x y : DS_ord D, R x y -> x <= y.
Lemma DSeq_rec : forall D (R : DStr D -> DStr D -> Prop),
(forall x1 x2 y1 y2:DS_ord D, R x1 y1 -> x1==x2 -> y1==y2 -> R x2 y2) ->
(forall a s (y:DS_ord D), R (Con a s) y -> exists t, y==Con a t /\ R s t)->
(forall a s (x:DS_ord D), R x (Con a s) -> exists t, x==Con a t /\ R t s)
-> forall x y : DS_ord D, R x y -> x == y.
CoFixpoint DS_bot (D:Type) : DS_ord D := Eps (DS_bot D).
Lemma DS_bot_eq (D:Type) : DS_bot D = Eps (DS_bot D).
Lemma DS_bot_least : forall D (x:DS_ord D), DS_bot D <= x.
Hint Resolve DS_bot_least.
Lemma chain_tl : forall D (c:natO-m> DS_ord D), isCon (c O) -> natO -m> DS_ord D.
Lemma chain_uncons :
forall D (c:natO -m> DS_ord D), isCon (c O) ->
{hd:D & {ctl : natO -m> DS_ord D | forall n, c n == Con hd (ctl n)}}.
Lemma fCon : forall D (c:natO -m> DS_ord D) (n:nat),
{hd: D &
{tlc:natO -m> DS_ord D|
exists m, m < n /\ forall k, c (k+m) == Con hd (tlc k)}}
+ {forall k, k<n -> isEps (c k)}.
Definition cpred D (c:natO -m> DS_ord D) : natO -m> DS_ord D.
CoFixpoint DS_lubn D (c:natO -m> DS_ord D) (n:nat) : DS_ord D :=
match fCon c n with
inleft (existS hd (exist tlc _)) => Con hd (DS_lubn tlc 1)
| inright _ => Eps (DS_lubn (cpred c) (S n))
end.
Definition DS_lub (D:Type) (c:natO -m> DS_ord D) := DS_lubn c 1.
Lemma DS_lubn_inv : forall D (c:natO -m> DS_ord D) (n:nat), DS_lubn c n =
match fCon c n with
inleft (existS hd (exist tlc _)) => Con hd (DS_lub tlc)
| inright _ => Eps (DS_lubn (cpred c) (S n))
end.
Lemma DS_lubn_pred_nth : forall D a (s:DS_ord D) n k p (c:natO -m> DS_ord D),
(n<k+p)%nat -> pred_nth (c n) k = Con a s ->
exists d:natO -m> DS_ord D,
DS_lubn c p == Con a (DS_lub d) /\ (s:DS_ord D) <= d n.
Lemma DS_lubn_pred_nth_inv : forall D a (s:DS_ord D) k p (c:natO -m> DS_ord D),
pred_nth (DS_lubn c p) k = Con a s ->
exists tlc :natO -m> DS_ord D, s= DS_lub tlc /\ exists m, forall l, c (l+m) == Con a (tlc l).
Lemma DS_lubCon_inv : forall D a (s:DS_ord D) (c:natO -m> DS_ord D),
(DS_lub c == Con a s) ->
exists tlc :natO -m> DS_ord D,
s==DS_lub tlc /\ exists m, forall l, c (l+m) == Con a (tlc l).
Lemma DS_lubCon : forall D a s n (c:natO -m> DS_ord D),
(Con a s :DS_ord D) <= c n ->
exists d:natO -m> DS_ord D,
DS_lub c == Con a (DS_lub d) /\ (s:DS_ord D) <= d n.
Lemma DS_lub_upper : forall D (c:natO -m> DS_ord D), forall n, c n <= DS_lub c.
Lemma DS_lub_least : forall D (c:natO -m> DS_ord D) x,
(forall n, c n <= x) -> DS_lub c <= x.
Definition DS : Type -> cpo.
Lemma DS_lub_inv : forall D (c:natO -m> DS D), lub c =
match fCon c 1 with
inleft (existS hd (exist tlc _)) => Con hd (lub (c:=DS D) tlc)
| inright _ => Eps (DS_lubn (cpred c) 2)
end.
Definition cons D (a : D) (s: DS D) : DS D := Con a s.
Lemma cons_le_compat :
forall D a b (s t:DS D), a = b -> s <= t -> cons a s <= cons b t.
Hint Resolve cons_le_compat.
Lemma cons_eq_compat :
forall D a b (s t:DS D), a = b -> s == t -> cons a s == cons b t.
Hint Resolve cons_eq_compat.
Add Morphism cons with signature eq ==> Oeq ==> Oeq as cons_eq_compat_morph.
Lemma not_le_consBot: forall D a (s:DS D), ~ cons a s <= 0.
Hint Resolve not_le_consBot.
Lemma DSle_intro_cons :
forall D (x y:DS D), (forall a s, x==cons a s -> cons a s <= y) -> x <= y.
Definition is_cons D (x:DS D) := isCon x.
Lemma is_cons_intro : forall D (a:D) (s:DS D), is_cons (cons a s).
Hint Resolve is_cons_intro.
Lemma is_cons_elim : forall D (x:DS D), is_cons x -> exists a, exists s : DS D, x == cons a s.
Lemma not_is_consBot : forall D, ~ is_cons (0:DS D).
Hint Resolve not_is_consBot.
Lemma is_cons_le_compat : forall D (x y:DS D), x <= y -> is_cons x -> is_cons y.
Lemma is_cons_eq_compat : forall D (x y:DS D), x == y -> is_cons x -> is_cons y.
Lemma DSle_intro_is_cons : forall D (x y:DS D), (is_cons x -> x <= y) -> x <= y.
Lemma DSeq_intro_is_cons : forall D (x y:DS D),
(is_cons x -> x <= y) -> (is_cons y -> y <= x) -> x == y.
Add Morphism is_cons with signature Oeq ==> iff as is_cons_eq_iff.
Add Morphism cons with signature eq ==> Ole ++> Ole as cons_le_morph.
Hint Resolve cons_le_morph.
Section Simple_functions.
Variable D D': Type.
Variable f : D -> DS D -m> DS D'.
CoFixpoint DScase (s:DS D) : DS D':=
match s with Eps x => Eps (DScase x) | Con a l => f a l end.
Lemma DScase_inv :
forall (s:DS D), DScase s = match s with Eps l => Eps (DScase l) | Con a l => f a l end.
Lemma DScaseEps : forall (s:DS D), DScase (Eps s) = Eps (DScase s).
Lemma DScase_cons : forall a (s:DS D), DScase (cons a s) = f a s.
Hint Resolve DScaseEps DScase_cons.
Lemma DScase_decomp : forall a (s x:DS D), decomp a s x -> DScase x == f a s.
Lemma DScase_eq_cons : forall a (s x:DS D), x == cons a s -> DScase x == f a s.
Hint Resolve DScase_eq_cons.
Lemma DScase_bot : DScase 0 <= 0.
Lemma DScase_le_cons : forall a (s x:DS D), cons a s <= x -> f a s <= DScase x.
Lemma DScase_le_compat : forall (s t:DS D), s <= t -> DScase s <= DScase t.
Hint Resolve DScase_le_compat.
Lemma DScase_eq_compat : forall (s t:DS D), s == t -> DScase s == DScase t.
Hint Resolve DScase_eq_compat.
Add Morphism DScase with signature Oeq ==> Oeq as DScase_eq_compat_morph.
Definition DSCase : DS D -m> DS D'.
Lemma DSCase_simpl : forall (s:DS D), DSCase s = DScase s.
Lemma DScase_decomp_elim : forall a (s:DS D') (x:DS D),
decomp a s (DScase x) -> exists b, exists t, x==cons b t /\ f b t == Con a s.
Lemma DScase_eq_cons_elim : forall a (s : DS D') (x:DS D),
DScase x == cons a s -> exists b, exists t, x==cons b t /\ f b t == cons a s.
Lemma DScase_is_cons : forall (x:DS D), is_cons (DScase x) -> is_cons x.
Lemma is_cons_DScase : (forall a (s:DS D), is_cons (f a s)) -> forall (x:DS D), is_cons x -> is_cons (DScase x).
Hypothesis fcont : forall c, continuous (f c).
Lemma DScase_cont : continuous DSCase.
Hint Resolve DScase_cont.
Lemma DScase_cont_eq : forall (c:natO-m>DS D), DScase (lub c) == lub (DSCase @ c).
End Simple_functions.
Hint Resolve DScaseEps DScase_cons DScase_le_compat DScase_eq_compat DScase_bot DScase_cont.
Definition DSCASE_mon : forall D D', (D-O->(DS D -M-> DS D')) -M-> DS D -M-> DS D'.
Lemma DSCASE_mon_simpl : forall D D' f s, DSCASE_mon D D' f s = DScase f s.
Lemma DSCASE_mon_cont : forall D D', continuous (DSCASE_mon D D').
Definition DSCASE_cont : forall D D', (D-O->(DS D -C-> DS D')) -m> (DS D -C-> DS D').
Lemma DSCASE_cont_simpl : forall D D' f s,
DSCASE_cont D D' f s = DScase (fun a => fcontit (f a)) s.
Definition DSCASE : forall D D', (D-O->DS D -C->DS D')-c> DS D -C->DS D'.
Lemma DSCASE_simpl : forall D D' f s, DSCASE D D' f s = DScase (fun a => fcontit (f a)) s.
- Cons is continuous
Definition Cons (D:Type): D -o> (DS D -m> DS D).
Lemma Cons_simpl : forall D (a : D) (s : DS D), Cons a s = cons a s.
Lemma Cons_cont : forall D (a : D), continuous (Cons a).
Hint Resolve Cons_cont.
Definition CONS D (a : D) : DS D -c> DS D := mk_fconti (Cons_cont a).
Lemma CONS_simpl : forall D (a : D) (s : DS D), CONS a s = cons a s.
- first takes a stream and return the stream with only the first element f a s = cons a nil
Definition firstf (D:Type) : D -> DS D -m>DS D:=
fun (d:D) => fmon_cte (DS D) (O2:=DS D) (cons d (0:DS D)).
Lemma firstf_simpl : forall D (a:D) (s:DS D), firstf a s = cons a (0:DS D).
Lemma firstf_cont : forall D (a:D) c, firstf a (lub c) <= lub (firstf a @ c).
Hint Resolve firstf_cont.
Definition First (D:Type) : DS D -m> DS D := DSCase (firstf (D:=D)).
Definition first D (s:DS D) := First D s.
Lemma first_simpl : forall D (s:DS D), first s = DScase (firstf (D:=D)) s.
Lemma first_le_compat : forall D (s t:DS D), s <= t -> first s <= first t.
Hint Resolve first_le_compat.
Lemma first_eq_compat : forall D (s t:DS D), s == t -> first s == first t.
Hint Resolve first_eq_compat.
Lemma first_cons : forall D a (s:DS D), first (cons a s) = cons a (0:DS D).
Lemma first_bot : forall D, first (D:=D) 0 <= 0.
Lemma first_cons_elim : forall D a (s t:DS D),
first t == cons a s -> exists u, t == cons a u /\ s==(0:DS D).
Add Morphism first with signature Oeq ==> Oeq as first_eq_compat_morph.
Add Morphism first with signature Ole ++> Ole as first_le_compat_morph.
Lemma is_cons_first : forall D (s:DS D), is_cons s -> is_cons (first s).
Hint Resolve is_cons_first.
Lemma first_is_cons : forall D (s:DS D), is_cons (first s) -> is_cons s.
Hint Immediate first_is_cons.
Lemma first_cont : forall D, continuous (First D).
Hint Resolve first_cont.
Definition FIRST (D:Type) : DS D -c> DS D.
Lemma FIRST_simpl : forall D s, FIRST D s = first s.
- rem returns the stream without the first element
Definition remf D (d: D) : DS D -m> DS D := fmon_id (DS D).
Lemma remf_simpl : forall D (a:D) s, remf a s = s.
Lemma remf_cont : forall D (a:D) s, remf a (lub s) <= lub (remf a @ s).
Hint Resolve remf_cont.
Definition Rem D : DS D -m> DS D := DSCase (remf (D:=D)).
Definition rem D (s:DS D) := Rem D s.
Lemma rem_simpl : forall D (s:DS D), rem s = DScase (remf (D:=D)) s.
Lemma rem_cons : forall D (a:D) s, rem (cons a s) = s.
Lemma rem_bot : forall D, rem (D:=D) 0 <= 0.
Lemma rem_le_compat : forall D (s t:DS D), s<=t -> rem s <= rem t.
Hint Resolve rem_le_compat.
Lemma rem_eq_compat : forall D (s t:DS D), s==t -> rem s == rem t.
Hint Resolve rem_eq_compat.
Add Morphism rem with signature Oeq ==> Oeq as rem_eq_compat_morph.
Add Morphism rem with signature Ole ++> Ole as rem_le_compat_morph.
Lemma rem_is_cons : forall D (s:DS D), is_cons (rem s) -> is_cons s.
Hint Immediate rem_is_cons.
Lemma rem_cont : forall D, continuous (Rem D).
Hint Resolve rem_cont.
Definition REM (D:Type) : DS D -c> DS D.
Lemma REM_simpl : forall D (s:DS D), REM D s = rem s.
- app s t concatenates the first element of s to t
Definition appf D (t:DS D) (d: D) : DS D -m>DS D := fmon_cte (DS D) (Cons d t).
Lemma appf_simpl D (t:DS D) : forall a s, appf t a s = cons a t.
Definition Appf : forall D, DS D -m> D -o> (DS D -m> DS D).
Lemma Appf_simpl : forall D t, Appf D t = appf t.
Lemma appf_cont D (t:DS D) : forall a c, appf t a (lub c) <= lub (appf t a @ c).
Hint Resolve appf_cont.
Lemma appf_cont_par : forall D, continuous (D2:=D -O-> (DS D -M->DS D)) (Appf D).
Hint Resolve appf_cont_par.
Definition AppI : forall D, DS D -m> DS D -m> DS D.
Lemma AppI_simpl : forall D s t, AppI D t s = DScase (appf t) s.
Definition App (D:Type) := fmon_shift (AppI D).
Lemma App_simpl : forall D s t, App D s t = DScase (appf t) s.
Definition app D s t := App D s t.
Lemma app_simpl : forall D (s t:DS D), app s t = DScase (appf t) s.
Lemma app_cons : forall D a (s t:DS D), app (cons a s) t = cons a t.
Lemma app_bot : forall D (s:DS D), app 0 s <= 0.
Lemma app_mon_left : forall D (s t u : DS D), s <= t -> app s u <= app t u.
Lemma app_cons_elim : forall D a (s t u:DS D), app t u == cons a s ->
exists t', t == cons a t' /\ s == u.
Lemma app_mon_right : forall D (s t u : DS D), t <= u -> app s t <= app s u.
Hint Resolve first_cons first_bot app_cons app_bot
app_mon_left app_mon_right rem_cons rem_bot.
Lemma app_le_compat : forall D (s t u v:DS D), s <= t -> u <= v -> app s u <= app t v.
Hint Immediate app_le_compat.
Lemma app_eq_compat : forall D (s t u v:DS D), s == t -> u == v -> app s u == app t v.
Hint Immediate app_eq_compat.
Add Morphism app with signature Oeq ==> Oeq ==> Oeq as app_eq_compat_morph.
Add Morphism app with signature Ole ++> Ole ++> Ole as app_le_compat_morph.
Lemma is_cons_app : forall D (x y : DS D), is_cons x -> is_cons (app x y).
Hint Resolve is_cons_app.
Lemma app_is_cons : forall D (x y : DS D), is_cons (app x y) -> is_cons x.
Lemma app_cont : forall D, continuous2 (App D).
Hint Resolve app_cont.
Definition APP (D:Type) : DS D -c> DS D -C-> DS D := continuous2_cont (app_cont (D:=D)).
Lemma APP_simpl : forall D (s t : DS D), APP D s t = app s t.
Lemma first_eq_bot : forall D, first (D:=D) 0 == 0.
Lemma rem_eq_bot : forall D, rem (D:=D) 0 == 0.
Lemma app_eq_bot : forall D (s:DS D), app 0 s == 0.
Hint Resolve first_eq_bot rem_eq_bot app_eq_bot.
Lemma DSle_app_bot_right_first : forall D (s:DS D), app s 0 <= first s.
Lemma DSle_first_app_bot_right : forall D (s:DS D), first s <= app s 0.
Lemma app_bot_right_first : forall D (s:DS D), app s 0 == first s.
Lemma DSle_first_app_first : forall D (x y:DS D), first (app x y) <= first x.
Lemma DSle_first_first_app : forall D (x y:DS D), first x <= first (app x y).
Lemma first_app_first : forall D (x y:DS D), first (app x y)==first x.
Hint Resolve app_bot_right_first first_app_first.
Lemma DSle_app_first_rem : forall D (x:DS D), app (first x) (rem x) <= x.
Lemma DSle_app_first_rem_sym : forall D (x:DS D), x <= app (first x) (rem x).
Lemma app_first_rem : forall D (x:DS D), app (first x) (rem x) == x.
Hint Resolve app_first_rem.
Lemma rem_app : forall D (x y:DS D), is_cons x -> rem (app x y) == y.
Hint Resolve rem_app.
Lemma rem_app_le : forall D (x y:DS D), rem (app x y) <= y.
Hint Resolve rem_app_le.
Lemma is_cons_rem_app : forall D (x y : DS D), is_cons x -> is_cons y -> is_cons (rem (app x y)).
Hint Resolve is_cons_rem_app.
Lemma rem_app_is_cons : forall D (x y : DS D), is_cons (rem (app x y)) -> is_cons y.
Lemma first_first_eq : forall D (s:DS D), first (first s) == first s.
Hint Resolve first_first_eq.
Lemma app_app_first : forall D (s t : DS D), app (first s) t == app s t.
Lemma DS_bisimulation : forall D (R: DS D -> DS D -> Prop),
(forall x1 x2 y1 y2, R x1 y1 -> x1==x2 -> y1==y2 -> R x2 y2)
-> (forall (x y:DS D), (is_cons x \/ is_cons y) -> R x y -> first x == first y)
-> (forall (x y:DS D), (is_cons x \/ is_cons y) -> R x y -> R (rem x) (rem y))
-> forall x y, R x y -> x == y.
Lemma DS_bisimulation2 : forall D (R: DS D -> DS D -> Prop),
(forall x1 x2 y1 y2, R x1 y1 -> x1==x2 -> y1==y2 -> R x2 y2)
-> (forall (x y:DS D), (is_cons x \/ is_cons y) -> R x y -> first x == first y)
-> (forall (x y:DS D), (is_cons (rem x) \/ is_cons (rem y)) -> R x y -> first (rem x) == first (rem y))
-> (forall (x y:DS D), (is_cons (rem x) \/ is_cons (rem y)) -> R x y -> R (rem (rem x)) (rem (rem y)))
-> forall x y, R x y -> x == y.
CoInductive infinite (D:Type) (s: DS D) : Prop :=
inf_intro : is_cons s -> infinite (rem s) -> infinite s.
Lemma infinite_le_compat : forall D (s t:DS D), s <= t -> infinite s -> infinite t.
Add Morphism infinite with signature Oeq ==> iff as infinite_morph.
Lemma not_infiniteBot : forall D, ~ infinite (0:DS D).
Hint Resolve not_infiniteBot.
Inductive finite (D:Type) (s:DS D) : Prop :=
fin_bot : s <= 0 -> finite s | fin_cons : finite (rem s) -> finite s.
Lemma finite_mon : forall D (s t:DS D), s <= t -> finite t -> finite s.
Add Morphism finite with signature Oeq ==> iff as finite_morph.
Lemma not_finite_infinite : forall D (s:DS D), finite s -> ~ infinite s.
Section MapStream.
Variable D D': Type.
Variable F : D -> D'.
Definition mapf : (DS D -C-> DS D') -m> D-O-> DS D -C->DS D'.
Lemma mapf_simpl : forall f, mapf f = fun a => CONS (F a) @_ f.
Definition Mapf : (DS D -C-> DS D') -c> D-O-> DS D -C->DS D'.
Lemma Mapf_simpl : forall f, Mapf f = fun a => CONS (F a) @_ f.
Definition MAP : DS D -C-> DS D' := FIXP (DS D-C->DS D') (DSCASE D D' @_ Mapf).
Lemma MAP_eq : MAP == DSCASE D D' (Mapf MAP).
Definition map (s: DS D) := MAP s.
Lemma map_eq : forall s:DS D, map s == DScase (fun a => Cons (F a) @ (fcontit MAP)) s.
Lemma map_bot : map 0 == 0.
Lemma map_eq_cons : forall a s,
map (cons a s) == cons (F a) (map s).
Lemma map_le_compat : forall s t, s <= t -> map s <= map t.
Lemma map_eq_compat : forall s t, s == t -> map s == map t.
Add Morphism map with signature Oeq ==> Oeq as map_eq_compat_morph_local.
Lemma is_cons_map : forall (s:DS D), is_cons s -> is_cons (map s).
Hint Resolve is_cons_map.
Lemma map_is_cons : forall s, is_cons (map s) -> is_cons s.
Hint Immediate map_is_cons.
End MapStream.
Hint Resolve map_bot map_eq_cons map_le_compat map_eq_compat is_cons_map.
Add Morphism map with signature eq ==> Oeq ==> Oeq as map_eq_compat_morph.
Section FilterStream.
Variable D : Type.
Variable P : D -> Prop.
Variable Pdec : forall x, {P x}+{~ P x}.
Definition filterf : (DS D -C-> DS D) -m> D-O-> DS D -C->DS D.
Lemma filterf_simpl : forall f, filterf f = fun a => if Pdec a then CONS a @_ f else f.
Definition Filterf : (DS D -C-> DS D) -c> D-O-> DS D -C->DS D.
Lemma Filterf_simpl : forall f, Filterf f = fun a => if Pdec a then CONS a @_ f else f.
Definition FILTER : DS D -C-> DS D := FIXP (DS D-C->DS D) (DSCASE D D @_ Filterf).
Lemma FILTER_eq : FILTER == DSCASE D D (Filterf FILTER).
Definition filter (s: DS D) := FILTER s.
Lemma filter_bot : filter 0 == 0.
Lemma filter_eq_cons : forall a s,
filter (cons a s) == if Pdec a then cons a (filter s) else filter s.
Lemma filter_le_compat : forall s t, s <= t -> filter s <= filter t.
Lemma filter_eq_compat : forall s t, s == t -> filter s == filter t.
End FilterStream.
Hint Resolve filter_bot filter_eq_cons filter_le_compat filter_eq_compat.
Library Cpo_nat
Require Export Cpo_streams_type.
- Natural numbers are a particular case of streams over the trivial type unit
Lemma unit_eq : forall x : unit, x = tt.
Hint Resolve unit_eq.
Definition DN : cpo := DS unit.
Definition DNS (n : DN) : DN := cons tt n.
Fixpoint nat2DN (n:nat) : DN := match n with 0 => 0 | S p => DNS (nat2DN p) end.
CoFixpoint DNinf : DN := DNS DNinf.
Lemma DNinf_inv : DNinf = DNS DNinf.
Lemma DNleinf : forall n:DN, n <= DNinf.
Hint Resolve DNleinf.
Lemma DNEps_left : forall x y:DN, x == y -> (Eps x :DN) == y.
Lemma DNEps_right : forall x y:DN, x == y -> x == Eps y.
Hint Immediate DNEps_left DNEps_right.
Lemma DNS_le_compat : forall (x y:DN) , x<=y -> DNS x <= DNS y.
Hint Resolve DNS_le_compat.
Lemma DNS_eq_compat : forall (x y:DN) , x==y -> DNS x == DNS y.
Hint Resolve DNS_eq_compat.
Add Morphism DNS with signature Oeq ==> Oeq as DNS_eq_compat_morph.
Lemma DNS_le_simpl : forall x y :DN, DNS x <= DNS y -> x <= y.
Hint Immediate DNS_le_simpl.
Lemma DNS_eq_simpl : forall x y :DN, DNS x == DNS y -> x == y.
Hint Immediate DNS_eq_simpl.
Lemma DNle_rec : forall R : DN -> DN -> Prop,
(forall x1 x2 y1 y2:DN, R x1 y1 -> x1==x2 -> y1==y2 -> R x2 y2) ->
(forall s (y:DN), R (DNS s) y -> exists t, y== DNS t /\ R s t)
-> forall x y : DN , R x y -> x <= y.
Lemma DNeq_rec : forall R : DN -> DN -> Prop,
(forall x1 x2 y1 y2:DN, R x1 y1 -> x1==x2 -> y1==y2 -> R x2 y2) ->
(forall s (y:DN), R (DNS s) y -> exists t, y==DNS t /\ R s t)->
(forall s (x:DN), R x (DNS s) -> exists t, x==DNS t /\ R t s)
-> forall x y : DN , R x y -> x == y.
Lemma DNle_n_Sn : forall x, x <= DNS x.
Hint Resolve DNle_n_Sn.
Lemma DNinf_le_intro : forall x, DNS x <= x -> DNinf <= x.
Hint Immediate DNinf_le_intro.
Lemma is_cons_S : forall n, is_cons n -> n == DNS (rem n).
Lemma infinite_S : forall n : DN, DNS n <= n -> infinite n.
CoFixpoint add (n m : DN) : DN :=
match n with (Eps n') => Eps (add m n')
| (Con _ n') => DNS (add m n')
end.
Lemma add_inv : forall (n m : DN),
add n m = match n with (Eps n') => Eps (add m n')
| (Con _ n') => DNS (add m n')
end.
Lemma add_decomp_elim : forall a (s x y:DN), decomp a s (add x y) ->
exists t, exists u, s = add t u /\
(x==DNS u /\ y==t \/ x==t /\ y == DNS u).
Lemma add_eqCons : forall (s x y:DN), add x y == DNS s ->
exists t, exists u, s == add t u /\
(x==DNS u /\ y==t \/ x == t /\ y == DNS u).
Lemma addS :
forall x' x, DNS x' <= x
-> forall y, (exists s, add x y == DNS s) /\ (exists s, add y x == DNS s).
Lemma addS_sym :
forall x y v:DN, add x y == DNS v -> exists t', add y x == DNS t'.
DNSn x n = S^n x
Fixpoint DNSn (x:DN) (n:nat) {struct n} :DN :=
match n with 0 => x | S p => DNSn (DNS x) p end.
Lemma DNSnS : forall n x, DNSn (DNS x) n = DNS (DNSn x n).
Hint Resolve DNSnS.
Lemma DNSn_mon : forall (n:nat) (x y:DN), x<=y -> DNSn x n <= DNSn y n.
Hint Resolve DNSn_mon.
Lemma DNSn_eq_compat : forall (n:nat) (x y:DN), x==y -> DNSn x n == DNSn y n.
Hint Resolve DNSn_eq_compat.
Condition S^l x <= z & y <= S^l t ensuring x+y <= z+t
Definition compat (x y z t:DN) := exists l:nat, (DNSn x l <= z /\ y <= DNSn t l).
Lemma compatS :
forall x y z t x' y' z' t',
compat x y z t ->
(x==DNS y' /\ y==x' \/ x==x' /\ y==DNS y')
-> (z==DNS t' /\ t==z' \/ z==z' /\ t==DNS t')
-> (compat x' y' z' t' \/ compat x' y' t' z' \/ compat y' x' z' t' \/ compat y' x' t' z').
Lemma compat_addS : forall n m p q v:DN,
(compat n m p q) -> add n m == DNS v -> exists t, add p q == DNS t.
Lemma add_compat :
forall n m p q,
(compat n m p q \/ compat n m q p \/ compat m n p q \/ compat m n q p)
-> add n m <= add p q.
Lemma add_mon : forall n p m q, n<=p -> m <= q -> add n m <= add p q.
Hint Resolve add_mon.
Definition Add : DN -m> DN -m> DN := le_compat2_mon add_mon.
Lemma Add_simpl : forall x y, Add x y = add x y.
Add Morphism add with signature Oeq ==> Oeq ==> Oeq as add_eq_compat.
Lemma add_le_sym : forall n m, add n m <= add m n.
Hint Resolve add_le_sym.
Lemma add_sym : forall n m, add n m == add m n.
Lemma addS_shift : forall n m, add (DNS n) m == add n (DNS m).
Hint Resolve addS_shift.
Lemma addS_simpl : forall n m, add (DNS n) m == DNS (add n m).
Hint Resolve addS_simpl.
Lemma not_le_S_0 : forall n, ~ (DNS n <= 0).
Hint Resolve not_le_S_0.
Lemma add_n_0 : forall n, add 0 n == n.
Lemma add_continuous_right : forall b, continuous (Add b).
Lemma add_continuous2 : continuous2 Add.
Lemma add_continuous : continuous (D2:=DN-M->DN) Add.
Definition LENGTH (D:Type) : DS D -c> DN := MAP (fun x:D=>tt).
Definition length (D:Type) (s:DS D) : DN := LENGTH D s.
Lemma length_simpl : forall (D:Type) (s:DS D), length s = map (fun x:D=>tt) s.
Lemma length_eq_cons : forall D a (s:DS D), length (cons a s) == DNS (length s).
Lemma length_nil : forall D, length (0:DS D) == 0.
Hint Resolve length_eq_cons length_nil.
Lemma length_le_compat : forall D (s t : DS D), s <= t -> length s <= length t.
Hint Resolve length_le_compat.
Lemma length_eq_compat : forall D (s t : DS D), s == t -> length s == length t.
Hint Resolve length_eq_compat.
Add Morphism length with signature Oeq ==> Oeq as length_morph.
Lemma is_cons_length : forall D (s:DS D), is_cons s -> is_cons (length s).
Hint Resolve is_cons_length.
Lemma length_is_cons : forall D (s:DS D), is_cons (length s) -> is_cons s.
Hint Immediate length_is_cons.
Lemma length_rem : forall D (s:DS D), length (rem s) == rem (length s).
Hint Resolve length_rem.
Lemma infinite_length : forall D (s:DS D), infinite s -> infinite (length s).
Hint Resolve infinite_length.
Lemma length_infinite : forall D (s:DS D), infinite (length s) -> infinite s.
Hint Immediate length_infinite.
Library Systems
Require Export Cpo_streams_type.
Definition of a multiple node :
- index for inputs with associated types
- index for outputs with associated types
- continuous function on corresponding streams
Definition DS_fam (I:Type)(SI:I -> Type) (i:I) := DS (SI i).
Definition DS_prod (I:Type)(SI:I -> Type) := Dprodi (DS_fam SI).
- A node is a continuous function from inpits to outputs
Definition node_fun (I O : Type) (SI : I -> Type) (SO : O -> Type) :cpo
:= DS_prod SI -C-> DS_prod SO.
- node with a single output
Definition snode_fun (I : Type) (SI : I -> Type) (SO : Type) : cpo := DS_prod SI -C-> DS SO.
- Each link is either an input link or is associated to the output of a simple node, each input of that node is associated to a link with the apropriate type
Definition inlSL (LI LO:Type) (SL:(LI+LO)->Type) (i:LI) := SL (inl LO i).
Definition inrSL (LI LO:Type) (SL:(LI+LO)->Type) (o:LO) := SL (inr LI o).
A system associates a continuous functions to a set of typed output links
Definition system (LI LO:Type) (SL:LI+LO->Type)
:= Dprodi (fun (o:LO) => DS_prod SL -C-> DS (inrSL SL o)).
Each system defines a new node with inputs for the inputs of the system
Equations are a continuous functional on links
Definition eqn_of_system : forall (LI LO:Type) (SL:LI+LO->Type),
system SL -> DS_prod (inlSL SL) -> DS_prod SL -m> DS_prod SL.
Lemma eqn_of_system_simpl : forall (LI LO:Type) (SL:LI+LO->Type)(s:system SL)
(init : DS_prod (inlSL SL)) (X:DS_prod SL),
eqn_of_system s init X =
fun l : LI+LO =>
match l return (DS (SL l)) with
inl i => init i
| inr o => s o X
end.
Lemma eqn_of_system_cont : forall (LI LO:Type) (SL:LI+LO->Type)(s:system SL)
(init : DS_prod (inlSL SL)), continuous (eqn_of_system s init).
Hint Resolve eqn_of_system_cont.
Definition EQN_of_system : forall (LI LO:Type) (SL:LI+LO->Type),
system SL -> DS_prod (inlSL SL) -> DS_prod SL -c> DS_prod SL.
Lemma EQN_of_system_simpl : forall (LI LO:Type) (SL:LI+LO->Type)(s:system SL)
(init : DS_prod (inlSL SL)) (X:DS_prod SL),
EQN_of_system s init X = eqn_of_system s init X.
The equations are monotonic with respect to the inputs and the system
Lemma EQN_of_system_mon : forall (LI LO:Type) (SL:LI+LO->Type)
(s1 s2 : system SL) (init1 init2 : DS_prod (inlSL SL)),
s1 <= s2 -> init1 <= init2 -> EQN_of_system s1 init1 <= EQN_of_system s2 init2.
Definition Eqn_of_system : forall (LI LO:Type) (SL:LI+LO->Type),
(system SL) -m> DS_prod (inlSL SL) -M-> DS_prod SL -C-> DS_prod SL.
Lemma Eqn_of_system_simpl : forall (LI LO:Type) (SL:LI+LO->Type)(s:system SL)
(init:DS_prod (inlSL SL)), Eqn_of_system SL s init = EQN_of_system s init.
The equations are continuous with respect to the inputs
Lemma Eqn_of_system_cont : forall (LI LO:Type) (SL:LI+LO->Type),
continuous2 (Eqn_of_system SL).
Hint Resolve Eqn_of_system_cont.
Lemma Eqn_of_system_cont2 : forall (LI LO:Type) (SL:LI+LO->Type)(s:system SL),
continuous (Eqn_of_system SL s).
Lemma Eqn_of_system_cont1 : forall (LI LO:Type) (SL:LI+LO->Type),
continuous (Eqn_of_system SL).
Definition EQN_of_SYSTEM (LI LO:Type) (SL:LI+LO->Type)
: system SL -c> DS_prod (inlSL SL) -C-> DS_prod SL -C-> DS_prod SL
:= continuous2_cont (Eqn_of_system_cont (SL:=SL)).
The solution is defined as the smallest fixpoint of the equations
it is a monotonic function of the inputs
Definition sol_of_system (LI LO:Type) (SL:LI+LO->Type)
: system SL -c> DS_prod (inlSL SL) -C-> DS_prod SL := FIXP (DS_prod SL) @@_ EQN_of_SYSTEM SL.
Lemma sol_of_system_simpl :
forall (LI LO:Type) (SL:LI+LO->Type) (s:system SL) (init:DS_prod (inlSL SL)),
sol_of_system SL s init = FIXP (DS_prod SL) (EQN_of_system s init).
Lemma sol_of_system_eq : forall (LI LO:Type) (SL:LI+LO->Type) (s:system SL) (init:DS_prod (inlSL SL)),
sol_of_system SL s init == eqn_of_system s init (sol_of_system SL s init).
We can choose an arbitrary set of outputs
Definition node_of_system (O:Type)(LI LO:Type) (SL:LI+LO->Type)(indO : O -> LO) :
system SL -C-> node_fun (fun i : LI => SL (inl LO i)) (fun o : O => SL (inr LI (indO o)))
:= DLIFTi (DS_fam SL) (fun o => inr LI (indO o)) @@_ (sol_of_system SL).
Library Example
Require Export Systems.
Require Export Cpo_nat.
Definition D := nat.
- f U V = app U (app V (f (rem U) (rem V)))
Definition Funf : (DS D -C-> DS D -C-> DS D) -c> (DS D) -C-> (DS D) -C-> DS D.
Lemma Funf_eq : forall (f : DS D -C-> DS D -C-> DS D) (U V : DS D),
Funf f U V == app U (app V (f (rem U) (rem V))).
Definition f : DS D -C-> DS D -C-> DS D := FIXP _ Funf.
Lemma f_eq : forall (p1 p2:DS D),
f p1 p2 == app p1 (app p2 (f (rem p1) (rem p2))).
Hint Resolve f_eq.
Lemma first_f_eq : forall (p1 p2:DS D), first (f p1 p2) == first p1.
Hint Resolve first_f_eq.
Lemma rem_f_eq : forall (p1 p2:DS D),
is_cons p1 -> rem (f p1 p2) == app p2 (f (rem p1) (rem p2)).
Hint Resolve rem_f_eq.
Lemma is_cons_f: forall (p1 p2:DS D), is_cons p1 -> is_cons (f p1 p2).
Lemma is_cons_rem_f: forall (p1 p2:DS D), is_cons p1 -> is_cons p2 -> is_cons (rem (f p1 p2)).
Lemma f_is_cons : forall (p1 p2:DS D), is_cons (f p1 p2) -> is_cons p1.
Lemma rem_f_is_cons : forall (p1 p2:DS D), is_cons (rem (f p1 p2)) -> is_cons p2.
- g1 U = app U g1 (rem (rem U)))
Definition Fung1 : (DS D -C-> DS D) -c> DS D -C-> DS D.
Lemma Fung1_eq : forall (g1 : DS D -c> DS D) (p:DS D),
Fung1 g1 p == app p (g1 (rem (rem p))).
Lemma Fung1_pair_eq : forall (g1 : DS D -C-> DS D) (p:DS D),
Fung1 g1 p == app p (g1 (rem (rem p))).
Definition g1 : DS D -c> DS D := FIXP (DS D -C-> DS D) Fung1.
Lemma g1_eq : forall (p:DS D),
g1 p == app p (g1 (rem (rem p))).
Hint Resolve g1_eq.
Lemma first_g1_eq : forall (p:DS D), first (g1 p) == first p.
Lemma rem_g1_eq : forall (p:DS D), is_cons p -> rem (g1 p) == g1 (rem (rem p)).
Lemma is_cons_g1 : forall (p:DS D), is_cons p -> is_cons (g1 p).
Hint Resolve is_cons_g1.
Lemma g1_is_cons : forall (p:DS D), is_cons (g1 p) -> is_cons p.
- g2 U = app (rem U) (g2 (rem (rem U)))
Definition Fung2 : (DS D -C-> DS D) -c> DS D -C-> DS D.
Lemma Fung2_eq : forall (g2 : DS D -c> DS D) (p:DS D),
Fung2 g2 p == app (rem p) (g2 (rem (rem p))).
Definition g2 : DS D -c> DS D := FIXP (DS D -C-> DS D) Fung2.
Lemma g2_eq : forall (p:DS D), g2 p == app (rem p) (g2 (rem (rem p))).
Hint Resolve g2_eq.
Lemma first_g2_eq : forall (p:DS D), first (g2 p) == first (rem p).
Lemma rem_g2_eq : forall (p:DS D), is_cons (rem p) -> rem (g2 p) == g2 (rem (rem p)).
Lemma is_cons_g2 : forall (p:DS D), is_cons (rem p) -> is_cons (g2 p).
Hint Resolve is_cons_g2.
Lemma g2_is_cons : forall (p:DS D), is_cons (g2 p) -> is_cons (rem p).
- h n s = cons n s
Definition h (n:nat) : DS D -c> DS D := CONS n.
Inductive LI : Type := .
Inductive LO : Type := X | Y | Z | T1 | T2.
Definition SL : LI+LO -> Type := fun x => D.
- X = f Y Z; Y = h 0 T1; Z = h 1 T2; T1 = g1 X; T2 = g2 X
Definition sys : system SL :=
fun x : LO => match x with
X => (f @2_ (PROJ (DS_fam SL) (inr LI Y))) (PROJ (DS_fam SL) (inr LI Z))
| Y => h O @_ PROJ (DS_fam SL) (inr LI T1)
| Z => h 1 @_ PROJ (DS_fam SL) (inr LI T2)
| T1 => g1 @_ PROJ (DS_fam SL) (inr LI X)
| T2 => g2 @_ PROJ (DS_fam SL) (inr LI X)
end.
- The system has no inputs
Definition init : Dprodi (DS_fam (inlSL SL)) := fun i : LI => match i with end.
- Equation associated to the system
Definition EQN_sys : Dprodi (DS_fam SL) -c> Dprodi (DS_fam SL)
:= EQN_of_system sys init.
- The result is given on the X node
Definition result : DS D := sol_of_system SL sys init (inr LI X).
- X == f (h O (g1 X)) (h 1 (g2 X))
Definition FunX : DS D -c> DS D := (f @2_ (h O @_ g1)) (h 1 @_ g2).
Lemma FunX_simpl : forall (s:DS D), FunX s = f (h O (g1 s)) (h 1 (g2 s)).
Lemma eqn_sys_FunX :
forall p : Dprodi (DS_fam SL),
fcont_compn EQN_sys 2 p (inr LI X) == FunX (p (inr LI X)).
Lemma result_eq : result == FIXP (DS D) FunX.
Lemma lem1 : forall s:DS D, FunX s == cons O (cons 1 (f (g1 s) (g2 s))).
Lemma R_is_cons : forall s t, t == f (g1 s) (g2 s) -> is_cons s -> is_cons t.
Lemma R_is_cons_rem : forall s t, t == f (g1 s) (g2 s)
-> is_cons (rem s) -> is_cons (rem t).
Lemma R_is_cons_inv : forall s t, t == f (g1 s) (g2 s) -> is_cons t -> is_cons s.
Lemma R_is_cons_rem_inv : forall s t, t == f (g1 s) (g2 s)
-> is_cons (rem t) -> is_cons (rem s).
Lemma lem2 : forall s:DS D, s == f (g1 s) (g2 s).
- result is an infinite stream alternating 0 and 1
Lemma result_alt : result == cons O (cons 1 result).
Lemma result_inf : infinite result.
Library Sieve
Require Export Systems.
Require Export Cpo_nat.
Require Export Arith.
Require Export Euclid.
- sift (cons a s) == cons a (sift (filter (div a) s))
Definition div (n m:nat) := exists q, m = q * n.
Lemma div0 : forall q n r, r=q * n -> r < n -> r = O.
Lemma div0bis : forall q q' n r, q * n = q' * n + r -> r < n -> r = O.
Definition div_dec : forall n m, {div n m}+ {~ div n m}.
- o = sift i is recursively defined by: o = app i Y ; Y = sift X; X = fdiv i
Definition LI : Type := unit.
Definition i := tt.
Inductive LO : Type := X | Y | o.
Definition D := nat.
Definition SL : LI+LO -> Type := fun i => D.
Definition fdiv : DS D -c> DS D := DSCASE D D (fun a => FILTER (div a) (div_dec a)).
Lemma fdiv_cons : forall a s, fdiv (cons a s) = filter (div a) (div_dec a) s.
Definition Funsift : (DS D -C-> DS D) -m> system SL.
Lemma Funsift_simpl : forall fs x, Funsift fs x = match x with X => fdiv @_ PROJ (DS_fam SL) (inl LO i)
| Y => fs @_ PROJ (DS_fam SL) (inr LI X)
| o => (APP D @2_ PROJ (DS_fam SL) (inl LO i))
(PROJ (DS_fam SL) (inr LI Y))
end.
Definition FunSift : (DS D -C-> DS D) -c> system SL.
Lemma FunSift_simpl : forall fs x, FunSift fs x = match x with X => fdiv @_ PROJ (DS_fam SL) (inl LO i)
| Y => fs @_ PROJ (DS_fam SL) (inr LI X)
| o => (APP D @2_ PROJ (DS_fam SL) (inl LO i))
(PROJ (DS_fam SL) (inr LI Y))
end.
-
focusrestrict to the input and output observed
Definition focus : (DS_prod (inlSL SL) -C-> DS_prod SL) -c> DS D -C-> DS D :=
PROJ (DS_fam SL) (inr LI o) @@_ fcont_SEQ (DS D) (DS_prod (inlSL SL)) (DS_prod SL) (PAIR1 (DS D)).
Lemma focus_simpl : forall (f : DS_prod (inlSL SL) -C-> DS_prod SL) (s:DS D),
focus f s = f (pair1 s) (inr LI o).
Definition sift : DS D -C-> DS D :=
FIXP (DS D -C->DS D) (focus @_ (sol_of_system SL @_ FunSift)).
Lemma sift_eq : sift == focus (sol_of_system SL (FunSift sift)).
Hint Resolve sift_eq.
Lemma sift_le_compat : forall x y, x <= y -> sift x <= sift y.
Hint Resolve sift_le_compat.
Lemma sift_eq_compat : forall x y, x == y -> sift x == sift y.
Hint Resolve sift_eq_compat.
Lemma sol_of_system_i : forall s : DS D, sol_of_system SL (FunSift sift) (pair1 s) (inl LO i) == s.
Lemma sol_of_system_X : forall s : DS D,
sol_of_system SL (FunSift sift) (pair1 s) (inr LI X) == fdiv s.
Lemma sol_of_system_Y : forall s : DS D,
sol_of_system SL (FunSift sift) (pair1 s) (inr LI Y) == sift (fdiv s).
Lemma sol_of_system_o : forall s : DS D,
sol_of_system SL (FunSift sift) (pair1 s) (inr LI o) == app s (sift (fdiv s)).
Lemma sift_prop : forall a s, sift (cons a s) == cons a (sift (filter (div a) (div_dec a) s)).
| 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 | _ | (870 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 | _ | (550 entries) |
| Constructor 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 | _ | (27 entries) |
| Inductive 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 | _ | (20 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 | _ | (265 entries) |
| 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 | _ | (8 entries) |
This page has been generated by coqdoc