Commit c5fc5262 authored by Ralf Jung's avatar Ralf Jung

improve n[] notation for nonexpansive maps: the proof of Proper is no longer...

improve n[] notation for nonexpansive maps: the proof of Proper is no longer required, it can be derived from nonexpansiveness
parent fd002a30
......@@ -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.
......
......@@ -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] ].
......
......@@ -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.
......
......@@ -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.
......@@ -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; [|].
......
......@@ -91,7 +91,6 @@ VFILES:=BI.v\
PCM.v\
Predom.v\
PreoMet.v\
TOTInst.v\
UPred.v
-include $(addsuffix .d,$(VFILES))
......
......@@ -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) _ _.
......
......@@ -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 σ)) _.
......
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.