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

Set Implicit Arguments.

Lemma only_alloc_allocates:
  ∀ lab sb rf mo hmap edge h l
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (VAL: hmap_valid lab sb rf hmap (hb_fst edge))
    (EV : edge_valid lab sb rf edge)
    (HM : hmap edge = Hdef h)
    (ALL: h l ≠ HVnone)
    (NAb: ∀ x h, sb x (hb_fst edge) →
                      hmap (hb_sb x (hb_fst edge)) = Hdef h → h l = HVnone)
    (NAr: ∀ x h, rf (hb_fst edge) = Some x →
                      hmap (hb_rf x (hb_fst edge)) = Hdef h → h l = HVnone),
    lab (hb_fst edge) = Aalloc l.
Proof.
  ins; unfold hmap_valid, unique in VAL.
  desf; try first [progress f_equal|exfalso]; desc;
   try (destruct DISJ; desc); try clear TYP;
   destruct edge; ins; desf;
   try (by red in EV; rewrite Heq in EV; desc);
   try (by specialize (CONS_RF e´); rewrite EV, Heq in CONS_RF; desf);
   try (by rewrite HM in sEQ; inv sEQ);
   try (eapply qU0 in EV; desf);
   try (by rewrite HM in *; desf; unfold hupd in *; desf; desf;
           exploit NAb; eauto).

  {
    assert (X: In e´ posts) by (by apply qOK).
    eapply In_split in X; desf; rewrite !map_app, hsum_app in *;
    ins; rewrite hsum_cons, HM in ×.
    assert (hf l ≠ HVnone).
    {
      intro.
      eapply hplus_nalloc in qEQ; eauto; desf.
      eapply hplus_nalloc in qEQ; eauto; desf.
      eapply hplus_nalloc in qEQ4; eauto; desf.
    }
    eapply hsum_alloc in pEQ; eauto; desf; eauto.
    eby repeat (rewrite In_map in *; desf);
        exploit NAb; try eapply pOK.
  }

  {
    rewrite HM in ×.
    eapply hplus_preserves_alloc_r in qEQ; eauto.
    eapply hsum_alloc in pEQ; eauto; desf; eauto.
    eby repeat (rewrite In_map in *; desf);
        exploit NAb; try eapply pOK.
  }

  {
    rewrite qEQ in ×.
    eapply hplus_alloc in HM; eauto; desf.
    × unfold hupd in HM0; desf; subst; try done.
      clear ALL; exploit NAb; eauto; ins.
      symmetry in pEQ´; eapply hplus_nalloc in pEQ´; eauto; desf.
      by rewrite hupds in ×.
    × eapply hplus_alloc in HM; eauto; desf.
      + eapply hsum_alloc_sim in rfsSIM; eauto; desc.
        repeat (rewrite In_map in *; desf).
        by eapply rfsOK in rfsSIM2; eauto.
      + symmetry in pEQ´; eapply hplus_preserves_alloc_r in pEQ´; eauto.
  }

  {
    symmetry in pEQ´; eapply hplus_preserves_alloc_l in pEQ´; eauto.
    rewrite sEQ in HM; inv HM.
    clear - ALL; unfold hupd in *; desf; desf.
  }

  {
    rewrite HM in *; desf; unfold hupd in *; desf; desf;
    by exploit NAb; eauto; intro X; rewrite X in ×.
  }

  {
    by rewrite rEQ in HM; unfold hemp in *; desf.
  }

  {
    specialize (NAb pre);
    destruct (hmap (hb_sb pre e)); desf;
    specialize (NAb _ pU eq_refl).
    rewrite HM in UPD.
    eapply hplus_preserves_alloc_l in UPD; eauto.
    by rewrite <- initialize_alloc in UPD.
  }

  {
    specialize (NAb pre);
    destruct (hmap (hb_sb pre e)); desf;
    specialize (NAb _ pU eq_refl).
    eapply hplus_nalloc with (loc := l) in UPD ; eauto; desf.
      2: unfold initialize, hupd; desf; congruence.
    rewrite Hsim_sym in rfsSIM; eapply hplus_nalloc_sim in rfsSIM; eauto; desf.
    eapply hsum_nalloc with (h := (Hdef h)) in rfsSIM; eauto; desf.
    by rewrite <- HM; repeat (eapply In_map; repeat eexists; try eapply rfsOK).
  }

  {
    specialize (NAb pre);
    destruct (hmap (hb_sb pre e)); desf;
    specialize (NAb _ pU eq_refl).
    eapply hplus_nalloc with (loc := l) in UPD ; eauto; desf.
    2: unfold initialize, hupd; desf; congruence.
    rewrite HM, Hsim_sym in rfsSIM; eapply hplus_nalloc_sim in rfsSIM; eauto; desf.
  }


  {
    specialize (NAb pre);
    destruct (hmap (hb_sb pre e)); desf;
    specialize (NAb _ pU eq_refl).
    rewrite HM in ×.
    assert (SIM: Hsim (Hdef h) (Hdef hf)).
    {
      rewrite qEQ, pEQ.
      apply hplus_sim.
      × apply Hsim_refl.
        by intro CONTRA; rewrite CONTRA, !hplus_undef_l in ×.
      × eapply hplus_sim; try by rewrite Hsim_sym.
        by intro CONTRA; rewrite CONTRA, !hplus_undef_r in ×.
      × by intro CONTRA; rewrite CONTRA in ×.
    }
    destruct ALL; clear - SIM NAb.
    red in SIM; desf.
    specialize (SIM1 l); rewrite NAb in SIM1.
    red in SIM1; desf.
  }
