From 25c7e78b4bf8ca947f7b1b366276165244bfd5f7 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 24 Feb 2015 17:36:18 +0100
Subject: [PATCH] re-establish the well-definedness of our core logic
---
iris_core.v | 31 ++++++-------
iris_plog.v | 81 ++++++++++++++++------------------
lib/ModuRes/RA.v | 104 ++------------------------------------------
world_prop.v | 4 +-
world_prop_recdom.v | 4 +-
5 files changed, 58 insertions(+), 166 deletions(-)
diff --git a/iris_core.v b/iris_core.v
index 5609f3f44..428e36cf4 100644
--- a/iris_core.v
+++ b/iris_core.v
@@ -73,7 +73,7 @@ Module Type IRIS_CORE (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
(** And now we're ready to build the IRIS-specific connectives! *)
- Implicit Types (P Q : Props) (w : Wld) (n i k : nat) (m : mask) (r : pres) (u v : res) (σ : state).
+ Implicit Types (P Q : Props) (w : Wld) (n i k : nat) (m : mask) (r u v : res) (σ : state).
Section Necessitation.
(** Note: this could be moved to BI, since it's possible to define
@@ -82,7 +82,7 @@ Module Type IRIS_CORE (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
Local Obligation Tactic := intros; resp_set || eauto with typeclass_instances.
Program Definition box : Props -n> Props :=
- n[(fun P => m[(fun w => mkUPred (fun n r => P w n ra_pos_unit) _)])].
+ n[(fun P => m[(fun w => mkUPred (fun n r => P w n 1) _)])].
Next Obligation.
intros n m r s HLe _ Hp; rewrite-> HLe; assumption.
Qed.
@@ -129,11 +129,20 @@ Module Type IRIS_CORE (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
intros w n r; reflexivity.
Qed.
+ Lemma box_dup P :
+ â–¡P == â–¡P * â–¡P.
+ Proof.
+ intros w n r. split.
+ - intros HP. exists 1 r. split; [now rewrite ra_op_unit|].
+ split; assumption.
+ - intros [r1 [r2 [_ [HP _] ] ] ]. assumption.
+ Qed.
+
(** "Internal" equality **)
Section IntEq.
Context {T} `{mT : metric T}.
- Program Definition intEqP (t1 t2 : T) : UPred pres :=
+ Program Definition intEqP (t1 t2 : T) : UPred res :=
mkUPred (fun n r => t1 = S n = t2) _.
Next Obligation.
intros n1 n2 _ _ HLe _; apply mono_dist; omega.
@@ -196,9 +205,9 @@ Module Type IRIS_CORE (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
Note that this makes ownR trivially *False* for invalid u: There is no
element v such that u · v = r (where r is valid) *)
Program Definition ownR: res -=> Props :=
- s[(fun u => pcmconst (mkUPred(fun n r => u ⊑ ra_proj r) _) )].
+ s[(fun u => pcmconst (mkUPred(fun n r => u ⊑ r) _) )].
Next Obligation.
- intros n m r1 r2 Hle [d Hd ] [e He]. change (u ⊑ (ra_proj r2)). rewrite <-Hd, <-He.
+ intros n m r1 r2 Hle [d Hd ] [e He]. change (u ⊑ r2). rewrite <-Hd, <-He.
exists (d · e). rewrite assoc. reflexivity.
Qed.
Next Obligation.
@@ -214,8 +223,7 @@ Module Type IRIS_CORE (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
Proof.
intros w n r; split; [intros Hut | intros [r1 [r2 [EQr [Hu Ht] ] ] ] ].
- destruct Hut as [s Heq]. rewrite-> assoc in Heq.
- exists↓ (s · u) by auto_valid.
- exists↓ v by auto_valid.
+ exists (s · u) v.
split; [|split].
+ rewrite <-Heq. reflexivity.
+ exists s. reflexivity.
@@ -226,13 +234,6 @@ Module Type IRIS_CORE (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
rewrite <-assoc, (comm _ u), assoc. reflexivity.
Qed.
- Lemma ownR_valid u (INVAL: ~↓u):
- ownR u ⊑ ⊥.
- Proof.
- intros w n [r VAL] [v Heq]. hnf. unfold ra_proj, proj1_sig in Heq.
- rewrite <-Heq in VAL. apply ra_op_valid2 in VAL. contradiction.
- Qed.
-
(** Proper physical state: ownership of the machine state **)
Program Definition ownS : state -n> Props :=
n[(fun s => ownR (ex_own _ s, 1))].
@@ -249,7 +250,7 @@ Module Type IRIS_CORE (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
n[(fun r : RL.res => ownR (1, r))].
Next Obligation.
intros r1 r2 EQr. destruct n as [| n]; [apply dist_bound |eapply dist_refl].
- simpl in EQr. intros w m t. simpl. change ( (ex_unit state, r1) ⊑ (ra_proj t) <-> (ex_unit state, r2) ⊑ (ra_proj t)). rewrite EQr. reflexivity.
+ simpl in EQr. intros w m t. simpl. change ( (ex_unit state, r1) ⊑ t <-> (ex_unit state, r2) ⊑ t). rewrite EQr. reflexivity.
Qed.
Lemma ownL_timeless {r : RL.res} : valid(timeless(ownL r)).
diff --git a/iris_plog.v b/iris_plog.v
index b6f23949b..eede7d4b0 100644
--- a/iris_plog.v
+++ b/iris_plog.v
@@ -17,14 +17,12 @@ Module Type IRIS_PLOG (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
Local Open Scope bi_scope.
Local Open Scope iris_scope.
- Implicit Types (P : Props) (w : Wld) (n i k : nat) (m : mask) (r : pres) (u v : res) (σ : state) (φ : vPred).
-
-
+ Implicit Types (P : Props) (w : Wld) (n i k : nat) (m : mask) (r u v : res) (σ : state) (φ : vPred).
Section Invariants.
(** Invariants **)
- Definition invP i P w : UPred pres :=
+ Definition invP i P w : UPred res :=
intEqP (w i) (Some (ı' P)).
Program Definition inv i : Props -n> Props :=
n[(fun P => m[(invP i P)])].
@@ -55,10 +53,10 @@ Module Type IRIS_PLOG (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
constructs. Hopefully we can provide a fold that'd work for
that at some point
*)
- Fixpoint comp_list (xs : list pres) : res :=
+ Fixpoint comp_list (xs : list res) : res :=
match xs with
| nil => 1
- | (x :: xs)%list => ra_proj x · comp_list xs
+ | (x :: xs)%list => x · comp_list xs
end.
Lemma comp_list_app rs1 rs2 :
@@ -68,45 +66,45 @@ Module Type IRIS_PLOG (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
now rewrite ->IHrs1, assoc.
Qed.
- Definition cod (m : nat -f> pres) : list pres := List.map snd (findom_t m).
- Definition comp_map (m : nat -f> pres) : res := comp_list (cod m).
+ Definition cod (m : nat -f> res) : list res := List.map snd (findom_t m).
+ Definition comp_map (m : nat -f> res) : res := comp_list (cod m).
- Lemma comp_map_remove (rs : nat -f> pres) i r (HLu : rs i == Some r) :
- comp_map rs == ra_proj r · comp_map (fdRemove i rs).
+ Lemma comp_map_remove (rs : nat -f> res) i r (HLu : rs i == Some r) :
+ comp_map rs == r · comp_map (fdRemove i rs).
Proof.
destruct rs as [rs rsP]; unfold comp_map, cod, findom_f in *; simpl findom_t in *.
induction rs as [| [j s] ]; [contradiction |]; simpl comp_list; simpl in HLu.
- destruct (comp i j); [do 5 red in HLu; rewrite-> HLu; reflexivity | contradiction |].
+ destruct (comp i j); [red in HLu; rewrite-> HLu; reflexivity | contradiction |].
simpl comp_list; rewrite ->IHrs by eauto using SS_tail.
- rewrite-> !assoc, (comm (_ s)); reflexivity.
+ rewrite-> !assoc, (comm s). reflexivity.
Qed.
- Lemma comp_map_insert_new (rs : nat -f> pres) i r (HNLu : rs i == None) :
- ra_proj r · comp_map rs == comp_map (fdUpdate i r rs).
+ Lemma comp_map_insert_new (rs : nat -f> res) i r (HNLu : rs i == None) :
+ r · comp_map rs == comp_map (fdUpdate i r rs).
Proof.
destruct rs as [rs rsP]; unfold comp_map, cod, findom_f in *; simpl findom_t in *.
induction rs as [| [j s] ]; [reflexivity | simpl comp_list; simpl in HNLu].
destruct (comp i j); [contradiction | reflexivity |].
simpl comp_list; rewrite <- IHrs by eauto using SS_tail.
- rewrite-> !assoc, (comm (_ r)); reflexivity.
+ rewrite-> !assoc, (comm r); reflexivity.
Qed.
- Lemma comp_map_insert_old (rs : nat -f> pres) i r1 r2 r
- (HLu : rs i == Some r1) (HEq : ra_proj r1 · ra_proj r2 == ra_proj r) :
- ra_proj r2 · comp_map rs == comp_map (fdUpdate i r rs).
+ Lemma comp_map_insert_old (rs : nat -f> res) i r1 r2 r
+ (HLu : rs i == Some r1) (HEq : r1 · r2 == r):
+ r2 · comp_map rs == comp_map (fdUpdate i r rs).
Proof.
destruct rs as [rs rsP]; unfold comp_map, cod, findom_f in *; simpl findom_t in *.
induction rs as [| [j s] ]; [contradiction |]; simpl comp_list; simpl in HLu.
- destruct (comp i j); [do 5 red in HLu; rewrite-> HLu; clear HLu | contradiction |].
- - simpl comp_list; rewrite ->assoc, (comm (_ r2)), <- HEq; reflexivity.
+ destruct (comp i j); [red in HLu; rewrite-> HLu; clear HLu | contradiction |].
+ - simpl comp_list; rewrite ->assoc, (comm r2), <- HEq; reflexivity.
- simpl comp_list; rewrite <- IHrs by eauto using SS_tail.
- rewrite-> !assoc, (comm (_ r2)); reflexivity.
+ rewrite-> !assoc, (comm r2); reflexivity.
Qed.
Definition state_sat (r: res) σ: Prop := ↓r /\
match fst r with
| ex_own s => s = σ
- | _ => True
+ | _ => True (* We don't care. Note that validity is ensured independently *)
end.
Global Instance state_sat_dist : Proper (equiv ==> equiv ==> iff) state_sat.
@@ -117,7 +115,7 @@ Module Type IRIS_PLOG (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
Global Instance preo_unit : preoType () := disc_preo ().
Program Definition wsat σ m (r : res) w : UPred () :=
- â–¹ (mkUPred (fun n _ => exists rs : nat -f> pres,
+ â–¹ (mkUPred (fun n _ => exists rs : nat -f> res,
state_sat (r · (comp_map rs)) σ
/\ forall i (Hm : m i),
(i ∈ dom rs <-> i ∈ dom w) /\
@@ -198,10 +196,10 @@ Module Type IRIS_PLOG (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
Section ViewShifts.
Local Obligation Tactic := intros.
- Program Definition preVS m1 m2 P w : UPred pres :=
+ Program Definition preVS m1 m2 P w : UPred res :=
mkUPred (fun n r => forall w1 (rf: res) mf σ k (HSub : w ⊑ w1) (HLe : k < n)
(HD : mf # m1 ∪ m2)
- (HE : wsat σ (m1 ∪ mf) (ra_proj r · rf) w1 @ S k),
+ (HE : wsat σ (m1 ∪ mf) (r · rf) w1 @ S k),
exists w2 r',
w1 ⊑ w2 /\ P w2 (S k) r'
/\ wsat σ (m2 ∪ mf) (r' · rf) w2 @ S k) _.
@@ -210,10 +208,9 @@ Module Type IRIS_PLOG (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
destruct (HP w1 (rd · rf) mf σ k) as [w2 [r1' [HW [HP' HE'] ] ] ];
try assumption; [now eauto with arith | |].
- eapply wsat_equiv, HE; try reflexivity.
- rewrite ->assoc, (comm (_ r1)), HR; reflexivity.
- - rewrite ->assoc, (comm (_ r1')) in HE'.
- exists w2. exists↓ (rd · ra_proj r1').
- { apply wsat_valid in HE'. auto_valid. }
+ rewrite ->assoc, (comm r1), HR; reflexivity.
+ - rewrite ->assoc, (comm r1') in HE'.
+ exists w2 (rd · r1').
split; [assumption | split; [| assumption] ].
eapply uni_pred, HP'; [reflexivity|]. exists rd. reflexivity.
Qed.
@@ -277,19 +274,19 @@ Module Type IRIS_PLOG (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
Definition wpFP safe m (WP : expr -n> vPred -n> Props) e φ w n r :=
forall w' k rf mf σ (HSw : w ⊑ w') (HLt : k < n) (HD : mf # m)
- (HE : wsat σ (m ∪ mf) (ra_proj r · rf) w' @ S k),
+ (HE : wsat σ (m ∪ mf) (r · rf) w' @ S k),
(forall (HV : is_value e),
exists w'' r', w' ⊑ w'' /\ φ (exist _ e HV) w'' (S k) r'
- /\ wsat σ (m ∪ mf) (ra_proj r' · rf) w'' @ S k) /\
+ /\ wsat σ (m ∪ mf) (r' · rf) w'' @ S k) /\
(forall σ' ei ei' K (HDec : e = K [[ ei ]])
(HStep : prim_step (ei, σ) (ei', σ')),
exists w'' r', w' ⊑ w'' /\ WP (K [[ ei' ]]) φ w'' k r'
- /\ wsat σ' (m ∪ mf) (ra_proj r' · rf) w'' @ k) /\
+ /\ wsat σ' (m ∪ mf) (r' · rf) w'' @ k) /\
(forall e' K (HDec : e = K [[ fork e' ]]),
exists w'' rfk rret, w' ⊑ w''
/\ WP (K [[ fork_ret ]]) φ w'' k rret
/\ WP e' (umconst ⊤) w'' k rfk
- /\ wsat σ (m ∪ mf) (ra_proj rfk · ra_proj rret · rf) w'' @ k) /\
+ /\ wsat σ (m ∪ mf) (rfk · rret · rf) w'' @ k) /\
(forall HSafe : safe = true, safeExpr e σ).
(* Define the function wp will be a fixed-point of *)
@@ -302,27 +299,23 @@ Module Type IRIS_PLOG (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
[| omega | ..]; try assumption; [].
split; [clear HS HF | split; [clear HV HF | split; clear HV HS; [| clear HF ] ] ]; intros.
- specialize (HV HV0); destruct HV as [w'' [r1' [HSw' [Hφ HE'] ] ] ].
- rewrite ->assoc, (comm (_ r1')) in HE'.
- exists w''. exists↓ (rd · ra_proj r1').
- { clear -HE'. apply wsat_valid in HE'. auto_valid. }
+ rewrite ->assoc, (comm r1') in HE'.
+ exists w'' (rd · r1').
split; [assumption | split; [| assumption] ].
eapply uni_pred, Hφ; [| exists rd]; reflexivity.
- specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r1' [HSw' [HWP HE'] ] ] ].
- rewrite ->assoc, (comm (_ r1')) in HE'. exists w''.
+ rewrite ->assoc, (comm r1') in HE'. exists w''.
destruct k as [| k]; [exists r1'; simpl wsat; tauto |].
- exists↓ (rd · ra_proj r1').
- { clear- HE'. apply wsat_valid in HE'. auto_valid. }
+ exists (rd · r1').
split; [assumption | split; [| assumption] ].
eapply uni_pred, HWP; [| exists rd]; reflexivity.
- specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret1 [HSw' [HWR [HWF HE'] ] ] ] ] ].
destruct k as [| k]; [exists w'' rfk rret1; simpl wsat; tauto |].
- rewrite ->assoc, <- (assoc (_ rfk)) in HE'.
- exists w''. exists rfk. exists↓ (rd · ra_proj rret1).
- { clear- HE'. apply wsat_valid in HE'. rewrite comm. eapply ra_op_valid, ra_op_valid; try now apply _.
- rewrite ->(comm (_ rfk)) in HE'. eassumption. }
+ rewrite ->assoc, <- (assoc rfk) in HE'.
+ exists w''. exists rfk (rd · rret1).
repeat (split; try assumption).
+ eapply uni_pred, HWR; [| exists rd]; reflexivity.
- + clear -HE'. unfold ra_proj. rewrite ->(comm _ rd) in HE'. exact HE'.
+ + clear -HE'. rewrite ->(comm _ rd) in HE'. exact HE'.
- auto.
Qed.
Next Obligation.
diff --git a/lib/ModuRes/RA.v b/lib/ModuRes/RA.v
index 74b939e96..1b88f573c 100644
--- a/lib/ModuRes/RA.v
+++ b/lib/ModuRes/RA.v
@@ -120,105 +120,9 @@ Section ProductLemmas.
End ProductLemmas.
-Section PositiveCarrier.
- Context {T} `{raT : RA T}.
-
- Definition ra_pos: Type := { t : T | ↓ t }.
- Coercion ra_proj (r:ra_pos): T := proj1_sig r.
-
- Implicit Types (t u : T) (r : ra_pos).
-
- Global Instance ra_pos_type : Setoid ra_pos := _.
-
- Definition ra_mk_pos t {VAL: ↓ t}: ra_pos := exist _ t VAL.
-
- Program Definition ra_pos_unit: ra_pos := exist _ 1 _.
- Next Obligation.
- now eapply ra_valid_unit; apply _.
- Qed.
-
- Lemma ra_proj_cancel t (VAL: ↓t):
- ra_proj (ra_mk_pos t (VAL:=VAL)) = t.
- Proof.
- reflexivity.
- Qed.
-
- Lemma ra_op_pos_valid t1 t2 r:
- t1 · t2 == ra_proj r -> ↓ t1.
- Proof.
- destruct r as [t Hval]; simpl. intros Heq. rewrite <-Heq in Hval.
- eapply ra_op_valid; eassumption.
- Qed.
-
- Lemma ra_op_pos_valid2 t1 t2 r:
- t1 · t2 == ra_proj r -> ↓ t2.
- Proof.
- rewrite comm. now eapply ra_op_pos_valid.
- Qed.
-
- Lemma ra_pos_valid r:
- ↓(ra_proj r).
- Proof.
- destruct r as [r VAL].
- exact VAL.
- Qed.
-
-End PositiveCarrier.
-Global Arguments ra_pos T {_}.
-Notation "'âº' T" := (ra_pos T) (at level 75) : type_scope.
-
-(** Validity automation tactics *)
-Ltac auto_valid_inner :=
- solve [ eapply ra_op_pos_valid; (eassumption || rewrite comm; eassumption)
- | eapply ra_op_pos_valid2; (eassumption || rewrite comm; eassumption)
- | eapply ra_op_valid; (eassumption || rewrite comm; eassumption) ].
-Ltac auto_valid := idtac; match goal with
- | |- @ra_valid ?T _ _ =>
- let H := fresh in assert (H : RA T) by apply _; auto_valid_inner
- end.
-
-(* FIXME put the common parts into a helper tactic, and allow arbitrary tactics after "by" *)
-Ltac exists_valid t tac := let H := fresh "Hval" in assert(H:(↓t)%ra); [tac|exists (ra_mk_pos t (VAL:=H) ) ].
-Tactic Notation "exists↓" constr(t) := exists_valid t idtac.
-Tactic Notation "exists↓" constr(t) "by" tactic(tac) := exists_valid t ltac:(now tac).
-
-Ltac pose_valid name t tac := let H := fresh "Hval" in assert(H:(↓t)%ra); [tac|pose (name := ra_mk_pos t (VAL:=H) ) ].
-Tactic Notation "pose↓" ident(name) ":=" constr(t) := pose_valid name t idtac.
-Tactic Notation "pose↓" ident(name) ":=" constr(t) "by" tactic(tac) := pose_valid name t ltac:(now tac).
-
-
Section Order.
Context T `{raT : RA T}.
- Implicit Types (t : T) (r s : ra_pos T).
-
- Definition pra_ord r1 r2 :=
- exists t, t · (ra_proj r1) == (ra_proj r2).
-
- Global Instance pra_ord_preo: PreOrder pra_ord.
- Proof.
- split.
- - intros x; exists 1. simpl. erewrite ra_op_unit by apply _; reflexivity.
- - intros z yz xyz [y Hyz] [x Hxyz]; unfold pra_ord.
- rewrite <- Hyz, assoc in Hxyz; setoid_rewrite <- Hxyz.
- exists (x · y). reflexivity.
- Qed.
-
- Global Program Instance pRA_preo : preoType (ra_pos T) | 0 := mkPOType pra_ord.
-
- Global Instance equiv_pord_pra : Proper (equiv ==> equiv ==> equiv) (pord (T := ra_pos T)).
- Proof.
- intros s1 s2 EQs t1 t2 EQt; split; intros [s HS].
- - exists s; rewrite <- EQs, <- EQt; assumption.
- - exists s; rewrite EQs, EQt; assumption.
- Qed.
-
- Lemma unit_min r : ra_pos_unit ⊑ r.
- Proof.
- exists (ra_proj r). simpl.
- now erewrite ra_op_unit2 by apply _.
- Qed.
-
Definition ra_ord t1 t2 :=
exists t, t · t1 == t2.
@@ -245,12 +149,10 @@ Section Order.
rewrite <- assoc, (comm y), <- assoc, assoc, (comm y1), EQx, EQy; reflexivity.
Qed.
- Lemma ord_res_pres r s :
- (r ⊑ s) <-> (ra_proj r ⊑ ra_proj s).
+ Lemma unit_min r : 1 ⊑ r.
Proof.
- split; intros HR.
- - destruct HR as [d EQ]. exists d. assumption.
- - destruct HR as [d EQ]. exists d. assumption.
+ exists r. simpl.
+ now erewrite ra_op_unit2 by apply _.
Qed.
End Order.
diff --git a/world_prop.v b/world_prop.v
index a6faa4534..cce80cff1 100644
--- a/world_prop.v
+++ b/world_prop.v
@@ -6,8 +6,6 @@ Require Import ModuRes.RA ModuRes.UPred.
(* This interface keeps some of the details of the solution opaque *)
Module Type WORLD_PROP (Res : RA_T).
- Definition pres := ra_pos Res.res.
-
(* PreProp: The solution to the recursive equation. Equipped with a discrete order. *)
Parameter PreProp : cmtyp.
Instance PProp_preo : preoType PreProp := disc_preo PreProp.
@@ -16,7 +14,7 @@ Module Type WORLD_PROP (Res : RA_T).
(* Defines Worlds, Propositions *)
Definition Wld := nat -f> PreProp.
- Definition Props := Wld -m> UPred pres.
+ Definition Props := Wld -m> UPred (Res.res).
(* Define all the things on Props, so they have names - this shortens the terms later. *)
Instance Props_ty : Setoid Props | 1 := _.
diff --git a/world_prop_recdom.v b/world_prop_recdom.v
index da2a12589..5d67bb3d5 100644
--- a/world_prop_recdom.v
+++ b/world_prop_recdom.v
@@ -7,9 +7,7 @@ Require Import world_prop.
(* Now we come to the actual implementation *)
Module WorldProp (Res : RA_T) : WORLD_PROP Res.
-
(** The construction is parametric in the monoid we choose *)
- Definition pres := ra_pos Res.res.
(** We need to build a functor that would describe the following
recursive domain equation:
@@ -25,7 +23,7 @@ Module WorldProp (Res : RA_T) : WORLD_PROP Res.
Local Instance pcm_disc P `{cmetric P} : pcmType P | 2000 := disc_pcm P.
Definition FProp P `{cmP : cmetric P} :=
- (nat -f> P) -m> UPred pres.
+ (nat -f> P) -m> UPred (Res.res).
Context {U V} `{cmU : cmetric U} `{cmV : cmetric V}.
--
GitLab