diff --git a/iris_core.v b/iris_core.v
index f5d92bbfa4a1a041c699628e0104a590bf65887f..9d05c4840c5ccdb11fe96901a04e928e4c2ac045 100644
--- a/iris_core.v
+++ b/iris_core.v
@@ -115,10 +115,6 @@ Module IrisCore (RL : PCM_T) (C : CORE_LANG).
intEqP (w i) (Some (ı' p)).
Program Definition inv i : Props -n> Props :=
n[(fun p => m[(invP i p)])].
- Next Obligation.
- intros w1 w2 EQw; unfold equiv, invP in *.
- apply intEq_equiv; [apply EQw | reflexivity].
- Qed.
Next Obligation.
intros w1 w2 EQw; unfold invP; simpl morph.
destruct n; [apply dist_bound |].
@@ -131,11 +127,6 @@ Module IrisCore (RL : PCM_T) (C : CORE_LANG).
destruct (w2 i) as [μ2 |]; [| contradiction]; simpl in Sw.
rewrite <- Sw; assumption.
Qed.
- Next Obligation.
- intros p1 p2 EQp w; unfold equiv, invP in *; simpl morph.
- apply intEq_equiv; [reflexivity |].
- rewrite EQp; reflexivity.
- Qed.
Next Obligation.
intros p1 p2 EQp w; unfold invP; simpl morph.
apply intEq_dist; [reflexivity |].
@@ -184,9 +175,6 @@ Module IrisCore (RL : PCM_T) (C : CORE_LANG).
Program Definition ownS : state -n> Props :=
n[(fun s => ownRP (ex_own _ s))].
- Next Obligation.
- intros r1 r2 EQr. hnf in EQr. now rewrite EQr.
- Qed.
Next Obligation.
intros r1 r2 EQr; destruct n as [| n]; [apply dist_bound |].
simpl in EQr. subst; reflexivity.
@@ -207,9 +195,6 @@ Module IrisCore (RL : PCM_T) (C : CORE_LANG).
| Some r => ownRL r
| None => ⊥
end)].
- Next Obligation.
- intros r1 r2 EQr; apply ores_equiv_eq in EQr; now rewrite EQr.
- Qed.
Next Obligation.
intros r1 r2 EQr; destruct n as [| n]; [apply dist_bound |].
destruct r1 as [r1 |]; destruct r2 as [r2 |]; try contradiction; simpl in EQr; subst; reflexivity.
@@ -247,12 +232,12 @@ Module IrisCore (RL : PCM_T) (C : CORE_LANG).
Proof.
intros w n r; split; [intros Hut | intros [r1 [r2 [EQr [Hu Ht] ] ] ] ].
- destruct (u · t)%pcm as [ut |] eqn: EQut; [| contradiction].
- do 15 red in Hut; rewrite <- Hut.
+ do 17 red in Hut. rewrite <- Hut.
destruct u as [u |]; [| now erewrite pcm_op_zero in EQut by apply _].
assert (HT := comm (Some u) t); rewrite EQut in HT.
destruct t as [t |]; [| now erewrite pcm_op_zero in HT by apply _]; clear HT.
exists (pcm_unit (pcm_res_ex state), u) (pcm_unit (pcm_res_ex state), t).
- split; [unfold pcm_op, res_op, pcm_op_prod | split; do 15 red; reflexivity].
+ split; [unfold pcm_op, res_op, pcm_op_prod | split; do 17 red; reflexivity].
now erewrite pcm_op_unit, EQut by apply _.
- destruct u as [u |]; [| contradiction]; destruct t as [t |]; [| contradiction].
destruct Hu as [ru EQu]; destruct Ht as [rt EQt].
@@ -278,10 +263,6 @@ Module IrisCore (RL : PCM_T) (C : CORE_LANG).
intros n1 n2 _ _ HLe _ HT w' k r HSw HLt Hp; eapply HT, Hp; [eassumption |].
now eauto with arith.
Qed.
- Next Obligation.
- intros w1 w2 EQw n rr; simpl; split; intros HT k r HLt;
- [rewrite <- EQw | rewrite EQw]; apply HT; assumption.
- Qed.
Next Obligation.
intros w1 w2 EQw k; simpl; intros _ HLt; destruct n as [| n]; [now inversion HLt |].
split; intros HT w' m r HSw HLt' Hp.
diff --git a/iris_vs.v b/iris_vs.v
index 3958f855720b46ea37d966b9fd00b4dbbbe07d89..1fb506dbd87747ae5cf604f39991d9bee341ef7c 100644
--- a/iris_vs.v
+++ b/iris_vs.v
@@ -34,13 +34,6 @@ Module IrisVS (RL : PCM_T) (C : CORE_LANG).
Program Definition pvs (m1 m2 : mask) : Props -n> Props :=
n[(fun p => m[(preVS m1 m2 p)])].
- Next Obligation.
- intros w1 w2 EQw n r; split; intros HP w2'; intros.
- - eapply HP; try eassumption; [].
- rewrite EQw; assumption.
- - eapply HP; try eassumption; [].
- rewrite <- EQw; assumption.
- Qed.
Next Obligation.
intros w1 w2 EQw n' r HLt; destruct n as [| n]; [now inversion HLt |]; split; intros HP w2'; intros.
- symmetry in EQw; assert (HDE := extend_dist _ _ _ _ EQw HSub).
@@ -65,11 +58,6 @@ Module IrisVS (RL : PCM_T) (C : CORE_LANG).
intros w1 w2 EQw n r HP w2'; intros; eapply HP; try eassumption; [].
etransitivity; eassumption.
Qed.
- Next Obligation.
- intros p1 p2 EQp w n r; split; intros HP w1; intros.
- - setoid_rewrite <- EQp; eapply HP; eassumption.
- - setoid_rewrite EQp; eapply HP; eassumption.
- Qed.
Next Obligation.
intros p1 p2 EQp w n' r HLt; split; intros HP w1; intros.
- edestruct HP as [w2 [r' [HW [HP' HE'] ] ] ]; try eassumption; [].
@@ -110,7 +98,7 @@ Module IrisVS (RL : PCM_T) (C : CORE_LANG).
Proof.
intros pw nn r w _; clear r pw.
intros n r _ _ HInv w'; clear nn; intros.
- do 12 red in HInv; destruct (w i) as [μ |] eqn: HLu; [| contradiction].
+ do 14 red in HInv; destruct (w i) as [μ |] eqn: HLu; [| contradiction].
apply ı in HInv; rewrite (isoR p) in HInv.
(* get rid of the invisible 1/2 *)
do 8 red in HInv.
@@ -146,7 +134,7 @@ Module IrisVS (RL : PCM_T) (C : CORE_LANG).
Proof.
intros pw nn r w _; clear r pw.
intros n r _ _ [r1 [r2 [HR [HInv HP] ] ] ] w'; clear nn; intros.
- do 12 red in HInv; destruct (w i) as [μ |] eqn: HLu; [| contradiction].
+ do 14 red in HInv; destruct (w i) as [μ |] eqn: HLu; [| contradiction].
apply ı in HInv; rewrite (isoR p) in HInv.
(* get rid of the invisible 1/2 *)
do 8 red in HInv.
@@ -254,16 +242,16 @@ Module IrisVS (RL : PCM_T) (C : CORE_LANG).
Definition ownLP (P : option RL.res -> Prop) : {s : option RL.res | P s} -n> Props :=
ownL <M< inclM.
-Lemma pcm_op_split rp1 rp2 rp sp1 sp2 sp :
- Some (rp1, sp1) · Some (rp2, sp2) == Some (rp, sp) <->
- Some rp1 · Some rp2 == Some rp /\ Some sp1 · Some sp2 == Some sp.
-Proof.
- unfold pcm_op at 1, res_op at 2, pcm_op_prod at 1.
- destruct (Some rp1 · Some rp2) as [rp' |]; [| simpl; tauto].
- destruct (Some sp1 · Some sp2) as [sp' |]; [| simpl; tauto].
- simpl; split; [| intros [EQ1 EQ2]; subst; reflexivity].
- intros EQ; inversion EQ; tauto.
-Qed.
+ Lemma pcm_op_split rp1 rp2 rp sp1 sp2 sp :
+ Some (rp1, sp1) · Some (rp2, sp2) == Some (rp, sp) <->
+ Some rp1 · Some rp2 == Some rp /\ Some sp1 · Some sp2 == Some sp.
+ Proof.
+ unfold pcm_op at 1, res_op at 2, pcm_op_prod at 1.
+ destruct (Some rp1 · Some rp2) as [rp' |]; [| simpl; tauto].
+ destruct (Some sp1 · Some sp2) as [sp' |]; [| simpl; tauto].
+ simpl; split; [| intros [EQ1 EQ2]; subst; reflexivity].
+ intros EQ; inversion EQ; tauto.
+ Qed.
Lemma vsGhostUpd m rl (P : option RL.res -> Prop)
(HU : forall rf (HD : rl · rf <> None), exists sl, P sl /\ sl · rf <> None) :
@@ -319,17 +307,10 @@ Qed.
Program Definition inv' m : Props -n> {n : nat | m n} -n> Props :=
n[(fun p => n[(fun n => inv n p)])].
- Next Obligation.
- intros i i' EQi; simpl in EQi; rewrite EQi; reflexivity.
- Qed.
Next Obligation.
intros i i' EQi; destruct n as [| n]; [apply dist_bound |].
simpl in EQi; rewrite EQi; reflexivity.
Qed.
- Next Obligation.
- intros p1 p2 EQp i; simpl morph.
- apply (morph_resp (inv (` i))); assumption.
- Qed.
Next Obligation.
intros p1 p2 EQp i; simpl morph.
apply (inv (` i)); assumption.
@@ -365,7 +346,7 @@ Qed.
now rewrite fdUpdate_neq by assumption.
}
exists (fdUpdate i (ı' p) w) (pcm_unit _); split; [assumption | split].
- - exists (exist _ i Hm); do 16 red.
+ - exists (exist _ i Hm); do 22 red.
unfold proj1_sig; rewrite fdUpdate_eq; reflexivity.
- erewrite pcm_op_unit by apply _.
destruct HE as [rs [HE HM] ].
diff --git a/iris_wp.v b/iris_wp.v
index 0e89112a7fb26421f3c96c0fdcbcb41602839b0a..7735080ceca5c18d91aedaedbc29dbc9b55850c2 100644
--- a/iris_wp.v
+++ b/iris_wp.v
@@ -87,12 +87,6 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
eapply uni_pred, HWR; [| eexists; rewrite <- HR]; reflexivity.
- auto.
Qed.
- Next Obligation.
- intros w1 w2 EQw n r; simpl.
- split; intros Hp w'; intros; eapply Hp; try eassumption.
- - rewrite EQw; assumption.
- - rewrite <- EQw; assumption.
- Qed.
Next Obligation.
intros w1 w2 EQw n' r HLt; simpl; destruct n as [| n]; [now inversion HLt |]; split; intros Hp w2'; intros.
- symmetry in EQw; assert (EQw' := extend_dist _ _ _ _ EQw HSw); assert (HSw' := extend_sub _ _ _ _ EQw HSw); symmetry in EQw'.
@@ -146,10 +140,6 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
intros w1 w2 Sw n r; simpl; intros Hp w'; intros; eapply Hp; try eassumption.
etransitivity; eassumption.
Qed.
- Next Obligation.
- intros φ1 φ2 EQφ w n r; simpl.
- unfold wpFP; setoid_rewrite EQφ; reflexivity.
- Qed.
Next Obligation.
intros φ1 φ2 EQφ w k r HLt; simpl; destruct n as [| n]; [now inversion HLt |].
split; intros Hp w'; intros; edestruct Hp as [HV [HS [HF HS'] ] ]; try eassumption; [|].
@@ -176,18 +166,10 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
eapply (met_morph_nonexp _ _ (WP _)), HWR; [eassumption | now eauto with arith].
+ auto.
Qed.
- Next Obligation.
- intros e1 e2 EQe φ w n r; simpl.
- simpl in EQe; subst e2; reflexivity.
- Qed.
Next Obligation.
intros e1 e2 EQe φ w k r HLt; destruct n as [| n]; [now inversion HLt | simpl].
simpl in EQe; subst e2; reflexivity.
Qed.
- Next Obligation.
- intros WP1 WP2 EQWP e φ w n r; simpl.
- unfold wpFP; setoid_rewrite EQWP; reflexivity.
- Qed.
Next Obligation.
intros WP1 WP2 EQWP e φ w k r HLt; destruct n as [| n]; [now inversion HLt | simpl].
split; intros Hp w'; intros; edestruct Hp as [HF [HS [HV HS'] ] ]; try eassumption; [|].
@@ -387,9 +369,6 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
Next Obligation.
firstorder.
Qed.
- Next Obligation.
- intros x y H_xy P n r. simpl. rewrite H_xy. tauto.
- Qed.
Next Obligation.
intros x y H_xy P m r. simpl in H_xy. destruct n.
- intros LEZ. exfalso. omega.
@@ -451,9 +430,6 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
(** Ret **)
Program Definition eqV v : vPred :=
n[(fun v' : value => v === v')].
- Next Obligation.
- intros v1 v2 EQv w n r; simpl in *; split; congruence.
- Qed.
Next Obligation.
intros v1 v2 EQv w m r HLt; destruct n as [| n]; [now inversion HLt | simpl in *].
split; congruence.
@@ -486,11 +462,6 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
and context is nonexpansive. *)
Program Definition plugV safe m φ φ' K :=
n[(fun v : value => ht safe m (φ v) (K [[` v]]) φ')].
- Next Obligation.
- intros v1 v2 EQv w n r; simpl.
- setoid_rewrite EQv at 1.
- simpl in EQv; rewrite EQv; reflexivity.
- Qed.
Next Obligation.
intros v1 v2 EQv; unfold ht; eapply (met_morph_nonexp _ _ box).
eapply (impl_dist (ComplBI := Props_BI)).
@@ -553,10 +524,6 @@ Module IrisWP (RL : PCM_T) (C : CORE_LANG).
postconditions is nonexpansive *)
Program Definition vsLift m1 m2 φ φ' :=
n[(fun v => vs m1 m2 (φ v) (φ' v))].
- Next Obligation.
- intros v1 v2 EQv; unfold vs.
- rewrite EQv; reflexivity.
- Qed.
Next Obligation.
intros v1 v2 EQv; unfold vs.
rewrite ->EQv; reflexivity.
diff --git a/lib/ModuRes/BI.v b/lib/ModuRes/BI.v
index 42de387d2df663883182f7a98def1722772b9a41..63304343dd4efed5ad901c18c47cec804236eb8b 100644
--- a/lib/ModuRes/BI.v
+++ b/lib/ModuRes/BI.v
@@ -448,10 +448,6 @@ Section MonotoneExt.
Global Program Instance all_mm : allBI (T -m> B) :=
fun U eqU mU cmU R =>
m[(fun t => all n[(fun u => R u t)])].
- Next Obligation.
- intros t1 t2 EQt; apply all_equiv; intros u; simpl morph.
- rewrite EQt; reflexivity.
- Qed.
Next Obligation.
intros t1 t2 EQt; apply all_dist; intros u; simpl morph.
rewrite EQt; reflexivity.
@@ -464,10 +460,6 @@ Section MonotoneExt.
Global Program Instance xist_mm : xistBI (T -m> B) :=
fun U eqU mU cmU R =>
m[(fun t => xist n[(fun u => R u t)])].
- Next Obligation.
- intros t1 t2 EQt; apply xist_equiv; intros u; simpl morph.
- rewrite EQt; reflexivity.
- Qed.
Next Obligation.
intros t1 t2 EQt; apply xist_dist; intros u; simpl morph.
rewrite EQt; reflexivity.
@@ -698,10 +690,6 @@ Section MComplUP.
intros n m v1 v2 HLe HSubv HT t' HSubt.
rewrite HLe, <- HSubv; apply HT, HSubt.
Qed.
- Next Obligation.
- intros t1 t2 EQt n v; split; intros HT t' Subt; apply HT; [| symmetry in EQt];
- rewrite EQt; assumption.
- Qed.
Next Obligation.
intros t1 t2 EQt m v HLt; split; intros HT t' Subt;
(destruct n as [| n]; [now inversion HLt |]).
@@ -716,9 +704,6 @@ Section MComplUP.
Next Obligation.
intros t1 t2 Subt n v HT t' Subt'; apply HT; etransitivity; eassumption.
Qed.
- Next Obligation.
- intros f1 f2 EQf u n v; split; intros HH u' HSub; apply EQf, HH, HSub.
- Qed.
Next Obligation.
intros f1 f2 EQf u m v HLt; split; intros HH u' HSub; apply EQf, HH; assumption.
Qed.
@@ -766,11 +751,6 @@ Section MComplMM.
intros [u1 v1] [u2 v2] [EQu EQv]; simpl morph.
unfold fst, snd in *; rewrite EQu, EQv; reflexivity.
Qed.
- Next Obligation.
- intros f1 f2 EQf u v; simpl morph.
- apply (morph_resp mclose); clear u v; intros [u v]; simpl morph.
- apply EQf.
- Qed.
Next Obligation.
intros f1 f2 EQf u v; simpl morph.
apply mclose; clear u v; intros [u v]; simpl morph.
@@ -792,7 +772,7 @@ Section MComplMM.
End MComplMM.
-Section Foo.
+Section BIValid.
Local Obligation Tactic := intros.
Global Program Instance BI_valid T `{ComplBI T} : Valid T :=
@@ -801,4 +781,4 @@ Section Foo.
etransitivity; [apply top_true | assumption].
Qed.
-End Foo.
+End BIValid.
diff --git a/lib/ModuRes/Finmap.v b/lib/ModuRes/Finmap.v
index 6f601f8eb34bf7077e64b2239dc9340c87dd3913..eaeede928dd0ad7ff31309ed052de80265ef5b39 100644
--- a/lib/ModuRes/Finmap.v
+++ b/lib/ModuRes/Finmap.v
@@ -691,14 +691,6 @@ Section FinDom.
Program Definition fdMap (f : U -m> V) : (K -f> U) -m> (K -f> V) :=
m[(pre_fdMap f)].
- Next Obligation.
- intros m1 m2 HEq k; simpl; specialize (HEq k).
- destruct (m1 k) as [u1 |] eqn: HFnd1; destruct (m2 k) as [u2 |] eqn: HFnd2;
- [| contradiction HEq | contradiction HEq |].
- - rewrite pre_fdMap_lookup with (u := u1), pre_fdMap_lookup with (u := u2); [apply morph_resp | ..];
- assumption.
- - rewrite !pre_fdMap_lookup_nf; assumption.
- Qed.
Next Obligation.
intros m1 m2 HEq; destruct n as [| n]; [apply dist_bound |]; intros k; simpl; specialize (HEq k).
destruct (m1 k) as [u1 |] eqn: HFnd1; destruct (m2 k) as [u2 |] eqn: HFnd2; try contradiction HEq; [|].
diff --git a/lib/ModuRes/Makefile b/lib/ModuRes/Makefile
index 0affb72850ca00c0ee77db57cd4b84877446c15e..daf2da6300098798ac397093aa40456e4b5bc681 100644
--- a/lib/ModuRes/Makefile
+++ b/lib/ModuRes/Makefile
@@ -91,7 +91,6 @@ VFILES:=BI.v\
PCM.v\
Predom.v\
PreoMet.v\
- TOTInst.v\
UPred.v
-include $(addsuffix .d,$(VFILES))
diff --git a/lib/ModuRes/MetricCore.v b/lib/ModuRes/MetricCore.v
index 0e40a2d0b1ba79cf1287e6c46e6fddcc86938586..3d519e5ae6d27fe3daa195514a2e450e8cff6f80 100644
--- a/lib/ModuRes/MetricCore.v
+++ b/lib/ModuRes/MetricCore.v
@@ -192,7 +192,17 @@ Record metric_morphism T U `{mT : metric T} `{mU : metric U} :=
Arguments mkUMorph [T U eqT mT eqT0 mU] _ _.
Arguments met_morph [T U] {eqT mT eqT0 mU} _.
Infix "-n>" := metric_morphism (at level 45, right associativity).
-Notation "'n[(' f ')]'" := (mkUMorph s[(f)] _).
+
+Program Definition mkNMorph T U `{mT : metric T} `{mU : metric U} (f: T -> U)
+ (NEXP : forall n, Proper (dist n ==> dist n) f) :=
+ mkUMorph s[(f)] _.
+Next Obligation.
+ intros x y Heq.
+ eapply dist_refl. intros n.
+ eapply NEXP. rewrite Heq. reflexivity.
+Qed.
+Arguments mkNMorph [T U eqT mT eqT0 mU] _ _.
+Notation "'n[(' f ')]'" := (mkNMorph f _).
Instance subrel_dist `{mT : metric T} n : subrelation equiv (dist n).
Proof.
@@ -202,7 +212,7 @@ Qed.
Section MMInst.
Context `{mT : metric T} `{mU : metric U}.
- Global Program Instance nonexp_type : Setoid (T -n> U) :=
+ Global Program Instance nonexp_type : Setoid (T -n> U) | 5 :=
mkType (fun f g => met_morph f == g).
Next Obligation.
split.
@@ -211,7 +221,7 @@ Section MMInst.
+ intros f g h Hfg Hgh x; etransitivity; [apply Hfg | apply Hgh].
Qed.
- Global Program Instance nonexp_metric : metric (T -n> U) :=
+ Global Program Instance nonexp_metric : metric (T -n> U) | 5 :=
mkMetr (fun n f g => forall x, f x = n = g x).
Next Obligation.
intros f1 f2 EQf g1 g2 EQg; split; intros EQfg x; [symmetry in EQf, EQg |];
@@ -409,9 +419,6 @@ Section Iteration.
Next Obligation.
induction n; simpl; [apply _ | resp_set].
Qed.
- Next Obligation.
- induction n; simpl; [apply _ | resp_set].
- Qed.
Lemma iter_plus f m n x : iter m f (iter n f x) = iter (m + n) f x.
Proof. induction m; simpl; [reflexivity | f_equal; assumption]. Qed.
@@ -510,11 +517,6 @@ Section ChainApps.
complete metric space. *)
Program Definition fun_lub : T -n> U :=
n[(fun x => compl (fun i => σ i x))].
- Next Obligation.
- intros x y HEq; rewrite <- dist_refl; intros n.
- rewrite (nonexp_lub n); [| rewrite HEq]; reflexivity.
- Qed.
- Next Obligation. exact (nonexp_lub n). Qed.
End ChainApps.
@@ -522,7 +524,7 @@ Section NonexpCMetric.
Context `{cT : cmetric T} `{cU : cmetric U}.
(** THe set of non-expansive morphisms between two complete metric spaces is again a complete metric space. *)
- Global Program Instance nonexp_cmetric : cmetric (T -n> U) :=
+ Global Program Instance nonexp_cmetric : cmetric (T -n> U) | 5 :=
mkCMetr fun_lub.
Next Obligation.
intros n; exists n; intros m HLe x.
@@ -830,10 +832,6 @@ Section Exponentials.
intros [a1 b1] [a2 b2] [Ha Hb]; simpl in *.
rewrite Ha, Hb; reflexivity.
Qed.
- Next Obligation.
- intros [a1 b1] [a2 b2] [Ha Hb]; simpl in *.
- rewrite Ha, Hb; reflexivity.
- Qed.
Program Definition curryM (f : T * U -n> V) : T -n> U -n> V := lift2m (mcurry f) _ _.
diff --git a/lib/ModuRes/PreoMet.v b/lib/ModuRes/PreoMet.v
index 87b11b3d62bc447279f2449a76aa840b70f76c7e..8332dbc270135f981758c66d5041ba80e96e4c3c 100644
--- a/lib/ModuRes/PreoMet.v
+++ b/lib/ModuRes/PreoMet.v
@@ -114,9 +114,6 @@ Section PUMMorphProps1.
Next Obligation.
intros x y HEq t; apply HEq.
Qed.
- Next Obligation.
- intros f g HEq t; apply HEq.
- Qed.
Program Definition PMCompl (σ : chain (T -m> U)) (σc : cchain σ) :=
mkMUMorph (compl (liftc mu_morph_ne σ)) _.
diff --git a/lib/ModuRes/TOTInst.v b/lib/ModuRes/TOTInst.v
deleted file mode 100644
index f0dc42b522dfcfc3efca6b7984f18a5fd98e0bf0..0000000000000000000000000000000000000000
--- a/lib/ModuRes/TOTInst.v
+++ /dev/null
@@ -1,452 +0,0 @@
-Require Import CSetoid.
-
-Require Import Relation_Definitions.
-
-Require Import MetricCore.
-
-Require Import MetricRec.
-
-Record Object : Type :=
- {
- obj :> nat -> Type;
- obj_eq : forall n, relation (obj n);
- obj_eq_equiv : forall n, Equivalence (obj_eq n);
- restr : forall n, obj (S n) -> obj n;
- restr_proper : forall n, Proper (obj_eq (S n) ==> obj_eq n) (restr n)
- }.
-
-Infix "≡" := (obj_eq _ _) (at level 70, no associativity).
-
-Program Instance Object_Equiv (X : Object) (n : nat) : Equivalence (obj_eq X n) := obj_eq_equiv X n.
-
-Program Instance Object_Setoid (X : Object) (n : nat) : Setoid (X n) :=
- {| equiv := obj_eq X n |}.
-
-Record Morphism (X Y : Object) : Type :=
- {
- morph :> forall n, X n -> Y n;
- morph_proper : forall n, Proper (obj_eq _ _ ==> obj_eq _ _) (morph n);
- morph_natural : forall n, forall (x : X (S n)), restr _ _ (morph _ x) ≡ morph _ (restr _ _ x)
- }.
-
-Infix "â†" := Morphism (at level 71, right associativity).
-
-Definition Morphism_Eq (X Y : Object): relation (X ↠Y).
- intros α β.
- destruct α as [f _ _] ; destruct β as [g _ _].
- exact (forall n, forall x, f n x ≡ g n x).
-Defined.
-
-Program Instance Morphism_Eq_Equivalence {X Y : Object}: Setoid (X ↠Y) :=
- {| equiv := (Morphism_Eq X Y);
- setoid_equiv := Build_Equivalence _ _ _ _ _
- |}.
-Next Obligation.
- intros [α αp αn] n x; simpl ; intuition.
-Defined.
-Next Obligation.
- intros [α αp αn] [β βp βn] Heq n; simpl ; symmetry ; auto.
-Defined.
-Next Obligation.
- intros [α αp αn] [β βp βn] [γ γp γn] Heq1 Heq2 n; etransitivity ; auto.
-Defined.
-
-Definition morph_dist (X Y : Object): nat -> X ↠Y -> _ :=
- fun n α β => forall k, k < n -> forall (x : X k), α k x ≡ β k x.
-
-Program Instance morph_metric {X Y : Object}: @metric (X ↠Y) (@Morphism_Eq_Equivalence X Y) :=
- {| dist := morph_dist X Y |}.
-Next Obligation.
- intros α β Hαβ γ δ Hγδ ; split ; intro Heq ;
- destruct α as [α αp αn] ; destruct β as [β βp βn] ; destruct γ as [γ γp γn] ; destruct δ as [δ δp δn] ;
- intros k Hlt x ; simpl ;
- assert (Hmid := Heq k Hlt x); assert (Hleft := Hαβ k x) ; assert (Hright := Hγδ k x) ; simpl in * ;
- destruct (obj_eq_equiv Y k) as [r s t] ; eauto.
-Defined.
-Next Obligation.
- destruct x as [α αp αn] ; destruct y as [β βp βn].
- split ; intros H n.
- - intros x ; assert (HH := (H (S n) n (le_n _) x)) ; auto.
- - intros m Hleq x ; apply H.
-Defined.
-Next Obligation.
- intros α β Hαβ k Hleq x.
- assert (Hn := Hαβ k Hleq x).
- symmetry ; auto.
-Defined.
-Next Obligation.
- intros α β γ Hαβ Hβγ k Hleq x.
- assert (H1 := Hαβ k Hleq x).
- assert (H2 := Hβγ k Hleq x).
- etransitivity ; auto.
-Defined.
-Next Obligation.
- intros k Hleq ; apply H ; auto.
-Defined.
-Next Obligation.
- intros k Hq ; inversion Hq.
-Defined.
-
-Program Instance morph_metric_compl {X Y : Object}: @cmetric (X ↠Y) _ (@morph_metric X Y) :=
- {| compl := fun σ Hcauchy =>
- {| morph := fun n x => σ (S (S n)) n x; (* This works because a Cauchy chain requires very
- strong convergence in this formalization *)
- morph_proper := _;
- morph_natural := fun n x => _
- |}
- |}.
-Next Obligation.
- destruct (σ (S (S n))) as [α αp αr] ; apply αp.
-Defined.
-Next Obligation.
- remember (σ (S (S n))) as σn ; destruct σn as [α αp αr] ; simpl.
- remember (σ (S (S (S n)))) as σSn ; destruct σSn as [β βp βr] ; simpl.
- destruct (obj_eq_equiv Y n) as [r s t].
- assert ((β n (restr X n x)) ≡ restr Y n (α (S n) x)).
- assert (α (S n) x ≡ β (S n) x).
- assert (forall y, α y = (σ (S (S n))) y) as Heqασ' by (intro y; rewrite <- Heqσn ; auto).
- rewrite Heqασ'.
- assert (forall y, β y = (σ (S (S (S n)))) y) as HeqαSσ' by (intro y; rewrite <- HeqσSn ; auto).
- rewrite HeqαSσ'.
- apply (Hcauchy _ _ _ _) ; auto.
- assert (HH := restr_proper Y n _ _ H) ; eauto.
- eapply (t _ _ _ (βr _ _) (t _ _ _ H (αr _ _))).
-Defined.
-Next Obligation.
- intros n.
- exists (S n) ; intros i Hi k Hlt x ; simpl.
- assert (S (S k) <= i) as Hleq by omega.
- assert (k < S (S k)) as Hlt' by omega.
- exact (σc (S (S k)) (S (S k)) i (le_n _) Hleq k Hlt' _).
-Defined.
-
-Program Definition comp {X Y Z : Object} (α : X ↠Y) (β : Y ↠Z): (X ↠Z) :=
- {| morph := fun n x => β _ (α _ x);
- morph_proper := fun n => _;
- morph_natural := fun n x => _
- |}.
-Next Obligation.
- destruct α as [α αp αr] ; destruct β as [β βp βr].
- intros x x' Heq ; apply βp ; apply αp ; auto.
-Defined.
-Next Obligation.
- destruct α as [α αp αr] ; destruct β as [β βp βr] ; simpl.
- etransitivity ; auto.
- apply βp ; auto.
-Defined.
-
-Program Instance comp_proper {X Y Z : Object}: Proper (Morphism_Eq X Y ==> Morphism_Eq Y Z ==> Morphism_Eq X Z) comp.
-Next Obligation.
- intros α β Heqαβ γ δ Heqγδ n x.
- destruct γ as [γ γp γr] ; destruct α as [α αp αr] ;
- destruct β as [β βp βr] ; destruct δ as [δ δp δr] ; simpl in *.
- etransitivity.
- - apply (γp n _ _ (Heqαβ n x)).
- - apply (Heqγδ _ _).
-Defined.
-
-Program Definition comp_metric_morph (X Y Z : Object): (X ↠Y) -n> (Y ↠Z) -n> (X ↠Z) :=
- {| met_morph := {| CSetoid.morph := fun α => {| met_morph := {| CSetoid.morph := comp α ;
- morph_resp := _
- |};
- met_morph_nonexp := _
- |};
- morph_resp := _
- |};
- met_morph_nonexp := fun n α α' Hαα' => _
- |}.
-Next Obligation.
- apply comp_proper, Morphism_Eq_Equivalence.
-Defined.
-Next Obligation.
- intros β γ Hβγ k Hlt x ; simpl ; auto.
-Defined.
-Next Obligation.
- intros α β Hαβ γ n x.
- destruct γ as [γ γp γr] ; simpl ; apply γp.
- destruct α as [α αp αr] ; destruct β as [β βp βr] ; auto.
-Defined.
-Next Obligation.
- intros k Hlt y ; simpl.
- destruct x as [β βp βr] ; apply βp ; auto.
-Defined.
-
-Program Definition hom_cmtyp (X Y : Object): cmtyp :=
- {| cmm := {| mtyp := {| eqtyp := X ↠Y;
- eqtype := Morphism_Eq_Equivalence
- |};
- mmetr := morph_metric
- |};
- iscm := _
- |}.
-
-Instance hom_BC_morph : BC_morph Object := hom_cmtyp.
-
-(* Terminal object *)
-Program Instance One : BC_term Object :=
- {| tto :=
- {| obj := fun n => unit;
- obj_eq := fun n => @eq unit
- |}
- |}.
-Next Obligation.
- intuition.
-Defined.
-
-Program Instance morph_One : BC_terminal Object :=
- fun X => {| morph := fun n x => tt |}.
-Next Obligation.
- intro ; auto.
-Defined.
-
-Program Instance morph_Comp : BC_comp Object :=
- fun X Y Z => mkUMorph (mkMorph (fun α => mkUMorph (mkMorph (fun β => comp β α) _) _) _) _.
-Next Obligation.
- intros β γ Heqβγ n x.
- destruct γ as [γ γp γr] ; destruct α as [α αp αr] ;
- destruct β as [β βp βr] ; simpl ; apply αp ; auto.
-Defined.
-Next Obligation.
- intros β γ Heqβγ k Hlt x ; simpl.
- destruct γ as [γ γp γr] ; destruct α as [α αp αr] ;
- destruct β as [β βp βr] ; simpl ; apply αp ; auto.
-Defined.
-Next Obligation.
- intros α α' Heqαα' β n x.
- destruct α' as [α' α'p α'r] ; destruct α as [α αp αr] ;
- destruct β as [β βp βr] ; simpl ; auto.
-Defined.
-Next Obligation.
- intros β γ Heqβγ δ k Hlt x ; simpl.
- destruct γ as [γ γp γr] ; destruct δ as [δ δp δr] ;
- destruct β as [β βp βr] ; simpl ; auto.
-Defined.
-
-Program Instance morph_id : BC_id Object :=
- fun X => {| morph := fun n x => x |}.
-Next Obligation.
- intros x x' ; auto.
-Defined.
-Next Obligation.
- reflexivity.
-Defined.
-
-Program Instance TOT : BaseCat Object :=
- {| tcomp_assoc := fun X Y Z W => _;
- tid_left := fun X Y α => _;
- tid_right := fun X Y α => _;
- tto_term_unique := fun X α β => _ |}.
-Next Obligation.
- reflexivity.
-Defined.
-Next Obligation.
- destruct α as [α αp αr] ; simpl ; reflexivity.
-Defined.
-Next Obligation.
- destruct α as [α αp αr] ; simpl ; reflexivity.
-Defined.
-Next Obligation.
- destruct α as [α αp αr] ; destruct β as [β βp βr] ; intros n x.
- destruct (α n x) ; destruct (β n x) ; reflexivity.
-Defined.
-
-Module TOTMcat <: MCat.
- Definition M := Object.
- Definition MArr : BC_morph M := _.
- Definition MTermO : BC_term M := _.
- Definition MTermA : BC_terminal M := _.
- Definition MComp : BC_comp M := _.
- Definition MId : BC_id M := _.
- Definition Cat : BaseCat M := _.
-
- Program Definition Lim_Object (T : Tower) : Object :=
- {| obj := fun n => { x : forall k, tow_objs T k n | forall k, tow_morphs T k n (x (S k)) ≡ x k };
- obj_eq := fun n u v => let (x, _) := u in
- let (y, _) := v in forall k, x k ≡ y k |}.
- Next Obligation.
- apply Build_Equivalence.
- intros u ; destruct u as [x Px] ; intros k ; reflexivity.
- intros u v H ; destruct u as [x Px] ; destruct v as [y Py] ; intros k ; symmetry ; auto.
- intros u v w H1 H2 ; destruct u as [x Px] ; destruct v as [y Py] ; destruct w as [z Pz] ;
- intros k ; etransitivity ; auto.
- Defined.
- Next Obligation.
- exists (fun k => restr (tow_objs T _) _ (X k)) ; intros k ; assert (Hk := H k).
- destruct (tow_morphs T k) as [α αp αr].
- symmetry ; etransitivity.
- - apply restr_proper.
- symmetry ; eassumption.
- - eauto.
- Defined.
- Next Obligation.
- intros [x Px] [y Py] Heq k.
- apply restr_proper ; auto.
- Defined.
-
- Program Definition AllLimits : forall T, Limit T :=
- fun T => {| lim_cone := {| cone_t := Lim_Object T;
- cone_m := fun i => {| morph := fun n u => let (x, _) := u in x i |} |};
- lim_exists := fun C => {| morph := fun n Xn => exist _ (fun k => cone_m _ C k _ Xn) _ |}
- |}.
- Next Obligation.
- intros [x Px] [y Py] Heq ; auto.
- Defined.
- Next Obligation.
- reflexivity.
- Defined.
- Next Obligation.
- assert (HC := cone_m_com T C k).
- destruct (cone_m T C k) as [α αp αr] ; auto.
- Defined.
- Next Obligation.
- intros u v Heq k ; apply morph_proper ; auto.
- Defined.
- Next Obligation.
- apply morph_natural.
- Defined.
- Next Obligation.
- remember (cone_m T C n) as cn.
- destruct cn as [β βp βr] ; intros k x ; simpl.
- rewrite <- Heqcn.
- reflexivity.
- Defined.
- Next Obligation.
- destruct h as [α αp αr] ; intros n x ; simpl.
- remember (α n x) as αnx.
- simpl in HEq ; destruct αnx as [u Pu] ; intros k.
- assert (HEqk := HEq k) ; clear HEq.
- destruct (cone_m T C k) as [β βp βr] ; simpl in HEqk ; simpl.
- assert (HEqnx := HEqk n x) ; rewrite <- Heqαnx in HEqnx.
- symmetry ; auto.
- Defined.
-End TOTMcat.
-
-
-(* Example of the stream functor, F(X) = N × ▸X *)
-
-Module StreamFunctor : InputType(TOTMcat).
- Import TOTMcat.
-
- Program Definition Prod (X Y : Object): Object :=
- {| obj := fun n => X n * Y n;
- obj_eq := fun n p q => let (x, y) := p in
- let (x', y') := q in
- x ≡ x' /\ y ≡ y';
- restr := fun n p => let (x, y) := p in
- (restr _ _ x, restr _ _ y)
- |}%type.
- Next Obligation.
- apply Build_Equivalence.
- intros p ; destruct p ; split ; reflexivity.
- intros p q; destruct p ; destruct q ; intuition.
- intros [x y] [x' y'] [x'' y''] ; intuition ; etransitivity ; eauto.
- Defined.
- Next Obligation.
- intros [x y] [z w] ; intuition ; apply restr_proper ; auto.
- Defined.
-
- Program Definition Nat : Object :=
- {| obj := fun n => nat;
- restr := fun n x => x;
- obj_eq := fun n => eq
- |}.
- Next Obligation.
- apply Build_Equivalence ; intuition.
- Defined.
-
- Program Definition Later (X : Object) : Object :=
- {| obj := fun n => match n with
- | O => unit
- | S m => X m
- end;
- restr := fun n => match n with
- | O => fun x => tt
- | S m => restr X m
- end;
- obj_eq := fun n => match n with
- | O => eq
- | S m => obj_eq X m
- end
- |}.
- Next Obligation.
- assert (H := obj_eq_equiv X).
- apply Build_Equivalence ; destruct n ; intuition.
- Defined.
- Next Obligation.
- intros x y Heq ; destruct n ; auto ; apply restr_proper ; auto.
- Defined.
-
- Program Definition next (X : Object): X ↠Later X :=
- {| morph := fun n x => match n with
- | O => tt
- | S m => restr X m x
- end
- |}.
- Next Obligation.
- intros x y Heq ; destruct n ; auto ; apply restr_proper ; auto.
- Defined.
- Next Obligation.
- destruct n ; eauto ; reflexivity.
- Defined.
-
- Program Definition F : M -> M -> M :=
- fun Xm Xp => Prod Nat (Later Xp).
-
- Program Definition Fmorph (X Y Z W : Object) (fs : (Y -t> X) * (Z -t> W)): forall n, F X Z n -> F Y W n :=
- fun k p => let (α, β) := fs in let (n, x) := p in (n, _).
- Next Obligation.
- destruct k.
- exact x.
- exact (β _ x).
- Defined.
-
- Program Definition FArr : BiFMap F :=
- fun X Y Z W => n[(fun fs => {| morph := Fmorph X Y Z W fs |})].
- Next Obligation.
- intros [â„“ x] [k y] Heq ; destruct n ; simpl ; intuition.
- apply morph_proper ; auto.
- Defined.
- Next Obligation.
- destruct n ; simpl ; intuition.
- apply morph_natural.
- Defined.
- Next Obligation.
- intros [â„“ x] [k y] [_ Heqxy] ; destruct n ; simpl ; [tauto | intros [a b]]; simpl.
- unfold snd in Heqxy; destruct x as [α αp αr] ; destruct y as [β βp βr] ; auto.
- Defined.
- Next Obligation.
- intros [â„“ x] [k y] [_ Heq] m Hlt [o u] ; destruct m ; simpl ; intuition.
- Defined.
-
- Program Definition FFun : @BiFunctor _ _ _ _ F FArr :=
- {| fmorph_comp := fun X Y Z W U V f g h k => _;
- fmorph_id := fun X Y => _
- |}.
- Next Obligation.
- destruct n ; simpl ; intuition.
- Defined.
- Next Obligation.
- destruct n ; simpl ; intuition.
- Defined.
-
- Program Definition tmorph_ne_fun n : One n -> F One One n :=
- fun _ => match n with
- | O => (O, tt)
- | S n => (O, tt)
- end.
-
- (* Program Definition does not work, that is, it gets confused for some reason. *)
- Definition tmorph_ne : 1 -t> (F 1 1).
- refine (Build_Morphism _ _ tmorph_ne_fun _ _).
- - intros n x ; destruct n ; simpl ; intuition.
- Defined.
-
- Theorem F_contractive : forall {m0 m1 m2 m3 : M}, contractive (@fmorph _ hom_BC_morph F FArr m0 m1 m2 m3).
- Proof.
- intros X Y Z W n [z [α αp αr]] [w [β βp βr]] Heq k Lt [ℓ x] ; simpl ; destruct k ; intuition.
- assert (k < n) as Hkn by auto with arith.
- destruct Heq as [_ Heq] ; assert (Heqk := Heq k Hkn x) ; auto.
- Defined.
-End StreamFunctor.
-
-Module Streams := Solution TOTMcat StreamFunctor.
diff --git a/world_prop.v b/world_prop.v
index be2fd5e60f23e06ba605ab6b9c6f161570eb30e4..22f7d0caf4859f98be95666eb061539d2adb4737 100644
--- a/world_prop.v
+++ b/world_prop.v
@@ -72,10 +72,6 @@ Module WorldProp (Res : PCM_T) : WORLD_PROP Res.
intros m1 m2 Eqm; unfold PropMorph, equiv in *.
rewrite Eqm; reflexivity.
Qed.
- Next Obligation.
- intros m1 m2 Eqm; unfold PropMorph.
- rewrite Eqm; reflexivity.
- Qed.
Instance FFun : BiFunctor F.
Proof.