Qed.

Lemma heap_loc_allocated :
  ∀ lab sb rf mo hmap V
    (ACYCLIC: IrreflexiveHBuRF sb rf )
    (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 (GET: hmap edge = Hdef h) l (LA: h l ≠ HVnone),
  ∃ c,
    lab c = Aalloc l ∧
    clos_refl_trans _ (happens_before_union_rf sb rf) c (hb_fst edge).
Proof.
  intros until h; revert h; pattern edge; eapply edge_depth_ind; eauto.
  clear edge EV IN; intros.
  specialize (VALID _ IN).
  destruct (classic (lab (hb_fst edge) = Aalloc l)) as [|NEQ].
    by eauto using clos_refl_trans.
  cut (∃ edge´ h´,
         edge_valid lab sb rf edge´ ∧
         hb_snd edge´ = Some (hb_fst edge) ∧
         hmap edge´ = Hdef h´ ∧
         h´ l ≠ HVnone).
    by intro; desf; exploit (IH edge´); eauto;
       [|intro; desf; repeat eexists; try edone];
       destruct edge´; ins; vauto; eauto using clos_refl_trans with hb.
  clear IH.
  apply NNPP; intro; destruct NEQ.
  eapply only_alloc_allocates; eauto.
    by ins; apply NNPP; intro; destruct H; eexists (hb_sb x _); ins; vauto.
  by ins; apply NNPP; intro; destruct H; eexists (hb_rf x _); ins; vauto.
Qed.

Definition independent sb rf T :=
  ∀ edge1 (IN1: In edge1 T) edge2 (IN2: In edge2 T)
      (HB: ∃ e, hb_snd edge1 = Some e ∧
           (e = hb_fst edge2 ∨ happens_before_union_rf sb rf e (hb_fst edge2))),
    False.

Lemma go_back_one :
  ∀ acts lab sb rf mo
    (FIN: ExecutionFinite acts lab sb)
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (CONS_A : ConsistentAlloc lab) hmap e
    (VALID : hmap_valid lab sb rf hmap e) hFR
    (ALLOC : ∀ hf loc,
               hFR = Hdef hf → hf loc ≠ HVnone →
               ∃ c, lab c = Aalloc loc ∧ c ≠ e),
   ∃ pres_sb pres_rf posts_sb posts_rf,
     NoDup pres_sb ∧
     NoDup pres_rf ∧
     NoDup posts_sb ∧
     NoDup posts_rf ∧
     (∀ x : actid, In x pres_sb ↔ sb x e) ∧
     (∀ x : actid, In x pres_rf ↔ rf e = Some x) ∧
     (∀ x : actid, In x posts_sb ↔ sb e x) ∧
     (∀ x : actid, In x posts_rf ↔ rf x = Some e) ∧
     (∀ h
       (EQ: hsum (map hmap (map (hb_sb^~ e) pres_sb)) +!+
            hsum (map hmap (map (hb_rf^~ e) pres_rf)) +!+ hFR =
            Hdef h),
      let hS := if excluded_middle_informative (ann_sink lab e) then hmap (hb_sink e) else hemp in
      ∃ h0 : val → HeapVal,
        hsum (map hmap (map (hb_sb e) posts_sb)) +!+
        hsum (map hmap (map (hb_rf e) posts_rf)) +!+ hS +!+ hFR =
        Hdef h0).
Proof.
  unfold hmap_valid, unique; ins; desf; desc; try (destruct DISJ; desc); try clear TYP;
    try (by red in a; rewrite Heq in a);
    try (by destruct n; red; rewrite Heq).

  Case Askip.
  {
    ∃ pres, nil, posts, nil; repeat (split; ins).
    by specialize (CONS_RF e); rewrite H, Heq in CONS_RF; desf.
    by specialize (CONS_RF x); rewrite H, Heq in CONS_RF; desf.

    rewrite pEQ, qEQ, !hplusA in EQ.
    rewrite hsum_nil, hplus_emp_l in ×.
    eby eexists.
  }


  Case Aload .
  {
    pose proof (has_rf_pres e FIN CONS_RF); desc.
    ∃ (pre :: nil), rfs, (post :: nil), nil; ins; repeat (split; ins; desf);
      rewrite ?hsum_one in *; eauto.

    by specialize (CONS_RF x); rewrite H, Heq in CONS_RF; desf.

    rewrite sEQ, qEQ, hsum_nil, !hplus_emp_l.
    eby rewrite (hplusC _ hFR), <- hplusA in EQ; eapply hplus_def_inv_l.
  }

  Case Aload .
  {
    ∃ (pre :: nil), rfs, (post :: nil), nil; ins; repeat (split; ins; desf);
      rewrite ?hsum_one, ?hsum_nil, ?hplus_emp_l in *; eauto.

    by specialize (CONS_RF x); rewrite H, Heq in CONS_RF; desf.

    rewrite sEQ in ×.
    rewrite <- hdef_alt, qEQ, !hplusA, hplusAC, (hplusAC _ hF hFR).
    rewrite pEQ, <- pEQ´, hplusA, (hplusAC _ hF), hplusAC,
            <- (ohlplus_same None), <- (ohlplus_same (Some _)),
            <- hplus_init1, (hplusC (hsingl _ _)) in EQ.
    rewrite <- (hplusA (hsingl _ _)).
    rewrite hplus_hsingl in *; try by vauto.
    ins; eapply hplus_sim_def; eauto; congruence.
   }


  Case Astore .
  {
    pose proof (has_rf_succs e FIN CONS_RF); desc.
    ∃ (pre :: nil), nil, (post :: nil), rfs; ins; repeat (split; ins; desf);
      rewrite ?sEQ, ?hsum_one, ?hplus_emp_l in *; eauto.

    by specialize (CONS_RF e); rewrite H, Heq in CONS_RF; desf.

    assert (M: hsum (map hmap (map (hb_rf e) rfs)) = hemp).
    {
      generalize (fun x ⇒ proj1 (INrfs x)); clear - rEQ.
      by induction rfs; ins; rewrite hsum_cons, IHrfs, hplus_emp_r; eauto.
    }
    rewrite M, hplus_emp_l in ×.
    by rewrite pEQ, qEQ in *; eauto using hdef_upd_alloc.
  }

  Case Astore .
  {
    ∃ (pre :: nil), nil, (post :: nil), rfs; ins; repeat (split; ins; desf);
      rewrite ?hsum_one, ?hsum_nil, ?hplus_emp_l in *; eauto.

    by specialize (CONS_RF e); rewrite H, Heq in CONS_RF; desf.

    rewrite pEQ in EQ.
    apply hplus_init_def with (l := l) in EQ.
    rewrite UPD, !hplusA, hdef_alt in EQ; desf.
    rewrite hplusAC in EQ.
    rewrite <- hdef_alt, <- (hplusA _ _ hFR), hplusAC.
    rewrite Hsim_sym in rfsSIM; eapply hplus_sim_def; eauto; congruence.
  }

  Case Aalloc.
  {
    ∃ (pre :: nil), nil, (post :: nil), nil; repeat (split; ins; desc);
      rewrite ?hsum_one, ?hsum_nil, ?hplus_emp_l in *; eauto; clear n;
      try (by desf);
      try (by specialize (CONS_RF e); rewrite H, Heq in CONS_RF; desf);
      try (by specialize (CONS_RF x); rewrite H, Heq in CONS_RF; desf).

    desf; rewrite pEQ, qEQ in *; destruct hFR; ins;
    rewrite hplus_unfold in *; desf; vauto;
    destruct n; intro l´; specialize (h0 l´);
    unfold hupd in *; desf; desf;
    specialize (ALLOC _ l eq_refl);
    destruct (hf0 l); desf; destruct ALLOC; desf;
    by edestruct H0; eapply CONS_A; rewrite ?H, ?Heq.
  }

  Case Afence.
  {
    ∃ (pre :: nil), nil, (post :: nil), nil; repeat (split; ins; desf);
      rewrite ?hsum_one, ?hsum_nil, ?hplus_emp_l in *; eauto.

    by specialize (CONS_RF e); rewrite H, Heq in CONS_RF; desf.
    by specialize (CONS_RF x); rewrite H, Heq in CONS_RF; desf.
    rewrite <- hdef_alt.
    apply hplus_sim_def with (h1 := hmap (hb_sb pre e)); try congruence.
    rewrite pEQ, qEQ in ×.
    apply hplus_sim; try congruence.
      by apply Hsim_refl; destruct hF; desf.
    apply hplus_sim; try done.
    by intro CONTRA; rewrite CONTRA, hplus_undef_r in ×.
  }
Qed.

Lemma get_pres_aux :
  ∀ sb rf V a
    (HC : hist_closed sb rf V)
    (IN : In a V),
   ∃ pres_sb pres_rf,
     << NDb : NoDup pres_sb >> ∧
     << NDr : NoDup pres_rf >> ∧
     << Pb : ∀ x, In x pres_sb ↔ sb x a >> ∧
     << Pr : ∀ x, In x pres_rf ↔ rf a = Some x >>.
Proof.
  intros; unfold NW.
  ∃ (undup (filter (fun x ⇒ mydec (sb x a)) V)),
         (undup (filter (fun x ⇒ mydec (rf a = Some x)) V)).
  do 2 (split; [by apply/uniqP; apply undup_uniq|]); split;
  ins; rewrite (In_mem_eq (mem_undup (T:=nat_eqType) _)), In_filter;
  unfold mydec; desf; split; ins; desf; eauto using hist_closedD with hb.
Qed.

Lemma get_pres :
  ∀ lab sb rf V
    (ACYCLIC: IrreflexiveHBuRF sb rf)
    (HC : hist_closed sb rf V) edge T
    (ND : NoDup T)
    (IN : In edge T)
    (INCL : ∀ edge, In edge T → In (hb_fst edge) V)
    (EVS : ∀ edge, In edge T → edge_valid lab sb rf edge)
    (DEEP : ∀ edge´, In edge´ T →
              happens_before_union_rf sb rf (hb_fst edge) (hb_fst edge´) → False)
    (IND: independent sb rf T),
   ∃ pres_sb pres_rf,
     let res := map (fun x ⇒ hb_sb x (hb_fst edge)) pres_sb ++
                map (fun x ⇒ hb_rf x (hb_fst edge)) pres_rf ++
                filter (fun x : hbcase ⇒ hb_fst x != hb_fst edge) T in
     << NDb : NoDup pres_sb >> ∧
     << NDr : NoDup pres_rf >> ∧
     << Pb : ∀ x, In x pres_sb ↔ sb x (hb_fst edge) >> ∧
     << Pr : ∀ x, In x pres_rf ↔ rf (hb_fst edge) = Some x >> ∧
     << ND´ : NoDup res >> ∧
     << METR: (depth_metric (happens_before_union_rf sb rf) V (map hb_fst res) <
               depth_metric (happens_before_union_rf sb rf) V (map hb_fst T) : Prop) >> ∧
     << INCL´: ∀ edge, In edge res → In (hb_fst edge) V >> ∧
     << EVS´ : ∀ edge, In edge res → edge_valid lab sb rf edge >> ∧
     << IND´ : independent sb rf res >>.
Proof.
  intros; exploit get_pres_aux; eauto; intro; desf.
  ∃ pres_sb, pres_rf; unfold NW;
  repeat (split; try done).

  by rewrite !nodup_app; intuition; try (apply nodup_map; try done; congruence);
     red; ins; rewrite ?In_app, ?In_filter, ?In_map in *; desf; ins;
     apply (IND _ IN2 _ IN); eexists; split; vauto.

  {
    apply depth_lt with (hb_fst edge);
    eauto using In_mapI.
      by ins; repeat (rewrite ?In_app, ?In_filter, ?In_map in *; desf; ins);
         rewrite ?Pr, ?Pb in *; eauto using In_mapI with hb; exfalso; eauto.

     intro; repeat (rewrite ?In_app, ?In_filter, ?In_map in *; desf; ins);
         rewrite ?Pr, ?Pb in *; eauto using In_mapI with hb.
     by destruct (eqP (hb_fst x) (hb_fst edge)).

     red; ins; repeat (rewrite ?In_app, ?In_filter, ?In_map in *; desf; ins);
     rewrite ?Pr, ?Pb in *; eauto with hb.

     by ins; rewrite In_map in *; desf; eauto.
  }

  by ins; rewrite ?In_app, ?In_filter, ?In_map in *; desf; ins;
     rewrite ?Pr, ?Pb in *; eauto with hb.

  by ins; rewrite ?In_app, ?In_filter, ?In_map in *; desf; ins;
     rewrite ?Pr, ?Pb in *; eauto.

  {
    red; ins; rewrite ?In_app, ?In_filter, ?In_map in *; desf; ins;
     rewrite ?Pw, ?Pb in *; try (injection HB; ins); subst; eauto with hb;
     try (revert IN0; case eqP; ins; congruence);
     try (apply (IND _ IN1 _ IN); eexists; split; eauto; right; vauto).
     × apply Pr in IN0; eapply ACYCLIC; vauto.
     × apply Pr in IN0; eapply ACYCLIC; vauto.
     × apply Pr in IN0; vauto.
     × apply happens_before_union_rf_trans with (b := x); vauto.
     × apply Pr in IN0; eapply ACYCLIC,happens_before_union_rf_trans; vauto.
     × apply Pr in IN0; eapply ACYCLIC,happens_before_union_rf_trans; vauto.
     × apply Pr in IN0; apply happens_before_union_rf_trans with (b := x); vauto.
  }
Qed.

Theorem independent_heap_compat :
  ∀ acts lab sb rf mo
    (FIN: ExecutionFinite acts lab sb)
    (ACYCLIC: IrreflexiveHBuRF sb rf)
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (CONS_A: ConsistentAlloc lab) hmap V
    (HC: hist_closed sb rf V)
    (VALID: hmap_valids lab sb rf hmap V)
    T (ND: NoDup T)
      (SSB: ∀ a b (IN: In (hb_sb a b) T), In a V)
      (SSW: ∀ a b (IN: In (hb_rf a b) T), In a V)
      (Ssink: ∀ a (IN: In (hb_sink a) T), In a V)
      (TSB: ∀ a b (IN: In (hb_sb a b) T), sb a b)
      (TSW: ∀ a b (IN: In (hb_rf a b) T), rf b = Some a)
      (Tsink: ∀ a (IN: In (hb_sink a) T), ann_sink lab a)
    (INDEP: independent sb rf T),
    ∃ h, hsum (map hmap T) = Hdef h.
Proof.
  intros until T; induction T using
    (well_founded_ind (wf_ltof
       (fun T ⇒ depth_metric (happens_before_union_rf sb rf) V (map hb_fst T)))).
  case_eq (depth_metric (happens_before_union_rf sb rf) V (map hb_fst T)); ins.
  {
    clear H.
    destruct T; unfold depth_metric in *; ins; vauto.
    assert (IN: In (hb_fst h) V) by (destruct h; ins; eauto).
    eapply In_implies_perm in IN; desf.
    rewrite (Permutation_count IN) in H0; ins; desf.
    unfold is_pred, mydec in Heq; ins; desf.
    exfalso; eauto using rt_refl.
  }
  exploit (get_deepest ACYCLIC HC (T:=T)).
    by intro; subst; clear - H0; induction V; ins.
    by destruct edge; ins; eauto.
  intro; clear n H0; desc.

  exploit get_pres; eauto; try (by intros []; eauto).
  ins; desf.

  destruct (H _ METR ND´); ins; eauto;
    try solve [by apply INCL´ in IN0|by apply EVS´ in IN0].
  clear H METR ND´.
  remember (hb_fst edge) as e; clear edge IN Heqe.

  rewrite !map_app, !hsum_app in ×.

  cut (∃ posts_sb posts_rf,
           NoDup posts_sb ∧ NoDup posts_rf ∧
           (∀ x, In x posts_sb ↔ sb e x) ∧
           (∀ x, In x posts_rf ↔ rf x = Some e) ∧
       ∃ h0,
         hsum (map hmap (filter (fun x ⇒ (hb_fst x != e) || (x == hb_sink e)) T)) +!+
         hsum (map hmap (map (hb_sb e) posts_sb)) +!+
         hsum (map hmap (map (hb_rf e) posts_rf)) = Hdef h0).
    intros; desf.
    assert (M := helper_perm_filter_post e T); desf.
    rewrite (hsum_perm (map_perm _ M)).
    destruct (@perm_from_subset _ posts_sb posts_sb0) as [? Psb].
      by eapply (Permutation_NoDup M) in ND; rewrite !nodup_app in ND;
         desf; eauto using NoDup_mapD.
      by symmetry in M; intros; apply H2, TSB, (Permutation_in _ M), In_appI2, In_appI1, In_mapI.

    destruct (@perm_from_subset _ posts_rf posts_rf0) as [? Prf].
      by eapply (Permutation_NoDup M) in ND; rewrite !nodup_app in ND;
         desf; eauto using NoDup_mapD.
      by symmetry in M; intros; apply H3, TSW, (Permutation_in _ M), In_appI2, In_appI2, In_mapI.

    rewrite (hsum_perm (map_perm _ (map_perm _ Psb))) in H4.
    rewrite (hsum_perm (map_perm _ (map_perm _ Prf))) in H4.

    eapply hplus_def_inv_l with (hf := h0); rewrite <- H4.
    rewrite !map_app, !hsum_app, !hplusA.
    f_equal; f_equal.
    by symmetry; rewrite hplusAC; f_equal.

  assert (ALLOC: ∀ hf loc,
            hsum (map hmap (filter (fun x ⇒ hb_fst x != e) T)) = Hdef hf →
            hf loc ≠ HVnone →
            ∃ c, lab c = Aalloc loc ∧ c ≠ e).
     intros; eapply hsum_alloc in H; eauto; desf.
     rewrite In_map in *; desf.
     rewrite In_filter in *; desf.
     exploit heap_loc_allocated; eauto; try (by destruct x0; ins; eauto).
     destruct (eqP (hb_fst x0) e); ins; desf; eexists,; eauto; intro; desf.
     by eapply clos_refl_trans_hbUrfE in x1; desf; eapply DEEP; eauto.

  red in VALID; desc.
  ins; exploit go_back_one; eauto; []; intro K; desc.
  exploit (NoDup_Permutation K NDb); [by intro; rewrite Pb|].
  exploit (NoDup_Permutation K0 NDr); [by intro; rewrite Pr|].
  clear Pb Pr; intros Pb Pr.
  rewrite (hsum_perm (map_perm _ (map_perm _ Pb))) in K7.
  rewrite (hsum_perm (map_perm _ (map_perm _ Pr))) in K7.
  edestruct K7; ins; eauto.
  ∃ posts_sb, posts_rf; repeat (split; ins).
  rewrite (hsum_perm ((map_perm _ (helper_filter_decide_sink _ ND)))).
  desf.
  by simpls; rewrite hsum_cons; rewrite hplusC, !hplusA; eexists; eauto.
  by specialize (Tsink _ i).
  eby rewrite !(hplusAC (hmap (hb_sink e))) in H; apply hplus_def_inv_r in H; desf;
      rewrite hplusC, hplusA; eexists.
  eby rewrite hplus_emp_l in H; rewrite hplusC, hplusA; eexists.
Qed.

Lemma independent_two :
  ∀ lab sb rf edge edge´,
    IrreflexiveHBuRF sb rf →
    edge_valid lab sb rf edge →
    edge_valid lab sb rf edge´ →
    hb_snd edge ≠ Some (hb_fst edge´) →
    hb_snd edge´ ≠ Some (hb_fst edge) →
    (¬ ∃ b, hb_snd edge = Some b ∧ happens_before_union_rf sb rf b (hb_fst edge´)) →
    (¬ ∃ b´, hb_snd edge´ = Some b´ ∧ happens_before_union_rf sb rf b´ (hb_fst edge )) →
    independent sb rf (edge :: edge´ :: nil).
Proof.
  ins; red; ins; desf.
  × subst edge2; destruct edge1; ins.
    + eby inv HB; eapply H, happens_before_union_rf_sb.
    + eby inv HB; eapply H, happens_before_union_rf_rf.
  × subst edge2; destruct edge1; ins.
    + eby inv HB; eapply H, happens_before_union_rf_sb.
    + eby inv HB; eapply H, happens_before_union_rf_rf.
  × subst edge2; destruct edge1; ins; eapply H, happens_before_union_rf_trans; vauto.
  × apply H5; repeat eexists; eauto.
  × apply H4; repeat eexists; eauto.
  × subst edge2; destruct edge1; ins; eapply H, happens_before_union_rf_trans; vauto.
Qed.

Lemma not_independent_two:
  ∀ acts lab sb rf mo hmap V
    (FIN: ExecutionFinite acts lab sb)
    (ACYCLIC: IrreflexiveHBuRF sb rf)
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (CONS_A: ConsistentAlloc lab)
    (HC: hist_closed sb rf V) (VALID: hmap_valids lab sb rf hmap V)
    edge1 edge2 (DIF: edge1 ≠ edge2) (IN1: In (hb_fst edge1) V) (IN1: In (hb_fst edge2) V)
    (EV1: edge_valid lab sb rf edge1) (EV2: edge_valid lab sb rf edge2)
    hf1 hf2 (MAP1: hmap edge1 = Hdef hf1) (MAP2: hmap edge2 = Hdef hf2)
    l (ALL1: hf1 l ≠ HVnone) (ALL2: hf2 l ≠ HVnone) (NA: is_nonatomic (hf1 l) ∨ is_nonatomic (hf2 l)),
  ¬ independent sb rf (edge1 :: edge2 :: nil).
Proof.
  ins; intro INDEP.
  exploit independent_heap_compat; try eassumption; ins; try (by clear NA; desf).
    by clear NA; apply NoDup_cons; eauto; ins; intro; desf; congruence.
  desc; rewrite MAP1, MAP2, hsum_two in x0.
  apply hplus_def_inv in x0; desc; clarify.
  specialize (DEFv l); clear - DEFv ALL1 ALL2 NA.
  destruct (hy l), (hz l); ins; desf.
Qed.

Lemma destruct_not_independent_two:
  ∀ lab sb rf (ACYCLIC: IrreflexiveHBuRF sb rf)
  edge1 edge2 (EV1: edge_valid lab sb rf edge1) (EV2: edge_valid lab sb rf edge2)
  (DEP: ¬ independent sb rf (edge1 :: edge2 :: nil)),
  (∃ b1, hb_snd edge1 = Some b1 ∧ clos_refl_trans _ (happens_before_union_rf sb rf) b1 (hb_fst edge2)) ∨
  (∃ b2, hb_snd edge2 = Some b2 ∧ clos_refl_trans _ (happens_before_union_rf sb rf) b2 (hb_fst edge1)).
Proof.
  ins; unfold independent in DEP.
  apply not_all_ex_not in DEP; desc.
  apply imply_to_and in DEP; desc.
  apply not_all_ex_not in DEP0; desc.
  apply imply_to_and in DEP0; desc.
  apply imply_to_and in DEP1; desc.
  ins; desf; desf; solve [ right; eexists,; vauto |
                           left; eexists,; vauto |
                           exfalso; destruct n0; ins; eapply ACYCLIC, t_trans; vauto
                         ].
Qed.