Commit 9ba9ef1b authored by David Swasey's avatar David Swasey

Notation and metavariables.

Moved connective notation to BI.

Added ⁺T for ra_pos T and eliminated BI.pres since I'd rather see ⁺res than BI.pres.

Bound mask_scope to type mask.
parent 0204cf5e
...@@ -24,6 +24,8 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG). ...@@ -24,6 +24,8 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG).
Module Export WP := WorldProp R. Module Export WP := WorldProp R.
Delimit Scope iris_scope with iris. Delimit Scope iris_scope with iris.
Local Open Scope ra_scope.
Local Open Scope bi_scope.
Local Open Scope iris_scope. Local Open Scope iris_scope.
(** Instances for a bunch of types (some don't even have Setoids) *) (** Instances for a bunch of types (some don't even have Setoids) *)
...@@ -61,24 +63,26 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG). ...@@ -61,24 +63,26 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG).
(** And now we're ready to build the IRIS-specific connectives! *) (** 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).
Section Necessitation. Section Necessitation.
(** Note: this could be moved to BI, since it's possible to define (** Note: this could be moved to BI, since it's possible to define
for any UPred over a monoid. **) for any UPred over a RA. **)
Local Obligation Tactic := intros; resp_set || eauto with typeclass_instances. Local Obligation Tactic := intros; resp_set || eauto with typeclass_instances.
Program Definition box : Props -n> Props := 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 ra_pos_unit) _)])].
Next Obligation. Next Obligation.
intros n m r s HLe _ Hp; rewrite-> HLe; assumption. intros n m r s HLe _ Hp; rewrite-> HLe; assumption.
Qed. Qed.
Next Obligation. Next Obligation.
intros w1 w2 EQw m r HLt; simpl. intros w1 w2 EQw m r HLt; simpl.
eapply (met_morph_nonexp _ _ p); eassumption. eapply (met_morph_nonexp _ _ P); eassumption.
Qed. Qed.
Next Obligation. Next Obligation.
intros w1 w2 Subw n r; simpl. intros w1 w2 Subw n r; simpl.
apply p; assumption. apply P; assumption.
Qed. Qed.
Next Obligation. Next Obligation.
intros p1 p2 EQp w m r HLt; simpl. intros p1 p2 EQp w m r HLt; simpl.
...@@ -87,6 +91,34 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG). ...@@ -87,6 +91,34 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG).
End Necessitation. End Necessitation.
Notation "□ P" := (box P) (at level 30, right associativity) : iris_scope.
(** Lemmas about box **)
Lemma box_intro P Q (Hpr : P Q) :
P Q.
Proof.
intros w n r Hp; simpl; apply Hpr, Hp.
Qed.
Lemma box_elim P :
P P.
Proof.
intros w n r Hp; simpl in Hp.
eapply uni_pred, Hp; [reflexivity |].
now eapply unit_min.
Qed.
Lemma box_top : == .
Proof.
intros w n r; simpl; unfold const; reflexivity.
Qed.
Lemma box_disj P Q :
(P Q) == P Q.
Proof.
intros w n r; reflexivity.
Qed.
(** "Internal" equality **) (** "Internal" equality **)
Section IntEq. Section IntEq.
Context {T} `{mT : metric T}. Context {T} `{mT : metric T}.
...@@ -124,10 +156,10 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG). ...@@ -124,10 +156,10 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG).
Section Invariants. Section Invariants.
(** Invariants **) (** Invariants **)
Definition invP (i : nat) (p : Props) (w : Wld) : UPred pres := Definition invP i P w : UPred pres :=
intEqP (w i) (Some (ı' p)). intEqP (w i) (Some (ı' P)).
Program Definition inv i : Props -n> Props := Program Definition inv i : Props -n> Props :=
n[(fun p => m[(invP i p)])]. n[(fun P => m[(invP i P)])].
Next Obligation. Next Obligation.
intros w1 w2 EQw; unfold invP; simpl morph. intros w1 w2 EQw; unfold invP; simpl morph.
destruct n; [apply dist_bound |]. destruct n; [apply dist_bound |].
...@@ -148,34 +180,12 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG). ...@@ -148,34 +180,12 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG).
End Invariants. End Invariants.
Notation "□ p" := (box p) (at level 30, right associativity) : iris_scope.
Notation "⊤" := (top : Props) : iris_scope.
Notation "⊥" := (bot : Props) : iris_scope.
Notation "p ∧ q" := (and p q : Props) (at level 40, left associativity) : iris_scope.
Notation "p ∨ q" := (or p q : Props) (at level 50, left associativity) : iris_scope.
Notation "p * q" := (sc p q : Props) (at level 40, left associativity) : iris_scope.
Notation "p → q" := (BI.impl p q : Props) (at level 55, right associativity) : iris_scope.
Notation "p '-*' q" := (si p q : Props) (at level 55, right associativity) : iris_scope.
Notation "∀ x , p" := (all n[(fun x => p)] : Props) (at level 60, x ident, no associativity) : iris_scope.
Notation "∃ x , p" := (xist n[(fun x => p)] : Props) (at level 60, x ident, no associativity) : iris_scope.
Notation "∀ x : T , p" := (all n[(fun x : T => p)] : Props) (at level 60, x ident, no associativity) : iris_scope.
Notation "∃ x : T , p" := (xist n[(fun x : T => p)] : Props) (at level 60, x ident, no associativity) : iris_scope.
Lemma valid_iff p :
valid p <-> ( p).
Proof.
split; intros Hp.
- intros w n r _; apply Hp.
- intros w n r; apply Hp; exact I.
Qed.
Section Ownership. Section Ownership.
Local Open Scope ra.
(** Ownership **) (** Ownership **)
(* We define this on *any* resource, not just the positive (valid) ones. (* We define this on *any* resource, not just the positive (valid) ones.
Note that this makes ownR trivially *False* for invalid u: There is no Note that this makes ownR trivially *False* for invalid u: There is no
elment v such that u · v = r (where r is valid) *) element v such that u · v = r (where r is valid) *)
Program Definition ownR: res -=> Props := 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 ra_proj r) _) )].
Next Obligation. Next Obligation.
...@@ -212,7 +222,7 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG). ...@@ -212,7 +222,7 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG).
(** Proper physical state: ownership of the machine state **) (** Proper physical state: ownership of the machine state **)
Program Definition ownS : state -n> Props := Program Definition ownS : state -n> Props :=
n[(fun s => ownR (ex_own _ s, 1%ra))]. n[(fun s => ownR (ex_own _ s, 1))].
Next Obligation. Next Obligation.
intros r1 r2 EQr; destruct n as [| n]; [apply dist_bound |]. intros r1 r2 EQr; destruct n as [| n]; [apply dist_bound |].
rewrite EQr. reflexivity. rewrite EQr. reflexivity.
...@@ -220,58 +230,32 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG). ...@@ -220,58 +230,32 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG).
(** Proper ghost state: ownership of logical **) (** Proper ghost state: ownership of logical **)
Program Definition ownL : RL.res -n> Props := Program Definition ownL : RL.res -n> Props :=
n[(fun r => ownR (1%ra, r))]. n[(fun r : RL.res => ownR (1, r))].
Next Obligation. Next Obligation.
intros r1 r2 EQr. destruct n as [| n]; [apply dist_bound |eapply dist_refl]. 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) (ra_proj t) <-> (ex_unit state, r2) (ra_proj t)). rewrite EQr. reflexivity.
Qed. Qed.
(** Ghost state ownership **) (** Ghost state ownership **)
Lemma ownL_sc (u t : RL.res) : Lemma ownL_sc (r s : RL.res) :
ownL (u · t) == ownL u * ownL t. ownL (r · s) == ownL r * ownL s.
Proof. Proof.
assert (Heq: (ex_unit state, u · t) == ((ex_unit state, u) · (ex_unit state, t)) ) by reflexivity. assert (Heq: (1, r · s) == ((1, r) · (1, s)) ) by reflexivity.
(* I cannot believe I have to write this... *) (* I cannot believe I have to write this... *)
change (ownR (ex_unit state, u · t) == ownR (ex_unit state, u) * ownR (ex_unit state, t)). change (ownR (1, r · s) == ownR (1, r) * ownR (1, s)).
rewrite Heq. rewrite Heq.
now eapply ownR_sc. now eapply ownR_sc.
Qed. Qed.
End Ownership. End Ownership.
(** Lemmas about box **)
Lemma box_intro p q (Hpq : p q) :
p q.
Proof.
intros w n r Hp; simpl; apply Hpq, Hp.
Qed.
Lemma box_elim p :
p p.
Proof.
intros w n r Hp; simpl in Hp.
eapply uni_pred, Hp; [reflexivity |].
now eapply unit_min.
Qed.
Lemma box_top : == .
Proof.
intros w n r; simpl; unfold const; reflexivity.
Qed.
Lemma box_disj p q :
(p q) == p q.
Proof.
intros w n r; reflexivity.
Qed.
(** Timeless *) (** Timeless *)
Definition timelessP (p : Props) w n := Definition timelessP P w n :=
forall w' k r (HSw : w w') (HLt : k < n) (Hp : p w' k r), p w' (S k) r. forall w' k r (HSw : w w') (HLt : k < n) (Hp : P w' k r), P w' (S k) r.
Program Definition timeless (p : Props) : Props := Program Definition timeless P : Props :=
m[(fun w => mkUPred (fun n r => timelessP p w n) _)]. m[(fun w => mkUPred (fun n r => timelessP P w n) _)].
Next Obligation. Next Obligation.
intros n1 n2 _ _ HLe _ HT w' k r HSw HLt Hp; eapply HT, Hp; [eassumption |]. intros n1 n2 _ _ HLe _ HT w' k r HSw HLt Hp; eapply HT, Hp; [eassumption |].
omega. omega.
...@@ -280,9 +264,9 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG). ...@@ -280,9 +264,9 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG).
intros w1 w2 EQw k; simpl; intros _ HLt; destruct n as [| n]; [now inversion HLt |]. intros w1 w2 EQw k; simpl; intros _ HLt; destruct n as [| n]; [now inversion HLt |].
split; intros HT w' m r HSw HLt' Hp. split; intros HT w' m r HSw HLt' Hp.
- symmetry in EQw; assert (HD := extend_dist _ _ _ _ EQw HSw); assert (HS := extend_sub _ _ _ _ EQw HSw). - symmetry in EQw; assert (HD := extend_dist _ _ _ _ EQw HSw); assert (HS := extend_sub _ _ _ _ EQw HSw).
apply (met_morph_nonexp _ _ p) in HD; apply HD, HT, HD, Hp; now (assumption || eauto with arith). apply (met_morph_nonexp _ _ P) in HD; apply HD, HT, HD, Hp; now (assumption || eauto with arith).
- assert (HD := extend_dist _ _ _ _ EQw HSw); assert (HS := extend_sub _ _ _ _ EQw HSw). - assert (HD := extend_dist _ _ _ _ EQw HSw); assert (HS := extend_sub _ _ _ _ EQw HSw).
apply (met_morph_nonexp _ _ p) in HD; apply HD, HT, HD, Hp; now (assumption || eauto with arith). apply (met_morph_nonexp _ _ P) in HD; apply HD, HT, HD, Hp; now (assumption || eauto with arith).
Qed. Qed.
Next Obligation. Next Obligation.
intros w1 w2 HSw n; simpl; intros _ HT w' m r HSw' HLt Hp. intros w1 w2 HSw n; simpl; intros _ HT w' m r HSw' HLt Hp.
...@@ -290,8 +274,6 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG). ...@@ -290,8 +274,6 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG).
Qed. Qed.
Section WorldSatisfaction. Section WorldSatisfaction.
Local Open Scope ra_scope.
Local Open Scope bi_scope.
(* First, we need to compose the resources of a finite map. This won't be pretty, for (* First, we need to compose the resources of a finite map. This won't be pretty, for
now, since the library does not provide enough now, since the library does not provide enough
...@@ -359,7 +341,7 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG). ...@@ -359,7 +341,7 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG).
Global Instance preo_unit : preoType () := disc_preo (). Global Instance preo_unit : preoType () := disc_preo ().
Program Definition wsat (σ : state) (m : mask) (r : res) (w : Wld) : UPred () := Program Definition wsat σ m (r : res) w : UPred () :=
(mkUPred (fun n _ => exists rs : nat -f> pres, (mkUPred (fun n _ => exists rs : nat -f> pres,
state_sat (r · (comp_map rs)) σ state_sat (r · (comp_map rs)) σ
/\ forall i (Hm : m i), /\ forall i (Hm : m i),
...@@ -383,7 +365,7 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG). ...@@ -383,7 +365,7 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG).
rewrite fdLookup_in; setoid_rewrite <- EQw; rewrite <- fdLookup_in; reflexivity. rewrite fdLookup_in; setoid_rewrite <- EQw; rewrite <- fdLookup_in; reflexivity.
Qed. Qed.
Global Instance wsat_dist n σ m r : Proper (dist n ==> dist n) (wsat σ m r). Global Instance wsat_dist n σ m u : Proper (dist n ==> dist n) (wsat σ m u).
Proof. Proof.
intros w1 w2 EQw [| n'] [] HLt; [reflexivity |]; destruct n as [| n]; [now inversion HLt |]. intros w1 w2 EQw [| n'] [] HLt; [reflexivity |]; destruct n as [| n]; [now inversion HLt |].
split; intros [rs [HE HM] ]; exists rs. split; intros [rs [HE HM] ]; exists rs.
...@@ -412,6 +394,15 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG). ...@@ -412,6 +394,15 @@ Module IrisCore (RL : RA_T) (C : CORE_LANG).
End WorldSatisfaction. End WorldSatisfaction.
Notation " p @ k " := ((p : UPred ()) k tt) (at level 60, no associativity). Notation " P @ k " := ((P : UPred ()) k tt) (at level 60, no associativity).
Lemma valid_iff P :
valid P <-> ( P).
Proof.
split; intros Hp.
- intros w n r _; apply Hp.
- intros w n r; apply Hp; exact I.
Qed.
End IrisCore. End IrisCore.
...@@ -7,14 +7,13 @@ Set Bullet Behavior "Strict Subproofs". ...@@ -7,14 +7,13 @@ Set Bullet Behavior "Strict Subproofs".
Module IrisMeta (RL : RA_T) (C : CORE_LANG). Module IrisMeta (RL : RA_T) (C : CORE_LANG).
Module Export WP := IrisWP RL C. Module Export WP := IrisWP RL C.
Delimit Scope iris_scope with iris. Local Open Scope lang_scope.
Local Open Scope ra_scope.
Local Open Scope bi_scope.
Local Open Scope iris_scope. Local Open Scope iris_scope.
Section Adequacy. Section Adequacy.
Local Open Scope mask_scope.
Local Open Scope ra_scope.
Local Open Scope bi_scope.
Local Open Scope lang_scope.
Local Open Scope list_scope. Local Open Scope list_scope.
(* weakest-pre for a threadpool *) (* weakest-pre for a threadpool *)
...@@ -201,11 +200,6 @@ Module IrisMeta (RL : RA_T) (C : CORE_LANG). ...@@ -201,11 +200,6 @@ Module IrisMeta (RL : RA_T) (C : CORE_LANG).
Section Lifting. Section Lifting.
Local Open Scope mask_scope.
Local Open Scope ra_scope.
Local Open Scope bi_scope.
Local Open Scope lang_scope.
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 : pres).
...@@ -242,6 +236,6 @@ Module IrisMeta (RL : RA_T) (C : CORE_LANG). ...@@ -242,6 +236,6 @@ Module IrisMeta (RL : RA_T) (C : CORE_LANG).
Proof. Proof.
Admitted. Admitted.
End Lifting. End Lifting.
End IrisMeta. End IrisMeta.
...@@ -6,10 +6,9 @@ Require Import ModuRes.RA ModuRes.UPred ModuRes.BI ModuRes.PreoMet ModuRes.Finma ...@@ -6,10 +6,9 @@ Require Import ModuRes.RA ModuRes.UPred ModuRes.BI ModuRes.PreoMet ModuRes.Finma
Module Unsafety (RL : RA_T) (C : CORE_LANG). Module Unsafety (RL : RA_T) (C : CORE_LANG).
Module Export Iris := IrisWP RL C. Module Export Iris := IrisWP RL C.
Local Open Scope mask_scope. Local Open Scope lang_scope.
Local Open Scope ra_scope. Local Open Scope ra_scope.
Local Open Scope bi_scope. Local Open Scope bi_scope.
Local Open Scope lang_scope.
Local Open Scope iris_scope. Local Open Scope iris_scope.
(* PDS: Move to iris_core.v *) (* PDS: Move to iris_core.v *)
...@@ -52,7 +51,6 @@ Module Unsafety (RL : RA_T) (C : CORE_LANG). ...@@ -52,7 +51,6 @@ Module Unsafety (RL : RA_T) (C : CORE_LANG).
PDS: Should be moved or discarded. PDS: Should be moved or discarded.
*) *)
Notation "p * q" := (BI.sc p q) (at level 40, left associativity) : iris_scope. (* RJ: there's already notation for this in iris_core? *) (* PDS: The notation in Iris core uses sc : UPred (ra_pos res) -> UPred (ra_pos res) -> UPred (ra_pos res) rather than BI.sc. This variant is generic, so it survives more simplification. *)
Lemma wpO {safe m e Q w r} : wp safe m e Q w O r. Lemma wpO {safe m e Q w r} : wp safe m e Q w O r.
Proof. Proof.
......
...@@ -7,20 +7,21 @@ Set Bullet Behavior "Strict Subproofs". ...@@ -7,20 +7,21 @@ Set Bullet Behavior "Strict Subproofs".
Module IrisVS (RL : RA_T) (C : CORE_LANG). Module IrisVS (RL : RA_T) (C : CORE_LANG).
Module Export CORE := IrisCore RL C. Module Export CORE := IrisCore RL C.
Delimit Scope iris_scope with iris. Local Open Scope ra_scope.
Local Open Scope bi_scope.
Local Open Scope iris_scope. Local Open Scope iris_scope.
Implicit Types (P Q R : Props) (w : Wld) (n i k : nat) (m : mask) (r : pres) (σ : state).
Section ViewShifts. Section ViewShifts.
Local Open Scope mask_scope.
Local Open Scope ra_scope.
Local Obligation Tactic := intros. Local Obligation Tactic := intros.
Program Definition preVS (m1 m2 : mask) (p : Props) (w : Wld) : UPred pres := Program Definition preVS m1 m2 P w : UPred pres :=
mkUPred (fun n r => forall w1 (rf: res) mf σ k (HSub : w w1) (HLe : k < n) mkUPred (fun n r => forall w1 (rf: res) mf σ k (HSub : w w1) (HLe : k < n)
(HD : mf # m1 m2) (HD : mf # m1 m2)
(HE : wsat σ (m1 mf) (ra_proj r · rf) w1 @ S k), (HE : wsat σ (m1 mf) (ra_proj r · rf) w1 @ S k),
exists w2 r', exists w2 r',
w1 w2 /\ p w2 (S k) r' w1 w2 /\ P w2 (S k) r'
/\ wsat σ (m2 mf) (r' · rf) w2 @ S k) _. /\ wsat σ (m2 mf) (r' · rf) w2 @ S k) _.
Next Obligation. Next Obligation.
intros n1 n2 r1 r2 HLe [rd HR] HP; intros. intros n1 n2 r1 r2 HLe [rd HR] HP; intros.
...@@ -35,8 +36,8 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG). ...@@ -35,8 +36,8 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG).
eapply uni_pred, HP'; [reflexivity|]. exists rd. reflexivity. eapply uni_pred, HP'; [reflexivity|]. exists rd. reflexivity.
Qed. Qed.
Program Definition pvs (m1 m2 : mask) : Props -n> Props := Program Definition pvs m1 m2 : Props -n> Props :=
n[(fun p => m[(preVS m1 m2 p)])]. n[(fun P => m[(preVS m1 m2 P)])].
Next Obligation. Next Obligation.
intros w1 w2 EQw n' r HLt; destruct n as [| n]; [now inversion HLt |]; split; intros HP w2'; intros. 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). - symmetry in EQw; assert (HDE := extend_dist _ _ _ _ EQw HSub).
...@@ -46,7 +47,7 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG). ...@@ -46,7 +47,7 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG).
+ symmetry in HDE; assert (HDE' := extend_dist _ _ _ _ HDE HW). + symmetry in HDE; assert (HDE' := extend_dist _ _ _ _ HDE HW).
assert (HSE' := extend_sub _ _ _ _ HDE HW); destruct HH as [HP HE']; assert (HSE' := extend_sub _ _ _ _ HDE HW); destruct HH as [HP HE'];
exists (extend w1'' w2') r'; split; [assumption | split]. exists (extend w1'' w2') r'; split; [assumption | split].
* eapply (met_morph_nonexp _ _ p), HP ; [symmetry; eassumption | omega]. * eapply (met_morph_nonexp _ _ P), HP ; [symmetry; eassumption | omega].
* eapply wsat_dist, HE'; [symmetry; eassumption | omega]. * eapply wsat_dist, HE'; [symmetry; eassumption | omega].
- assert (HDE := extend_dist _ _ _ _ EQw HSub); assert (HSE := extend_sub _ _ _ _ EQw HSub); specialize (HP (extend w2' w2)). - assert (HDE := extend_dist _ _ _ _ EQw HSub); assert (HSE := extend_sub _ _ _ _ EQw HSub); specialize (HP (extend w2' w2)).
edestruct HP as [w1'' [r' [HW HH] ] ]; try eassumption; clear HP; [ | ]. edestruct HP as [w1'' [r' [HW HH] ] ]; try eassumption; clear HP; [ | ].
...@@ -54,7 +55,7 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG). ...@@ -54,7 +55,7 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG).
+ symmetry in HDE; assert (HDE' := extend_dist _ _ _ _ HDE HW). + symmetry in HDE; assert (HDE' := extend_dist _ _ _ _ HDE HW).
assert (HSE' := extend_sub _ _ _ _ HDE HW); destruct HH as [HP HE']; assert (HSE' := extend_sub _ _ _ _ HDE HW); destruct HH as [HP HE'];
exists (extend w1'' w2') r'; split; [assumption | split]. exists (extend w1'' w2') r'; split; [assumption | split].
* eapply (met_morph_nonexp _ _ p), HP ; [symmetry; eassumption | omega]. * eapply (met_morph_nonexp _ _ P), HP ; [symmetry; eassumption | omega].
* eapply wsat_dist, HE'; [symmetry; eassumption | omega]. * eapply wsat_dist, HE'; [symmetry; eassumption | omega].
Qed. Qed.
Next Obligation. Next Obligation.
...@@ -71,22 +72,17 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG). ...@@ -71,22 +72,17 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG).
apply EQp; [now eauto with arith | assumption]. apply EQp; [now eauto with arith | assumption].
Qed. Qed.
Definition vs (m1 m2 : mask) (p q : Props) : Props := Definition vs m1 m2 P Q : Props :=
(p pvs m1 m2 q). (P pvs m1 m2 Q).
End ViewShifts. End ViewShifts.
Section ViewShiftProps. Section ViewShiftProps.
Local Open Scope mask_scope.
Local Open Scope ra_scope.
Local Open Scope bi_scope.
Implicit Types (p q r : Props) (i : nat) (m : mask).
Definition mask_sing i := mask_set mask_emp i True. Definition mask_sing i := mask_set mask_emp i True.
Lemma vsTimeless m p : Lemma vsTimeless m P :
timeless p vs m m ( p) p. timeless P vs m m (P) P.
Proof. Proof.
intros w' n r1 HTL w HSub; rewrite ->HSub in HTL; clear w' HSub. intros w' n r1 HTL w HSub; rewrite ->HSub in HTL; clear w' HSub.
intros np rp HLe HS Hp w1; intros. intros np rp HLe HS Hp w1; intros.
...@@ -96,13 +92,13 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG). ...@@ -96,13 +92,13 @@ Module IrisVS (RL : RA_T) (C : CORE_LANG).
rewrite <- HSub; apply HTL, Hp; [reflexivity | assumption]. rewrite <- HSub; apply HTL, Hp; [reflexivity | assumption].
Qed. Qed.
Lemma vsOpen i p : Lemma vsOpen i P :
valid (vs (mask_sing i) mask_emp (inv i p) ( p)). valid (vs (mask_sing i) mask_emp (inv i P) (P)).
Proof. Proof.
intros pw nn r w _; clear r pw.