From Stdlib Require Import List Program Lia ConstructiveEpsilon Arith Classes.Morphisms.
From mathcomp Require Import zify.
From Equations Require Import Equations.
Require Import extra_principles Util continuity_zoo_Prop partial embed_nat Common.
Import EmbedNatNotations PartialTactics ListNotations.
Section PartialZoo.
Context `{Partiality : partiality}.
Definition modulus_at [Q A R : Type] (F : (Q -> part A) -> part R)
(f : Q -> part A) (l : list Q) :=
ter (F f) ->
forall (g : Q -> part A), Forall (fun q => equiv (f q) (g q)) l ->
equiv (F f) (F g).
Definition ex_modulus_cont [Q A R : Type] (F : (Q -> part A) -> part R) :=
forall (f : Q -> part A), ter (F f) -> exists (l : list Q), modulus_at F f l.
Definition modulus [Q A R : Type] (F : (Q -> part A) -> part R)
(M : (Q -> part A) -> part (list Q)) :=
forall (f : Q -> part A), ter (F f) ->
exists (l : list Q), hasvalue (M f) l /\
modulus_at F f l.
Definition modulus' [Q A R : Type] (F : (Q -> part A) -> part R)
(M : (Q -> part A) -> part (list Q)) :=
modulus F M /\ forall (f : Q -> part A), ter (M f) -> ter (F f).
Definition strictify_modulus [Q A R : Type] (F : (Q -> part A) -> part R)
(M : (Q -> part A) -> part (list Q)) : (Q -> part A) -> part (list Q) :=
fun f => bind (F f) (fun _ => M f).
Lemma strictify_modulus_ter [Q A R : Type] (F : (Q -> part A) -> part R)
(M : (Q -> part A) -> part (list Q)) : modulus F M ->
forall (f : Q -> part A), ter (F f) <-> ter (strictify_modulus F M f).
Proof.
intros HM f.
split; intros Hf.
- unfold strictify_modulus.
destruct (HM f Hf) as (l & Hl & Hl').
exists l.
destruct Hf as (x & Hx).
psimpl.
- destruct Hf as (l & Hl).
unfold strictify_modulus in Hl.
psimpl.
eexists; eassumption.
Qed.
Lemma strictify_modulus_hasvalue [Q A R : Type] (F : (Q -> part A) -> part R)
(M : (Q -> part A) -> part (list Q)) :
forall (f : Q -> part A) (l : list Q),
hasvalue (M f) l -> ter (F f) -> hasvalue (strictify_modulus F M f) l.
Proof.
intros f l HM (a & Ha).
unfold strictify_modulus.
psimpl.
Qed.
Lemma strictify_modulus_hasvalue' [Q A R : Type] (F : (Q -> part A) -> part R)
(M : (Q -> part A) -> part (list Q)) :
forall (f : Q -> part A) (l : list Q),
hasvalue (strictify_modulus F M f) l -> hasvalue (M f) l.
Proof.
intros f l HM.
unfold strictify_modulus in HM.
psimpl.
Qed.
Lemma strictify_modulus_ter' [Q A R : Type] (F : (Q -> part A) -> part R)
(M : (Q -> part A) -> part (list Q)) : modulus F M ->
forall (f : Q -> part A), ter (strictify_modulus F M f) -> ter (M f).
Proof.
intros HM f (l & Hl).
exists l.
eapply strictify_modulus_hasvalue'.
eassumption.
Qed.
Lemma strict_modulus [Q A R : Type] (F : (Q -> part A) -> part R)
(M : (Q -> part A) -> part (list Q)) : modulus F M -> modulus' F (strictify_modulus F M).
Proof.
intros HM.
split.
- intros f Hf.
pose proof (Hf' := Hf).
rewrite strictify_modulus_ter with (1 := HM) in Hf'.
destruct Hf' as (l & Hl).
exists l.
split; unfold modulus in HM; try assumption.
apply strictify_modulus_hasvalue' in Hl.
destruct (HM f Hf) as (l' & Hl' & HFl').
assert (E : l = l') by (eapply hasvalue_det; eassumption).
destruct E; assumption.
- apply strictify_modulus_ter.
assumption.
Qed.
Lemma strictify_modulus_at [Q A R : Type] (F : (Q -> part A) -> part R)
(M : (Q -> part A) -> part (list Q)) : modulus F M ->
forall (f : Q -> part A) (l l' : list Q),
modulus_at M f l ->
hasvalue (M f) l' ->
modulus_at (strictify_modulus F M) f (l ++ l').
Proof.
intros HM f l l' Hl Hl' Hter g Hg.
pose proof (Hter' := Hter).
rewrite <- strictify_modulus_ter with (1 := HM) in Hter'.
assert (HMf : ter (M f)) by
(eapply strictify_modulus_ter'; eassumption).
assert (Hg1 : Forall (fun q : Q => equiv (A:=A) (f q) (g q)) l)
by (eapply Forall_app_l; eassumption).
assert (Hg2 : Forall (fun q : Q => equiv (A:=A) (f q) (g q)) l')
by (eapply Forall_app_r; eassumption).
specialize (Hl HMf g Hg1).
destruct (HM _ Hter') as (a & Ha & Ha').
assert (a = l') by (eapply hasvalue_det; eassumption).
subst.
specialize (Ha' Hter' g Hg2).
destruct Hter'.
unfold strictify_modulus.
intros v.
specialize (Hl v).
psimpl.
all: try firstorder.
specialize (Ha' x).
rewrite Ha' in H.
eassumption.
Qed.
Definition comp_modulus_cont [Q A R : Type] (F : (Q -> part A) -> part R) :=
exists (M : (Q -> part A) -> part (list Q)), modulus F M.
Definition comp_modulus'_cont [Q A R : Type] (F : (Q -> part A) -> part R) :=
exists (M : (Q -> part A) -> part (list Q)), modulus' F M.
Lemma comp_modulus_equiv [Q A R : Type] (F : (Q -> part A) -> part R) :
comp_modulus_cont F <-> comp_modulus'_cont F.
Proof.
split.
2: firstorder.
intros (M & HM).
eexists.
apply strict_modulus.
eassumption.
Qed.
Definition continuous_modulus_cont [Q A R : Type] (F : (Q -> part A) -> part R) :=
exists (M : (Q -> part A) -> part (list Q)), modulus F M /\ ex_modulus_cont M.
Definition continuous_modulus'_cont [Q A R : Type] (F : (Q -> part A) -> part R) :=
exists (M : (Q -> part A) -> part (list Q)), modulus' F M /\ ex_modulus_cont M.
Lemma continuous_modulus_equiv [Q A R : Type] (F : (Q -> part A) -> part R) :
continuous_modulus_cont F <-> continuous_modulus'_cont F.
Proof.
split.
2: firstorder.
intros (M & HF & HM).
exists (strictify_modulus F M).
split.
- apply strict_modulus.
assumption.
- intros f (a & Ha).
assert (Hf : ter (M f)). {
eapply strictify_modulus_ter'; try eassumption.
eexists; eassumption.
}
specialize (HM f Hf).
destruct HM as (l & Hl).
specialize Hl.
destruct Hf as (l' & Hl').
exists (l ++ l').
apply strictify_modulus_at; assumption.
Qed.
Definition self_modulus_cont [Q A R : Type] (F : (Q -> part A) -> part R) :=
exists (M : (Q -> part A) -> part (list Q)), modulus F M /\ modulus M M.
Definition self_modulus'_cont [Q A R : Type] (F : (Q -> part A) -> part R) :=
exists (M : (Q -> part A) -> part (list Q)), modulus' F M /\ modulus' M M.
Lemma double_modulus_at [Q A R : Type] (F : (Q -> part A) -> part R)
(f : Q -> part A) (l : list Q) :
modulus_at F f (l ++ l) -> modulus_at F f l.
Proof.
intros H Hf g Hg.
assert (Hg' : Forall (fun q : Q => equiv (A:=A) (f q) (g q)) (l ++ l))
by (apply Forall_app; assumption).
specialize (H Hf g Hg').
assumption.
Qed.
Lemma self_modulus_equiv [Q A R : Type] (F : (Q -> part A) -> part R) :
self_modulus_cont F <-> self_modulus'_cont F.
Proof.
split.
2: firstorder.
intros (M & HF & HM).
exists (strictify_modulus F M).
split; [
apply strict_modulus;
assumption
| ].
split.
2: firstorder.
intros f Hf.
pose proof (Hf' := Hf).
destruct Hf' as (l & Hl).
exists l.
split; try assumption.
apply double_modulus_at.
assert (M f =! l) by (eapply strictify_modulus_hasvalue'; eassumption).
apply strictify_modulus_at; try assumption.
assert (Hf' : ter (M f))
by (eapply strictify_modulus_ter'; [eapply HF | eassumption]).
specialize (HM f Hf').
destruct HM as (l' & Hl' & HMl').
assert (l' = l) by (eapply hasvalue_det; eassumption).
subst.
assumption.
Qed.
Lemma self_modulus_cont_to_continuous_modulus_cont [Q A R : Type]
(F : (Q -> part A) -> part R) :
self_modulus_cont F -> continuous_modulus_cont F.
Proof.
intros (M & HF & HM).
unfold continuous_modulus_cont.
exists M.
split; try assumption.
unfold ex_modulus_cont.
intros f Hf.
specialize (HM f Hf).
firstorder.
Qed.
Lemma continuous_modulus_cont_to_have_modulus_fn [Q A R : Type]
(F : (Q -> part A) -> part R) :
continuous_modulus_cont F -> exists M, modulus F M.
Proof.
firstorder.
Qed.
Lemma modulus_fn_to_have_modulus [Q A R : Type] (F : (Q -> part A) -> part R) :
(exists M, modulus F M) -> ex_modulus_cont F.
Proof.
intros (M & HM) f Hf.
specialize (HM f Hf) as (l & _ & Hl).
eauto.
Qed.
Definition por (p1 p2 : part bool) : part bool :=
bind (par p1 p2) (fun r => match r with
| inl true => ret true
| inl false => p2
| inr true => ret true
| inr false => p1
end).
Lemma por_false : forall (p1 p2 : part bool),
por p1 p2 =! false <->
p1 =! false /\ p2 =! false.
Proof.
intros p1 p2; unfold por; split.
- intros H.
psimpl.
destruct x;
(apply par_hasvalue1 in H || apply par_hasvalue2 in H);
destruct b;
(apply ret_hasvalue_inv in H0; inversion H0) ||
(split; auto).
- intros (H1 & H2).
unfold par.
rewrite equiv_bind_mult.
eset (mu_tot (fun n => _)).
assert (ter p). {
rewrite seval_hasvalue in H1, H2.
destruct H1 as (n & Hn), H2 as (m & Hm).
apply mu_tot_ter with (n := n).
rewrite Hn.
reflexivity.
}
destruct H as (k & Hk).
rewrite bind_hasvalue.
exists k; split; auto.
unfold p in Hk.
rewrite mu_tot_hasvalue in Hk.
destruct Hk as (Hk1 & Hk2).
destruct (seval p1 k) as [ [] | ] eqn:E.
+ assert (Hc : false = true). {
eapply hasvalue_det.
1: apply H1.
rewrite seval_hasvalue.
exists k; auto.
}
inversion Hc.
+ psimpl.
+ destruct (seval p2 k) as [ [] | ] eqn:E'; psimpl.
assert (Hc : false = true). {
eapply hasvalue_det.
1: apply H2.
rewrite seval_hasvalue.
exists k; auto.
}
inversion Hc.
Qed.
Lemma por_true : forall (p1 p2 : part bool),
por p1 p2 =! true <-> (p1 =! true \/ p2 =! true).
Proof.
intros p1 p2.
unfold por; split.
- intros H.
psimpl.
destruct x;
(apply par_hasvalue1 in H || apply par_hasvalue2 in H);
destruct b; auto.
- intros H.
assert (H' : ter p1 \/ ter p2)
by (unfold ter; firstorder);
destruct (par_hasvalue3 H') as (r & Hr).
rewrite (bind_hasvalue_given _ _ Hr).
destruct r as [[]|[]]; psimpl;
[apply par_hasvalue1 in Hr | apply par_hasvalue2 in Hr];
destruct H; auto;
assert (Hc : true = false) by (eapply hasvalue_det; eassumption);
inversion Hc.
Qed.
#[global]
Add Parametric Morphism : por
with signature @equiv _ bool
==> @equiv _ bool
==> @equiv _ bool
as por_morph.
Proof.
intros p1 p2 Hp q1 q2 Hq.
intros v.
destruct v.
- split; repeat rewrite por_true; rewrite Hp, Hq; auto.
- split; repeat rewrite por_false; rewrite Hp, Hq; auto.
Qed.
(* If we write exists (r : R), F f =! r /\ F g =! r, we force ter (M f) -> ter (F f) *)
(* But we can always suppose that it is the case, as shown below *)
Definition weak_modulus [Q A R : Type] (F : (Q -> part A) -> part R) (M : (Q -> part A) -> part (list Q)) : Prop :=
forall (f : Q -> part A), (ter (F f) -> ter (M f)) /\
forall (l : list Q), M f =! l -> forall (g : Q -> part A),
Forall (fun q => exists v, f q =! v /\ g q =! v) l ->
forall (r : R), F f =! r -> F g =! r.
Definition ex_mod_continuous_weak [Q A R : Type] (F : (Q -> part A) -> part R) :=
forall (f : Q -> part A) (r : R), F f =! r ->
exists (l : list Q),
forall (g : Q -> part A),
Forall (fun q => exists v, f q =! v /\ g q =! v) l ->
F g =! r.
Definition continuous_mod_weak_continuous [Q A R : Type] (F : (Q -> part A) -> part R) :=
exists (M : (Q -> part A) -> part (list Q)), weak_modulus F M /\ ex_mod_continuous_weak M.
Definition self_mod_weak_continuous [Q A R : Type] (F : (Q -> part A) -> part R) :=
exists (M : (Q -> part A) -> part (list Q)), weak_modulus F M /\ weak_modulus M M.
Lemma modulus_to_weak_modulus [Q A R : Type] : forall (F : (Q -> part A) -> part R) (M : (Q -> part A) -> part (list Q)),
modulus F M -> weak_modulus F M.
Proof.
intros F M H.
intros f.
specialize (H f).
split.
- intros Hf.
apply H in Hf as (l & Hl & _).
eexists; eauto.
- intros l Hl g Hg r Hr.
specialize (H ltac:(eexists; eauto)) as (l' & Hl' & Hf).
assert (l' = l) by (eapply hasvalue_det; eauto); subst.
specialize (Hf ltac:(eexists; eauto) g).
apply Hf; eauto.
clear Hl' Hl Hf.
induction Hg as [| a l Hl IHl ]; constructor; auto.
destruct Hl as (? & ? & ?); eapply equiv_hasvalue; eauto.
Qed.
Lemma ex_mod_to_ex_mod_weak [Q A R : Type] :
forall (F : (Q -> part A) -> part R), ex_modulus_cont F -> ex_mod_continuous_weak F.
Proof.
intros F HF.
intros f r Hr.
specialize (HF f ltac:(eexists; eauto)) as (l & Hl).
specialize (Hl ltac:(eexists; eauto)).
exists l.
intros g Hg.
apply Hl; eauto.
clear Hl; induction Hg as [| a l Hl IHl ]; constructor; eauto.
destruct Hl as (? & ? & ?); eapply equiv_hasvalue; eauto.
Qed.
Lemma continuous_mod_to_continuous_mod_weak [Q A R : Type] :
forall (F : (Q -> part A) -> part R), continuous_modulus_cont F -> continuous_mod_weak_continuous F.
Proof.
intros F (M & HF & HM).
exists M;
split.
- apply modulus_to_weak_modulus; auto.
- apply ex_mod_to_ex_mod_weak; auto.
Qed.
Lemma self_mod_to_self_mod_weak [Q A R : Type] :
forall (F : (Q -> part A) -> part R), self_modulus_cont F -> self_mod_weak_continuous F.
Proof.
intros F (M & HF & HM).
exists M;
split.
- apply modulus_to_weak_modulus; auto.
- apply modulus_to_weak_modulus; auto.
Qed.
Definition weak_modulus' [Q A R : Type] (F : (Q -> part A) -> part R) (M : (Q -> part A) -> part (list Q)) : Prop :=
forall (f : Q -> part A), (ter (F f) <-> ter (M f)) /\
forall (l : list Q), M f =! l -> forall (g : Q -> part A),
Forall (fun q => exists v, f q =! v /\ g q =! v) l ->
forall (r : R), F f =! r -> F g =! r.
Definition continuous_mod_weak_continuous' [Q A R : Type] (F : (Q -> part A) -> part R) :=
exists (M : (Q -> part A) -> part (list Q)), weak_modulus' F M /\ ex_mod_continuous_weak M.
Definition self_mod_weak_continuous' [Q A R : Type] (F : (Q -> part A) -> part R) :=
exists (M : (Q -> part A) -> part (list Q)), weak_modulus' F M /\ weak_modulus' M M.
Lemma strictify_weak_modulus [Q A R : Type] (F : (Q -> part A) -> part R) (M : (Q -> part A) -> part (list Q)) :
weak_modulus F M -> weak_modulus' F (strictify_modulus F M).
Proof.
intros HM.
intros f.
specialize (HM f) as (Hf' & Hf).
split.
- split.
+ intros Hter.
pose proof Hter as (r & Hr).
apply Hf' in Hter as (l & Hl).
eexists; psimpl.
+ intros (r & Hr).
unfold strictify_modulus in Hr.
psimpl; eexists; psimpl.
- intros l Hl.
unfold strictify_modulus in Hl.
psimpl.
Qed.
Lemma strictify_continuous_mod_weak [Q A R : Type] :
forall (F : (Q -> part A) -> part R),
continuous_mod_weak_continuous F <-> continuous_mod_weak_continuous' F.
Proof.
intros F; split; intros (M & HF & HM).
2: firstorder.
exists (strictify_modulus F M); split.
- apply strictify_weak_modulus; auto.
- intros f r Hr.
unfold strictify_modulus in Hr |- *.
apply bind_hasvalue in Hr as (? & ? & ?).
specialize (HM f r H0) as (l & Hl).
exists (r ++ l).
intros g Hg.
psimpl.
+ specialize (HF f) as (_ & Hf).
eapply Hf; eauto.
eapply Forall_app_l; eauto.
+ apply Hl.
eapply Forall_app_r; eauto.
Qed.
Lemma strictify_self_mod_weak [Q A R : Type] :
forall (F : (Q -> part A) -> part R),
self_mod_weak_continuous F <-> self_mod_weak_continuous' F.
Proof.
intros F; split; intros (M & HF & HM).
2: firstorder.
exists (strictify_modulus F M); split.
- apply strictify_weak_modulus; auto.
- intros f.
split; auto.
intros l Hl g Hg r Hr.
unfold strictify_modulus in *.
apply bind_hasvalue in Hl as (? & ? & ?).
apply bind_hasvalue in Hr as (? & ? & ?).
assert (x0 = x) by (eapply hasvalue_det; eauto); subst.
assert (r = l) by (eapply hasvalue_det; eauto); subst.
assert (F g =! x). {
specialize (HF f) as (_ & Hf).
eapply Hf; eauto.
}
assert (M g =! l). {
specialize (HM f) as (_ & Hf).
eapply Hf; eauto.
}
psimpl.
Qed.
Definition strong_modulus [Q A R : Type] (F : (Q -> part A) -> part R) (M : (Q -> part A) -> part (list Q)) :=
forall (f : Q -> part A) (r : R), F f =! r ->
exists (l : list Q), M f =! l /\
Forall (fun q => ter (f q)) l /\ forall (g : Q -> part A),
Forall (fun q => equiv (f q) (g q)) l -> F g =! r.
Definition ex_strong_modulus [Q A R : Type] (F : (Q -> part A) -> part R) :=
forall (f : Q -> part A) (r : R), F f =! r ->
exists (l : list Q),
Forall (fun q => ter (f q)) l /\ forall (g : Q -> part A),
Forall (fun q => equiv (f q) (g q)) l -> F g =! r.
Definition strong_modulus_cont [Q A R : Type] (F : (Q -> part A) -> part R) :=
exists (M : (Q -> part A) -> part (list Q)), strong_modulus F M.
Definition strong_cont_modulus_cont [Q A R : Type] (F : (Q -> part A) -> part R) :=
exists (M : (Q -> part A) -> part (list Q)), strong_modulus F M /\ strong_modulus_cont M.
Definition strong_self_modulus_cont [Q A R : Type] (F : (Q -> part A) -> part R) :=
exists (M : (Q -> part A) -> part (list Q)), strong_modulus F M /\ strong_modulus M M.
Definition monotonic_modulus [Q A R : Type] (F : (Q -> part A) -> part R) (M : (Q -> part A) -> part (list Q)) :=
forall (f : Q -> part A) (r : R), F f =! r ->
exists (l : list Q), M f =! l /\ forall (g : Q -> part A),
Forall (fun q => forall (a : A), f q =! a -> g q =! a) l ->
F g =! r.
Definition ex_monotonic_modulus [Q A R : Type] (F : (Q -> part A) -> part R) :=
forall (f : Q -> part A) (r : R), F f =! r ->
exists (l : list Q), forall (g : Q -> part A),
Forall (fun q => forall (a : A), f q =! a -> g q =! a) l -> F g =! r.
Definition monotonic_modulus_cont [Q A R : Type] (F : (Q -> part A) -> part R) :=
exists (M : (Q -> part A) -> part (list Q)), monotonic_modulus F M.
Definition monotonic_cont_modulus_cont [Q A R : Type] (F : (Q -> part A) -> part R) :=
exists (M : (Q -> part A) -> part (list Q)), monotonic_modulus F M /\ monotonic_modulus_cont M.
Definition monotonic_self_modulus_cont [Q A R : Type] (F : (Q -> part A) -> part R) :=
exists (M : (Q -> part A) -> part (list Q)), monotonic_modulus F M /\ monotonic_modulus M M.
Lemma ex_strong_mod_to_ex_monotonic_mod [Q A R : Type] :
forall (F : (Q -> part A) -> part R), ex_strong_modulus F -> ex_monotonic_modulus F.
Proof.
intros F HF f r Hr.
specialize (HF f r Hr) as (l & Hl & Hf).
exists l.
intros g Hg.
apply Hf.
clear Hf.
induction Hg as [|a l Ha HL' IHl]; auto.
inversion Hl; subst.
destruct H1.
constructor; auto.
eapply equiv_hasvalue; eauto.
Qed.
Lemma strong_modulus_to_monotonic_modulus [Q A R : Type] :
forall (F : (Q -> part A) -> part R) (M : (Q -> part A) -> part (list Q)),
strong_modulus F M -> monotonic_modulus F M.
Proof.
intros F M HM f r Hr.
specialize (HM f r Hr) as (l & HM & Hl' & Hl).
exists l; split; auto.
intros g Hg.
apply Hl.
clear HM Hl.
induction Hg as [|q l Hq IHl]; constructor; inversion Hl'; subst; eauto.
destruct H1.
eapply equiv_hasvalue; eauto.
Qed.
Lemma ex_monotonic_mod_to_ex_mod [Q A R : Type] :
forall (F : (Q -> part A) -> part R),
ex_monotonic_modulus F -> ex_modulus_cont F.
Proof.
intros F HF f (r & Hr).
specialize (HF f r Hr) as (l & Hl).
exists l.
intros _ g Hg.
eapply equiv_hasvalue; eauto.
apply Hl.
clear Hl.
induction Hg as [|a l Ha Hl IHl]; constructor; auto.
apply Ha.
Qed.
Lemma monotonic_modulus_to_modulus [Q A R : Type] :
forall (F : (Q -> part A) -> part R) (M : (Q -> part A) -> part (list Q)),
monotonic_modulus F M -> modulus F M.
Proof.
intros F M HM f (r & Hr).
specialize (HM f r Hr) as (l & Hl' & Hl).
exists l; split; auto.
intros _ g Hg.
eapply equiv_hasvalue; eauto.
apply Hl.
clear Hl Hl'.
induction Hg as [|a l Ha IHl]; constructor; eauto.
apply Ha.
Qed.
Lemma lpo_monotonic_mod_is_strong_mod [Q A R : Type] :
(forall (p : part A), {ter p} + {~ter p}) ->
forall (F : (Q -> part A) -> part R),
ex_monotonic_modulus F -> ex_strong_modulus F.
Proof.
intros LPO F HF f r Hr.
specialize (HF f r Hr) as (l & Hl).
exists (filter (fun q => if LPO (f q) then true else false) l).
split.
- rewrite Forall_forall.
intros q (_ & Hq)%filter_In.
now destruct (LPO (f q)).
- intros g Hg.
rewrite Forall_forall in Hg.
apply Hl.
rewrite Forall_forall.
intros q Hq a Ha.
apply Hg; eauto.
apply filter_In.
split; eauto.
destruct (LPO (f q)) as [_ | Hc]; eauto.
contradict Hc.
eexists; eauto.
Qed.
Lemma lpo_monotonic_mod_fn_is_strong_mod_fn [Q A R : Type] :
(forall (p : part A), {ter p} + {~ter p}) ->
forall (F : (Q -> part A) -> part R),
monotonic_modulus_cont F -> strong_modulus_cont F.
Proof.
intros LPO F (M & HM).
set (M' f := bind (M f) (fun l => ret (filter (fun q => if LPO (f q) then true else false) l))).
exists M'.
intros f r Hr.
apply HM in Hr as (l & Hl & Hr).
eexists; split.
1: unfold M'; psimpl.
split.
- rewrite Forall_forall.
intros q (_ & Hq)%filter_In.
now destruct (LPO (f q)).
- intros g Hg.
rewrite Forall_forall in Hg.
apply Hr.
rewrite Forall_forall.
intros q Hq a Ha.
apply Hg; eauto.
apply filter_In.
split.
1:eauto.
destruct (LPO (f q)) as [_ | Hc].
1:eauto.
contradict Hc.
eexists; eauto.
Qed.
Definition monotonic_seq [A : Type] (u : nat -> part A) :=
forall n m, n <= m -> forall v, u n =! v -> u m =! v.
Definition sup [A : Type] (u : nat -> part A) (p : part A) :=
forall v, p =! v <-> exists n, u n =! v.
Definition omega_cpo (A : Type) : forall (u : nat -> part A),
monotonic_seq u ->
{ p : part A & sup u p }.
Proof.
intros u Hu.
set (p := mkpart (fun k => let (n, m) := unembed k in seval (u n) m)).
exists p.
intros v.
split; intros Hv.
- apply mkpart_hasvalue1 in Hv.
destruct Hv as (k & Hk).
destruct (unembed k) as (n & m).
exists n.
rewrite seval_hasvalue.
exists m; eauto.
- destruct Hv as (n & Hn).
rewrite seval_hasvalue in Hn.
destruct Hn as (m & Hk).
apply mkpart_hasvalue2 with (n := embed (n, m)).
+ intros k1 k2 a1 a2 Ha1 Ha2.
destruct (unembed k1) as (n1 & m1), (unembed k2) as (n2 & m2).
assert (H1 : u n1 =! a1) by (rewrite seval_hasvalue; eauto).
assert (H2 : u n2 =! a2) by (rewrite seval_hasvalue; eauto).
destruct (Nat.le_ge_cases n1 n2) as [H | H]; specialize (Hu _ _ H).
* apply (Hu a1) in H1.
eapply hasvalue_det; eauto.
* apply (Hu a2) in H2.
eapply hasvalue_det; eauto.
+ simpl.
rewrite embedP.
assumption.
Defined.
Definition cpo_cont [Q A R : Type] (F : (Q -> part A) -> part R) :=
forall (f : nat -> Q -> part A),
(forall (q : Q), monotonic_seq (fun n => f n q)) ->
forall (f' : Q -> part A),
(forall (q : Q), sup (fun n => f n q) (f' q)) ->
sup (fun n => F (f n)) (F f').
(* Si S est un ensemble dirigé infini dans un omega-cpo de la forme A -> lift B,
alors S a un sup. De plus, si f est une fonction de ce cpo vers un autre omega-cpo de la forme lift C,
alors f(S) a un sup, et sup(f(S)) = f(sup S).
Hmmm. Si c'est infini je peux extraire *une* suite. Pas nécessairement une qui tend vers le sup.
Typiquement, dans omega * 2 + 1, avec une suite qui tend vers omega au lieu de omega * 2.
Et je ne peux pas disjoncter selon si un des éléments de S est pas undef ou non.*)
Definition extensional [Q A R : Type] (F : (Q -> part A) -> part R) :=
forall (f g : Q -> part A),
pointwise_relation Q (equiv (A := A)) f g ->
equiv (F f) (F g).
Lemma modulus_cont_to_extensional [Q A R : Type] (F : (Q -> part A) -> part R) :
ex_modulus_cont F -> extensional F.
Proof.
intros Hmod.
intros f g Hfg.
pose proof (Hmod f) as Hf.
pose proof (Hmod g) as Hg.
assert (H: forall l, Forall (fun q => equiv (f q) (g q)) l). {
intros l.
induction l; constructor; eauto; try now rewrite Hfg.
}
intros v; split; intros Hv.
- destruct (Hf ltac:(eexists; eauto)) as (l & Hl).
specialize (Hl ltac:(eexists; eauto) g (H l)).
apply Hl; eauto.
- destruct (Hg ltac:(eexists; eauto)) as (l & Hl).
assert (H' : forall q, (equiv (f q) (g q)) <-> equiv (g q) (f q))
by (intros; split; intros; symmetry; assumption).
setoid_rewrite H' in H.
specialize (Hl ltac:(eexists; eauto) f (H l)).
apply Hl; eauto.
Qed.
Goal forall (Q A : Type) (f g : Q -> part A) (l : list Q),
Forall (fun q => equiv (f q) (g q)) l /\ Forall (fun q => ter (f q)) l
<-> Forall (fun q => exists v, f q =! v /\ g q =! v) l.
Proof.
intros Q A f g l.
split.
- intros (Hl1 & Hl2). revert Hl2.
induction Hl1 as [| a l1 Ha Hl1 IHl1 ]; intros Hl2; auto.
inversion Hl2; subst.
destruct H1 as (v & Hv).
constructor; firstorder.
- intros Hl.
induction Hl as [| a l (v & Hv1 & Hv2) Hl (IHl & IHl2) ]; auto.
split; constructor; try firstorder.
eapply equiv_hasvalue; eauto.
Qed.
Definition monotonic [Q A R : Type] (F : (Q -> part A) -> part R) :=
forall (f g : Q -> part A),
(forall (q : Q) (a : A), f q =! a -> g q =! a) ->
forall (r : R), F f =! r -> F g =! r.
Lemma cpo_cont_to_monotonic [Q A R : Type] (F : (Q -> part A) -> part R) :
cpo_cont F -> monotonic F.
Proof.
intros HF f g Hfg r Hr.
set (h := fun n q => match n with 0 => f q | S _ => g q end).
assert (Hh : forall (q : Q), monotonic_seq (fun n => h n q)). {
intros q [|n];
intros [|m] Hm v Hv; unfold h in Hv |- *;
inversion Hm; subst;
try assumption; try apply Hfg; try assumption.
}
assert (Hh' : forall (q : Q), sup (fun n => h n q) (g q)). {
intros q.
intros v; split; intros Hv.
- exists 2.
assumption.
- destruct Hv as ([|n] & Hn).
+ apply Hfg.
assumption.
+ assumption.
}
specialize (HF h Hh g Hh' r).
apply HF; exists 0; eauto.
Qed.
(* il faut faire plus compliqué si on force la terminaison sur le module *)
Definition approx [A : Type] (f : nat -> part A) : nat -> nat -> part A :=
fun n m => if m <=? n then f m else undef.
Lemma approx_monotonic_seq [A : Type] : forall (f : nat -> part A) (q : nat),
monotonic_seq (fun n => approx f n q).
Proof.
intros f q n m Hnm r Hr.
unfold approx in *.
destruct (q <=? n) eqn:E; psimpl.
apply leb_complete in E.
rewrite leb_correct; try lia.
psimpl.
Qed.
Lemma approx_sup [A : Type] : forall (f : nat -> part A) (q : nat),
sup (fun n => approx f n q) (f q).
Proof.
intros f q a.
unfold approx in *; split.
+ intros Ha.
exists q.
rewrite leb_correct; try lia.
psimpl.
+ intros (n & Hn).
destruct (q <=? n); psimpl.
Qed.
Definition modulus_of_cpo_nat [A R : Type] (F : (nat -> part A) -> part R) : cpo_cont F ->
(nat -> part A) -> part (list nat).
Proof.
intros HF.
refine (fun f => bind (proof_ter (F f)) (fun Hter => ret _)).
specialize (HF (approx f) ltac:(apply approx_monotonic_seq) f ltac:(apply approx_sup)).
assert (Hf : hasvalue (F f) (eval Hter)) by apply eval_hasvalue.
apply HF in Hf.
assert (Hseval : exists k, let (n, m) := unembed k in
if seval (F (approx f n)) m then True else False
). {
destruct Hf as (n & Hn).
apply seval_hasvalue in Hn as (m & Hm).
exists (embed (n, m)).
rewrite embedP.
rewrite Hm.
auto.
}
apply constructive_indefinite_ground_description_nat in Hseval as (k & Hk). 2:{
intros k.
destruct (unembed k) eqn:E.
destruct (seval _ _); auto.
}
destruct (unembed k) eqn:E.
exact (tabulate id 0 (S n)).
Defined.
Lemma modulus_of_cpo_nat_is_modulus [A R : Type] (F : (nat -> part A) -> part R) :
forall (HF : cpo_cont F), monotonic_modulus F (modulus_of_cpo_nat F HF).
Proof.
intros HF f r Hr.
assert (exists (n : nat), modulus_of_cpo_nat F HF f =! tabulate id 0 (S n) /\ ter (F (approx f n))) as (n & Hn & Hn'). {
assert (ter (proof_ter (F f))) as (Hter & ?) by (apply proof_ter_spec; eexists; eauto).
assert (ter (modulus_of_cpo_nat F HF f)) as (l & Hl) by (eapply bind_ter; eauto; eexists; psimpl).
unfold modulus_of_cpo_nat in Hl |- *.
rewrite bind_hasvalue_given in Hl; eauto.
setoid_rewrite bind_hasvalue_given; eauto.
apply ret_hasvalue_inv in Hl.
setoid_rewrite <- ret_hasvalue_iff.
set (Q k := let (n, m) := unembed k in _ : Prop) in *.
set (Hdec k := _ : {Q k} + {~Q k}) in *.
set (HQ := match _ with ex_intro x H => _ end : exists k, Q k) in *.
set (c := constructive_indefinite_ground_description_nat Q Hdec HQ) in *.
destruct c as (k & Hk).
unfold Q in Hk.
destruct (unembed k) as (n & m) eqn:E.
exists n.
destruct (seval _ _) eqn:E'; try now inversion Hk.
split; auto.
eexists; apply seval_hasvalue; eauto.
}
eexists; split; eauto.
destruct Hn' as (r' & Hr').
assert (r' = r). {
eapply hasvalue_det.
2: eauto.
eapply (HF (approx f)); eauto.
- apply approx_monotonic_seq.
- apply approx_sup.
}
subst.
intros g Hg.
eapply equiv_hasvalue; eauto.
eapply cpo_cont_to_monotonic; try eassumption.
clear Hn Hr'.
induction n as [|n IHn]; intros q a Hq.
+ unfold approx in Hq.
destruct (q <=? 0) eqn:E; psimpl.
apply leb_complete in E.
inversion E; subst.
cbn in Hg.
inversion Hg; subst.
apply H1; eauto.
+ unfold approx in Hq.
destruct (q <=? S n) eqn:E; psimpl.
apply leb_complete in E.
rewrite tabulate_succ' in Hg; try lia.
inversion E; subst.
* apply Forall_app_r in Hg.
inversion Hg; subst.
apply H1; auto.
* apply Forall_app_l in Hg.
inversion Hg; subst.
apply IHn; eauto.
unfold approx.
rewrite leb_correct; eauto.
Qed.
Lemma ex_monotonic_mod_to_monotonic [Q A R : Type] :
forall (F : (Q -> part A) -> part R), ex_monotonic_modulus F -> monotonic F.
Proof.
intros F HF f g Hfg r Hr.
apply HF in Hr as (l & Hg).
apply Hg.
clear Hg.
induction l; eauto.
Qed.
Lemma ex_self_mod_to_cpo_cont [Q A R : Type] :
forall (F : (Q -> part A) -> part R),
ex_strong_modulus F -> cpo_cont F.
Proof.
intros F HF f Hf f' Hf' r.
split.
- intros (l & Hl & Hf'')%HF.
enough (exists n, forall m, n <= m -> Forall (fun q => equiv (f' q) (f m q)) l) as (n & Hn)
by (eexists; eapply Hf''; eauto).
clear Hf''.
induction Hl as [|q l (a & (m & Hm)%Hf') Hl (n & Hn)];
unshelve eauto; try now exact 0.
exists (max n m).
intros k Hk.
constructor.
1:eapply equiv_hasvalue; (eapply Hf' || eapply Hf in Hm);
eauto; try lia.
apply Hn; lia.
- intros (n & Hn).
eapply ex_monotonic_mod_to_monotonic; try eassumption.
1:apply ex_strong_mod_to_ex_monotonic_mod; firstorder.
intros q a Ha.
apply Hf'.
eauto.
Qed.
Lemma cpo_cont_to_monotonic_modulus_cont_nat [A R : Type] :
forall (F : (nat -> part A) -> part R), cpo_cont F -> monotonic_modulus_cont F.
Proof.
intros F HF.
exists (modulus_of_cpo_nat F HF).
apply modulus_of_cpo_nat_is_modulus.
Qed.
Definition lpo (A : Type) := forall (p : part A), {ter p} + {~ter p}.
Lemma lpo_cpo_cont_is_strong_mod_cont_nat [A R : Type] :
lpo A ->
forall (F : (nat -> part A) -> part R),
cpo_cont F <-> strong_modulus_cont F.
Proof.
intros LPO F.
split; intros HF.
- apply lpo_monotonic_mod_fn_is_strong_mod_fn; eauto.
apply cpo_cont_to_monotonic_modulus_cont_nat; eauto.
- apply ex_self_mod_to_cpo_cont.
firstorder.
Qed.
Lemma lpo_cpo_cont_is_monotonic_mod_cont_nat [A R : Type] :
lpo A ->
forall (F : (nat -> part A) -> part R),
cpo_cont F <-> monotonic_modulus_cont F.
Proof.
intros LPO F.
split; intros HF.
- now apply cpo_cont_to_monotonic_modulus_cont_nat.
- apply lpo_monotonic_mod_fn_is_strong_mod_fn in HF; eauto.
apply ex_self_mod_to_cpo_cont.
firstorder.
Qed.
Lemma monotonic_to_extensional [Q A R : Type] :
forall (F : (Q -> part A) -> part R), monotonic F -> extensional F.
Proof.
intros F HF.
assert (Hext : forall f g,
pointwise_relation Q (equiv (A := A)) f g ->
(forall q a, f q =! a -> g q =! a)
). {
intros f g Heq q a Ha.
now apply Heq.
}
intros f g Hfg.
pose proof Hfg as Hgf.
symmetry in Hgf.
split; intros H; eapply HF; eauto.
Qed.
Lemma lots_of_separation : exists (F : (bool -> part unit) -> part unit),
(monotonic_self_modulus_cont F) /\
(exists (M : (bool -> part unit) -> part (list bool)), monotonic_modulus F M /\ strong_modulus_cont M) /\
(exists (M : (bool -> part unit) -> part (list bool)), strong_modulus F M) /\
~(exists (M : (bool -> part unit) -> part (list bool)), strong_modulus F M /\ ex_monotonic_modulus M).
Proof.
set (F (f : bool -> part unit) := bind (par (f true) (f false)) (fun _ => ret ())).
exists F.
repeat split.
- exists (fun f => ret [ true ; false ]).
split.
+ intros f () (b & Hr & _)%bind_hasvalue.
eexists; split; psimpl.
intros g Hg.
inversion Hg; subst.
inversion H2; subst.
unfold F in *.
enough (ter (par (g true) (g false))) as (? & ?) by (rewrite bind_hasvalue_given; psimpl).
apply par_hasvalue3.
destruct b; [
apply par_hasvalue1 in Hr; apply H1 in Hr; left; eexists; eauto
| apply par_hasvalue2 in Hr; apply H3 in Hr; right; eexists; eauto
].
+ intros f l Hr%ret_hasvalue_iff.
exists l; split; subst; psimpl.
intros; psimpl.
- exists (fun f => ret [ true ; false ]).
split.
+ intros f () (b & Hr & _)%bind_hasvalue.
eexists; split; psimpl.
intros g Hg.
inversion Hg; subst.
inversion H2; subst.
unfold F in *.
enough (ter (par (g true) (g false))) as (? & ?) by (rewrite bind_hasvalue_given; psimpl).
apply par_hasvalue3.
destruct b; [
apply par_hasvalue1 in Hr; apply H1 in Hr; left; eexists; eauto
| apply par_hasvalue2 in Hr; apply H3 in Hr; right; eexists; eauto
].
+ exists (fun f => ret nil).
intros f l Hl%ret_hasvalue_iff; subst.
eexists; split; psimpl.
split; eauto.
intros g Hg; psimpl.
- set (M (f : bool -> part unit) := bind (par (f true) (f false))
(fun o => ret (match o with
| inl _ => [ true ]
| inr _ => [ false ]
end))). (* Je ne peux pas montrer que M est continue, quelle que soit le sens de continue ici *)
exists M.
intros f () (b & Hb & _)%bind_hasvalue.
unfold F, M.
eexists; split; [ rewrite bind_hasvalue_given; eauto; psimpl |].
destruct b; apply par_hasvalue1 in Hb || apply par_hasvalue2 in Hb;
(split; [repeat econstructor; eauto |]); intros g Hg; inversion Hg; subst;
enough (ter (par (g true) (g false))) as (? & ?)
by (rewrite bind_hasvalue_given; psimpl); apply par_hasvalue3;
[ left | right ]; eexists; apply H1; apply Hb.
- intros (M & HF & HM).
set (f1 (b : bool) := if b then ret () else undef).
set (f2 (b : bool) := if b then undef else ret ()).
set (f3 (b : bool) := @undef _ unit).
set (f4 (b : bool) := ret ()).
assert (F f1 =! ()) as (l1 & Hl1 & Hter1 & Hf1)%HF. {
unfold F.
eenough (ter (par (f1 true) (f1 false))) as (? & ?)
by (rewrite bind_hasvalue_given; psimpl).
apply par_hasvalue3; left; eexists; psimpl.
}
assert (F f2 =! ()) as (l2 & Hl2 & Hter2 & Hf2)%HF. {
unfold F.
eenough (ter (par (f2 true) (f2 false))) as (? & ?)
by (rewrite bind_hasvalue_given; psimpl).
apply par_hasvalue3; right; eexists; psimpl.
}
assert (Hter : ~ter (F f3)). {
intros (() & Hr).
unfold F, f3 in Hr.
psimpl.
destruct x; apply par_hasvalue1 in H || apply par_hasvalue2 in H; psimpl.
}
destruct l1 as [|[] l1]. {
apply Hter; eexists.
apply Hf1; auto.
} 2:{
inversion Hter1; subst.
destruct H1 as (? & ?); unfold f1 in *; psimpl.
}
destruct l2 as [|[] l2]. {
apply Hter; eexists.
apply Hf2; auto.
} 1:{
inversion Hter2; subst.
destruct H1 as (? & ?); unfold f2 in *; psimpl.
}
assert (HM' : monotonic M) by now apply ex_monotonic_mod_to_monotonic.
assert (forall q a, f1 q =! a -> f4 q =! a) by (unfold f4; intros _ () _; psimpl).
assert (forall q a, f2 q =! a -> f4 q =! a) by (unfold f4; intros _ () _; psimpl).
enough (true :: l1 = false :: l2) as [=];
eapply hasvalue_det; eapply HM'.
2,4: eauto.
1,2: eauto.
Qed.
Lemma ext_but_not_mono : lpo unit ->
exists (F : (bool -> part unit) -> part bool), ex_modulus_cont F /\ ~monotonic F.
Proof.
intros HLPO.
(* F f =! true si f true et f false terminent, =! false sinon *)
(* on peut aussi se demander : quid de "un seul parmi f true et f false termine" ? *)
set (F := fun (f : bool -> part unit) =>
match HLPO (f true), HLPO (f false) with
| left _, left _ => ret true
| _, _ => ret false
end
).
exists F.
split.
- intros f Hf.
exists [ true; false ].
intros _ g Hg.
inversion Hg; subst.
inversion H2; subst.
clear Hg H2 H4.
unfold F.
destruct (HLPO (f true)), (HLPO (f false)), (HLPO (g true)), (HLPO (g false));
eapply equiv_hasvalue; psimpl;
try (rewrite H1 in * |- ; contradiction);
try (rewrite H3 in * |- ; contradiction).
- intros Hfg.
set (f1 := fun (_ : bool) => undef (A := unit)).
set (f2 := fun (_ : bool) => ret ()).
assert (H1 : F f1 =! false). {
unfold F.
destruct (HLPO (f1 true)) as [(? & ?)|], (HLPO (f1 false)) as [(? & ?)|];
unfold f1 in *; try psimpl.
}
assert (H2 : F f2 =! true). {
unfold F.
destruct (HLPO (f2 true)) as [(? & ?)| H], (HLPO (f2 false)) as [(? & ?)| H'];
unfold f2 in *; try psimpl;
(contradict H || contradict H'); eexists; psimpl.
}
enough (true = false) as [=].
eapply hasvalue_det; eauto.
eapply Hfg with (f := f1); eauto.
intros q () _; psimpl.
Qed.
End PartialZoo.
From mathcomp Require Import zify.
From Equations Require Import Equations.
Require Import extra_principles Util continuity_zoo_Prop partial embed_nat Common.
Import EmbedNatNotations PartialTactics ListNotations.
Section PartialZoo.
Context `{Partiality : partiality}.
Definition modulus_at [Q A R : Type] (F : (Q -> part A) -> part R)
(f : Q -> part A) (l : list Q) :=
ter (F f) ->
forall (g : Q -> part A), Forall (fun q => equiv (f q) (g q)) l ->
equiv (F f) (F g).
Definition ex_modulus_cont [Q A R : Type] (F : (Q -> part A) -> part R) :=
forall (f : Q -> part A), ter (F f) -> exists (l : list Q), modulus_at F f l.
Definition modulus [Q A R : Type] (F : (Q -> part A) -> part R)
(M : (Q -> part A) -> part (list Q)) :=
forall (f : Q -> part A), ter (F f) ->
exists (l : list Q), hasvalue (M f) l /\
modulus_at F f l.
Definition modulus' [Q A R : Type] (F : (Q -> part A) -> part R)
(M : (Q -> part A) -> part (list Q)) :=
modulus F M /\ forall (f : Q -> part A), ter (M f) -> ter (F f).
Definition strictify_modulus [Q A R : Type] (F : (Q -> part A) -> part R)
(M : (Q -> part A) -> part (list Q)) : (Q -> part A) -> part (list Q) :=
fun f => bind (F f) (fun _ => M f).
Lemma strictify_modulus_ter [Q A R : Type] (F : (Q -> part A) -> part R)
(M : (Q -> part A) -> part (list Q)) : modulus F M ->
forall (f : Q -> part A), ter (F f) <-> ter (strictify_modulus F M f).
Proof.
intros HM f.
split; intros Hf.
- unfold strictify_modulus.
destruct (HM f Hf) as (l & Hl & Hl').
exists l.
destruct Hf as (x & Hx).
psimpl.
- destruct Hf as (l & Hl).
unfold strictify_modulus in Hl.
psimpl.
eexists; eassumption.
Qed.
Lemma strictify_modulus_hasvalue [Q A R : Type] (F : (Q -> part A) -> part R)
(M : (Q -> part A) -> part (list Q)) :
forall (f : Q -> part A) (l : list Q),
hasvalue (M f) l -> ter (F f) -> hasvalue (strictify_modulus F M f) l.
Proof.
intros f l HM (a & Ha).
unfold strictify_modulus.
psimpl.
Qed.
Lemma strictify_modulus_hasvalue' [Q A R : Type] (F : (Q -> part A) -> part R)
(M : (Q -> part A) -> part (list Q)) :
forall (f : Q -> part A) (l : list Q),
hasvalue (strictify_modulus F M f) l -> hasvalue (M f) l.
Proof.
intros f l HM.
unfold strictify_modulus in HM.
psimpl.
Qed.
Lemma strictify_modulus_ter' [Q A R : Type] (F : (Q -> part A) -> part R)
(M : (Q -> part A) -> part (list Q)) : modulus F M ->
forall (f : Q -> part A), ter (strictify_modulus F M f) -> ter (M f).
Proof.
intros HM f (l & Hl).
exists l.
eapply strictify_modulus_hasvalue'.
eassumption.
Qed.
Lemma strict_modulus [Q A R : Type] (F : (Q -> part A) -> part R)
(M : (Q -> part A) -> part (list Q)) : modulus F M -> modulus' F (strictify_modulus F M).
Proof.
intros HM.
split.
- intros f Hf.
pose proof (Hf' := Hf).
rewrite strictify_modulus_ter with (1 := HM) in Hf'.
destruct Hf' as (l & Hl).
exists l.
split; unfold modulus in HM; try assumption.
apply strictify_modulus_hasvalue' in Hl.
destruct (HM f Hf) as (l' & Hl' & HFl').
assert (E : l = l') by (eapply hasvalue_det; eassumption).
destruct E; assumption.
- apply strictify_modulus_ter.
assumption.
Qed.
Lemma strictify_modulus_at [Q A R : Type] (F : (Q -> part A) -> part R)
(M : (Q -> part A) -> part (list Q)) : modulus F M ->
forall (f : Q -> part A) (l l' : list Q),
modulus_at M f l ->
hasvalue (M f) l' ->
modulus_at (strictify_modulus F M) f (l ++ l').
Proof.
intros HM f l l' Hl Hl' Hter g Hg.
pose proof (Hter' := Hter).
rewrite <- strictify_modulus_ter with (1 := HM) in Hter'.
assert (HMf : ter (M f)) by
(eapply strictify_modulus_ter'; eassumption).
assert (Hg1 : Forall (fun q : Q => equiv (A:=A) (f q) (g q)) l)
by (eapply Forall_app_l; eassumption).
assert (Hg2 : Forall (fun q : Q => equiv (A:=A) (f q) (g q)) l')
by (eapply Forall_app_r; eassumption).
specialize (Hl HMf g Hg1).
destruct (HM _ Hter') as (a & Ha & Ha').
assert (a = l') by (eapply hasvalue_det; eassumption).
subst.
specialize (Ha' Hter' g Hg2).
destruct Hter'.
unfold strictify_modulus.
intros v.
specialize (Hl v).
psimpl.
all: try firstorder.
specialize (Ha' x).
rewrite Ha' in H.
eassumption.
Qed.
Definition comp_modulus_cont [Q A R : Type] (F : (Q -> part A) -> part R) :=
exists (M : (Q -> part A) -> part (list Q)), modulus F M.
Definition comp_modulus'_cont [Q A R : Type] (F : (Q -> part A) -> part R) :=
exists (M : (Q -> part A) -> part (list Q)), modulus' F M.
Lemma comp_modulus_equiv [Q A R : Type] (F : (Q -> part A) -> part R) :
comp_modulus_cont F <-> comp_modulus'_cont F.
Proof.
split.
2: firstorder.
intros (M & HM).
eexists.
apply strict_modulus.
eassumption.
Qed.
Definition continuous_modulus_cont [Q A R : Type] (F : (Q -> part A) -> part R) :=
exists (M : (Q -> part A) -> part (list Q)), modulus F M /\ ex_modulus_cont M.
Definition continuous_modulus'_cont [Q A R : Type] (F : (Q -> part A) -> part R) :=
exists (M : (Q -> part A) -> part (list Q)), modulus' F M /\ ex_modulus_cont M.
Lemma continuous_modulus_equiv [Q A R : Type] (F : (Q -> part A) -> part R) :
continuous_modulus_cont F <-> continuous_modulus'_cont F.
Proof.
split.
2: firstorder.
intros (M & HF & HM).
exists (strictify_modulus F M).
split.
- apply strict_modulus.
assumption.
- intros f (a & Ha).
assert (Hf : ter (M f)). {
eapply strictify_modulus_ter'; try eassumption.
eexists; eassumption.
}
specialize (HM f Hf).
destruct HM as (l & Hl).
specialize Hl.
destruct Hf as (l' & Hl').
exists (l ++ l').
apply strictify_modulus_at; assumption.
Qed.
Definition self_modulus_cont [Q A R : Type] (F : (Q -> part A) -> part R) :=
exists (M : (Q -> part A) -> part (list Q)), modulus F M /\ modulus M M.
Definition self_modulus'_cont [Q A R : Type] (F : (Q -> part A) -> part R) :=
exists (M : (Q -> part A) -> part (list Q)), modulus' F M /\ modulus' M M.
Lemma double_modulus_at [Q A R : Type] (F : (Q -> part A) -> part R)
(f : Q -> part A) (l : list Q) :
modulus_at F f (l ++ l) -> modulus_at F f l.
Proof.
intros H Hf g Hg.
assert (Hg' : Forall (fun q : Q => equiv (A:=A) (f q) (g q)) (l ++ l))
by (apply Forall_app; assumption).
specialize (H Hf g Hg').
assumption.
Qed.
Lemma self_modulus_equiv [Q A R : Type] (F : (Q -> part A) -> part R) :
self_modulus_cont F <-> self_modulus'_cont F.
Proof.
split.
2: firstorder.
intros (M & HF & HM).
exists (strictify_modulus F M).
split; [
apply strict_modulus;
assumption
| ].
split.
2: firstorder.
intros f Hf.
pose proof (Hf' := Hf).
destruct Hf' as (l & Hl).
exists l.
split; try assumption.
apply double_modulus_at.
assert (M f =! l) by (eapply strictify_modulus_hasvalue'; eassumption).
apply strictify_modulus_at; try assumption.
assert (Hf' : ter (M f))
by (eapply strictify_modulus_ter'; [eapply HF | eassumption]).
specialize (HM f Hf').
destruct HM as (l' & Hl' & HMl').
assert (l' = l) by (eapply hasvalue_det; eassumption).
subst.
assumption.
Qed.
Lemma self_modulus_cont_to_continuous_modulus_cont [Q A R : Type]
(F : (Q -> part A) -> part R) :
self_modulus_cont F -> continuous_modulus_cont F.
Proof.
intros (M & HF & HM).
unfold continuous_modulus_cont.
exists M.
split; try assumption.
unfold ex_modulus_cont.
intros f Hf.
specialize (HM f Hf).
firstorder.
Qed.
Lemma continuous_modulus_cont_to_have_modulus_fn [Q A R : Type]
(F : (Q -> part A) -> part R) :
continuous_modulus_cont F -> exists M, modulus F M.
Proof.
firstorder.
Qed.
Lemma modulus_fn_to_have_modulus [Q A R : Type] (F : (Q -> part A) -> part R) :
(exists M, modulus F M) -> ex_modulus_cont F.
Proof.
intros (M & HM) f Hf.
specialize (HM f Hf) as (l & _ & Hl).
eauto.
Qed.
Definition por (p1 p2 : part bool) : part bool :=
bind (par p1 p2) (fun r => match r with
| inl true => ret true
| inl false => p2
| inr true => ret true
| inr false => p1
end).
Lemma por_false : forall (p1 p2 : part bool),
por p1 p2 =! false <->
p1 =! false /\ p2 =! false.
Proof.
intros p1 p2; unfold por; split.
- intros H.
psimpl.
destruct x;
(apply par_hasvalue1 in H || apply par_hasvalue2 in H);
destruct b;
(apply ret_hasvalue_inv in H0; inversion H0) ||
(split; auto).
- intros (H1 & H2).
unfold par.
rewrite equiv_bind_mult.
eset (mu_tot (fun n => _)).
assert (ter p). {
rewrite seval_hasvalue in H1, H2.
destruct H1 as (n & Hn), H2 as (m & Hm).
apply mu_tot_ter with (n := n).
rewrite Hn.
reflexivity.
}
destruct H as (k & Hk).
rewrite bind_hasvalue.
exists k; split; auto.
unfold p in Hk.
rewrite mu_tot_hasvalue in Hk.
destruct Hk as (Hk1 & Hk2).
destruct (seval p1 k) as [ [] | ] eqn:E.
+ assert (Hc : false = true). {
eapply hasvalue_det.
1: apply H1.
rewrite seval_hasvalue.
exists k; auto.
}
inversion Hc.
+ psimpl.
+ destruct (seval p2 k) as [ [] | ] eqn:E'; psimpl.
assert (Hc : false = true). {
eapply hasvalue_det.
1: apply H2.
rewrite seval_hasvalue.
exists k; auto.
}
inversion Hc.
Qed.
Lemma por_true : forall (p1 p2 : part bool),
por p1 p2 =! true <-> (p1 =! true \/ p2 =! true).
Proof.
intros p1 p2.
unfold por; split.
- intros H.
psimpl.
destruct x;
(apply par_hasvalue1 in H || apply par_hasvalue2 in H);
destruct b; auto.
- intros H.
assert (H' : ter p1 \/ ter p2)
by (unfold ter; firstorder);
destruct (par_hasvalue3 H') as (r & Hr).
rewrite (bind_hasvalue_given _ _ Hr).
destruct r as [[]|[]]; psimpl;
[apply par_hasvalue1 in Hr | apply par_hasvalue2 in Hr];
destruct H; auto;
assert (Hc : true = false) by (eapply hasvalue_det; eassumption);
inversion Hc.
Qed.
#[global]
Add Parametric Morphism : por
with signature @equiv _ bool
==> @equiv _ bool
==> @equiv _ bool
as por_morph.
Proof.
intros p1 p2 Hp q1 q2 Hq.
intros v.
destruct v.
- split; repeat rewrite por_true; rewrite Hp, Hq; auto.
- split; repeat rewrite por_false; rewrite Hp, Hq; auto.
Qed.
(* If we write exists (r : R), F f =! r /\ F g =! r, we force ter (M f) -> ter (F f) *)
(* But we can always suppose that it is the case, as shown below *)
Definition weak_modulus [Q A R : Type] (F : (Q -> part A) -> part R) (M : (Q -> part A) -> part (list Q)) : Prop :=
forall (f : Q -> part A), (ter (F f) -> ter (M f)) /\
forall (l : list Q), M f =! l -> forall (g : Q -> part A),
Forall (fun q => exists v, f q =! v /\ g q =! v) l ->
forall (r : R), F f =! r -> F g =! r.
Definition ex_mod_continuous_weak [Q A R : Type] (F : (Q -> part A) -> part R) :=
forall (f : Q -> part A) (r : R), F f =! r ->
exists (l : list Q),
forall (g : Q -> part A),
Forall (fun q => exists v, f q =! v /\ g q =! v) l ->
F g =! r.
Definition continuous_mod_weak_continuous [Q A R : Type] (F : (Q -> part A) -> part R) :=
exists (M : (Q -> part A) -> part (list Q)), weak_modulus F M /\ ex_mod_continuous_weak M.
Definition self_mod_weak_continuous [Q A R : Type] (F : (Q -> part A) -> part R) :=
exists (M : (Q -> part A) -> part (list Q)), weak_modulus F M /\ weak_modulus M M.
Lemma modulus_to_weak_modulus [Q A R : Type] : forall (F : (Q -> part A) -> part R) (M : (Q -> part A) -> part (list Q)),
modulus F M -> weak_modulus F M.
Proof.
intros F M H.
intros f.
specialize (H f).
split.
- intros Hf.
apply H in Hf as (l & Hl & _).
eexists; eauto.
- intros l Hl g Hg r Hr.
specialize (H ltac:(eexists; eauto)) as (l' & Hl' & Hf).
assert (l' = l) by (eapply hasvalue_det; eauto); subst.
specialize (Hf ltac:(eexists; eauto) g).
apply Hf; eauto.
clear Hl' Hl Hf.
induction Hg as [| a l Hl IHl ]; constructor; auto.
destruct Hl as (? & ? & ?); eapply equiv_hasvalue; eauto.
Qed.
Lemma ex_mod_to_ex_mod_weak [Q A R : Type] :
forall (F : (Q -> part A) -> part R), ex_modulus_cont F -> ex_mod_continuous_weak F.
Proof.
intros F HF.
intros f r Hr.
specialize (HF f ltac:(eexists; eauto)) as (l & Hl).
specialize (Hl ltac:(eexists; eauto)).
exists l.
intros g Hg.
apply Hl; eauto.
clear Hl; induction Hg as [| a l Hl IHl ]; constructor; eauto.
destruct Hl as (? & ? & ?); eapply equiv_hasvalue; eauto.
Qed.
Lemma continuous_mod_to_continuous_mod_weak [Q A R : Type] :
forall (F : (Q -> part A) -> part R), continuous_modulus_cont F -> continuous_mod_weak_continuous F.
Proof.
intros F (M & HF & HM).
exists M;
split.
- apply modulus_to_weak_modulus; auto.
- apply ex_mod_to_ex_mod_weak; auto.
Qed.
Lemma self_mod_to_self_mod_weak [Q A R : Type] :
forall (F : (Q -> part A) -> part R), self_modulus_cont F -> self_mod_weak_continuous F.
Proof.
intros F (M & HF & HM).
exists M;
split.
- apply modulus_to_weak_modulus; auto.
- apply modulus_to_weak_modulus; auto.
Qed.
Definition weak_modulus' [Q A R : Type] (F : (Q -> part A) -> part R) (M : (Q -> part A) -> part (list Q)) : Prop :=
forall (f : Q -> part A), (ter (F f) <-> ter (M f)) /\
forall (l : list Q), M f =! l -> forall (g : Q -> part A),
Forall (fun q => exists v, f q =! v /\ g q =! v) l ->
forall (r : R), F f =! r -> F g =! r.
Definition continuous_mod_weak_continuous' [Q A R : Type] (F : (Q -> part A) -> part R) :=
exists (M : (Q -> part A) -> part (list Q)), weak_modulus' F M /\ ex_mod_continuous_weak M.
Definition self_mod_weak_continuous' [Q A R : Type] (F : (Q -> part A) -> part R) :=
exists (M : (Q -> part A) -> part (list Q)), weak_modulus' F M /\ weak_modulus' M M.
Lemma strictify_weak_modulus [Q A R : Type] (F : (Q -> part A) -> part R) (M : (Q -> part A) -> part (list Q)) :
weak_modulus F M -> weak_modulus' F (strictify_modulus F M).
Proof.
intros HM.
intros f.
specialize (HM f) as (Hf' & Hf).
split.
- split.
+ intros Hter.
pose proof Hter as (r & Hr).
apply Hf' in Hter as (l & Hl).
eexists; psimpl.
+ intros (r & Hr).
unfold strictify_modulus in Hr.
psimpl; eexists; psimpl.
- intros l Hl.
unfold strictify_modulus in Hl.
psimpl.
Qed.
Lemma strictify_continuous_mod_weak [Q A R : Type] :
forall (F : (Q -> part A) -> part R),
continuous_mod_weak_continuous F <-> continuous_mod_weak_continuous' F.
Proof.
intros F; split; intros (M & HF & HM).
2: firstorder.
exists (strictify_modulus F M); split.
- apply strictify_weak_modulus; auto.
- intros f r Hr.
unfold strictify_modulus in Hr |- *.
apply bind_hasvalue in Hr as (? & ? & ?).
specialize (HM f r H0) as (l & Hl).
exists (r ++ l).
intros g Hg.
psimpl.
+ specialize (HF f) as (_ & Hf).
eapply Hf; eauto.
eapply Forall_app_l; eauto.
+ apply Hl.
eapply Forall_app_r; eauto.
Qed.
Lemma strictify_self_mod_weak [Q A R : Type] :
forall (F : (Q -> part A) -> part R),
self_mod_weak_continuous F <-> self_mod_weak_continuous' F.
Proof.
intros F; split; intros (M & HF & HM).
2: firstorder.
exists (strictify_modulus F M); split.
- apply strictify_weak_modulus; auto.
- intros f.
split; auto.
intros l Hl g Hg r Hr.
unfold strictify_modulus in *.
apply bind_hasvalue in Hl as (? & ? & ?).
apply bind_hasvalue in Hr as (? & ? & ?).
assert (x0 = x) by (eapply hasvalue_det; eauto); subst.
assert (r = l) by (eapply hasvalue_det; eauto); subst.
assert (F g =! x). {
specialize (HF f) as (_ & Hf).
eapply Hf; eauto.
}
assert (M g =! l). {
specialize (HM f) as (_ & Hf).
eapply Hf; eauto.
}
psimpl.
Qed.
Definition strong_modulus [Q A R : Type] (F : (Q -> part A) -> part R) (M : (Q -> part A) -> part (list Q)) :=
forall (f : Q -> part A) (r : R), F f =! r ->
exists (l : list Q), M f =! l /\
Forall (fun q => ter (f q)) l /\ forall (g : Q -> part A),
Forall (fun q => equiv (f q) (g q)) l -> F g =! r.
Definition ex_strong_modulus [Q A R : Type] (F : (Q -> part A) -> part R) :=
forall (f : Q -> part A) (r : R), F f =! r ->
exists (l : list Q),
Forall (fun q => ter (f q)) l /\ forall (g : Q -> part A),
Forall (fun q => equiv (f q) (g q)) l -> F g =! r.
Definition strong_modulus_cont [Q A R : Type] (F : (Q -> part A) -> part R) :=
exists (M : (Q -> part A) -> part (list Q)), strong_modulus F M.
Definition strong_cont_modulus_cont [Q A R : Type] (F : (Q -> part A) -> part R) :=
exists (M : (Q -> part A) -> part (list Q)), strong_modulus F M /\ strong_modulus_cont M.
Definition strong_self_modulus_cont [Q A R : Type] (F : (Q -> part A) -> part R) :=
exists (M : (Q -> part A) -> part (list Q)), strong_modulus F M /\ strong_modulus M M.
Definition monotonic_modulus [Q A R : Type] (F : (Q -> part A) -> part R) (M : (Q -> part A) -> part (list Q)) :=
forall (f : Q -> part A) (r : R), F f =! r ->
exists (l : list Q), M f =! l /\ forall (g : Q -> part A),
Forall (fun q => forall (a : A), f q =! a -> g q =! a) l ->
F g =! r.
Definition ex_monotonic_modulus [Q A R : Type] (F : (Q -> part A) -> part R) :=
forall (f : Q -> part A) (r : R), F f =! r ->
exists (l : list Q), forall (g : Q -> part A),
Forall (fun q => forall (a : A), f q =! a -> g q =! a) l -> F g =! r.
Definition monotonic_modulus_cont [Q A R : Type] (F : (Q -> part A) -> part R) :=
exists (M : (Q -> part A) -> part (list Q)), monotonic_modulus F M.
Definition monotonic_cont_modulus_cont [Q A R : Type] (F : (Q -> part A) -> part R) :=
exists (M : (Q -> part A) -> part (list Q)), monotonic_modulus F M /\ monotonic_modulus_cont M.
Definition monotonic_self_modulus_cont [Q A R : Type] (F : (Q -> part A) -> part R) :=
exists (M : (Q -> part A) -> part (list Q)), monotonic_modulus F M /\ monotonic_modulus M M.
Lemma ex_strong_mod_to_ex_monotonic_mod [Q A R : Type] :
forall (F : (Q -> part A) -> part R), ex_strong_modulus F -> ex_monotonic_modulus F.
Proof.
intros F HF f r Hr.
specialize (HF f r Hr) as (l & Hl & Hf).
exists l.
intros g Hg.
apply Hf.
clear Hf.
induction Hg as [|a l Ha HL' IHl]; auto.
inversion Hl; subst.
destruct H1.
constructor; auto.
eapply equiv_hasvalue; eauto.
Qed.
Lemma strong_modulus_to_monotonic_modulus [Q A R : Type] :
forall (F : (Q -> part A) -> part R) (M : (Q -> part A) -> part (list Q)),
strong_modulus F M -> monotonic_modulus F M.
Proof.
intros F M HM f r Hr.
specialize (HM f r Hr) as (l & HM & Hl' & Hl).
exists l; split; auto.
intros g Hg.
apply Hl.
clear HM Hl.
induction Hg as [|q l Hq IHl]; constructor; inversion Hl'; subst; eauto.
destruct H1.
eapply equiv_hasvalue; eauto.
Qed.
Lemma ex_monotonic_mod_to_ex_mod [Q A R : Type] :
forall (F : (Q -> part A) -> part R),
ex_monotonic_modulus F -> ex_modulus_cont F.
Proof.
intros F HF f (r & Hr).
specialize (HF f r Hr) as (l & Hl).
exists l.
intros _ g Hg.
eapply equiv_hasvalue; eauto.
apply Hl.
clear Hl.
induction Hg as [|a l Ha Hl IHl]; constructor; auto.
apply Ha.
Qed.
Lemma monotonic_modulus_to_modulus [Q A R : Type] :
forall (F : (Q -> part A) -> part R) (M : (Q -> part A) -> part (list Q)),
monotonic_modulus F M -> modulus F M.
Proof.
intros F M HM f (r & Hr).
specialize (HM f r Hr) as (l & Hl' & Hl).
exists l; split; auto.
intros _ g Hg.
eapply equiv_hasvalue; eauto.
apply Hl.
clear Hl Hl'.
induction Hg as [|a l Ha IHl]; constructor; eauto.
apply Ha.
Qed.
Lemma lpo_monotonic_mod_is_strong_mod [Q A R : Type] :
(forall (p : part A), {ter p} + {~ter p}) ->
forall (F : (Q -> part A) -> part R),
ex_monotonic_modulus F -> ex_strong_modulus F.
Proof.
intros LPO F HF f r Hr.
specialize (HF f r Hr) as (l & Hl).
exists (filter (fun q => if LPO (f q) then true else false) l).
split.
- rewrite Forall_forall.
intros q (_ & Hq)%filter_In.
now destruct (LPO (f q)).
- intros g Hg.
rewrite Forall_forall in Hg.
apply Hl.
rewrite Forall_forall.
intros q Hq a Ha.
apply Hg; eauto.
apply filter_In.
split; eauto.
destruct (LPO (f q)) as [_ | Hc]; eauto.
contradict Hc.
eexists; eauto.
Qed.
Lemma lpo_monotonic_mod_fn_is_strong_mod_fn [Q A R : Type] :
(forall (p : part A), {ter p} + {~ter p}) ->
forall (F : (Q -> part A) -> part R),
monotonic_modulus_cont F -> strong_modulus_cont F.
Proof.
intros LPO F (M & HM).
set (M' f := bind (M f) (fun l => ret (filter (fun q => if LPO (f q) then true else false) l))).
exists M'.
intros f r Hr.
apply HM in Hr as (l & Hl & Hr).
eexists; split.
1: unfold M'; psimpl.
split.
- rewrite Forall_forall.
intros q (_ & Hq)%filter_In.
now destruct (LPO (f q)).
- intros g Hg.
rewrite Forall_forall in Hg.
apply Hr.
rewrite Forall_forall.
intros q Hq a Ha.
apply Hg; eauto.
apply filter_In.
split.
1:eauto.
destruct (LPO (f q)) as [_ | Hc].
1:eauto.
contradict Hc.
eexists; eauto.
Qed.
Definition monotonic_seq [A : Type] (u : nat -> part A) :=
forall n m, n <= m -> forall v, u n =! v -> u m =! v.
Definition sup [A : Type] (u : nat -> part A) (p : part A) :=
forall v, p =! v <-> exists n, u n =! v.
Definition omega_cpo (A : Type) : forall (u : nat -> part A),
monotonic_seq u ->
{ p : part A & sup u p }.
Proof.
intros u Hu.
set (p := mkpart (fun k => let (n, m) := unembed k in seval (u n) m)).
exists p.
intros v.
split; intros Hv.
- apply mkpart_hasvalue1 in Hv.
destruct Hv as (k & Hk).
destruct (unembed k) as (n & m).
exists n.
rewrite seval_hasvalue.
exists m; eauto.
- destruct Hv as (n & Hn).
rewrite seval_hasvalue in Hn.
destruct Hn as (m & Hk).
apply mkpart_hasvalue2 with (n := embed (n, m)).
+ intros k1 k2 a1 a2 Ha1 Ha2.
destruct (unembed k1) as (n1 & m1), (unembed k2) as (n2 & m2).
assert (H1 : u n1 =! a1) by (rewrite seval_hasvalue; eauto).
assert (H2 : u n2 =! a2) by (rewrite seval_hasvalue; eauto).
destruct (Nat.le_ge_cases n1 n2) as [H | H]; specialize (Hu _ _ H).
* apply (Hu a1) in H1.
eapply hasvalue_det; eauto.
* apply (Hu a2) in H2.
eapply hasvalue_det; eauto.
+ simpl.
rewrite embedP.
assumption.
Defined.
Definition cpo_cont [Q A R : Type] (F : (Q -> part A) -> part R) :=
forall (f : nat -> Q -> part A),
(forall (q : Q), monotonic_seq (fun n => f n q)) ->
forall (f' : Q -> part A),
(forall (q : Q), sup (fun n => f n q) (f' q)) ->
sup (fun n => F (f n)) (F f').
(* Si S est un ensemble dirigé infini dans un omega-cpo de la forme A -> lift B,
alors S a un sup. De plus, si f est une fonction de ce cpo vers un autre omega-cpo de la forme lift C,
alors f(S) a un sup, et sup(f(S)) = f(sup S).
Hmmm. Si c'est infini je peux extraire *une* suite. Pas nécessairement une qui tend vers le sup.
Typiquement, dans omega * 2 + 1, avec une suite qui tend vers omega au lieu de omega * 2.
Et je ne peux pas disjoncter selon si un des éléments de S est pas undef ou non.*)
Definition extensional [Q A R : Type] (F : (Q -> part A) -> part R) :=
forall (f g : Q -> part A),
pointwise_relation Q (equiv (A := A)) f g ->
equiv (F f) (F g).
Lemma modulus_cont_to_extensional [Q A R : Type] (F : (Q -> part A) -> part R) :
ex_modulus_cont F -> extensional F.
Proof.
intros Hmod.
intros f g Hfg.
pose proof (Hmod f) as Hf.
pose proof (Hmod g) as Hg.
assert (H: forall l, Forall (fun q => equiv (f q) (g q)) l). {
intros l.
induction l; constructor; eauto; try now rewrite Hfg.
}
intros v; split; intros Hv.
- destruct (Hf ltac:(eexists; eauto)) as (l & Hl).
specialize (Hl ltac:(eexists; eauto) g (H l)).
apply Hl; eauto.
- destruct (Hg ltac:(eexists; eauto)) as (l & Hl).
assert (H' : forall q, (equiv (f q) (g q)) <-> equiv (g q) (f q))
by (intros; split; intros; symmetry; assumption).
setoid_rewrite H' in H.
specialize (Hl ltac:(eexists; eauto) f (H l)).
apply Hl; eauto.
Qed.
Goal forall (Q A : Type) (f g : Q -> part A) (l : list Q),
Forall (fun q => equiv (f q) (g q)) l /\ Forall (fun q => ter (f q)) l
<-> Forall (fun q => exists v, f q =! v /\ g q =! v) l.
Proof.
intros Q A f g l.
split.
- intros (Hl1 & Hl2). revert Hl2.
induction Hl1 as [| a l1 Ha Hl1 IHl1 ]; intros Hl2; auto.
inversion Hl2; subst.
destruct H1 as (v & Hv).
constructor; firstorder.
- intros Hl.
induction Hl as [| a l (v & Hv1 & Hv2) Hl (IHl & IHl2) ]; auto.
split; constructor; try firstorder.
eapply equiv_hasvalue; eauto.
Qed.
Definition monotonic [Q A R : Type] (F : (Q -> part A) -> part R) :=
forall (f g : Q -> part A),
(forall (q : Q) (a : A), f q =! a -> g q =! a) ->
forall (r : R), F f =! r -> F g =! r.
Lemma cpo_cont_to_monotonic [Q A R : Type] (F : (Q -> part A) -> part R) :
cpo_cont F -> monotonic F.
Proof.
intros HF f g Hfg r Hr.
set (h := fun n q => match n with 0 => f q | S _ => g q end).
assert (Hh : forall (q : Q), monotonic_seq (fun n => h n q)). {
intros q [|n];
intros [|m] Hm v Hv; unfold h in Hv |- *;
inversion Hm; subst;
try assumption; try apply Hfg; try assumption.
}
assert (Hh' : forall (q : Q), sup (fun n => h n q) (g q)). {
intros q.
intros v; split; intros Hv.
- exists 2.
assumption.
- destruct Hv as ([|n] & Hn).
+ apply Hfg.
assumption.
+ assumption.
}
specialize (HF h Hh g Hh' r).
apply HF; exists 0; eauto.
Qed.
(* il faut faire plus compliqué si on force la terminaison sur le module *)
Definition approx [A : Type] (f : nat -> part A) : nat -> nat -> part A :=
fun n m => if m <=? n then f m else undef.
Lemma approx_monotonic_seq [A : Type] : forall (f : nat -> part A) (q : nat),
monotonic_seq (fun n => approx f n q).
Proof.
intros f q n m Hnm r Hr.
unfold approx in *.
destruct (q <=? n) eqn:E; psimpl.
apply leb_complete in E.
rewrite leb_correct; try lia.
psimpl.
Qed.
Lemma approx_sup [A : Type] : forall (f : nat -> part A) (q : nat),
sup (fun n => approx f n q) (f q).
Proof.
intros f q a.
unfold approx in *; split.
+ intros Ha.
exists q.
rewrite leb_correct; try lia.
psimpl.
+ intros (n & Hn).
destruct (q <=? n); psimpl.
Qed.
Definition modulus_of_cpo_nat [A R : Type] (F : (nat -> part A) -> part R) : cpo_cont F ->
(nat -> part A) -> part (list nat).
Proof.
intros HF.
refine (fun f => bind (proof_ter (F f)) (fun Hter => ret _)).
specialize (HF (approx f) ltac:(apply approx_monotonic_seq) f ltac:(apply approx_sup)).
assert (Hf : hasvalue (F f) (eval Hter)) by apply eval_hasvalue.
apply HF in Hf.
assert (Hseval : exists k, let (n, m) := unembed k in
if seval (F (approx f n)) m then True else False
). {
destruct Hf as (n & Hn).
apply seval_hasvalue in Hn as (m & Hm).
exists (embed (n, m)).
rewrite embedP.
rewrite Hm.
auto.
}
apply constructive_indefinite_ground_description_nat in Hseval as (k & Hk). 2:{
intros k.
destruct (unembed k) eqn:E.
destruct (seval _ _); auto.
}
destruct (unembed k) eqn:E.
exact (tabulate id 0 (S n)).
Defined.
Lemma modulus_of_cpo_nat_is_modulus [A R : Type] (F : (nat -> part A) -> part R) :
forall (HF : cpo_cont F), monotonic_modulus F (modulus_of_cpo_nat F HF).
Proof.
intros HF f r Hr.
assert (exists (n : nat), modulus_of_cpo_nat F HF f =! tabulate id 0 (S n) /\ ter (F (approx f n))) as (n & Hn & Hn'). {
assert (ter (proof_ter (F f))) as (Hter & ?) by (apply proof_ter_spec; eexists; eauto).
assert (ter (modulus_of_cpo_nat F HF f)) as (l & Hl) by (eapply bind_ter; eauto; eexists; psimpl).
unfold modulus_of_cpo_nat in Hl |- *.
rewrite bind_hasvalue_given in Hl; eauto.
setoid_rewrite bind_hasvalue_given; eauto.
apply ret_hasvalue_inv in Hl.
setoid_rewrite <- ret_hasvalue_iff.
set (Q k := let (n, m) := unembed k in _ : Prop) in *.
set (Hdec k := _ : {Q k} + {~Q k}) in *.
set (HQ := match _ with ex_intro x H => _ end : exists k, Q k) in *.
set (c := constructive_indefinite_ground_description_nat Q Hdec HQ) in *.
destruct c as (k & Hk).
unfold Q in Hk.
destruct (unembed k) as (n & m) eqn:E.
exists n.
destruct (seval _ _) eqn:E'; try now inversion Hk.
split; auto.
eexists; apply seval_hasvalue; eauto.
}
eexists; split; eauto.
destruct Hn' as (r' & Hr').
assert (r' = r). {
eapply hasvalue_det.
2: eauto.
eapply (HF (approx f)); eauto.
- apply approx_monotonic_seq.
- apply approx_sup.
}
subst.
intros g Hg.
eapply equiv_hasvalue; eauto.
eapply cpo_cont_to_monotonic; try eassumption.
clear Hn Hr'.
induction n as [|n IHn]; intros q a Hq.
+ unfold approx in Hq.
destruct (q <=? 0) eqn:E; psimpl.
apply leb_complete in E.
inversion E; subst.
cbn in Hg.
inversion Hg; subst.
apply H1; eauto.
+ unfold approx in Hq.
destruct (q <=? S n) eqn:E; psimpl.
apply leb_complete in E.
rewrite tabulate_succ' in Hg; try lia.
inversion E; subst.
* apply Forall_app_r in Hg.
inversion Hg; subst.
apply H1; auto.
* apply Forall_app_l in Hg.
inversion Hg; subst.
apply IHn; eauto.
unfold approx.
rewrite leb_correct; eauto.
Qed.
Lemma ex_monotonic_mod_to_monotonic [Q A R : Type] :
forall (F : (Q -> part A) -> part R), ex_monotonic_modulus F -> monotonic F.
Proof.
intros F HF f g Hfg r Hr.
apply HF in Hr as (l & Hg).
apply Hg.
clear Hg.
induction l; eauto.
Qed.
Lemma ex_self_mod_to_cpo_cont [Q A R : Type] :
forall (F : (Q -> part A) -> part R),
ex_strong_modulus F -> cpo_cont F.
Proof.
intros F HF f Hf f' Hf' r.
split.
- intros (l & Hl & Hf'')%HF.
enough (exists n, forall m, n <= m -> Forall (fun q => equiv (f' q) (f m q)) l) as (n & Hn)
by (eexists; eapply Hf''; eauto).
clear Hf''.
induction Hl as [|q l (a & (m & Hm)%Hf') Hl (n & Hn)];
unshelve eauto; try now exact 0.
exists (max n m).
intros k Hk.
constructor.
1:eapply equiv_hasvalue; (eapply Hf' || eapply Hf in Hm);
eauto; try lia.
apply Hn; lia.
- intros (n & Hn).
eapply ex_monotonic_mod_to_monotonic; try eassumption.
1:apply ex_strong_mod_to_ex_monotonic_mod; firstorder.
intros q a Ha.
apply Hf'.
eauto.
Qed.
Lemma cpo_cont_to_monotonic_modulus_cont_nat [A R : Type] :
forall (F : (nat -> part A) -> part R), cpo_cont F -> monotonic_modulus_cont F.
Proof.
intros F HF.
exists (modulus_of_cpo_nat F HF).
apply modulus_of_cpo_nat_is_modulus.
Qed.
Definition lpo (A : Type) := forall (p : part A), {ter p} + {~ter p}.
Lemma lpo_cpo_cont_is_strong_mod_cont_nat [A R : Type] :
lpo A ->
forall (F : (nat -> part A) -> part R),
cpo_cont F <-> strong_modulus_cont F.
Proof.
intros LPO F.
split; intros HF.
- apply lpo_monotonic_mod_fn_is_strong_mod_fn; eauto.
apply cpo_cont_to_monotonic_modulus_cont_nat; eauto.
- apply ex_self_mod_to_cpo_cont.
firstorder.
Qed.
Lemma lpo_cpo_cont_is_monotonic_mod_cont_nat [A R : Type] :
lpo A ->
forall (F : (nat -> part A) -> part R),
cpo_cont F <-> monotonic_modulus_cont F.
Proof.
intros LPO F.
split; intros HF.
- now apply cpo_cont_to_monotonic_modulus_cont_nat.
- apply lpo_monotonic_mod_fn_is_strong_mod_fn in HF; eauto.
apply ex_self_mod_to_cpo_cont.
firstorder.
Qed.
Lemma monotonic_to_extensional [Q A R : Type] :
forall (F : (Q -> part A) -> part R), monotonic F -> extensional F.
Proof.
intros F HF.
assert (Hext : forall f g,
pointwise_relation Q (equiv (A := A)) f g ->
(forall q a, f q =! a -> g q =! a)
). {
intros f g Heq q a Ha.
now apply Heq.
}
intros f g Hfg.
pose proof Hfg as Hgf.
symmetry in Hgf.
split; intros H; eapply HF; eauto.
Qed.
Lemma lots_of_separation : exists (F : (bool -> part unit) -> part unit),
(monotonic_self_modulus_cont F) /\
(exists (M : (bool -> part unit) -> part (list bool)), monotonic_modulus F M /\ strong_modulus_cont M) /\
(exists (M : (bool -> part unit) -> part (list bool)), strong_modulus F M) /\
~(exists (M : (bool -> part unit) -> part (list bool)), strong_modulus F M /\ ex_monotonic_modulus M).
Proof.
set (F (f : bool -> part unit) := bind (par (f true) (f false)) (fun _ => ret ())).
exists F.
repeat split.
- exists (fun f => ret [ true ; false ]).
split.
+ intros f () (b & Hr & _)%bind_hasvalue.
eexists; split; psimpl.
intros g Hg.
inversion Hg; subst.
inversion H2; subst.
unfold F in *.
enough (ter (par (g true) (g false))) as (? & ?) by (rewrite bind_hasvalue_given; psimpl).
apply par_hasvalue3.
destruct b; [
apply par_hasvalue1 in Hr; apply H1 in Hr; left; eexists; eauto
| apply par_hasvalue2 in Hr; apply H3 in Hr; right; eexists; eauto
].
+ intros f l Hr%ret_hasvalue_iff.
exists l; split; subst; psimpl.
intros; psimpl.
- exists (fun f => ret [ true ; false ]).
split.
+ intros f () (b & Hr & _)%bind_hasvalue.
eexists; split; psimpl.
intros g Hg.
inversion Hg; subst.
inversion H2; subst.
unfold F in *.
enough (ter (par (g true) (g false))) as (? & ?) by (rewrite bind_hasvalue_given; psimpl).
apply par_hasvalue3.
destruct b; [
apply par_hasvalue1 in Hr; apply H1 in Hr; left; eexists; eauto
| apply par_hasvalue2 in Hr; apply H3 in Hr; right; eexists; eauto
].
+ exists (fun f => ret nil).
intros f l Hl%ret_hasvalue_iff; subst.
eexists; split; psimpl.
split; eauto.
intros g Hg; psimpl.
- set (M (f : bool -> part unit) := bind (par (f true) (f false))
(fun o => ret (match o with
| inl _ => [ true ]
| inr _ => [ false ]
end))). (* Je ne peux pas montrer que M est continue, quelle que soit le sens de continue ici *)
exists M.
intros f () (b & Hb & _)%bind_hasvalue.
unfold F, M.
eexists; split; [ rewrite bind_hasvalue_given; eauto; psimpl |].
destruct b; apply par_hasvalue1 in Hb || apply par_hasvalue2 in Hb;
(split; [repeat econstructor; eauto |]); intros g Hg; inversion Hg; subst;
enough (ter (par (g true) (g false))) as (? & ?)
by (rewrite bind_hasvalue_given; psimpl); apply par_hasvalue3;
[ left | right ]; eexists; apply H1; apply Hb.
- intros (M & HF & HM).
set (f1 (b : bool) := if b then ret () else undef).
set (f2 (b : bool) := if b then undef else ret ()).
set (f3 (b : bool) := @undef _ unit).
set (f4 (b : bool) := ret ()).
assert (F f1 =! ()) as (l1 & Hl1 & Hter1 & Hf1)%HF. {
unfold F.
eenough (ter (par (f1 true) (f1 false))) as (? & ?)
by (rewrite bind_hasvalue_given; psimpl).
apply par_hasvalue3; left; eexists; psimpl.
}
assert (F f2 =! ()) as (l2 & Hl2 & Hter2 & Hf2)%HF. {
unfold F.
eenough (ter (par (f2 true) (f2 false))) as (? & ?)
by (rewrite bind_hasvalue_given; psimpl).
apply par_hasvalue3; right; eexists; psimpl.
}
assert (Hter : ~ter (F f3)). {
intros (() & Hr).
unfold F, f3 in Hr.
psimpl.
destruct x; apply par_hasvalue1 in H || apply par_hasvalue2 in H; psimpl.
}
destruct l1 as [|[] l1]. {
apply Hter; eexists.
apply Hf1; auto.
} 2:{
inversion Hter1; subst.
destruct H1 as (? & ?); unfold f1 in *; psimpl.
}
destruct l2 as [|[] l2]. {
apply Hter; eexists.
apply Hf2; auto.
} 1:{
inversion Hter2; subst.
destruct H1 as (? & ?); unfold f2 in *; psimpl.
}
assert (HM' : monotonic M) by now apply ex_monotonic_mod_to_monotonic.
assert (forall q a, f1 q =! a -> f4 q =! a) by (unfold f4; intros _ () _; psimpl).
assert (forall q a, f2 q =! a -> f4 q =! a) by (unfold f4; intros _ () _; psimpl).
enough (true :: l1 = false :: l2) as [=];
eapply hasvalue_det; eapply HM'.
2,4: eauto.
1,2: eauto.
Qed.
Lemma ext_but_not_mono : lpo unit ->
exists (F : (bool -> part unit) -> part bool), ex_modulus_cont F /\ ~monotonic F.
Proof.
intros HLPO.
(* F f =! true si f true et f false terminent, =! false sinon *)
(* on peut aussi se demander : quid de "un seul parmi f true et f false termine" ? *)
set (F := fun (f : bool -> part unit) =>
match HLPO (f true), HLPO (f false) with
| left _, left _ => ret true
| _, _ => ret false
end
).
exists F.
split.
- intros f Hf.
exists [ true; false ].
intros _ g Hg.
inversion Hg; subst.
inversion H2; subst.
clear Hg H2 H4.
unfold F.
destruct (HLPO (f true)), (HLPO (f false)), (HLPO (g true)), (HLPO (g false));
eapply equiv_hasvalue; psimpl;
try (rewrite H1 in * |- ; contradiction);
try (rewrite H3 in * |- ; contradiction).
- intros Hfg.
set (f1 := fun (_ : bool) => undef (A := unit)).
set (f2 := fun (_ : bool) => ret ()).
assert (H1 : F f1 =! false). {
unfold F.
destruct (HLPO (f1 true)) as [(? & ?)|], (HLPO (f1 false)) as [(? & ?)|];
unfold f1 in *; try psimpl.
}
assert (H2 : F f2 =! true). {
unfold F.
destruct (HLPO (f2 true)) as [(? & ?)| H], (HLPO (f2 false)) as [(? & ?)| H'];
unfold f2 in *; try psimpl;
(contradict H || contradict H'); eexists; psimpl.
}
enough (true = false) as [=].
eapply hasvalue_det; eauto.
eapply Hfg with (f := f1); eauto.
intros q () _; psimpl.
Qed.
End PartialZoo.