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.
Lemma all_permissions_zero PS : @permissionsOK PS (Pzero PS) (Pzero PS) (Pzero PS) → False.
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'.
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.
Lemma has_value_sim PS PSg (hv hv': HeapVal PS PSg) v (SIM: HVsim hv hv'): has_value hv v ↔ has_value hv' v.
Lemma is_lvalue_implies_is_nonatomic PS PSg (hv : HeapVal PS PSg): is_lvalue hv → is_nonatomic hv.
Lemma is_rvalue_implies_is_nonatomic PS PSg (hv : HeapVal PS PSg): is_rvalue hv → is_nonatomic hv.
Lemma is_lvalue_implies_normal PS PSg hv: is_lvalue hv → HVlabeled hv HLnormal ∧ hv ≠ @HVnone PS PSg.
Lemma is_rvalue_implies_normal PS PSg hv: is_rvalue hv → HVlabeled hv HLnormal ∧ hv ≠ @HVnone PS PSg.
Lemma is_lvalue_implies_normal_weak PS PSg (hv : HeapVal PS PSg): is_lvalue hv → HVlabeled hv HLnormal.
Lemma is_rvalue_implies_normal_weak PS PSg (hv : HeapVal PS PSg): is_rvalue hv → HVlabeled hv HLnormal.
Lemma reduce_label_to_basic (lbl: HeapLabelCombination):
∃ (lblB : HeapLabel), HLleq lblB lbl.
Lemma labeled_lvalue PS PSg (hv : HeapVal PS PSg) lbl : is_lvalue hv → HVlabeled hv lbl → lbl = HLnormal.
Lemma is_rvalue_weaken PS PSg: ∀ (hv : HeapVal PS PSg) v, is_rvalueV hv v → is_rvalue hv.
Lemma hvplusDEF_with_lvalue PS PSg:
∀ hv1 hv2 (LVAL: is_lvalue hv1) (DEF: hvplusDEF hv1 hv2), hv2 = @HVnone PS PSg.
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).
Lemma lupd_sim2 PS PSg:
∀ (h h' : heap PS PSg) lbl, Hsim h h' → Hsim (lupd h lbl) h'.
Lemma lupd_label PS PSg:
∀ (h : heap PS PSg) lbl, h ≠ Hundef → HlabeledExact (lupd h lbl) lbl.
Lemma lupd_eq PS PSg:
∀ (h h' : heap PS PSg) lbl (SIM: Hsim h h') (LBL: HlabeledExact h lbl), h = lupd h' lbl.
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'.
Lemmas about heap labels and hlplus.
Lemma Rlabel_implies_label PS PSg: ∀ (hv : HeapVal PS PSg) lbl, HVlabeledR hv lbl → HVlabeled hv lbl.
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'.
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'.
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'.
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'.
Lemma nonatomic_label PS PSg:
∀ (hv : HeapVal PS PSg) (NA: is_nonatomic hv) lbl, HVlabeledExact hv lbl → HVlabeled hv lbl.
Lemma basic_is_normal:
∀ (lbl: HeapLabel), is_normal lbl ↔ lbl = HLnormal.
Lemma basic_is_triangle:
∀ (lbl: HeapLabel), is_triangle lbl ↔ lbl = HLtriangle.
Lemma basic_is_nabla:
∀ (lbl: HeapLabel), is_nabla lbl ↔ lbl = HLnabla.
Lemma HLleq_trans:
∀ lbl1 lbl2 lbl3, HLleq lbl1 lbl2 ∧ HLleq lbl2 lbl3 → HLleq lbl1 lbl3.
Lemma HLleq_refl:
∀ lbl, HLleq lbl lbl.
Lemma hlplus_same lbl:
hlplus lbl lbl = lbl.
Lemma hlplusC lbl1 lbl2:
hlplus lbl1 lbl2 = hlplus lbl2 lbl1.
Lemma hlplusA lbl1 lbl2 lbl3:
hlplus (hlplus lbl1 lbl2) lbl3 = hlplus lbl1 (hlplus lbl2 lbl3).
Lemma hlplus_monotone:
∀ lbl1 lbl2 lbl1' lbl2',
HLleq lbl1 lbl1' ∧ HLleq lbl2 lbl2' → HLleq (hlplus lbl1 lbl2) (hlplus lbl1' lbl2').
Lemma hlplus_monotone_inv: ∀ (lbl: HeapLabel) lbl1 lbl2,
HLleq lbl (hlplus lbl1 lbl2) → HLleq lbl lbl1 ∨ HLleq lbl lbl2.
Lemma hlplus_monotone1:
∀ lbl lbl', HLleq lbl (hlplus lbl lbl').
Lemma hlplus_monotone2:
∀ lbl lbl1 lbl2, HLleq lbl lbl1 → HLleq lbl (hlplus lbl1 lbl2).
Lemma is_normal_monotone:
∀ lbl lbl' (LEQ: HLleq lbl lbl'), is_normal lbl → is_normal lbl'.
Lemma normal_hlplus:
∀ lbl1 lbl2, is_normal (hlplus lbl1 lbl2) → is_normal lbl1 ∨ is_normal lbl2.
Lemma not_normal_hlplus:
∀ lbl1 lbl2, ¬ is_normal (hlplus lbl1 lbl2) → ¬ is_normal lbl1 ∧ ¬ is_normal lbl2.
Lemma hlplus_eq_basic:
∀ lbl1 lbl2 (lbl: HeapLabel), hlplus lbl1 lbl2 = lbl → lbl1 = lbl ∧ lbl2 = lbl.
Lemma oHLleq_trans:
∀ lbl1 lbl2 lbl3, oHLleq lbl1 lbl2 ∧ oHLleq lbl2 lbl3 → oHLleq lbl1 lbl3.
Lemma oHLleq_refl:
∀ lbl, oHLleq lbl lbl.
Lemma ohlplus_same lbl:
ohlplus lbl lbl = lbl.
Lemma ohlplusC lbl1 lbl2:
ohlplus lbl1 lbl2 = ohlplus lbl2 lbl1.
Lemma ohlplusA lbl1 lbl2 lbl3:
ohlplus (ohlplus lbl1 lbl2) lbl3 = ohlplus lbl1 (ohlplus lbl2 lbl3).
Lemma ohlplus_none_l: ∀ lbl, ohlplus None lbl = lbl.
Lemma ohlplus_monotone:
∀ lbl1 lbl2 lbl1' lbl2',
oHLleq lbl1 lbl1' ∧ oHLleq lbl2 lbl2' → oHLleq (ohlplus lbl1 lbl2) (ohlplus lbl1' lbl2').
Lemma ohlplus_monotone1:
∀ lbl lbl', oHLleq lbl (ohlplus lbl lbl').
Lemma ohlplus_monotone2:
∀ lbl lbl1 lbl2, oHLleq lbl lbl1 → oHLleq lbl (ohlplus lbl1 lbl2).
Lemma is_normalO_monotone:
∀ lbl lbl' (LEQ: oHLleq lbl lbl'), is_normalO lbl → is_normalO lbl'.
Lemma normalO_ohlplus:
∀ lbl1 lbl2, is_normalO (ohlplus lbl1 lbl2) → is_normalO lbl1 ∨ is_normalO lbl2.
Lemma ohlplus_oHLleq:
∀ lbl1 lbl2 lbl, ohlplus lbl1 lbl2 = lbl → oHLleq lbl1 lbl ∧ oHLleq lbl2 lbl.
Lemma ohlplus_HLleq: ∀ lbl lbl' olbl, ohlplus (Some lbl) olbl = Some lbl' → HLleq lbl lbl'.
Lemma ohlplus_is_some:
∀ olbl1 olbl2 lbl,
ohlplus olbl1 olbl2 = Some lbl → ∃ lbl', (olbl1 = Some lbl' ∨ olbl2 = Some lbl') ∧ HLleq lbl' lbl.
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''.
Lemma label_hdef PS PSg:
∀ (hf : val → HeapVal PS PSg) g lbl, HFlabeled hf lbl ↔ Hlabeled (Hdef hf g) lbl.
Lemma label_exact_hdef PS PSg:
∀ (hf : val → HeapVal PS PSg) g lbl, HFlabeledExact hf lbl ↔ HlabeledExact (Hdef hf g) lbl.
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.
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.
Lemmas about heap similarity.
Lemma HLCsim_refl: ∀ lbl, HLCsim lbl lbl.
Lemma HLCsim_sym: ∀ lbl lbl', HLCsim lbl lbl' ↔ HLCsim lbl' lbl.
Lemma ohlplus_sim: ∀ lbl1 lbl2 lbl1' lbl2'
(SIM1: HLCsim lbl1 lbl1')
(SIM2: HLCsim lbl2 lbl2'),
HLCsim (ohlplus lbl1 lbl2) (ohlplus lbl1' lbl2').
Lemma HLCsim_trans lbl1 lbl2 lbl3: HLCsim lbl1 lbl2 → HLCsim lbl2 lbl3 → HLCsim lbl1 lbl3.
Lemma HVsim_refl PS PSg: ∀ (hv : HeapVal PS PSg), HVsim hv hv.
Lemma HVsim_sym PS PSg: ∀ (hv hv' : HeapVal PS PSg), HVsim hv hv' ↔ HVsim hv' hv.
Lemma HVsim_trans PS PSg (hv1 hv2 hv3 : HeapVal PS PSg): HVsim hv1 hv2 → HVsim hv2 hv3 → HVsim hv1 hv3.
Lemma HVsim_alloc PS PSg:
∀ (hv1 hv2 : HeapVal PS PSg) (SIM: HVsim hv1 hv2),
hv1 ≠ HVnone ↔ hv2 ≠ HVnone.
Lemma is_atomic_sim PS PSg: ∀ (hv hv' : HeapVal PS PSg) (SIM: HVsim hv hv'), is_atomic hv ↔ is_atomic hv'.
Lemma is_nonatomic_sim PS PSg:
∀ (hv hv' : HeapVal PS PSg) (SIM: HVsim hv hv'), is_nonatomic hv ↔ is_nonatomic hv'.
Lemma HFsim_refl PS PSg: ∀ (hf : val → HeapVal PS PSg), HFsim hf hf.
Lemma HFsim_sym PS PSg: ∀ (hf hf' : val → HeapVal PS PSg), HFsim hf hf' ↔ HFsim hf' hf.
Lemma HFsim_trans PS PSg (hf1 hf2 hf3 : val → HeapVal PS PSg): HFsim hf1 hf2 → HFsim hf2 hf3 → HFsim hf1 hf3.
Lemma Hsim_alt PS PSg: ∀ (hf hf' : val → HeapVal PS PSg) g, HFsim hf hf' ↔ Hsim (Hdef hf g) (Hdef hf' g).
Lemma Hsim_sym PS PSg: ∀ (h h' : heap PS PSg), Hsim h h' ↔ Hsim h' h.
Lemma Hsim_refl PS PSg: ∀ h, h ≠ @Hundef PS PSg → Hsim h h.
Lemma Hsim_trans PS PSg (h1 h2 h3 : heap PS PSg): Hsim h1 h2 → Hsim h2 h3 → Hsim h1 h3.
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.
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'.
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.
Lemma label_sim PS PSg:
∀ (hv1 hv2 : HeapVal PS PSg) (SIM: HVsim hv1 hv2) lbl (LBL: HVlabeled hv1 lbl),
∃ lbl', HVlabeled hv2 lbl'.
Lemma Rlabel_sim PS PSg:
∀ (hv1 hv2 : HeapVal PS PSg) (SIM: HVsim hv1 hv2) lbl (LBL: HVlabeledR hv1 lbl),
∃ lbl', HVlabeledR hv2 lbl'.
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'.
Lemma exact_label_sim PS PSg:
∀ (h1 h2 : heap PS PSg) lbl, HlabeledExact h1 lbl → HlabeledExact h2 lbl → Hsim h1 h2 → h1 = h2.
Some basic lemmas about heaps and hplus.
Lemma hdef_alt PS PSg h : h ≠ @Hundef PS PSg ↔ ∃ hf g, h = Hdef hf g.
Lemma AcombinableC PS PSg (P Q : assn PS PSg): Acombinable P Q → Acombinable Q P.
Lemma assn_mod_eqI1 PS PSg (P Q: assn_mod PS PSg): proj1_sig P = proj1_sig Q → P = Q.
Lemma assn_mod_eqI PS PSg (P Q: assn_mod PS PSg): Asim (sval P) (sval Q) → P = Q.
Lemma AsimD PS PSg (P Q : assn PS PSg) : Asim P Q → mk_assn_mod P = mk_assn_mod Q.
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.
Lemma hvplusDEFC PS PSg (hv1 hv2 : HeapVal PS PSg): hvplusDEF hv1 hv2 → hvplusDEF hv2 hv1.
Lemma hvplusC PS PSg (hv1 hv2 : HeapVal PS PSg): hvplusDEF hv1 hv2 → hvplus hv1 hv2 = hvplus hv2 hv1.
Lemma hplusC PS PSg (h1 h2 : heap PS PSg): hplus h1 h2 = hplus h2 h1.
Lemma hplus_emp_l PS PSg h : hplus (@hemp PS PSg) h = h.
Lemma hplus_emp_r PS PSg h : hplus h (@hemp PS PSg) = h.
Lemma hplus_eq_emp PS PSg (h1 h2 : heap PS PSg) :
hplus h1 h2 = (@hemp PS PSg) ↔ h1 = hemp ∧ h2 = hemp.
Lemma assn_norm_mod PS PSg (Q : assn_mod PS PSg) : assn_norm (sval Q) = sval Q.
Lemma hvplusDEF_hvplusA PS PSg (h1 h2 h3 : HeapVal PS PSg) :
hvplusDEF h1 h2 →
hvplusDEF (hvplus h1 h2) h3 →
hvplusDEF h1 (hvplus h2 h3).
Lemma hvplusDEF_hvplus1 PS PSg (h1 h2 h3 : HeapVal PS PSg) :
hvplusDEF h2 h3 →
hvplusDEF h1 (hvplus h2 h3) →
hvplusDEF h1 h2.
Lemma hvplusDEF_hvplus2 PS PSg (h1 h2 h3 : HeapVal PS PSg) :
hvplusDEF h1 h2 →
hvplusDEF (hvplus h1 h2) h3 →
hvplusDEF h2 h3.
Lemma hvplusA PS PSg (h1 h2 h3 : HeapVal PS PSg) :
hvplusDEF h1 h2 →
hvplus (hvplus h1 h2) h3 = hvplus h1 (hvplus h2 h3).
Lemma hplusA PS PSg (h1 h2 h3 : heap PS PSg) :
hplus (hplus h1 h2) h3 = hplus h1 (hplus h2 h3).
Lemma hplusAC PS PSg (h1 h2 h3 : heap PS PSg) :
hplus h2 (hplus h1 h3) = hplus h1 (hplus h2 h3).
Lemma hplus_add_same PS PSg: ∀ (h1 h2 h : heap PS PSg), h1 = h2 → hplus h1 h = hplus h2 h.
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).
Further properties of hplus
Lemma hplus_not_undef_l PS PSg h h' : hplus h h' ≠ @Hundef PS PSg → h ≠ @Hundef PS PSg.
Lemma hplus_not_undef_r PS PSg h h' : hplus h h' ≠ @Hundef PS PSg → h' ≠ @Hundef PS PSg.
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.
Lemma hplus_undef_l PS PSg: ∀ h, hplus (@Hundef PS PSg) h = @Hundef PS PSg.
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 >>.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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.
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).
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).
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).
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).
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)).
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.
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.
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).
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).
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).
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)).
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).
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).
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)).
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'.
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').
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.
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'.
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.
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.
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.
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.
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.
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'.
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.
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').
Lemma exact_label_hplus_dist PS PSg:
∀ (h1 h2: heap PS PSg) lbl, HlabeledExact (hplus h1 h2) lbl → HlabeledExact h1 lbl ∧ HlabeledExact h2 lbl.
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.
Lemma lupd_hplus_dist PS PSg:
∀ (h1 h2: heap PS PSg) lbl, lupd (hplus h1 h2) lbl = hplus (lupd h1 lbl) (lupd h2 lbl).
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'.
Lemmas about hsum
Lemma hsum_nil PS PSg : hsum nil = @hemp PS PSg.
Lemma hsum_cons PS PSg (a: heap PS PSg) l : hsum (a :: l) = hplus a (hsum l).
Lemma hsum_one PS PSg (h: heap PS PSg) : hsum (h :: nil) = h.
Lemma hsum_two PS PSg (h h': heap PS PSg) : hsum (h :: h' :: nil) = hplus h h'.
Lemma hsum_perm PS PSg (l l': list (heap PS PSg)) : Permutation l l' → hsum l = hsum l'.
Lemma hsum_app PS PSg (l l': list (heap PS PSg)) : hsum (l ++ l') = hplus (hsum l) (hsum l').
Lemma hsum_undef PS PSg: ∀ hlist, In (@Hundef PS PSg) hlist → hsum hlist = @Hundef PS PSg.
Lemma hsum_eq_emp PS PSg: ∀ hlist, hsum hlist = @hemp PS PSg ↔ ∀ h (IN: In h hlist), h = hemp.
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'.
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.
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.
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.
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.
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.
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.
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.
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.
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).
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).
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).
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).
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).
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).
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).
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.
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.
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.
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'.
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.
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.
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.
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.
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.
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'.
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').
Lemmas about initialize
Lemma initialize_alloc PS PSg: ∀ hf l l', hf l ≠ @HVnone PS PSg ↔ initialize hf l' l ≠ @HVnone PS PSg.
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.
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'.
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'.
Lemma initialize_is_rvalue PS PSg:
∀ (hf : val → HeapVal PS PSg) l l', is_rvalue (initialize hf l l') → is_rvalue (hf l').
Lemma initialize_is_lvalue PS PSg:
∀ (hf : val → HeapVal PS PSg) l l', is_lvalue (initialize hf l l') → is_lvalue (hf l').
Lemma initialize_is_atomic PS PSg:
∀ (hf : val → HeapVal PS PSg) l l', is_atomic (initialize hf l l') → is_atomic (hf l').
Lemma initialize_is_nonatomic PS PSg:
∀ (hf : val → HeapVal PS PSg) l l', is_nonatomic (initialize hf l l') → is_nonatomic (hf l').
Lemma initialize_preserves_label PS PSg:
∀ (hf : val → HeapVal PS PSg) l l' lbl, HVlabeled (hf l) lbl → HVlabeled (initialize hf l' l) lbl.
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.
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.
Lemmas about assertions
Lemma assn_sem_def PS PSg P h : assn_sem P h → h ≠ @Hundef PS PSg.
Lemma sim_assn_sem PS PSg:
∀ (p p': assn PS PSg) (S: Asim p p') h, assn_sem p h ↔ assn_sem p' h.
Lemma assn_sem_satD PS PSg (Q: assn PS PSg) h : assn_sem Q h → ∃ hf g, h = Hdef hf g.
Lemma precise_emp PS PSg : precise (@Aemp PS PSg).
Lemma precise_star PS PSg (P Q: assn PS PSg) : precise P → precise Q → precise (Astar P Q).
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.
Lemma assn_sem_exists PS PSg PP (h: heap PS PSg) :
assn_sem (Aexists PP) h ↔ ∃ x, assn_sem (PP x) h.
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.
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).
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').
Lemma implies_trans PS PSg (P Q R: assn PS PSg): implies P Q ∧ implies Q R → implies P R.
Lemma implies_frame PS PSg (P Q F: assn PS PSg): implies P Q → implies (Astar P F) (Astar Q F).
Lemma assn_sem_assn_norm PS PSg (P: assn PS PSg) h: assn_sem (assn_norm P) h ↔ assn_sem P h.
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.
Lemma precise_assn_norm PS PSg (P: assn PS PSg): precise P ↔ precise (assn_norm P).
Lemma normalizable_star PS PSg (P Q: assn PS PSg) :
normalizable P → normalizable Q → normalizable (Astar P Q).
Lemma normalizable_assn_norm PS PSg (P: assn PS PSg): normalizable P ↔ normalizable (assn_norm P).
Lemma normalizable_emp PS PSg: normalizable (@Aemp PS PSg).
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)).
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)).
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))))).
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))))).
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).
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) >>.
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))).
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).
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).
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'.
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'.
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.
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.
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.
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.
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.
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)).
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)).
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')).
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))).
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))).
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).
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).
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).
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).
Lemma is_nonatomic_initialize PS PSg :
∀ (hf: val → HeapVal PS PSg) l l', is_nonatomic (hf l) → is_nonatomic (initialize hf l' l).
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.
Lemma is_nonatomic_hsim PS PSg :
∀ (hf1 hf2: val → HeapVal PS PSg) l, HFsim hf1 hf2 → (is_nonatomic (hf1 l) ↔ is_nonatomic (hf2 l)).
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.
Opaque hplus.
This page has been generated by coqdoc