Skip to content

Instantly share code, notes, and snippets.

@gaxiiiiiiiiiiii

gaxiiiiiiiiiiii/ScottModel.v

Last active November 21, 2023 12:56
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save gaxiiiiiiiiiiii/e0511b71394775539c56b50935276544 to your computer and use it in GitHub Desktop.
Save gaxiiiiiiiiiiii/e0511b71394775539c56b50935276544 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
ScottModel.v
From UniMath Require Export MoreFoundations.All.
From UniMath Require Export OrderTheory.Posets.
From UniMath Require Export OrderTheory.DCPOs.
From DomainTheory Require Export Pataraia.
From mathcomp Require Export ssreflect.
Open Scope dcpo.
Open Scope subtype.
Open Scope logic.
Definition dcppo_funspace (D E : dcppo) : dcppo.
Proof.
split with (dcpo_funspace D E).
split with (dcpo_funspace D E).
use tpair.
- split with (fun _ => ⊥_{E}).
use make_is_scott_continuous.
+ move => f g H.
apply refl_dcpo.
+ move => H.
apply antisymm_dcpo.
* apply is_min_bottom_dcppo.
* apply dcpo_lub_is_least => /= i.
cbn.
apply refl_dcpo.
- simpl.
move => f g.
apply is_min_bottom_dcppo.
Defined.
Definition ep_pair (D E : dcppo) :=
∑ (f : dcppo_funspace D E) (g : dcppo_funspace E D),(
(∏ d, (pr1 g) (pr1 f d) = d) ×
(∏ e, (pr1 f) (pr1 g e) ≤ e)
)%type.
Definition embd {X Y}(ep : ep_pair X Y) : X -> Y := pr11 ep.
Definition proj {X Y}(ep : ep_pair X Y) : Y -> X := pr112 ep.
Lemma embd_is_injective {X Y}(ep : ep_pair X Y) :
∏ x y, embd ep x = embd ep y -> x = y.
Proof.
move => x y H.
rewrite <- (pr122 ep x).
rewrite <- (pr122 ep y).
unfold embd in H.
rewrite H; auto.
Qed.
Lemma embd_proj_le {X Y}(ep : ep_pair X Y) :
∏ x y, (embd ep x ≤ y <-> x ≤ proj ep y).
Proof.
move => x y; split => H.
- move : (pr1 (pr212 ep) _ _ H).
rewrite (pr122 ep x).
apply.
- eapply trans_dcpo.
* apply ((pr121 ep) _ _ H).
* apply ((pr222 ep) y).
Qed.
Lemma proj_embd_le {X Y}(ep : ep_pair X Y) :
∏ x y, (x ≤ embd ep y -> proj ep x ≤ y).
Proof.
set f := pr11 ep.
set g := pr112 ep.
set f_mono := pr121 ep.
set g_mono := (pr1 (pr212 ep)).
simpl in *.
move => y x H.
move : (g_mono _ _ H) => H0.
eapply trans_dcpo; eauto.
rewrite (pr122 ep x).
apply refl_dcpo.
Qed.
Lemma embd_proj {X Y}(f g : ep_pair X Y) :
pr1 f ≤ pr1 g <-> pr12 g ≤ pr12 f.
Proof.
simpl.
move : (pr122 g).
move : (pr222 g).
change (pr11 f) with (embd f) in *.
change (pr11 g) with (embd g) in *.
change (pr112 f) with (proj f) in *.
change (pr112 g) with (proj g) in *.
move => Hg2 Hg1 ; split => H.
- move => y.
move : (H (proj g y)) => Hg.
move : (Hg2 y) => Hg2y.
apply embd_proj_le.
eapply trans_dcpo; eauto.
- move => x.
move : (H (embd g x)).
rewrite (Hg1 x) => H0.
apply embd_proj_le; auto.
Qed.
Lemma compose_is_scott_continuous {X Y Z: dcpo} (f : X -> Y) (g : Y -> Z) :
is_scott_continuous (pr2 X) (pr2 Y) f ->
is_scott_continuous (pr2 Y) (pr2 Z) g ->
is_scott_continuous (pr2 X) (pr2 Z) (g ∘ f).
Proof.
move => [Hf1 Hf2] [Hg1 Hg2].
split.
- move => x y H.
apply Hg1.
apply Hf1.
auto.
- move => I D HD x Hx.
move : (Hf2 I D HD x Hx) => [H1' H2'].
refine (Hg2 I (f ∘ D) _ (f x) _).
* induction HD as [HI HD].
split; auto.
move => i j.
move : (HD i j).
unfold ishinh; apply => [[k [Hk1 Hk2]]].
move => P; apply; clear P.
exists k; split; apply Hf1; auto.
* induction Hx as [H1 H2].
split.
+ move => i.
apply Hf1.
apply (H1 i).
+ move => y Hy.
eapply (H2' y); auto.
Qed.
Lemma compose_dcpo_funspace {X Y Z}(f : dcpo_funspace X Y)(g : dcpo_funspace Y Z) :
dcpo_funspace X Z.
Proof.
split with (pr1 g ∘ pr1 f).
induction f as [f Hf].
induction g as [g Hg].
apply compose_is_scott_continuous; auto.
Defined.
Notation "f <∘> g" := (compose_dcpo_funspace g f)(at level 30).
Definition compose_ep_pair {X Y Z}(f : ep_pair X Y)(g : ep_pair Y Z) : ep_pair X Z.
Proof.
split with (compose_dcpo_funspace (pr1 f) (pr1 g)).
split with (compose_dcpo_funspace (pr12 g) (pr12 f)).
split => /=.
- move => x.
rewrite (pr122 g ((pr11 f x))).
apply (pr122 f x).
- move => z.
apply embd_proj_le.
apply (pr222 f).
Qed.
Definition lift_ep_pair {X1 X2 Y1 Y2} (f : ep_pair X1 X2) (g : ep_pair Y1 Y2) : ep_pair ( dcppo_funspace X1 Y1) ( dcppo_funspace X2 Y2).
Proof.
set fe := pr11 f.
set fp := pr112 f.
set ge := pr11 g.
set gp := pr112 g.
use tpair; [|use tpair; [|split]].
- use tpair => /=.
* move => [h Hh].
split with (ge ∘ h ∘ fp).
eapply compose_is_scott_continuous.
+ apply (pr212 f).
+ eapply compose_is_scott_continuous; auto.
apply (pr21 g).
* simpl.
set F : dcpo_funspace X1 Y1 → dcpo_funspace X2 Y2 :=
(λ h : scott_continuous_map X1 Y1,
ge ∘ pr1 h ∘ fp,,
compose_is_scott_continuous fp (ge ∘ pr1 h) (pr212 f)
(compose_is_scott_continuous (pr1 h) ge (pr2 h) (pr21 g))).
use (make_is_scott_continuous F).
+ move => h h' H x.
simpl.
apply (pr121 g).
simpl in H.
apply (H (fp x)).
+ move => /= D.
apply (@antisymm_dcpo (dcpo_funspace X2 Y2)).
* move => x /=.
apply embd_proj_le.
apply dcpo_lub_is_least => /=.
move => j.
cbn.
apply embd_proj_le.
eapply less_than_dcpo_lub.
cbn.
apply refl_dcpo.
* apply dcpo_lub_is_least.
move => /= i x.
apply (pr121 g).
eapply less_than_dcpo_lub => /=.
cbn.
apply refl_dcpo.
- use tpair.
* move => [h Hh].
split with (gp ∘ h ∘ fe).
eapply compose_is_scott_continuous.
+ apply (pr21 f).
+ eapply compose_is_scott_continuous; auto.
apply (pr212 g).
* simpl.
set F : dcpo_funspace X2 Y2 → dcpo_funspace X1 Y1 :=
(λ h : scott_continuous_map X2 Y2,
gp ∘ pr1 h ∘ fe,,
compose_is_scott_continuous fe (gp ∘ pr1 h) (pr21 f)
(compose_is_scott_continuous (pr1 h) gp (pr2 h)
(pr212 g))).
use (make_is_scott_continuous F).
+ move => h h' H x.
simpl.
apply (pr1 (pr212 g)).
simpl in H.
apply (H (fe x)).
+ move => /= D.
apply subtypePath.
{ move => h. apply isaprop_is_scott_continuous. }
apply funextfun => x.
set F' := (F,,
((λ (h h' : scott_continuous_map X2 Y2) (H : ∏ x0 : X2, pr1 h x0 ≤ pr1 h' x0)
(x0 : X1), (pr121 (pr2 g)) (pr1 h (fe x0)) (pr1 h' (fe x0)) (H (fe x0))) :
is_monotone (dcpo_funspace X2 Y2) (dcpo_funspace X1 Y1) F)
).
unfold F, pr1, funcomp.
set D' :=
fun i => pr1 (compose_dcpo_funspace (pr1 f) (D i)) x.
assert (is_directed (pr2 Y2) D'). {
split.
- apply D.
- move => j l.
move : (pr222 D j l).
unfold ishinh; apply => [[k [H1 H2]]].
move => P; apply; clear P.
exists k; split; unfold D' => /=.
move : H1; apply.
move : H2; apply.
}
set D_ : directed_set Y2 := pr1 D,,D',,X.
move : (scott_continuous_map_on_lub (gp,, (pr212 g)) D_) => H0.
simpl in H0.
eapply (@pathscomp0 _ _ (gp (⨆ D_))).
- apply antisymm_dcpo;
apply (pr12 (pr12 g));
apply dcpo_lub_is_least => i; cbn;
apply less_than_dcpo_lub with i; cbn;
apply refl_dcpo.
- rewrite H0.
apply antisymm_dcpo;
apply dcpo_lub_is_least => i;
apply less_than_dcpo_lub with i; cbn;
apply refl_dcpo.
all : simpl.
- move => d.
apply (@antisymm_dcpo ( (dcpo_funspace X1 Y1))) => /= x.
- move : (pr122 g (d (fp (fe x)))).
move : (pr122 f x).
unfold ge, fp, gp.
move ->.
move ->.
apply refl_dcpo.
- move : (pr122 g (d (fp (fe x)))).
move : (pr122 f x).
unfold ge, fp, gp.
move ->.
move ->.
apply refl_dcpo.
- move => e x.
eapply trans_dcpo.
- apply (pr222 g).
- apply (pr12 e).
apply (pr222 f).
Defined.
Definition D_iter (D: dcppo) (n : nat) : dcppo.
Proof.
induction n as [|n D'].
- exact D.
- split with (pr1 (dcpo_funspace D' D')).
split with (pr2 (dcpo_funspace D' D')).
use tpair.
* split with (fun _ => ⊥_{D'}).
use make_is_scott_continuous.
+ move => f g H.
apply refl_dcpo.
+ move => E.
apply antisymm_dcpo.
- apply is_min_bottom_dcppo.
- apply dcpo_lub_is_least => /= i.
cbn.
apply refl_dcpo.
* simpl.
move => f g.
apply is_min_bottom_dcppo.
Defined.
Definition D_constant (D : dcppo) (d : D): dcppo_funspace D D.
Proof.
split with (fun _ => d).
use make_is_scott_continuous.
- move => x y H /=.
apply refl_dcpo.
- move => E.
eapply antisymm_dcpo.
* move : (pr122 E).
unfold ishinh; apply => i.
eapply less_than_dcpo_lub.
simpl. cbn.
apply refl_dcpo.
Unshelve.
2 : auto.
* apply dcpo_lub_is_least => /= => i.
cbn.
apply refl_dcpo.
Defined.
Definition ep_pair_iter (D : dcppo) (n : nat) : ep_pair (D_iter D n) (D_iter D (S n)).
Proof.
induction n as [| n f].
- simpl.
use tpair; [|use tpair; [|split]].
* split with (fun d => D_constant D d).
use (make_is_scott_continuous (fun d => D_constant D d)).
+ move => x y H //=.
+ move => E.
apply antisymm_dcpo.
- move => x.
unfold D_constant => /=.
apply dcpo_lub_is_least => /= i.
eapply less_than_dcpo_lub.
simpl. cbn.
apply refl_dcpo.
- simpl => x.
apply dcpo_lub_is_least => /= i.
apply less_than_dcpo_lub with i.
apply refl_dcpo.
* set h := fun f : dcpo_funspace D D => pr1 f ⊥_{D}.
split with h.
use (make_is_scott_continuous h); unfold h.
+ move => x y /= H.
apply H.
+ move => E.
apply antisymm_dcpo.
- apply dcpo_lub_is_least => /= i.
eapply less_than_dcpo_lub.
simpl. cbn.
apply refl_dcpo.
- apply dcpo_lub_is_least => i.
eapply less_than_dcpo_lub.
cbn.
apply refl_dcpo.
all : simpl; auto.
* move => e x.
apply (pr12 e).
apply is_min_bottom_dcppo.
- exact (lift_ep_pair f f).
Defined.
Definition D_inf (D : dcppo) :=
∑ (d : ∏ n, D_iter D n), ∏ n, (d n) = pr112 (ep_pair_iter D n) (d (S n)).
Lemma isaset_D_inf D : isaset (D_inf D).
Proof.
apply isaset_total2.
- apply impred_isaset => n.
induction n.
* simpl.
apply setproperty.
* simpl.
unfold scott_continuous_map.
+ apply isaset_total2.
apply isaset_set_fun_space.
+ move => f.
apply isasetaprop.
apply isaprop_is_scott_continuous.
- move => x.
apply impred_isaset => n.
apply isasetaprop.
apply (propproperty (x n = (pr112 (ep_pair_iter D n)) (x (S n)))).
Qed.
Definition D_inf_hSet D : hSet := make_hSet (D_inf D) (isaset_D_inf D).
Definition D_inf_order D : PartialOrder (D_inf_hSet D).
Proof.
use make_PartialOrder => /=.
+ unfold D_inf => [[x Hx] [y Hy]].
exact (∀ n, x n ≤ y n).
split; [split|].
+ move => x y z H1 H2 n.
eapply trans_dcpo; eauto.
+ move => x n.
apply refl_dcpo.
+ move => [x Hx] [y Hy] H1 H2.
assert (x = y). {
apply funextsec2 => n.
apply antisymm_dcpo; auto.
}
induction X.
assert (Hx = Hy). {
apply funextsec => n.
move : (propproperty (x n = (pr112 (ep_pair_iter D n)) (x (S n))) (Hx n) (Hy n)).
case; auto.
}
induction X.
auto.
Defined.
Definition dcpo_inf (D : dcppo) : dcppo.
Proof.
split with (D_inf_hSet D).
use tpair => /=.
- use make_dcpo_struct.
* apply (D_inf_order D).
* move => I E HE.
simpl in E.
set E' := fun n i => pr1 (E i) n.
assert (∏ n, is_directed (pr2 (D_iter D n)) (E' n)) as HE'. {
move => n.
move : (pr1 HE) => HI.
split; auto.
move => i j.
move : (pr2 HE i j).
unfold ishinh; apply => [[k /= [Hk1 Hk2]]].
move => P; apply; clear P.
exists k; split; unfold E'; eauto.
}
set En : ∏ n, directed_set (pr2 (D_iter D n)) := fun n => I,, E' n,, HE' n.
set supn : ∏ n, (D_iter D n) := fun n => @dcpo_lub (D_iter D n) (En n).
use tpair => /=.
+ split with supn.
move => n.
unfold supn.
move : ((pr212 (ep_pair_iter D n))).
set fp := pr112 (ep_pair_iter D n) => Hfp.
move : (scott_continuous_map_on_lub (fp,,Hfp) (En (S n))) => H0.
simpl in H0.
rewrite H0.
apply antisymm_dcpo;
apply dcpo_lub_is_least => /= i;
eapply less_than_dcpo_lub with i;
cbn;
unfold E';
induction (E i) as [f Hf] => /=;
rewrite (Hf n);
apply refl_dcpo.
all : simpl.
split.
+ move => i x.
unfold supn.
eapply less_than_dcpo_lub with i.
unfold En, E' => /=.
cbn.
apply refl_dcpo.
+ move => x Hx n.
unfold supn.
apply dcpo_lub_is_least => i.
unfold En, E'; cbn.
apply Hx.
- use tpair.
* use tpair.
+ move => n.
exact (⊥_{D_iter D n}).
+ move => n.
apply antisymm_dcpo.
- apply is_min_bottom_dcppo.
- apply proj_embd_le.
apply is_min_bottom_dcppo.
* simpl.
move => x n.
apply is_min_bottom_dcppo.
Defined.
Notation "D ∞" := (dcpo_inf D) (at level 10).
Lemma le_ex_mid (n m : nat) : n <= m -> ∑ k, paths m (k + n).
Proof.
move : m.
induction n => m H.
- exists m.
rewrite (natplusr0 m); auto.
- destruct m.
- inversion H.
- assert (n <= m) by auto.
move : (IHn _ X) => [k ->] /=.
exists k.
rewrite plus_n_Sm; auto.
Qed.
Definition dcpo_funspace_id D i :
dcpo_funspace (D_iter D i) (D_iter D i).
Proof.
split with (fun x => x).
use make_is_scott_continuous.
+ move => x y xy //=.
+ move => /= E.
apply (@antisymm_dcpo (D_iter D i));
apply dcpo_lub_is_least => k;
apply less_than_dcpo_lub with k; cbn;
apply refl_dcpo.
Defined.
Lemma compose_dcpo_funspace_id_r D i j (f : dcpo_funspace (D_iter D i) (D_iter D j)) :
f <∘> dcpo_funspace_id D i = f.
Proof.
apply subtypePairEquality.
{ move => g. apply isaprop_is_scott_continuous. }
apply funextfun => x //=.
Qed.
Lemma compose_dcpo_funspace_id_l D i j (f : dcpo_funspace (D_iter D j) (D_iter D i)) :
dcpo_funspace_id D i <∘> f = f.
Proof.
apply subtypePairEquality.
{ move => g. apply isaprop_is_scott_continuous. }
apply funextfun => x //=.
Qed.
(* chain_embd *)
Definition chain_embd D i j (H : i <= j) :
dcpo_funspace (D_iter D i) (D_iter D j).
Proof.
move : (le_ex_mid _ _ H) => [k ->].
induction k.
- simpl.
apply dcpo_funspace_id.
- eapply compose_dcpo_funspace; eauto.
exact (pr1 (ep_pair_iter D (k + i))).
Defined.
Lemma chain_embd_id D i : chain_embd D i i (isreflnatleh i) = dcpo_funspace_id D i.
Proof.
apply subtypePairEquality.
{ move => f. apply isaprop_is_scott_continuous. }
induction (le_ex_mid _ _ (isreflnatleh i)) as [k Hk].
assert (0 = k).
{ induction i.
rewrite (natplusr0 k) in Hk; auto.
rewrite <- plus_n_Sm in Hk.
inversion Hk.
apply IHi.
induction H0; auto.
}
induction X.
simpl in Hk.
move : (isasetnat i i Hk (idpath i)) => [E _].
rewrite E.
cbn.
apply funextfun => x //=.
Qed.
Lemma chain_embd_single D i :
chain_embd D i (S i) (natlehnsn i) = pr1 (ep_pair_iter D i).
Proof.
unfold chain_embd, internal_paths_rew_r, nat_rect.
move : (le_ex_mid _ _ (natlehnsn i)) => [k Hk].
assert (1 = k).
{ induction i.
rewrite (natplusr0 k) in Hk; auto.
rewrite <- plus_n_Sm in Hk.
inversion Hk.
apply IHi.
induction H0; auto.
}
induction X.
move : (isasetnat _ _ Hk (idpath (S i))) => [E _].
rewrite E.
simpl.
rewrite (compose_dcpo_funspace_id_r D i (S i)).
auto.
Qed.
Lemma chain_embd_double D i :
chain_embd D i (S (S i)) (istransnatleh (natlehnsn i) (natlehnsn (S i))) =
(pr1 (ep_pair_iter D (S i))) <∘> (pr1 (ep_pair_iter D i)).
Proof.
unfold chain_embd, internal_paths_rew_r, nat_rect.
move : (le_ex_mid _ _ (istransnatleh (natlehnsn i) (natlehnsn (S i)))) => [k Hk].
assert (2 = k).
{ induction i.
rewrite (natplusr0 k) in Hk; auto.
rewrite <- plus_n_Sm in Hk.
inversion Hk.
apply IHi.
induction H0; auto.
}
induction X.
move : (isasetnat _ _ Hk (idpath (S (S i)))) => [E _].
rewrite E.
rewrite (compose_dcpo_funspace_id_r D).
auto.
Qed.
Lemma transportf_le (i j1 j2 : nat) (H1 : i <= j1) (H2 : i <= j2) (H : j1 = j2) :
transportf (fun j => i <= j) H H1 = H2.
Proof.
induction H.
move : (propproperty (i <= j1) H1 H2) => [E _].
rewrite E.
apply (idpath_transportf (λ j : nat, (i <= j))).
Qed.
Lemma transportf_le_S (i : nat) (p1 p2 : ∑ j, i <= j) (H : p1 = p2) (H1 : S i <= pr1 p1) (H2 : S i <= pr1 p2) :
transportf (λ p : ∑ j, (i <= j), ((S i) <= pr1 p)) H H1 = H2.
Proof.
induction H.
move : (propproperty _ H1 H2) => [E _].
rewrite E.
apply (idpath_transportf (λ p : ∑ j, (i <= j), ((S i) <= pr1 p))).
Qed.
Lemma transportf_le' (i j1 j2: nat) (H1 : i <= S (S j1)) (H2 : (i <= S (S j2))) (H : j1 = j2) :
transportf (fun j => i <= S (S j)) H H1 = H2.
Proof.
induction H.
move : (propproperty _ H1 H2) => [E _].
rewrite E.
apply (idpath_transportf (λ j : nat, (i <= S (S j)))).
Qed.
Lemma transportf_le_S' (i : nat) (p1 p2 : ∑ j, i <= S (S j)) (H : p1 = p2) (H1 : S i <= pr1 p1) (H2 : S i <= pr1 p2) :
transportf (λ p : ∑ j, (i <= S (S j)), ((S i) <= pr1 p)) H H1 = H2.
Proof.
induction H.
move : (propproperty _ H1 H2) => [E _].
rewrite E.
apply (idpath_transportf (λ p : ∑ j, (i <= S (S j)), ((S i) <= pr1 p))).
Qed.
Lemma chain_embd_composed_with_single D i j (H : S i <= j) :
let Hij := istransnatleh (natlehnsn i) H in
(
chain_embd D i j Hij =
chain_embd D (S i) j H <∘> (pr1 (ep_pair_iter D i))
×
chain_embd D i (S j) (natlehtolehs _ _ Hij) =
(pr1 (ep_pair_iter D j)) <∘> chain_embd D i j Hij
)%type.
Proof.
move => Hij; unfold Hij; clear Hij.
induction (le_ex_mid _ _ H) as [k Hk].
symmetry in Hk; induction Hk.
move : i H.
induction k => i H.
- split.
+ move : (propproperty (S i <= S i) H (isreflnatleh (S i))) => [E _].
rewrite E; clear E.
rewrite chain_embd_id.
rewrite compose_dcpo_funspace_id_l.
move : (propproperty (i <= S i)
(istransnatleh (natlehnsn i) (isreflnatleh (S i)))
(natlehnsn i)
) => [E _].
rewrite E; clear E.
rewrite chain_embd_single.
auto.
+ move : (propproperty (i <= S i) (istransnatleh (natlehnsn i) H) (natlehnsn i)) => [E _].
rewrite E; clear E.
rewrite chain_embd_single.
rewrite chain_embd_double.
auto.
- move : (IHk _ (natlehmplusnm k (S i))) => [IH1' IH1].
rewrite IH1' in IH1.
rename IH1' into IH0.
move : (propproperty (i <= S k + S i)
(istransnatleh (natlehnsn i) H)
(natlehtolehs i (k + S i) (istransnatleh (natlehnsn i) (natlehmplusnm k (S i))))
) => [E _].
rewrite E; clear E.
rewrite IH1.
split.
- apply subtypePairEquality.
{ move => f. apply isaprop_is_scott_continuous. }
rewrite funcomp_assoc.
suff : (pr1 (chain_embd D (S i) (S k + S i) H) = pr11 (ep_pair_iter D (k + S i)) ∘ pr1 (chain_embd D (S i) (k + S i) (natlehmplusnm k (S i))))%type.
{ move -> => //=. }
(*****)
move : (IHk _ (natlehmplusnm k (S (S i)))) => [IH2 IH2'].
move : IH0 IH1 IH2 IH2'.
change (S (k + S i)) with (S k + S i).
set k_SSi := k + S (S i).
set Sk_Si := S k + S i.
set Si__k_SSi := (istransnatleh (natlehnsn (S i)) (natlehmplusnm k (S (S i)))).
set SSi__k_SSi := (natlehmplusnm k (S (S i))).
rename H into Si__Sk_Si.
assert (S (S i) <= S k + S i) as SSi__Sk_Si. {
repeat rewrite <- plus_n_Sm.
apply (natlehmplusnm k i).
}
assert (S k + S i = k + S (S i)) as Sk_Si__k_SSi. {
simpl; rewrite plus_n_Sm; auto.
}
move => IH0 IH1 IH2 IH3.
assert ((k_SSi,, Si__k_SSi) = ((Sk_Si,, Si__Sk_Si) : (∑ j, S i <= j))). {
use total2_paths2_f; auto.
symmetry; auto.
apply transportf_le.
}
assert ((k_SSi,, Si__k_SSi),, SSi__k_SSi = ((((Sk_Si,, Si__Sk_Si),, SSi__Sk_Si)) : (∑ p : (∑ j, S i <= j ), S (S i) <= pr1 p))). {
use total2_paths2_f; auto.
unfold transportf, constr1, paths_rect.
apply transportf_le_S.
}
set P1 := fun p : (∑ (p : ∑ j, S i <= j), S (S i) <= pr1 p) =>
chain_embd D (S i) (pr11 p) (pr21 p) = chain_embd D (S (S i)) (pr11 p) (pr2 p) <∘> pr1 (ep_pair_iter D (S i)).
set P2 := fun p : (∑ j, S i <= j) =>
chain_embd D (S i) (S (pr1 p)) (natlehtolehs (S i) (pr1 p) (pr2 p)) = pr1 (ep_pair_iter D (pr1 p)) <∘> chain_embd D (S i) (pr1 p) (pr2 p).
move : (transportf P1 X0 IH2); clear IH2 => IH2.
move : (transportf P2 X IH3); clear IH3 => IH3.
unfold P1, P2, pr1, pr2 in IH2, IH3.
(*****)
rewrite IH2 in IH3.
rewrite IH2.
apply funextfun => x.
eapply (embd_is_injective (ep_pair_iter D Sk_Si)).
unfold embd.
apply base_paths in IH3.
unfold compose_dcpo_funspace, pr1 in IH3.
assert (
pr1 (chain_embd D (S i) (S Sk_Si) (natlehtolehs (S i) Sk_Si Si__Sk_Si)) x =
(pr11 (ep_pair_iter D Sk_Si) ∘ (pr1 (chain_embd D (S (S i)) Sk_Si SSi__Sk_Si) ∘ pr11 (ep_pair_iter D (S i)))) x
) as IH3' by (rewrite IH3; auto ).
unfold funcomp in IH3'.
unfold compose_dcpo_funspace, funcomp, pr1.
eapply pathscomp0.
{ symmetry. apply IH3'. }
set f := (pr1 (chain_embd D (S i) (k + S i) (natlehmplusnm k (S i)))).
unfold chain_embd, internal_paths_rew_r.
induction (le_ex_mid (S i) (S Sk_Si) (natlehtolehs (S i) Sk_Si Si__Sk_Si)) as [l Hl].
unfold Sk_Si in Hl.
simpl in Hl.
assert (S (S k) = l). {
move : Hl.
clear => Hl.
repeat rewrite <- plus_n_Sm in Hl.
induction i; simpl in *.
- repeat rewrite natplusr0 in Hl.
inversion Hl; auto.
- repeat rewrite <- plus_n_Sm in Hl.
inversion Hl; auto.
apply IHi.
inversion H0; auto.
}
induction X1.
simpl in Hl.
move : (isasetnat _ _ Hl (idpath (S (S (k + S i))))) => [E _].
rewrite E.
unfold nat_rect.
unfold compose_dcpo_funspace, pr1, funcomp.
repeat apply maponpaths_1.
unfold f.
clear.
unfold chain_embd, internal_paths_rew_r, nat_rect.
induction (le_ex_mid (S i) (k + S i) (natlehmplusnm k (S i))) as [l Hl].
move : (natplusrcan _ _ _ Hl) => kl.
induction kl.
move : (isasetnat _ _ Hl (idpath (k + S i))) => [E _].
rewrite E.
auto.
-
set i__SSk_Si := (natlehtolehs i (S k + S i) (natlehtolehs i (k + S i) (istransnatleh (natlehnsn i) (natlehmplusnm k (S i))))).
set Si__k_Si := (natlehmplusnm k (S i)).
set i__SSSk_i := (natlehmplusnm (S (S (S k))) i).
assert (S i <= S k + i) as Si__Sk_i. {
rewrite <- plus_n_Sm in Si__k_Si.
auto.
}
set U := (∑ p : ∑ j : nat, (i ≤ S (S j))%nat, S i ≤ pr1 p)%nat.
assert ((((S k + i,,i__SSSk_i),,Si__Sk_i) : U) = (k + S i,,i__SSk_Si),,Si__k_Si). {
clear.
use total2_paths2_f.
- use total2_paths2_f.
* simpl; rewrite plus_n_Sm; auto.
* apply transportf_le'.
- apply transportf_le_S'.
}
set Q := fun p : U =>
chain_embd D i (S (S (pr11 p))) (pr21 p) =
pr1 (ep_pair_iter D (S (pr11 p))) <∘>
(pr1 (ep_pair_iter D (pr11 p)) <∘>
(chain_embd D (S i) (pr11 p) (pr2 p) <∘> pr1 (ep_pair_iter D i))).
suff : (Q ((k + S i,,i__SSk_Si),,Si__k_Si)) by auto.
apply (transportf Q X).
unfold Q, pr1, pr2.
set f := (chain_embd D (S i) (S k + i) Si__Sk_i).
unfold chain_embd, internal_paths_rew_r.
unfold f; clear f.
induction (le_ex_mid i (S (S (S k + i))) i__SSSk_i) as [l Hl].
assert (S (S (S k)) = l). {
move : Hl; clear => Hl.
induction i.
- repeat rewrite natplusr0 in Hl; auto.
-
repeat rewrite <- plus_n_Sm in Hl.
inversion Hl; auto.
apply IHi.
rewrite H0; auto.
}
induction X0.
simpl in Hl.
move : (isasetnat _ _ Hl (idpath (S (S (S (k + i)))))) => [E _].
rewrite E.
unfold nat_rect.
set f := ((fix F (n : nat) : dcpo_funspace (D_iter D i) (D_iter D (n + i)) :=
match n as n0 return (dcpo_funspace (D_iter D i) (D_iter D (n0 + i))) with
| 0 => dcpo_funspace_id D i
| S n0 =>
(λ x0 : D_iter D i, (pr11 (ep_pair_iter D (n0 + i))) (pr1 (F n0) x0)),,
compose_is_scott_continuous (pr1 (F n0)) (pr11 (ep_pair_iter D (n0 + i)))
(pr2 (F n0)) (pr21 (ep_pair_iter D (n0 + i)))
end) k).
assert (f = chain_embd D i (k + i) (natlehmplusnm k i)). {
unfold chain_embd, internal_paths_rew_r.
induction (le_ex_mid i (k + i) (natlehmplusnm k i)) as [l Hk].
move : (natplusrcan _ _ _ Hk) => E0.
induction E0.
move : (isasetnat _ _ Hk (idpath (k + i))) => [E0 _].
rewrite E0.
unfold f; auto.
}
rewrite X0; clear X0 f.
suff : (
pr1 (ep_pair_iter D (S k + i)) <∘>
(pr1 (ep_pair_iter D (k + i)) <∘> chain_embd D i (k + i) (natlehmplusnm k i))
=
pr1 (ep_pair_iter D (S k + i)) <∘>
(chain_embd D (S i) (S k + i) Si__Sk_i <∘> pr1 (ep_pair_iter D i))
). { move ->. reflexivity. }
move : IH1; clear => IH.
assert (((k + S i,, natlehmplusnm k (S i)) : ∑ j, (S i) <= j) = S k + i,, Si__Sk_i). {
use total2_paths2_f.
- rewrite <- plus_n_Sm; auto.
- apply transportf_le.
}
assert (
∏ i (p1 p2 : ∑ j, S i <= j) (H : p1 = p2)
(H1 : i <= S (pr1 p1)) (H2 : i <= S (pr1 p2)),
transportf (fun p : ∑ j, S i <= j => i <= S (pr1 p)) H H1 = H2
). {
clear; intros.
induction H.
move : (propproperty _ H1 H2) => [E _].
rewrite E.
apply (idpath_transportf(fun p : ∑ j, S i <= j => i <= S (pr1 p))).
}
set i__Sk_Si := (natlehtolehs i (k + S i) (istransnatleh (natlehnsn i) (natlehmplusnm k (S i)))) .
assert (
(((k + S i,, natlehmplusnm k (S i)),, i__Sk_Si) : (∑ p : (∑ j, S i <= j), i <= S (pr1 p)))
=
(S k + i,, Si__Sk_i),, natlehmplusnm (S (S k)) i
). {
use total2_paths2_f; auto.
apply X0.
}
set P := fun p : (∑ p : (∑ j, S i <= j), i <= S (pr1 p)) =>
chain_embd D i (S (pr11 p)) (pr2 p) =
pr1 (ep_pair_iter D (pr11 p )) <∘>
((chain_embd D (S i) (pr11 p) (pr21 p) <∘> pr1 (ep_pair_iter D i))).
move : (transportf P X1 IH) => IH'.
unfold P, pr1, pr2 in IH'.
eapply pathscomp0; first last.
apply IH'.
set f := chain_embd D i (k + i) (natlehmplusnm k i).
unfold chain_embd, internal_paths_rew_r, nat_rect.
induction (le_ex_mid i (S (S k + i)) (natlehmplusnm (S (S k)) i)) as [l Hl].
assert (S (S k) = l). {
move : Hl; clear => Hl.
induction i.
- repeat rewrite natplusr0 in Hl; auto.
- repeat rewrite <- plus_n_Sm in Hl.
inversion Hl; auto.
apply IHi.
rewrite H0; auto.
}
induction X2.
move : (isasetnat _ _ Hl (idpath (S (S k) + i))) => [E _].
rewrite E.
apply subtypePairEquality.
{ move => g. apply isaprop_is_scott_continuous. }
apply funextfun => x.
unfold compose_dcpo_funspace, pr1, funcomp, f.
repeat apply maponpaths.
clear.
unfold chain_embd, internal_paths_rew_r, nat_rect.
induction (le_ex_mid i (k + i) (natlehmplusnm k i)) as [l Hl].
move : (natplusrcan _ _ _ Hl) => kl.
induction kl.
move : (isasetnat _ _ Hl (idpath (k + i))) => [E _].
rewrite E.
auto.
Qed.
Lemma chain_embd_composed_with_single' D i j (H : S i <= j) :
let Hij := istransnatleh (natlehnsn i) H in
(
chain_embd D i (S j) (natlehtolehs _ _ Hij) =
(pr1 (ep_pair_iter D j)) <∘> (chain_embd D (S i) j H <∘> (pr1 (ep_pair_iter D i)))
)%type.
Proof.
move => Hij; unfold Hij; clear Hij.
move : (chain_embd_composed_with_single D i j H) => [H1 H2].
rewrite <- H1.
rewrite H2.
auto.
Qed.
Lemma compose_dcpo_funspace_assoc D i j k l
(f : dcpo_funspace (D_iter D i) (D_iter D j))
(g : dcpo_funspace (D_iter D j) (D_iter D k))
(h : dcpo_funspace (D_iter D k) (D_iter D l)) :
h <∘> (g <∘> f) = h <∘> g <∘> f.
Proof.
apply subtypePairEquality.
{ move => x. apply isaprop_is_scott_continuous. }
unfold compose_dcpo_funspace, pr1, funcomp.
apply funextfun => x.
auto.
Qed.
Lemma chain_embd_compose D i j k (ij : i <= j) (jk : j <= k) :
(chain_embd D j k jk) <∘> (chain_embd D i j ij) =
chain_embd D i k (istransnatleh ij jk).
Proof.
move : (le_ex_mid _ _ ij) => [l Hl].
symmetry in Hl; induction Hl.
move : i k ij jk.
induction l => i k Hi Hk.
- move : (propproperty _ Hi (isreflnatleh i)) => [E _].
rewrite E; clear E.
rewrite chain_embd_id.
rewrite compose_dcpo_funspace_id_r.
move : (propproperty _ (istransnatleh (isreflnatleh i) Hk) Hk) => [E _].
rewrite E; clear E.
auto.
- move : (IHl i (S l + i) (natlehmplusnm l i) (natlehnsn (l + i))).
rewrite (pr1 (propproperty _ (istransnatleh (natlehmplusnm l i) (natlehnsn (l + i))) Hi)).
move <-.
move : (chain_embd_composed_with_single D (l + i) k Hk) => [H1 _].
rewrite chain_embd_single.
rewrite compose_dcpo_funspace_assoc.
change (S l + i) with (S (l + i)).
rewrite <- H1.
set Hi' := (natlehmplusnm l i).
set Hj' := istransnatleh (natlehnsn (l + i)) Hk.
move : (propproperty _ (istransnatleh Hi Hk) ((istransnatleh Hi' Hj'))) => [E _].
rewrite E.
apply IHl.
Qed.
Definition chain_proj D i j (H : i <= j) :
dcpo_funspace (D_iter D j) (D_iter D i).
Proof.
move : (le_ex_mid _ _ H) => [k ->].
induction k.
- simpl.
apply dcpo_funspace_id.
- eapply compose_dcpo_funspace; eauto.
exact (pr12 (ep_pair_iter D (k + i))).
Defined.
Lemma chain_proj_id D i : chain_proj D i i (isreflnatleh i) = dcpo_funspace_id D i.
Proof.
apply subtypePairEquality.
{ move => f. apply isaprop_is_scott_continuous. }
induction (le_ex_mid _ _ (isreflnatleh i)) as [k Hk].
assert (0 = k).
{ induction i.
rewrite (natplusr0 k) in Hk; auto.
rewrite <- plus_n_Sm in Hk.
inversion Hk.
apply IHi.
induction H0; auto.
}
induction X.
simpl in Hk.
move : (isasetnat i i Hk (idpath i)) => [E _].
rewrite E.
cbn.
apply funextfun => x //=.
Qed.
Lemma chain_proj_single D i :
chain_proj D i (S i) (natlehnsn i) = pr12 (ep_pair_iter D i).
Proof.
unfold chain_proj, internal_paths_rew_r, nat_rect.
move : (le_ex_mid _ _ (natlehnsn i)) => [k Hk].
assert (1 = k).
{ induction i.
rewrite (natplusr0 k) in Hk; auto.
rewrite <- plus_n_Sm in Hk.
inversion Hk.
apply IHi.
induction H0; auto.
}
induction X.
move : (isasetnat _ _ Hk (idpath (S i))) => [E _].
rewrite E.
simpl.
rewrite (compose_dcpo_funspace_id_l D i (S i)).
auto.
Qed.
Lemma chain_proj_double D i :
chain_proj D i (S (S i)) (istransnatleh (natlehnsn i) (natlehnsn (S i))) =
(pr12 (ep_pair_iter D i)) <∘> (pr12 (ep_pair_iter D (S i))) .
Proof.
unfold chain_proj, internal_paths_rew_r, nat_rect.
move : (le_ex_mid _ _ (istransnatleh (natlehnsn i) (natlehnsn (S i)))) => [k Hk].
assert (2 = k).
{ induction i.
rewrite (natplusr0 k) in Hk; auto.
rewrite <- plus_n_Sm in Hk.
inversion Hk.
apply IHi.
induction H0; auto.
}
induction X.
move : (isasetnat _ _ Hk (idpath (S (S i)))) => [E _].
rewrite E.
rewrite (compose_dcpo_funspace_id_l D).
auto.
Qed.
Lemma chain_proj_composed_with_single D i j (H : S i <= j) :
let Hij := istransnatleh (natlehnsn i) H in
(
chain_proj D i j Hij =
(pr12 (ep_pair_iter D i)) <∘> chain_proj D (S i) j H
×
chain_proj D i (S j) (natlehtolehs _ _ Hij) =
chain_proj D i j Hij <∘> (pr12 (ep_pair_iter D j))
)%type.
Proof.
move => Hij; unfold Hij; clear Hij.
induction (le_ex_mid _ _ H) as [k Hk].
symmetry in Hk; induction Hk.
move : i H.
induction k => i H.
- change (0 + S i) with (S i).
split.
+ set H' := (istransnatleh (natlehnsn i) H).
move : (propproperty (S i <= S i) H (isreflnatleh (S i))) => [E _].
rewrite E; clear E.
rewrite chain_proj_id.
rewrite compose_dcpo_funspace_id_r.
move : (propproperty (i <= S i)
H'
(natlehnsn i)
) => [E _].
rewrite E; clear E.
rewrite chain_proj_single.
auto.
+ move : (propproperty (i <= S i) (istransnatleh (natlehnsn i) H) (natlehnsn i)) => [E _].
rewrite E; clear E.
rewrite chain_proj_single.
rewrite chain_proj_double.
auto.
- move : (IHk _ (natlehmplusnm k (S i))) => [IH1' IH1].
rewrite IH1' in IH1.
rename IH1' into IH0.
move : (propproperty (i <= S k + S i)
(istransnatleh (natlehnsn i) H)
(natlehtolehs i (k + S i) (istransnatleh (natlehnsn i) (natlehmplusnm k (S i))))
) => [E _].
rewrite E; clear E.
rewrite IH1.
(* clear IH1. *)
split.
-
rewrite <- compose_dcpo_funspace_assoc.
suff : (chain_proj D (S i) (k + S i) (natlehmplusnm k (S i)) <∘> pr12 (ep_pair_iter D (k + S i)))
= chain_proj D (S i) (S k + S i) H.
{ move -> => //=. }
(*****)
move : (IHk _ (natlehmplusnm k (S (S i)))) => [IH2 IH3].
move : IH0 IH1 IH2 IH3.
set k_SSi := k + S (S i).
set Sk_Si := S k + S i.
set Si__k_SSi := (istransnatleh (natlehnsn (S i)) (natlehmplusnm k (S (S i)))).
set SSi__k_SSi := (natlehmplusnm k (S (S i))).
rename H into Si__Sk_Si.
assert (S (S i) <= S k + S i) as SSi__Sk_Si. {
repeat rewrite <- plus_n_Sm.
apply (natlehmplusnm k i).
}
assert (S k + S i = k + S (S i)) as Sk_Si__k_SSi. {
simpl; rewrite plus_n_Sm; auto.
}
move => IH0 IH1 IH2 IH3.
assert ((k_SSi,, Si__k_SSi) = ((Sk_Si,, Si__Sk_Si) : (∑ j, S i <= j))). {
use total2_paths2_f; auto.
symmetry; auto.
apply transportf_le.
}
assert ((k_SSi,, Si__k_SSi),, SSi__k_SSi = ((((Sk_Si,, Si__Sk_Si),, SSi__Sk_Si)) : (∑ p : (∑ j, S i <= j ), S (S i) <= pr1 p))). {
use total2_paths2_f; auto.
unfold transportf, constr1, paths_rect.
apply transportf_le_S.
}
set P2 := fun p : (∑ (p : ∑ j, S i <= j), S (S i) <= pr1 p) =>
chain_proj D (S i) (pr11 p) (pr21 p) =
pr12 (ep_pair_iter D (S i)) <∘> chain_proj D (S (S i)) (pr11 p) (pr2 p) .
set P3 := fun p : (∑ j, S i <= j) =>
chain_proj D (S i) (S (pr1 p)) (natlehtolehs (S i) (pr1 p) (pr2 p)) =
chain_proj D (S i) (pr1 p) (pr2 p) <∘> pr12 (ep_pair_iter D (pr1 p)).
move : (transportf P2 X0 IH2); clear IH2 => IH2.
move : (transportf P3 X IH3); clear IH3 => IH3.
unfold P3, P2, pr1, pr2 in IH2, IH3.
clear X X0 P2 P3 k_SSi Si__k_SSi SSi__k_SSi IHk.
rewrite IH2 in IH3.
rewrite IH2.
apply subtypePairEquality.
{ move => f; apply isaprop_is_scott_continuous. }
apply funextfun => x.
unfold funcomp.
apply base_paths in IH3.
unfold compose_dcpo_funspace, pr1, funcomp in IH3.
assert (
pr1 (chain_proj D (S i) (S Sk_Si) (natlehtolehs (S i) Sk_Si Si__Sk_Si)) ((pr11 (ep_pair_iter D Sk_Si)) x) =
pr112 (ep_pair_iter D (S i))
(pr1 (chain_proj D (S (S i)) Sk_Si SSi__Sk_Si) ((pr112 (ep_pair_iter D Sk_Si)) (((pr11 (ep_pair_iter D Sk_Si)) x))))
) as IH3' by (rewrite IH3; auto ).
move : (pr122 (ep_pair_iter D Sk_Si) x) => Hx.
rewrite Hx in IH3'.
eapply pathscomp0; first last.
apply IH3'.
set f := pr1 (chain_proj D (S i) (k + S i) (natlehmplusnm k (S i))) ((pr112 (ep_pair_iter D (k + S i))) x).
unfold chain_proj, internal_paths_rew_r.
induction (le_ex_mid (S i) (S Sk_Si) (natlehtolehs (S i) Sk_Si Si__Sk_Si)) as [l Hl].
unfold Sk_Si in Hl.
simpl in Hl.
assert (S (S k) = l). {
move : Hl.
clear => Hl.
repeat rewrite <- plus_n_Sm in Hl.
induction i; simpl in *.
- repeat rewrite natplusr0 in Hl.
inversion Hl; auto.
- repeat rewrite <- plus_n_Sm in Hl.
inversion Hl; auto.
apply IHi.
inversion H0; auto.
}
induction X.
simpl in Hl.
move : (isasetnat _ _ Hl (idpath (S (S (k + S i))))) => [E _].
rewrite E.
unfold nat_rect.
set g := (((fix F (n : nat) : dcpo_funspace (D_iter D (n + S i)) (D_iter D (S i)) :=
match n as n0 return (dcpo_funspace (D_iter D (n0 + S i)) (D_iter D (S i))) with
| 0 => dcpo_funspace_id D (S i)
| S n0 => F n0 <∘> pr12 (ep_pair_iter D (n0 + S i))
end) k)).
unfold compose_dcpo_funspace, pr1, funcomp.
rewrite Hx.
unfold f.
suff : g = (chain_proj D (S i) (k + S i) (natlehmplusnm k (S i))) .
{ move -> => //=. }
unfold g.
clear.
unfold chain_proj, internal_paths_rew_r, nat_rect.
induction (le_ex_mid (S i) (k + S i) (natlehmplusnm k (S i))) as [l Hl].
move : (natplusrcan _ _ _ Hl) => kl.
induction kl.
move : (isasetnat _ _ Hl (idpath (k + S i))) => [E _].
rewrite E.
reflexivity.
- set i__SSk_Si := (natlehtolehs i (S k + S i) (natlehtolehs i (k + S i) (istransnatleh (natlehnsn i) (natlehmplusnm k (S i))))).
set Si__k_Si := (natlehmplusnm k (S i)).
set i__SSSk_i := (natlehmplusnm (S (S (S k))) i).
assert (S i <= S k + i) as Si__Sk_i. {
rewrite <- plus_n_Sm in Si__k_Si.
auto.
}
set U := (∑ p : ∑ j : nat, (i ≤ S (S j))%nat, S i ≤ pr1 p)%nat.
assert ((((S k + i,,i__SSSk_i),,Si__Sk_i) : U) = (k + S i,,i__SSk_Si),,Si__k_Si). {
clear.
use total2_paths2_f.
- use total2_paths2_f.
* simpl; rewrite plus_n_Sm; auto.
* apply transportf_le'.
- apply transportf_le_S'.
}
set Q := fun p : U =>
chain_proj D i (S (S (pr11 p))) (pr21 p) =
((pr12 (ep_pair_iter D i) <∘> chain_proj D (S i) (pr11 p) (pr2 p)) <∘>
pr12 (ep_pair_iter D (pr11 p)) <∘> (pr12 (ep_pair_iter D (S (pr11 p))))).
suff : (Q ((k + S i,,i__SSk_Si),,Si__k_Si)) by auto.
apply (transportf Q X).
unfold Q, pr1, pr2.
set f := (chain_proj D (S i) (S k + i) Si__Sk_i).
unfold chain_proj, internal_paths_rew_r.
unfold f; clear f.
induction (le_ex_mid i (S (S (S k + i))) i__SSSk_i) as [l Hl].
assert (S (S (S k)) = l). {
move : Hl; clear => Hl.
induction i.
- repeat rewrite natplusr0 in Hl; auto.
-
repeat rewrite <- plus_n_Sm in Hl.
inversion Hl; auto.
apply IHi.
rewrite H0; auto.
}
induction X0.
simpl in Hl.
move : (isasetnat _ _ Hl (idpath (S (S (S (k + i)))))) => [E _].
rewrite E.
unfold nat_rect.
set f :=(fix F (n : nat) : dcpo_funspace (D_iter D (n + i)) (D_iter D i) :=
match n as n0 return (dcpo_funspace (D_iter D (n0 + i)) (D_iter D i)) with
| 0 => dcpo_funspace_id D i
| S n0 => F n0 <∘> pr12 (ep_pair_iter D (n0 + i))
end) k.
assert (f = chain_proj D i (k + i) (natlehmplusnm k i)). {
unfold chain_proj, internal_paths_rew_r.
induction (le_ex_mid i (k + i) (natlehmplusnm k i)) as [l Hk].
move : (natplusrcan _ _ _ Hk) => E0.
induction E0.
move : (isasetnat _ _ Hk (idpath (k + i))) => [E0 _].
rewrite E0.
unfold f; auto.
}
rewrite X0; clear X0 f.
change (S (S k) + i) with (S (S k + i)).
suff : (
(chain_proj D i (k + i) (natlehmplusnm k i) <∘> pr12 (ep_pair_iter D (k + i)))
<∘> pr12 (ep_pair_iter D (S k + i))
=
(pr12 (ep_pair_iter D i) <∘> chain_proj D (S i) (S k + i) Si__Sk_i)
<∘> pr12 (ep_pair_iter D (S k + i))
). { move ->; reflexivity. }
move : IH1; clear => IH.
assert (((k + S i,, natlehmplusnm k (S i)) : ∑ j, (S i) <= j) = S k + i,, Si__Sk_i). {
use total2_paths2_f.
- rewrite <- plus_n_Sm; auto.
- apply transportf_le.
}
assert (
∏ i (p1 p2 : ∑ j, S i <= j) (H : p1 = p2)
(H1 : i <= S (pr1 p1)) (H2 : i <= S (pr1 p2)),
transportf (fun p : ∑ j, S i <= j => i <= S (pr1 p)) H H1 = H2
). {
clear; intros.
induction H.
move : (propproperty _ H1 H2) => [E _].
rewrite E.
apply (idpath_transportf(fun p : ∑ j, S i <= j => i <= S (pr1 p))).
}
set i__Sk_Si := (natlehtolehs i (k + S i) (istransnatleh (natlehnsn i) (natlehmplusnm k (S i)))) .
assert (
(((k + S i,, natlehmplusnm k (S i)),, i__Sk_Si) : (∑ p : (∑ j, S i <= j), i <= S (pr1 p)))
=
(S k + i,, Si__Sk_i),, natlehmplusnm (S (S k)) i
). {
use total2_paths2_f; auto.
apply X0.
}
set P := fun p : (∑ p : (∑ j, S i <= j), i <= S (pr1 p)) =>
chain_proj D i (S (pr11 p)) (pr2 p) =
(pr12 (ep_pair_iter D i) <∘> chain_proj D (S i) (pr11 p) (pr21 p)) <∘>
pr12 (ep_pair_iter D (pr11 p )).
move : (transportf P X1 IH) => IH'.
unfold P, pr1, pr2 in IH'.
eapply pathscomp0; first last.
apply IH'.
set f := chain_proj D i (k + i) (natlehmplusnm k i).
unfold chain_proj, internal_paths_rew_r, nat_rect.
induction (le_ex_mid i (S (S k + i)) (natlehmplusnm (S (S k)) i)) as [l Hl].
assert (S (S k) = l). {
move : Hl; clear => Hl.
induction i.
- repeat rewrite natplusr0 in Hl; auto.
- repeat rewrite <- plus_n_Sm in Hl.
inversion Hl; auto.
apply IHi.
rewrite H0; auto.
}
induction X2.
move : (isasetnat _ _ Hl (idpath (S (S k) + i))) => [E _].
rewrite E.
set g := ((fix F (n : nat) : dcpo_funspace (D_iter D (n + i)) (D_iter D i) :=
match n as n0 return (dcpo_funspace (D_iter D (n0 + i)) (D_iter D i)) with
| 0 => dcpo_funspace_id D i
| S n0 => F n0 <∘> pr12 (ep_pair_iter D (n0 + i))
end) k).
repeat rewrite <- compose_dcpo_funspace_assoc.
suff : f = g. { move ->. auto. }
unfold f, g.
clear.
unfold chain_proj, internal_paths_rew_r, nat_rect.
induction (le_ex_mid i (k + i) (natlehmplusnm k i)) as [l Hl].
move : (natplusrcan _ _ _ Hl) => kl.
induction kl.
move : (isasetnat _ _ Hl (idpath (k + i))) => [E _].
rewrite E.
reflexivity.
Qed.
Lemma chain_proj_compose D i j k (ij : i <= j) (jk : j <= k) :
(chain_proj D i j ij) <∘> (chain_proj D j k jk) =
chain_proj D i k (istransnatleh ij jk).
Proof.
move : (le_ex_mid _ _ ij) => [l Hl].
symmetry in Hl; induction Hl.
move : i k ij jk.
induction l => i k Hi Hk.
- move : (propproperty _ Hi (isreflnatleh i)) => [E _].
rewrite E; clear E.
rewrite chain_proj_id.
rewrite compose_dcpo_funspace_id_l.
move : (propproperty _ (istransnatleh (isreflnatleh i) Hk) Hk) => [E _].
rewrite E; clear E.
auto.
-
move : (IHl i (S l + i) (natlehmplusnm l i) (natlehnsn (l + i))).
rewrite (pr1 (propproperty _ (istransnatleh (natlehmplusnm l i) (natlehnsn (l + i))) Hi)).
move <-.
move : (chain_proj_composed_with_single D (l + i) k Hk) => [H1 _].
rewrite chain_proj_single.
rewrite <- compose_dcpo_funspace_assoc.
change (S l + i) with (S (l + i)).
rewrite <- H1.
set Hi' := (natlehmplusnm l i).
set Hj' := istransnatleh (natlehnsn (l + i)) Hk.
move : (propproperty _ (istransnatleh Hi Hk) ((istransnatleh Hi' Hj'))) => [E _].
rewrite E.
apply IHl.
Qed.
Definition dcpo_inf_proj D n : dcpo_funspace (D ∞) (D_iter D n).
Proof.
split with (fun f => pr1 f n).
use make_is_scott_continuous.
* move => /= x y H.
eauto.
* move => E.
apply antisymm_dcpo.
- apply dcpo_lub_is_least => /= i.
eapply less_than_dcpo_lub.
cbn => /=.
apply refl_dcpo.
- apply dcpo_lub_is_least => /= i.
eapply less_than_dcpo_lub.
simpl. cbn.
apply refl_dcpo.
Defined.
Definition chain_ep_pair D i j (H : i <= j) :
ep_pair (D_iter D i) (D_iter D j).
Proof.
use tpair; [|use tpair; [|split]].
- exact (chain_embd D i j H).
- exact (chain_proj D i j H).
- move => di.
move : (le_ex_mid _ _ H) => [k Hk].
symmetry in Hk; induction Hk.
move : i H di.
induction k => i H di.
* rewrite (pr1 (propproperty _ H (isreflnatleh i))).
rewrite chain_proj_id.
rewrite chain_embd_id.
simpl; auto.
* assert ((chain_proj D i (S k + i) H) =
((chain_proj D i (k + i) (natlehmplusnm k i)) <∘> (pr12 (ep_pair_iter D (k + i))))).
{ rewrite <- chain_proj_single.
rewrite chain_proj_compose.
rewrite (pr1 (propproperty _ H (istransnatleh (natlehmplusnm k i) (natlehnsn (k + i))))).
auto.
}
rewrite X; clear X.
assert ((chain_embd D i (S k + i) H) =
((pr1 (ep_pair_iter D (k + i))) <∘> (chain_embd D i (k + i) (natlehmplusnm k i)))).
{ rewrite <- chain_embd_single.
rewrite chain_embd_compose.
rewrite (pr1 (propproperty _ H (istransnatleh (natlehmplusnm k i) (natlehnsn (k + i))))).
auto.
}
rewrite X; clear X.
unfold compose_dcpo_funspace, pr1, funcomp.
rewrite (pr122 (ep_pair_iter D (k + i))).
apply IHk.
- move => di.
move : (le_ex_mid _ _ H) => [k Hk].
symmetry in Hk; induction Hk.
move : i H di.
induction k => i H di.
* rewrite (pr1 (propproperty _ H (isreflnatleh i))).
rewrite chain_proj_id.
rewrite chain_embd_id.
simpl; auto.
apply refl_dcpo.
* assert ((chain_proj D i (S k + i) H) =
((chain_proj D i (k + i) (natlehmplusnm k i)) <∘> (pr12 (ep_pair_iter D (k + i))))).
{ rewrite <- chain_proj_single.
rewrite chain_proj_compose.
rewrite (pr1 (propproperty _ H (istransnatleh (natlehmplusnm k i) (natlehnsn (k + i))))).
auto.
}
rewrite X; clear X.
assert ((chain_embd D i (S k + i) H) =
((pr1 (ep_pair_iter D (k + i))) <∘> (chain_embd D i (k + i) (natlehmplusnm k i)))).
{ rewrite <- chain_embd_single.
rewrite chain_embd_compose.
rewrite (pr1 (propproperty _ H (istransnatleh (natlehmplusnm k i) (natlehnsn (k + i))))).
auto.
}
rewrite X; clear X.
unfold compose_dcpo_funspace, pr1, funcomp.
move : (IHk i (natlehmplusnm k i) ((pr112 (ep_pair_iter D (k + i))) di)) => H0.
move : (pr121 (ep_pair_iter D (k + i)) _ _ H0) => H1.
eapply trans_dcpo; eauto.
apply (pr222 (ep_pair_iter D (k + i))).
Defined.
Definition kapper D (i j : nat) : dcpo_funspace (D_iter D i) (D_iter D j) :=
pr12 (chain_ep_pair D j (i + j) (natlehmplusnm i j)) <∘> pr1 (chain_ep_pair D i (i + j) (natlehnplusnm i j)).
Definition rho D n : (D_iter D n) -> (D ∞).
Proof.
move => x.
use tpair.
* move => m.
exact (pr1 (kapper D n m) x).
* move => m.
unfold kapper, chain_ep_pair, pr1, pr2.
rewrite <- chain_proj_single.
unfold compose_dcpo_funspace, pr1, funcomp in *.
move : (chain_proj_compose D m (S m) (n + S m) (natlehnsn m) (natlehmplusnm n (S m))) => H0.
apply base_paths in H0 .
unfold compose_dcpo_funspace, pr1 in H0.
assert (
(pr1 (chain_proj D m (S m) (natlehnsn m)) ∘
pr1 (chain_proj D (S m) (n + S m) (natlehmplusnm n (S m))))
(pr1 (chain_embd D n (n + S m) (natlehnplusnm n (S m))) x) =
(pr1 (chain_proj D m (n + S m) (istransnatleh (natlehnsn m) (natlehmplusnm n (S m))))
(pr1 (chain_embd D n (n + S m) (natlehnplusnm n (S m))) x))
). {rewrite H0. auto. }
clear H0.
unfold funcomp in X.
rewrite X.
assert (n + m <= n + S m). {
rewrite <- plus_n_Sm.
apply natlehnsn.
}
move : (chain_proj_compose D m (n + m) (n + S m) (natlehmplusnm n m) X0) => H0.
set y := (pr1 (chain_embd D n (n + S m) (natlehnplusnm n (S m))) x).
assert (
( pr1 (chain_proj D m (n + m) (natlehmplusnm n m)) ∘ pr1 (chain_proj D (n + m) (n + S m) X0)) y =
pr1 (chain_proj D m (n + S m) (istransnatleh (natlehmplusnm n m) X0)) y
). { rewrite <- H0; auto. }
clear H0.
rewrite <- (pr1 (propproperty _ (istransnatleh (natlehmplusnm n m) X0) (istransnatleh (natlehnsn m) (natlehmplusnm n (S m))) )).
rewrite <- X1.
clear X1.
move : (chain_embd_compose D n (n + m) (n + S m) (natlehnplusnm n m) X0) => H0.
assert (
(pr1 (chain_embd D (n + m) (n + S m) X0) ∘ pr1 (chain_embd D n (n + m) (natlehnplusnm n m))) x =
pr1 (chain_embd D n (n + S m) (istransnatleh (natlehnplusnm n m) X0)) x
). { rewrite <- H0; auto. }
unfold funcomp in X1.
unfold y.
rewrite (pr1 (propproperty _ (natlehnplusnm n (S m)) (istransnatleh (natlehnplusnm n m) X0))).
rewrite <- X1.
unfold funcomp.
rewrite (pr122 (chain_ep_pair D (n + m) (n + S m) X0)).
auto.
Defined.
Definition dcpo_inf_embd D n : dcpo_funspace (D_iter D n) (D ∞).
Proof.
split with (rho D n).
use make_is_scott_continuous.
- move => /= x y H m.
apply (pr12 (chain_proj D m (n + m) (natlehmplusnm n m))).
apply (pr12 (chain_embd D n (n + m) (natlehnplusnm n m))).
auto.
- move => E.
apply antisymm_dcpo => /= m.
all :move : (scott_continuous_map_on_lub (kapper D n m) E) => H.
all : unfold kapper in H.
all : unfold compose_dcpo_funspace, pr1, funcomp in H.
all : simpl in H.
all : rewrite H.
all : apply dcpo_lub_is_least => /= i;
eapply less_than_dcpo_lub;
simpl; cbn;
apply refl_dcpo.
Defined.
Lemma dcpo_inf_chain_proj D (f : D∞) n m (H : n <= m) :
pr1 f n = pr1 (chain_proj D n m H) (pr1 f m).
Proof.
move : (le_ex_mid _ _ H) => [k Hk].
symmetry in Hk; induction Hk.
move : n H f.
induction k => n H f.
- simpl.
rewrite (pr1 (propproperty _ H (isreflnatleh n))).
rewrite chain_proj_id => //=.
- move : (pr2 f) => Hf.
rewrite (IHk n (natlehmplusnm k n) f).
rewrite (Hf (k + n)).
set F := (pr1 f (S k + n)).
rewrite <- chain_proj_single.
move : (chain_proj_compose D n (k + n) (S k + n)
(natlehmplusnm k n) (natlehnsn (k + n))).
rewrite (pr1 (propproperty _ (istransnatleh (natlehmplusnm k n) (natlehnsn (k + n))) H)).
move => H0.
assert (
(pr1 (chain_proj D n (k + n) (natlehmplusnm k n)) ∘
pr1 (chain_proj D (k + n) (S k + n) (natlehnsn (k + n)))) F =
pr1 (chain_proj D n (S k + n) H) F
). { rewrite <- H0; auto. }
unfold funcomp in X.
auto.
Qed.
Definition dcpo_inf_ep_pair D n :
ep_pair (D_iter D n) (D ∞).
Proof.
use tpair; [|use tpair; [|split]].
- exact (dcpo_inf_embd D n).
- exact (dcpo_inf_proj D n).
- move => /= x.
move : (pr122 (chain_ep_pair D n (n + n) (natlehmplusnm n n)) x).
unfold chain_ep_pair, pr1, pr2.
rewrite (pr1 (propproperty _ (natlehnplusnm n n) (natlehmplusnm n n))).
apply.
- move => /= f m /=.
rewrite (dcpo_inf_chain_proj D f _ _ (natlehnplusnm n m)).
rewrite (dcpo_inf_chain_proj D f _ _ (natlehmplusnm n m)).
apply (pr12 (chain_proj D m (n + m) (natlehmplusnm n m))).
apply (pr222 (chain_ep_pair D n (n + m) (natlehnplusnm n m))).
Defined.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment