diff --git a/iris_core.v b/iris_core.v
index e51560d5167a31603e016ba65c03ddf181f4162e..0864d1233f788800b920a757a007b3cf87e2fc46 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.
@@ -211,9 +220,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.
@@ -229,8 +238,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.
@@ -241,13 +249,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))].
@@ -264,7 +265,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_derived_rules.v b/iris_derived_rules.v
index 3d4b04cb8e1c18277f63989d811460bb2931940a..eb9452559fb19f20427c36f6db7f341bf0114bb6 100644
--- a/iris_derived_rules.v
+++ b/iris_derived_rules.v
@@ -15,8 +15,6 @@ Module Type IRIS_DERIVED_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (W
Section DerivedRules.
- Existing Instance LP_isval.
-
Implicit Types (P : Props) (i : nat) (m : mask) (e : expr) (r : res).
Lemma vsFalse m1 m2 :
diff --git a/iris_ht_rules.v b/iris_ht_rules.v
index 7d5f1e5f4b00a2571d8a8488c91d03986bac923a..203e9d70c28962e72e3c60e4bdbd0bb38d93a131 100644
--- a/iris_ht_rules.v
+++ b/iris_ht_rules.v
@@ -16,7 +16,7 @@ Module Type IRIS_HT_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
Existing Instance LP_isval.
- Implicit Types (P : Props) (i : nat) (safe : bool) (m : mask) (e : expr) (Q : vPred) (r : pres).
+ Implicit Types (P : Props) (i : nat) (safe : bool) (m : mask) (e : expr) (Q : vPred) (r : res).
(** Ret **)
Program Definition eqV v : vPred :=
@@ -247,24 +247,20 @@ Module Type IRIS_HT_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
rewrite <- EQr, <- assoc in HE; edestruct He as [HV [HS [HF HS'] ] ]; try eassumption; [].
clear He; split; [intros HVal; clear HS HF IH HE | split; [clear HV HF HE | clear HV HS HE; split; [clear HS' | clear HF] ]; intros ].
- specialize (HV HVal); destruct HV as [w'' [r1' [HSw' [Hφ HE] ] ] ].
- rewrite ->assoc in HE. exists w''.
- exists↓ (ra_proj r1' · ra_proj r2).
- { apply wsat_valid in HE. auto_valid. }
+ rewrite ->assoc in HE. exists w'' (r1' · r2).
split; [eassumption | split; [| eassumption ] ].
exists r1' r2; split; [reflexivity | split; [assumption |] ].
unfold lt in HLt; rewrite ->HLt, <- HSw', <- HSw; apply HLR.
- edestruct HS as [w'' [r1' [HSw' [He HE] ] ] ]; try eassumption; []; clear HS.
destruct k as [| k]; [exists w' r1'; split; [reflexivity | split; [apply wpO | exact I] ] |].
- rewrite ->assoc in HE. exists w''. exists↓ (ra_proj r1' · ra_proj r2).
- { apply wsat_valid in HE. auto_valid. }
+ rewrite ->assoc in HE. exists w'' (r1' · r2).
split; [eassumption | split; [| eassumption] ].
eapply IH; try eassumption; [ reflexivity |].
unfold lt in HLt; rewrite ->Le.le_n_Sn, HLt, <- HSw', <- HSw; apply HLR.
- specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [HSw' [HWF [HWR HE] ] ] ] ] ].
destruct k as [| k]; [exists w' rfk rret; split; [reflexivity | split; [apply wpO | split; [apply wpO | exact I] ] ] |].
- rewrite ->assoc, <- (assoc (_ rfk)) in HE.
- exists w''. exists rfk. exists↓ (ra_proj rret · ra_proj r2).
- { clear- HE. apply wsat_valid in HE. eapply ra_op_valid2, ra_op_valid; try now apply _. eassumption. }
+ rewrite ->assoc, <- (assoc rfk) in HE.
+ exists w''. exists rfk (rret · r2).
split; [eassumption | split; [| split; eassumption] ].
eapply IH; try eassumption; [ reflexivity |].
unfold lt in HLt; rewrite ->Le.le_n_Sn, HLt, <- HSw', <- HSw; apply HLR.
@@ -288,8 +284,7 @@ Module Type IRIS_HT_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
edestruct He as [_ [HeS _] ]; try eassumption; [].
edestruct HeS as [w'' [r1' [HSw' [He' HE'] ] ] ]; try eassumption; [].
clear HE He HeS; rewrite ->assoc in HE'.
- exists w''. exists↓ (ra_proj r1' · ra_proj r2).
- { clear- HE'. apply wsat_valid in HE'. auto_valid. }
+ exists w'' (r1' · r2).
split; [eassumption | split; [| eassumption] ].
assert (HNV : ~ is_value ei)
by (intros HV; eapply (values_stuck _ HV); [symmetry; apply fill_empty | repeat eexists; eassumption]).
@@ -299,12 +294,11 @@ Module Type IRIS_HT_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
assert (HVal := atomic_step _ _ _ _ HAt HStep).
clear - He' HVal HLR; rename w'' into w; rewrite ->unfold_wp; intros w'; intros.
split; [intros HV; clear HVal | split; intros; [exfalso| split; intros; [exfalso |] ] ].
- + rewrite ->unfold_wp in He'. rewrite ra_proj_cancel in HE. rewrite <-assoc in HE.
+ + rewrite ->unfold_wp in He'. rewrite <-assoc in HE.
edestruct He' as [HVal _]; try eassumption; [].
specialize (HVal HV); destruct HVal as [w'' [r1'' [HSw' [Hφ HE'] ] ] ].
rewrite ->assoc in HE'.
- exists w''. exists↓ (ra_proj r1'' · ra_proj r2).
- { clear- HE'. apply wsat_valid in HE'. auto_valid. }
+ exists w'' (r1'' · r2).
split; [eassumption | split; [| eassumption] ].
exists r1'' r2; split; [reflexivity | split; [assumption |] ].
unfold lt in HLt; rewrite <- HLt, HSw, HSw' in HLR; apply HLR.
@@ -315,7 +309,7 @@ Module Type IRIS_HT_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
+ unfold safeExpr. now auto.
- subst; eapply fork_not_atomic; eassumption.
- rewrite <- EQr, <- assoc in HE; rewrite ->unfold_wp in He.
- specialize (He w' k (ra_proj r2 · rf) mf σ HSw HLt HD0 HE); clear HE.
+ specialize (He w' k (r2 · rf) mf σ HSw HLt HD0 HE); clear HE.
destruct He as [_ [_ [_ HS'] ] ]; auto.
Qed.
@@ -339,7 +333,7 @@ Module Type IRIS_HT_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
rewrite ->fill_empty; rewrite ->unfold_wp; rewrite <- (le_S_n _ _ HLt), HSw in HLR.
clear - HLR; intros w''; intros; split; [intros | split; intros; [exfalso | split; intros; [exfalso |] ] ].
+ do 2 eexists; split; [reflexivity | split; [| eassumption] ].
- exists (ra_pos_unit) r2; split; [unfold ra_pos_unit; simpl; now erewrite ra_op_unit by apply _ |].
+ exists 1 r2; split; [simpl; now erewrite ra_op_unit by apply _ |].
split; [| unfold lt in HLt; rewrite <- HLt, HSw in HLR; apply HLR].
simpl; reflexivity.
+ eapply values_stuck; [exact fork_ret_is_value | eassumption | repeat eexists; eassumption].
diff --git a/iris_meta.v b/iris_meta.v
index d75aa2f42deb8a5146e714d80a36b30d2a81f834..5f65742ad9913c595981c5b0d2ce1caa1807930e 100644
--- a/iris_meta.v
+++ b/iris_meta.v
@@ -17,7 +17,7 @@ Module Type IRIS_META (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
Local Open Scope list_scope.
(* weakest-pre for a threadpool *)
- Inductive wptp (safe : bool) (m : mask) (w : Wld) (n : nat) : tpool -> list pres -> list vPred -> Prop :=
+ Inductive wptp (safe : bool) (m : mask) (w : Wld) (n : nat) : tpool -> list res -> list vPred -> Prop :=
| wp_emp : wptp safe m w n nil nil nil
| wp_cons e φ r tp rs φs
(WPE : wp safe m e φ w n r)
@@ -77,7 +77,7 @@ Module Type IRIS_META (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
[reflexivity | now apply le_n | now apply mask_emp_disjoint | |].
+ eapply wsat_equiv, HE; try reflexivity; [apply mask_emp_union |].
rewrite !comp_list_app; simpl comp_list; unfold equiv.
- rewrite ->assoc, (comm (_ r)), <- assoc. reflexivity.
+ rewrite ->assoc, (comm r), <- assoc. reflexivity.
+ edestruct HS as [w' [r' [HSW [WPE' HE'] ] ] ];
[reflexivity | eassumption | clear WPE HS].
setoid_rewrite HSW. eapply IHn; clear IHn.
@@ -86,7 +86,7 @@ Module Type IRIS_META (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
constructor; [eassumption | eapply wptp_closure, WPTP; [assumption | now auto with arith] ].
* eapply wsat_equiv, HE'; [now erewrite mask_emp_union| |reflexivity].
rewrite !comp_list_app; simpl comp_list; unfold equiv.
- rewrite ->2!assoc, (comm (_ r')). reflexivity.
+ rewrite ->2!assoc, (comm r'). reflexivity.
}
(* fork *)
inversion H; subst; clear H.
@@ -96,7 +96,7 @@ Module Type IRIS_META (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
[reflexivity | now apply le_n | now apply mask_emp_disjoint | |].
+ eapply wsat_equiv, HE; try reflexivity; [apply mask_emp_union |].
rewrite !comp_list_app; simpl comp_list; unfold equiv.
- rewrite ->assoc, (comm (_ r)), <- assoc. reflexivity.
+ rewrite ->assoc, (comm r), <- assoc. reflexivity.
+ specialize (HF _ _ eq_refl); destruct HF as [w' [rfk [rret [HSW [WPE' [WPS HE'] ] ] ] ] ]; clear WPE.
setoid_rewrite HSW. edestruct IHn as [w'' [rs'' [φs'' [HSW'' [HSWTP'' HSE''] ] ] ] ]; first eassumption; first 2 last.
* exists w'' rs'' ([umconst ⊤] ++ φs''). split; [eassumption|].
@@ -107,16 +107,16 @@ Module Type IRIS_META (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
constructor; [|now constructor]. eassumption.
* eapply wsat_equiv, HE'; try reflexivity; [symmetry; apply mask_emp_union |].
rewrite comp_list_app. simpl comp_list. rewrite !comp_list_app. simpl comp_list.
- rewrite (comm (_ rfk)). erewrite ra_op_unit by apply _.
- rewrite (comm _ (_ rfk)). rewrite ->!assoc. eapply ra_op_proper;[now apply _ | |reflexivity]. unfold equiv.
- rewrite <-assoc, (comm (_ rret)). rewrite (comm (_ rret)). reflexivity.
+ rewrite (comm rfk). erewrite ra_op_unit by apply _.
+ rewrite (comm _ rfk). rewrite ->!assoc. eapply ra_op_proper;[now apply _ | |reflexivity]. unfold equiv.
+ rewrite <-assoc, (comm rret). rewrite comm. reflexivity.
Qed.
Lemma adequacy_ht {safe m e P Q n k tp' σ σ' w r}
(HT : valid (ht safe m P e Q))
(HSN : stepn n ([e], σ) (tp', σ'))
(HP : P w (n + S k) r)
- (HE : wsat σ m (ra_proj r) w @ n + S k) :
+ (HE : wsat σ m r w @ n + S k) :
exists w' rs' φs',
w ⊑ w' /\ wptp safe m w' (S k) tp' rs' (Q :: φs') /\ wsat σ' m (comp_list rs') w' @ S k.
Proof.
@@ -134,13 +134,12 @@ Module Type IRIS_META (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
wptp safe m w' (S k') tp' rs' (Q :: φs') /\ wsat σ' m (comp_list rs') w' @ S k'.
Proof.
destruct (steps_stepn _ _ HSN) as [n HSN']. clear HSN.
- pose↓ r := (ex_own _ σ, 1:RL.res).
- { unfold ra_valid. simpl. split; [|eapply ra_valid_unit; now apply _]. exact I. }
+ pose (r := (ex_own _ σ, 1:RL.res)).
edestruct (adequacy_ht (w:=fdEmpty) (k:=k') (r:=r) HT HSN') as [w' [rs' [φs' [HW [HSWTP HWS] ] ] ] ]; clear HT HSN'.
- exists (ra_unit _); now rewrite ->ra_op_unit by apply _.
- - hnf. rewrite Plus.plus_comm. exists (fdEmpty (V:=pres)). split.
- + unfold r, comp_map. simpl. rewrite ra_op_unit2. split; first assumption.
- reflexivity.
+ - hnf. rewrite Plus.plus_comm. exists (fdEmpty (V:=res)). split.
+ + unfold r, comp_map. simpl. rewrite ra_op_unit2. split; last reflexivity.
+ unfold ra_valid. simpl. split; [|eapply ra_valid_unit; now apply _]. exact I.
+ intros i _; split; [reflexivity |].
intros _ _ [].
- do 3 eexists. split; [eassumption|]. assumption.
@@ -192,7 +191,7 @@ Module Type IRIS_META (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
- rewrite mask_emp_union.
eapply wsat_equiv, HWS; try reflexivity.
rewrite comp_list_app. simpl comp_list.
- rewrite ->(assoc (comp_list rs1)), ->(comm (comp_list rs1) (ra_proj r)), <-assoc. reflexivity.
+ rewrite ->(assoc (comp_list rs1)), ->(comm (comp_list rs1) r), <-assoc. reflexivity.
- apply HSafe. reflexivity.
Qed.
@@ -203,7 +202,7 @@ Module Type IRIS_META (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
Definition wf_nat_ind := well_founded_induction Wf_nat.lt_wf.
- Implicit Types (P : Props) (i n k : nat) (safe : bool) (m : mask) (e : expr) (Q : vPred) (r : pres) (w : Wld) (σ : state).
+ Implicit Types (P : Props) (i n k : nat) (safe : bool) (m : mask) (e : expr) (Q : vPred) (r : res) (w : Wld) (σ : state).
Program Definition restrictV (Q : expr -n> Props) : vPred :=
n[(fun v => Q (` v))].
@@ -288,7 +287,7 @@ Module Type IRIS_META (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
have {Hei} Hei: (E ei) w' (S k) rei by propsM Hei.
have HSw': w' ⊑ w' by reflexivity.
have HLe: S k <= S k by omega.
- have H1ei: ra_pos_unit ⊑ rei by apply: unit_min.
+ have H1ei: 1 ⊑ rei by apply: unit_min.
have HLt': k < S k by omega.
move: HW; rewrite {1}mask_full_union -{1}(mask_full_union mask_emp) -assoc => HW.
case: (atomic_dec ei) => HA; last first.
@@ -302,10 +301,8 @@ Module Type IRIS_META (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
move: {HD} (mask_emp_disjoint (mask_full ∪ mask_full)) => HD.
move: {He HSw' HW} (He _ _ _ _ _ HSw' HLt' HD HW) => [w'' [r' [HSw' [Hei' HW] ] ] ].
move: HW; rewrite assoc=>HW.
- pose↓ α := (ra_proj r' · ra_proj rK).
- + by apply wsat_valid in HW; auto_valid.
have {HSw₀} HSw₀: w₀ ⊑ w'' by transitivity w'.
- exists w'' α; split; [done| split]; last first.
+ exists w'' (r' · rK); split; [done| split]; last first.
+ by move: HW; rewrite 2! mask_full_union => HW; wsatM HW.
apply: (IH _ HLt _ _ _ _ HSwâ‚€); last done.
rewrite fillE; exists r' rK; split; [exact: equivR | split; [by propsM Hei' |] ].
@@ -334,9 +331,7 @@ Module Type IRIS_META (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
move: {Hv} (Hv HV) => [w''' [rei' [HSw'' [Hei' HW] ] ] ].
(* now IH *)
move: HW; rewrite assoc => HW.
- pose↓ α := (ra_proj rei' · ra_proj rK).
- + by apply wsat_valid in HW; auto_valid.
- exists w''' α. split; first by transitivity w''.
+ exists w''' (rei' · rK). split; first by transitivity w''.
split; last by rewrite mask_full_union -(mask_full_union mask_emp).
rewrite/= in Hei'; rewrite fill_empty -Hk' in Hei' * => {Hk'}.
have {HSw₀} HSw₀ : w₀ ⊑ w''' by transitivity w''; first by transitivity w'.
@@ -351,7 +346,7 @@ Module Type IRIS_META (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WORLD_
Section Lifting.
- Implicit Types (P : Props) (i : nat) (safe : bool) (m : mask) (e : expr) (Q R : vPred) (r : pres).
+ Implicit Types (P : Props) (i : nat) (safe : bool) (m : mask) (e : expr) (Q R : vPred) (r : res).
Program Definition lift_ePred (φ : expr -=> Prop) : expr -n> Props :=
diff --git a/iris_plog.v b/iris_plog.v
index 1f9118f2e0f8e7d7af5dfd26c8c95444ecf7a477..3df7d55d8804d273e73a536cb1c1aec6c3202595 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 :=
intEq (w i) (Some (ı' P)) w.
Program Definition inv i : Props -n> Props :=
n[(fun P => m[(invP i P)])].
@@ -58,10 +56,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 :
@@ -71,57 +69,54 @@ 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
- end.
+ (* When is a resource okay with a state? *)
+ Definition res_sat (r: res) σ: Prop := ↓r /\ fst r == ex_own state σ.
- Global Instance state_sat_dist : Proper (equiv ==> equiv ==> iff) state_sat.
+ Global Instance res_sat_dist : Proper (equiv ==> equiv ==> iff) res_sat.
Proof.
- intros [ [s1| |] r1] [ [s2| |] r2] [EQs EQr] σ1 σ2 EQσ; unfold state_sat; simpl in *; try tauto; try rewrite !EQs; try rewrite !EQr; try rewrite !EQσ; reflexivity.
+ intros [ [s1| |] r1] [ [s2| |] r2] [EQs EQr] σ1 σ2 EQσ; unfold res_sat; simpl in *; try tauto; try rewrite !EQs; try rewrite !EQr; try rewrite !EQσ; reflexivity.
Qed.
Global Instance preo_unit : preoType () := disc_preo ().
Program Definition wsat σ m (r : res) w : UPred () :=
- â–¹ (mkUPred (fun n _ => exists rs : nat -f> pres,
- state_sat (r · (comp_map rs)) σ
+ â–¹ (mkUPred (fun n _ => exists rs : nat -f> res,
+ res_sat (r · (comp_map rs)) σ
/\ forall i (Hm : m i),
(i ∈ dom rs <-> i ∈ dom w) /\
forall π ri (HLw : w i == Some π) (HLrs : rs i == Some ri),
@@ -201,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) _.
@@ -213,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.
@@ -280,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 *)
@@ -305,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/iris_vs_rules.v b/iris_vs_rules.v
index 5b905802b583ae68295efbeed8b366afe33df548..31b32531f20e507ef2a0a5e4f823ecee8c0451b6 100644
--- a/iris_vs_rules.v
+++ b/iris_vs_rules.v
@@ -11,7 +11,7 @@ Module Type IRIS_VS_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
Local Open Scope bi_scope.
Local Open Scope iris_scope.
- Implicit Types (P Q R : Props) (w : Wld) (n i k : nat) (m : mask) (r : pres) (σ : state).
+ Implicit Types (P Q R : Props) (w : Wld) (n i k : nat) (m : mask) (r : res) (σ : state).
Section ViewShiftProps.
@@ -38,14 +38,13 @@ Module Type IRIS_VS_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
destruct HE as [rs [HE HM] ].
destruct (rs i) as [ri |] eqn: HLr.
- rewrite ->comp_map_remove with (i := i) (r := ri) in HE by now eapply equivR.
- rewrite ->assoc, <- (assoc (_ r)), (comm rf), assoc in HE.
- exists w'.
- exists↓ (ra_proj r · ra_proj ri). { destruct HE as [HE _]. eapply ra_op_valid, ra_op_valid; eauto with typeclass_instances. }
+ rewrite ->assoc, <- (assoc r), (comm rf), assoc in HE.
+ exists w' (r · ri).
split; [reflexivity |].
split.
+ simpl; eapply HInv; [now auto with arith |].
eapply uni_pred, HM with i;
- [| exists (ra_proj r) | | | rewrite HLr]; try reflexivity; [reflexivity| |].
+ [| exists r | | | rewrite HLr]; try reflexivity.
* left; unfold mask_sing, mask_set.
destruct (Peano_dec.eq_nat_dec i i); tauto.
* specialize (HSub i); rewrite HLu in HSub.
@@ -72,17 +71,10 @@ Module Type IRIS_VS_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
(* get rid of the invisible 1/2 *)
do 8 red in HInv.
destruct HE as [rs [HE HM] ].
- exists w' ra_pos_unit; split; [reflexivity | split; [exact I |] ].
- rewrite ->(comm (_ r)), <-assoc in HE.
- remember (match rs i with Some ri => ri | None => ra_pos_unit end) as ri eqn: EQri.
- pose↓ rri := (ra_proj ri · ra_proj r).
- { destruct (rs i) as [rsi |] eqn: EQrsi; subst;
- [| simpl; rewrite ->ra_op_unit by apply _; now apply ra_pos_valid].
- clear - HE EQrsi. destruct HE as [HE _].
- rewrite ->comp_map_remove with (i:=i) in HE by (eapply equivR; eassumption).
- rewrite ->(assoc (_ r)), (comm (_ r)), comm, assoc, <-(assoc (_ rsi) _), (comm _ (ra_proj r)), assoc in HE.
- eapply ra_op_valid, ra_op_valid; now eauto with typeclass_instances.
- }
+ exists w' 1; split; [reflexivity | split; [exact I |] ].
+ rewrite ->(comm r), <-assoc in HE.
+ remember (match rs i with Some ri => ri | None => 1 end) as ri eqn: EQri.
+ pose (rri := (ri · r)).
exists (fdUpdate i rri rs); split; [| intros j Hm].
- simpl. erewrite ra_op_unit by apply _.
clear - HE EQri. destruct (rs i) as [rsi |] eqn: EQrsi.
@@ -102,11 +94,8 @@ Module Type IRIS_VS_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
apply HInv; [now auto with arith |].
eapply uni_pred, HP; [now auto with arith |].
rewrite <-HLrs. clear dependent ri0.
- exists (ra_proj ri · ra_proj r1).
- subst rri.
- (* Coq, are you serious?!?? *)
- change (ra_proj ri · ra_proj r1 · ra_proj r2 == (ra_proj ri · ra_proj r)).
- rewrite <-HR, assoc. reflexivity.
+ exists (ri · r1).
+ subst rri. rewrite <-HR, assoc. reflexivity.
Qed.
Lemma vsTrans P Q R m1 m2 m3 (HMS : m2 ⊆ m1 ∪ m3) :
@@ -134,7 +123,7 @@ Module Type IRIS_VS_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
intros w' n r1 Himp w HSub; rewrite ->HSub in Himp; clear w' HSub.
intros np rp HLe HS Hp w1; intros.
exists w1 rp; split; [reflexivity | split; [| assumption ] ].
- eapply Himp; [assumption | now eauto with arith | now apply ord_res_pres, unit_min | ].
+ eapply Himp; [assumption | now eauto with arith | now apply unit_min | ].
unfold lt in HLe0; rewrite ->HLe0, <- HSub; assumption.
Qed.
@@ -143,8 +132,8 @@ Module Type IRIS_VS_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
Proof.
intros w' n r1 HVS w HSub; specialize (HVS _ HSub); clear w' r1 HSub.
intros np rpr HLe _ [rp [rr [HR [Hp Hr] ] ] ] w'; intros.
- assert (HS : ra_unit _ ⊑ ra_proj rp) by (eapply unit_min).
- specialize (HVS _ _ HLe HS Hp w' (ra_proj rr · rf) (mf ∪ mf0) σ k); clear HS.
+ assert (HS : ra_unit _ ⊑ rp) by (eapply unit_min).
+ specialize (HVS _ _ HLe HS Hp w' (rr · rf) (mf ∪ mf0) σ k); clear HS.
destruct HVS as [w'' [rq [HSub' [Hq HEq] ] ] ]; try assumption; [| |].
- (* disjointness of masks: possible lemma *)
clear - HD HDisj; intros i [ [Hmf | Hmf] Hm12]; [eapply HDisj; now eauto |].
@@ -152,8 +141,7 @@ Module Type IRIS_VS_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
- rewrite ->assoc, HR; eapply wsat_equiv, HE; try reflexivity; [].
clear; intros i; unfold mcup; tauto.
- rewrite ->assoc in HEq.
- exists w''. exists↓ (ra_proj rq · ra_proj rr).
- { apply wsat_valid in HEq. auto_valid. }
+ exists w'' (rq · rr).
split; [assumption | split].
+ unfold lt in HLe0; rewrite ->HSub, HSub', <- HLe0 in Hr; exists rq rr.
split; now auto.
@@ -174,18 +162,14 @@ Module Type IRIS_VS_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
(HU : forall rf (HD : ↓(rl · rf)), exists sl, P sl /\ ↓(sl · rf)) :
valid (vs m m (ownL rl) (xist (ownLP P))).
Proof.
- unfold ownLP; intros _ _ _ w _ n [ [rp' rl'] Hrval] _ _ HG w'; intros.
- destruct HE as [rs [ Hsat HE] ]. rewrite <-assoc in Hsat. simpl in Hsat. destruct Hsat as [Hval Hst].
+ unfold ownLP; intros _ _ _ w _ n [rp' rl'] _ _ HG w'; intros.
+ destruct HE as [rs [ Hsat HE] ]. rewrite <-assoc in Hsat. destruct Hsat as [Hval Hst].
destruct HG as [ [rdp rdl] [_ EQrl] ]. simpl in EQrl. clear rdp.
destruct (HU (rdl · snd(rf · comp_map rs))) as [rsl [HPrsl HCrsl] ].
- clear - Hval EQrl. eapply ra_prod_valid in Hval. destruct Hval as [_ Hsnd].
rewrite ->assoc, (comm rl), EQrl.
rewrite ra_op_prod_snd in Hsnd. exact Hsnd.
- - exists w'. exists↓ (rp', rsl).
- { clear - Hval HCrsl.
- apply ra_prod_valid. split; [|auto_valid].
- eapply ra_prod_valid in Hval. destruct Hval as [Hfst _].
- rewrite ra_op_prod_fst in Hfst. auto_valid. }
+ - exists w' (rp', rsl).
split; first reflexivity. split.
+ exists (exist _ rsl HPrsl). simpl.
exists (rp', 1:RL.res). simpl.
@@ -239,10 +223,10 @@ Module Type IRIS_VS_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
{ intros j; destruct (Peano_dec.eq_nat_dec i j); [subst j; rewrite HLi; exact I|].
now rewrite ->fdUpdate_neq by assumption.
}
- exists (fdUpdate i (ı' P) w) (ra_pos_unit); split; [assumption | split].
+ exists (fdUpdate i (ı' P) w) 1; split; [assumption | split].
- exists (exist _ i Hm). do 22 red.
unfold proj1_sig. rewrite fdUpdate_eq; reflexivity.
- - unfold ra_pos_unit, proj1_sig. erewrite ra_op_unit by apply _.
+ - erewrite ra_op_unit by apply _.
destruct HE as [rs [HE HM] ].
exists (fdUpdate i r rs).
assert (HRi : rs i = None).
@@ -264,6 +248,18 @@ Module Type IRIS_VS_RULES (RL : RA_T) (C : CORE_LANG) (R: IRIS_RES RL C) (WP: WO
apply HM; assumption.
Qed.
+ Lemma vsNotOwnInvalid m1 m2 r
+ (Hnval: ~↓r):
+ valid (vs m1 m2 (ownR r) ⊥).
+ Proof.
+ intros pw n s w _. clear pw s.
+ intros m s _ _. clear n.
+ intros [rs Heq] w' rf mf σ k _ _ _ [ ri [ [ Hval _ ] ] ].
+ exfalso.
+ apply Hnval. rewrite <-Heq in Hval.
+ eapply ra_op_valid2, ra_op_valid, ra_op_valid; last eassumption; now apply _.
+ Qed.
+
End ViewShiftProps.
End IRIS_VS_RULES.
diff --git a/lib/ModuRes/BI.v b/lib/ModuRes/BI.v
index 8c97a665e45c9e4391407db55c05c5d5576644ac..87d1927bebdd6551de14676d9272c585c45e0e87 100644
--- a/lib/ModuRes/BI.v
+++ b/lib/ModuRes/BI.v
@@ -156,26 +156,24 @@ Section UPredBI.
Local Open Scope ra_scope.
Local Obligation Tactic := intros; eauto with typeclass_instances.
- Let pres := âºres.
-
(* Standard interpretations of propositional connectives. *)
- Global Program Instance top_up : topBI (UPred pres) := up_cr (const True).
- Global Program Instance bot_up : botBI (UPred pres) := up_cr (const False).
+ Global Program Instance top_up : topBI (UPred res) := up_cr (const True).
+ Global Program Instance bot_up : botBI (UPred res) := up_cr (const False).
- Global Program Instance and_up : andBI (UPred pres) :=
+ Global Program Instance and_up : andBI (UPred res) :=
fun P Q =>
mkUPred (fun n r => P n r /\ Q n r) _.
Next Obligation.
intros n m r1 r2 HLe HSub; rewrite HSub, HLe; tauto.
Qed.
- Global Program Instance or_up : orBI (UPred pres) :=
+ Global Program Instance or_up : orBI (UPred res) :=
fun P Q =>
mkUPred (fun n r => P n r \/ Q n r) _.
Next Obligation.
intros n m r1 r2 HLe HSub; rewrite HSub, HLe; tauto.
Qed.
- Global Program Instance impl_up : implBI (UPred pres) :=
+ Global Program Instance impl_up : implBI (UPred res) :=
fun P Q =>
mkUPred (fun n r => forall m r', m <= n -> r ⊑ r' -> P m r' -> Q m r') _.
Next Obligation.
@@ -184,13 +182,13 @@ Section UPredBI.
Qed.
(* BI connectives. *)
- Global Program Instance sc_up : scBI (UPred pres) :=
+ Global Program Instance sc_up : scBI (UPred res) :=
fun P Q =>
- mkUPred (fun n r => exists r1 r2, ra_proj r1 · ra_proj r2 == ra_proj r /\ P n r1 /\ Q n r2) _.
+ mkUPred (fun n r => exists r1 r2, r1 · r2 == r /\ P n r1 /\ Q n r2) _.
Next Obligation.
intros n m r1 r2 HLe [rd HEq] [r11 [r12 [HEq' [HP HQ]]]].
rewrite <- HEq', assoc in HEq; setoid_rewrite HLe.
- exists↓ (rd · ra_proj r11) by auto_valid.
+ exists (rd · r11).
exists r12.
split; [|split;[|assumption] ].
- simpl. assumption.
@@ -198,27 +196,27 @@ Section UPredBI.
exists rd. reflexivity.
Qed.
- Global Program Instance si_up : siBI (UPred pres) :=
+ Global Program Instance si_up : siBI (UPred res) :=
fun P Q =>
- mkUPred (fun n r => forall m r' rr, ra_proj r · ra_proj r' == ra_proj rr -> m <= n -> P m r' -> Q m rr) _.
+ mkUPred (fun n r => forall m r' rr, r · r' == rr -> m <= n -> P m r' -> Q m rr) _.
Next Obligation.
intros n m r1 r2 HLe [r12 HEq] HSI k r rr HEq' HSub HP.
rewrite comm in HEq; rewrite <- HEq, <- assoc in HEq'.
- pose↓ rc := (r12 · ra_proj r) by auto_valid.
+ pose (rc := (r12 · r)).
eapply HSI with (r':=rc); [| etransitivity; eassumption |].
- simpl. assumption.
- eapply uni_pred, HP; [reflexivity|]. exists r12. reflexivity.
Qed.
(* Quantifiers. *)
- Global Program Instance all_up : allBI (UPred pres) :=
+ Global Program Instance all_up : allBI (UPred res) :=
fun T eqT mT cmT R =>
mkUPred (fun n r => forall t, R t n r) _.
Next Obligation.
intros n m r1 r2 HLe HSub HR t; rewrite HLe, <- HSub; apply HR.
Qed.
- Global Program Instance xist_up : xistBI (UPred pres) :=
+ Global Program Instance xist_up : xistBI (UPred res) :=
fun T eqT mT cmT R =>
mkUPred (fun n r => exists t, R t n r) _.
Next Obligation.
@@ -315,23 +313,23 @@ Section UPredBI.
Existing Instance nonexp_type.
- Global Instance all_up_equiv : Proper (equiv (A := V -n> UPred pres) ==> equiv) all.
+ Global Instance all_up_equiv : Proper (equiv (A := V -n> UPred res) ==> equiv) all.
Proof.
intros R1 R2 EQR n r; simpl.
setoid_rewrite EQR; tauto.
Qed.
- Global Instance all_up_dist n : Proper (dist (T := V -n> UPred pres) n ==> dist n) all.
+ Global Instance all_up_dist n : Proper (dist (T := V -n> UPred res) n ==> dist n) all.
Proof.
intros R1 R2 EQR m r HLt; simpl.
split; intros; apply EQR; now auto.
Qed.
- Global Instance xist_up_equiv : Proper (equiv (A := V -n> UPred pres) ==> equiv) xist.
+ Global Instance xist_up_equiv : Proper (equiv (A := V -n> UPred res) ==> equiv) xist.
Proof.
intros R1 R2 EQR n r; simpl.
setoid_rewrite EQR; tauto.
Qed.
- Global Instance xist_up_dist n : Proper (dist (T := V -n> UPred pres)n ==> dist n) xist.
+ Global Instance xist_up_dist n : Proper (dist (T := V -n> UPred res)n ==> dist n) xist.
Proof.
intros R1 R2 EQR m r HLt; simpl.
split; intros [t HR]; exists t; apply EQR; now auto.
@@ -339,7 +337,7 @@ Section UPredBI.
End Quantifiers.
- Global Program Instance bi_up : ComplBI (UPred pres).
+ Global Program Instance bi_up : ComplBI (UPred res).
Next Obligation.
intros n r _; exact I.
Qed.
@@ -371,29 +369,27 @@ Section UPredBI.
Qed.
Next Obligation.
intros P Q n r; simpl.
- setoid_rewrite (comm (Commutative := ra_op_comm _)) at 1.
- firstorder.
+ split; intros [r1 [r2 HPQ]]; exists r2 r1; rewrite comm; tauto.
Qed.
Next Obligation.
intros P Q R n r; split.
- intros [r1 [rr [EQr [HP [r2 [r3 [EQrr [HQ HR]]]]]]]].
rewrite <- EQrr, assoc in EQr. unfold sc.
- exists↓ (ra_proj r1 · ra_proj r2) by auto_valid.
+ exists (r1 · r2).
exists r3; split; [assumption | split; [| assumption] ].
exists r1 r2; split; [reflexivity | split; assumption].
- intros [rr [r3 [EQr [[r1 [r2 [EQrr [HP HQ]]]] HR]]]].
rewrite <- EQrr, <- assoc in EQr; clear EQrr.
exists r1.
- exists↓ (ra_proj r2 · ra_proj r3) by auto_valid.
+ exists (r2 · r3).
split; [assumption | split; [assumption |] ].
exists r2 r3; split; [reflexivity | split; assumption].
Qed.
Next Obligation.
intros n r; split.
- intros [r1 [r2 [EQr [_ HP]]]].
- eapply uni_pred, HP; [reflexivity|]. exists (ra_proj r1). assumption.
- - intros HP. exists (ra_pos_unit (T:=res)) r. split;
- [simpl; erewrite ra_op_unit by apply _; reflexivity |].
+ eapply uni_pred, HP; [reflexivity|]. exists (r1). assumption.
+ - intros HP. exists (ra_unit res) r. split; [simpl; erewrite ra_op_unit by apply _; reflexivity |].
simpl; unfold const; tauto.
Qed.
Next Obligation.
diff --git a/lib/ModuRes/RA.v b/lib/ModuRes/RA.v
index 695fe2139e6aaea467aba5a4950cd7a37f0808b4..6a848f2801967fa40cf4aef83a1c77b297c50a9b 100644
--- a/lib/ModuRes/RA.v
+++ b/lib/ModuRes/RA.v
@@ -1,4 +1,4 @@
-(** Resource algebras: Commutative monoids with a decidable validity predicate. *)
+(** Resource algebras: Commutative monoids with a validity predicate. *)
Require Import Bool.
Require Import Predom.
@@ -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 a6faa4534961f59b7a7050d668b3696708cf0d26..cce80cff1078f13ec0805ccc8584123895dc6418 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 da2a1258913b24b260bd35b34e00ff49578ab1ff..5d67bb3d55e55adde8b4560184b5037fd5dbe5e2 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}.