Require Import List Vbase Varith Vlist extralib.
Require Import Classical ClassicalDescription IndefiniteDescription.
Require Import Permutation rslassn.

Set Implicit Arguments.

Transparent 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; 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;
    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; 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);
  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.
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 !orbA; 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).
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_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_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_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_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:
  ∀ h h1 h2 l v,
    Hdef h = hplus h1 h2 →
    (∀ h'', Hdef h'' = h1 → h'' l = HVval v) →
    h l = HVval v.
Proof.
  destruct h1, h2; ins; desf.
  specialize (H0 _ eq_refl); specialize (h0 l).
  rewrite H0 in *; ins; desf.
Qed.

Lemma hplus_val_rD:
  ∀ h h1 h2 l v,
    Hdef h = hplus h1 h2 →
    (∀ h'', Hdef h'' = h2 → h'' l = HVval v) →
    h l = HVval v.
Proof.
  ins; rewrite hplusC in *; eauto using hplus_val_lD.
Qed.

Lemma hplus_valD:
  ∀ h h1 h2 l v,
    hplus h1 h2 = Hdef h →
    h l = HVval v →
    ∃ hf1 hf2, h1 = Hdef hf1 ∧ h2 = Hdef hf2 ∧ (hf1 l = HVval v ∨ hf2 l = HVval v).
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 isrmw,
    hplus h1 h2 = Hdef h →
    h l = HVra PP QQ isrmw true →
    ∃ hf PP' QQ' isrmw',
      (h1 = Hdef hf ∨ h2 = Hdef hf) ∧ hf l = HVra PP' QQ' isrmw' true.
Proof.
  destruct h1, h2; unfold NW; ins; desf.
  specialize (h0 l); red in h0; desf; ins; desf; try destruct init, init0; ins;
    try solve [repeat (eexists; try edone); eauto].
Qed.

