From 848ce08eca398d647f1412922c79cca41c5634a6 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 26 Feb 2015 14:26:49 +0100
Subject: [PATCH] try to play with (dist n) as equivalence relations... and
quickly stop again...
---
iris_core.v | 28 +++++++++++++---------------
iris_plog.v | 21 ++++++++++++---------
lib/ModuRes/MetricCore.v | 17 ++++++++++++++++-
lib/ModuRes/RA.v | 2 +-
4 files changed, 42 insertions(+), 26 deletions(-)
diff --git a/iris_core.v b/iris_core.v
index b6835b6b4..743d66ba2 100644
--- a/iris_core.v
+++ b/iris_core.v
@@ -139,24 +139,22 @@ Module Type IRIS_CORE (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
intros n1 n2 _ _ HLe _; apply mono_dist; omega.
Qed.
- Definition intEq (t1 t2 : T) : Props := pcmconst (intEqP t1 t2).
-
- Instance intEq_equiv : Proper (equiv ==> equiv ==> equiv) intEqP.
+ Instance subrel_dist_n `{mT : metric T} (n m: nat) (Hlt: m < n) : subrelation (dist n) (dist m).
Proof.
- intros l1 l2 EQl r1 r2 EQr n r.
- split; intros HEq; do 2 red.
- - rewrite <- EQl, <- EQr; assumption.
- - rewrite ->EQl, EQr; assumption.
+ intros x y HEq. eapply mono_dist, HEq. omega.
Qed.
- Instance intEq_dist n : Proper (dist n ==> dist n ==> dist n) intEqP.
- Proof.
- intros l1 l2 EQl r1 r2 EQr m r HLt.
- split; intros HEq; do 2 red.
- - etransitivity; [| etransitivity; [apply HEq |] ];
- apply mono_dist with n; eassumption || now auto with arith.
- - etransitivity; [| etransitivity; [apply HEq |] ];
- apply mono_dist with n; eassumption || now auto with arith.
+ Program Definition intEq: T -n> T -n> Props :=
+ n[(fun t1 => n[(fun t2 => pcmconst (intEqP t1 t2))])].
+ Next Obligation.
+ intros t2 t2' Heqt2. intros w m r HLt.
+ change ((t1 = S m = t2) <-> (t1 = S m = t2')). (* Why, oh why... *)
+ split; (etransitivity; [eassumption|]); eapply mono_dist; (eassumption || symmetry; eassumption).
+ Qed.
+ Next Obligation.
+ intros t1 t1' Heqt1. intros t2 w m r HLt.
+ change ((t1 = S m = t2) <-> (t1' = S m = t2)). (* Why, oh why... *)
+ split; (etransitivity; [|eassumption]); eapply mono_dist; (eassumption || symmetry; eassumption).
Qed.
End IntEq.
diff --git a/iris_plog.v b/iris_plog.v
index b6f23949b..1f9118f2e 100644
--- a/iris_plog.v
+++ b/iris_plog.v
@@ -25,25 +25,28 @@ Module Type IRIS_PLOG (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
(** Invariants **)
Definition invP i P w : UPred pres :=
- intEqP (w i) (Some (ı' P)).
+ intEq (w i) (Some (ı' P)) w.
Program Definition inv i : Props -n> Props :=
n[(fun P => m[(invP i P)])].
Next Obligation.
- intros w1 w2 EQw; unfold invP; simpl morph.
+ intros w1 w2 EQw; unfold invP.
destruct n; [apply dist_bound |].
- apply intEq_dist; [apply EQw | reflexivity].
+ rewrite (EQw i).
+ now eapply met_morph_nonexp.
Qed.
Next Obligation.
- intros w1 w2 Sw; unfold invP; simpl morph.
- intros n r HP; do 2 red; specialize (Sw i); do 2 red in HP.
+ intros w1 w2 Sw; unfold invP.
+ intros n r HP; specialize (Sw i).
destruct (w1 i) as [μ1 |]; [| contradiction].
- destruct (w2 i) as [μ2 |]; [| contradiction]; simpl in Sw.
+ destruct (w2 i) as [μ2 |]; [| contradiction]. simpl in Sw.
rewrite <- Sw; assumption.
Qed.
Next Obligation.
- intros p1 p2 EQp w; unfold invP; simpl morph.
- apply intEq_dist; [reflexivity |].
- apply dist_mono, (met_morph_nonexp _ _ ı'), EQp.
+ intros p1 p2 EQp w; unfold invP.
+ cut ((w i === Some (ı' p1)) = n = (w i === Some (ı' p2))).
+ { intros Heq. now eapply Heq. }
+ eapply met_morph_nonexp.
+ now eapply dist_mono, (met_morph_nonexp _ _ ı').
Qed.
End Invariants.
diff --git a/lib/ModuRes/MetricCore.v b/lib/ModuRes/MetricCore.v
index ecb555cbc..210bf9156 100644
--- a/lib/ModuRes/MetricCore.v
+++ b/lib/ModuRes/MetricCore.v
@@ -37,6 +37,15 @@ Record Mtyp :=
Instance mtyp_proj_metr {M : Mtyp} : metric M := mmetr M.
Definition mfromType (T : Type) `{mT : metric T} := Build_Mtyp (fromType T) _.
+(* And now it gets annoying that we are not fully unbundled... *)
+Global Instance metric_dist_equiv (T: Type) `{mT: metric T} n: Equivalence (dist n).
+Proof.
+ split.
+ - intros x. eapply dist_refl. reflexivity.
+ - now eapply dist_sym.
+ - now eapply dist_trans.
+Qed.
+
Section DistProps.
Context `{mT : metric T}.
@@ -193,6 +202,12 @@ 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).
+Global Instance metric_morphism_proper T U `{mT : metric T} `{mU : metric U} n (f: T -n> U):
+ Proper (dist n ==> dist n) f.
+Proof.
+ now eapply met_morph_nonexp.
+Qed.
+
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)] _.
@@ -204,7 +219,7 @@ 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).
+Instance subrel_dist `{mT : metric T} n : subrelation equiv (dist n) | 5.
Proof.
intros x y HEq; revert n; rewrite dist_refl; assumption.
Qed.
diff --git a/lib/ModuRes/RA.v b/lib/ModuRes/RA.v
index 74b939e96..695fe2139 100644
--- a/lib/ModuRes/RA.v
+++ b/lib/ModuRes/RA.v
@@ -391,7 +391,7 @@ Section InfiniteProduct.
Global Instance ra_equiv_infprod : Equivalence ra_eq_infprod.
Proof. split; repeat intro; [ | rewrite (H i) | rewrite (H i), (H0 i) ]; reflexivity. Qed.
- Global Instance ra_type_infprod : Setoid ra_res_infprod := mkType ra_eq_infprod.
+ Global Instance ra_type_infprod : Setoid ra_res_infprod | 5 := mkType ra_eq_infprod.
Global Instance ra_unit_infprod : RA_unit _ := fun i => ra_unit (S i).
Global Instance ra_op_infprod : RA_op _ := fun f g i => f i · g i.
Global Instance ra_valid_infprod : RA_valid _ := fun f => forall i, ra_valid (f i).
--
GitLab