Require Import List Vbase Varith Vlist extralib.
Require Import Classical ClassicalDescription IndefiniteDescription.
Require Import Permutation fslassn.
Set Implicit Arguments.
Transparent hplus.
Simple lemmas about values and labels.
Lemma has_value_alt hv v: has_value hv v ↔ ∃ lbl, hv = HVval v lbl.
Lemma has_value_sim hv hv´ v (SIM: HVsim hv hv´): has_value hv v ↔ has_value hv´ v.
Lemma is_val_implies_is_nonatomic hv: is_val hv → is_nonatomic hv.
Lemma is_val_implies_normal hv: is_val hv → HVlabeled hv HLnormal.
Hint Resolve is_val_implies_is_nonatomic is_val_implies_normal.
Simple lemmas about lupd.
Lemma lupd_sim:
∀ h lbl, h ≠ Hundef → Hsim h (lupd h lbl).
Lemma lupd_label:
∀ h lbl, h ≠ Hundef → HlabeledExact (lupd h lbl) lbl.
Lemma lupd_eq: ∀ h h´ lbl (SIM: Hsim h h´) (LBL: HlabeledExact h lbl), h = lupd h´ lbl.
Lemma lupd_eq_lupd: ∀ h h´ lbl (DEF: h ≠ Hundef) (EQ: lupd h lbl = lupd h´ lbl), Hsim h h´.
Lemmas about heap labels and hlplus.
Lemma Wlabel_implies_label: ∀ hv lbl, HVlabeledW hv lbl → HVlabeled hv lbl.
Lemma Rlabel_implies_label: ∀ hv lbl, HVlabeledR hv lbl → HVlabeled hv lbl.
Lemma label_is_consistent_with_exact_label:
∀ hv (N: hv ≠ HVnone) lbl lbl´ (LAB: HVlabeled hv lbl) (LABx: HVlabeledExact hv lbl´), lbl = lbl´.
Lemma Rlabel_is_consistent_with_exact_label:
∀ hv lbl lbl´ (LAB: HVlabeledR hv lbl) (LABx: HVlabeledExact hv lbl´), lbl = lbl´.
Lemma Wlabel_is_consistent_with_exact_label:
∀ hv lbl lbl´ (LAB: HVlabeledW hv lbl) (LABx: HVlabeledExact hv lbl´), lbl = lbl´.
Lemma nonatomic_label:
∀ hv (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:
∀ hf lbl, HFlabeled hf lbl ↔ Hlabeled (Hdef hf) lbl.
Lemma label_exact_hdef:
∀ hf lbl, HFlabeledExact hf lbl ↔ HlabeledExact (Hdef hf) lbl.
Lemma label_hvplus:
∀ hv1 hv2 lbl
(DEF: hvplusDEF hv1 hv2)
(PLUS: HVlabeled (hvplus hv1 hv2) lbl),
HVlabeled hv1 lbl ∨ HVlabeled hv2 lbl.
Lemma Rlabel_hvplus:
∀ hv1 hv2 lbl
(DEF: hvplusDEF hv1 hv2)
(PLUS: HVlabeledR (hvplus hv1 hv2) lbl),
HVlabeledR hv1 lbl ∨ HVlabeledR hv2 lbl.
Lemma Wlabel_hvplus:
∀ hv1 hv2 lbl
(DEF: hvplusDEF hv1 hv2)
(PLUS: HVlabeledW (hvplus hv1 hv2) lbl),
HVlabeledW hv1 lbl ∨ HVlabeledW 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: ∀ hv, HVsim hv hv.
Lemma HVsim_sym: ∀ hv hv´, HVsim hv hv´ ↔ HVsim hv´ hv.
Lemma HVsim_trans hv1 hv2 hv3: HVsim hv1 hv2 → HVsim hv2 hv3 → HVsim hv1 hv3.
Lemma HVsim_alloc: ∀ hv1 hv2 (SIM: HVsim hv1 hv2), hv1 ≠ HVnone ↔ hv2 ≠ HVnone.
Lemma is_atomic_sim: ∀ hv hv´ (SIM: HVsim hv hv´), is_atomic hv ↔ is_atomic hv´.
Lemma is_nonatomic_sim: ∀ hv hv´ (SIM: HVsim hv hv´), is_nonatomic hv ↔ is_nonatomic hv´.
Lemma HFsim_refl: ∀ hf, HFsim hf hf.
Lemma HFsim_sym: ∀ hf hf´, HFsim hf hf´ ↔ HFsim hf´ hf.
Lemma HFsim_trans hf1 hf2 hf3: HFsim hf1 hf2 → HFsim hf2 hf3 → HFsim hf1 hf3.
Lemma Hsim_alt: ∀ hf hf´, HFsim hf hf´ ↔ Hsim (Hdef hf) (Hdef hf´).
Lemma Hsim_sym: ∀ h h´, Hsim h h´ ↔ Hsim h´ h.
Lemma Hsim_refl: ∀ h, h ≠ Hundef → Hsim h h.
Lemma Hsim_trans h1 h2 h3: Hsim h1 h2 → Hsim h2 h3 → Hsim h1 h3.
Lemma Hsim_alloc:
∀ h hf l
(SIM: Hsim h (Hdef hf))
(DEF: hf l ≠ HVnone),
∃ hf´, h = Hdef hf´ ∧ hf´ l ≠ HVnone.
Lemma label_sim:
∀ hv1 hv2 (SIM: HVsim hv1 hv2) lbl (LBL: HVlabeled hv1 lbl),
∃ lbl´, HVlabeled hv2 lbl´.
Lemma Rlabel_sim:
∀ hv1 hv2 (SIM: HVsim hv1 hv2) lbl (LBL: HVlabeledR hv1 lbl),
∃ lbl´, HVlabeledR hv2 lbl´.
Lemma Wlabel_sim:
∀ hv1 hv2 (SIM: HVsim hv1 hv2) lbl (LBL: HVlabeledW hv1 lbl),
∃ lbl´, HVlabeledW hv2 lbl´.
Lemma exact_label_sim:
∀ h1 h2 lbl, HlabeledExact h1 lbl → HlabeledExact h2 lbl → Hsim h1 h2 → h1 = h2.
Some basic lemmas about heaps and hplus.
Lemma hdef_alt h : h ≠ Hundef ↔ ∃ hf, h = Hdef hf.
Lemma AcombinableC P Q: Acombinable P Q → Acombinable Q P.
Lemma assn_mod_eqI1 (P Q: assn_mod): proj1_sig P = proj1_sig Q → P = Q.
Lemma assn_mod_eqI (P Q: assn_mod): Asim (sval P) (sval Q) → P = Q.
Lemma AsimD P Q : Asim P Q → mk_assn_mod P = mk_assn_mod Q.
Lemma hv_acq_defC b1 Q1 b2 Q2 :
hv_acq_def b1 Q1 b2 Q2 → hv_acq_def b2 Q2 b1 Q1.
Lemma hvplusDEFC hv1 hv2: hvplusDEF hv1 hv2 → hvplusDEF hv2 hv1.
Lemma hvplusC hv1 hv2: hvplusDEF hv1 hv2 → hvplus hv1 hv2 = hvplus hv2 hv1.
Lemma hplusC h1 h2: hplus h1 h2 = hplus h2 h1.
Lemma hplus_emp_l h : hplus hemp h = h.
Lemma hplus_emp_r h : hplus h hemp = h.
Lemma hplus_eq_emp h1 h2 : hplus h1 h2 = hemp ↔ h1 = hemp ∧ h2 = hemp.
Lemma assn_norm_mod (Q : assn_mod) : assn_norm (sval Q) = sval Q.
Lemma hvplusDEF_hvplusA h1 h2 h3 :
hvplusDEF h1 h2 →
hvplusDEF (hvplus h1 h2) h3 →
hvplusDEF h1 (hvplus h2 h3).
Lemma hvplusDEF_hvplus1 h1 h2 h3 :
hvplusDEF h2 h3 →
hvplusDEF h1 (hvplus h2 h3) →
hvplusDEF h1 h2.
Lemma hvplusDEF_hvplus2 h1 h2 h3 :
hvplusDEF h1 h2 →
hvplusDEF (hvplus h1 h2) h3 →
hvplusDEF h2 h3.
Lemma hvplusA h1 h2 h3 :
hvplusDEF h1 h2 →
hvplus (hvplus h1 h2) h3 = hvplus h1 (hvplus h2 h3).
Lemma hplusA h1 h2 h3 :
hplus (hplus h1 h2) h3 = hplus h1 (hplus h2 h3).
Lemma hplusAC h1 h2 h3 :
hplus h2 (hplus h1 h3) = hplus h1 (hplus h2 h3).
Lemma hplus_add_same: ∀ h1 h2 h, h1 = h2 → hplus h1 h = hplus h2 h.
Lemma hplus_unfold h1 h2 :
hplus (Hdef h1) (Hdef h2) =
(if excluded_middle_informative (∀ v : val, hvplusDEF (h1 v) (h2 v))
then Hdef (fun v : val ⇒ hvplus (h1 v) (h2 v))
else Hundef).
Further properties of hplus
Lemma hplus_not_undef_l h h´ : hplus h h´ ≠ Hundef → h ≠ Hundef.
Lemma hplus_not_undef_r h h´ : hplus h h´ ≠ Hundef → h´ ≠ Hundef.
Hint Resolve hplus_not_undef_l.
Hint Resolve hplus_not_undef_r.
Lemma hplus_undef_r: ∀ h, hplus h Hundef = Hundef.
Lemma hplus_undef_l: ∀ h : heap, hplus Hundef h = Hundef.
Lemma hplus_def_inv h h´ hx (P: hplus h h´ = Hdef hx) :
∃ hy hz, h = Hdef hy ∧ h´ = Hdef hz
∧ << DEFv: ∀ l, hvplusDEF (hy l) (hz l) >>
∧ << PLUSv: ∀ l, hx l = hvplus (hy l) (hz l) >>.
Lemma hplus_def_inv_l h h´ hf : hplus h h´ = Hdef hf → ∃ h3, h = Hdef h3.
Lemma hplus_def_inv_r h h´ hf : hplus h h´ = Hdef hf → ∃ h3, h´ = Hdef h3.
Lemma hplus_preserves_alloc_l:
∀ h1 h2 h l (SUM: Hdef h = hplus (Hdef h1) h2 ) (ALL: h1 l ≠ HVnone), h l ≠ HVnone.
Lemma hplus_preserves_alloc_r:
∀ h1 h2 h l (SUM: Hdef h = hplus h1 (Hdef h2)) (ALL: h2 l ≠ HVnone), h l ≠ HVnone.
Lemma hplus_alloc h1 h2 h l :
hplus h1 h2 = Hdef h →
h l ≠ HVnone →
∃ h´, h1 = Hdef h´ ∧ h´ l ≠ HVnone ∨ h2 = Hdef h´ ∧ h´ l ≠ HVnone.
Lemma hplus_nalloc h1 h2 h loc :
Hdef h = hplus h1 h2 →
h loc = HVnone →
∃ h1f h2f, Hdef h1f = h1 ∧ h1f loc = HVnone ∧ Hdef h2f = h2 ∧ h2f loc = HVnone.
Lemma hplus_nalloc_sim h1 h2 h loc :
Hsim (Hdef h) (hplus h1 h2) →
h loc = HVnone →
∃ h1f h2f, Hdef h1f = h1 ∧ h1f loc = HVnone ∧ Hdef h2f = h2 ∧ h2f loc = HVnone.
Lemma hplus_nalloc_spec: ∀ h h1 h2 l
(SUM: hplus (Hdef h1) (Hdef h2) = Hdef h)
(NONEres: h l = HVnone),
h1 l = HVnone ∧ h2 l = HVnone.
Lemma hplus_has_val_l :
∀ h h1 h2 l,
hplus h1 h2 = Hdef h →
(∀ h´´, h1 = Hdef h´´ → is_val (h´´ l)) →
is_val (h l).
Lemma hplus_has_val_r :
∀ h h1 h2 l,
hplus h1 h2 = Hdef h →
(∀ h´´, h2 = Hdef h´´ → is_val (h´´ l)) →
is_val (h l).
Lemma hplus_is_val :
∀ h h1 h2 l,
hplus h1 h2 = Hdef h →
is_val (h l) →
∃ hf1 hf2,
h1 = Hdef hf1 ∧ h2 = Hdef hf2 ∧ (is_val (hf1 l) ∨ is_val (hf2 l)).
Lemma hplus_val_lD:
∀ hf h1 h2 l v lbl,
Hdef hf = hplus h1 h2 →
(∀ hf´´, Hdef hf´´ = h1 → hf´´ l = HVval v lbl) →
hf l = HVval v lbl.
Lemma hplus_val_lD_weak:
∀ hf h1 h2 l v,
Hdef hf = hplus h1 h2 →
(∀ hf´´, Hdef hf´´ = h1 → has_value (hf´´ l) v) →
has_value (hf l) v.
Lemma hplus_val_rD:
∀ hf h1 h2 l v lbl,
Hdef hf = hplus h1 h2 →
(∀ hf´´, Hdef hf´´ = h2 → hf´´ l = HVval v lbl) →
hf l = HVval v lbl.
Lemma hplus_val_rD_weak:
∀ hf h1 h2 l v,
Hdef hf = hplus h1 h2 →
(∀ hf´´, Hdef hf´´ = h2 → has_value (hf´´ l) v) →
has_value (hf l) v.
Lemma hplus_valD:
∀ hf h1 h2 l v lbl,
hplus h1 h2 = Hdef hf →
hf l = HVval v lbl →
∃ hf1 hf2, h1 = Hdef hf1 ∧ h2 = Hdef hf2 ∧ (hf1 l = HVval v lbl ∨ hf2 l = HVval v lbl).
Lemma hplus_valD_weak:
∀ hf h1 h2 l v,
hplus h1 h2 = Hdef hf →
has_value (hf l) v →
∃ hf1 hf2, h1 = Hdef hf1 ∧ h2 = Hdef hf2 ∧ (has_value (hf1 l) v ∨ has_value (hf2 l) v).
Lemma hplus_uval_lD:
∀ hf h1 h2 l lbl,
Hdef hf = hplus h1 h2 →
(∀ hf´´, Hdef hf´´ = h1 → hf´´ l = HVuval lbl) →
hf l = HVuval lbl.
Lemma hplus_uval_rD:
∀ hf h1 h2 l lbl,
Hdef hf = hplus h1 h2 →
(∀ hf´´, Hdef hf´´ = h2 → hf´´ l = HVuval lbl) →
hf l = HVuval lbl.
Lemma hplus_uvalD:
∀ hf h1 h2 l lbl,
hplus h1 h2 = Hdef hf →
hf l = HVuval lbl →
∃ hf1 hf2, h1 = Hdef hf1 ∧ h2 = Hdef hf2 ∧ (hf1 l = HVuval lbl ∨ hf2 l = HVuval lbl).
Lemma hplus_has_atomic_l :
∀ h h1 h2 l,
hplus h1 h2 = Hdef h →
(∀ h´´, h1 = Hdef h´´ → is_atomic (h´´ l)) →
is_atomic (h l).
Lemma hplus_has_atomic_r :
∀ h h1 h2 l,
hplus h1 h2 = Hdef h →
(∀ h´´, h2 = Hdef h´´ → is_atomic (h´´ l)) →
is_atomic (h l).
Lemma hplus_is_atomic :
∀ h h1 h2 l,
hplus h1 h2 = Hdef h →
is_atomic (h l) →
∃ hf1 hf2,
h1 = Hdef hf1 ∧ h2 = Hdef hf2 ∧ (is_atomic (hf1 l) ∨ is_atomic (hf2 l)).
Lemma hplus_has_nonatomic_l :
∀ h h1 h2 l,
hplus h1 h2 = Hdef h →
(∀ h´´, h1 = Hdef h´´ → is_nonatomic (h´´ l)) →
is_nonatomic (h l).
Lemma hplus_has_nonatomic_r :
∀ h h1 h2 l,
hplus h1 h2 = Hdef h →
(∀ h´´, h2 = Hdef h´´ → is_nonatomic (h´´ l)) →
is_nonatomic (h l).
Lemma hplus_is_nonatomic :
∀ h h1 h2 l,
hplus h1 h2 = Hdef h →
is_nonatomic (h l) →
∃ hf1 hf2,
h1 = Hdef hf1 ∧ h2 = Hdef hf2 ∧ (is_nonatomic (hf1 l) ∨ is_nonatomic (hf2 l)).
Lemma hplus_eq_ra_initD:
∀ h h1 h2 l PP QQ perm isrmw init,
hplus h1 h2 = Hdef h →
h l = HVra PP QQ isrmw perm init →
is_normalO init →
∃ hf PP´ QQ´ perm´ isrmw´ init´,
(h1 = Hdef hf ∨ h2 = Hdef hf) ∧ hf l = HVra PP´ QQ´ isrmw´ perm´ init´ ∧ is_normalO init´.
Lemma hplus_hsingl: ∀ l hv hv´ (DEFv: hvplusDEF hv hv´),
hplus (hsingl l hv) (hsingl l hv´) = hsingl l (hvplus hv hv´).
Definition hvplus_ra_ret hv QQ´ :=
match hv with
| HVnone ⇒ False
| HVuval _ ⇒ False
| HVval _ _ ⇒ False
| HVra _ QQ _ _ _ ⇒ QQ = QQ´
end.
Lemma hvplus_ra_ret_initialize: ∀ h l l´ QQ,
hvplus_ra_ret (h l) QQ ↔ hvplus_ra_ret (initialize h l´ l) QQ.
Definition hvplus_ra2_ret hv (QQ´ : val → assn_mod) :=
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 hv hv´ PP´ QQ´ perm´ isrmw´ init´:
hv = HVra PP´ QQ´ isrmw´ perm´ init´ →
hvplusDEF hv hv´ →
hvplus_ra2_ret (hvplus hv hv´) QQ´.
Lemma hplus_preserves_label: ∀ hf hf1 h2 l lbl
(SUM: Hdef hf = hplus (Hdef hf1) h2)
(LABEL: HVlabeled (hf1 l) lbl)
(DEF: hf1 l ≠ HVnone),
hf l ≠ HVnone ∧ HVlabeled (hf l) lbl.
Lemma hplus_preserves_Rlabel: ∀ hf hf1 h2 l lbl
(SUM: Hdef hf = hplus (Hdef hf1) h2)
(LABEL: HVlabeledR (hf1 l) lbl),
HVlabeledR (hf l) lbl.
Lemma hplus_preserves_Wlabel: ∀ hf hf1 h2 l lbl
(SUM: Hdef hf = hplus (Hdef hf1) h2)
(LABEL: HVlabeledW (hf1 l) lbl),
HVlabeledW (hf l) lbl.
Lemma hplus_preserves_label_inv:
∀ hf h1 h2 l lbl
(SUM: hplus h1 h2 = Hdef hf)
(LABEL: HVlabeled (hf l) lbl)
(ALL: hf l ≠ HVnone),
∃ hf´, (h1 = Hdef hf´ ∨ h2 = Hdef hf´) ∧ HVlabeled (hf´ l) lbl ∧ hf´ l ≠ HVnone.
Lemma hplus_preserves_Rlabel_inv:
∀ hf h1 h2 l lbl
(SUM: hplus h1 h2 = Hdef hf)
(LABEL: HVlabeledR (hf l) lbl),
∃ hf´, (h1 = Hdef hf´ ∨ h2 = Hdef hf´) ∧ HVlabeledR (hf´ l) lbl.
Lemma hplus_preserves_Wlabel_inv:
∀ hf h1 h2 l lbl
(SUM: hplus h1 h2 = Hdef hf)
(LABEL: HVlabeledW (hf l) lbl),
∃ hf´, (h1 = Hdef hf´ ∨ h2 = Hdef hf´) ∧ HVlabeledW (hf´ l) lbl.
Lemma hplus_alloc_label:
∀ h1 h2 h l lbl
(SUM: hplus h1 h2 = Hdef h)
(DEF: h l ≠ HVnone)
(LABEL: HVlabeled (h l) lbl),
∃ h´, h1 = Hdef h´ ∧ h´ l ≠ HVnone ∧ HVlabeled (h´ l) lbl ∨
h2 = Hdef h´ ∧ h´ l ≠ HVnone ∧ HVlabeled (h´ l) lbl.
Lemma hplus_sim_def: ∀ h h1 h2 (SIM: Hsim h1 h2) (DEF: hplus h1 h ≠ Hundef), hplus h2 h ≠ Hundef.
Lemma hplus_sim: ∀ h1 h2 h1´ h2´
(SIM1: Hsim h1 h1´)
(SIM2: Hsim h2 h2´)
(DEF: hplus h1 h2 ≠ Hundef),
Hsim (hplus h1 h2) (hplus h1´ h2´).
Lemma exact_label_hplus_dist:
∀ h1 h2 lbl, HlabeledExact (hplus h1 h2) lbl → HlabeledExact h1 lbl ∧ HlabeledExact h2 lbl.
Lemma exact_label_hplus_dist_inv:
∀ h1 h2 lbl
(DEF: hplus h1 h2 ≠ Hundef)
(L1: HlabeledExact h1 lbl)
(L2: HlabeledExact h2 lbl),
HlabeledExact (hplus h1 h2) lbl.
Lemma lupd_hplus_dist:
∀ h1 h2 lbl, lupd (hplus h1 h2) lbl = hplus (lupd h1 lbl) (lupd h2 lbl).
Lemmas about hsum
Lemma hsum_nil : hsum nil = hemp.
Lemma hsum_cons a l : hsum (a :: l) = hplus a (hsum l).
Lemma hsum_one h : hsum (h :: nil) = h.
Lemma hsum_two h h´ : hsum (h :: h´ :: nil) = hplus h h´.
Lemma hsum_perm l l´ : Permutation l l´ → hsum l = hsum l´.
Lemma hsum_app l l´ : hsum (l ++ l´) = hplus (hsum l) (hsum l´).
Lemma hsum_eq_emp: ∀ hlist, hsum hlist = hemp ↔ ∀ h (IN: In h hlist), h = hemp.
Lemma hsum_def_inv: ∀ hlist hf (SUM: hsum hlist = Hdef hf),
∀ h (IN: In h hlist), ∃ hf´, h = Hdef hf´.
Lemma hsum_alloc l h loc :
hsum l = Hdef h →
h loc ≠ HVnone →
∃ h´, In (Hdef h´) l ∧ h´ loc ≠ HVnone.
Lemma hsum_alloc_sim l h loc :
Hsim (hsum l) (Hdef h) →
h loc ≠ HVnone →
∃ h´, In (Hdef h´) l ∧ h´ loc ≠ HVnone.
Lemma hsum_nalloc hs hf h loc :
Hdef hf = hsum hs →
hf loc = HVnone →
In h hs →
∃ hf, Hdef hf = h ∧ hf loc = HVnone.
Lemma hsum_nalloc_all: ∀ hlist hf l
(SUM: hsum hlist = Hdef hf)
(NALLOC: hf l = HVnone),
∀ h (IN: In h hlist), ∃ hf´, h = Hdef hf´ ∧ hf´ l = HVnone.
Lemma hsum_preserves_alloc:
∀ hs hf (SUM: hsum hs = Hdef hf) hf´ (IN: In (Hdef hf´) hs) l (ALL: hf´ l ≠ HVnone),
hf l ≠ HVnone.
Lemma hsum_none: ∀ hlist hf (SUM: hsum hlist = Hdef hf)
l (NONE: ∀ hf´ (IN: In (Hdef hf´) hlist), hf´ l = HVnone),
hf l = HVnone.
Lemma hsum_has_val :
∀ h hs h´´ l,
hsum hs = Hdef h →
In (Hdef h´´) hs →
is_val (h´´ l) →
is_val (h l).
Lemma hsum_is_val :
∀ hs h l,
hsum hs = Hdef h →
is_val (h l) →
∃ hf, In (Hdef hf) hs ∧ is_val (hf l).
Lemma hsum_is_atomic :
∀ hs h l,
hsum hs = Hdef h →
is_atomic (h l) →
∃ hf, In (Hdef hf) hs ∧ is_atomic (hf l).
Lemma hsum_has_atomic: ∀ hs hf l (SUM: hsum hs = Hdef hf)
hf´ (IN: In (Hdef hf´) hs) (NAT: is_atomic (hf´ l)),
is_atomic (hf l).
Lemma hsum_is_nonatomic :
∀ hs h l,
hsum hs = Hdef h →
is_nonatomic (h l) →
∃ hf, In (Hdef hf) hs ∧ is_nonatomic (hf l).
Lemma hsum_has_nonatomic: ∀ hs hf l (SUM: hsum hs = Hdef hf)
hf´ (IN: In (Hdef hf´) hs) (NAT: is_nonatomic (hf´ l)),
is_nonatomic (hf l).
Lemma hsum_valD :
∀ hf hs h´´ l v lbl,
hsum hs = Hdef hf →
In (Hdef h´´) hs →
h´´ l = HVval v lbl →
hf l = HVval v lbl.
Lemma hsum_valD_weak :
∀ hf hs h´´ l v,
hsum hs = Hdef hf →
In (Hdef h´´) hs →
has_value (h´´ l) v →
has_value (hf l) v.
Lemma hsum_eq_val :
∀ hs hf l v lbl,
hsum hs = Hdef hf →
hf l = HVval v lbl →
∃ hf, In (Hdef hf) hs ∧ hf l = HVval v lbl.
Lemma hsum_eq_val_weak :
∀ hs hf l v,
hsum hs = Hdef hf →
has_value (hf l) v →
∃ hf, In (Hdef hf) hs ∧ has_value (hf l) v.
Lemma hsum_eq_ra_initD:
∀ h´ hs l PP QQ isrmw perm init,
hsum hs = Hdef h´ →
h´ l = HVra PP QQ isrmw perm init →
is_normalO init →
∃ h´´ PP´ QQ´ isrmw´ perm´ init´,
In (Hdef h´´) hs ∧
h´´ l = HVra PP´ QQ´ isrmw´ perm´ init´ ∧ is_normalO init´.
Lemma hsum_preserves_label:
∀ hs hf hf´ l lbl
(SUM: Hdef hf = hsum hs)
(IN: In (Hdef hf´) hs)
(LABEL: HVlabeled (hf´ l) lbl)
(DEF: hf´ l ≠ HVnone),
hf l ≠ HVnone ∧ HVlabeled (hf l) lbl.
Lemma hsum_preserves_Rlabel:
∀ hs hf hf´ l lbl
(SUM: Hdef hf = hsum hs)
(IN: In (Hdef hf´) hs)
(LABEL: HVlabeledR (hf´ l) lbl),
HVlabeledR (hf l) lbl.
Lemma hsum_preserves_Wlabel:
∀ hs hf hf´ l lbl
(SUM: Hdef hf = hsum hs)
(IN: In (Hdef hf´) hs)
(LABEL: HVlabeledW (hf´ l) lbl),
HVlabeledW (hf l) lbl.
Lemma hsum_preserves_label_inv:
∀ hs hf l lbl
(SUM: Hdef hf = hsum hs)
(LABEL: HVlabeled (hf l) lbl)
(ALL: hf l ≠ HVnone),
∃ hf´, In (Hdef hf´) hs ∧ HVlabeled (hf´ l) lbl ∧ hf´ l ≠ HVnone.
Lemma hsum_preserves_Rlabel_inv:
∀ hs hf l lbl
(SUM: Hdef hf = hsum hs)
(LABEL: HVlabeledR (hf l) lbl),
∃ hf´, In (Hdef hf´) hs ∧ HVlabeledR (hf´ l) lbl.
Lemma hsum_preserves_Wlabel_inv:
∀ hs hf l lbl
(SUM: Hdef hf = hsum hs)
(LABEL: HVlabeledW (hf l) lbl),
∃ hf´, In (Hdef hf´) hs ∧ HVlabeledW (hf´ l) lbl.
Lemma hsum_alloc_label:
∀ hs h l lbl
(SUM: hsum hs = Hdef h)
(DEF: h l ≠ HVnone)
(LABEL: HVlabeled (h l) lbl),
∃ h´, In (Hdef h´) hs ∧ h´ l ≠ HVnone ∧ HVlabeled (h´ l) lbl.
Lemma hdef_upd_alloc hf l v´ h h´ lbl :
is_val (hf l) →
hplus (Hdef hf) h = Hdef h´ →
∃ h´´, hplus (Hdef (hupd hf l (HVval v´ lbl))) h = Hdef h´´.
Lemma hdef_upd_alloc2 hf l v´ h h´ lbl :
is_val (hf l) →
hplus (Hdef hf) h = Hdef h´ →
∃ h´´,
hplus (Hdef (hupd hf l (HVval v´ lbl))) h = Hdef h´´
∧ (∀ l´ (NEQ: l´ ≠ l), h´´ l´ = h´ l´).
Lemmas about initialize
Lemma initialize_alloc: ∀ hf l l´, hf l ≠ HVnone ↔ initialize hf l´ l ≠ HVnone.
Lemma hplus_init_def hf l h h´ :
hplus (Hdef hf) h = Hdef h´ →
hplus (Hdef (initialize hf l)) h ≠ Hundef.
Lemma hplus_init_def2 hf l h h´ :
hplus (Hdef hf) h = Hdef h´ →
hf l ≠ HVnone →
hplus (Hdef (initialize hf l)) h = Hdef (initialize h´ l).
Lemma initialize_eq_raD hf l l´ PP QQ isrmw perm init:
initialize hf l l´ = HVra PP QQ isrmw perm init →
∃ init´, hf l´ = HVra PP QQ isrmw perm init´.
Lemma initialize_is_val: ∀ hf l l´, is_val (initialize hf l l´) → is_val (hf l´).
Lemma initialize_is_atomic: ∀ hf l l´, is_atomic (initialize hf l l´) → is_atomic (hf l´).
Lemma initialize_is_nonatomic: ∀ hf l l´, is_nonatomic (initialize hf l l´) → is_nonatomic (hf l´).
Lemma initialize_preserves_label:
∀ hf l l´ lbl, is_nonatomic (hf l) → HVlabeled (hf l) lbl → HVlabeled (initialize hf l´ l) lbl.
Lemma initialize_Wlabel: ∀ hf l l´ lbl, HVlabeledW (initialize hf l l´) lbl ↔ HVlabeledW (hf l´) lbl.
Lemma initialize_not_normal:
∀ hf l l´ lbl (LAB: HVlabeled (initialize hf l´ l) lbl) (N: lbl ≠ HLnormal), HVlabeled (hf l ) lbl.
Lemma initialize_not_normalR:
∀ hf l l´ lbl (LAB: HVlabeledR (initialize hf l´ l) lbl) (N: lbl ≠ HLnormal), HVlabeledR (hf l ) lbl.
Lemma initialize_not_normalW:
∀ hf l l´ lbl (LAB: HVlabeledW (initialize hf l´ l) lbl) (N: lbl ≠ HLnormal), HVlabeledW (hf l ) lbl.
Lemmas about assertions
Lemma assn_sem_def P h : assn_sem P h → h ≠ Hundef.
Lemma sim_assn_sem :
∀ p p´ (S: Asim p p´) h, assn_sem p h ↔ assn_sem p´ h.
Lemma assn_sem_satD Q h : assn_sem Q h → ∃ hf, h = Hdef hf.
Lemma precise_emp : precise Aemp.
Lemma precise_star P Q : precise P → precise Q → precise (Astar P Q).
Hint Resolve precise_emp precise_star.
Lemma assn_sem_disj P Q h :
assn_sem (Adisj P Q) h ↔ assn_sem P h ∨ assn_sem Q h.
Lemma assn_sem_exists PP h :
assn_sem (Aexists PP) h ↔ ∃ x, assn_sem (PP x) h.
Lemma foldr_star_perm :
∀ l l´ (P: Permutation l l´) init h,
assn_sem (foldr Astar l init) h →
assn_sem (foldr Astar l´ init) h.
Lemma foldr_star_perm2 :
∀ l l´ (P: Permutation l l´) init,
Asim (foldr Astar l init) (foldr Astar l´ init).
Lemma assn_sem_foldr_true_ext A (f: A → assn) l h h´ :
assn_sem (foldr Astar (List.map f l) Atrue) h →
hplus h h´ ≠ Hundef →
assn_sem (foldr Astar (List.map f l) Atrue) (hplus h h´).
Lemma implies_trans: ∀ P Q R, implies P Q ∧ implies Q R → implies P R.
Lemma implies_frame: ∀ P Q F, implies P Q → implies (Astar P F) (Astar Q F).
Lemma assn_sem_assn_norm: ∀ P h, assn_sem (assn_norm P) h ↔ assn_sem P h.
Lemma nabla_star_dist:
∀ h P Q, assn_sem (Anabla (Astar P Q)) h ↔ assn_sem (Astar (Anabla P) (Anabla Q)) h.
Lemma precise_assn_norm: ∀ P, precise P ↔ precise (assn_norm P).
Lemma normalizable_star P Q: normalizable P → normalizable Q → normalizable (Astar P Q).
Lemma normalizable_assn_norm: ∀ P, normalizable P ↔ normalizable (assn_norm P).
Lemma normalizable_emp: normalizable Aemp.
Hint Resolve normalizable_emp.
More lemmas
Lemma hplus_ram_lD:
∀ h h1 h2 l PP QQ perm init,
hplus (Hdef h1) h2 = Hdef h →
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, h2 = Hdef hf ∧
(hf l = HVnone ∧ 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:
∀ h h1 h2 l PP QQ perm init,
hplus h1 (Hdef h2) = Hdef h →
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, h1 = Hdef hf ∧
(hf l = HVnone ∧ 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:
∀ h h1 h2 l PP QQ perm init,
hplus (Hdef h1) h2 = Hdef h →
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, h2 = Hdef hf ∧
(hf l = HVnone ∧ (∀ 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:
∀ h h1 h2 l PP QQ perm init,
hplus h1 (Hdef h2) = Hdef h →
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, h1 = Hdef hf ∧
(hf l = HVnone ∧ (∀ 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:
∀ h hs h´´ l PP QQ isrmw perm init,
hsum hs = Hdef h →
In (Hdef h´´) hs →
h´´ l = HVra 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:
∀ h h1 h2 l PP QQ isrmw perm init,
hplus h1 h2 = Hdef h →
h l = HVra PP QQ isrmw perm init →
∃ hf1 hf2,
h1 = Hdef hf1 ∧ h2 = Hdef hf2
∧ << N: hf1 l ≠ HVnone ∨ hf2 l ≠ HVnone >>
∧ << L: hf1 l = HVnone ∨ ∃ 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 ∨ ∃ 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´:
∀ h h1 h2 l PP QQ isrmw perm init,
hplus h1 h2 = Hdef h →
h l = HVra PP QQ isrmw perm init →
∃ hf1 hf2, h1 = Hdef hf1 ∧ h2 = Hdef hf2 ∧
( (hf1 l = HVnone ∧ ∃ PP´ QQ´, hf2 l = HVra PP´ QQ´ isrmw perm init ∧ PP´ = PP ∧ QQ´ = QQ)
∨ (hf2 l = HVnone ∧ ∃ 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:
∀ h h1 h2 l PP QQ isrmw perm init v,
hplus h1 h2 = Hdef h →
h l = HVra PP QQ isrmw perm init →
∃ hf PP´ QQ´ isrmw´ perm´ init´,
(h1 = Hdef hf ∨ h2 = Hdef hf) ∧ 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:
∀ h´ hs l PP QQ isrmw perm init v,
hsum hs = Hdef h´ →
h´ l = HVra PP QQ isrmw perm init →
∃ h´´ PP´ QQ´ isrmw´ perm´ init´,
In (Hdef h´´) 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 h h1 h2 l PP QQ perm init:
hplus h1 h2 = Hdef h →
h l = HVra PP QQ true perm init →
∃ hf PP´ QQ´ perm´ init´,
(h1 = Hdef hf ∨ h2 = Hdef hf) ∧ hf l = HVra PP´ QQ´ true perm´ init´.
Lemma hsum_eq_ra_rmwD:
∀ h´ hs l PP QQ perm init,
hsum hs = Hdef h´ →
h´ l = HVra PP QQ true perm init →
∃ h´´ PP´ QQ´ perm´ init´, In (Hdef h´´) hs ∧ h´´ l = HVra PP´ QQ´ true perm´ init´.
Lemma hplus_eq_ra_ownD h h1 h2 l PP QQ perm init v :
hplus h1 h2 = Hdef h →
h l = HVra PP QQ false perm init →
sval (QQ v) ≠ Aemp →
sval (QQ v) ≠ Afalse →
∃ hf PP´ QQ´ perm´ init´,
(h1 = Hdef hf ∨ h2 = Hdef hf) ∧ hf l = HVra PP´ QQ´ false perm´ init´
∧ sval (QQ´ v) ≠ Aemp ∧ sval (QQ´ v) ≠ Afalse.
Lemma hsum_eq_ra_ownD:
∀ h´ hs l PP QQ perm init v,
hsum hs = Hdef h´ →
h´ l = HVra PP QQ false perm init →
sval (QQ v) ≠ Aemp →
sval (QQ v) ≠ Afalse →
∃ h´´ PP´ QQ´ perm´ init´,
In (Hdef h´´) hs ∧ h´´ l = HVra PP´ QQ´ false perm´ init´
∧ sval (QQ´ v) ≠ Aemp ∧ sval (QQ´ v) ≠ Afalse.
Lemma hplus_ra_own_l h h1 h2 l PP QQ perm init v :
hplus (Hdef h1) h2 = Hdef h →
h1 l = HVra 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 h h1 h2 l PP QQ perm init v :
hplus h1 (Hdef h2) = Hdef h →
h2 l = HVra 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 h hs hf l PP QQ perm init v :
hsum hs = Hdef h →
In (Hdef hf) hs →
hf l = HVra 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 E PP QQ isrmw perm1 perm2 init1 init2 :
hplus (hsingl E (HVra PP QQ isrmw perm1 init1)) (hsingl E (HVra Wemp Remp false perm2 init2))
= hsingl E (HVra PP QQ isrmw (ohlplus perm1 perm2) (ohlplus init1 init2)).
Lemma atomic_hsingl_duplicate:
∀ l PP QQ isrmw perm init, hsingl l (HVra PP QQ isrmw perm init) =
hplus (hsingl l (HVra PP QQ isrmw perm init))
(hsingl l (HVra Wemp Remp false perm init)).
Lemma hdef_initializeE hf E PP QQ isrmw perm init:
hf E = HVra PP QQ isrmw perm init →
Hdef (initialize hf E) = hplus (Hdef hf) (hsingl E (HVra Wemp Remp false None (Some HLCnormal))).
Lemma hplus_is_nonatomic_full :
∀ h h1 h2 l,
hplus h1 h2 = Hdef h →
is_nonatomic (h l) →
∃ hf1 hf2,
h1 = Hdef hf1 ∧ h2 = Hdef hf2 ∧
( (is_nonatomic (hf1 l) ∧ hf2 l = HVnone) ∨
(is_nonatomic (hf2 l) ∧ hf1 l = HVnone) ).
Lemma hsum_is_nonatomic_all :
∀ hs h l,
hsum hs = Hdef h →
is_nonatomic (h l) →
∀ hf, In (Hdef hf) hs → hf l = HVnone ∨ is_nonatomic (hf l).
Lemma is_nonatomic_initialize :
∀ hf l l´, is_nonatomic (hf l) → is_nonatomic (initialize hf l´ l).
Lemma Hsim_nalloc :
∀ h hf l ,
Hsim h (Hdef hf) →
hf l = HVnone →
∃ hf´, h = Hdef hf´ ∧ hf´ l = HVnone.
Lemma is_nonatomic_hsim :
∀ hf1 hf2 l, HFsim hf1 hf2 → (is_nonatomic (hf1 l) ↔ is_nonatomic (hf2 l)).
Lemma hplus_has_nonatomic_l_eq:
∀ hf hf1 h2 (SUM: hplus (Hdef hf1) h2 = Hdef hf) l (NA: is_nonatomic (hf1 l)), hf l = hf1 l.
Lemma hplus_has_nonatomic_r_eq:
∀ hf h1 hf2 (SUM: hplus h1 (Hdef hf2) = Hdef hf) l (NA: is_nonatomic (hf2 l)), hf l = hf2 l.
Lemma hplus_is_nonatomic_eq:
∀ hf h1 h2 (SUM: hplus h1 h2 = Hdef hf) l (NA: is_nonatomic (hf l)),
∃ hf1 hf2, h1 = Hdef hf1 ∧ h2 = Hdef hf2 ∧
((hf1 l = hf l ∧ hf2 l = HVnone) ∨ (hf1 l = HVnone ∧ hf2 l = hf l)).
Lemma hsum_has_nonatomic_eq:
∀ hlist hs (SUM: hsum hlist = Hdef hs) hf (IN: In (Hdef hf) hlist) l (NA: is_nonatomic (hf l)),
hs l = hf l.
Lemma hsum_is_nonatomic_eq:
∀ hlist hs (SUM: hsum hlist = Hdef hs) l (NA: is_nonatomic (hs l)),
∀ hf (IN: In (Hdef hf) hlist), hf l = hs l ∨ hf l = HVnone.
Opaque hplus.
Lemma hplus_propagate_initialize:
∀ hf l (A: is_atomic (hf l)) hFR h (EQ: hplus (Hdef hf) hFR = Hdef h),
hplus (Hdef (initialize hf l)) hFR = Hdef (initialize h l).
This page has been generated by coqdoc