Definition hvplus_ra2_ret hv (QQ' : val → assn_mod) :=
  match hv with
    | HVra PP QQ isrmw init ⇒
      ∀ v, ∃ QR, Asim (sval (QQ v)) (Astar (sval (QQ' v)) QR)
    | _ ⇒ False
  end.

Lemma hvplus_ra2 hv hv' PP' QQ' isrmw' init' :
  hv = HVra PP' QQ' isrmw' init' →
  hvplusDEF hv hv' →
  hvplus_ra2_ret (hvplus hv hv') QQ'.
Proof.
  ins; subst; desf; ins; desf; ins; desf; 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 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_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_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_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_valD :
  ∀ h hs h'' l v,
    hsum hs = Hdef h →
    In (Hdef h'') hs →
    h'' l = HVval v →
    h l = HVval v.
Proof.
  intros until 0; induction[h] hs; ins; rewrite hsum_cons in ×.
  desf; eauto using hplus_val_rD.
  eapply hplus_val_lD; eauto; ins; desf.
Qed.

Lemma hsum_eq_val :
  ∀ hs h l v,
    hsum hs = Hdef h →
    h l = HVval v →
    ∃ hf, In (Hdef hf) hs ∧ hf l = HVval v.
Proof.
  induction hs; rewrite ?hsum_nil, ?hsum_cons in *; ins; desf.
    by inv H.
  eapply hplus_valD in H; eauto; desf; eauto.
  exploit IHhs; eauto; ins; desf; eauto.
Qed.

Lemma hsum_eq_ra_initD:
  ∀ h' hs l PP QQ isrmw,
    hsum hs = Hdef h' →
    h' l = HVra PP QQ isrmw true →
    ∃ h'' PP' QQ' isrmw',
      In (Hdef h'') hs ∧
      h'' l = HVra PP' QQ' isrmw' true.
Proof.
  intros until 0; induction[h' PP QQ isrmw] 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; eauto 10.
Qed.

Lemma hdef_upd_alloc hf l v' h h' :
  is_val (hf l) →
  hplus (Hdef hf) h = Hdef h' →
  ∃ h'', hplus (Hdef (hupd hf l (HVval v'))) h = Hdef h''.
Proof.
  intros; eapply hplus_def_inv in H0; desc.
  ∃ (hupd h' l (HVval v')).
  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' :
  is_val (hf l) →
  hplus (Hdef hf) h = Hdef h' →
  ∃ h'',
    hplus (Hdef (hupd hf l (HVval v'))) 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')); 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.

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.

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.
  f_equal; extensionality l'; ins; unfold initialize, hupd; desf; ins; desf.
Qed.

Lemma initialize_eq_raD hf l l' PP QQ isrmw init :
  initialize hf l l' = HVra PP QQ isrmw init →
  ∃ init', hf l' = HVra PP QQ isrmw init'.
Proof.
  unfold initialize, hupd; ins; desf; vauto.
Qed.

Lemma assn_sem_def P h : assn_sem P h → h ≠ Hundef.
Proof.
  induction P; ins; desf.
  eby eapply (H 0).
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.
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 hplus_ram_lD:
  ∀ h h1 h2 l PP QQ init,
    hplus (Hdef h1) h2 = Hdef h →
    h1 l = HVra PP QQ true init →
    ∃ PP' init',
      h l = HVra PP' QQ true init' ∧
      (∀ v h, assn_sem (sval (PP v)) h → assn_sem (sval (PP' v)) h) ∧
      ∃ hf, h2 = Hdef hf ∧
        (hf l = HVnone ∧ init = init'
         ∨ ∃ PP'' QQ'' isrmw'' init'',
              hf l = HVra PP'' QQ'' isrmw'' init'' ∧
              init' = (init || init'') ∧
              (∀ 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 init,
    hplus h1 (Hdef h2) = Hdef h →
    h2 l = HVra PP QQ true init →
    ∃ PP' init',
      h l = HVra PP' QQ true init' ∧
      (∀ v h, assn_sem (sval (PP v)) h → assn_sem (sval (PP' v)) h) ∧
      ∃ hf, h1 = Hdef hf ∧
        (hf l = HVnone ∧ init = init'
         ∨ ∃ PP'' QQ'' isrmw'' init'',
              hf l = HVra PP'' QQ'' isrmw'' init'' ∧
              init' = (init || init'') ∧
              (∀ 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 init,
    hplus (Hdef h1) h2 = Hdef h →
    h1 l = HVra PP QQ false init →
    ∃ PP' QQ' isrmw' init',
      h l = HVra PP' QQ' isrmw' 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
         ∨ ∃ PP'' QQ'' init'',
           hf l = HVra PP'' QQ'' isrmw' init'' ∧
           init' = (init || init'') ∧
           (∀ 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 init,
    hplus h1 (Hdef h2) = Hdef h →
    h2 l = HVra PP QQ false init →
    ∃ PP' QQ' isrmw' init',
      h l = HVra PP' QQ' isrmw' 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
         ∨ ∃ PP'' QQ'' init'',
           hf l = HVra PP'' QQ'' isrmw' init'' ∧
           init' = (init || init'') ∧
           (∀ 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 init,
    hsum hs = Hdef h →
    In (Hdef h'') hs →
    h'' l = HVra PP QQ isrmw init →
    ∃ PP' QQ' isrmw' init',
      h l = HVra PP' QQ' isrmw' init' ∧ (init → init') ∧ (isrmw → isrmw')
      ∧ (∀ v h, assn_sem (sval (PP v)) h → assn_sem (sval (PP' v)) h).
Proof.
  intros until 0; induction[h PP QQ] hs; ins; rewrite hsum_cons in ×.
  desf.
  destruct isrmw.
    by eapply hplus_ram_lD in H; eauto; desf; repeat (eexists; eauto); ins; desf.
    by eapply hplus_ra_lD in H; eauto; desf; repeat (eexists; eauto); ins; desf.
  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;
    try solve [by rewrite H2 | by apply H4 in H; rewrite e in *].
Qed.

Lemma hplus_raD:
  ∀ h h1 h2 l PP QQ isrmw init,
    hplus h1 h2 = Hdef h →
    h l = HVra PP QQ isrmw init →
    ∃ hf1 hf2,
      h1 = Hdef hf1 ∧ h2 = Hdef hf2
      ∧ << N: hf1 l ≠ HVnone ∨ hf2 l ≠ HVnone >>
      ∧ << L: hf1 l = HVnone ∨ ∃ PP' QQ' isrmw' init',
               hf1 l = HVra PP' QQ' isrmw' init' ∧
               (∀ v h, assn_sem (sval (PP' v)) h → assn_sem (sval (PP v)) h) >>
      ∧ << R: hf2 l = HVnone ∨ ∃ PP' QQ' isrmw' init',
               hf2 l = HVra PP' QQ' isrmw' 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 init,
    hplus h1 h2 = Hdef h →
    h l = HVra PP QQ isrmw init →
    ∃ hf1 hf2, h1 = Hdef hf1 ∧ h2 = Hdef hf2 ∧
     ( (hf1 l = HVnone ∧ ∃ PP' QQ', hf2 l = HVra PP' QQ' isrmw init ∧ PP' = PP ∧ QQ' = QQ)
      ∨ (hf2 l = HVnone ∧ ∃ PP' QQ', hf1 l = HVra PP' QQ' isrmw init ∧ PP' = PP ∧ QQ' = QQ)
      ∨ (∃ PP1 QQ1 isrmw1 init1 PP2 QQ2 isrmw2 init2,
            hf1 l = HVra PP1 QQ1 isrmw1 init1 ∧
            hf2 l = HVra PP2 QQ2 isrmw2 init2 ∧
            init = 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 init v,
    hplus h1 h2 = Hdef h →
    h l = HVra PP QQ isrmw init →
    ∃ hf PP' QQ' isrmw' init',
      (h1 = Hdef hf ∨ h2 = Hdef hf) ∧ hf l = HVra PP' QQ' isrmw' 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 init v,
    hsum hs = Hdef h' →
    h' l = HVra PP QQ isrmw init →
    ∃ h'' PP' QQ' isrmw' init',
      In (Hdef h'') hs ∧
      h'' l = HVra PP' QQ' isrmw' init' ∧
      (∀ h, assn_sem (sval (PP v)) h ↔ assn_sem (sval (PP' v)) h).
Proof.
  intros until 0; induction[h' PP QQ isrmw 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 6 eexists; eauto.
  by split; try edone; ins; rewrite H2.
Qed.

Lemma hplus_init1 E PP QQ isrmw init :
  hplus (hsingl E (HVra PP QQ isrmw init))
        (hsingl E (HVra Wemp Remp false true)) =
  hsingl E (HVra PP QQ isrmw true).
Proof.
  rewrite hplusC; simpl; desf; f_equal.
    exten; ins; unfold hupd; desf; ins; desf; f_equal.
    exten; ins; apply assn_mod_eqI; ins; desf; ins.
    by Asim_simpl; vauto.
  destruct n; intro v; unfold hupd; desf; split; ins; vauto.
  by destruct isrmw; vauto.
Qed.

Lemma hdef_initializeE hf E PP QQ isrmw init :
  hf E = HVra PP QQ isrmw init →
  Hdef (initialize hf E) = hplus (Hdef hf) (hsingl E (HVra Wemp Remp false true)).
Proof.
  rewrite hplusC; unfold initialize, hupd; ins; desf.
   f_equal; extensionality w; specialize (h w);
         red in h; ins; desf; ins; try congruence.
   rewrite Heq in *; desf; f_equal.
   extensionality y; eapply assn_mod_eqI; ins; desf; ins; Asim_simpl; vauto.
  by destruct n; intro m; ins; desf; ins; desf; split; ins; vauto; destruct isrmw; vauto.
Qed.

Opaque hplus.

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.