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.
Proof.
unfold has_value; split; ins; desf; eauto.
Qed.
Lemma has_value_sim hv hv´ v (SIM: HVsim hv hv´): has_value hv v ↔ has_value hv´ v.
Proof.
unfold has_value; desf; ins; desf.
Qed.
Lemma is_val_implies_is_nonatomic hv: is_val hv → is_nonatomic hv.
Proof.
destruct hv; ins.
Qed.
Lemma is_val_implies_normal hv: is_val hv → HVlabeled hv HLnormal.
Proof.
destruct hv; ins; desf.
Qed.
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).
Proof.
destruct h; ins; unfold Hsim, lupd; desf.
repeat eexists; try edone.
red; ins; desf.
Qed.
Lemma lupd_label:
∀ h lbl, h ≠ Hundef → HlabeledExact (lupd h lbl) lbl.
Proof.
destruct h; ins; unfold Hsim, lupd; desf.
repeat eexists; try edone.
red; ins; desf.
Qed.
Lemma lupd_eq: ∀ h h´ lbl (SIM: Hsim h h´) (LBL: HlabeledExact h lbl), h = lupd h´ lbl.
Proof.
unfold Hsim, HlabeledExact; ins; desf; ins.
f_equal; extensionality l.
specialize (LBL0 l); specialize (SIM1 l); desf; red in SIM1; desf; ins; desf; desf.
Qed.
Lemma lupd_eq_lupd: ∀ h h´ lbl (DEF: h ≠ Hundef) (EQ: lupd h lbl = lupd h´ lbl), Hsim h h´.
Proof.
ins; red; desf.
destruct h, h´; ins; desf.
repeat eexists; try edone.
red; ins.
apply equal_f with (x := l) in H0; desf.
Qed.
Lemmas about heap labels and hlplus.
Lemma Wlabel_implies_label: ∀ hv lbl, HVlabeledW hv lbl → HVlabeled hv lbl.
Proof.
ins; red in H; desf; ins; desf; vauto.
Qed.
Lemma Rlabel_implies_label: ∀ hv lbl, HVlabeledR hv lbl → HVlabeled hv lbl.
Proof.
ins; red in H; desf; ins; desf; vauto.
Qed.
Lemma label_is_consistent_with_exact_label:
∀ hv (N: hv ≠ HVnone) 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 Rlabel_is_consistent_with_exact_label:
∀ hv 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 Wlabel_is_consistent_with_exact_label:
∀ hv lbl lbl´ (LAB: HVlabeledW hv lbl) (LABx: HVlabeledExact hv lbl´), lbl = lbl´.
Proof.
ins.
assert (N: hv ≠ HVnone) by (intro N; rewrite N in *; ins).
eby ins; apply Wlabel_implies_label in LAB; eapply label_is_consistent_with_exact_label.
Qed.
Lemma nonatomic_label:
∀ hv (NA: is_nonatomic hv) lbl, HVlabeledExact hv lbl ↔ HVlabeled hv lbl.
Proof. destruct hv; simpls. 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:
∀ hf lbl, HFlabeled hf lbl ↔ Hlabeled (Hdef hf) lbl.
Proof.
split; ins.
by ∃ hf.
by unfold Hlabeled in H; desf.
Qed.
Lemma label_exact_hdef:
∀ hf lbl, HFlabeledExact hf lbl ↔ HlabeledExact (Hdef hf) lbl.
Proof.
split; ins.
by ∃ hf.
by unfold HlabeledExact in H; desf.
Qed.
Lemma label_hvplus:
∀ hv1 hv2 lbl
(DEF: hvplusDEF hv1 hv2)
(PLUS: HVlabeled (hvplus hv1 hv2) lbl),
HVlabeled hv1 lbl ∨ HVlabeled hv2 lbl.
Proof.
ins.
red in DEF; desf; simpls; try solve [by left | by right].
desf; desf; simpls;
solve [
inv Heq0; vauto
|
inv Heq; apply hlplus_monotone_inv in PLUS; desf; vauto
].
Qed.
Lemma Rlabel_hvplus:
∀ hv1 hv2 lbl
(DEF: hvplusDEF hv1 hv2)
(PLUS: HVlabeledR (hvplus hv1 hv2) lbl),
HVlabeledR hv1 lbl ∨ HVlabeledR hv2 lbl.
Proof.
ins.
red in DEF; desf; simpls; try solve [by left | by right]; desf;
exploit ohlplus_with_basic_label; eauto; ins; desf; eauto.
Qed.
Lemma Wlabel_hvplus:
∀ hv1 hv2 lbl
(DEF: hvplusDEF hv1 hv2)
(PLUS: HVlabeledW (hvplus hv1 hv2) lbl),
HVlabeledW hv1 lbl ∨ HVlabeledW hv2 lbl.
Proof.
ins.
red in DEF; desf; simpls; try solve [by left | by right]; desf;
exploit ohlplus_with_basic_label; eauto; ins; desf; eauto.
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: ∀ hv, HVsim hv hv.
Proof.
ins; red; desf; repeat split; apply HLCsim_refl.
Qed.
Lemma HVsim_sym: ∀ hv hv´, HVsim hv hv´ ↔ HVsim hv´ hv.
Proof.
by unfold HVsim; split; ins; desf; repeat split; desf; rewrite HLCsim_sym.
Qed.
Lemma HVsim_trans hv1 hv2 hv3: HVsim hv1 hv2 → HVsim hv2 hv3 → HVsim hv1 hv3.
Proof.
unfold HVsim; ins; desf; desf; eauto 7 using HLCsim_trans.
Qed.
Lemma HVsim_alloc: ∀ hv1 hv2 (SIM: HVsim hv1 hv2), hv1 ≠ HVnone ↔ hv2 ≠ HVnone.
Proof.
ins; red in SIM; desf.
Qed.
Lemma is_atomic_sim: ∀ hv hv´ (SIM: HVsim hv hv´), is_atomic hv ↔ is_atomic hv´.
Proof.
split; ins; destruct hv, hv´; simpls.
Qed.
Lemma is_nonatomic_sim: ∀ hv hv´ (SIM: HVsim hv hv´), is_nonatomic hv ↔ is_nonatomic hv´.
Proof.
split; ins; destruct hv, hv´; simpls.
Qed.
Lemma HFsim_refl: ∀ hf, HFsim hf hf.
Proof.
ins; red; ins; apply HVsim_refl.
Qed.
Lemma HFsim_sym: ∀ hf hf´, HFsim hf hf´ ↔ HFsim hf´ hf.
Proof.
by ins; split; red; ins; specialize (H l); rewrite HVsim_sym.
Qed.
Lemma HFsim_trans hf1 hf2 hf3: HFsim hf1 hf2 → HFsim hf2 hf3 → HFsim hf1 hf3.
Proof.
unfold HFsim; ins; eauto using HVsim_trans.
Qed.
Lemma Hsim_alt: ∀ hf hf´, HFsim hf hf´ ↔ Hsim (Hdef hf) (Hdef hf´).
Proof.
split; ins.
by ∃ hf, hf´; vauto.
by unfold Hsim in *; desf.
Qed.
Lemma Hsim_sym: ∀ h h´, 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: ∀ h, h ≠ Hundef → Hsim h h.
Proof.
destruct h; ins; rewrite <- Hsim_alt; apply HFsim_refl.
Qed.
Lemma Hsim_trans h1 h2 h3: Hsim h1 h2 → Hsim h2 h3 → Hsim h1 h3.
Proof.
unfold Hsim; ins; desf; repeat eexists; eauto using HFsim_trans.
Qed.
Lemma Hsim_alloc:
∀ h hf l
(SIM: Hsim h (Hdef hf))
(DEF: hf l ≠ HVnone),
∃ hf´, h = Hdef hf´ ∧ hf´ l ≠ HVnone.
Proof.
by unfold Hsim, HFsim, HVsim; ins; desf; specialize (SIM1 l); eexists; split; eauto; intro; desf.
Qed.
Lemma label_sim:
∀ hv1 hv2 (SIM: HVsim hv1 hv2) lbl (LBL: HVlabeled hv1 lbl),
∃ lbl´, HVlabeled hv2 lbl´.
Proof.
unfold HVlabeled; ins; desf; ins; desf; try (by eexists; eauto);
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:
∀ hv1 hv2 (SIM: HVsim hv1 hv2) lbl (LBL: HVlabeledR hv1 lbl),
∃ lbl´, HVlabeledR hv2 lbl´.
Proof.
unfold HVlabeledR; ins; desf; ins; desf; try (by eexists; eauto);
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 Wlabel_sim:
∀ hv1 hv2 (SIM: HVsim hv1 hv2) lbl (LBL: HVlabeledW hv1 lbl),
∃ lbl´, HVlabeledW hv2 lbl´.
Proof.
unfold HVlabeledW; ins; desf; ins; desf; try (by eexists; eauto);
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 exact_label_sim:
∀ h1 h2 lbl, HlabeledExact h1 lbl → HlabeledExact h2 lbl → Hsim h1 h2 → h1 = h2.
Proof.
unfold HlabeledExact, Hsim; ins; desf.
f_equal; extensionality l; specialize (H3 l); specialize (H4 l); specialize (H5 l).
red in H3; red in H4; red in H5; desf; desf.
Qed.
Some basic lemmas about heaps and hplus.
Lemma hdef_alt h : h ≠ Hundef ↔ ∃ hf, h = Hdef hf.
Proof. destruct h; split; ins; desf; vauto. Qed.
Lemma AcombinableC P Q: Acombinable P Q → Acombinable Q P.
Proof. unfold Acombinable; ins; desf; eauto. Qed.
Lemma assn_mod_eqI1 (P Q: assn_mod): 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 (P Q: assn_mod): 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 P Q : Asim P Q → mk_assn_mod P = mk_assn_mod Q.
Proof. ins; apply assn_mod_eqI; Asim_simpl. Qed.
Lemma hv_acq_defC b1 Q1 b2 Q2 :
hv_acq_def b1 Q1 b2 Q2 → hv_acq_def b2 Q2 b1 Q1.
Proof. destruct 1; desc; vauto. Qed.
Lemma hvplusDEFC hv1 hv2: hvplusDEF hv1 hv2 → hvplusDEF hv2 hv1.
Proof.
unfold hvplusDEF; desf; ins; desf; repeat split;
eauto using AcombinableC, eq_sym, hv_acq_defC.
Qed.
Lemma hvplusC hv1 hv2: hvplusDEF hv1 hv2 → hvplus hv1 hv2 = hvplus hv2 hv1.
Proof.
unfold hvplus, hvplusDEF; ins; desf; desf; f_equal; eauto using andbC, orbC, eq_sym, ohlplusC;
try solve [by exfalso; eauto]; exten; ins; desf; apply assn_mod_eqI1;
try solve [specialize (H0 x); unfold Acombinable in *; desf; congruence].
by specialize (H x); destruct H; desc; ins; congruence.
by apply assn_norm_ok; vauto.
Qed.
Lemma hplusC h1 h2: hplus h1 h2 = hplus h2 h1.
Proof.
unfold hplus; desf; f_equal; try exten; ins; eauto using hvplusC;
try solve [exfalso; eauto using hvplusDEFC].
Qed.
Lemma hplus_emp_l h : hplus hemp h = h.
Proof. by unfold hplus, hemp; desf; destruct n; ins. Qed.
Lemma hplus_emp_r h : hplus h hemp = h.
Proof. by rewrite hplusC, hplus_emp_l. Qed.
Lemma hplus_eq_emp h1 h2 : hplus h1 h2 = hemp ↔ h1 = hemp ∧ h2 = hemp.
Proof.
split; ins; desf; try apply hplus_emp_r.
destruct h1, h2; ins; desf; inv H.
split; unfold hemp; f_equal; extensionality l; apply (f_equal (fun f ⇒ f l)) in H1; ins;
destruct (hf l), (hf0 l); ins.
Qed.
Lemma assn_norm_mod (Q : assn_mod) : assn_norm (sval Q) = sval Q.
Proof. destruct Q; ins. Qed.
Lemma hvplusDEF_hvplusA h1 h2 h3 :
hvplusDEF h1 h2 →
hvplusDEF (hvplus h1 h2) h3 →
hvplusDEF h1 (hvplus h2 h3).
Proof.
destruct h1, h2, h3; ins; desf; desf; ins; f_equal; 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.
Qed.
Lemma hvplusDEF_hvplus1 h1 h2 h3 :
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.
Qed.
Lemma hvplusDEF_hvplus2 h1 h2 h3 :
hvplusDEF h1 h2 →
hvplusDEF (hvplus h1 h2) h3 →
hvplusDEF h2 h3.
Proof.
ins; rewrite hvplusC in *; eauto using hvplusDEFC, hvplusDEF_hvplus1.
Qed.
Lemma hvplusA h1 h2 h3 :
hvplusDEF h1 h2 →
hvplus (hvplus h1 h2) h3 = hvplus h1 (hvplus h2 h3).
Proof.
destruct h1, h2, h3; ins; desf; desf; ins; rewrite !ohlplusA; f_equal;
try (by destruct Heq; vauto);
try (by destruct Heq0; vauto);
try (exten; intro y; desf;
apply assn_mod_eqI; ins; Asim_simpl; vauto); apply hlplusA.
Qed.
Lemma hplusA h1 h2 h3 :
hplus (hplus h1 h2) h3 = hplus h1 (hplus h2 h3).
Proof.
unfold hplus; desf; try solve [f_equal; exten; eauto using hvplusA];
destruct n; ins; eauto using hvplusDEF_hvplusA, hvplusDEF_hvplus1, hvplusDEF_hvplus2.
rewrite hvplusC; eauto.
apply hvplusDEFC, hvplusDEF_hvplusA; eauto using hvplusDEFC.
rewrite hvplusC; eauto using hvplusDEFC.
Qed.
Lemma hplusAC h1 h2 h3 :
hplus h2 (hplus h1 h3) = hplus h1 (hplus h2 h3).
Proof.
by rewrite <- (hplusA h2), (hplusC h2), hplusA.
Qed.
Lemma hplus_add_same: ∀ h1 h2 h, h1 = h2 → hplus h1 h = hplus h2 h.
Proof.
by ins; subst.
Qed.
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).
Proof.
done.
Qed.
Further properties of hplus
Lemma hplus_not_undef_l h h´ : hplus h h´ ≠ Hundef → h ≠ Hundef.
Proof. by destruct h, h´; ins. Qed.
Lemma hplus_not_undef_r h h´ : hplus h h´ ≠ Hundef → h´ ≠ Hundef.
Proof. by destruct h, h´; ins. Qed.
Hint Resolve hplus_not_undef_l.
Hint Resolve hplus_not_undef_r.
Lemma hplus_undef_r: ∀ h, hplus h Hundef = Hundef.
Proof.
by ins; destruct h; desf.
Qed.
Lemma hplus_undef_l: ∀ h : heap, hplus Hundef h = Hundef.
Proof.
by ins; rewrite hplusC; apply hplus_undef_r.
Qed.
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) >>.
Proof.
destruct h, h´; ins; desf; vauto.
Qed.
Lemma hplus_def_inv_l h h´ hf : hplus h h´ = Hdef hf → ∃ h3, h = Hdef h3.
Proof. destruct h, h´; vauto. Qed.
Lemma hplus_def_inv_r h h´ hf : hplus h h´ = Hdef hf → ∃ h3, h´ = Hdef h3.
Proof. destruct h, h´; vauto. Qed.
Lemma hplus_preserves_alloc_l:
∀ h1 h2 h l (SUM: Hdef h = hplus (Hdef h1) h2 ) (ALL: h1 l ≠ HVnone), h l ≠ HVnone.
Proof.
ins; intro CONTRA; destruct ALL; desf; unfold hvplus in CONTRA; desf.
Qed.
Lemma hplus_preserves_alloc_r:
∀ h1 h2 h l (SUM: Hdef h = hplus h1 (Hdef h2)) (ALL: h2 l ≠ HVnone), h l ≠ HVnone.
Proof.
eby ins; rewrite hplusC in SUM; eapply hplus_preserves_alloc_l.
Qed.
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.
Proof.
destruct h1, h2; ins; desf.
generalize (h0 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_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.
Proof.
destruct h1, h2; ins; desf.
repeat eexists; try edone;
by destruct (hf loc), (hf0 loc).
Qed.
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.
Proof.
ins.
red in H; desf.
specialize (H2 loc).
exploit hplus_nalloc; eauto.
rewrite H0 in H2; ins; desf.
Qed.
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.
Proof.
by ins; desf; specialize (h0 l); destruct (h1 l), (h2 l); simpls; congruence.
Qed.
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).
Proof.
destruct h1, h2; ins; desf.
specialize (H0 _ eq_refl); specialize (h0 l).
unfold is_val in *; desf; ins; desf.
Qed.
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).
Proof.
ins; rewrite hplusC in *; eauto using hplus_has_val_l.
Qed.
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)).
Proof.
destruct h1, h2; ins; desf.
repeat eexists; specialize (h0 l); unfold hvplusDEF in *; desf; vauto.
Qed.
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.
Proof.
destruct h1, h2; ins; desf.
specialize (H0 _ eq_refl); specialize (h l).
rewrite H0 in *; ins; desf.
Qed.
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.
Proof.
destruct h1, h2; ins; desf.
specialize (H0 _ eq_refl); specialize (h l).
rewrite has_value_alt in H0; desf.
rewrite H0; ins; desf.
Qed.
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.
Proof.
ins; rewrite hplusC in *; eauto using hplus_val_lD.
Qed.
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.
Proof.
ins; rewrite hplusC in *; eauto using hplus_val_lD_weak.
Qed.
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).
Proof.
destruct h1, h2; ins; desf.
repeat eexists; specialize (h l); unfold hvplusDEF in *; desf; vauto.
Qed.
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).
Proof.
destruct h1, h2; ins; desf.
repeat eexists; specialize (h l); unfold hvplusDEF in *; desf; vauto.
Qed.
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.
Proof.
destruct h1, h2; ins; desf.
specialize (H0 _ eq_refl); specialize (h l).
rewrite H0 in *; ins; desf.
Qed.
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.
Proof.
ins; rewrite hplusC in *; eauto using hplus_uval_lD.
Qed.
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).
Proof.
destruct h1, h2; ins; desf.
repeat eexists; specialize (h l); unfold hvplusDEF in *; desf; vauto.
Qed.
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).
Proof.
destruct h1, h2; ins; desf.
specialize (H0 _ eq_refl); specialize (h0 l).
unfold is_atomic in *; desf; ins; desf.
Qed.
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).
Proof.
ins; rewrite hplusC in *; eauto using hplus_has_atomic_l.
Qed.
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)).
Proof.
destruct h1, h2; ins; desf.
repeat eexists; specialize (h0 l); unfold hvplusDEF in *; desf; vauto.
Qed.
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).
Proof.
destruct h1, h2; ins; desf.
specialize (H0 _ eq_refl); specialize (h0 l).
unfold is_nonatomic in *; desf; ins; desf.
Qed.
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).
Proof.
ins; rewrite hplusC in *; eauto using hplus_has_nonatomic_l.
Qed.
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)).
Proof.
destruct h1, h2; ins; desf.
repeat eexists; specialize (h0 l); unfold hvplusDEF in *; desf; vauto.
Qed.
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´.
Proof.
destruct h1 as [|hf1]; destruct h2 as [|hf2]; unfold NW; ins; desf.
specialize (h0 l); red in h0; desf; ins; desf.
× ∃ hf2; repeat eexists; eauto.
× ∃ hf1; repeat eexists; eauto.
× red in H1; desf.
unfold ohlplus in Heq1; desf.
+ apply normal_hlplus in H1; desf.
- ∃ hf1; repeat eexists; eauto.
- ∃ hf2; repeat eexists; eauto.
+ ∃ hf1; repeat eexists; eauto.
+ ∃ hf2; repeat eexists; eauto.
Qed.
Lemma hplus_hsingl: ∀ l hv hv´ (DEFv: hvplusDEF hv hv´),
hplus (hsingl l hv) (hsingl l hv´) = hsingl l (hvplus hv hv´).
Proof.
by ins; desf; [f_equal; extensionality v | destruct n; ins]; unfold hupd; desf.
Qed.
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.
Proof.
ins; unfold initialize, hupd; destruct (classic (l´ = l)).
by desf; destruct (h l).
by desf.
Qed.
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´.
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: ∀ 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.
Proof.
ins; desf; split; specialize (h l); red in h; desf.
simpls; desf; try (by simpls; desf); desf;
try solve [
try left; apply ohlplus_HLleq in Heq1; eapply HLleq_trans; eauto; done
|
try right; apply ohlplus_HLleq in Heq2; eapply HLleq_trans; eauto; done
].
Qed.
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.
Proof.
ins; desf; specialize (h l); red in h; desf.
unfold HVlabeledR in *; ins; desf.
× eapply HLleq_trans; split; eauto.
eby eapply ohlplus_HLleq.
× ins; desf.
Qed.
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.
Proof.
ins; desf; specialize (h l); red in h; desf.
unfold HVlabeledW in *; ins; desf.
× eapply HLleq_trans; split; eauto.
eby eapply ohlplus_HLleq.
× ins; desf.
Qed.
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.
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 (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; rewrite Y; ins; repeat split; try by eauto; instantiate; desf; eauto |
∃ hz; rewrite Z; ins; repeat split; try by eauto; instantiate; desf; eauto].
Qed.
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.
Proof.
ins; apply hplus_def_inv in SUM; desf; rewrite PLUSv in LABEL.
by apply Rlabel_hvplus in LABEL; desf; [∃ hy | ∃ hz]; auto.
Qed.
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.
Proof.
ins; apply hplus_def_inv in SUM; desf; rewrite PLUSv in LABEL.
by apply Wlabel_hvplus in LABEL; desf; [∃ hy | ∃ hz]; auto.
Qed.
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.
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; right; rewrite Z; ins; eauto
|
∃ hy; left; rewrite Y; ins; eauto
|
eapply ohlplus_with_basic_label in Heq; eauto; desf; [
∃ hy; left; rewrite Y; ins; desf; repeat (split; eauto; try done)
|
∃ hz; right; rewrite Z; ins; desf; repeat (split; eauto; try done)
]
|
eapply ohlplus_with_basic_label in Heq0; eauto; desf; [
∃ hy; left; rewrite Y; ins; desf; repeat (split; eauto; try done)
|
∃ hz; right; rewrite Z; ins; desf; repeat (split; eauto; try done)
]
].
Qed.
Lemma hplus_sim_def: ∀ h h1 h2 (SIM: Hsim h1 h2) (DEF: hplus h1 h ≠ Hundef), hplus h2 h ≠ Hundef.
Proof.
ins; rewrite hdef_alt in *; unfold Hsim in SIM; desf.
assert (hDEF := (hplus_def_inv_r _ _ DEF)); desf.
rewrite hplus_unfold in *; desf.
eby eexists.
by destruct n; ins; specialize (h v); specialize (SIM1 v);
unfold HVsim, hvplusDEF in *; desf; desf.
Qed.
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´).
Proof.
unfold Hsim; ins; desf.
rewrite hdef_alt in DEF; desf.
assert (DEF´: hplus (Hdef hf´0) (Hdef hf´) ≠ Hundef).
{
intro UNDEF.
rewrite hplus_unfold in *; desf.
destruct n; ins.
specialize (h v); specialize (SIM3 v); specialize (SIM5 v).
by unfold hvplusDEF, HVsim in *; desf; desf.
}
rewrite hdef_alt in DEF´; desf.
eexists,; repeat split; eauto.
red; ins.
specialize (SIM3 l); specialize (SIM5 l).
desf.
specialize (h0 l); specialize (h l).
by unfold HVsim, hvplusDEF, hvplus in *; desf; desf; repeat split; apply ohlplus_sim.
Qed.
Lemma exact_label_hplus_dist:
∀ h1 h2 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; ins; desf;
try apply hlplus_eq_basic in H0; try apply hlplus_eq_basic in H1; desf.
Qed.
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.
Proof.
ins.
rewrite hdef_alt in DEF; desf.
apply hplus_def_inv in DEF; desf.
rewrite hplus_unfold; desf.
clear h PLUSv.
rewrite <- label_exact_hdef in ×.
red; ins.
specialize (DEFv l); specialize (L1 l); specialize (L2 l).
unfold hvplus; desf; ins; desf; ins; desf; eauto using hlplus_same.
Qed.
Lemma lupd_hplus_dist:
∀ h1 h2 lbl, lupd (hplus h1 h2) lbl = hplus (lupd h1 lbl) (lupd h2 lbl).
Proof.
ins.
unfold lupd; desf; rewrite hplus_unfold in *; desf; try (by destruct n; ins; specialize (h v); desf).
by f_equal; extensionality v; specialize (h0 v); specialize (h v); desf; ins; desf; f_equal; rewrite hlplus_same.
Qed.
Lemmas about hsum
Lemma hsum_nil : hsum nil = hemp.
Proof. done. Qed.
Lemma hsum_cons a l : hsum (a :: l) = hplus a (hsum l).
Proof. done. Qed.
Lemma hsum_one h : hsum (h :: nil) = h.
Proof. apply hplus_emp_r. Qed.
Lemma hsum_two h h´ : hsum (h :: h´ :: nil) = hplus h h´.
Proof. by unfold hsum; ins; rewrite hplus_emp_r. Qed.
Lemma hsum_perm l l´ : Permutation l l´ → hsum l = hsum l´.
Proof. unfold hsum; induction 1; ins; try congruence; apply hplusAC. Qed.
Lemma hsum_app l l´ : 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_eq_emp: ∀ hlist, hsum hlist = hemp ↔ ∀ 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: ∀ hlist hf (SUM: hsum hlist = Hdef hf),
∀ h (IN: In h hlist), ∃ hf´, h = Hdef hf´.
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 l h loc :
hsum l = Hdef h →
h loc ≠ HVnone →
∃ h´, In (Hdef h´) l ∧ h´ loc ≠ HVnone.
Proof.
unfold hsum.
induction[h] l; ins; [by inv H|].
eapply hplus_alloc in H; eauto; desf; eauto.
exploit IHl; eauto; intro; desf; eauto.
Qed.
Lemma hsum_alloc_sim l h loc :
Hsim (hsum l) (Hdef h) →
h loc ≠ HVnone →
∃ h´, In (Hdef h´) l ∧ h´ loc ≠ HVnone.
Proof.
ins.
red in H; desf.
specialize (H2 loc).
exploit hsum_alloc; eauto.
intro N; rewrite N in *; ins; desf.
Qed.
Lemma hsum_nalloc hs hf h loc :
Hdef hf = hsum hs →
hf loc = HVnone →
In h hs →
∃ hf, Hdef hf = h ∧ hf loc = HVnone.
Proof.
unfold hsum; induction[hf] hs; ins; desf;
eapply hplus_nalloc in H; eauto; desf; eauto.
Qed.
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.
Proof.
ins.
assert (DEF := ((hsum_def_inv _ SUM) _ IN)); desf.
∃ hf´; 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:
∀ hs hf (SUM: hsum hs = Hdef hf) hf´ (IN: In (Hdef hf´) hs) l (ALL: hf´ l ≠ HVnone),
hf l ≠ HVnone.
Proof.
ins; intro.
exploit hsum_nalloc_all; eauto; ins; desf.
Qed.
Lemma hsum_none: ∀ hlist hf (SUM: hsum hlist = Hdef hf)
l (NONE: ∀ hf´ (IN: In (Hdef hf´) hlist), hf´ l = HVnone),
hf l = HVnone.
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_val :
∀ h hs h´´ l,
hsum hs = Hdef h →
In (Hdef h´´) hs →
is_val (h´´ l) →
is_val (h l).
Proof.
intros until 0; induction[h] hs; ins; rewrite hsum_cons in ×.
desf; eauto using hplus_has_val_r.
eapply hplus_has_val_l; eauto; ins; desf.
Qed.
Lemma hsum_is_val :
∀ hs h l,
hsum hs = Hdef h →
is_val (h l) →
∃ hf, In (Hdef hf) hs ∧ is_val (hf l).
Proof.
induction hs; rewrite ?hsum_nil, ?hsum_cons in *; ins; desf.
by inv H.
eapply hplus_is_val in H; eauto; desf; eauto.
exploit IHhs; eauto; ins; desf; eauto.
Qed.
Lemma hsum_is_atomic :
∀ hs h l,
hsum hs = Hdef h →
is_atomic (h l) →
∃ hf, In (Hdef hf) 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: ∀ hs hf l (SUM: hsum hs = Hdef hf)
hf´ (IN: In (Hdef hf´) 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 :
∀ hs h l,
hsum hs = Hdef h →
is_nonatomic (h l) →
∃ hf, In (Hdef hf) 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: ∀ hs hf l (SUM: hsum hs = Hdef hf)
hf´ (IN: In (Hdef hf´) 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 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.
Proof.
intros until 0; induction[hf] hs; ins; rewrite hsum_cons in ×.
desf; eauto using hplus_val_rD.
eapply hplus_val_lD; eauto; ins; desf.
Qed.
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.
Proof.
intros until 0; induction[hf] hs; ins; rewrite hsum_cons in ×.
desf; eauto using hplus_val_rD_weak.
eapply hplus_val_lD_weak; eauto; ins; desf.
Qed.
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.
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_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.
Proof.
induction hs; rewrite ?hsum_nil, ?hsum_cons in *; ins; desf.
by inv H.
eapply hplus_valD_weak in H; eauto; desf; eauto.
exploit IHhs; eauto; ins; desf; eauto.
Qed.
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´.
Proof.
intros until 0; induction[h´ PP QQ isrmw perm init] hs; ins; [by inv H|].
rewrite hsum_cons in ×.
eapply hplus_eq_ra_initD in H; eauto.
desf; eauto 10.
exploit IHhs; eauto; intro; desf.
repeat eexists; eauto.
Qed.
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.
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:
∀ hs hf hf´ l lbl
(SUM: Hdef hf = hsum hs)
(IN: In (Hdef hf´) 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_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.
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_Wlabel in SUM; eauto; desf;
split; desf; eexists.
Qed.
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.
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´; vauto.
symmetry in SUM; specialize (IHhs _ _ _ SUM SUM0); desf.
exploit IHhs; eauto; ins; desf.
by ∃ hf´0; vauto.
Qed.
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.
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´; vauto.
symmetry in SUM; specialize (IHhs _ _ _ SUM SUM0); desf.
by ∃ hf´0; vauto.
Qed.
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.
Proof.
induction hs.
× rewrite hsum_nil; ins.
inv SUM.
× ins.
rewrite hsum_cons in SUM.
symmetry in SUM. assert (SUMcopy := SUM).
eapply hplus_preserves_Wlabel_inv in SUM; eauto; desf.
by ∃ hf´; vauto.
symmetry in SUM; specialize (IHhs _ _ _ SUM SUM0); desf.
by ∃ hf´0; vauto.
Qed.
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.
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 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´´.
Proof.
intros; eapply hplus_def_inv in H0; desc.
∃ (hupd h´ l (HVval v´ lbl)).
unfold hplus, hupd; desc; des_if; f_equal.
extensionality l´; ins; des_if; try subst l´; eauto; simpl; desf.
destruct n; intro l´; specialize (DEFv l´); desf; desf; unfold is_val in *; desf.
Qed.
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´).
Proof.
intros; eapply hplus_def_inv in H0; desc.
∃ (hupd h´ l (HVval v´ lbl)); desf.
unfold hupd, is_val in *; desf; ins; desf;
try solve [destruct n; intro l´´; specialize (DEFv l´´); desf; subst;
try rewrite Heq in *; eauto];
split; ins; desf; desf;
try solve [f_equal; extensionality l´; ins; des_if; ins; desf].
Qed.
Lemmas about initialize
Lemma initialize_alloc: ∀ hf l l´, hf l ≠ HVnone ↔ initialize hf l´ l ≠ HVnone.
Proof.
unfold initialize, hupd; split; ins; desf; congruence.
Qed.
Lemma hplus_init_def hf l h h´ :
hplus (Hdef hf) h = Hdef h´ →
hplus (Hdef (initialize hf l)) h ≠ Hundef.
Proof.
unfold hplus; intros; desf; desf; try by destruct n;
intros; unfold initialize, hupd; try specialize (h v); try red in h; desf; ins; desf.
Qed.
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).
Proof.
unfold hplus; intros; desf; desf;
try by destruct n; intros; unfold initialize, hupd;
try specialize (h v); try red in h; desf; ins; desf.
by f_equal; extensionality l´; unfold initialize, hupd; desf; simpls; desf; f_equal;
rewrite !ohlplusA, (ohlplusC _ init1).
Qed.
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´.
Proof.
eby unfold initialize, hupd; ins; desf; eexists.
Qed.
Lemma initialize_is_val: ∀ hf l l´, is_val (initialize hf l l´) → is_val (hf l´).
Proof.
by unfold initialize; ins; desf; unfold hupd in H; desf; try done; subst; rewrite Heq.
Qed.
Lemma initialize_is_atomic: ∀ hf 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: ∀ hf 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:
∀ hf l l´ lbl, is_nonatomic (hf l) → HVlabeled (hf l) lbl → HVlabeled (initialize hf l´ l) lbl.
Proof.
ins; unfold initialize, hupd; desf; rewrite ?Heq0 in *; ins.
Qed.
Lemma initialize_Wlabel: ∀ hf l l´ lbl, HVlabeledW (initialize hf l l´) lbl ↔ HVlabeledW (hf l´) lbl.
Proof.
unfold HVlabeledW, initialize, hupd; split; ins; desf; congruence.
Qed.
Lemma initialize_not_normal:
∀ hf 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:
∀ hf 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.
Lemma initialize_not_normalW:
∀ hf l l´ lbl (LAB: HVlabeledW (initialize hf l´ l) lbl) (N: lbl ≠ HLnormal), HVlabeledW (hf l ) lbl.
Proof.
unfold initialize, hupd; desf; ins; desf; rewrite ?Heq0; ins; desf.
Qed.
Lemmas about assertions
Lemma assn_sem_def P h : assn_sem P h → h ≠ Hundef.
Proof.
induction P; ins; desf.
eby eapply (H 0).
by red in H; desf.
by red in H; desf.
Qed.
Lemma sim_assn_sem :
∀ p p´ (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 Q h : assn_sem Q h → ∃ hf, h = Hdef hf.
Proof.
ins; eapply assn_sem_def in H; destruct h; vauto.
Qed.
Lemma precise_emp : precise Aemp.
Proof. red; ins; desf; rewrite !hplus_emp_l in *; vauto. Qed.
Lemma precise_star P Q : 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 P Q 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 PP h :
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 :
∀ l l´ (P: Permutation l l´) init h,
assn_sem (foldr Astar l init) h →
assn_sem (foldr Astar l´ init) h.
Proof.
induction 1; ins; desf; eauto 8.
rewrite hplusAC in *; repeat eexists; eauto.
Qed.
Lemma foldr_star_perm2 :
∀ l l´ (P: Permutation l l´) init,
Asim (foldr Astar l init) (foldr Astar l´ init).
Proof.
induction 1; ins; desf; eauto 8 using Asim.
Qed.
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´).
Proof.
induction[h] l; ins; desf; rewrite hplusA in ×.
repeat eexists; eauto; eapply IHl; ins.
Qed.
Lemma implies_trans: ∀ P Q R, implies P Q ∧ implies Q R → implies P R.
Proof.
unfold implies; ins; desf.
by apply H1, H.
Qed.
Lemma implies_frame: ∀ P Q F, implies P Q → implies (Astar P F) (Astar Q F).
Proof.
by unfold implies; ins; desf; eexists,; eauto.
Qed.
Lemma assn_sem_assn_norm: ∀ P 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:
∀ h 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,.
× 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: ∀ P, 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 P Q: 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: ∀ P, 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: normalizable Aemp.
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:
∀ 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)).
Proof.
destruct h2; ins; desf.
specialize (h0 l); rewrite H0 in *; ins; desf;
repeat eexists; vauto; try red; ins; desf; try (by rewrite e in *).
right; repeat eexists; ins; vauto.
destruct (h0 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:
∀ 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)).
Proof.
ins; rewrite hplusC in *; eauto using hplus_ram_lD.
Qed.
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))))).
Proof.
destruct h2; ins; desf.
specialize (h0 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 (h0 v); ins; desf; rewrite H, ?H1; Asim_simpl; eauto using Asim.
by right; repeat eexists; ins; vauto; Asim_simpl.
Qed.
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))))).
Proof.
ins; rewrite hplusC in *; eauto using hplus_ra_lD.
Qed.
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).
Proof.
intros until 0; induction[h 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 (h0 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:
∀ 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) >>.
Proof.
destruct h1, h2; unfold NW; ins; desf.
repeat eexists; specialize (h0 l); unfold hvplusDEF in *; desf; vauto;
right; vauto; repeat eexists; ins; desf; try congruence; eauto;
specialize (h1 v); rewrite ?e in *; ins; red in h1; desf; rewrite h1, ?e, ?h2 in *; ins.
Qed.
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))).
Proof.
destruct h1, h2; unfold NW; ins; desf.
repeat eexists; specialize (h0 l); unfold hvplusDEF in *; desf; vauto;
[left|right;left|right;right]; repeat (eexists; ins); desf;
specialize (h1 v); unfold Acombinable in *; ins; desf;
rewrite ?h1, ?h2, ?e in *; desf; vauto.
Qed.
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).
Proof.
destruct h1, h2; unfold NW; ins; desf.
specialize (h0 l); red in h0; desf; ins; desf;
try solve [repeat (eexists; try edone); eauto].
specialize (h1 v); red in h1; desf; try congruence.
by clear Heq0; repeat (eexists; try edone); eauto.
repeat (eexists; try edone); eauto; congruence.
Qed.
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).
Proof.
intros until 0; induction[h´ PP QQ isrmw perm init] hs; ins; [by inv H|].
rewrite hsum_cons in ×.
eapply hplus_eq_raD in H; eauto.
desf; eauto 10.
exploit IHhs; eauto; intro; desf; eauto 10.
do 7 eexists; eauto.
by split; try edone; ins; rewrite H2.
Qed.
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´.
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:
∀ 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´.
Proof.
intros until 0; generalize perm init; induction[h´ PP QQ init] hs; ins; [by inv H|].
rewrite hsum_cons in *; eapply hplus_eq_ra_rmwD in H; eauto.
desf; eauto 8; exploit IHhs; eauto; ins; desf; eauto 8.
Qed.
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.
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 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:
∀ 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.
Proof.
intros until 0; generalize perm init; induction[h´ PP QQ init] hs; ins; [by inv H|].
rewrite hsum_cons in *; eapply hplus_eq_ra_ownD in H; eauto.
desf; eauto 10; exploit IHhs; eauto; ins; desf; eauto 12.
Qed.
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.
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 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.
Proof. by rewrite hplusC; apply hplus_ra_own_l. Qed.
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.
Proof.
induction[h 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 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)).
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:
∀ 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)).
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 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))).
Proof.
rewrite hplusC; unfold initialize, hupd; ins; desf.
× f_equal; extensionality w; specialize (h w); red in h; 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.
× by destruct n; intro m; ins; desf; ins; desf; repeat split; try apply Lcombinable_same;
ins; vauto; destruct isrmw; vauto.
Qed.
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) ).
Proof.
ins.
exploit hplus_is_nonatomic; eauto; ins; desc.
eexists,; repeat split; eauto.
desf.
× left; intuition.
rewrite hplus_unfold in H; desf.
specialize (h0 l).
destruct (hf1 l); ins; desf.
× right; intuition.
rewrite hplus_unfold in H; desf.
specialize (h0 l).
rewrite hvplusC in H0; ins.
apply hvplusDEFC in h0.
destruct (hf2 l); ins; desf.
Qed.
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).
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 :
∀ hf l l´, is_nonatomic (hf l) → is_nonatomic (initialize hf l´ l).
Proof.
unfold initialize, is_nonatomic, hupd; ins; desf.
Qed.
Lemma Hsim_nalloc :
∀ h hf l ,
Hsim h (Hdef hf) →
hf l = HVnone →
∃ hf´, h = Hdef hf´ ∧ hf´ l = HVnone.
Proof.
unfold Hsim; ins; desf; eexists; split; eauto.
specialize (H2 l); rewrite H0 in H2; red in H2; desf.
Qed.
Lemma is_nonatomic_hsim :
∀ hf1 hf2 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_has_nonatomic_l_eq:
∀ hf hf1 h2 (SUM: hplus (Hdef hf1) h2 = Hdef hf) l (NA: is_nonatomic (hf1 l)), hf l = hf1 l.
Proof.
ins; desf.
specialize (h l); destruct (hf1 l); ins; desf.
Qed.
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.
Proof.
eby ins; rewrite hplusC in SUM; eapply hplus_has_nonatomic_l_eq.
Qed.
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)).
Proof.
ins.
apply hplus_def_inv in SUM; desf.
specialize (DEFv l); specialize (PLUSv l).
eexists,; repeat split; eauto.
destruct (hy l), (hz l); desf; ins; eauto.
rewrite PLUSv in NA; ins.
Qed.
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.
Proof.
induction hlist; ins.
rewrite hsum_cons in SUM; desf.
× eby eapply hplus_has_nonatomic_l_eq.
× case_eq (hsum hlist).
by intro U; rewrite U, hplus_undef_r in SUM.
ins.
rewrite H in SUM.
assert (hf0 l = hf l) by (apply IHhlist; done).
eby rewrite <- H0 in *; eapply hplus_has_nonatomic_r_eq.
Qed.
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.
Proof.
induction hlist; ins.
rewrite hsum_cons in SUM; desf; eapply hplus_is_nonatomic_eq in SUM; desf; eauto.
× eapply hsum_nalloc_all in SUM0; desf; eauto.
inv SUM0; eauto.
× eby rewrite <- SUM2 in *; eapply IHhlist.
Qed.
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).
Proof.
ins.
exploit (hplus_has_atomic_l _ l EQ); ins; desf.
unfold is_atomic in *; desf.
erewrite (hdef_initializeE); eauto.
rewrite hplusA, (hplusC _ hFR), <- hplusA, EQ.
eby erewrite hdef_initializeE.
Qed.
This page has been generated by coqdoc