Require Import List Vbase Varith Vlist extralib.
Require Import Classical ClassicalDescription IndefiniteDescription.
Require Import Permutation permission fslassn fslassnsem.
Require Import GpsSepAlg.
Set Implicit Arguments.
Transparent hplus.
Ltac eq_rect_simpl := rewrite <- ?eq_rect_eq in ×.
Lemmas about permissions on non-atomic locations.
Lemma get_nonzero_permission PS x y z:
@permissionsOK PS x y z → x ≠ Pzero PS ∨ y ≠ Pzero PS ∨ z ≠ Pzero PS.
Proof.
ins. red in H; desf.
repeat (apply permission_plus_not_zero in PSUMnonzero; desf; eauto).
Qed.
Lemma all_permissions_zero PS : @permissionsOK PS (Pzero PS) (Pzero PS) (Pzero PS) → False.
Proof.
ins; apply get_nonzero_permission in H; desf.
Qed.
Lemmas about values and labels.
Lemma HVval_equal PS PSg (Perm Perm': Permission) v
(pNormal pTriangle pNabla : Perm) OK v'
(pNormal' pTriangle' pNabla' : Perm') OK' (EQ: Perm = Perm'):
v = v' → (eq_rect Perm (fun x ⇒ x) pNormal Perm' EQ) = pNormal'
→ (eq_rect Perm (fun x ⇒ x) pTriangle Perm' EQ) = pTriangle'
→ ((eq_rect Perm (fun x ⇒ x) pNabla Perm' EQ)) = pNabla'
→ @HVval PS PSg v Perm pNormal pTriangle pNabla OK = @HVval PS PSg v' Perm' pNormal' pTriangle' pNabla' OK'.
Proof.
ins; desf; f_equal; apply proof_irrelevance.
Qed.
Lemma has_value_alt PS PSg hv v:
has_value hv v ↔ ∃ PErm pNormal pTriangle pNabla OK,
hv = @HVval PS PSg v PErm pNormal pTriangle pNabla OK.
Proof.
unfold has_value; split; ins; desf.
eexists _, _; eauto.
Qed.
Lemma has_value_sim PS PSg (hv hv': HeapVal PS PSg) v (SIM: HVsim hv hv'): has_value hv v ↔ has_value hv' v.
Proof.
unfold has_value; desf; ins; desf; desf.
Qed.
Lemma is_lvalue_implies_is_nonatomic PS PSg (hv : HeapVal PS PSg): is_lvalue hv → is_nonatomic hv.
Proof.
destruct hv; ins.
Qed.
Lemma is_rvalue_implies_is_nonatomic PS PSg (hv : HeapVal PS PSg): is_rvalue hv → is_nonatomic hv.
Proof.
destruct hv; ins.
Qed.
Lemma is_lvalue_implies_normal PS PSg hv: is_lvalue hv → HVlabeled hv HLnormal ∧ hv ≠ @HVnone PS PSg.
Proof.
by destruct hv; ins; desf; split; try apply Pfull_is_not_Pzero.
Qed.
Lemma is_rvalue_implies_normal PS PSg hv: is_rvalue hv → HVlabeled hv HLnormal ∧ hv ≠ @HVnone PS PSg.
Proof.
by destruct hv; ins; desf; try apply Pfull_is_not_Pzero.
Qed.
Lemma is_lvalue_implies_normal_weak PS PSg (hv : HeapVal PS PSg): is_lvalue hv → HVlabeled hv HLnormal.
Proof.
by ins; eapply is_lvalue_implies_normal.
Qed.
Lemma is_rvalue_implies_normal_weak PS PSg (hv : HeapVal PS PSg): is_rvalue hv → HVlabeled hv HLnormal.
Proof.
by ins; eapply is_rvalue_implies_normal.
Qed.
Lemma reduce_label_to_basic (lbl: HeapLabelCombination):
∃ (lblB : HeapLabel), HLleq lblB lbl.
Proof.
destruct lbl; try solve [∃ HLnormal; vauto | ∃ HLnabla; ins; red; eauto 8 | ∃ HLtriangle; vauto].
Qed.
Lemma labeled_lvalue PS PSg (hv : HeapVal PS PSg) lbl : is_lvalue hv → HVlabeled hv lbl → lbl = HLnormal.
Proof.
by destruct hv; ins; desf;
red in WFperm; desf; apply nonextendable_full_permission in PSUMdef; pplus_eq_zero.
Qed.
Lemma is_rvalue_weaken PS PSg: ∀ (hv : HeapVal PS PSg) v, is_rvalueV hv v → is_rvalue hv.
Proof.
ins; red; desf; ins; desf.
Qed.
Lemma hvplusDEF_with_lvalue PS PSg:
∀ hv1 hv2 (LVAL: is_lvalue hv1) (DEF: hvplusDEF hv1 hv2), hv2 = @HVnone PS PSg.
Proof.
eby ins; red in LVAL, DEF; desf; desf;
try red in DEF; try red in DEF0; desf; rewrite !permission_plusA in PSUMdef;
apply nonextendable_full_permission in PSUMdef;
pplus_eq_zero; exfalso; eapply all_permissions_zero.
Qed.
Hint Resolve is_lvalue_implies_is_nonatomic is_lvalue_implies_normal_weak
is_rvalue_implies_is_nonatomic is_rvalue_implies_normal_weak
is_rvalue_weaken.
Lemmas about lupd.
Lemma lupd_sim PS PSg:
∀ (h : heap PS PSg) lbl, h ≠ Hundef → Hsim h (lupd h lbl).
Proof.
destruct h; ins; repeat eexists; red; ins; desf; ins; desf;
rewrite <- ?eq_rect_eq, ?permission_plus_zero_r, ?permission_plus_zero_l; eauto.
Qed.
Lemma lupd_sim2 PS PSg:
∀ (h h' : heap PS PSg) lbl, Hsim h h' → Hsim (lupd h lbl) h'.
Proof.
ins; red in H; desf; ins; desf; repeat (eexists; try edone); red; ins;
specialize (H1 l); desf; ins; desf; desf; pplus_zero_simpl; eauto.
Qed.
Lemma lupd_label PS PSg:
∀ (h : heap PS PSg) lbl, h ≠ Hundef → HlabeledExact (lupd h lbl) lbl.
Proof.
destruct h; ins; repeat eexists; red; ins; desf.
Qed.
Lemma lupd_eq PS PSg:
∀ (h h' : heap PS PSg) lbl (SIM: Hsim h h') (LBL: HlabeledExact h lbl), h = lupd h' lbl.
Proof.
unfold Hsim, HlabeledExact; ins; desf; ins.
f_equal; extensionality l.
by specialize (LBL0 l); specialize (SIM1 l); desf; red in SIM1; desf; ins; desf; desf;
rewrite ?permission_plus_zero_r, ?permission_plus_zero_l in *; subst; f_equal;
apply proof_irrelevance.
Qed.
Lemma lupd_eq_lupd PS PSg:
∀ (h h': heap PS PSg) lbl (DEF: h ≠ Hundef) (EQ: lupd h lbl = lupd h' lbl), Hsim h h'.
Proof.
ins; red; desf.
destruct h, h'; ins; try done.
injection EQ; clear EQ; intros ? EQ; subst.
repeat eexists; try edone.
red; ins.
by apply equal_f with (x := l) in EQ; desf; ins; desf; rewrite <- !eq_rect_eq.
Qed.
Lemmas about heap labels and hlplus.
Lemma Rlabel_implies_label PS PSg: ∀ (hv : HeapVal PS PSg) lbl, HVlabeledR hv lbl → HVlabeled hv lbl.
Proof.
ins; red in H; desf; ins; desf; vauto.
Qed.
Lemma label_is_consistent_with_exact_label PS PSg:
∀ hv (N: hv ≠ @HVnone PS PSg) lbl lbl' (LAB: HVlabeled hv lbl) (LABx: HVlabeledExact hv lbl'), lbl = lbl'.
Proof.
unfold HVlabeled, HVlabeledExact; ins; desf; desf;
destruct lbl, lbl'; ins; unfold is_normal, is_triangle, is_nabla in*; desf.
Qed.
Lemma label_is_consistent_with_exact_label_spec PS PSg:
∀ hf g l lbl lbl' (N: hf l ≠ @HVnone PS PSg) (L: HVlabeled (hf l) lbl)
(HL: HlabeledExact (Hdef hf g) lbl'),
lbl = lbl'.
Proof.
ins.
eapply label_is_consistent_with_exact_label; eauto.
red in HL; desf.
Qed.
Lemma Rlabel_is_consistent_with_exact_label PS PSg:
∀ (hv : HeapVal PS PSg) lbl lbl' (LAB: HVlabeledR hv lbl) (LABx: HVlabeledExact hv lbl'), lbl = lbl'.
Proof.
ins.
assert (N: hv ≠ HVnone) by (intro N; rewrite N in *; ins).
eby apply Rlabel_implies_label in LAB; eapply label_is_consistent_with_exact_label.
Qed.
Lemma Rlabel_is_consistent_with_exact_label_spec PS PSg:
∀ (hf : val → HeapVal PS PSg) g l lbl lbl'
(L: HVlabeledR (hf l) lbl) (HL: HlabeledExact (Hdef hf g) lbl'),
lbl = lbl'.
Proof.
ins.
eapply Rlabel_is_consistent_with_exact_label; eauto.
red in HL; desf.
Qed.
Lemma nonatomic_label PS PSg:
∀ (hv : HeapVal PS PSg) (NA: is_nonatomic hv) lbl, HVlabeledExact hv lbl → HVlabeled hv lbl.
Proof.
by destruct hv; simpls; ins; desf; desf; red in WFperm; desf;
rewrite ?permission_plus_zero_r, ?permission_plus_zero_l in ×.
Qed.
Lemma basic_is_normal:
∀ (lbl: HeapLabel), is_normal lbl ↔ lbl = HLnormal.
Proof.
ins; destruct lbl; unfold is_normal; split; ins; desf; tauto.
Qed.
Lemma basic_is_triangle:
∀ (lbl: HeapLabel), is_triangle lbl ↔ lbl = HLtriangle.
Proof.
ins; destruct lbl; unfold is_triangle; split; ins; desf; tauto.
Qed.
Lemma basic_is_nabla:
∀ (lbl: HeapLabel), is_nabla lbl ↔ lbl = HLnabla.
Proof.
ins; destruct lbl; unfold is_nabla; split; ins; desf; tauto.
Qed.
Lemma HLleq_trans:
∀ lbl1 lbl2 lbl3, HLleq lbl1 lbl2 ∧ HLleq lbl2 lbl3 → HLleq lbl1 lbl3.
Proof.
unfold HLleq; try unfold is_normal; try unfold is_triangle; try unfold is_nabla;
ins; destruct lbl1, lbl2, lbl3; desf; tauto.
Qed.
Lemma HLleq_refl:
∀ lbl, HLleq lbl lbl.
Proof.
ins; unfold HLleq, is_normal, is_nabla, is_triangle; destruct lbl; tauto.
Qed.
Lemma hlplus_same lbl:
hlplus lbl lbl = lbl.
Proof.
by destruct lbl.
Qed.
Lemma hlplusC lbl1 lbl2:
hlplus lbl1 lbl2 = hlplus lbl2 lbl1.
Proof.
by ins; destruct lbl1, lbl2; simpls.
Qed.
Lemma hlplusA lbl1 lbl2 lbl3:
hlplus (hlplus lbl1 lbl2) lbl3 = hlplus lbl1 (hlplus lbl2 lbl3).
Proof.
by intros; destruct lbl1, lbl2, lbl3; simpls.
Qed.
Lemma hlplus_monotone:
∀ lbl1 lbl2 lbl1' lbl2',
HLleq lbl1 lbl1' ∧ HLleq lbl2 lbl2' → HLleq (hlplus lbl1 lbl2) (hlplus lbl1' lbl2').
Proof.
unfold HLleq; ins; desf;
try unfold is_normal in *;
try unfold is_triangle in *;
try unfold is_nabla in *;
desf; simpl; tauto.
Qed.
Lemma hlplus_monotone_inv: ∀ (lbl: HeapLabel) lbl1 lbl2,
HLleq lbl (hlplus lbl1 lbl2) → HLleq lbl lbl1 ∨ HLleq lbl lbl2.
Proof.
ins; unfold hlplus in H; desf; (try by auto);
unfold HLleq, is_triangle, is_normal, is_nabla in *; desf; desf;
solve [
destruct lbl; done
|
red in H; desf
|
tauto
].
Qed.
Lemma hlplus_monotone1:
∀ lbl lbl', HLleq lbl (hlplus lbl lbl').
Proof.
ins; unfold HLleq, hlplus, is_normal, is_triangle, is_nabla; destruct lbl, lbl'; tauto.
Qed.
Lemma hlplus_monotone2:
∀ lbl lbl1 lbl2, HLleq lbl lbl1 → HLleq lbl (hlplus lbl1 lbl2).
Proof.
destruct lbl, lbl1, lbl2; desf; ins; try red in H; desf; try red; try tauto.
Qed.
Lemma is_normal_monotone:
∀ lbl lbl' (LEQ: HLleq lbl lbl'), is_normal lbl → is_normal lbl'.
Proof.
unfold HLleq; ins; desf; red in H; desf; red; tauto.
Qed.
Lemma normal_hlplus:
∀ lbl1 lbl2, is_normal (hlplus lbl1 lbl2) → is_normal lbl1 ∨ is_normal lbl2.
Proof.
unfold is_normal; destruct lbl1, lbl2; ins; desf; tauto.
Qed.
Lemma not_normal_hlplus:
∀ lbl1 lbl2, ¬ is_normal (hlplus lbl1 lbl2) → ¬ is_normal lbl1 ∧ ¬ is_normal lbl2.
Proof.
unfold is_normal; ins; split; intro; destruct H; desf; try destruct lbl1; try destruct lbl2; tauto.
Qed.
Lemma hlplus_eq_basic:
∀ lbl1 lbl2 (lbl: HeapLabel), hlplus lbl1 lbl2 = lbl → lbl1 = lbl ∧ lbl2 = lbl.
Proof.
by unfold hlplus; ins; destruct lbl; desf; vauto.
Qed.
Lemma oHLleq_trans:
∀ lbl1 lbl2 lbl3, oHLleq lbl1 lbl2 ∧ oHLleq lbl2 lbl3 → oHLleq lbl1 lbl3.
Proof.
unfold oHLleq; ins; desf; eapply HLleq_trans; eauto.
Qed.
Lemma oHLleq_refl:
∀ lbl, oHLleq lbl lbl.
Proof.
ins; red; desf; apply HLleq_refl.
Qed.
Lemma ohlplus_same lbl:
ohlplus lbl lbl = lbl.
Proof.
destruct lbl; simpl; try done.
f_equal; apply hlplus_same.
Qed.
Lemma ohlplusC lbl1 lbl2:
ohlplus lbl1 lbl2 = ohlplus lbl2 lbl1.
Proof.
unfold ohlplus; desf.
by rewrite hlplusC.
Qed.
Lemma ohlplusA lbl1 lbl2 lbl3:
ohlplus (ohlplus lbl1 lbl2) lbl3 = ohlplus lbl1 (ohlplus lbl2 lbl3).
Proof.
unfold ohlplus; desf.
by rewrite hlplusA.
Qed.
Lemma ohlplus_none_l: ∀ lbl, ohlplus None lbl = lbl.
Proof.
ins.
Qed.
Lemma ohlplus_monotone:
∀ lbl1 lbl2 lbl1' lbl2',
oHLleq lbl1 lbl1' ∧ oHLleq lbl2 lbl2' → oHLleq (ohlplus lbl1 lbl2) (ohlplus lbl1' lbl2').
Proof.
unfold oHLleq, ohlplus; ins; desf.
× by apply hlplus_monotone.
× eapply HLleq_trans; split; eauto; apply hlplus_monotone1.
× rewrite hlplusC; eapply HLleq_trans; split; eauto; apply hlplus_monotone1.
Qed.
Lemma ohlplus_monotone1:
∀ lbl lbl', oHLleq lbl (ohlplus lbl lbl').
Proof.
unfold oHLleq, ohlplus; ins; desf.
by apply hlplus_monotone1.
by apply HLleq_refl.
Qed.
Lemma ohlplus_monotone2:
∀ lbl lbl1 lbl2, oHLleq lbl lbl1 → oHLleq lbl (ohlplus lbl1 lbl2).
Proof.
by unfold oHLleq, ohlplus; ins; desf; apply hlplus_monotone2.
Qed.
Lemma is_normalO_monotone:
∀ lbl lbl' (LEQ: oHLleq lbl lbl'), is_normalO lbl → is_normalO lbl'.
Proof.
eby unfold oHLleq, is_normalO; ins; desf; eapply is_normal_monotone.
Qed.
Lemma normalO_ohlplus:
∀ lbl1 lbl2, is_normalO (ohlplus lbl1 lbl2) → is_normalO lbl1 ∨ is_normalO lbl2.
Proof.
by unfold is_normalO, ohlplus; ins; desf; auto; apply normal_hlplus.
Qed.
Lemma ohlplus_oHLleq:
∀ lbl1 lbl2 lbl, ohlplus lbl1 lbl2 = lbl → oHLleq lbl1 lbl ∧ oHLleq lbl2 lbl.
Proof.
unfold ohlplus; split; desf; simpls.
by apply hlplus_monotone1.
by apply HLleq_refl.
by rewrite hlplusC; apply hlplus_monotone1.
by apply oHLleq_refl.
Qed.
Lemma ohlplus_HLleq: ∀ lbl lbl' olbl, ohlplus (Some lbl) olbl = Some lbl' → HLleq lbl lbl'.
Proof.
unfold ohlplus; ins; desf.
by apply hlplus_monotone1.
by apply HLleq_refl.
Qed.
Lemma ohlplus_is_some:
∀ olbl1 olbl2 lbl,
ohlplus olbl1 olbl2 = Some lbl → ∃ lbl', (olbl1 = Some lbl' ∨ olbl2 = Some lbl') ∧ HLleq lbl' lbl.
Proof.
ins; destruct olbl1, olbl2; desf.
× apply ohlplus_HLleq in H; ins; eauto.
× ins; ∃ h; inv H; split; [eauto | eapply HLleq_refl].
× ins; ∃ h; inv H; split; [eauto | eapply HLleq_refl].
Qed.
Lemma ohlplus_with_basic_label:
∀ olbl1 olbl2 lbl' (EQ: ohlplus olbl1 olbl2 = Some lbl')
(lbl: HeapLabel) (L: HLleq lbl lbl'),
∃ lbl'', (olbl1 = Some lbl'' ∨ olbl2 = Some lbl'') ∧ HLleq lbl lbl''.
Proof.
ins; destruct olbl1, olbl2; desf; ins.
× inv EQ; clear EQ.
apply hlplus_monotone_inv in L; desf; eauto.
× inv EQ; clear EQ; eauto.
× inv EQ; clear EQ; eauto.
Qed.
Lemma label_hdef PS PSg:
∀ (hf : val → HeapVal PS PSg) g lbl, HFlabeled hf lbl ↔ Hlabeled (Hdef hf g) lbl.
Proof.
split; ins.
by ∃ hf, g.
by unfold Hlabeled in H; desf.
Qed.
Lemma label_exact_hdef PS PSg:
∀ (hf : val → HeapVal PS PSg) g lbl, HFlabeledExact hf lbl ↔ HlabeledExact (Hdef hf g) lbl.
Proof.
split; ins.
by ∃ hf, g.
by unfold HlabeledExact in H; desf.
Qed.
Lemma label_hvplus PS PSg:
∀ (hv1 hv2 : HeapVal PS PSg) lbl
(DEF: hvplusDEF hv1 hv2)
(PLUS: HVlabeled (hvplus hv1 hv2) lbl),
HVlabeled hv1 lbl ∨ HVlabeled hv2 lbl.
Proof.
ins.
red in DEF; desf; ins; eauto; desf; desf; ins;
solve [
by eq_rect_simpl; apply permission_plus_not_zero
|
inv Heq0; vauto
|
inv Heq; apply hlplus_monotone_inv in PLUS; desf; vauto
].
Qed.
Lemma Rlabel_hvplus PS PSg:
∀ (hv1 hv2 : HeapVal PS PSg) lbl
(DEF: hvplusDEF hv1 hv2)
(PLUS: HVlabeledR (hvplus hv1 hv2) lbl),
HVlabeledR hv1 lbl ∨ HVlabeledR hv2 lbl.
Proof.
ins.
red in DEF; desf; ins; eauto; try des_eqrefl; try done; desf; ins; eq_rect_simpl;
try (by apply permission_plus_not_zero); desf; eauto.
by apply hlplus_monotone_inv.
Qed.
Lemmas about heap similarity.
Lemma HLCsim_refl: ∀ lbl, HLCsim lbl lbl.
Proof.
ins; red; desf.
Qed.
Lemma HLCsim_sym: ∀ lbl lbl', HLCsim lbl lbl' ↔ HLCsim lbl' lbl.
Proof.
unfold HLCsim; ins; desf.
Qed.
Lemma ohlplus_sim: ∀ lbl1 lbl2 lbl1' lbl2'
(SIM1: HLCsim lbl1 lbl1')
(SIM2: HLCsim lbl2 lbl2'),
HLCsim (ohlplus lbl1 lbl2) (ohlplus lbl1' lbl2').
Proof.
unfold HLCsim, ohlplus; ins; desf.
Qed.
Lemma HLCsim_trans lbl1 lbl2 lbl3: HLCsim lbl1 lbl2 → HLCsim lbl2 lbl3 → HLCsim lbl1 lbl3.
Proof.
unfold HLCsim; ins; desf.
Qed.
Lemma HVsim_refl PS PSg: ∀ (hv : HeapVal PS PSg), HVsim hv hv.
Proof.
ins; red; desf; eq_rect_simpl; repeat split; apply HLCsim_refl.
Qed.
Lemma HVsim_sym PS PSg: ∀ (hv hv' : HeapVal PS PSg), HVsim hv hv' ↔ HVsim hv' hv.
Proof.
by unfold HVsim; split; ins; desf; eq_rect_simpl; repeat split; desf; rewrite HLCsim_sym.
Qed.
Lemma HVsim_trans PS PSg (hv1 hv2 hv3 : HeapVal PS PSg): HVsim hv1 hv2 → HVsim hv2 hv3 → HVsim hv1 hv3.
Proof.
unfold HVsim; ins; desf; desf; eq_rect_simpl; eauto 7 using HLCsim_trans; try split; congruence.
Qed.
Lemma HVsim_alloc PS PSg:
∀ (hv1 hv2 : HeapVal PS PSg) (SIM: HVsim hv1 hv2),
hv1 ≠ HVnone ↔ hv2 ≠ HVnone.
Proof.
ins; red in SIM; desf.
Qed.
Lemma is_atomic_sim PS PSg: ∀ (hv hv' : HeapVal PS PSg) (SIM: HVsim hv hv'), is_atomic hv ↔ is_atomic hv'.
Proof.
split; ins; destruct hv, hv'; simpls.
Qed.
Lemma is_nonatomic_sim PS PSg:
∀ (hv hv' : HeapVal PS PSg) (SIM: HVsim hv hv'), is_nonatomic hv ↔ is_nonatomic hv'.
Proof.
split; ins; destruct hv, hv'; simpls.
Qed.
Lemma HFsim_refl PS PSg: ∀ (hf : val → HeapVal PS PSg), HFsim hf hf.
Proof.
ins; red; ins; apply HVsim_refl.
Qed.
Lemma HFsim_sym PS PSg: ∀ (hf hf' : val → HeapVal PS PSg), HFsim hf hf' ↔ HFsim hf' hf.
Proof.
by ins; split; red; ins; specialize (H l); rewrite HVsim_sym.
Qed.
Lemma HFsim_trans PS PSg (hf1 hf2 hf3 : val → HeapVal PS PSg): HFsim hf1 hf2 → HFsim hf2 hf3 → HFsim hf1 hf3.
Proof.
unfold HFsim; ins; eauto using HVsim_trans.
Qed.
Lemma Hsim_alt PS PSg: ∀ (hf hf' : val → HeapVal PS PSg) g, HFsim hf hf' ↔ Hsim (Hdef hf g) (Hdef hf' g).
Proof.
split; ins.
by ∃ hf, hf'; vauto.
by unfold Hsim in *; desf.
Qed.
Lemma Hsim_sym PS PSg: ∀ (h h' : heap PS PSg), Hsim h h' ↔ Hsim h' h.
Proof.
by ins; unfold Hsim; split; ins; desf; eexists _, _, _; repeat split; eauto; rewrite HFsim_sym.
Qed.
Lemma Hsim_refl PS PSg: ∀ h, h ≠ @Hundef PS PSg → Hsim h h.
Proof.
destruct h; ins; rewrite <- Hsim_alt; apply HFsim_refl.
Qed.
Lemma Hsim_trans PS PSg (h1 h2 h3 : heap PS PSg): Hsim h1 h2 → Hsim h2 h3 → Hsim h1 h3.
Proof.
unfold Hsim; ins; desf; repeat eexists; eauto using HFsim_trans.
Qed.
Lemma Hsim_alloc PS PSg:
∀ (h : heap PS PSg) hf g l
(SIM: Hsim h (Hdef hf g))
(DEF: hf l ≠ HVnone),
∃ hf', h = Hdef hf' g ∧ hf' l ≠ HVnone.
Proof.
by unfold Hsim, HFsim, HVsim; ins; desf; specialize (SIM1 l); eexists; split; eauto; intro; desf.
Qed.
Lemma Hsim_alloc_label PS PSg:
∀ (h : heap PS PSg) hf g l lbl
(SIM: Hsim h (Hdef hf g))
(DEF: hf l ≠ HVnone)
(LBL: HVlabeled (hf l) lbl),
∃ hf' lbl', h = Hdef hf' g ∧ hf' l ≠ HVnone∧ HVlabeled (hf' l) lbl'.
Proof.
unfold Hsim, HFsim, HVsim; ins; desf; specialize (SIM1 l); desf;
try by (eexists _, _; repeat split; eauto; rewrite Heq; ins).
× ∃ hf0.
assert (L := get_nonzero_permission WFperm); desf.
by ∃ HLnormal; rewrite Heq; repeat split.
by ∃ HLtriangle; rewrite Heq; repeat split.
by ∃ HLnabla; rewrite Heq; repeat split.
× by ∃ hf0; rewrite Heq; ins; desf; assert (L := reduce_label_to_basic h);
desc; ∃ lblB; repeat split; eauto.
Qed.
Lemma HFsim_alloc_label PS PSg:
∀ hf hf' lbl' l (SIM: HFsim hf hf') (LBL: HVlabeled (hf' l) lbl') (ALL: hf' l ≠ @HVnone PS PSg),
hf l ≠ @HVnone PS PSg ∧ ∃ lbl, HVlabeled (hf l) lbl.
Proof.
ins.
assert (Hsim (Hdef hf gres_emp) (Hdef hf' gres_emp)) by (eexists _, _, _; eauto).
eapply Hsim_alloc_label in H; desf; eauto.
Qed.
Lemma label_sim PS PSg:
∀ (hv1 hv2 : HeapVal PS PSg) (SIM: HVsim hv1 hv2) lbl (LBL: HVlabeled hv1 lbl),
∃ lbl', HVlabeled hv2 lbl'.
Proof.
unfold HVlabeled; ins; desf; ins; desf; try (eby eexists);
try (apply get_nonzero_permission in WFperm; desf;
solve [by ∃ HLnormal | by ∃ HLtriangle | by ∃ HLnabla]);
destruct h; solve [∃ HLnormal; ins; try unfold is_normal; eauto |
∃ HLtriangle; ins; try unfold is_triangle; eauto |
∃ HLnabla; ins; try unfold is_nabla; eauto].
Qed.
Lemma Rlabel_sim PS PSg:
∀ (hv1 hv2 : HeapVal PS PSg) (SIM: HVsim hv1 hv2) lbl (LBL: HVlabeledR hv1 lbl),
∃ lbl', HVlabeledR hv2 lbl'.
Proof.
unfold HVlabeledR; ins; desf; ins; desf;
try (apply get_nonzero_permission in WFperm; desf;
solve [by ∃ HLnormal | by ∃ HLtriangle | by ∃ HLnabla]);
destruct h; solve [∃ HLnormal; ins; try unfold is_normal; eauto |
∃ HLtriangle; ins; try unfold is_triangle; eauto |
∃ HLnabla; ins; try unfold is_nabla; eauto].
Qed.
Lemma Rlabel_hsim PS PSg:
∀ (h : heap PS PSg) hf g l lbl (SIM: Hsim h (Hdef hf g)) (RL: HVlabeledR (hf l) lbl),
∃ hf' lbl', h = Hdef hf' g ∧ HVlabeledR (hf' l) lbl'.
Proof.
ins.
red in SIM; desf.
specialize (SIM1 l).
rewrite HVsim_sym in SIM1.
exploit Rlabel_sim; eauto.
ins; desf; eexists _, _; eauto.
Qed.
Lemma exact_label_sim PS PSg:
∀ (h1 h2 : heap PS PSg) lbl, HlabeledExact h1 lbl → HlabeledExact h2 lbl → Hsim h1 h2 → h1 = h2.
Proof.
unfold HlabeledExact, Hsim; ins; desf.
by f_equal; extensionality l; specialize (H3 l); specialize (H4 l); specialize (H5 l);
red in H3; red in H4; red in H5; desf; desf; eapply HVval_equal; eq_rect_simpl; try done;
pplus_zero_simpl.
Grab Existential Variables. all: done.
Qed.
Some basic lemmas about heaps and hplus.
Lemma hdef_alt PS PSg h : h ≠ @Hundef PS PSg ↔ ∃ hf g, h = Hdef hf g.
Proof. destruct h; split; ins; desf; vauto. Qed.
Lemma AcombinableC PS PSg (P Q : assn PS PSg): Acombinable P Q → Acombinable Q P.
Proof. unfold Acombinable; ins; desf; eauto. Qed.
Lemma assn_mod_eqI1 PS PSg (P Q: assn_mod PS PSg): proj1_sig P = proj1_sig Q → P = Q.
Proof.
destruct P, Q; ins; revert e0; subst; ins; f_equal; apply proof_irrelevance.
Qed.
Lemma assn_mod_eqI PS PSg (P Q: assn_mod PS PSg): Asim (sval P) (sval Q) → P = Q.
Proof.
ins; apply assn_mod_eqI1; apply assn_norm_ok in H.
destruct P, Q; ins; congruence.
Qed.
Lemma AsimD PS PSg (P Q : assn PS PSg) : Asim P Q → mk_assn_mod P = mk_assn_mod Q.
Proof. ins; apply assn_mod_eqI; Asim_simpl. Qed.
Lemma hv_acq_defC PS PSg b1 b2 (Q1 Q2 : assn PS PSg) :
hv_acq_def b1 Q1 b2 Q2 → hv_acq_def b2 Q2 b1 Q1.
Proof. destruct 1; desc; vauto. Qed.
Lemma hvplusDEFC PS PSg (hv1 hv2 : HeapVal PS PSg): hvplusDEF hv1 hv2 → hvplusDEF hv2 hv1.
Proof.
unfold hvplusDEF; desf; ins; desf; eq_rect_simpl; repeat split;
eauto using AcombinableC, eq_sym, hv_acq_defC;
rewrite (permission_plusC _ pNormal0), (permission_plusC _ pTriangle0), (permission_plusC _ pNabla0);
first [red in H | red in H0]; desf.
Qed.
Lemma hvplusC PS PSg (hv1 hv2 : HeapVal PS PSg): hvplusDEF hv1 hv2 → hvplus hv1 hv2 = hvplus hv2 hv1.
Proof.
unfold hvplus, hvplusDEF; ins; desf; desf; try des_eqrefl; try done; f_equal; desf; try des_eqrefl; desf;
try (by exfalso; desf);
try eapply HVval_equal; eq_rect_simpl; try (by exfalso; desf); desf; desf; eq_rect_simpl;
eauto using andbC, orbC, ohlplusC, permission_plusC, eq_sym;
try (by rewrite (permission_plusC _ pNormal0),
(permission_plusC _ pTriangle0),
(permission_plusC _ pNabla0) in *);
try (by extensionality v; desf; apply assn_mod_eqI1; try congruence;
specialize (H0 v); red in H0; desf).
by extensionality v; apply assn_mod_eqI1; specialize (H v); red in H; desf; congruence.
by extensionality v; apply AsimD, Asim_starC.
Grab Existential Variables. all: done.
Qed.
Lemma hplusC PS PSg (h1 h2 : heap PS PSg): hplus h1 h2 = hplus h2 h1.
Proof.
by unfold hplus; desf; f_equal; try exten; ins; desf; eauto using hvplusC, gres_plus_totalC; desf;
destruct n; split; eauto using hvplusDEFC; rewrite gres_plusC.
Qed.
Lemma hplus_emp_l PS PSg h : hplus (@hemp PS PSg) h = h.
Proof.
unfold hplus, hemp; desf.
by rewrite gres_plus_total_emp_l.
destruct n; split; ins.
by rewrite gres_plusC, gres_plus_emp_r.
Qed.
Lemma hplus_emp_r PS PSg h : hplus h (@hemp PS PSg) = h.
Proof. by rewrite hplusC, hplus_emp_l. Qed.
Lemma hplus_eq_emp PS PSg (h1 h2 : heap PS PSg) :
hplus h1 h2 = (@hemp PS PSg) ↔ h1 = hemp ∧ h2 = hemp.
Proof.
split; ins; desf; try apply hplus_emp_r.
destruct h1, h2; ins; desf; desf; inv H.
split; unfold hemp; f_equal;
try (by extensionality l; apply (f_equal (fun f ⇒ f l)) in H1;
destruct (hf l), (hf0 l); ins; desf).
by unfold gres_plus_total in H2; desf; apply gres_eq_empD in Heq.
by unfold gres_plus_total in H2; desf; rewrite gres_plusC in Heq; apply gres_eq_empD in Heq.
Qed.
Lemma assn_norm_mod PS PSg (Q : assn_mod PS PSg) : assn_norm (sval Q) = sval Q.
Proof. destruct Q; ins. Qed.
Lemma hvplusDEF_hvplusA PS PSg (h1 h2 h3 : HeapVal PS PSg) :
hvplusDEF h1 h2 →
hvplusDEF (hvplus h1 h2) h3 →
hvplusDEF h1 (hvplus h2 h3).
Proof.
destruct h1, h2, h3; ins; desf; desf; ins;
try solve [
split; ins; try congruence;
try match goal with |- Acombinable _ _ ⇒
specialize (H2 v); specialize (H1 v); desf;
unfold Acombinable in *; eauto
end; clear H2 H1; specialize (H v); specialize (H0 v);
unfold hv_acq_def in *; simpls; desf;
repeat match goal with
| H : _ = Aemp |- _ ⇒ apply assn_norm_star_eq_emp in H; desc
| H : _ = Afalse |- _ ⇒ apply assn_norm_star_eq_false in H; destruct H as [H|[H|H]]; desc
| H : _ = Aemp |- _ ⇒ rewrite H in *; revert H
| H : Aemp = _ |- _ ⇒ rewrite <- H in *; revert H
end; rewrite ?assn_norm_star_emp, ?assn_norm_star_emp_r, ?assn_norm_mod in *; eauto
|
by right; rewrite H0, H1, H2, assn_norm_star_false
]; desf.
by split; desf; desf; eq_rect_simpl; rewrite !permission_plusA in ×.
destruct n; desf; desf; eq_rect_simpl; split.
by intro CONTRA; red in H2; desf;
rewrite !permission_plusA in *;
rewrite !(permission_plusAC _ pNabla), !(permission_plusAC _ pTriangle), !(permission_plusAC _ pNormal),
CONTRA, !permission_plus_undef_r in PSUMdef.
eby intro; pplus_eq_zero; exfalso; eapply all_permissions_zero.
split; ins.
× clear H2 H1; specialize (H v); specialize (H0 v); unfold hv_acq_def in *; simpls; desf.
by rewrite <- !H, <- !H0, assn_norm_star_emp, assn_norm_emp; eauto.
by rewrite !H, <- !H0, !H1, assn_norm_star_emp_r, assn_norm_false; eauto.
by rewrite <- H, !H0, !H1, assn_norm_star_emp, assn_norm_false; eauto.
by rewrite !H0, !H1, !H2, assn_norm_star_false; eauto.
× specialize (H2 v); specialize (H1 v); desf; unfold Acombinable in *; eauto.
Qed.
Lemma hvplusDEF_hvplus1 PS PSg (h1 h2 h3 : HeapVal PS PSg) :
hvplusDEF h2 h3 →
hvplusDEF h1 (hvplus h2 h3) →
hvplusDEF h1 h2.
Proof.
destruct h1, h2, h3; ins; repeat split; desf; desf; ins; f_equal; ins; try congruence;
try apply Lcombinable_hlplus1 with lbl1;
try match goal with |- Acombinable _ _ ⇒
specialize (H2 v); specialize (H1 v); desf;
unfold Acombinable in *; eauto
end; try specialize (H v); try specialize (H0 v); try specialize (H1 v);
try specialize (H2 v); try specialize (H3 v);
try destruct isrmwflag;
unfold hv_acq_def in *; simpls; desf;
repeat match goal with
| H : ?x = ?x |- _ ⇒ clear H
| H : Aemp = _ |- _ ⇒ symmetry in H
| H : Afalse = _ |- _ ⇒ symmetry in H
| H : _ = Aemp |- _ ⇒ apply assn_norm_star_eq_emp in H; desc
| H : _ = Afalse |- _ ⇒ apply assn_norm_star_eq_false in H; destruct H as [H|[H|H]]; desc
| H : _ = Aemp |- _ ⇒ apply assn_norm_star_eq_emp in H; desc
| H : _ = Aemp |- _ ⇒ rewrite H in *; revert H
end; rewrite ?assn_norm_star_emp, ?assn_norm_star_emp_r, ?assn_norm_mod in *; eauto; intuition try congruence;
try rewrite e; unfold Acombinable; eauto.
split.
by intro CONTRA; red in H1; desf;
rewrite !permission_plusA in *;
rewrite (permission_plusC _ _ pNabla1), !(permission_plusAC _ pNabla1),
!(permission_plusAC _ pTriangle1), !(permission_plusAC _ pNormal1),
CONTRA, !permission_plus_undef_r in PSUMdef.
eby intro; pplus_eq_zero; exfalso; eapply all_permissions_zero.
Qed.
Lemma hvplusDEF_hvplus2 PS PSg (h1 h2 h3 : HeapVal PS PSg) :
hvplusDEF h1 h2 →
hvplusDEF (hvplus h1 h2) h3 →
hvplusDEF h2 h3.
Proof.
ins; rewrite hvplusC in *; eauto using hvplusDEFC, hvplusDEF_hvplus1.
Qed.
Lemma hvplusA PS PSg (h1 h2 h3 : HeapVal PS PSg) :
hvplusDEF h1 h2 →
hvplus (hvplus h1 h2) h3 = hvplus h1 (hvplus h2 h3).
Proof.
destruct h1, h2, h3; ins; desf; desf; ins; desf; rewrite ?ohlplusA;
first [eapply HVval_equal | f_equal]; eq_rect_simpl; rewrite ?permission_plusA in *; try done;
try (eby destruct n; split;
[ intro CONTRA; (try red in p1); (try red in p0); desf; rewrite !permission_plusA in *;
rewrite !(permission_plusAC _ pNabla), !(permission_plusAC _ pTriangle),
!(permission_plusAC _ pNormal), CONTRA, !permission_plus_undef_r in ×
| intro; pplus_eq_zero; exfalso; eapply all_permissions_zero]);
try (eby destruct n0; split;
[ intro CONTRA; (try red in p1); (try red in p0); desf; rewrite !permission_plusA in *;
rewrite !(permission_plusAC _ pNabla), !(permission_plusAC _ pTriangle),
!(permission_plusAC _ pNormal), CONTRA, !permission_plus_undef_r in ×
| intro; pplus_eq_zero; exfalso; eapply all_permissions_zero]);
try (eby exfalso; red in p; red in p0; desf;
rewrite !permission_plusA, permission_plusAC in *;
match goal with H : Pfull _ ## _ ≠ Pundef _ |- _ ⇒ apply nonextendable_full_permission in H end;
pplus_eq_zero; exfalso; eapply all_permissions_zero);
try (by destruct Heq; vauto);
try (by destruct Heq0; vauto);
try (by exten; intro y; desf; apply assn_mod_eqI; ins; Asim_simpl; vauto).
Grab Existential Variables. all: done.
Qed.
Lemma hplusA PS PSg (h1 h2 h3 : heap PS PSg) :
hplus (hplus h1 h2) h3 = hplus h1 (hplus h2 h3).
Proof.
unfold hplus; desf; desf.
× destruct n; split; ins.
by eauto using hvplusDEF_hvplusA, hvplusDEF_hvplus1, hvplusDEF_hvplus2.
eby eapply gres_plus_gres_plus_total_not_none.
× destruct n; split; ins.
by eauto using hvplusDEF_hvplusA, hvplusDEF_hvplus1, hvplusDEF_hvplus2.
eby rewrite gres_plusC, gres_plus_totalC in *; eapply gres_plus_gres_plus_total_not_none.
× f_equal.
by exten; eauto using hvplusA.
by apply gres_plus_totalA.
× destruct n; split; ins.
by eauto using hvplusDEF_hvplusA, hvplusDEF_hvplus1, hvplusDEF_hvplus2.
by rewrite gres_plus_gres_plus_totalA.
× destruct n; unnw; split; ins.
by rewrite hvplusC; eauto; apply hvplusDEFC, hvplusDEF_hvplusA; eauto using hvplusDEFC;
rewrite hvplusC; eauto using hvplusDEFC.
by rewrite <- gres_plus_gres_plus_totalA.
Qed.
Lemma hplusAC PS PSg (h1 h2 h3 : heap PS PSg) :
hplus h2 (hplus h1 h3) = hplus h1 (hplus h2 h3).
Proof.
by rewrite <- (hplusA h2), (hplusC h2), hplusA.
Qed.
Lemma hplus_add_same PS PSg: ∀ (h1 h2 h : heap PS PSg), h1 = h2 → hplus h1 h = hplus h2 h.
Proof.
by ins; subst.
Qed.
Lemma hplus_unfold PS PSg h1 h2 g1 g2 :
hplus (Hdef h1 g1) (Hdef h2 g2) =
(if resources_compatible h1 h2 g1 g2
then Hdef (fun v : val ⇒ hvplus (h1 v) (h2 v)) (gres_plus_total g1 g2)
else @Hundef PS PSg).
Proof.
done.
Qed.
Further properties of hplus
Lemma hplus_not_undef_l PS PSg h h' : hplus h h' ≠ @Hundef PS PSg → h ≠ @Hundef PS PSg.
Proof. by destruct h, h'; ins. Qed.
Lemma hplus_not_undef_r PS PSg h h' : hplus h h' ≠ @Hundef PS PSg → h' ≠ @Hundef PS PSg.
Proof. by destruct h, h'; ins. Qed.
Hint Resolve hplus_not_undef_l.
Hint Resolve hplus_not_undef_r.
Lemma hplus_undef_r PS PSg: ∀ h, hplus h (@Hundef PS PSg) = @Hundef PS PSg.
Proof.
by ins; destruct h; desf.
Qed.
Lemma hplus_undef_l PS PSg: ∀ h, hplus (@Hundef PS PSg) h = @Hundef PS PSg.
Proof.
by ins; rewrite hplusC; apply hplus_undef_r.
Qed.
Lemma hplus_def_inv PS PSg (h h': heap PS PSg) hx gx (P: hplus h h' = Hdef hx gx) :
∃ hy hz gy gz, h = Hdef hy gy ∧ h' = Hdef hz gz
∧ << DEFv: ∀ l, hvplusDEF (hy l) (hz l) >>
∧ << PLUSv: ∀ l, hx l = hvplus (hy l) (hz l) >>
∧ << PLUSg: gres_plus gy gz = Some gx >>.
Proof.
destruct h, h'; ins; desf; desf.
repeat eexists; try done.
unfold gres_plus_total; desf.
Qed.
Lemma hplus_def_inv_l PS PSg (h h' : heap PS PSg) hf g : hplus h h' = Hdef hf g → ∃ h3 g3, h = Hdef h3 g3.
Proof. destruct h, h'; vauto. Qed.
Lemma hplus_def_inv_r PS PSg (h h' : heap PS PSg) hf g : hplus h h' = Hdef hf g → ∃ h3 g3, h' = Hdef h3 g3.
Proof. destruct h, h'; vauto. Qed.
Lemma hplus_eq_gheap:
∀ PS PSg (h1 h2 : heap PS PSg) g (SUM: hplus h1 h2 = gheap _ _ g),
∃ g1 g2, h1 = gheap _ _ g1 ∧ h2 = gheap _ _ g2 ∧ gres_plus g1 g2 = Some g.
Proof.
ins; apply hplus_def_inv in SUM; desf.
eexists _, _; repeat split; eauto; f_equal; extensionality x; specialize (PLUSv x); unfold hvplus in PLUSv; desf.
Qed.
Lemma hplus_preserves_alloc_l PS PSg:
∀ h1 g1 h2 h g l (SUM: Hdef h g = hplus (Hdef h1 g1) h2 ) (ALL: h1 l ≠ @HVnone PS PSg),
h l ≠ @HVnone PS PSg.
Proof.
ins; intro CONTRA; destruct ALL; desf; unfold hvplus in CONTRA; desf.
Qed.
Lemma hplus_preserves_galloc_l PS PSg:
∀ h h1 (h2: heap PS PSg) g1 g l (SUM: Hdef h g = hplus (Hdef h1 g1) h2 ) (ALL: g1 l ≠ None),
g l ≠ None.
Proof.
ins; desf; desf.
unfold gres_plus_total; desf.
unfold gres_plus in *; des_eqrefl; try done; desf.
clear GHOSTcompat; simpl.
inv_lplus l.
unfold olift_plus in EQ; desf; congruence.
Qed.
Lemma hplus_preserves_alloc_r PS PSg:
∀ h1 h2 g2 h g l (SUM: Hdef h g = hplus h1 (Hdef h2 g2)) (ALL: h2 l ≠ @HVnone PS PSg),
h l ≠ @HVnone PS PSg.
Proof.
eby ins; rewrite hplusC in SUM; eapply hplus_preserves_alloc_l.
Qed.
Lemma hplus_preserves_galloc_r PS PSg:
∀ (h1: heap PS PSg) h2 g2 h g l (SUM: Hdef h g = hplus h1 (Hdef h2 g2)) (ALL: g2 l ≠ None), g l ≠ None.
Proof.
eby ins; rewrite hplusC in SUM; eapply hplus_preserves_galloc_l.
Qed.
Lemma hplus_alloc PS PSg h1 h2 h g l :
hplus h1 h2 = Hdef h g →
h l ≠ @HVnone PS PSg →
∃ h' g', h1 = Hdef h' g' ∧ h' l ≠ @HVnone PS PSg ∨ h2 = Hdef h' g' ∧ h' l ≠ @HVnone PS PSg.
Proof.
destruct h1, h2; ins; desf; desf.
generalize (HEAPcompat l); revert H0; case_eq (hf l); case_eq (hf0 l); ins; desf;
eexists _, _; try solve [left; split; ins; congruence|right;split;ins;congruence].
Qed.
Lemma hplus_galloc PS PSg (h1 h2: heap PS PSg) h g l :
hplus h1 h2 = Hdef h g →
g l ≠ None →
∃ h' g', h1 = Hdef h' g' ∧ g' l ≠ None ∨ h2 = Hdef h' g' ∧ g' l ≠ None.
Proof.
destruct h1, h2; ins; desf; desf.
unfold gres_plus_total in *; desf.
unfold gres_plus in *; des_eqrefl; try done.
desf. simpls. clear GHOSTcompat.
inv_lplus l.
unfold olift_plus in *; desf;
by (eexists _, _; try solve [left; split; eauto; congruence | right; split; eauto; congruence]).
Qed.
Lemma hplus_gnalloc_l PS PSg:
∀ hf g hf' g' (h: heap PS PSg)
(SUM: hplus (Hdef hf' g') h = Hdef hf g)
l (N: g l = None),
g' l = None.
Proof.
ins; desf; desf.
unfold gres_plus_total in N; desf.
unfold gres_plus in Heq; des_eqrefl; try edone; desf; ins.
clear GHOSTcompat; inv_lplus l.
rewrite N in EQ; unfold olift_plus in EQ; desf.
Qed.
Lemma hplus_gnalloc_r PS PSg:
∀ hf g hf' g' (h: heap PS PSg)
(SUM: hplus h (Hdef hf' g') = Hdef hf g)
l (N: g l = None),
g' l = None.
Proof.
eby intros; rewrite hplusC in *; eapply hplus_gnalloc_l.
Qed.
Lemma hplus_nalloc PS PSg h1 h2 h g loc :
Hdef h g = hplus h1 h2 →
h loc = @HVnone PS PSg →
∃ h1f g1 h2f g2, Hdef h1f g1 = h1 ∧ h1f loc = @HVnone PS PSg ∧
Hdef h2f g2 = h2 ∧ h2f loc = @HVnone PS PSg.
Proof.
destruct h1, h2; ins; desf.
repeat eexists; try edone; unfold hvplus in *; desf.
Qed.
Lemma hplus_gnalloc PS PSg (h1 h2: heap PS PSg) h g loc :
Hdef h g = hplus h1 h2 →
g loc = None →
∃ h1f g1 h2f g2, Hdef h1f g1 = h1 ∧ g1 loc = None ∧ Hdef h2f g2 = h2 ∧ g2 loc = None.
Proof.
intros.
assert (∃ hf1 g1 hf2 g2, h1 = Hdef hf1 g1 ∧ h2 = Hdef hf2 g2).
by destruct h1, h2; ins; desf; repeat eexists.
desc; subst.
symmetry in H; repeat eexists; try edone.
eby eapply hplus_gnalloc_l.
eby eapply hplus_gnalloc_r.
Qed.
Lemma hplus_nalloc_sim PS PSg h1 h2 h g loc :
Hsim (Hdef h g) (hplus h1 h2) →
h loc = @HVnone PS PSg →
∃ h1f h2f g1 g2, Hdef h1f g1 = h1 ∧ h1f loc = @HVnone PS PSg ∧
Hdef h2f g2 = h2 ∧ h2f loc = @HVnone PS PSg.
Proof.
ins.
red in H; desf.
specialize (H2 loc); rewrite H0 in *; ins; desf.
exploit hplus_nalloc; eauto.
ins; desf.
by repeat eexists.
Qed.
Lemma hplus_nalloc_spec PS PSg: ∀ h g h1 g1 h2 g2 l
(SUM: hplus (Hdef h1 g1) (Hdef h2 g2) = Hdef h g)
(NONEres: h l = @HVnone PS PSg),
h1 l = @HVnone PS PSg ∧ h2 l = @HVnone PS PSg.
Proof.
ins; desf; unfold hvplus in *; desf.
Qed.
Lemma hplus_has_rvalue_l PS PSg:
∀ h g (h1 h2: heap PS PSg) l,
hplus h1 h2 = Hdef h g →
(∀ h'' g'', h1 = Hdef h'' g'' → is_rvalue (h'' l)) →
is_rvalue (h l).
Proof.
destruct h1, h2; ins; desf; desf.
specialize (H0 _ _ eq_refl); specialize (HEAPcompat l).
unfold is_rvalue in *; desf; ins; desf.
by intro CONTRA; apply permission_plus_eq_zero in CONTRA; desf.
by apply Pfull_is_not_Pzero.
Qed.
Lemma hplus_has_rvalue_r PS PSg:
∀ h g (h1 h2: heap PS PSg) l,
hplus h1 h2 = Hdef h g →
(∀ h'' g'', h2 = Hdef h'' g'' → is_rvalue (h'' l)) →
is_rvalue (h l).
Proof.
ins; rewrite hplusC in *; eauto using hplus_has_rvalue_l.
Qed.
Lemma hplus_has_lvalue_l PS PSg:
∀ h g (h1 h2: heap PS PSg) l,
hplus h1 h2 = Hdef h g →
(∀ h'' g'', h1 = Hdef h'' g'' → is_lvalue (h'' l)) →
is_lvalue (h l).
Proof.
destruct h1, h2; ins; desf; desf.
specialize (H0 _ _ eq_refl); specialize (HEAPcompat l).
by unfold is_lvalue in *; desf; ins; desf;
red in WFperm; desf; rewrite !permission_plusA in PSUMdef;
apply nonextendable_full_permission in PSUMdef; pplus_eq_zero; rewrite permission_plus_zero_r.
Qed.
Lemma hplus_has_lvalue_r PS PSg:
∀ h g (h1 h2: heap PS PSg) l,
hplus h1 h2 = Hdef h g →
(∀ h'' g'', h2 = Hdef h'' g'' → is_lvalue (h'' l)) →
is_lvalue (h l).
Proof.
ins; rewrite hplusC in *; eauto using hplus_has_lvalue_l.
Qed.
Lemma hplus_is_rvalue PS PSg:
∀ h g (h1 h2: heap PS PSg) l,
hplus h1 h2 = Hdef h g →
is_rvalue (h l) →
∃ hf1 g1 hf2 g2,
h1 = Hdef hf1 g1 ∧ h2 = Hdef hf2 g2 ∧ (is_rvalue (hf1 l) ∨ is_rvalue (hf2 l)).
Proof.
destruct h1, h2; ins; desf; desf.
by repeat eexists; specialize (HEAPcompat l); unfold hvplusDEF in *; desf; vauto; ins; desf; ins;
eq_rect_simpl; apply permission_plus_not_zero.
Qed.
Lemma hplus_val_lD PS PSg:
∀ hf g (h1 h2: heap PS PSg) l v,
Hdef hf g = hplus h1 h2 →
(∀ hf'' g'', Hdef hf'' g'' = h1 → has_value (hf'' l) v) →
has_value (hf l) v.
Proof.
destruct h1, h2; ins; desf; desf.
specialize (H0 _ _ eq_refl); specialize (HEAPcompat l).
rewrite has_value_alt in H0; desf.
rewrite H0 in *; ins; desf; desf.
Qed.
Lemma hplus_val_rD PS PSg:
∀ hf g (h1 h2: heap PS PSg) l v,
Hdef hf g = hplus h1 h2 →
(∀ hf'' g'', Hdef hf'' g'' = h2 → has_value (hf'' l) v) →
has_value (hf l) v.
Proof.
ins; rewrite hplusC in *; eauto using hplus_val_lD.
Qed.
Lemma hplus_valD PS PSg:
∀ hf g (h1 h2: heap PS PSg) l v,
hplus h1 h2 = Hdef hf g →
has_value (hf l) v →
∃ hf1 g1 hf2 g2, h1 = Hdef hf1 g1 ∧ h2 = Hdef hf2 g2 ∧ (has_value (hf1 l) v ∨ has_value (hf2 l) v).
Proof.
destruct h1, h2; ins; desf; desf.
repeat eexists; specialize (HEAPcompat l); unfold hvplusDEF in *; desf; vauto; ins; desf; ins; desf; eauto.
by destruct n; eq_rect_simpl.
Qed.
Lemma hplus_has_atomic_l PS PSg:
∀ h g (h1 h2: heap PS PSg) l,
hplus h1 h2 = Hdef h g →
(∀ h'' g'', h1 = Hdef h'' g'' → is_atomic (h'' l)) →
is_atomic (h l).
Proof.
destruct h1, h2; ins; desf; desf.
specialize (H0 _ _ eq_refl); specialize (HEAPcompat l).
unfold is_atomic in *; desf; ins; desf.
Qed.
Lemma hplus_has_atomic_r PS PSg :
∀ h g (h1 h2: heap PS PSg) l,
hplus h1 h2 = Hdef h g →
(∀ h'' g'', h2 = Hdef h'' g'' → is_atomic (h'' l)) →
is_atomic (h l).
Proof.
ins; rewrite hplusC in *; eauto using hplus_has_atomic_l.
Qed.
Lemma hplus_is_atomic PS PSg:
∀ h g (h1 h2: heap PS PSg) l,
hplus h1 h2 = Hdef h g →
is_atomic (h l) →
∃ hf1 g1 hf2 g2,
h1 = Hdef hf1 g1 ∧ h2 = Hdef hf2 g2 ∧ (is_atomic (hf1 l) ∨ is_atomic (hf2 l)).
Proof.
destruct h1, h2; ins; desf; desf.
repeat eexists; specialize (HEAPcompat l); unfold hvplusDEF in *; desf; vauto; ins; desf.
Qed.
Lemma hplus_has_nonatomic_l PS PSg:
∀ h g (h1 h2: heap PS PSg) l,
hplus h1 h2 = Hdef h g →
(∀ h'' g'', h1 = Hdef h'' g'' → is_nonatomic (h'' l)) →
is_nonatomic (h l).
Proof.
destruct h1, h2; ins; desf; desf.
specialize (H0 _ _ eq_refl); specialize (HEAPcompat l).
unfold is_nonatomic in *; desf; ins; desf.
Qed.
Lemma hplus_has_nonatomic_r PS PSg:
∀ h g (h1 h2: heap PS PSg) l,
hplus h1 h2 = Hdef h g →
(∀ h'' g'' , h2 = Hdef h'' g'' → is_nonatomic (h'' l)) →
is_nonatomic (h l).
Proof.
ins; rewrite hplusC in *; eauto using hplus_has_nonatomic_l.
Qed.
Lemma hplus_is_nonatomic PS PSg:
∀ h g (h1 h2: heap PS PSg) l,
hplus h1 h2 = Hdef h g →
is_nonatomic (h l) →
∃ hf1 g1 hf2 g2,
h1 = Hdef hf1 g1 ∧ h2 = Hdef hf2 g2 ∧ (is_nonatomic (hf1 l) ∨ is_nonatomic (hf2 l)).
Proof.
destruct h1, h2; ins; desf; desf.
repeat eexists; specialize (HEAPcompat l); unfold hvplusDEF in *; desf; vauto.
Qed.
Lemma hplus_eq_ra_initD PS PSg:
∀ h g (h1 h2: heap PS PSg) l PP QQ perm isrmw init,
hplus h1 h2 = Hdef h g →
h l = HVra PP QQ isrmw perm init →
is_normalO init →
∃ hf g PP' QQ' perm' isrmw' init',
(h1 = Hdef hf g ∨ h2 = Hdef hf g) ∧ hf l = HVra PP' QQ' isrmw' perm' init' ∧ is_normalO init'.
Proof.
destruct h1 as [|hf1]; destruct h2 as [|hf2]; unfold NW; ins; desf; desf.
specialize (HEAPcompat l); red in HEAPcompat; desf; ins; desf.
× ∃ hf2, g1; repeat eexists; eauto.
× ∃ hf1, g0; repeat eexists; eauto.
× red in H1; desf.
unfold ohlplus in Heq1; desf.
+ apply normal_hlplus in H1; desf.
- ∃ hf1, g0; repeat eexists; eauto.
- ∃ hf2, g1; repeat eexists; eauto.
+ ∃ hf1, g0; repeat eexists; eauto.
+ ∃ hf2, g1; repeat eexists; eauto.
Qed.
Lemma hplus_hsingl PS PSg: ∀ l (hv hv': HeapVal PS PSg) (DEFv: hvplusDEF hv hv'),
hplus (hsingl _ _ l hv) (hsingl _ _ l hv') = hsingl _ _ l (hvplus hv hv').
Proof.
ins; desf.
× f_equal.
by extensionality v; unfold hupd; desf.
by apply gres_plus_total_emp_l.
× destruct n; unnw; split; ins.
by unfold hupd; desf.
by rewrite gres_plus_emp_r.
Qed.
Definition hvplus_ra_ret PS PSg (hv: HeapVal PS PSg) QQ' :=
match hv with
| HVnone ⇒ False
| HVuval _ ⇒ False
| HVval _ _ _ _ _ _ ⇒ False
| HVra _ QQ _ _ _ ⇒ QQ = QQ'
end.
Lemma hvplus_ra_ret_initialize PS PSg: ∀ (h: val → HeapVal PS PSg) l l' QQ,
hvplus_ra_ret (h l) QQ ↔ hvplus_ra_ret (initialize h l' l) QQ.
Proof.
ins; unfold initialize, hupd; destruct (classic (l' = l)).
by desf; destruct (h l).
by desf.
Qed.
Definition hvplus_ra2_ret PS PSg hv (QQ' : val → assn_mod PS PSg) :=
match hv with
| HVra PP QQ isrmw perm init ⇒
∀ v, ∃ QR, Asim (sval (QQ v)) (Astar (sval (QQ' v)) QR)
| _ ⇒ False
end.
Lemma hvplus_ra2 PS PSg hv hv' PP' QQ' perm' isrmw' init':
hv = @HVra PS PSg PP' QQ' isrmw' perm' init' →
hvplusDEF hv hv' →
hvplus_ra2_ret (hvplus hv hv') QQ'.
Proof.
ins; subst; desf; ins; desf; ins; desf; ins; eauto using Asim.
by destruct (H0 v); ins; desc; rewrite H, ?H2 in *; eauto using Asim.
by eexists; apply Asim_sym, Asim_assn_norm.
Qed.
Lemma hplus_preserves_label PS PSg:
∀ hf g hf1 g1 h2 l lbl
(SUM: Hdef hf g = hplus (Hdef hf1 g1) h2)
(LABEL: HVlabeled (hf1 l) lbl)
(DEF: hf1 l ≠ @HVnone PS PSg),
hf l ≠ @HVnone PS PSg ∧ HVlabeled (hf l) lbl.
Proof.
ins; desf; desf; split; specialize (HEAPcompat l); red in HEAPcompat; desf; eq_rect_simpl;
try (by ins; desf; ins; intro; pplus_eq_zero);
ins; desf; ins; eq_rect_simpl; desf; eauto using hlplus_monotone2;
by intro; pplus_eq_zero.
Qed.
Lemma hplus_preserves_Rlabel PS PSg: ∀ hf g hf1 g1 (h2: heap PS PSg) l lbl
(SUM: Hdef hf g = hplus (Hdef hf1 g1) h2)
(LABEL: HVlabeledR (hf1 l) lbl),
HVlabeledR (hf l) lbl.
Proof.
ins; desf; desf; specialize (HEAPcompat l); red in HEAPcompat; desf;
eq_rect_simpl; desf; ins; desf; ins; eq_rect_simpl; try by intro; pplus_eq_zero.
by desf; eapply HLleq_trans; split; eauto using hlplus_monotone1.
by desf.
Qed.
Lemma hplus_preserves_label_inv PS PSg:
∀ hf g h1 h2 l lbl
(SUM: hplus h1 h2 = Hdef hf g)
(LABEL: HVlabeled (hf l) lbl)
(ALL: hf l ≠ @HVnone PS PSg),
∃ hf' g', (h1 = Hdef hf' g' ∨ h2 = Hdef hf' g') ∧ HVlabeled (hf' l) lbl ∧ hf' l ≠ @HVnone PS PSg.
Proof.
ins; apply hplus_def_inv in SUM; desf; rewrite PLUSv in ×.
specialize (DEFv l).
case_eq (hy l) as Y; case_eq (hz l) as Z; ins; desf; try (
try (by ∃ hz; rewrite Z; ins; eauto);
try (by ∃ hy; rewrite Y; ins; eauto);
desf; first [ exploit ohlplus_with_basic_label; eauto; ins; [] |
clear Heq; exploit ohlplus_with_basic_label; eauto; ins; [] |
clear Heq0; exploit ohlplus_with_basic_label; eauto; ins; []];
desf; solve [ ∃ hy, gy; rewrite Y; ins; repeat split; try by eauto; instantiate; desf; eauto |
∃ hz, gz; rewrite Z; ins; repeat split; try by eauto; instantiate; desf; eauto]);
ins; desf; ins; apply permission_plus_not_zero in LABEL; desf;
try (by ∃ hy, gy; rewrite Y; ins; repeat split; eauto);
try (by ∃ hz, gz; rewrite Z; ins; repeat split; eauto).
Qed.
Lemma hplus_preserves_Rlabel_inv PS PSg:
∀ hf g (h1 h2: heap PS PSg) l lbl
(SUM: hplus h1 h2 = Hdef hf g)
(LABEL: HVlabeledR (hf l) lbl),
∃ hf' g', (h1 = Hdef hf' g' ∨ h2 = Hdef hf' g') ∧ HVlabeledR (hf' l) lbl.
Proof.
ins; apply hplus_def_inv in SUM; desf; rewrite PLUSv in LABEL.
by apply Rlabel_hvplus in LABEL; desf; [∃ hy, gy | ∃ hz, gz]; auto.
Qed.
Lemma hplus_alloc_label PS PSg:
∀ h1 h2 h g l lbl
(SUM: hplus h1 h2 = Hdef h g)
(DEF: h l ≠ @HVnone PS PSg)
(LABEL: HVlabeled (h l) lbl),
∃ h' g', h1 = Hdef h' g' ∧ h' l ≠ @HVnone PS PSg ∧ HVlabeled (h' l) lbl ∨
h2 = Hdef h' g' ∧ h' l ≠ @HVnone PS PSg ∧ HVlabeled (h' l) lbl.
Proof.
ins.
apply hplus_def_inv in SUM; desf.
specialize (DEFv l); specialize (PLUSv l).
rewrite PLUSv in ×.
case_eq (hy l) as Y; case_eq (hz l) as Z; ins; desf; desf;
solve [
∃ hz, gz; right; rewrite Z; ins; eauto
|
∃ hy, gy; left; rewrite Y; ins; eauto
|
ins; desf; ins; apply permission_plus_not_zero in LABEL; desf;
try (by ∃ hy, gy; left; rewrite Y; ins; repeat split; eauto);
try (by ∃ hz, gz; right; rewrite Z; ins; repeat split; eauto)
|
eapply ohlplus_with_basic_label in Heq; eauto; desf; [
∃ hy, gy; left; rewrite Y; ins; desf; repeat (split; eauto; try done)
|
∃ hz, gz; right; rewrite Z; ins; desf; repeat (split; eauto; try done)
]
|
eapply ohlplus_with_basic_label in Heq0; eauto; desf; [
∃ hy, gy; left; rewrite Y; ins; desf; repeat (split; eauto; try done)
|
∃ hz, gz; right; rewrite Z; ins; desf; repeat (split; eauto; try done)
]
].
Qed.
Lemma hplus_sim_def_strong PS PSg:
∀ (h h1 h2: heap PS PSg) hf g
(SIM: Hsim h1 h2)
(DEF: hplus h1 h = Hdef hf g),
∃ hf', hplus h2 h = Hdef hf' g ∧ HFsim hf hf'.
Proof.
ins; unfold Hsim in SIM; desf.
destruct h; ins; desf; desf.
× eexists; split; try done.
red; ins.
specialize (SIM1 l); specialize (HEAPcompat l); specialize (HEAPcompat0 l).
unfold HVsim, hvplus; desf; ins; desf; try congruence;
try (by repeat split; try done; unfold HLCsim, ohlplus; desf);
try (by rewrite Heq in Heq0; desf; repeat split; try done; apply HLCsim_refl);
eq_rect_simpl; split; desf.
rewrite <- !permission_plusA in SIM0.
by rewrite !permission_plusA,
!(permission_plusAC _ pNabla1), !(permission_plusAC _ pTriangle1), !(permission_plusAC _ pNormal1),
!(permission_plusAC _ pNabla0), !(permission_plusAC _ pTriangle0), !(permission_plusAC _ pNormal0),
<- !permission_plusA, SIM0.
× destruct n; unnw; split; ins; specialize (HEAPcompat v); specialize (SIM1 v);
unfold HVsim, hvplusDEF in *; desf; desf; eq_rect_simpl; repeat split; try done;
by red in HEAPcompat0; desf; rewrite !permission_plusA in *;
rewrite !(permission_plusAC _ pNabla), !(permission_plusAC _ pTriangle),
!(permission_plusAC _ pNormal), <- !permission_plusA;
try (rewrite <- !permission_plusA in SIM1; rewrite <- SIM1);
try (rewrite <- !permission_plusA in SIM0; rewrite <- SIM0);
rewrite !(permission_plusAC _ pNabla1), !(permission_plusAC _ pTriangle1),
!(permission_plusAC _ pNormal1), <- !permission_plusA in ×.
Qed.
Lemma hplus_sim_def PS PSg:
∀ h h1 h2 (SIM: Hsim h1 h2) (DEF: hplus h1 h ≠ @Hundef PS PSg), hplus h2 h ≠ @Hundef PS PSg.
Proof.
ins; rewrite hdef_alt in *; ins; desf.
exploit hplus_sim_def_strong; eauto; ins; desf.
eby eexists _, _.
Qed.
Lemma hplus_sim PS PSg:
∀ h1 h2 h1' h2'
(SIM1: Hsim h1 h1')
(SIM2: Hsim h2 h2')
(DEF: hplus h1 h2 ≠ @Hundef PS PSg),
Hsim (hplus h1 h2) (hplus h1' h2').
Proof.
unfold Hsim; ins; desf.
rewrite hdef_alt in DEF; desf.
assert (DEF': hplus (Hdef hf'0 g0) (Hdef hf' g) ≠ Hundef).
{
intro UNDEF.
rewrite hplus_unfold in *; desf; desf.
destruct n; unnw; split; ins.
specialize (HEAPcompat v); specialize (SIM3 v); specialize (SIM5 v).
unfold hvplusDEF, HVsim in *; desf; desf; eq_rect_simpl; repeat split; try done.
try red in HEAPcompat0; try red in h0; desf; rewrite !permission_plusA in ×.
2: eby intro; pplus_eq_zero; eapply all_permissions_zero.
clear - SIM1 SIM0 PSUMdef.
rewrite <- !permission_plusA in SIM1.
rewrite !(permission_plusAC _ pNabla), !(permission_plusAC _ pTriangle), !(permission_plusAC _ pNormal),
<- SIM0, <- !permission_plusA, <- SIM1, !permission_plusA.
by rewrite !(permission_plusAC _ pNabla1), !(permission_plusAC _ pTriangle1),
!(permission_plusAC _ pNormal1) in PSUMdef.
}
rewrite hdef_alt in DEF'; desf.
eexists _, _, _; repeat split; eauto.
by ins; desf.
red; ins.
specialize (SIM3 l); specialize (SIM5 l).
desf; desf.
specialize (HEAPcompat l); specialize (HEAPcompat0 l).
unfold HVsim, hvplusDEF, hvplus in *; desf; desf; eq_rect_simpl; repeat split;
try (by apply ohlplus_sim); try done.
rewrite !permission_plusA, !(permission_plusAC _ pNabla1), !(permission_plusAC _ pTriangle1),
!(permission_plusAC _ pNormal1), !(permission_plusAC _ pNabla0), !(permission_plusAC _ pTriangle0),
!(permission_plusAC _ pNormal0), SIM0.
rewrite <- !(permission_plusC _ pNabla2), !(permission_plusAC _ pNabla2); f_equal.
rewrite <- !(permission_plusC _ pTriangle2), !(permission_plusAC _ pTriangle2); f_equal.
rewrite <- !(permission_plusC _ pNormal2), !(permission_plusAC _ pNormal2); f_equal.
done.
Qed.
Lemma exact_label_hplus_dist PS PSg:
∀ (h1 h2: heap PS PSg) lbl, HlabeledExact (hplus h1 h2) lbl → HlabeledExact h1 lbl ∧ HlabeledExact h2 lbl.
Proof.
ins.
red in H; desf.
apply hplus_def_inv in H; desf.
rewrite <- !label_exact_hdef.
unfold HFlabeledExact.
rewrite <- forall_and_dist; intro l; specialize (DEFv l); specialize (PLUSv l); specialize (H0 l).
rewrite PLUSv in H0; clear PLUSv; unfold hvplus in H0; desf; ins; desf; desf; eq_rect_simpl; ins; desf;
try apply hlplus_eq_basic in H0; try apply hlplus_eq_basic in H1; desf; pplus_eq_zero; eauto.
Qed.
Lemma exact_label_hplus_dist_inv PS PSg:
∀ h1 h2 lbl
(DEF: hplus h1 h2 ≠ @Hundef PS PSg)
(L1: HlabeledExact h1 lbl)
(L2: HlabeledExact h2 lbl),
HlabeledExact (hplus h1 h2) lbl.
Proof.
ins.
rewrite hdef_alt in DEF; desf.
apply hplus_def_inv in DEF; desf.
rewrite hplus_unfold; desf.
clear a PLUSv.
rewrite <- label_exact_hdef in ×.
red; ins.
specialize (DEFv l); specialize (L1 l); specialize (L2 l).
unfold hvplus; desf; ins; desf; eq_rect_simpl; ins; desf; eauto using hlplus_same, permission_plus_zero_l.
destruct n; split; try done.
congruence.
Qed.
Lemma lupd_hplus_dist PS PSg:
∀ (h1 h2: heap PS PSg) lbl, lupd (hplus h1 h2) lbl = hplus (lupd h1 lbl) (lupd h2 lbl).
Proof.
ins; unfold lupd; desf; rewrite hplus_unfold in *; desf; desf;
try (by destruct n; split; try done; unnw; ins; specialize (HEAPcompat v); desf; ins; repeat split;
desf; desf; split; try done; eq_rect_simpl;
red in HEAPcompat0; desf; rewrite !permission_plusA in *; pplus_zero_simpl;
try (by split; rewrite !permission_plusA, !(permission_plusAC _ pNabla),
!(permission_plusAC _ pTriangle), !(permission_plusAC _ pNormal));
try (by split; pplus_zero_simpl; rewrite !(permission_plusAC _ pNabla), !(permission_plusAC _ pTriangle),
!(permission_plusAC _ pNormal) in *));
f_equal; extensionality v; specialize (HEAPcompat v); specialize (HEAPcompat0 v); desf; ins; desf;
eapply HVval_equal; eq_rect_simpl; desf; desf; pplus_zero_simpl; try done;
by rewrite !permission_plusA, !(permission_plusAC _ pNabla0), !(permission_plusAC _ pTriangle0),
!(permission_plusAC _ pNormal0).
Grab Existential Variables. all: done.
Qed.
Lemma hplus_gheap PS PSg:
∀ (hf hf': val → HeapVal PS PSg) g g' g'',
Hdef hf g = hplus (Hdef hf' g') (gheap _ _ g'') → hf = hf'.
Proof.
ins; desf; desf.
by exten; ins; rewrite hvplusC.
Qed.
Lemmas about hsum
Lemma hsum_nil PS PSg : hsum nil = @hemp PS PSg.
Proof. done. Qed.
Lemma hsum_cons PS PSg (a: heap PS PSg) l : hsum (a :: l) = hplus a (hsum l).
Proof. done. Qed.
Lemma hsum_one PS PSg (h: heap PS PSg) : hsum (h :: nil) = h.
Proof. apply hplus_emp_r. Qed.
Lemma hsum_two PS PSg (h h': heap PS PSg) : hsum (h :: h' :: nil) = hplus h h'.
Proof. by unfold hsum; ins; rewrite hplus_emp_r. Qed.
Lemma hsum_perm PS PSg (l l': list (heap PS PSg)) : Permutation l l' → hsum l = hsum l'.
Proof. unfold hsum; induction 1; ins; try congruence; apply hplusAC. Qed.
Lemma hsum_app PS PSg (l l': list (heap PS PSg)) : hsum (l ++ l') = hplus (hsum l) (hsum l').
Proof.
unfold hsum; induction l; intros; try done; [by rewrite hplus_emp_l|].
by simpl; rewrite hplusA, IHl.
Qed.
Lemma hsum_undef PS PSg: ∀ hlist, In (@Hundef PS PSg) hlist → hsum hlist = @Hundef PS PSg.
Proof.
ins.
apply In_split in H; desf.
rewrite hsum_app, hsum_cons; eauto using hplus_undef_l, hplus_undef_r.
Qed.
Lemma hsum_eq_emp PS PSg: ∀ hlist, hsum hlist = @hemp PS PSg ↔ ∀ h (IN: In h hlist), h = hemp.
Proof.
induction hlist as [ | head tail]; ins; rewrite hsum_cons; split; ins.
by rewrite hplus_eq_emp in *; desf; apply IHtail.
rewrite hplus_eq_emp; split.
by apply H; vauto.
by rewrite IHtail; ins; apply H; vauto.
Qed.
Lemma hsum_def_inv PS PSg:
∀ hlist (hf: val → HeapVal PS PSg) g (SUM: hsum hlist = Hdef hf g),
∀ h (IN: In h hlist), ∃ hf' g', h = Hdef hf' g'.
Proof.
intros until hlist.
induction hlist as [ | h htail]; ins; desf.
by rewrite hsum_cons in SUM; apply hplus_def_inv_l in SUM.
rewrite hsum_cons in SUM; apply hplus_def_inv_r in SUM; desf.
by eapply IHhtail; eauto.
Qed.
Lemma hsum_alloc PS PSg l h g loc :
hsum l = Hdef h g →
h loc ≠ @HVnone PS PSg →
∃ h' g', In (Hdef h' g') l ∧ h' loc ≠ @HVnone PS PSg.
Proof.
unfold hsum.
induction[h g] l; ins; [by inv H|].
eapply hplus_alloc in H; eauto; desf; eauto.
exploit IHl; eauto; intro; desf; eauto.
Qed.
Lemma hsum_galloc PS PSg l (h: val → HeapVal PS PSg) g loc :
hsum l = Hdef h g →
g loc ≠ None →
∃ h' g', In (Hdef h' g') l ∧ g' loc ≠ None.
Proof.
unfold hsum.
induction[h g] l; ins; [by inv H|].
eapply hplus_galloc in H; eauto; desf; eauto.
exploit IHl; eauto; intro; desf; eauto.
Qed.
Lemma hsum_alloc_sim PS PSg l h g loc :
Hsim (hsum l) (Hdef h g) →
h loc ≠ @HVnone PS PSg →
∃ h' g', In (Hdef h' g') l ∧ h' loc ≠ @HVnone PS PSg.
Proof.
ins.
red in H; desf.
specialize (H2 loc).
exploit hsum_alloc; eauto.
intro N; rewrite N in *; ins; desf.
Qed.
Lemma hsum_nalloc PS PSg hs hf g h loc :
Hdef hf g = hsum hs →
hf loc = @HVnone PS PSg→
In h hs →
∃ hf g, Hdef hf g = h ∧ hf loc = @HVnone PS PSg.
Proof.
unfold hsum; induction[hf g] hs; ins; desf;
eapply hplus_nalloc in H; eauto; desf; eauto.
Qed.
Lemma hsum_nalloc_all PS PSg:
∀ hlist hf g l
(SUM: hsum hlist = Hdef hf g)
(NALLOC: hf l = @HVnone PS PSg),
∀ h (IN: In h hlist), ∃ hf' g', h = Hdef hf' g' ∧ hf' l = @HVnone PS PSg.
Proof.
ins.
assert (DEF := ((hsum_def_inv _ SUM) _ IN)); desf.
∃ hf', g'; intuition.
apply In_implies_perm in IN as [hlist' IN]; desf.
rewrite (hsum_perm IN), hsum_cons in SUM.
apply hplus_def_inv in SUM; desf.
specialize (PLUSv l); rewrite NALLOC in PLUSv.
unfold hvplus in PLUSv; desf.
Qed.
Lemma hsum_preserves_alloc PS PSg:
∀ hs hf g (SUM: hsum hs = Hdef hf g) hf' g' (IN: In (Hdef hf' g') hs) l (ALL: hf' l ≠ @HVnone PS PSg),
hf l ≠ @HVnone PS PSg.
Proof.
ins; intro.
exploit hsum_nalloc_all; eauto; ins; desf.
Qed.
Lemma hsum_preserves_galloc PS PSg:
∀ hs (hf: val → HeapVal PS PSg)
g (SUM: hsum hs = Hdef hf g)
hf' g' (IN: In (Hdef hf' g') hs)
l (ALL: g' l ≠ None),
g l ≠ None.
Proof.
induction hs; ins.
rewrite hsum_cons in SUM; desf.
eby symmetry in SUM; eapply hplus_preserves_galloc_l.
assert (D := hplus_def_inv_r _ _ SUM); desf; rewrite D in SUM.
specialize (IHhs _ _ D _ _ IN _ ALL).
eby symmetry in SUM; eapply hplus_preserves_galloc_r.
Qed.
Lemma hsum_none PS PSg:
∀ hlist hf g (SUM: hsum hlist = Hdef hf g)
l (NONE: ∀ hf' g' (IN: In (Hdef hf' g') hlist), hf' l = @HVnone PS PSg),
hf l = @HVnone PS PSg.
Proof.
intros until hlist.
induction hlist; ins.
by rewrite hsum_nil in SUM; inv SUM.
rewrite hsum_cons in SUM.
apply NNPP; intro ALLOC.
by eapply hplus_alloc in SUM; desf; eauto.
Qed.
Lemma hsum_has_rvalue PS PSg:
∀ (h: val → HeapVal PS PSg) g hs h'' g'' l,
hsum hs = Hdef h g →
In (Hdef h'' g'') hs →
is_rvalue (h'' l) →
is_rvalue (h l).
Proof.
intros until 0; induction[h g] hs; ins; rewrite hsum_cons in ×.
desf; eauto using hplus_has_rvalue_r.
eapply hplus_has_rvalue_l; eauto; ins; desf.
Qed.
Lemma hsum_has_lvalue PS PSg:
∀ (h: val → HeapVal PS PSg) g hs h'' g'' l,
hsum hs = Hdef h g →
In (Hdef h'' g'') hs →
is_lvalue (h'' l) →
is_lvalue (h l).
Proof.
intros until 0; induction[h g] hs; ins; rewrite hsum_cons in ×.
desf; eauto using hplus_has_lvalue_r.
eapply hplus_has_lvalue_l; eauto; ins; desf.
Qed.
Lemma hsum_is_rvalue PS PSg:
∀ hs (h : val → HeapVal PS PSg) g l,
hsum hs = Hdef h g →
is_rvalue (h l) →
∃ hf g', In (Hdef hf g') hs ∧ is_rvalue (hf l).
Proof.
induction hs; rewrite ?hsum_nil, ?hsum_cons in *; ins; desf.
by inv H.
eapply hplus_is_rvalue in H; eauto; desf; eauto.
exploit IHhs; eauto; ins; desf; eauto.
Qed.
Lemma hsum_is_atomic PS PSg:
∀ hs (h : val → HeapVal PS PSg) g l,
hsum hs = Hdef h g →
is_atomic (h l) →
∃ hf g', In (Hdef hf g') hs ∧ is_atomic (hf l).
Proof.
induction hs; rewrite ?hsum_nil, ?hsum_cons in *; ins; desf.
by inv H.
eapply hplus_is_atomic in H; eauto; desf; eauto.
exploit IHhs; eauto; ins; desf; eauto.
Qed.
Lemma hsum_has_atomic PS PSg:
∀ hs (hf : val → HeapVal PS PSg) g l (SUM: hsum hs = Hdef hf g)
hf' g' (IN: In (Hdef hf' g') hs) (NAT: is_atomic (hf' l)),
is_atomic (hf l).
Proof.
induction hs as [ | h hs']; ins.
rewrite hsum_cons in SUM; desf.
× eapply hplus_has_atomic_l; eauto; ins. inv H.
× eapply hplus_has_atomic_r; eauto.
Qed.
Lemma hsum_is_nonatomic PS PSg:
∀ hs (h : val → HeapVal PS PSg) g l,
hsum hs = Hdef h g →
is_nonatomic (h l) →
∃ hf g', In (Hdef hf g') hs ∧ is_nonatomic (hf l).
Proof.
induction hs; rewrite ?hsum_nil, ?hsum_cons in *; ins; desf.
by inv H.
eapply hplus_is_nonatomic in H; eauto; desf; eauto.
exploit IHhs; eauto; ins; desf; eauto.
Qed.
Lemma hsum_has_nonatomic PS PSg:
∀ hs (hf : val → HeapVal PS PSg) g l (SUM: hsum hs = Hdef hf g)
hf' g' (IN: In (Hdef hf' g') hs) (NAT: is_nonatomic (hf' l)),
is_nonatomic (hf l).
Proof.
induction hs as [ | h hs']; ins.
rewrite hsum_cons in SUM; desf.
× eapply hplus_has_nonatomic_l; eauto; ins. inv H.
× eapply hplus_has_nonatomic_r; eauto.
Qed.
Lemma exact_label_hsum_dist PS PSg:
∀ hlist lbl (LBL: HlabeledExact (hsum hlist) lbl) (h: heap PS PSg) (IN: In h hlist),
HlabeledExact h lbl.
Proof.
induction hlist; ins.
rewrite hsum_cons in LBL; apply exact_label_hplus_dist in LBL; desf.
by apply IHhlist.
Qed.
Lemma hsum_valD PS PSg:
∀ (hf : val → HeapVal PS PSg) g hs h'' g'' l v,
hsum hs = Hdef hf g →
In (Hdef h'' g'') hs →
has_value (h'' l) v →
has_value (hf l) v.
Proof.
intros until 0; induction[hf g] hs; ins; rewrite hsum_cons in ×.
desf; eauto using hplus_val_rD.
eapply hplus_val_lD; eauto; ins; desf.
Qed.
Lemma hsum_eq_val PS PSg:
∀ hs (hf : val → HeapVal PS PSg) g l v,
hsum hs = Hdef hf g →
has_value (hf l) v →
∃ hf g', In (Hdef hf g') hs ∧ has_value (hf l) v.
Proof.
induction hs; rewrite ?hsum_nil, ?hsum_cons in *; ins; desf.
by inv H.
eapply hplus_valD in H; eauto; desf; eauto.
exploit IHhs; eauto; ins; desf; eauto.
Qed.
Lemma hsum_eq_ra_initD PS PSg:
∀ h' g' hs l PP QQ isrmw perm init,
hsum hs = Hdef h' g' →
h' l = @HVra PS PSg PP QQ isrmw perm init →
is_normalO init →
∃ h'' g'' PP' QQ' isrmw' perm' init',
In (Hdef h'' g'') hs ∧
h'' l = HVra PP' QQ' isrmw' perm' init' ∧ is_normalO init'.
Proof.
intros until 0; induction[h' g' PP QQ isrmw perm init] hs; ins; [by inv H|].
rewrite hsum_cons in ×.
eapply hplus_eq_ra_initD in H; eauto.
desf; eauto 12.
exploit IHhs; eauto; intro; desf.
repeat eexists; eauto.
Qed.
Lemma hsum_preserves_label PS PSg:
∀ hs hf g hf' g' l lbl
(SUM: Hdef hf g = hsum hs)
(IN: In (Hdef hf' g') hs)
(LABEL: HVlabeled (hf' l) lbl)
(DEF: hf' l ≠ @HVnone PS PSg),
hf l ≠ @HVnone PS PSg ∧ HVlabeled (hf l) lbl.
Proof.
by ins;
apply In_implies_perm in IN; desf;
apply hsum_perm in IN; rewrite IN in SUM;
rewrite hsum_cons in SUM;
eapply hplus_preserves_label in SUM; eauto; desf;
split; desf; eexists.
Qed.
Lemma hsum_preserves_Rlabel PS PSg:
∀ hs (hf : val → HeapVal PS PSg) g hf' g' l lbl
(SUM: Hdef hf g = hsum hs)
(IN: In (Hdef hf' g') hs)
(LABEL: HVlabeledR (hf' l) lbl),
HVlabeledR (hf l) lbl.
Proof.
by ins;
apply In_implies_perm in IN; desf;
apply hsum_perm in IN; rewrite IN in SUM;
rewrite hsum_cons in SUM;
eapply hplus_preserves_Rlabel in SUM; eauto; desf;
split; desf; eexists.
Qed.
Lemma hsum_preserves_label_inv PS PSg:
∀ hs hf g l lbl
(SUM: Hdef hf g = hsum hs)
(LABEL: HVlabeled (hf l) lbl)
(ALL: hf l ≠ @HVnone PS PSg),
∃ hf' g', In (Hdef hf' g') hs ∧ HVlabeled (hf' l) lbl ∧ hf' l ≠ @HVnone PS PSg.
Proof.
induction hs; ins.
by rewrite hsum_nil in SUM; inv SUM.
rewrite hsum_cons in SUM.
symmetry in SUM. assert (SUMcopy := SUM).
eapply hplus_preserves_label_inv in SUM; eauto; desf.
by ∃ hf', g'; vauto.
symmetry in SUM; specialize (IHhs _ _ _ _ SUM SUM0); desf.
exploit IHhs; eauto; ins; desf.
by ∃ hf'0, g'0; vauto.
Qed.
Lemma hsum_preserves_Rlabel_inv PS PSg:
∀ hs (hf : val → HeapVal PS PSg) g l lbl
(SUM: Hdef hf g = hsum hs)
(LABEL: HVlabeledR (hf l) lbl),
∃ hf' g', In (Hdef hf' g') hs ∧ HVlabeledR (hf' l) lbl.
Proof.
induction hs.
× rewrite hsum_nil; ins.
inv SUM.
× ins.
rewrite hsum_cons in SUM.
symmetry in SUM. assert (SUMcopy := SUM).
eapply hplus_preserves_Rlabel_inv in SUM; eauto; desf.
by ∃ hf', g'; vauto.
symmetry in SUM; specialize (IHhs _ _ _ _ SUM SUM0); desf.
by ∃ hf'0, g'0; vauto.
Qed.
Lemma hsum_alloc_label PS PSg:
∀ hs h g l lbl
(SUM: hsum hs = Hdef h g)
(DEF: h l ≠ @HVnone PS PSg)
(LABEL: HVlabeled (h l) lbl),
∃ h' g', In (Hdef h' g') hs ∧ h' l ≠ @HVnone PS PSg ∧ HVlabeled (h' l) lbl.
Proof.
induction hs; ins.
by exfalso; destruct DEF; rewrite hsum_nil in SUM; injection SUM; ins; desf.
by rewrite hsum_cons in SUM; eapply hplus_alloc_label in SUM; eauto; desf;
[ | specialize (IHhs _ _ _ _ SUM SUM0 SUM1); desf];
eexists; eauto.
Qed.
Lemma hdef_upd_alloc PS PSg Perm hf g l v h h' g' :
is_lvalue (hf l) →
hplus (Hdef hf g) h = Hdef h' g' →
∃ h'', hplus (Hdef (hupd hf l (lvalue PS PSg Perm v)) g) h = Hdef h'' g'.
Proof.
intros; eapply hplus_def_inv in H0; desf.
∃ (hupd h' l (lvalue _ _ Perm v)).
unfold hplus, hupd; desc; des_if; desc; f_equal.
× extensionality l'; desf; desf. specialize (DEFv l).
red in H; desf; ins; desf; desf; eq_rect_simpl.
+ red in DEFv0; desf.
rewrite !permission_plusA in PSUMdef.
apply nonextendable_full_permission in PSUMdef; pplus_eq_zero.
by eapply HVval_equal; pplus_zero_simpl; eq_rect_simpl.
+ destruct n; red in DEFv0; desf; eq_rect_simpl.
rewrite !permission_plusA in PSUMdef.
apply nonextendable_full_permission in PSUMdef; pplus_eq_zero.
by pplus_zero_simpl.
+ red in DEFv0; desf.
rewrite !permission_plusA in PSUMdef.
apply nonextendable_full_permission in PSUMdef; pplus_eq_zero.
eby exfalso; eapply all_permissions_zero.
× by unfold gres_plus_total; rewrite PLUSg.
× destruct n; split; try congruence. intro l'. specialize (DEFv l'); desf; desf.
red in H; desf; ins; desf; desf; exfalso;
try red in DEFv; try red in DEFv0; desf;
rewrite !permission_plusA in PSUMdef;
apply nonextendable_full_permission in PSUMdef; pplus_eq_zero;
eby eapply all_permissions_zero.
Grab Existential Variables. done.
Qed.
Lemma hdef_upd_alloc2 PS PSg Perm hf g l v' h h' g' :
is_lvalue (hf l) →
hplus (Hdef hf g) h = Hdef h' g' →
∃ h'',
hplus (Hdef (hupd hf l (lvalue PS PSg Perm v')) g) h = Hdef h'' g'
∧ (∀ l' (NEQ: l' ≠ l), h'' l' = h' l').
Proof.
intros; eapply hplus_def_inv in H0; desc.
∃ (hupd h' l (lvalue _ _ Perm v')); desf.
unfold hupd, is_lvalue in *; desf; ins; desf; desc;
split; ins; desf; desf;
solve [
f_equal; [ | by unfold gres_plus_total; rewrite PLUSg];
extensionality l'; desf; ins; desf; exfalso;
solve [ specialize (HEAPcompat l); desf; desf; apply hvplusDEF_with_lvalue in HEAPcompat; congruence
| eby exfalso; eq_rect_simpl; red in p; desf; rewrite !permission_plusA in PSUMdef;
apply nonextendable_full_permission in PSUMdef; pplus_eq_zero; eapply all_permissions_zero ]
|
eby destruct n; split; [ | congruence]; unnw; ins; desf; desf; specialize (DEFv l); rewrite Heq in DEFv;
ins; desf; desf; try red in DEFv; try red in DEFv0; desf;
rewrite !permission_plusA in PSUMdef; apply nonextendable_full_permission in PSUMdef;
pplus_eq_zero; exfalso; eapply all_permissions_zero
].
Qed.
Lemmas about initialize
Lemma initialize_alloc PS PSg: ∀ hf l l', hf l ≠ @HVnone PS PSg ↔ initialize hf l' l ≠ @HVnone PS PSg.
Proof.
unfold initialize, hupd; split; ins; desf; congruence.
Qed.
Lemma hplus_init_def PS PSg hf g l h h' g' :
hplus (Hdef hf g) h = Hdef h' g' →
hplus (Hdef (initialize hf l) g) h ≠ @Hundef PS PSg.
Proof.
unfold hplus; intros; desf; desf; destruct n; split; try done. red.
intros; unfold initialize, hupd; try specialize (HEAPcompat v); try red in HEAPcompat; desf; ins; desf.
Qed.
Lemma hplus_init_def2 PS PSg hf g l h h' g' :
hplus (Hdef hf g) h = Hdef h' g' →
hf l ≠ @HVnone PS PSg →
hplus (Hdef (initialize hf l) g) h = Hdef (initialize h' l) g'.
Proof.
unfold hplus; intros; desf; desf.
by f_equal; extensionality l'; unfold initialize, hupd; desf; simpls; desf; f_equal;
rewrite !ohlplusA, (ohlplusC _ init1).
by destruct n; split; try done; red; intros; unfold initialize, hupd;
try specialize (HEAPcompat v); try red in HEAPcompat; desf; ins; desf.
Qed.
Lemma initialize_eq_raD PS PSg hf l l' PP QQ isrmw perm init:
initialize hf l l' = @HVra PS PSg PP QQ isrmw perm init →
∃ init', hf l' = HVra PP QQ isrmw perm init'.
Proof.
eby unfold initialize, hupd; ins; desf; eexists.
Qed.
Lemma initialize_is_rvalue PS PSg:
∀ (hf : val → HeapVal PS PSg) l l', is_rvalue (initialize hf l l') → is_rvalue (hf l').
Proof.
by unfold initialize; ins; desf; unfold hupd in H; desf; try done; subst; rewrite Heq.
Qed.
Lemma initialize_is_lvalue PS PSg:
∀ (hf : val → HeapVal PS PSg) l l', is_lvalue (initialize hf l l') → is_lvalue (hf l').
Proof.
by unfold initialize; ins; desf; unfold hupd in H; desf; try done; subst; rewrite Heq.
Qed.
Lemma initialize_is_atomic PS PSg:
∀ (hf : val → HeapVal PS PSg) l l', is_atomic (initialize hf l l') → is_atomic (hf l').
Proof.
by unfold initialize; ins; desf; unfold hupd in H; desf; try done; subst; rewrite Heq.
Qed.
Lemma initialize_is_nonatomic PS PSg:
∀ (hf : val → HeapVal PS PSg) l l', is_nonatomic (initialize hf l l') → is_nonatomic (hf l').
Proof.
by unfold initialize; ins; desf; unfold hupd in H; desf; try done; subst; rewrite Heq.
Qed.
Lemma initialize_preserves_label PS PSg:
∀ (hf : val → HeapVal PS PSg) l l' lbl, HVlabeled (hf l) lbl → HVlabeled (initialize hf l' l) lbl.
Proof.
ins; unfold initialize, hupd; desf; rewrite ?Heq0 in *; ins.
desf; desf; ins; desf; eauto.
by right; apply hlplus_monotone2.
by apply hlplus_monotone2.
Qed.
Lemma initialize_not_normal PS PSg:
∀ (hf : val → HeapVal PS PSg) l l' lbl
(LAB: HVlabeled (initialize hf l' l) lbl) (N: lbl ≠ HLnormal),
HVlabeled (hf l ) lbl.
Proof.
unfold initialize, hupd; desf; ins; desf; rewrite ?Heq0; ins; desf; eauto.
× desf; eauto.
right; red; destruct h0; ins; desf; ins; solve [ by destruct lbl; ins |
by red; eauto |
by red in LAB; desf ].
× desf; eauto.
ins; desf; destruct lbl; ins; red in LAB; desf.
× red; destruct h; ins; desf; ins; solve [ by destruct lbl; ins |
by red; eauto |
by red in LAB; desf ].
× ins; desf; destruct lbl; ins; red in LAB; desf.
Qed.
Lemma initialize_not_normalR PS PSg:
∀ (hf : val → HeapVal PS PSg) l l' lbl
(LAB: HVlabeledR (initialize hf l' l) lbl) (N: lbl ≠ HLnormal),
HVlabeledR (hf l ) lbl.
Proof.
unfold initialize, hupd; desf; ins; desf; rewrite ?Heq0; ins; desf.
× exploit ohlplus_with_basic_label; eauto; ins; desf.
apply hlplus_monotone_inv in LAB; desf.
destruct lbl; ins; red in LAB; desf.
× ins; desf.
destruct lbl; ins; red in LAB; desf.
Qed.
Lemmas about assertions
Lemma assn_sem_def PS PSg P h : assn_sem P h → h ≠ @Hundef PS PSg.
Proof.
induction P; ins; desf; try congruence.
eby eapply (H 0).
by red in H; desf.
by red in H; desf.
Qed.
Lemma sim_assn_sem PS PSg:
∀ (p p': assn PS PSg) (S: Asim p p') h, assn_sem p h ↔ assn_sem p' h.
Proof.
induction 1; ins; desf; eauto.
by split; ins; desf.
by split; ins; desf; eauto 8 using hplus_emp_r, assn_sem_def; try rewrite hplus_emp_r in *; desf.
by split; ins; desf; rewrite hplusC in *; vauto.
by split; ins; desf; first [rewrite hplusA in *|rewrite <- hplusA in *]; eauto 15.
by rewrite IHS.
by rewrite IHS1, IHS2.
by rewrite IHS1, IHS2.
by split; intros; apply H.
by split; ins; desf; repeat eexists; eauto; try apply IHS1; try apply IHS2.
by replace (fun x : val ⇒ mk_assn_mod (P2 x)) with (fun x : val ⇒ mk_assn_mod (P1 x));
try done; exten; intro; apply assn_mod_eqI1; simpl; apply assn_norm_ok.
by replace (fun x : val ⇒ mk_assn_mod (Q2 x)) with (fun x : val ⇒ mk_assn_mod (Q1 x));
try done; exten; intro; apply assn_mod_eqI1; simpl; apply assn_norm_ok.
by replace (fun x : val ⇒ mk_assn_mod (Q2 x)) with (fun x : val ⇒ mk_assn_mod (Q1 x));
try done; exten; intro; apply assn_mod_eqI1; simpl; apply assn_norm_ok.
by split; ins; split; desf; eexists; repeat split; eauto; apply IHS.
by split; ins; split; desf; eexists; repeat split; eauto; apply IHS.
Qed.
Lemma assn_sem_satD PS PSg (Q: assn PS PSg) h : assn_sem Q h → ∃ hf g, h = Hdef hf g.
Proof.
ins; eapply assn_sem_def in H; destruct h; vauto.
Qed.
Lemma precise_emp PS PSg : precise (@Aemp PS PSg).
Proof. red; ins; desf; rewrite !hplus_emp_l in *; vauto. Qed.
Lemma precise_star PS PSg (P Q: assn PS PSg) : precise P → precise Q → precise (Astar P Q).
Proof.
unfold precise; ins; desf; rewrite !hplusA in ×.
exploit (H _ SEM1 _ SEM'1); eauto; intro; desf.
exploit (H0 _ SEM2 _ SEM'2); eauto; intro; desf; eauto.
Qed.
Hint Resolve precise_emp precise_star.
Lemma assn_sem_disj PS PSg (P Q: assn PS PSg) h :
assn_sem (Adisj P Q) h ↔ assn_sem P h ∨ assn_sem Q h.
Proof.
by unfold Adisj; simpl; intuition; try tauto; apply assn_sem_def in H0.
Qed.
Lemma assn_sem_exists PS PSg PP (h: heap PS PSg) :
assn_sem (Aexists PP) h ↔ ∃ x, assn_sem (PP x) h.
Proof.
unfold Aexists; split; ins; desf; repeat split; ins; eauto using assn_sem_def.
by apply NNPP; intro; eauto.
specialize (H0 x); tauto.
Qed.
Lemma foldr_star_perm PS PSg:
∀ l l' (P: Permutation l l') init h,
assn_sem (foldr (@Astar PS PSg) l init) h →
assn_sem (foldr (@Astar PS PSg) l' init) h.
Proof.
induction 1; ins; desf; eauto 8.
rewrite hplusAC in *; repeat eexists; eauto.
Qed.
Lemma foldr_star_perm2 PS PSg:
∀ l l' (P: Permutation l l') init,
Asim (foldr (@Astar PS PSg) l init) (foldr (@Astar PS PSg) l' init).
Proof.
induction 1; ins; desf; eauto 8 using Asim.
Qed.
Lemma assn_sem_foldr_true_ext PS PSg A (f: A → assn PS PSg) l h h' :
assn_sem (foldr (@Astar _ _) (List.map f l) Atrue ) h →
hplus h h' ≠ @Hundef PS PSg →
assn_sem (foldr (@Astar _ _) (List.map f l) Atrue ) (hplus h h').
Proof.
induction[h] l; ins; desf; rewrite hplusA in ×.
repeat eexists; eauto; eapply IHl; ins.
Qed.
Lemma implies_trans PS PSg (P Q R: assn PS PSg): implies P Q ∧ implies Q R → implies P R.
Proof.
unfold implies; ins; desf; eauto.
Qed.
Lemma implies_frame PS PSg (P Q F: assn PS PSg): implies P Q → implies (Astar P F) (Astar Q F).
Proof.
by unfold implies; ins; desf; eexists _, _; eauto.
Qed.
Lemma assn_sem_assn_norm PS PSg (P: assn PS PSg) h: assn_sem (assn_norm P) h ↔ assn_sem P h.
Proof.
ins; apply sim_assn_sem, Asim_sym, Asim_assn_norm.
Qed.
Lemma nabla_star_dist PS PSg:
∀ (h: heap PS PSg) P Q, assn_sem (Anabla (Astar P Q)) h ↔ assn_sem (Astar (Anabla P) (Anabla Q)) h.
Proof.
split; ins; desf.
{
∃ (lupd h1 HLnabla), (lupd h2 HLnabla) ; repeat (apply conj).
by red in H; desf.
{ rewrite <- lupd_hplus_dist.
eapply exact_label_sim; eauto.
apply lupd_label.
by red in H1; desf.
eapply Hsim_sym, Hsim_trans; eauto.
apply lupd_sim.
red in H1; desf.
}
eby eapply lupd_label, assn_sem_def.
{ eexists;repeat split; try edone.
eby eapply Hsim_sym, lupd_sim, assn_sem_def.
apply exact_label_hplus_dist in H2; desf.
}
eby eapply lupd_label, assn_sem_def.
{
eexists;repeat split; try edone.
eby eapply Hsim_sym, lupd_sim, assn_sem_def.
apply exact_label_hplus_dist in H2; desf.
}
}
{
split.
by apply exact_label_hplus_dist_inv.
assert (S: Hsim (hplus h1 h2) (hplus h'0 h')) by (by apply hplus_sim).
eexists _; split.
× eexists _, _; repeat apply conj; try exact H3; try exact H6.
2: edone.
red in S; desf; congruence.
× split; try done.
apply exact_label_hplus_dist_inv; try done.
red in S; desf; congruence.
}
Qed.
Lemma precise_assn_norm PS PSg (P: assn PS PSg): precise P ↔ precise (assn_norm P).
Proof.
unfold precise; split; ins.
by rewrite assn_sem_assn_norm in *; apply H.
by rewrite <- assn_sem_assn_norm in *; apply H.
Qed.
Lemma normalizable_star PS PSg (P Q: assn PS PSg) :
normalizable P → normalizable Q → normalizable (Astar P Q).
Proof.
unfold normalizable; ins; desf.
specialize (H _ H3); specialize (H0 _ H4); desf.
∃ (hplus hN0 hN), (hplus h'0 h'); split.
× repeat eexists; try exact H; try exact H0.
rewrite hplusA, (hplusAC hN), <- hplusA in H1.
eby eapply hplus_not_undef_l.
× split.
+ apply exact_label_hplus_dist_inv; try done.
rewrite hplusA, (hplusAC hN), <- hplusA in H1.
eby eapply hplus_not_undef_l.
+ by rewrite !hplusA, (hplusAC hN).
Qed.
Lemma normalizable_assn_norm PS PSg (P: assn PS PSg): normalizable P ↔ normalizable (assn_norm P).
Proof.
unfold normalizable; split; ins; desf.
× rewrite assn_sem_assn_norm in ×.
specialize (H _ H0); desc.
∃ hN, h'.
rewrite assn_sem_assn_norm; eauto.
× rewrite <- assn_sem_assn_norm in ×.
specialize (H _ H0); desc.
∃ hN, h'.
rewrite <- assn_sem_assn_norm; eauto.
Qed.
Lemma normalizable_emp PS PSg: normalizable (@Aemp PS PSg).
Proof.
red; ins.
∃ hemp, hemp.
rewrite hplus_emp_l; intuition.
eby unfold hemp; eexists _, _.
Qed.
Hint Resolve normalizable_emp.
More lemmas
Lemma hplus_ram_lD PS PSg:
∀ h g h1 g1 h2 l PP QQ perm init,
hplus (Hdef h1 g1) h2 = Hdef h g→
h1 l = HVra PP QQ true perm init →
∃ PP' perm' init',
h l = HVra PP' QQ true perm' init' ∧
(∀ v h, assn_sem (sval (PP v)) h → assn_sem (sval (PP' v)) h) ∧
∃ hf g', h2 = Hdef hf g' ∧
(hf l = @HVnone PS PSg ∧ init = init' ∧ perm = perm'
∨ ∃ PP'' QQ'' isrmw'' perm'' init'',
hf l = HVra PP'' QQ'' isrmw'' perm'' init'' ∧
init' = ohlplus init init'' ∧
perm' = ohlplus perm perm'' ∧
(∀ v, sval (QQ'' v) = Aemp ∨ QQ'' v = QQ v)).
Proof.
destruct h2; ins; desf; desf.
specialize (HEAPcompat l); rewrite H0 in *; ins; desf;
repeat eexists; vauto; try red; ins; desf; try (by rewrite e in *).
right; repeat eexists; ins; vauto.
destruct (HEAPcompat v); ins; desf.
by destruct isrmwflag; ins; eauto using sym_eq, assn_mod_eqI1.
right; apply assn_mod_eqI1; congruence.
Qed.
Lemma hplus_ram_rD PS PSg:
∀ h g h1 h2 g2 l PP QQ perm init,
hplus h1 (Hdef h2 g2) = Hdef h g →
h2 l = HVra PP QQ true perm init →
∃ PP' perm' init',
h l = HVra PP' QQ true perm' init' ∧
(∀ v h, assn_sem (sval (PP v)) h → assn_sem (sval (PP' v)) h) ∧
∃ hf g', h1 = Hdef hf g' ∧
(hf l = @HVnone PS PSg ∧ init = init' ∧ perm = perm'
∨ ∃ PP'' QQ'' isrmw'' perm'' init'',
hf l = HVra PP'' QQ'' isrmw'' perm'' init'' ∧
init' = ohlplus init init'' ∧
perm' = ohlplus perm perm'' ∧
(∀ v, sval (QQ'' v) = Aemp ∨ QQ'' v = QQ v)).
Proof.
ins; rewrite hplusC in *; eauto using hplus_ram_lD.
Qed.
Lemma hplus_ra_lD PS PSg:
∀ h g h1 g1 h2 l PP QQ perm init,
hplus (Hdef h1 g1) h2 = Hdef h g →
h1 l = HVra PP QQ false perm init →
∃ PP' QQ' isrmw' perm' init',
h l = HVra PP' QQ' isrmw' perm' init' ∧
(∀ v h, assn_sem (sval (PP v)) h → assn_sem (sval (PP' v)) h) ∧
∃ hf g', h2 = Hdef hf g' ∧
(hf l = @HVnone PS PSg ∧ (∀ v, QQ' v = QQ v) ∧ init = init' ∧ isrmw' = false ∧ perm = perm'
∨ ∃ PP'' QQ'' perm'' init'',
hf l = HVra PP'' QQ'' isrmw' perm'' init'' ∧
init' = ohlplus init init'' ∧
perm' = ohlplus perm perm'' ∧
(∀ v, Asim (sval (QQ' v)) (Astar (sval (QQ v)) (sval (QQ'' v))))).
Proof.
destruct h2; ins; desf; desf.
specialize (HEAPcompat l); rewrite H0 in *; ins; desf;
repeat eexists; vauto; try red; ins; desf; try (by rewrite e in *).
right; repeat eexists; ins; vauto.
by destruct (HEAPcompat v); ins; desf; rewrite H, ?H1; Asim_simpl; eauto using Asim.
by right; repeat eexists; ins; vauto; Asim_simpl.
Qed.
Lemma hplus_ra_rD PS PSg:
∀ h g h1 h2 g2 l PP QQ perm init,
hplus h1 (Hdef h2 g2) = Hdef h g →
h2 l = HVra PP QQ false perm init →
∃ PP' QQ' isrmw' perm' init',
h l = HVra PP' QQ' isrmw' perm' init' ∧
(∀ v h, assn_sem (sval (PP v)) h → assn_sem (sval (PP' v)) h) ∧
∃ hf g', h1 = Hdef hf g' ∧
(hf l = @HVnone PS PSg∧ (∀ v, QQ' v = QQ v) ∧ init = init' ∧ isrmw' = false ∧ perm = perm'
∨ ∃ PP'' QQ'' perm'' init'',
hf l = HVra PP'' QQ'' isrmw' perm'' init'' ∧
init' = ohlplus init init'' ∧
perm' = ohlplus perm perm'' ∧
(∀ v, Asim (sval (QQ' v)) (Astar (sval (QQ v)) (sval (QQ'' v))))).
Proof.
ins; rewrite hplusC in *; eauto using hplus_ra_lD.
Qed.
Lemma hsum_raD PS PSg:
∀ h g hs h'' g'' l PP QQ isrmw perm init,
hsum hs = Hdef h g →
In (Hdef h'' g'') hs →
h'' l = @HVra PS PSg PP QQ isrmw perm init →
∃ PP' QQ' isrmw' perm' init',
h l = HVra PP' QQ' isrmw' perm' init' ∧ oHLleq init init' ∧ (isrmw → isrmw') ∧ oHLleq perm perm'
∧ (∀ v h, assn_sem (sval (PP v)) h → assn_sem (sval (PP' v)) h).
Proof.
intros until 0; induction[h g PP QQ perm init] hs; ins; rewrite hsum_cons in ×.
desf.
× destruct isrmw.
+ eapply hplus_ram_lD in H; desf; eauto; repeat (eexists; eauto); ins; desf;
auto using oHLleq_refl, ohlplus_monotone1.
+ eapply hplus_ra_lD in H; eauto; desf; repeat (eexists; eauto); ins; desf;
auto using oHLleq_refl, ohlplus_monotone1.
× rewrite hplusC in H; destruct (hsum hs); ins; desf.
eapply (IHhs _ _ _ _ _ _ eq_refl) in H0; eauto; desf.
specialize (HEAPcompat l); rewrite H0 in *; ins; desf; repeat (eexists; eauto); ins; desf; eauto;
solve [
eapply oHLleq_trans; split; eauto using ohlplus_monotone1
|
apply H5 in H; rewrite e in *; done
].
Qed.
Lemma hplus_raD PS PSg:
∀ h g h1 h2 l PP QQ isrmw perm init,
hplus h1 h2 = Hdef h g →
h l = HVra PP QQ isrmw perm init →
∃ hf1 g1 hf2 g2,
h1 = Hdef hf1 g1 ∧ h2 = Hdef hf2 g2
∧ << N: hf1 l ≠ @HVnone PS PSg ∨ hf2 l ≠ @HVnone PS PSg >>
∧ << L: hf1 l = @HVnone PS PSg ∨ ∃ PP' QQ' isrmw' perm' init',
hf1 l = HVra PP' QQ' isrmw' perm' init' ∧
(∀ v h, assn_sem (sval (PP' v)) h → assn_sem (sval (PP v)) h) >>
∧ << R: hf2 l = @HVnone PS PSg ∨ ∃ PP' QQ' isrmw' perm' init',
hf2 l = HVra PP' QQ' isrmw' perm' init' ∧
(∀ v h, assn_sem (sval (PP' v)) h → assn_sem (sval (PP v)) h) >>.
Proof.
destruct h1, h2; unfold NW; ins; desf; desf.
repeat eexists; specialize (HEAPcompat l); unfold hvplusDEF in *; desf; vauto;
right; vauto; repeat eexists; ins; desf; try congruence; eauto;
specialize (HEAPcompat0 v); rewrite ?e in *; ins.
red in HEAPcompat0; desf; rewrite HEAPcompat0, ?e, ?a2 in *; ins.
Grab Existential Variables. all: done.
Qed.
Lemma hplus_raD' PS PSg:
∀ h g h1 h2 l PP QQ isrmw perm init,
hplus h1 h2 = Hdef h g →
h l = HVra PP QQ isrmw perm init →
∃ hf1 g1 hf2 g2, h1 = Hdef hf1 g1 ∧ h2 = Hdef hf2 g2 ∧
( (hf1 l = @HVnone PS PSg ∧ ∃ PP' QQ', hf2 l = HVra PP' QQ' isrmw perm init ∧ PP' = PP ∧ QQ' = QQ)
∨ (hf2 l = @HVnone PS PSg ∧ ∃ PP' QQ', hf1 l = HVra PP' QQ' isrmw perm init ∧ PP' = PP ∧ QQ' = QQ)
∨ (∃ PP1 QQ1 isrmw1 perm1 init1 PP2 QQ2 isrmw2 perm2 init2,
hf1 l = HVra PP1 QQ1 isrmw1 perm1 init1 ∧
hf2 l = HVra PP2 QQ2 isrmw2 perm2 init2 ∧
perm = ohlplus perm1 perm2 ∧
init = ohlplus init1 init2 ∧
isrmw = isrmw1 || isrmw2 ∧
(∀ v, Acombinable (sval (PP1 v)) (sval (PP2 v))) ∧
(∀ v h, assn_sem (sval (PP v)) h ↔
assn_sem (sval (PP1 v)) h ∨ assn_sem (sval (PP2 v)) h))).
Proof.
destruct h1, h2; unfold NW; ins; desf; desf;
repeat eexists. specialize (HEAPcompat l); unfold hvplusDEF in *; desf; vauto; try (by ins; desf);
[left | right;left | right;right]; try (repeat (eexists; ins); desf;
specialize (HEAPcompat0 v); unfold Acombinable in *; ins; desf; desf;
rewrite ?HEAPcompat0, ?e in *; desf; vauto).
Qed.
Lemma hplus_eq_raD PS PSg:
∀ h g h1 h2 l PP QQ isrmw perm init v,
hplus h1 h2 = Hdef h g →
h l = @HVra PS PSg PP QQ isrmw perm init →
∃ hf g' PP' QQ' isrmw' perm' init',
(h1 = Hdef hf g' ∨ h2 = Hdef hf g') ∧ hf l = HVra PP' QQ' isrmw' perm' init' ∧
(∀ h, assn_sem (sval (PP v)) h ↔ assn_sem (sval (PP' v)) h).
Proof.
destruct h1, h2; unfold NW; ins; desf; desf.
specialize (HEAPcompat l); red in HEAPcompat; desf; ins; desf;
try solve [repeat (eexists; try edone); eauto].
specialize (HEAPcompat0 v); red in HEAPcompat0; desf; try congruence.
by clear Heq0; repeat (eexists; try edone); eauto.
by repeat (eexists; try edone); eauto; congruence.
Qed.
Lemma hsum_eq_raD PS PSg:
∀ h' g' hs l PP QQ isrmw perm init v,
hsum hs = Hdef h' g' →
h' l = @HVra PS PSg PP QQ isrmw perm init →
∃ h'' g'' PP' QQ' isrmw' perm' init',
In (Hdef h'' g'') hs ∧
h'' l = HVra PP' QQ' isrmw' perm' init' ∧
(∀ h, assn_sem (sval (PP v)) h ↔ assn_sem (sval (PP' v)) h).
Proof.
intros until 0; induction[h' g' PP QQ isrmw perm init] hs; ins; [by inv H|].
rewrite hsum_cons in ×.
eapply hplus_eq_raD in H; eauto.
desf; eauto 15.
exploit IHhs; eauto; intro; desf; eauto 10.
do 8 eexists; eauto.
by split; try edone; ins; rewrite H2.
Qed.
Lemma hplus_eq_ra_rmwD PS PSg h g h1 h2 l PP QQ perm init:
hplus h1 h2 = Hdef h g →
h l = @HVra PS PSg PP QQ true perm init →
∃ hf g' PP' QQ' perm' init',
(h1 = Hdef hf g' ∨ h2 = Hdef hf g') ∧ hf l = HVra PP' QQ' true perm' init'.
Proof.
ins; eapply hplus_def_inv in H; desf.
specialize (DEFv l); rewrite PLUSv in *; clear PLUSv.
red in DEFv; desf; ins; desf; try destruct isrmwflag; ins; desf;
try by (repeat eexists; try edone; eauto).
Qed.
Lemma hsum_eq_ra_rmwD PS PSg:
∀ h' g' hs l PP QQ perm init,
hsum hs = Hdef h' g' →
h' l = @HVra PS PSg PP QQ true perm init →
∃ h'' g'' PP' QQ' perm' init', In (Hdef h'' g'') hs ∧ h'' l = HVra PP' QQ' true perm' init'.
Proof.
intros until 0; generalize perm init; induction[h' g' PP QQ init] hs; ins; [by inv H|].
rewrite hsum_cons in *; eapply hplus_eq_ra_rmwD in H; eauto.
desf; eauto 10; exploit IHhs; eauto; ins; desf; eauto 10.
Qed.
Lemma hplus_eq_ra_ownD PS PSg h g h1 h2 l PP QQ perm init v :
hplus h1 h2 = Hdef h g →
h l = @HVra PS PSg PP QQ false perm init →
sval (QQ v) ≠ Aemp →
sval (QQ v) ≠ Afalse →
∃ hf g' PP' QQ' perm' init',
(h1 = Hdef hf g' ∨ h2 = Hdef hf g') ∧ hf l = HVra PP' QQ' false perm' init'
∧ sval (QQ' v) ≠ Aemp ∧ sval (QQ' v) ≠ Afalse.
Proof.
ins; eapply hplus_def_inv in H; desf; desf.
specialize (DEFv l); rewrite PLUSv in *; clear PLUSv.
red in DEFv; desf; ins; desf; try destruct isrmwflag; ins; desf;
try solve [repeat (eexists; try eassumption); eauto].
case_eq (sval (QQ0 v)); ins;
try solve [clear Heq0; repeat (eexists; try eassumption); eauto;
instantiate; congruence].
case_eq (sval (QQ1 v)); ins;
try solve [clear Heq; repeat (eexists; try eassumption); eauto;
instantiate; congruence].
by rewrite H, H0, assn_norm_star_false in ×.
by rewrite H, H0, assn_norm_star_emp_r in ×.
clear Heq; repeat (eexists; try eassumption); eauto.
by intro H0; apply H1; rewrite H, H0, assn_norm_star_emp, assn_norm_emp.
by intro H0; apply H2; rewrite H, H0, assn_norm_star_emp.
Qed.
Lemma hsum_eq_ra_ownD PS PSg:
∀ h' g' hs l PP QQ perm init v,
hsum hs = Hdef h' g' →
h' l = @HVra PS PSg PP QQ false perm init →
sval (QQ v) ≠ Aemp →
sval (QQ v) ≠ Afalse →
∃ h'' g'' PP' QQ' perm' init',
In (Hdef h'' g'') hs ∧ h'' l = HVra PP' QQ' false perm' init'
∧ sval (QQ' v) ≠ Aemp ∧ sval (QQ' v) ≠ Afalse.
Proof.
intros until 0; generalize perm init; induction[h' g' PP QQ init] hs; ins; [by inv H|].
rewrite hsum_cons in *; eapply hplus_eq_ra_ownD in H; eauto.
desf; eauto 12; exploit IHhs; eauto; ins; desf; eauto 15.
Qed.
Lemma hplus_ra_own_l PS PSg h g h1 g1 h2 l PP QQ perm init v :
hplus (Hdef h1 g1) h2 = Hdef h g →
h1 l = @HVra PS PSg PP QQ false perm init →
sval (QQ v) ≠ Aemp →
sval (QQ v) ≠ Afalse →
∃ PP' QQ' perm' init',
h l = HVra PP' QQ' false perm' init' ∧ sval (QQ' v) ≠ Aemp ∧ sval (QQ' v) ≠ Afalse.
Proof.
intros; eapply hplus_def_inv in H; desf.
specialize (DEFv l); rewrite PLUSv in *; clear PLUSv;
red in DEFv; desf; ins; desf; try destruct isrmwflag; ins; desf;
try solve [repeat eexists; eauto].
by exfalso; destruct (DEFv v); desf.
repeat eexists; ins; intro; [
apply assn_norm_star_eq_emp in H |
apply assn_norm_star_eq_false in H ]; desf; auto;
eapply H1; destruct (QQ v); ins; congruence.
Qed.
Lemma hplus_ra_own_r PS PSg h g h1 h2 g2 l PP QQ perm init v :
hplus h1 (Hdef h2 g2) = Hdef h g →
h2 l = @HVra PS PSg PP QQ false perm init →
sval (QQ v) ≠ Aemp →
sval (QQ v) ≠ Afalse →
∃ PP' QQ' perm' init',
h l = HVra PP' QQ' false perm' init' ∧ sval (QQ' v) ≠ Aemp ∧ sval (QQ' v) ≠ Afalse.
Proof. by rewrite hplusC; apply hplus_ra_own_l. Qed.
Lemma hsum_has_ra_own PS PSg h g hs hf g' l PP QQ perm init v :
hsum hs = Hdef h g →
In (Hdef hf g') hs →
hf l = @HVra PS PSg PP QQ false perm init →
sval (QQ v) ≠ Aemp →
sval (QQ v) ≠ Afalse →
∃ PP' QQ' perm' init',
h l = HVra PP' QQ' false perm' init' ∧ sval (QQ' v) ≠ Aemp ∧ sval (QQ' v) ≠ Afalse.
Proof.
induction[h g PP QQ init] hs; ins.
rewrite hsum_cons in *; desf.
eapply hplus_ra_own_l; eauto.
exploit hplus_def_inv; eauto; ins; desf.
exploit IHhs; eauto; intro; desf.
rewrite x1 in *; eapply hplus_ra_own_r; eauto.
Qed.
Lemma hplus_init1 PS PSg E PP QQ isrmw perm1 perm2 init1 init2 :
hplus (hsingl PS PSg E (HVra PP QQ isrmw perm1 init1))
(hsingl PS PSg E (HVra Wemp Remp false perm2 init2))
= hsingl PS PSg E (HVra PP QQ isrmw (ohlplus perm1 perm2) (ohlplus init1 init2)).
Proof.
rewrite hplus_hsingl.
× f_equal; extensionality l.
unfold hupd; desf; simpls.
f_equal.
+ extensionality v; desf.
apply assn_mod_eqI; unfold Wemp; rewrite e; simpl.
apply Asim_sym, Asim_assn_norm.
+ desf; extensionality v.
apply assn_mod_eqI; simpl.
rewrite assn_norm_emp, assn_norm_star_emp_r.
apply Asim_sym, Asim_assn_norm.
+ by destruct isrmw.
× split; ins; vauto.
left; unfold hv_rval; desf.
Qed.
Lemma atomic_hsingl_duplicate PS PSg:
∀ l PP QQ isrmw perm init, hsingl PS PSg l (HVra PP QQ isrmw perm init) =
hplus (hsingl PS PSg l (HVra PP QQ isrmw perm init))
(hsingl PS PSg l (HVra Wemp Remp false perm init)).
Proof.
intros; rewrite hplus_hsingl.
× f_equal; extensionality l'.
unfold hupd; desf; simpls.
f_equal; try by rewrite ohlplus_same.
+ by extensionality v; desf; apply assn_mod_eqI1.
+ extensionality v; desf; apply assn_mod_eqI1; simpl.
by rewrite assn_norm_emp, assn_norm_star_emp_r, assn_norm_mod.
+ by destruct isrmw.
× split; ins; vauto.
left; unfold hv_rval; desf.
Qed.
Lemma hplus_hsingl_rel_rmwacq PS PSg:
∀ l PP QQ labW labW' labR labR',
hplus (hsingl PS PSg l (HVra PP Remp false labW labR))
(hsingl PS PSg l (HVra Wemp QQ true labW' labR'))
= hsingl PS PSg l (HVra PP QQ true (ohlplus labW labW') (ohlplus labR labR')).
Proof.
intros; rewrite hplus_hsingl.
2: by split; ins; vauto.
ins; f_equal. exten; ins; unfold hupd; desf; desf.
f_equal.
by exten; ins; desf; apply assn_mod_eqI1.
Qed.
Lemma hdef_initializeE PS PSg hf g E PP QQ isrmw perm init:
hf E = HVra PP QQ isrmw perm init →
Hdef (initialize hf E) g = hplus (Hdef hf g)
(hsingl PS PSg E (HVra Wemp Remp false None (Some HLCnormal))).
Proof.
rewrite hplusC; unfold initialize, hupd; ins; desf; desf.
× f_equal.
2: by rewrite gres_plus_total_emp_l.
extensionality w; specialize (HEAPcompat w); red in HEAPcompat; ins; desf; ins; try congruence.
rewrite Heq1 in Heq; inv Heq.
f_equal; desf.
extensionality v; eapply assn_mod_eqI; ins; desf; ins; Asim_simpl; vauto.
× destruct n; split.
2: by rewrite gres_plusC, gres_plus_emp_r.
intro m; ins; desf; ins; desf; repeat split; try apply Lcombinable_same;
ins; vauto; destruct isrmw; vauto.
Qed.
Lemma hdef_initializeE2 PS PSg: ∀ hf g E (AT: is_atomic (hf E)),
Hdef (initialize hf E) g = hplus (Hdef hf g)
(hsingl PS PSg E (HVra Wemp Remp false None (Some HLCnormal))).
Proof.
unfold is_atomic; intros; desf.
eby eapply hdef_initializeE.
Qed.
Lemma hplus_is_nonatomic_full PS PSg:
∀ h g h1 h2 l,
hplus h1 h2 = Hdef h g →
is_nonatomic (h l) →
∃ hf1 g1 hf2 g2,
h1 = Hdef hf1 g1 ∧ h2 = Hdef hf2 g2 ∧
(is_nonatomic (hf1 l) ∨ hf1 l = @HVnone PS PSg) ∧
(is_nonatomic (hf2 l) ∨ hf2 l = @HVnone PS PSg) ∧
(hf1 l ≠ @HVnone PS PSg ∨ hf2 l ≠ @HVnone PS PSg).
Proof.
ins.
exploit hplus_is_nonatomic; eauto; ins; desc.
eexists _, _, _, _; repeat split; eauto.
× desf; eauto.
rewrite hplus_unfold in H; desf; desf.
specialize (HEAPcompat l).
destruct (hf1 l); ins; desf; eauto.
× desf; eauto.
rewrite hplus_unfold in H; desf; desf.
specialize (HEAPcompat l).
rewrite hvplusC in H0; ins.
apply hvplusDEFC in HEAPcompat.
destruct (hf2 l); ins; desf; eauto.
× apply not_and_or; intro C; desc; rewrite C, C0 in *; desf.
Qed.
Lemma hplus_is_nonatomic_l PS PSg :
∀ h g h1 h2 l,
hplus h1 h2 = Hdef h g →
is_nonatomic (h l) →
∃ hf1 g1,
h1 = Hdef hf1 g1 ∧ (is_nonatomic (hf1 l) ∨ hf1 l = @HVnone PS PSg).
Proof.
ins; exploit hplus_is_nonatomic_full; eauto.
ins; desc.
eby eexists _, _.
Qed.
Lemma hplus_is_nonatomic_r PS PSg :
∀ h g h1 h2 l,
hplus h1 h2 = Hdef h g →
is_nonatomic (h l) →
∃ hf2 g2,
h2 = Hdef hf2 g2 ∧ (is_nonatomic (hf2 l) ∨ hf2 l = @HVnone PS PSg).
Proof.
ins; exploit hplus_is_nonatomic_full; eauto.
ins; desc.
eby eexists _, _.
Qed.
Lemma hsum_is_nonatomic_all PS PSg :
∀ hs h g l,
hsum hs = Hdef h g →
is_nonatomic (h l) →
∀ hf g, In (Hdef hf g) hs → hf l = @HVnone PS PSg ∨ is_nonatomic (hf l).
Proof.
induction hs; ins; desf.
× rewrite hsum_cons in H.
eapply hplus_is_nonatomic_full in H; eauto; desf; eauto.
× rewrite hsum_cons in H.
eapply hplus_is_nonatomic_full in H; eauto; desf; eauto;
exploit hsum_nalloc_all; eauto; ins; desf; eauto.
Qed.
Lemma is_nonatomic_initialize PS PSg :
∀ (hf: val → HeapVal PS PSg) l l', is_nonatomic (hf l) → is_nonatomic (initialize hf l' l).
Proof.
unfold initialize, is_nonatomic, hupd; ins; desf.
Qed.
Lemma Hsim_nalloc PS PSg :
∀ h hf g l ,
Hsim h (Hdef hf g) →
hf l = @HVnone PS PSg →
∃ hf', h = Hdef hf' g ∧ hf' l = @HVnone PS PSg.
Proof.
unfold Hsim; ins; desf; eexists; split; eauto.
specialize (H2 l); rewrite H0 in H2; red in H2; desf.
Qed.
Lemma is_nonatomic_hsim PS PSg :
∀ (hf1 hf2: val → HeapVal PS PSg) l, HFsim hf1 hf2 → (is_nonatomic (hf1 l) ↔ is_nonatomic (hf2 l)).
Proof.
by ins; specialize (H l); destruct (hf1 l), (hf2 l).
Qed.
Lemma hplus_propagate_initialize PS PSg:
∀ (hf: val → HeapVal PS PSg) g' l (A: is_atomic (hf l))
hFR h g (EQ: hplus (Hdef hf g') hFR = Hdef h g),
hplus (Hdef (initialize hf l) g') hFR = Hdef (initialize h l) g.
Proof.
intros.
exploit (hplus_has_atomic_l _ l EQ); intros; desf.
unfold is_atomic in *; desf.
erewrite hdef_initializeE; eauto.
rewrite hplusA, (hplusC _ hFR), <- hplusA, EQ.
eby erewrite hdef_initializeE.
Qed.
Opaque hplus.
This page has been generated by coqdoc