From a01925c464eb72c5aa5651b164568509aa6ae32e Mon Sep 17 00:00:00 2001
From: Filip Sieczkowski <filips@cs.au.dk>
Date: Wed, 4 Jun 2014 16:44:09 +0200
Subject: [PATCH] Simplified some def's, proved more lemmas (box, composition
of ghosts, more view-shifts), stated lemmas about hoare triples.
---
iris.v | 561 ++++++++++++++++++++++++++++++++++++++++-----------------
1 file changed, 394 insertions(+), 167 deletions(-)
diff --git a/iris.v b/iris.v
index bef92ebde..51e592ff4 100644
--- a/iris.v
+++ b/iris.v
@@ -156,6 +156,53 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
| None => ⊥
end.
+ Lemma ores_equiv_eq (r1 r2 : option res) (HEq : r1 == r2) : r1 = r2.
+ Proof.
+ destruct r1 as [r1 |]; destruct r2 as [r2 |]; try contradiction;
+ simpl in HEq; subst; reflexivity.
+ Qed.
+
+ (** 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 |].
+ exists r; now erewrite comm, pcm_op_unit by apply _.
+ Qed.
+
+ (** Ghost state ownership **)
+ Lemma ownL_sc (u t : option RL.res) :
+ ownL (u · t)%pcm == ownL u * ownL t.
+ Proof.
+ intros w n r; split; [intros Hut | intros [r1 [r2 [EQr [Hu Ht] ] ] ] ].
+ - destruct (u · t)%pcm as [ut |] eqn: EQut; [| contradiction].
+ do 13 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 RP.res, u) (pcm_unit RP.res, t).
+ split; [unfold pcm_op, res_op, pcm_op_prod | split; do 13 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].
+ rewrite <- EQt, assoc, (comm (Some r1)) in EQr.
+ rewrite <- EQu, assoc, <- (assoc (Some rt · Some ru)%pcm) in EQr.
+ unfold pcm_op at 3, res_op at 4, pcm_op_prod at 1 in EQr.
+ erewrite pcm_op_unit in EQr by apply _; clear EQu EQt.
+ destruct (Some u · Some t)%pcm as [ut |];
+ [| now erewrite comm, pcm_op_zero in EQr by apply _].
+ destruct (Some rt · Some ru)%pcm as [rut |];
+ [| now erewrite pcm_op_zero in EQr by apply _].
+ exists rut; assumption.
+ Qed.
+
Section Erasure.
Local Open Scope pcm_scope.
Local Open Scope bi_scope.
@@ -208,11 +255,11 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
Global Instance preo_unit : preoType () := disc_preo ().
- Program Definition erasure (σ : state) (m : mask) (r s : res) (w : Wld) : UPred () :=
+ Program Definition erasure (σ : state) (m : mask) (r s : option res) (w : Wld) : UPred () :=
â–¹ (mkUPred (fun n _ =>
- erase_state (option_map fst (Some r · Some s)) σ
+ erase_state (option_map fst (r · s)) σ
/\ exists rs : nat -f> res,
- erase rs == Some s /\
+ erase rs == s /\
forall i (Hm : m i),
(i ∈ dom rs <-> i ∈ dom w) /\
forall π ri (HLw : w i == Some π) (HLrs : rs i == Some ri),
@@ -222,9 +269,10 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
setoid_rewrite HLe; eassumption.
Qed.
- Global Instance erasure_equiv σ : Proper (meq ==> eq ==> eq ==> equiv ==> equiv) (erasure σ).
+ Global Instance erasure_equiv σ : Proper (meq ==> equiv ==> equiv ==> equiv ==> equiv) (erasure σ).
Proof.
- intros m1 m2 EQm r r' EQr s s' EQs w1 w2 EQw [| n] []; [reflexivity |]; subst r' s'.
+ intros m1 m2 EQm r r' EQr s s' EQs w1 w2 EQw [| n] []; [reflexivity |];
+ apply ores_equiv_eq in EQr; apply ores_equiv_eq in EQs; subst r' s'.
split; intros [HES [rs [HE HM] ] ]; (split; [tauto | clear HES; exists rs]).
- split; [assumption | intros; apply EQm in Hm; split; [| setoid_rewrite <- EQw; apply HM, Hm] ].
destruct (HM _ Hm) as [HD _]; rewrite HD; clear - EQw.
@@ -263,25 +311,31 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
Local Open Scope pcm_scope.
Local Obligation Tactic := intros.
+Lemma erasure_not_empty σ m r s w k (HN : r · s == 0) :
+ ~ erasure σ m r s w @ S k.
+Proof.
+ intros [HD _]; apply ores_equiv_eq in HN; setoid_rewrite HN in HD.
+ now apply erase_state_nonzero in HD.
+Qed.
+
Program Definition preVS (m1 m2 : mask) (p : Props) (w : Wld) : UPred res :=
- mkUPred (fun n r => forall w1 rf rr s mf σ k (HSub : w ⊑ w1) (HLe : k < n)
- (HD : mf # m1 ∪ m2) (HEq : Some r · Some rf == Some rr)
- (HE : erasure σ (m1 ∪ mf) rr s w1 @ S k),
- exists w2 r' rr' s',
- w1 ⊑ w2 /\ p w2 (S k) r' /\ Some r' · Some rf == Some rr'
- /\ erasure σ (m2 ∪ mf) rr' s' w2 @ S k) _.
+ mkUPred (fun n r => forall w1 rf s mf σ k (HSub : w ⊑ w1) (HLe : k < n)
+ (HD : mf # m1 ∪ m2)
+ (HE : erasure σ (m1 ∪ mf) (Some r · rf) s w1 @ S k),
+ exists w2 r' s',
+ w1 ⊑ w2 /\ p w2 (S k) r'
+ /\ erasure σ (m2 ∪ mf) (Some r' · rf) s' w2 @ S k) _.
Next Obligation.
intros n1 n2 r1 r2 HLe [rd HR] HP; intros.
- rewrite <- HR, (comm (Some rd)), <- assoc in HEq; clear r2 HR.
- destruct (Some rd · Some rf) as [rf' |] eqn: HR;
- [| erewrite comm, pcm_op_zero in HEq by apply _; contradiction].
- destruct (HP w1 rf' rr s mf σ k) as [w2 [r1' [rr' [s' [HW [HP' [HR' HE'] ] ] ] ] ] ]; try assumption; [|].
- - eauto with arith.
- - rewrite <- HR, assoc in HR'; clear rf' HR HEq HP.
- destruct (Some r1' · Some rd) as [r2' |] eqn: HR;
- [| erewrite pcm_op_zero in HR' by apply _; contradiction].
- exists w2 r2' rr' s'; split; [assumption | split; [| split; assumption] ].
- eapply uni_pred, HP'; [| exists rd; rewrite comm, HR]; reflexivity.
+ destruct (HP w1 (Some rd · rf) s mf σ k) as [w2 [r1' [s' [HW [HP' HE'] ] ] ] ];
+ try assumption; [now eauto with arith | |].
+ - eapply erasure_equiv, HE; try reflexivity.
+ rewrite assoc, (comm (Some r1)), HR; reflexivity.
+ - rewrite assoc, (comm (Some r1')) in HE'.
+ destruct (Some rd · Some r1') as [r2' |] eqn: HR';
+ [| apply erasure_not_empty in HE'; [contradiction | now erewrite !pcm_op_zero by apply _] ].
+ exists w2 r2' s'; split; [assumption | split; [| assumption] ].
+ eapply uni_pred, HP'; [| exists rd; rewrite HR']; reflexivity.
Qed.
Program Definition pvs (m1 m2 : mask) : Props -n> Props :=
@@ -297,19 +351,19 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
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).
assert (HSE := extend_sub _ _ _ _ EQw HSub); specialize (HP (extend w2' w1)).
- edestruct HP as [w1'' [r' [rr' [s' [HW HH] ] ] ] ]; try eassumption; clear HP; [ | ].
+ edestruct HP as [w1'' [r' [s' [HW HH] ] ] ]; try eassumption; clear HP; [ | ].
+ eapply erasure_dist, HE; [symmetry; eassumption | now eauto with arith].
+ symmetry in HDE; assert (HDE' := extend_dist _ _ _ _ HDE HW).
- assert (HSE' := extend_sub _ _ _ _ HDE HW); destruct HH as [HP [HR HE'] ];
- exists (extend w1'' w2') r' rr' s'; split; [assumption | split; [| split; [assumption |] ] ].
+ assert (HSE' := extend_sub _ _ _ _ HDE HW); destruct HH as [HP HE'];
+ exists (extend w1'' w2') r' s'; split; [assumption | split].
* eapply (met_morph_nonexp _ _ p), HP ; [symmetry; eassumption | now eauto with arith].
* eapply erasure_dist, HE'; [symmetry; eassumption | now eauto with arith].
- assert (HDE := extend_dist _ _ _ _ EQw HSub); assert (HSE := extend_sub _ _ _ _ EQw HSub); specialize (HP (extend w2' w2)).
- edestruct HP as [w1'' [r' [rr' [s' [HW HH] ] ] ] ]; try eassumption; clear HP; [ | ].
+ edestruct HP as [w1'' [r' [s' [HW HH] ] ] ]; try eassumption; clear HP; [ | ].
+ eapply erasure_dist, HE; [symmetry; eassumption | now eauto with arith].
+ symmetry in HDE; assert (HDE' := extend_dist _ _ _ _ HDE HW).
- assert (HSE' := extend_sub _ _ _ _ HDE HW); destruct HH as [HP [HR HE'] ];
- exists (extend w1'' w2') r' rr' s'; split; [assumption | split; [| split; [assumption |] ] ].
+ assert (HSE' := extend_sub _ _ _ _ HDE HW); destruct HH as [HP HE'];
+ exists (extend w1'' w2') r' s'; split; [assumption | split].
* eapply (met_morph_nonexp _ _ p), HP ; [symmetry; eassumption | now eauto with arith].
* eapply erasure_dist, HE'; [symmetry; eassumption | now eauto with arith].
Qed.
@@ -324,10 +378,10 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
Qed.
Next Obligation.
intros p1 p2 EQp w n' r HLt; split; intros HP w1; intros.
- - edestruct HP as [w2 [r' [rr' [s' [HW [HP' HE'] ] ] ] ] ]; try eassumption; [].
+ - edestruct HP as [w2 [r' [s' [HW [HP' HE'] ] ] ] ]; try eassumption; [].
clear HP; repeat (eexists; try eassumption); [].
apply EQp; [now eauto with arith | assumption].
- - edestruct HP as [w2 [r' [rr' [s' [HW [HP' HE'] ] ] ] ] ]; try eassumption; [].
+ - edestruct HP as [w2 [r' [s' [HW [HP' HE'] ] ] ] ]; try eassumption; [].
clear HP; repeat (eexists; try eassumption); [].
apply EQp; [now eauto with arith | assumption].
Qed.
@@ -358,30 +412,21 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
destruct HE as [HES [rs [HE HM] ] ].
destruct (rs i) as [ri |] eqn: HLr.
- rewrite erase_remove with (i := i) (r := ri) in HE by assumption.
- destruct (Some rr · Some s) as [ss |] eqn: HR; setoid_rewrite HR in HES;
- [| contradiction (erase_state_nonzero _ HES) ].
- destruct (Some r · Some rf) as [rr' |] eqn: HR1;
- [simpl in HEq; subst rr' | contradiction].
- destruct (Some ri · erase (fdRemove i rs)) as [s' |] eqn: HR2;
- [simpl in HE; subst s' | contradiction].
- assert (HEq : Some r · Some ri · Some rf · erase (fdRemove i rs) == Some ss).
- { rewrite <- (assoc (Some r)), (comm (Some ri)), assoc, HR1, <- assoc, HR2, HR; reflexivity. }
- clear HR HR1 HR2; destruct (Some r · Some ri) as [rri |] eqn: HR1;
- [| now erewrite !pcm_op_zero in HEq by apply _].
- destruct (Some rri · Some rf) as [rr' |] eqn: HR2;
- [| now erewrite pcm_op_zero in HEq by apply _].
- destruct (erase (fdRemove i rs)) as [s' |] eqn: HRS;
- [| now erewrite comm, pcm_op_zero in HEq by apply _].
- exists w' rri rr' s'; split; [reflexivity | split; [| split; [rewrite HR2; reflexivity | split] ] ].
+ assert (HR : Some r · rf · s == Some r · Some ri · rf · erase (fdRemove i rs))
+ by (rewrite <- HE, assoc, <- (assoc (Some r)), (comm rf), assoc; reflexivity).
+ apply ores_equiv_eq in HR; setoid_rewrite HR in HES; clear HR.
+ destruct (Some r · Some ri) as [rri |] eqn: HR;
+ [| erewrite !pcm_op_zero in HES by apply _; now apply erase_state_nonzero in HES].
+ exists w' rri (erase (fdRemove i rs)); split; [reflexivity |].
+ split; [| split; [assumption |] ].
+ simpl; eapply HInv; [now auto with arith |].
- specialize (HSub i); rewrite HLu in HSub.
- eapply uni_pred, HM with i; [| exists r; rewrite <- HR1 | | | rewrite HLr]; try reflexivity; [|].
+ eapply uni_pred, HM with i;
+ [| exists r; rewrite <- HR | | | rewrite HLr]; try reflexivity; [|].
* left; unfold mask_sing, mask_set.
destruct (Peano_dec.eq_nat_dec i i); tauto.
- * symmetry; destruct (w' i); [assumption | contradiction].
- + destruct (Some rr' · Some s') as [ss' |] eqn: HR; [| contradiction].
- setoid_rewrite HR; simpl in HEq; subst; assumption.
- + exists (fdRemove i rs); split; [rewrite HRS; reflexivity | intros j Hm].
+ * specialize (HSub i); rewrite HLu in HSub.
+ symmetry; destruct (w' i); [assumption | contradiction].
+ + exists (fdRemove i rs); split; [reflexivity | intros j Hm].
destruct Hm as [| Hm]; [contradiction |]; specialize (HD j); simpl in HD.
unfold mask_sing, mask_set in HD; destruct (Peano_dec.eq_nat_dec i j);
[subst j; contradiction HD; tauto | clear HD].
@@ -393,7 +438,7 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
destruct (Peano_dec.eq_nat_dec i i); tauto.
Qed.
- (*Lemma vsClose i p :
+ Lemma vsClose i p :
valid (vs mask_emp (mask_sing i) (inv i p * ▹ p) ⊤).
Proof.
intros pw nn r w _; clear r pw.
@@ -402,38 +447,51 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
apply ı in HInv; rewrite (isoR p) in HInv.
(* get rid of the invisible 1/2 *)
do 8 red in HInv.
- destruct k as [| k]; [now inversion HGt |].
destruct HE as [HES [rs [HE HM] ] ].
- exists w' 1 (r · s); split; [reflexivity | split; [exact I |] ].
- split; [erewrite pcm_op_unit, assoc, (comm rf) by apply _; assumption |].
- remember (match rs i with Some ri => ri | None => 1 end) as ri eqn: EQri.
- exists (fdUpdate i (ri · r) rs); split; intros.
- - clear -HE EQri; destruct (rs i) as [rsi |] eqn: EQrsi; subst;
- [erewrite erase_insert_old; [reflexivity | assumption] |].
- erewrite pcm_op_unit, erase_insert_new; [reflexivity | assumption | apply _].
- - specialize (HD i0); unfold mask_sing, mask_set in *; simpl in Hm, HD.
- destruct (Peano_dec.eq_nat_dec i i0); [subst i0; clear Hm | destruct Hm as [Hm | Hm]; [contradiction |] ].
- + split; intros.
- * specialize (HSub i); rewrite HLu in HSub.
- rewrite !fdLookup_in_strong, fdUpdate_eq; destruct (w' i);
- [intuition now eauto | contradiction].
- * rewrite fdUpdate_eq in HLrs; simpl in HLrs; subst ri0.
- destruct n as [| n]; [now inversion HLe |]; simpl in HP.
- rewrite <- HSub; specialize (HSub i); rewrite HLu in HSub.
- destruct (w' i) as [Ï€' |]; [| contradiction]; simpl in HSub, HLw.
- rewrite <- HLw, <- HSub; apply HInv; [now auto with arith |].
- eapply uni_pred, HP; [now auto with arith |].
- subst r; rewrite assoc; eexists; reflexivity.
- + rewrite fdLookup_in_strong, fdUpdate_neq, <- fdLookup_in_strong by assumption.
- auto.
- Qed.*)
+ exists w' (pcm_unit _) (Some r · s); split; [reflexivity | split; [exact I |] ].
+ assert (HR' : Some r · rf · s = rf · (Some r · s))
+ by (apply ores_equiv_eq; rewrite assoc, (comm rf); reflexivity).
+ setoid_rewrite HR' in HES; erewrite pcm_op_unit by apply _.
+ split; [assumption |].
+ remember (match rs i with Some ri => ri | None => pcm_unit _ end) as ri eqn: EQri.
+ destruct (Some ri · Some r) as [rri |] eqn: EQR.
+ - exists (fdUpdate i rri rs); split; [| intros j Hm].
+ + symmetry; rewrite <- HE; clear - EQR EQri; destruct (rs i) as [rsi |] eqn: EQrsi; subst;
+ [eapply erase_insert_old; [eassumption | rewrite <- EQR; reflexivity] |].
+ erewrite pcm_op_unit in EQR by apply _; rewrite EQR.
+ now apply erase_insert_new.
+ + specialize (HD j); unfold mask_sing, mask_set in *; simpl in Hm, HD.
+ destruct (Peano_dec.eq_nat_dec i j);
+ [subst j; clear Hm |
+ destruct Hm as [Hm | Hm]; [contradiction | rewrite fdLookup_in_strong, fdUpdate_neq, <- fdLookup_in_strong by assumption; now auto] ].
+ rewrite !fdLookup_in_strong, fdUpdate_eq.
+ destruct n as [| n]; [now inversion HLe | simpl in HP].
+ rewrite HSub in HP; specialize (HSub i); rewrite HLu in HSub.
+ destruct (w' i) as [Ï€' |]; [| contradiction].
+ split; [intuition now eauto | intros].
+ simpl in HLw, HLrs, HSub; subst ri0; rewrite <- HLw, <- HSub.
+ apply HInv; [now auto with arith |].
+ eapply uni_pred, HP; [now auto with arith |].
+ assert (HT : Some ri · Some r1 · Some r2 == Some rri)
+ by (rewrite <- EQR, <- HR, assoc; reflexivity); clear - HT.
+ destruct (Some ri · Some r1) as [rd |];
+ [| now erewrite pcm_op_zero in HT by apply _].
+ exists rd; assumption.
+ - destruct (rs i) as [rsi |] eqn: EQrsi; subst;
+ [| erewrite pcm_op_unit in EQR by apply _; discriminate].
+ contradiction (erase_state_nonzero σ); clear - HE HES EQrsi EQR.
+ assert (HH : rf · (Some r · s) = 0); [clear HES | rewrite HH in HES; assumption].
+ apply ores_equiv_eq; rewrite <- HE, erase_remove by eassumption.
+ rewrite (assoc (Some r)), (comm (Some r)), EQR, comm.
+ erewrite !pcm_op_zero by apply _; reflexivity.
+ Qed.
Lemma vsTrans p q r m1 m2 m3 (HMS : m2 ⊆ m1 ∪ m3) :
vs m1 m2 p q ∧ vs m2 m3 q r ⊑ vs m1 m3 p r.
Proof.
intros w' n r1 [Hpq Hqr] w HSub; specialize (Hpq _ HSub); rewrite HSub in Hqr; clear w' HSub.
intros np rp HLe HS Hp w1; intros; specialize (Hpq _ _ HLe HS Hp).
- edestruct Hpq as [w2 [rq [rrq [sq [HSw12 [Hq [HEq' HErq] ] ] ] ] ] ]; try eassumption; [|].
+ edestruct Hpq as [w2 [rq [sq [HSw12 [Hq HEq] ] ] ] ]; try eassumption; [|].
{ (* XXX: possible lemma *)
clear - HD HMS.
intros j [Hmf Hm12]; apply (HD j); split; [assumption |].
@@ -441,7 +499,7 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
}
clear HS; assert (HS : pcm_unit _ ⊑ rq) by (exists rq; now erewrite comm, pcm_op_unit by apply _).
rewrite <- HLe, HSub in Hqr; specialize (Hqr _ HSw12); clear Hpq HE w HSub Hp.
- edestruct (Hqr (S k) _ HLe0 HS Hq w2) as [w3 [rR [rrR [sR [HSw23 [Hr [HR HEr] ] ] ] ] ] ];
+ edestruct (Hqr (S k) _ HLe0 HS Hq w2) as [w3 [rR [sR [HSw23 [Hr HEr] ] ] ] ];
try (reflexivity || eassumption); [now auto with arith | |].
{ (* XXX: possible lemma *)
clear - HD HMS.
@@ -457,29 +515,32 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
Proof.
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 rr s; split; [reflexivity | split; [| split; assumption ] ].
+ exists w1 rp s; split; [reflexivity | split; [| assumption ] ].
eapply Himp; [assumption | now eauto with arith | exists rp; now erewrite comm, pcm_op_unit by apply _ |].
unfold lt in HLe0; rewrite HLe0, <- HSub; assumption.
Qed.
- (* Lemma vsFrame p q r m1 m2 mf (HDisj : mf # m1 ∪ m2) :
+ Lemma vsFrame p q r m1 m2 mf (HDisj : mf # m1 ∪ m2) :
vs m1 m2 p q ⊑ vs (m1 ∪ mf) (m2 ∪ mf) (p * r) (q * r).
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 : 1 ⊑ rp) by (exists rp; erewrite comm, pcm_op_unit by apply _; reflexivity).
- specialize (HVS _ _ HLe HS Hp w' s (rr · rf) (mf ∪ mf0) σ k); clear HS.
+ assert (HS : pcm_unit _ ⊑ rp) by (exists rp; now erewrite comm, pcm_op_unit by apply _).
+ specialize (HVS _ _ HLe HS Hp w' (Some rr · rf) s (mf ∪ mf0) σ k); clear HS.
destruct HVS as [w'' [rq [s' [HSub' [Hq HEq] ] ] ] ]; try assumption; [| |].
- - (* disjointness: possible lemma *)
+ - (* disjointness of masks: possible lemma *)
clear - HD HDisj; intros i [ [Hmf | Hmf] Hm12]; [eapply HDisj; now eauto |].
eapply HD; split; [eassumption | tauto].
- rewrite assoc, HR; eapply erasure_equiv, HE; try reflexivity; [].
clear; intros i; tauto.
- - exists w'' (rq · rr) s'; split; [assumption | split].
- + rewrite HSub, HSub', <- HLe0 in Hr; exists rq rr; now auto.
- + rewrite <- assoc; eapply erasure_equiv, HEq; try reflexivity; [].
+ - rewrite assoc in HEq; destruct (Some rq · Some rr) as [rqr |] eqn: HR';
+ [| apply erasure_not_empty in HEq; [contradiction | now erewrite !pcm_op_zero by apply _] ].
+ exists w'' rqr s'; split; [assumption | split].
+ + unfold lt in HLe0; rewrite HSub, HSub', <- HLe0 in Hr; exists rq rr.
+ rewrite HR'; split; now auto.
+ + eapply erasure_equiv, HEq; try reflexivity; [].
clear; intros i; tauto.
- Qed.*)
+ Qed.
Lemma vsFalse m1 m2 :
valid (vs m1 m2 ⊥ ⊥).
@@ -488,7 +549,84 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
intros n r _ _ HB; contradiction.
Qed.
- (* XXX missing statements: NewInv, NewGhost, GhostUpd, VSTimeless *)
+ Global Instance nat_type : Setoid nat := discreteType.
+ Global Instance nat_metr : metric nat := discreteMetric.
+ Global Instance nat_cmetr : cmetric nat := discreteCMetric.
+
+ 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.
+ Qed.
+
+ Lemma fresh_region (w : Wld) m (HInf : mask_infinite m) :
+ exists i, m i /\ w i = None.
+ Proof.
+ destruct (HInf (S (List.last (dom w) 0%nat))) as [i [HGe Hm] ];
+ exists i; split; [assumption |]; clear - HGe.
+ rewrite <- fdLookup_notin_strong.
+ destruct w as [ [| [n v] w] wP]; unfold dom in *; simpl findom_t in *; [tauto |].
+ simpl List.map in *; rewrite last_cons in HGe.
+ unfold ge in HGe; intros HIn; eapply Gt.gt_not_le, HGe.
+ apply Le.le_n_S, SS_last_le; assumption.
+ Qed.
+
+ (* XXX: move up to definitions *)
+ Definition injProp (P : Prop) : Props :=
+ pcmconst (up_cr (const P)).
+
+ Instance LP_mask m : LimitPreserving m.
+ Proof.
+ intros σ σc Hp; apply Hp.
+ Qed.
+
+ Lemma vsNewInv p m (HInf : mask_infinite m) :
+ valid (vs m m (â–¹ p) (xist (inv' m p))).
+ Proof.
+ intros pw nn r w _; clear r pw.
+ intros n r _ _ HP w'; clear nn; intros.
+ destruct n as [| n]; [now inversion HLe | simpl in HP].
+ rewrite HSub in HP; clear w HSub; rename w' into w.
+ destruct (fresh_region w m HInf) as [i [Hm HLi] ].
+ assert (HSub : w ⊑ fdUpdate i (ı' p) w).
+ { 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) (pcm_unit _) (Some r · s); split; [assumption | split].
+ - exists (exist _ i Hm); do 16 red.
+ unfold proj1_sig; rewrite fdUpdate_eq; reflexivity.
+ - erewrite pcm_op_unit by apply _.
+ assert (HR : rf · (Some r · s) = Some r · rf · s)
+ by (apply ores_equiv_eq; rewrite assoc, (comm rf); reflexivity).
+ destruct HE as [HES [rs [HE HM] ] ].
+ split; [setoid_rewrite HR; assumption | clear HR].
+ assert (HRi : rs i = None).
+ { destruct (HM i) as [HDom _]; [tauto |].
+ rewrite <- fdLookup_notin_strong, HDom, fdLookup_notin_strong; assumption.
+ }
+ exists (fdUpdate i r rs); split; [now rewrite <- erase_insert_new, HE by assumption | intros j Hm'].
+ rewrite !fdLookup_in_strong; destruct (Peano_dec.eq_nat_dec i j).
+ + subst j; rewrite !fdUpdate_eq; split; [intuition now eauto | intros].
+ simpl in HLw, HLrs; subst ri; rewrite <- HLw, isoR, <- HSub.
+ eapply uni_pred, HP; [now auto with arith | reflexivity].
+ + rewrite !fdUpdate_neq, <- !fdLookup_in_strong by assumption.
+ setoid_rewrite <- HSub.
+ apply HM; assumption.
+ Qed.
+
+ (* XXX missing statements: NewGhost, GhostUpd, VSTimeless *)
End ViewShiftProps.
@@ -512,52 +650,49 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
Local Obligation Tactic := intros; eauto with typeclass_instances.
Definition wpFP m (WP : expr -n> (value -n> Props) -n> Props) e φ w n r :=
- forall w' k s rf rr σ
- (HSw : w ⊑ w') (HLt : k < n) (HR : Some r · Some rf == Some rr)
- (HE : erasure σ m rr s w' @ S k),
+ forall w' k s rf σ (HSw : w ⊑ w') (HLt : k < n)
+ (HE : erasure σ m (Some r · rf) s w' @ S k),
(forall (HV : is_value e),
- exists w'' r' rr' s', w' ⊑ w'' /\ φ (exist _ e HV) w'' (S k) r'
- /\ Some r' · Some rf == Some rr'
- /\ erasure σ m rr' s' w'' @ S k) /\
+ exists w'' r' s', w' ⊑ w'' /\ φ (exist _ e HV) w'' (S k) r'
+ /\ erasure σ m (Some r' · rf) s' w'' @ S k) /\
(forall σ' ei ei' K (HDec : e = K [[ ei ]])
(HStep : prim_step (ei, σ) (ei', σ')),
- exists w'' r' rr' s', w' ⊑ w'' /\ WP (K [[ ei' ]]) φ w'' k r'
- /\ Some r' · Some rf == Some rr'
- /\ erasure σ' m rr' s' w'' @ k) /\
+ exists w'' r' s', w' ⊑ w'' /\ WP (K [[ ei' ]]) φ w'' k r'
+ /\ erasure σ' m (Some r' · rf) s' w'' @ k) /\
(forall e' K (HDec : e = K [[ e' ]]),
- exists w'' rfk rret rr' s', w' ⊑ w'' /\ Some rfk · Some rret · Some rf == Some rr'
- /\ WP (K [[ fork_ret ]]) φ w'' k rret
- /\ WP e' (umconst ⊤) w'' k rfk
- /\ erasure σ m rr' s' w'' @ k).
+ exists w'' rfk rret s', w' ⊑ w''
+ /\ WP (K [[ fork_ret ]]) φ w'' k rret
+ /\ WP e' (umconst ⊤) w'' k rfk
+ /\ erasure σ m (Some rfk · Some rret · rf) s' w'' @ k).
Program Definition wpF m : (expr -n> (value -n> Props) -n> Props) -n> expr -n> (value -n> Props) -n> Props :=
n[(fun WP => n[(fun e => n[(fun φ => m[(fun w => mkUPred (wpFP m WP e φ w) _)])])])].
Next Obligation.
- intros n1 n2 r1 r2 HLe [rd EQr] Hp w' k s rf rr σ HSw HLt HR HE.
- rewrite <- EQr, (comm (Some rd)), <- assoc in HR.
- destruct (Some rd · Some rf) as [rf' |] eqn: HRF;
- [| now erewrite comm, pcm_op_zero in HR by apply _].
- specialize (Hp w' k s rf' rr σ); destruct Hp as [HV [HS HF] ];
+ intros n1 n2 r1 r2 HLe [rd EQr] Hp w' k s rf σ HSw HLt HE.
+ rewrite <- EQr, (comm (Some rd)), <- assoc in HE.
+ specialize (Hp w' k s (Some rd · rf) σ); destruct Hp as [HV [HS HF] ];
[| now eauto with arith | ..]; try assumption; [].
split; [clear HS HF | split; [clear HV HF | clear HV HS] ]; intros.
- - specialize (HV HV0); destruct HV as [w'' [r2' [rr' [s' [HSw' [Hφ [HR' HE'] ] ] ] ] ] ].
- rewrite <- HRF, assoc, (comm (Some r2')) in HR'.
- destruct (Some rd · Some r2') as [r1' |] eqn: HR1;
- [| now erewrite pcm_op_zero in HR' by apply _].
- exists w'' r1' rr' s'; split; [assumption | split; [| split; assumption] ].
- eapply uni_pred, Hφ; [| eexists; rewrite <- HR1]; reflexivity.
- - specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r2' [rr' [s' [HSw' [HWP [HR' HE'] ] ] ] ] ] ].
- rewrite <- HRF, assoc, (comm (Some r2')) in HR'.
- destruct (Some rd · Some r2') as [r1' |] eqn: HR1;
- [| now erewrite pcm_op_zero in HR' by apply _].
- exists w'' r1' rr' s'; split; [assumption | split; [| split; assumption] ].
- eapply uni_pred, HWP; [| eexists; rewrite <- HR1]; reflexivity.
- - specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret2 [rr' [s' [HSw' [HR' [HWR [HWF HE'] ] ] ] ] ] ] ] ].
- rewrite <- HRF, assoc, <- (assoc (Some rfk)), (comm (Some rret2)) in HR'.
- destruct (Some rd · Some rret2) as [rret1 |] eqn: HR1;
- [| now erewrite (comm _ 0), !pcm_op_zero in HR' by apply _].
- exists w'' rfk rret1 rr'; exists s'; repeat (split; try assumption); [].
- eapply uni_pred, HWR; [| eexists; rewrite <- HR1]; reflexivity.
+ - specialize (HV HV0); destruct HV as [w'' [r1' [s' [HSw' [Hφ HE'] ] ] ] ].
+ rewrite assoc, (comm (Some r1')) in HE'.
+ destruct (Some rd · Some r1') as [r2' |] eqn: HR;
+ [| apply erasure_not_empty in HE'; [contradiction | now erewrite !pcm_op_zero by apply _] ].
+ exists w'' r2' s'; split; [assumption | split; [| assumption] ].
+ eapply uni_pred, Hφ; [| eexists; rewrite <- HR]; reflexivity.
+ - specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r1' [s' [HSw' [HWP HE'] ] ] ] ].
+ rewrite assoc, (comm (Some r1')) in HE'.
+ destruct k as [| k]; [exists w'' r1' s'; simpl erasure; tauto |].
+ destruct (Some rd · Some r1') as [r2' |] eqn: HR;
+ [| apply erasure_not_empty in HE'; [contradiction | now erewrite !pcm_op_zero by apply _] ].
+ exists w'' r2' s'; split; [assumption | split; [| assumption] ].
+ eapply uni_pred, HWP; [| eexists; rewrite <- HR]; reflexivity.
+ - specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret1 [s' [HSw' [HWR [HWF HE'] ] ] ] ] ] ].
+ destruct k as [| k]; [exists w'' rfk rret1 s'; simpl erasure; tauto |].
+ rewrite assoc, <- (assoc (Some rfk)), (comm (Some rret1)) in HE'.
+ destruct (Some rd · Some rret1) as [rret2 |] eqn: HR;
+ [| apply erasure_not_empty in HE'; [contradiction | now erewrite (comm _ 0), !pcm_op_zero by apply _] ].
+ exists w'' rfk rret2 s'; repeat (split; try assumption); [].
+ eapply uni_pred, HWR; [| eexists; rewrite <- HR]; reflexivity.
Qed.
Next Obligation.
intros w1 w2 EQw n r; simpl.
@@ -571,44 +706,44 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
edestruct (Hp (extend w2' w1)) as [HV [HS HF] ]; try eassumption;
[eapply erasure_dist, HE; [eassumption | now eauto with arith] |].
split; [clear HS HF | split; [clear HV HF | clear HV HS] ]; intros.
- + specialize (HV HV0); destruct HV as [w1'' [r' [rr' [s' [HSw'' [Hφ [HR' HE'] ] ] ] ] ] ].
+ + specialize (HV HV0); destruct HV as [w1'' [r' [s' [HSw'' [Hφ HE'] ] ] ] ].
assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
- exists (extend w1'' w2') r' rr' s'; split; [assumption |].
- split; [| split; [assumption | eapply erasure_dist, HE'; [eassumption | now eauto with arith] ] ].
+ exists (extend w1'' w2') r' s'; split; [assumption |].
+ split; [| eapply erasure_dist, HE'; [eassumption | now eauto with arith] ].
eapply (met_morph_nonexp _ _ (φ _)), Hφ; [eassumption | now eauto with arith].
- + specialize (HS _ _ _ _ HDec HStep); destruct HS as [w1'' [r' [rr' [s' [HSw'' [HWP [HR' HE'] ] ] ] ] ] ].
+ + specialize (HS _ _ _ _ HDec HStep); destruct HS as [w1'' [r' [s' [HSw'' [HWP HE'] ] ] ] ].
assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
- exists (extend w1'' w2') r' rr' s'; split; [assumption |].
- split; [| split; [assumption | eapply erasure_dist, HE'; [eassumption | now eauto with arith] ] ].
+ exists (extend w1'' w2') r' s'; split; [assumption |].
+ split; [| eapply erasure_dist, HE'; [eassumption | now eauto with arith] ].
eapply (met_morph_nonexp _ _ (WP _ _)), HWP; [eassumption | now eauto with arith].
- + specialize (HF _ _ HDec); destruct HF as [w1'' [rfk [rret [rr' [s' [HSw'' [HR' [HWR [HWF HE'] ] ] ] ] ] ] ] ].
+ + specialize (HF _ _ HDec); destruct HF as [w1'' [rfk [rret [s' [HSw'' [HWR [HWF HE'] ] ] ] ] ] ].
assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
- exists (extend w1'' w2') rfk rret rr'; exists s'; do 2 (split; [assumption |]).
+ exists (extend w1'' w2') rfk rret s'; split; [assumption |].
split; [| split; [| eapply erasure_dist, HE'; [eassumption | now eauto with arith] ] ];
eapply (met_morph_nonexp _ _ (WP _ _)); try eassumption; now eauto with arith.
- assert (EQw' := extend_dist _ _ _ _ EQw HSw); assert (HSw' := extend_sub _ _ _ _ EQw HSw); symmetry in EQw'.
edestruct (Hp (extend w2' w2)) as [HV [HS HF] ]; try eassumption;
[eapply erasure_dist, HE; [eassumption | now eauto with arith] |].
split; [clear HS HF | split; [clear HV HF | clear HV HS] ]; intros.
- + specialize (HV HV0); destruct HV as [w1'' [r' [rr' [s' [HSw'' [Hφ [HR' HE'] ] ] ] ] ] ].
+ + specialize (HV HV0); destruct HV as [w1'' [r' [s' [HSw'' [Hφ HE'] ] ] ] ].
assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
- exists (extend w1'' w2') r' rr' s'; split; [assumption |].
- split; [| split; [assumption | eapply erasure_dist, HE'; [eassumption | now eauto with arith] ] ].
+ exists (extend w1'' w2') r' s'; split; [assumption |].
+ split; [| eapply erasure_dist, HE'; [eassumption | now eauto with arith] ].
eapply (met_morph_nonexp _ _ (φ _)), Hφ; [eassumption | now eauto with arith].
- + specialize (HS _ _ _ _ HDec HStep); destruct HS as [w1'' [r' [rr' [s' [HSw'' [HWP [HR' HE'] ] ] ] ] ] ].
+ + specialize (HS _ _ _ _ HDec HStep); destruct HS as [w1'' [r' [s' [HSw'' [HWP HE'] ] ] ] ].
assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
- exists (extend w1'' w2') r' rr' s'; split; [assumption |].
- split; [| split; [assumption | eapply erasure_dist, HE'; [eassumption | now eauto with arith] ] ].
+ exists (extend w1'' w2') r' s'; split; [assumption |].
+ split; [| eapply erasure_dist, HE'; [eassumption | now eauto with arith] ].
eapply (met_morph_nonexp _ _ (WP _ _)), HWP; [eassumption | now eauto with arith].
- + specialize (HF _ _ HDec); destruct HF as [w1'' [rfk [rret [rr' [s' [HSw'' [HR' [HWR [HWF HE'] ] ] ] ] ] ] ] ].
+ + specialize (HF _ _ HDec); destruct HF as [w1'' [rfk [rret [s' [HSw'' [HWR [HWF HE'] ] ] ] ] ] ].
assert (EQw'' := extend_dist _ _ _ _ EQw' HSw''); symmetry in EQw'';
assert (HSw''' := extend_sub _ _ _ _ EQw' HSw'').
- exists (extend w1'' w2') rfk rret rr'; exists s'; do 2 (split; [assumption |]).
+ exists (extend w1'' w2') rfk rret s'; split; [assumption |].
split; [| split; [| eapply erasure_dist, HE'; [eassumption | now eauto with arith] ] ];
eapply (met_morph_nonexp _ _ (WP _ _)); try eassumption; now eauto with arith.
Qed.
@@ -624,24 +759,24 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
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] ]; try eassumption; [|].
- split; [| split]; intros.
- + clear HS HF; specialize (HV HV0); destruct HV as [w'' [r' [rr' [s' [HSw' [Hφ [HR' HE'] ] ] ] ] ] ].
- exists w'' r' rr' s'; split; [assumption | split; [| split; assumption] ].
+ + clear HS HF; specialize (HV HV0); destruct HV as [w'' [r' [s' [HSw' [Hφ HE'] ] ] ] ].
+ exists w'' r' s'; split; [assumption | split; [| assumption] ].
apply EQφ, Hφ; now eauto with arith.
- + clear HV HF; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [rr' [s' [HSw' [Hφ [HR' HE'] ] ] ] ] ] ].
- exists w'' r' rr' s'; split; [assumption | split; [| split; assumption] ].
+ + clear HV HF; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [s' [HSw' [Hφ HE'] ] ] ] ].
+ exists w'' r' s'; split; [assumption | split; [| assumption] ].
eapply (met_morph_nonexp _ _ (WP _)), Hφ; [symmetry; eassumption | now eauto with arith].
- + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [rr' [s' [HSw' [HR' [HWR [HWF HE'] ] ] ] ] ] ] ] ].
- exists w'' rfk rret rr'; exists s'; repeat (split; try assumption); [].
+ + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [s' [HSw' [HWR [HWF HE'] ] ] ] ] ] ].
+ exists w'' rfk rret s'; repeat (split; try assumption); [].
eapply (met_morph_nonexp _ _ (WP _)), HWR; [symmetry; eassumption | now eauto with arith].
- split; [| split]; intros.
- + clear HS HF; specialize (HV HV0); destruct HV as [w'' [r' [rr' [s' [HSw' [Hφ [HR' HE'] ] ] ] ] ] ].
- exists w'' r' rr' s'; split; [assumption | split; [| split; assumption] ].
+ + clear HS HF; specialize (HV HV0); destruct HV as [w'' [r' [s' [HSw' [Hφ HE'] ] ] ] ].
+ exists w'' r' s'; split; [assumption | split; [| assumption] ].
apply EQφ, Hφ; now eauto with arith.
- + clear HV HF; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [rr' [s' [HSw' [Hφ [HR' HE'] ] ] ] ] ] ].
- exists w'' r' rr' s'; split; [assumption | split; [| split; assumption] ].
+ + clear HV HF; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [s' [HSw' [Hφ HE'] ] ] ] ].
+ exists w'' r' s'; split; [assumption | split; [| assumption] ].
eapply (met_morph_nonexp _ _ (WP _)), Hφ; [eassumption | now eauto with arith].
- + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [rr' [s' [HSw' [HR' [HWR [HWF HE'] ] ] ] ] ] ] ] ].
- exists w'' rfk rret rr'; exists s'; repeat (split; try assumption); [].
+ + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [s' [HSw' [HWR [HWF HE'] ] ] ] ] ] ].
+ exists w'' rfk rret s'; repeat (split; try assumption); [].
eapply (met_morph_nonexp _ _ (WP _)), HWR; [eassumption | now eauto with arith].
Qed.
Next Obligation.
@@ -660,18 +795,18 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
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] ]; try eassumption; [|].
- split; [assumption | split; intros].
- + clear HF HV; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [rr' [s' [HSw' [HWP [HR' HE'] ] ] ] ] ] ].
- exists w'' r' rr' s'; split; [assumption | split; [| split; assumption] ].
+ + clear HF HV; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [s' [HSw' [HWP HE'] ] ] ] ].
+ exists w'' r' s'; split; [assumption | split; [| assumption] ].
eapply (EQWP _ _ _), HWP; now eauto with arith.
- + clear HF HS; specialize (HV _ _ HDec); destruct HV as [w'' [rfk [rret [rr' [s' [HSw' [HR' [HWR [HWF HE'] ] ] ] ] ] ] ] ].
- exists w'' rfk rret rr'; exists s'; do 2 (split; [assumption |]).
+ + clear HF HS; specialize (HV _ _ HDec); destruct HV as [w'' [rfk [rret [s' [HSw' [HWR [HWF HE'] ] ] ] ] ] ].
+ exists w'' rfk rret s'; split; [assumption |].
split; [| split; [| assumption] ]; eapply EQWP; try eassumption; now eauto with arith.
- split; [assumption | split; intros].
- + clear HF HV; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [rr' [s' [HSw' [HWP [HR' HE'] ] ] ] ] ] ].
- exists w'' r' rr' s'; split; [assumption | split; [| split; assumption] ].
+ + clear HF HV; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [s' [HSw' [HWP HE'] ] ] ] ].
+ exists w'' r' s'; split; [assumption | split; [| assumption] ].
eapply (EQWP _ _ _), HWP; now eauto with arith.
- + clear HF HS; specialize (HV _ _ HDec); destruct HV as [w'' [rfk [rret [rr' [s' [HSw' [HR' [HWR [HWF HE'] ] ] ] ] ] ] ] ].
- exists w'' rfk rret rr'; exists s'; do 2 (split; [assumption |]).
+ + clear HF HS; specialize (HV _ _ HDec); destruct HV as [w'' [rfk [rret [s' [HSw' [HWR [HWF HE'] ] ] ] ] ] ].
+ exists w'' rfk rret s'; split; [assumption |].
split; [| split; [| assumption] ]; eapply EQWP; try eassumption; now eauto with arith.
Qed.
@@ -680,18 +815,18 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
intros n WP1 WP2 EQWP e φ w k r HLt.
split; intros Hp w'; intros; edestruct Hp as [HV [HS HF] ]; try eassumption; [|].
- split; [assumption | split; intros].
- + clear HF HV; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [rr' [s' [HSw' [HWP [HR' HE'] ] ] ] ] ] ].
- exists w'' r' rr' s'; split; [assumption | split; [| split; assumption] ].
+ + clear HF HV; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [s' [HSw' [HWP HE'] ] ] ] ].
+ exists w'' r' s'; split; [assumption | split; [| assumption] ].
eapply EQWP, HWP; now eauto with arith.
- + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [rr' [s' [HSw' [HR' [HWR [HWF HE'] ] ] ] ] ] ] ] ].
- exists w'' rfk rret rr'; exists s'; do 2 (split; [assumption |]).
+ + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [s' [HSw' [HWR [HWF HE'] ] ] ] ] ] ].
+ exists w'' rfk rret s'; split; [assumption |].
split; [| split; [| assumption] ]; eapply EQWP; try eassumption; now eauto with arith.
- split; [assumption | split; intros].
- + clear HF HV; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [rr' [s' [HSw' [HWP [HR' HE'] ] ] ] ] ] ].
- exists w'' r' rr' s'; split; [assumption | split; [| split; assumption] ].
+ + clear HF HV; specialize (HS _ _ _ _ HDec HStep); destruct HS as [w'' [r' [s' [HSw' [HWP HE'] ] ] ] ].
+ exists w'' r' s'; split; [assumption | split; [| assumption] ].
eapply EQWP, HWP; now eauto with arith.
- + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [rr' [s' [HSw' [HR' [HWR [HWF HE'] ] ] ] ] ] ] ] ].
- exists w'' rfk rret rr'; exists s'; do 2 (split; [assumption |]).
+ + clear HV HS; specialize (HF _ _ HDec); destruct HF as [w'' [rfk [rret [s' [HSw' [HWR [HWF HE'] ] ] ] ] ] ].
+ exists w'' rfk rret s'; split; [assumption |].
split; [| split; [| assumption] ]; eapply EQWP; try eassumption; now eauto with arith.
Qed.
@@ -702,4 +837,96 @@ Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
End HoareTriples.
+ Section HoareTripleProperties.
+ Local Open Scope mask_scope.
+ Local Open Scope pcm_scope.
+ Local Open Scope bi_scope.
+ Local Open Scope lang_scope.
+
+ Existing Instance LP_isval.
+
+ Implicit Types (P Q R : Props) (i : nat) (m : mask) (e : expr) (φ : value -n> Props) (r : res).
+
+ (** Ret **)
+ Program Definition eqV v : value -n> Props :=
+ 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.
+ Qed.
+
+ Lemma htRet e (HV : is_value e) m :
+ valid (ht m ⊤ e (eqV (exist _ e HV))).
+ Proof.
+ Admitted.
+
+ (** Bind **)
+ Program Definition plugV m φ φ' K :=
+ n[(fun v : value => ht 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)).
+ - apply φ; assumption.
+ - destruct n as [| n]; [apply dist_bound | simpl in EQv].
+ rewrite EQv; reflexivity.
+ Qed.
+
+ Lemma htBind P φ φ' K e m :
+ ht m P e φ ∧ all (plugV m φ φ' K) ⊑ ht m P (K [[ e ]]) φ'.
+ Proof.
+ Admitted.
+
+ Lemma htBind_alt P Q φ φ' K e m
+ (He : Q ⊑ ht m P e φ)
+ (HK : forall v, Q ⊑ ht m (φ v) (K [[` v ]]) φ') :
+ Q ⊑ ht m P (K [[ e ]]) φ'.
+ Admitted.
+
+ Implicit Type (C : Props).
+
+ (** Consequence **)
+
+ Lemma htCons C P P' φ φ' m e
+ (HPre : C ⊑ vs m m P P')
+ (HT : C ⊑ ht m P' e φ')
+ (HPost : forall v, C ⊑ vs m m (φ' v) (φ v)) :
+ C ⊑ ht m P e φ.
+ Admitted.
+
+ Lemma htACons C P P' φ φ' m m' e
+ (HAt : atomic e)
+ (HSub : m' ⊆ m)
+ (HPre : C ⊑ vs m m' P P')
+ (HT : C ⊑ ht m' P' e φ')
+ (HPost : forall v, C ⊑ vs m' m (φ' v) (φ v)) :
+ C ⊑ ht m P e φ.
+ Admitted.
+
+ (** Framing **)
+
+ Lemma htFrame m P R e φ :
+ ht m P e φ ⊑ ht m (P * R) e (lift_bin sc φ (umconst R)).
+ Admitted.
+
+ Lemma htAFrame m P R e φ
+ (HAt : atomic e) :
+ ht m P e φ ⊑ ht m (P * ▹ R) e (lift_bin sc φ (umconst R)).
+ Admitted.
+
+ (** Fork **)
+
+ Lemma htFork m P R e φ :
+ ht m P e φ ⊑ ht m (P * ▹ R) (fork e) (lift_bin sc (eqV (exist _ fork_ret fork_ret_is_value)) (umconst R)).
+ Admitted.
+
+ End HoareTripleProperties.
+
End Iris.
--
GitLab