Require Import Vbase.
Require Import Relations Classical ClassicalDescription.
Require Import List Permutation Vlistbase Vlist extralib.
Require Import c11 fslassn fslassnsem fslassnlemmas fslmodel fslhmap ihc.
Require Import permission.

Set Implicit Arguments.

Lemma go_back_one_val PS PSg :
  ∀ lab sb rf mo hmap ga edge
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (VALID : hmap_valid lab sb rf hmap ga (hb_fst edge))
    (EV : edge_valid lab sb rf edge) hf g
    (GET : hmap edge = Hdef hf g) l v
    (LA : has_value (hf l) v)
    (NW: ¬ is_writeLV (lab (hb_fst edge)) l v),
  ∃ edge',
    edge_valid lab sb rf edge' ∧
    hb_snd edge' = Some (hb_fst edge) ∧
    ¬ is_writeL (lab (hb_fst edge)) l ∧
    ∃ hf' g', hmap edge' = @Hdef PS PSg hf' g' ∧ has_value (hf' l) v.
Proof.
  unfold hmap_valid, unique; ins; desf; desc; try destruct DISJ; desc; try clear TYP; desf.

  Case Askip.
  {
    destruct edge; ins; subst.
    × rewrite hdef_alt in DEF; desf; rewrite DEF in ×.
      assert (X := hplus_def_inv _ _ DEF); desf; rewrite X in ×.
      eapply hsum_valD in X; eauto; desf; desf.
        2: by repeat (rewrite In_map; eexists; split; try edone); eapply qOK.
      symmetry in DEF; eapply hplus_val_lD in DEF; ins; desf; try edone.
      eapply hplus_valD in EQ; eauto; desf.
      eapply hsum_eq_val in EQ; eauto; desf.
      repeat (rewrite In_map in *; desf); rewrite pOK in ×.
      by repeat (eexists; try edone).
    × by specialize (CONS_RF e'); rewrite EV, Heq in CONS_RF; desf.
    × rewrite hdef_alt in DEF; desf; rewrite GET, DEF in ×.
      symmetry in DEF; eapply hplus_val_rD in DEF; ins; desf; try edone.
      eapply hplus_valD in EQ; eauto; desf.
      eapply hsum_eq_val in EQ; eauto; desf.
      repeat (rewrite In_map in *; desf); rewrite pOK in ×.
      by repeat (eexists; try edone).
  }

  Case Aalloc.   {
     destruct edge; ins; subst;
      try (by red in EV; rewrite Heq in *; desf);
      try (by specialize (CONS_RF e'); rewrite EV, Heq in CONS_RF; desf); [].
    apply qU0 in EV; subst e'; rewrite GET in *; desf;
    apply hplus_gheap in qEQ; subst;
    unfold hupd in *; desf; desf;
    by ∃ (hb_sb pre e); repeat (eexists; try edone).
  }

  Case Aalloc.   {
     destruct edge; ins; subst;
      try (by red in EV; rewrite Heq in *; desf);
      try (by specialize (CONS_RF e'); rewrite EV, Heq in CONS_RF; desf); [].
    apply qU0 in EV; subst e'; rewrite GET in *; desf;
    apply hplus_gheap in qEQ; subst;
    unfold hupd in *; desf; desf;
    by ∃ (hb_sb pre e); repeat (eexists; try edone).
  }

  Case Aload .
  {
    destruct edge; ins; try by by specialize (CONS_RF e'); desf; rewrite Heq in *; desf.
    × apply qU0 in EV; subst e'; rewrite GET in *; desf.
      rewrite pEQ in ×.
      apply hplus_gheap in qEQ; subst.
      ∃ (hb_sb pre e); ins; repeat (split; ins; desf);
        rewrite ?hsum_one, ?hsum_nil, ?hplus_emp_l, ?hplus_emp_r in *; eauto.
    × rewrite GET in sEQ; inv sEQ.
  }

  Case Aload .
  {
    destruct edge; ins; try by specialize (CONS_RF e'); desf; rewrite Heq in *; desf.
    × apply qU0 in EV; subst e'; rewrite GET in *; desf.
      symmetry in qEQ; eapply hplus_valD in qEQ; eauto; desf.
        by unfold hupd in qEQ1; desf; desf.
      eapply hplus_valD in qEQ0; eauto; desf.
      + red in rfsSIM; desf.
        specialize (rfsSIM1 l).
        rewrite <- has_value_sim in qEQ3; eauto.
        eapply hsum_eq_val in rfsSIM; eauto; desf.
        repeat (rewrite In_map in *; desf).
        rewrite rfsOK in rfsSIM3.
        eexists (hb_rf _ _); repeat split; ins; eauto.
      + eapply hplus_valD in qEQ2; eauto; desf.
        symmetry in pEQ'; eapply hplus_val_rD in pEQ'; ins; desf; eauto.
        eexists (hb_sb _ _); repeat split; ins; eauto.
    × rewrite GET in sEQ; inv sEQ.
      clear - LA; unfold hupd in LA; desf; desf.
  }

  Case Astore .
  {
    destruct edge; ins; try by rewrite ?rEQ, ?sEQ in GET; inv GET.
    apply qU0 in EV; subst e'; rewrite GET in *; desf.
    apply hplus_gheap in qEQ; subst.
    ∃ (hb_sb pre e); ins; repeat (split; ins; desf);
      rewrite ?hsum_one, ?hsum_nil, ?hplus_emp_l, ?hplus_emp_r in *; eauto.
    × intro; desf; rewrite hupds in ×.
      red in LA; destruct NW; eauto.
    × by unfold hupd in *; ins; desf; vauto; exfalso; eauto.
  }

  Case Astore .
  {
    ∃ (hb_sb pre (hb_fst edge)); ins; do 2 (split; ins; desf);
      rewrite ?hsum_one, ?hsum_nil, ?hplus_emp_l, ?hplus_emp_r in *; eauto.
    cut (has_value (hf0 l) v).
    {
      intro V; split; [ | eby eexists _, _].
      intro; desf.
      symmetry in UPD; eapply hplus_ra_lD in UPD.
        2: by rewrite hupds; eauto.
      by desf; unfold initialize in UPD; desf; rewrite hupds in UPD.
    }
    {
      apply hplus_eq_gheap in ghostEQ; desf.
      destruct edge; ins.
      × rewrite (qU0 _ EV), GET in ×.
        rewrite <- hplusA in qEQ; symmetry in qEQ; assert (D := hplus_def_inv _ _ qEQ); desf.
        rewrite <- hplusA in UPD; rewrite D in ×.
        symmetry in qEQ; apply hplus_gheap in qEQ; subst.
        eapply hplus_val_lD in UPD; ins; desf; eauto.
        clear - UPD; unfold initialize, hupd in UPD; desf; try done.
        by rewrite Heq0.
      × red in rfsSIM; desf.
        generalize (hplus_def_inv _ _ rfsSIM0); ins; desf.
        symmetry in rfsSIM0; apply hplus_gheap in rfsSIM0; desf.
        specialize (rfsSIM1 l).
        assert (EQ := hplus_def_inv_l _ _ rfsSIM); desf; rewrite EQ in ×.
        eapply hsum_valD in EQ; eauto.
          2: by repeat (rewrite In_map; eexists; split; eauto); rewrite rfsOK.
        symmetry in rfsSIM; eapply hplus_val_lD in rfsSIM; ins; desf; eauto.
        rewrite (has_value_sim _ _ _ rfsSIM1) in rfsSIM.
        rewrite <- hplusA in UPD; eapply hplus_val_rD in UPD; ins; desf; eauto.
        clear - UPD; unfold initialize, hupd in UPD; desf; try done.
        by rewrite Heq0.
      × red in rfsSIM; desf.
        generalize (hplus_def_inv _ _ rfsSIM0); ins; desf.
        symmetry in rfsSIM0; apply hplus_gheap in rfsSIM0; desf.
        specialize (rfsSIM1 l).
        rewrite GET in ×.
        symmetry in rfsSIM; eapply hplus_val_rD in rfsSIM; ins; desf; eauto.
        rewrite (has_value_sim _ _ _ rfsSIM1) in rfsSIM.
        rewrite <- hplusA in UPD; eapply hplus_val_rD in UPD; ins; desf; eauto.
        clear - UPD; unfold initialize, hupd in UPD; desf; try done.
        by rewrite Heq0.
    }
  }

  Case Armw.
  {
    RMWin_heap.
    rewrite hdef_alt in DEF; desf; assert (DEF' := DEF).
    rewrite qEQ, rOutEQ, !hplusA, <- !(hplusAC sbg), ghostEQ, (hplusC _ (gheap _ _ _)),
              !(hplusAC (gheap _ _ _)) in DEF; desf.
    assert (D := hplus_def_inv_r _ _ DEF); desf; rewrite D in ×.
    symmetry in DEF; rewrite hplusC in DEF; apply hplus_gheap in DEF; subst.
    assert (H: has_value (hf0 l) v).
    {
      cut (Hsim (Hdef h3 g3) (Hdef hf0 g0)).
      {
         intro SIM; red in SIM; desf.
         specialize (SIM1 l).
         destruct edge; ins.
         × rewrite (qU0 _ EV), GET in ×.
           symmetry in DEF'; eapply hplus_val_lD in DEF'; ins; desf; eauto; desc.
           eapply has_value_sim; try edone.
           by rewrite HVsim_sym.
         × assert (R := hplus_def_inv_r _ _ DEF'); desf.
           apply hplus_def_inv_l in R; desf.
           rewrite R, hplusAC in DEF'.
           eapply hsum_valD in R; eauto; desc.
             2: by repeat (rewrite In_map; eexists; split; try edone); apply rfsOutOK.
           symmetry in DEF'; eapply hplus_val_lD in DEF'; ins; desf; eauto.
           eapply has_value_sim; try edone.
           by rewrite HVsim_sym.
         × rewrite GET, <- hplusA in DEF'.
           symmetry in DEF'; eapply hplus_val_rD in DEF'; ins; desf; eauto.
           eapply has_value_sim; try edone.
           by rewrite HVsim_sym.
      }
      {
        rewrite pEQ, rInEQ, !hplusA in DEFin.
        rewrite qEQ, rOutEQ, !hplusA, (hplusAC hrel'), (hplusAC hrel'), <- (hplusAC hacq') in DEF'.
        rewrite <- DEFin, <- D.
        do 2 rewrite (hplusAC hacq).
        rewrite <- (hplusAC hrel).
        by repeat (apply hplus_sim; try apply Hsim_refl;
           try by intro U; rewrite U, ?hplus_undef_l, ?hplus_undef_r in D);
           rewrite Hsim_sym.
      }
    }
    assert (L: l0 ≠ l).
    {
      intro; subst.
      rewrite pEQ, !hplusA in DEFin.
      eapply hplus_has_atomic_l with (l := l) in DEFin.
      by rewrite has_value_alt in H; desf; rewrite H in DEFin.
      by ins; desf; rewrite hupds.
    }

    eapply hplus_valD in DEFin; eauto; desf.
    × eexists (hb_sb _ _); repeat split; eauto.
    × eapply hsum_eq_val in DEFin0; eauto; desf.
      repeat (rewrite In_map in *; desf).
      eexists (hb_rf _ _); repeat split; eauto.
      by ins; apply rfsInOK.
  }

  Case Afence.
  {
    exploit FenceInDEF; eauto.
    rewrite hdef_alt in DEF; intro DEFin; desf; rewrite DEF, DEFin in ×.
    rewrite <- !hplusA in qEQ. symmetry in qEQ;
    assert (D := hplus_def_inv_l _ _ qEQ); desf; rewrite D in ×.
    symmetry in qEQ; apply hplus_gheap in qEQ; subst.
    cut (Hsim (Hdef h3 g3) (Hdef hf0 g0)).
    {
      intro SIM.
      red in SIM; desf.
      eexists (hb_sb _ _); repeat split; eauto.
      destruct edge; ins; try (by specialize (CONS_RF e'); rewrite EV, Heq in CONS_RF; desf);
        try (by red in EV; rewrite Heq in *; desf).
      rewrite (qU0 _ EV), GET in *; desf.
      specialize (SIM1 l); red in SIM1; desf; desf.
      ins; desf.
      repeat eexists; try edone.
      by rewrite Heq1.
    }
    {
      rewrite hplusA in D.
      rewrite Hsim_sym, pEQ, <- D.
      apply hplus_sim; try congruence.
        by apply Hsim_refl; intro U; rewrite U, !hplus_undef_l in ×.
      apply hplus_sim; try done.
      by intro U; rewrite U, hplus_undef_r in ×.
    }
  }
Qed.

Lemma is_write_weaken typ l v : is_writeLV typ l v → is_writeL typ l.
Proof. destruct typ; ins; desf. Qed.

Lemma is_write_weaken2 typ l : is_writeL typ l → is_write typ.
Proof. destruct typ; ins; desf. Qed.

Lemma is_access_weaken typ l v : is_writeLV typ l v → is_access typ.
Proof. destruct typ; ins; desf. Qed.

Hint Resolve is_write_weaken is_write_weaken2 is_access_weaken.

Lemma heap_loc_na_initialized2 PS PSg :
  ∀ acts lab sb rf mo hmap V
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (FIN: ExecutionFinite acts lab sb)
    (ACYCLIC: IrreflexiveHBuRF sb rf)
    (CONS_A: ConsistentAlloc lab)
    (HC: hist_closed sb rf V)
    (VALID: hmap_valids lab sb rf hmap V)
    edge (EV: edge_valid lab sb rf edge) (IN: In (hb_fst edge) V)
    h g (GET: hmap edge = Hdef h g) l v (LA: has_value (h l) v),
  ∃ cpre c hf g',
    sb cpre c ∧
    is_writeLV (lab c) l v ∧
    hmap (hb_sb cpre c) = @Hdef PS PSg hf g' ∧
    is_lvalue (hf l) ∧
    (c = hb_fst edge ∨ happens_before_union_rf sb rf c (hb_fst edge)) ∧
    (∀ d
      (HB1: d = hb_fst edge ∨ happens_before_union_rf sb rf d (hb_fst edge))
      (HB2: happens_before_union_rf sb rf c d),
      ¬ is_writeL (lab d) l).
Proof.
  intros until h; revert h; pattern edge; eapply edge_depth_ind; eauto.
  clear edge EV IN; intros.
  red in VALID; desc.
  generalize (VLD _ IN).

  destruct (classic (is_writeLV (lab (hb_fst edge)) l v)) as [|NEQ]; eauto.
  {
    ins; red in H0; unfold unique in *; desf; ins; desf.
      ∃ pre; repeat eexists; try eapply H2; eauto.
        by rewrite Heq.
      by red; ins; desf; eauto with hb.

    exfalso; destruct (hmap (hb_sb pre (hb_fst edge))); ins; desf.
    assert (N: has_value (hf l) v).
    {
      apply hplus_eq_gheap in ghostEQ; desf.
      destruct edge; ins.
      × exfalso.
        rewrite (qU0 _ EV), GET in ×.
        symmetry in qEQ; eapply hplus_ra_lD in qEQ.
          2: eby rewrite hupds.
        by desf; rewrite qEQ in ×.
      × red in rfsSIM; desf.
        generalize (hplus_def_inv _ _ rfsSIM0); ins; desf.
        symmetry in rfsSIM0; apply hplus_gheap in rfsSIM0; desf.
        specialize (rfsSIM1 l).
        assert (EQ := hplus_def_inv_l _ _ rfsSIM); desf; rewrite EQ in ×.
        eapply hsum_valD in EQ; eauto.
          2: by repeat (rewrite In_map; eexists; split; eauto); rewrite rfsOK.
        symmetry in rfsSIM; eapply hplus_val_lD in rfsSIM; ins; desf; eauto.
        rewrite (has_value_sim _ _ _ rfsSIM1) in rfsSIM.
        rewrite <- hplusA in UPD; eapply hplus_val_rD in UPD; ins; desf; eauto.
        by clear - UPD; unfold initialize, hupd in UPD; desf.
      × red in rfsSIM; desf.
        generalize (hplus_def_inv _ _ rfsSIM0); ins; desf.
        symmetry in rfsSIM0; apply hplus_gheap in rfsSIM0; desf.
        specialize (rfsSIM1 l).
        rewrite GET in ×.
        symmetry in rfsSIM; eapply hplus_val_rD in rfsSIM; ins; desf; eauto.
        rewrite (has_value_sim _ _ _ rfsSIM1) in rfsSIM.
        rewrite <- hplusA in UPD; eapply hplus_val_rD in UPD; ins; desf; eauto.
        by clear - UPD; unfold initialize, hupd in UPD; desf.
    }
    clear - UPD N.
    symmetry in UPD; eapply hplus_ra_lD in UPD.
      2: eby rewrite hupds.
    by desf; unfold initialize in UPD; desf; rewrite hupds in UPD.

    exfalso; destruct (hmap (hb_sb pre (hb_fst edge))); ins; desf.
    assert (N: has_value (hf l) v).
    {
      apply hplus_eq_gheap in ghostEQ; desf.
      destruct edge; ins.
      × exfalso.
        rewrite (qU0 _ EV), GET in ×.
        symmetry in qEQ; eapply hplus_ra_lD in qEQ.
          2: eby rewrite hupds.
        by desf; rewrite qEQ in ×.
      × red in rfsSIM; desf.
        generalize (hplus_def_inv _ _ rfsSIM0); ins; desf.
        symmetry in rfsSIM0; apply hplus_gheap in rfsSIM0; desf.
        specialize (rfsSIM1 l).
        assert (EQ := hplus_def_inv_l _ _ rfsSIM); desf; rewrite EQ in ×.
        eapply hsum_valD in EQ; eauto.
          2: by repeat (rewrite In_map; eexists; split; eauto); rewrite rfsOK.
        symmetry in rfsSIM; eapply hplus_val_lD in rfsSIM; ins; desf; eauto.
        rewrite (has_value_sim _ _ _ rfsSIM1) in rfsSIM.
        rewrite <- hplusA in UPD; eapply hplus_val_rD in UPD; ins; desf; eauto.
        by clear - UPD; unfold initialize, hupd in UPD; desf.
      × red in rfsSIM; desf.
        generalize (hplus_def_inv _ _ rfsSIM0); ins; desf.
        symmetry in rfsSIM0; apply hplus_gheap in rfsSIM0; desf.
        specialize (rfsSIM1 l).
        rewrite GET in ×.
        symmetry in rfsSIM; eapply hplus_val_rD in rfsSIM; ins; desf; eauto.
        rewrite (has_value_sim _ _ _ rfsSIM1) in rfsSIM.
        rewrite <- hplusA in UPD; eapply hplus_val_rD in UPD; ins; desf; eauto.
        by clear - UPD; unfold initialize, hupd in UPD; desf.
    }
    clear - UPD N.
    symmetry in UPD; eapply hplus_ra_lD in UPD.
      2: eby rewrite hupds.
    by desf; unfold initialize in UPD; desf; rewrite hupds in UPD.

    exfalso; destruct edge; ins.
    × rewrite (qU0 _ EV), GET in ×.
      symmetry in qEQ; eapply hplus_has_atomic_l with (l := l) in qEQ.
      by rewrite has_value_alt in LA; desf; rewrite LA in qEQ.
      by ins; desf; rewrite hupds.
    × rewrite hdef_alt in DEF; desf.
      assert (R := hplus_def_inv_r _ _ DEF); desf; apply hplus_def_inv_l in R; desf; rewrite R in ×.
      eapply hsum_valD in R; eauto.
        2: by repeat (rewrite In_map; eexists; split; try edone); apply rfsOutOK.
      exploit hplus_val_lD.
        by symmetry in DEF; rewrite hplusAC in DEF; exact DEF.
        eby ins; desf.
      intro NA.
      rewrite qEQ, !hplusA in DEF.
      eapply hplus_has_atomic_l with (l := l) in DEF.
      by rewrite has_value_alt in NA; desf; rewrite NA in DEF.
      by ins; desf; rewrite hupds.
    × rewrite hdef_alt in DEF; desf.
      rewrite GET in DEF.
      exploit hplus_val_rD.
        by symmetry in DEF; rewrite <- hplusA in DEF; exact DEF.
        eby ins; desf.
      intro NA.
      rewrite qEQ, !hplusA in DEF.
      eapply hplus_has_atomic_l with (l := l) in DEF.
      by rewrite has_value_alt in NA; desf; rewrite NA in DEF.
      by ins; desf; rewrite hupds.
  }


  
  exploit go_back_one_val; eauto.
  ins; desf.
  assert (HB: happens_before_union_rf sb rf (hb_fst edge') (hb_fst edge)).
    by destruct edge'; ins; desf; eauto with hb.
  exploit (IH edge'); eauto.
  intro; desf; repeat eexists; eauto with hb; ins; desf.

  {
    intro M; eapply x10, M; eauto.
    assert (N := M).
    eapply is_write_weaken2, valid_writeD in N.
      2: by eapply VLD; eauto using hist_closedD; desf.
    desc.
    replace (loc (lab d)) with l in × by (desf; clear - M; destruct (lab d); ins; desf).
    clear M; apply NNPP; intro M; apply not_or_and in M; desc.
    revert N1.
    assert (IND : independent sb rf (edge' :: hb_sb pre d :: nil)).
    {
      clear IH.
      assert (∀ b, hb_snd edge = Some b → happens_before_union_rf sb rf (hb_fst edge) b)
        by (destruct edge; ins; desf; eauto with hb).
      assert (∀ b', hb_snd edge' = Some b' → happens_before_union_rf sb rf (hb_fst edge') b')
        by (destruct edge'; ins; desf; eauto with hb).
      eapply independent_two; ins; eauto; intro; desf; eauto 6 with hb.
    }
    eapply independent_heap_compat in IND; eauto; try (by ins; desf; ins; desf; eauto with hb).
      2: eby eexists; split; eauto.
      2: by constructor; ins; intro; desf; ins; desf; eauto using t_trans, t_step.
    desc; simpls; rewrite hsum_two, N0, x3, hplus_unfold in IND; desfh; desfh.
    specialize (HEAPcompat l); red in x4; desfh; ins; desf; ins; desf.
    red in HEAPcompat0; desf.
    rewrite !permission_plusA, permission_plusAC in PSUMdef.
    eby apply nonextendable_full_permission in PSUMdef; pplus_eq_zero; eapply all_permissions_zero.
  }

  {
    intro M; eapply x10, M; eauto.
    assert (N := M).
    eapply is_write_weaken2, valid_writeD in N.
      2: by eapply VLD; eauto using hist_closedD; desf.
    replace (loc (lab d)) with l in × by (clear - M; destruct (lab d); ins; desf).
    clear M; apply NNPP; intro M; apply not_or_and in M; desc.
    revert N1.
    assert (IND : independent sb rf (edge' :: hb_sb pre d :: nil)).
    {
      clear IH.
      assert (∀ b, hb_snd edge = Some b → happens_before_union_rf sb rf (hb_fst edge) b)
        by (destruct edge; ins; desf; eauto with hb).
      assert (∀ b', hb_snd edge' = Some b' → happens_before_union_rf sb rf (hb_fst edge') b')
        by (destruct edge'; ins; desf; eauto with hb).
      eapply independent_two; ins; eauto; intro; desf; eauto 6 with hb.
    }
    eapply independent_heap_compat in IND; eauto; try (by ins; desf; ins; desf; eauto with hb).
      2: eby eexists; split; eauto.
      2: by constructor; ins; intro; desf; ins; desf; eauto using t_trans, t_step.
    desc; simpls; rewrite hsum_two, N0, x3, hplus_unfold in IND; desf; desf.
    specialize (HEAPcompat l); red in x4; desfh; ins; desf; ins; desf.
    red in HEAPcompat0; desf.
    rewrite !permission_plusA, permission_plusAC in PSUMdef.
    eby apply nonextendable_full_permission in PSUMdef; pplus_eq_zero; eapply all_permissions_zero.
  }
Qed.

Lemma two_access_cases PS PSg :
  ∀ pre a b acts lab sb rf mo hmap V hf g
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (FIN: ExecutionFinite acts lab sb)
    (ACYCLIC: IrreflexiveHBuRF sb rf)
    (CONS_A: ConsistentAlloc lab)
    (HC: hist_closed sb rf V)
    (VALID: hmap_valids lab sb rf hmap V)
    (INa : In a V)
    (INb : In b V)
    (SB : sb pre a) (HD: hmap (hb_sb pre a) = @Hdef PS PSg hf g) (IV: is_lvalue (hf (loc (lab a))))
    (B : is_access (lab b)) (LOC : loc (lab a) = loc (lab b)),
  a = b ∨ happens_before_union_rf sb rf a b ∨ happens_before_union_rf sb rf b a.
Proof.
  ins.
  red in VALID; desc.
  eapply valid_accessD in B; eauto; desf.
  apply NNPP; intro X; apply not_or_and in X; desc; apply not_or_and in X0; desc.
  rewrite LOC in ×.
  assert (IND: independent sb rf (hb_sb pre a :: hb_sb pre0 b :: nil)).
    by eapply independent_two; ins; eauto; intro; desf; eauto with hb.
  eapply independent_heap_compat in IND; eauto; try (by ins; desf; ins; desf; eauto with hb).
    2: eby eexists; split; eauto.
    2: by constructor; ins; intro; desf; ins; desf; eauto using t_trans, t_step.
  desf; ins; rewrite hsum_two, HD, B0, hplus_unfold in IND; desf; desf.
  by specialize (HEAPcompat (loc (lab b))); apply hvplusDEF_with_lvalue in HEAPcompat.
  Grab Existential Variables. done.
Qed.

Lemma go_back_one_na PS PSg :
  ∀ lab sb rf mo hmap ga edge
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (VAL: hmap_valid lab sb rf hmap ga (hb_fst edge))
    (EV : edge_valid lab sb rf edge) hf g
    (GET: hmap edge = Hdef hf g) l
    (LA : is_nonatomic (hf l))
    (NA : lab (hb_fst edge) ≠ Aalloc l),
  ∃ edge' hf' g',
    edge_valid lab sb rf edge' ∧
    hb_snd edge' = Some (hb_fst edge) ∧
    hmap edge' = @Hdef PS PSg hf' g' ∧
    is_nonatomic (hf' l).
Proof.
  unfold hmap_valid, unique; ins; desf; desc; try destruct DISJ; desc; try clear TYP; desf.

  Case Askip.
  {
    destruct edge; ins; subst.
    × rewrite hdef_alt in DEF; desf; rewrite DEF in ×.
      assert (X := hplus_def_inv _ _ DEF); desf; rewrite X in ×.
      eapply hsum_has_nonatomic in X; eauto; desf; desf.
        2: by repeat (rewrite In_map; eexists; split; try edone); eapply qOK.
      eapply hplus_has_nonatomic_l in DEF; ins; desf; try edone.
      eapply hplus_is_nonatomic in EQ; eauto; desf.
      eapply hsum_is_nonatomic in EQ; eauto; desf.
      repeat (rewrite In_map in *; desf); rewrite pOK in ×.
      by repeat (eexists; try edone).
    × by specialize (CONS_RF e'); rewrite EV, Heq in CONS_RF; desf.
    × rewrite hdef_alt in DEF; desf; rewrite GET, DEF in ×.
      eapply hplus_has_nonatomic_r in DEF; ins; desf; try edone.
      eapply hplus_is_nonatomic in EQ; ins; desf; eauto.
      eapply hsum_is_nonatomic in EQ; eauto; desf.
      repeat (rewrite In_map in *; desf); rewrite pOK in ×.
      by repeat (eexists; try edone).
  }
  
  Case Aalloc.   {
     destruct edge; ins; subst;
      try (by red in EV; rewrite Heq in *; desf);
      try (by specialize (CONS_RF e'); rewrite EV, Heq in CONS_RF; desf); [].
    apply qU0 in EV; subst e'; rewrite GET in *; desf;
    apply hplus_gheap in qEQ; subst;
    unfold hupd in *; desf; desf;
    by ∃ (hb_sb pre e); repeat (eexists; try edone).
  }

  Case Aalloc.   {
     destruct edge; ins; subst;
      try (by red in EV; rewrite Heq in *; desf);
      try (by specialize (CONS_RF e'); rewrite EV, Heq in CONS_RF; desf); [].
    apply qU0 in EV; subst e'; rewrite GET in *; desf;
    apply hplus_gheap in qEQ; subst;
    unfold hupd in *; desf; desf;
    by ∃ (hb_sb pre e); repeat (eexists; try edone).
  }

  Case Aload .
  {
    destruct edge; ins; try by by specialize (CONS_RF e'); desf; rewrite Heq in *; desf.
    × apply qU0 in EV; subst e'; rewrite GET in *; desf.
      rewrite pEQ in ×.
      apply hplus_gheap in qEQ; subst.
      eexists (hb_sb pre e), _, _; ins; repeat (split; ins; desf);
        rewrite ?hsum_one, ?hsum_nil, ?hplus_emp_l, ?hplus_emp_r in *; eauto.
    × rewrite GET in sEQ; inv sEQ.
  }

  Case Aload .
  {
    destruct edge; ins; try by specialize (CONS_RF e'); desf; rewrite Heq in *; desf.
    × apply qU0 in EV; subst e'; rewrite GET in *; desf.
      symmetry in qEQ; eapply hplus_is_nonatomic in qEQ; eauto; desf.
        by unfold hupd in qEQ1; desf; desf.
      eapply hplus_is_nonatomic in qEQ0; eauto; desf.
      + red in rfsSIM; desf.
        specialize (rfsSIM1 l).
        rewrite <- is_nonatomic_sim in qEQ3; eauto.
        eapply hsum_is_nonatomic in rfsSIM; eauto; desf.
        repeat (rewrite In_map in *; desf).
        rewrite rfsOK in rfsSIM3.
        eexists (hb_rf _ _), _; repeat split; ins; eauto.
      + eapply hplus_is_nonatomic in qEQ2; eauto; desf.
        eapply hplus_has_nonatomic_r in pEQ'; ins; desf; eauto.
        eexists (hb_sb _ _), _, _; repeat split; ins; eauto.
    × rewrite GET in sEQ; inv sEQ.
      clear - LA; unfold hupd in LA; desf; desf.
  }

  Case Astore .
  {
    destruct edge; ins; try by rewrite ?rEQ, ?sEQ in GET; inv GET.
    apply qU0 in EV; subst e'; rewrite GET in *; desf.
    apply hplus_gheap in qEQ; subst.
    eexists (hb_sb pre e); ins; repeat (split; ins; desf);
      rewrite ?hsum_one, ?hsum_nil, ?hplus_emp_l, ?hplus_emp_r in *; eauto.
    repeat eexists; eauto.
    unfold hupd in LA; desf; desf.
    red in IV; desf.
  }

  Case Astore .
  {
    eexists (hb_sb pre (hb_fst edge)), _, _; ins; repeat (split; try edone);
      rewrite ?hsum_one, ?hsum_nil, ?hplus_emp_l, ?hplus_emp_r in *; eauto.
    apply hplus_eq_gheap in ghostEQ; desf.
    destruct edge; ins.
    × rewrite (qU0 _ EV), GET in ×.
      rewrite <- hplusA in qEQ; symmetry in qEQ; assert (D := hplus_def_inv _ _ qEQ); desf.
      rewrite <- hplusA in UPD; rewrite D in ×.
      symmetry in qEQ; apply hplus_gheap in qEQ; subst.
      symmetry in UPD; eapply hplus_has_nonatomic_l in UPD; ins; desf; eauto.
      eby eapply initialize_is_nonatomic.
    × red in rfsSIM; desf.
      generalize (hplus_def_inv_l _ _ rfsSIM0); ins; desf.
      symmetry in rfsSIM0; apply hplus_gheap in rfsSIM0; desf.
      specialize (rfsSIM1 l).
      assert (EQ := hplus_def_inv_l _ _ rfsSIM); desf; rewrite EQ in ×.
      eapply hsum_has_nonatomic in EQ; eauto.
        2: by repeat (rewrite In_map; eexists; split; eauto); rewrite rfsOK.
      eapply hplus_has_nonatomic_l in rfsSIM; ins; desf; eauto.
      rewrite (is_nonatomic_sim _ _ rfsSIM1) in rfsSIM.
      rewrite <- hplusA in UPD; symmetry in UPD; eapply hplus_has_nonatomic_r in UPD; ins; desf; eauto.
      eby eapply initialize_is_nonatomic.
    × red in rfsSIM; desf.
      generalize (hplus_def_inv_l _ _ rfsSIM0); ins; desf.
      symmetry in rfsSIM0; apply hplus_gheap in rfsSIM0; desf.
      specialize (rfsSIM1 l).
      rewrite GET in ×.
      eapply hplus_has_nonatomic_r in rfsSIM; ins; desf; eauto.
      rewrite (is_nonatomic_sim _ _ rfsSIM1) in rfsSIM.
      rewrite <- hplusA in UPD; symmetry in UPD; eapply hplus_has_nonatomic_r in UPD; ins; desf; eauto.
      eby eapply initialize_is_nonatomic.
  }

  Case Armw.
  {
    RMWin_heap.
    rewrite hdef_alt in DEF; desf; assert (DEF' := DEF).
    rewrite qEQ, rOutEQ, !hplusA, <- !(hplusAC sbg), ghostEQ, (hplusC _ (gheap _ _ _)),
              !(hplusAC (gheap _ _ _)) in DEF; desf.
    assert (D := hplus_def_inv_r _ _ DEF); desf; rewrite D in ×.
    symmetry in DEF; rewrite hplusC in DEF; apply hplus_gheap in DEF; subst.
    assert (H: is_nonatomic (hf0 l)).
    {
      cut (Hsim (Hdef h3 g3) (Hdef hf0 g0)).
      {
         intro SIM; red in SIM; desf.
         specialize (SIM1 l).
         destruct edge; ins.
         × rewrite (qU0 _ EV), GET in ×.
           eapply hplus_has_nonatomic_l in DEF'; ins; desf; eauto.
           eapply is_nonatomic_sim; try eauto.
           by rewrite HVsim_sym.
         × assert (R := hplus_def_inv_r _ _ DEF'); desf.
           apply hplus_def_inv_l in R; desf.
           rewrite R, hplusAC in DEF'.
           eapply hsum_has_nonatomic in R; ins; desf; eauto.
             2: by repeat (rewrite In_map; eexists; split; try edone); apply rfsOutOK.
           eapply hplus_has_nonatomic_l in DEF'; ins; desf; eauto.
           eapply is_nonatomic_sim; try eauto.
           by rewrite HVsim_sym.
         × rewrite GET, <- hplusA in DEF'.
           eapply hplus_has_nonatomic_r in DEF'; ins; desf; eauto.
           eapply is_nonatomic_sim; try eauto.
           by rewrite HVsim_sym.
      }
      {
        rewrite pEQ, rInEQ, !hplusA in DEFin.
        rewrite qEQ, rOutEQ, !hplusA, (hplusAC hrel'), (hplusAC hrel'), <- (hplusAC hacq') in DEF'.
        rewrite <- D, <- DEFin.
        do 2 rewrite (hplusAC hacq).
        rewrite <- (hplusAC hrel).
        by repeat (apply hplus_sim; try apply Hsim_refl;
           try by intro U; rewrite U, ?hplus_undef_l, ?hplus_undef_r in D);
           rewrite Hsim_sym.
      }
    }
    assert (L: l0 ≠ l).
    {
      intro; subst.
      rewrite pEQ, !hplusA in DEFin.
      eapply hplus_has_atomic_l with (l := l) in DEFin.
      by destruct (hf0 l).
      by ins; desf; rewrite hupds.
    }

    eapply hplus_is_nonatomic in DEFin; eauto; desf.
    × eexists (hb_sb _ _), _, _; repeat split; eauto.
    × eapply hsum_is_nonatomic in DEFin0; eauto; desf.
      repeat (rewrite In_map in *; desf).
      eexists (hb_rf _ _), _, _; repeat split; eauto.
      by ins; apply rfsInOK.
  }

  Case Afence.
  {
    exploit FenceInDEF; eauto.
    rewrite hdef_alt in DEF; intro DEFin; desf; rewrite DEF, DEFin in ×.
    rewrite <- !hplusA in qEQ. symmetry in qEQ;
    assert (D := hplus_def_inv_l _ _ qEQ); desf; rewrite D in ×.
    symmetry in qEQ; apply hplus_gheap in qEQ; subst.
    cut (Hsim (Hdef h3 g3) (Hdef hf0 g0)).
    {
      intro SIM.
      red in SIM; desf.
      eexists (hb_sb _ _), _, _; repeat split; eauto.
      destruct edge; ins; try (by specialize (CONS_RF e'); rewrite EV, Heq in CONS_RF; desf);
        try (by red in EV; rewrite Heq in *; desf).
      rewrite (qU0 _ EV), GET in *; desf.
      specialize (SIM1 l); red in SIM1; desf; desf.
    }
    {
      rewrite hplusA in D.
      rewrite Hsim_sym, pEQ, <- D.
      apply hplus_sim; try congruence.
        by apply Hsim_refl; intro U; rewrite U, !hplus_undef_l in ×.
      apply hplus_sim; try done.
      by intro U; rewrite U, hplus_undef_r in ×.
    }
  }
Qed.

Lemma heap_loc_allocated_nonatomic PS PSg :
  ∀ lab sb rf mo hmap V
    (ACYCLIC: IrreflexiveHBuRF sb rf)
    (CONS_A: ConsistentAlloc lab)
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (HC: hist_closed sb rf V)
    (VALID: hmap_valids lab sb rf hmap V)
    edge (EV: edge_valid lab sb rf edge) (IN: In (hb_fst edge) V)
    h g (GET: hmap edge = Hdef h g) l
    (LA: is_nonatomic (h l)),
  ∃ cpre c hf g',
    sb cpre c ∧
    lab cpre = Aalloc l ∧
    hmap (hb_sb cpre c) = @Hdef PS PSg hf g' ∧
    is_nonatomic (hf l) ∧
    (cpre = hb_fst edge ∨ happens_before_union_rf sb rf cpre (hb_fst edge)).
Proof.
  intros until h; revert h; pattern edge; eapply edge_depth_ind; eauto.
  clear edge EV IN; intros.
  red in VALID; desc.
  generalize (VLD _ IN).
  destruct (classic (lab (hb_fst edge) = Aalloc l)) as [|NEQ]; eauto.
  × ins; destruct edge; ins.
    by repeat (eexists; try edone); vauto.
    by specialize (CONS_RF e'); rewrite EV, H in CONS_RF; desf.
    by red in EV; rewrite H in EV.
  × intros; exploit go_back_one_na; eauto; ins; desf.
    assert (HB: happens_before_union_rf sb rf (hb_fst edge') (hb_fst edge)).
      by destruct edge'; ins; desf; eauto with hb.
    exploit (IH edge'); eauto.
    intro; desf; repeat eexists; eauto using implies_trans with hb ; ins; desf; eauto.
Qed.