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

Set Implicit Arguments.

Hint Unfold imm_happens_before.

Lemma hupds A h l (y : A) : hupd h l y l = y.
Proof. unfold hupd; desf; congruence. Qed.

Lemma hist_closed_trans :
  ∀ sb rf V (HC: hist_closed sb rf V)
    a b (TR: clos_refl_trans _ sb a b) (IN: In b V), In a V.
Proof. induction 2; ins; eauto using hc_edge. Qed.

Lemma hist_closedD :
  ∀ sb rf V (HC: hist_closed sb rf V)
    a b (TR: happens_before_union_rf sb rf a b) (IN: In b V), In a V.
Proof. induction 2; ins; unfold imm_happens_before in *; desf; eauto using hc_edge. Qed.

Lemma happens_before_trans lab sb rf mo a b c :
  happens_before lab sb rf mo a b →
  happens_before lab sb rf mo b c →
  happens_before lab sb rf mo a c.
Proof. apply t_trans. Qed.

Lemma happens_before_union_rf_trans sb rf a b c :
  happens_before_union_rf sb rf a b →
  happens_before_union_rf sb rf b c →
  happens_before_union_rf sb rf a c.
Proof. apply t_trans. Qed.

Lemma happens_before_sb lab (sb : relation actid) rf mo a b :
  sb a b → happens_before lab sb rf mo a b.
Proof. ins; apply t_step; auto. Qed.

Lemma happens_before_sw lab sb rf mo a b :
  synchronizes_with lab sb rf mo a b → happens_before lab sb rf mo a b.
Proof. ins; apply t_step; auto. Qed.

Lemma happens_before_union_rf_sb (sb : relation actid) rf a b :
  sb a b → happens_before_union_rf sb rf a b.
Proof. ins; apply t_step; vauto. Qed.

Lemma happens_before_union_rf_rf (sb : relation actid) rf a b :
  rf b = Some a → happens_before_union_rf sb rf a b.
Proof. ins; apply t_step; vauto. Qed.

Lemma clos_trans_hbE :
  ∀ lab sb rf mo a b (HB: clos_trans actid (happens_before lab sb rf mo) a b),
    happens_before lab sb rf mo a b.
Proof.
  induction 1; vauto.
Qed.

Lemma clos_trans_hbUrfE :
  ∀ sb rf a b (HB: clos_trans actid (happens_before_union_rf sb rf) a b),
    happens_before_union_rf sb rf a b.
Proof.
  induction 1; vauto.
Qed.

Hint Immediate clos_trans_hbE : hb.
Hint Immediate clos_trans_hbUrfE : hb.

Hint Resolve
  happens_before_sb happens_before_sw happens_before_union_rf_sb happens_before_union_rf_rf
  happens_before_trans happens_before_union_rf_trans t_step hist_closedD : hb.

Lemma count_implies :
  ∀ (T: eqType) (f1 f2 : T → bool) (IMP : ∀ x, f1 x → f2 x) l,
  count f1 l ≤ count f2 l.
Proof.
  induction l; ins; desf; eauto.
  by rewrite IMP in Heq0.
Qed.

Lemma hasP´ :
  ∀ (T : eqType) (a : pred T) (l : list_predType T),
    reflect (∃ x : T, In x l ∧ a x) (has a l).
Proof.
  ins; case hasP; intro H; constructor; try red; intros; destruct H; desf.
    by apply/inP in H; eauto.
  by ∃ x; try apply/inP; eauto.
Qed.

Lemma clos_refl_transE X rel a b :
    clos_refl_trans X rel a b ↔ a = b ∨ clos_trans X rel a b.
Proof.
  split; ins; desf; try induction H; desf; eauto using clos_refl_trans, clos_trans.
Qed.

Lemma clos_refl_trans_hbE :
  ∀ lab sb rf mo a b,
    clos_refl_trans actid (happens_before lab sb rf mo) a b →
    happens_before lab sb rf mo a b ∨ a = b.
Proof.
  unfold happens_before; induction 1; desf; vauto.
Qed.

Lemma clos_refl_trans_hbUrfE :
  ∀ sb rf a b,
    clos_refl_trans actid (happens_before_union_rf sb rf) a b →
    happens_before_union_rf sb rf a b ∨ a = b.
Proof.
  induction 1; desf; vauto.
Qed.

Lemma helper_perm_filter_post :
  ∀ e T,
    ∃ posts_sb posts_rf,
      Permutation T (filter (fun x : hbcase ⇒ (hb_fst x != e) || (x == hb_sink e)) T ++
                     map (hb_sb e) posts_sb ++
                     map (hb_rf e) posts_rf).
Proof.
  induction T as [|hb T´]; ins; desc.
     by ∃ nil, nil.
  case eqP; ins; subst; [|eby do 2 eexists; eapply Permutation_cons].
  destruct hb; ins.
  × ∃ (e´ :: posts_sb), posts_rf; simpl.
    by apply Permutation_cons_app.
  × ∃ posts_sb, (e´ :: posts_rf); simpl.
    by rewrite <- appA in *; apply Permutation_cons_app.
  × desf; [∃ posts_sb, posts_rf | done].
    by rewrite <- app_comm_cons; apply Permutation_cons.
Qed.

Lemma helper_filter_decide_sink: ∀ a T (ND: NoDup T),
      Permutation (filter (fun x : hbcase ⇒ (hb_fst x != a) || (x == hb_sink a)) T)
        (if excluded_middle_informative (In (hb_sink a) T)
          then hb_sink a :: (filter (fun x : hbcase ⇒ hb_fst x != a) T)
          else (filter (fun x : hbcase ⇒ hb_fst x != a) T)).
    Proof.
      ins; induction T as [ | edge T´]; simpls; desf; apply nodup_cons in ND; desf;
      solve [
        apply Permutation_cons with (a := edge) in IHT´; ins; eapply perm_trans; eauto; apply perm_swap
        |
        apply perm_skip; apply IHT´; done
        |
        destruct n; right; done
        |
        destruct n; left; done
        |
        destruct Heq; left; done
        |
        destruct Heq; right; done
        |
        apply IHT´; done
      ].
    Qed.

Lemma has_rf_succs acts lab sb rf mo (a: actid) :
  ExecutionFinite acts lab sb →
  ConsistentRF_basic lab sb rf mo →
  ∃ (rfs: list actid),
    << NDrfs: NoDup rfs >> ∧
    << INrfs: ∀ x, In x rfs ↔ rf x = Some a >>.
Proof.
  ∃ (undup (filter (fun x ⇒ mydec (rf x = Some a)) acts)).
  unfold NW; split; [by apply/uniqP; apply undup_uniq|].
  intros; rewrite (In_mem_eq (mem_undup (T:=nat_eqType) _)), In_filter.
  unfold mydec; desf; split; ins; desf; eauto.
  split; try done.
  red in H, H0; desf.
  by generalize (CLOlab x), (H0 x); rewrite H1 in *; destruct (lab x); ins; desf; vauto; eapply H.
Qed.

Lemma has_rf_pres acts lab sb rf mo a :
  ExecutionFinite acts lab sb →
  ConsistentRF_basic lab sb rf mo →
  ∃ rfs,
    << NDrfs: NoDup rfs >> ∧
    << INrfs: ∀ x, In x rfs ↔ rf a = Some x >>.
Proof.
  ∃ (undup (filter (fun x ⇒ mydec (rf a = Some x)) acts)).
  unfold NW; split; [by apply/uniqP; apply undup_uniq|].
  intros; rewrite (In_mem_eq (mem_undup (T:=nat_eqType) _)), In_filter.
  unfold mydec; desf; split; ins; desf; eauto.
  split; try done.
  red in H, H0; desf.
  by generalize (CLOlab x), (H0 a); rewrite H1 in *; destruct (lab x); ins; desf; vauto; eapply H.
Qed.

Definition wf_ltof A (f : A → nat) :
  well_founded (fun x y ⇒ f x < f y).
Proof.
  by apply Wf_nat.well_founded_lt_compat with f; intros x y; case ltP.
Qed.

Lemma In_implies_perm A (x : A) l (IN: In x l) :
  ∃ l´, Permutation l (x :: l´).
Proof.
  induction l; ins; desf; eauto.
  destruct IHl; eauto using Permutation.
Qed.

Lemma Permutation_count A l l´ (P : Permutation (A:=A) l l´) f :
  count f l = count f l´.
Proof.
  induction P; ins; desf; congruence.
Qed.

Lemma count_eq_0: ∀ A f (lst: list A), count f lst = 0 ↔ ∀ x (IN: In x lst), ¬ f x.
Proof.
  split; ins.
  × intro.
    apply In_implies_perm in IN; desf.
    apply Permutation_count with (f := f) in IN.
    rewrite IN in H.
    rewrite <- (app_nil_l l´) , <- app_cons, count_app in H.
    by simpls; desf.
  × induction lst as [ | h tl]; simpls; desf.
    by exfalso; exploit (H h); vauto.
    by apply IHtl; ins; apply H; vauto.
Qed.

Lemma Permutation_hmap_valids :
  ∀ l l´ (P : Permutation l l´) lab sb rf hmap,
    hmap_valids lab sb rf hmap l →
    hmap_valids lab sb rf hmap l´.
Proof.
  by red; ins; apply H, Permutation_in with (l := l´); [eapply Permutation_sym | ].
Qed.

Lemma Permutation_hmap_valids_strong :
  ∀ l l´ (P : Permutation l l´) lab sb rf hmap,
    hmap_valids_strong lab sb rf hmap l →
    hmap_valids_strong lab sb rf hmap l´.
Proof.
  red; ins; split; red; red in H; desf; ins.
    eby eapply Permutation_hmap_valids.
  apply (RESTR e); try done.
  eby intro; destruct NIN; eapply Permutation_in.
  desf; [left | right; split]; try done.
  intro SB; destruct H0.
  eby unfold is_sb_out in *; split; desf; eapply Permutation_in.
Qed.

Lemma Permutation_hist_closed :
  ∀ l l´ (P : Permutation l l´) sb rf,
    hist_closed sb rf l →
    hist_closed sb rf l´.
Proof.
  red; ins; eapply H in HB.
    by apply (Permutation_in _ P) in HB.
  by eapply Permutation_in, IN; eauto using Permutation_sym.
Qed.

Lemma Consistent_perm :
  ∀ acts lab sb rf mo sc mt (CONS : Consistent acts lab sb rf mo sc mt)
         acts´ (EQ: perm_eq acts acts´),
    Consistent acts´ lab sb rf mo sc mt.
Proof.
  unfold Consistent; ins; desf; intuition.
  red in FIN; desf; split; red; ins; rewrite <- !(In_perm _ _ _ EQ) in *; eauto.
Qed.

Lemma weakConsistent_perm :
  ∀ acts lab sb rf mo sc mt (CONS : weakConsistent acts lab sb rf mo sc mt)
         acts´ (EQ: perm_eq acts acts´),
    weakConsistent acts´ lab sb rf mo sc mt.
Proof.
  unfold weakConsistent; ins; desf; intuition.
  red in FIN; desf; split; red; ins; rewrite <- !(In_perm _ _ _ EQ) in *; eauto.
Qed.

Lemma weakConsistent_Permutation :
  ∀ acts lab sb rf mo sc mt (CONS : weakConsistent acts lab sb rf mo sc mt)
         acts´ (EQ: Permutation acts acts´),
    weakConsistent acts´ lab sb rf mo sc mt.
Proof.
  unfold weakConsistent; ins; desf; intuition.
  red in FIN; desf; split; red; ins.
    by apply (Permutation_in _ EQ), CLOlab.
  by apply CLOsb in H; desf; split; apply (Permutation_in _ EQ).
Qed.

Lemma Permutation_flatten A l l´ (P : Permutation l l´) :
  Permutation (A:=A) (flatten l) (flatten l´).
Proof.
  induction P; ins; rewrite ?flatten_cons, <- ?appA;
  eauto using Permutation, Permutation_app, Permutation_app_comm.
Qed.

Lemma AcyclicStrong_implies_IrreflexiveHBuRF:
  ∀ lab sb rf mo, AcyclicStrong lab sb rf mo → IrreflexiveHBuRF sb rf.
Proof.
  ins.
  do 2 red; ins.
  eapply H; instantiate (1 := x).
  red in H0.
  revert H0; generalize x at 1 3; intros y H0.
  induction H0; eauto using clos_trans.
  destruct H0; eauto using t_step with hb.
Qed.

Hint Resolve AcyclicStrong_implies_IrreflexiveHBuRF.

Definition is_pred A (rel : A → A → Prop) B a :=
  has (fun b ⇒ mydec (clos_refl_trans A rel a b)) B.

Definition depth_metric A (rel: A → A → Prop) V a :=
  count (is_pred rel a) V.

Lemma clos_transK T (rel: relation T) x y :
  clos_trans _ (clos_trans _ rel) x y →
  clos_trans _ rel x y.
Proof. induction 1; eauto using clos_trans. Qed.

Lemma clos_refl_transD T rel a b :
  clos_refl_trans T rel a b → a = b ∨ clos_trans T rel a b.
Proof. induction 1; desf; eauto using clos_trans. Qed.

Lemma depth_lt (rel : relation actid) V A B
  (HB : ∀ a, In a A → ¬ In a B →
        ∃ b, In b B ∧ rel a b)
  b (IN : In b B) (NIN: ¬ In b A)
  (NHB: ∀ a, In a A → ¬ clos_trans _ rel b a)
  (SUB: ∀ b, In b B → In b V) :
  depth_metric rel V A < depth_metric rel V B.
Proof.
  unfold depth_metric; ins.
  assert (IMP: ∀ x, is_pred rel A x → is_pred rel B x).
    clear -HB; unfold is_pred, mydec; ins; desf.
    apply/@hasP´; apply/@hasP´ in H; destruct H; desf.
    destruct (inP x0 B); [by ∃ x0; ins; desf|].
    eapply HB in H; desf; eexists,; try edone; desf.
    by exfalso; eauto using rt_trans, rt_step.
  assert (P1: is_pred rel B b).
    unfold is_pred, mydec; desf.
    eapply In_split in IN; desf.
    rewrite has_app; ins; desf; clarsimp.
    by destruct n; vauto.
  assert (P2: is_pred rel A b = false).
    clear -NHB NIN; apply/hasP´; unfold mydec; intro; desf; eauto.
    by apply clos_refl_transD in c; unfold not in *; desf; eauto.
  assert (IN´ : In b V) by eauto.
  eapply In_split in IN´; desf; rewrite !count_app; ins.
  ins; rewrite P1, P2, addnS, ltnS.
  eauto using len_add, count_implies.
Qed.

Lemma edge_depth_ind lab sb rf V
  (ACYCLIC: IrreflexiveHBuRF sb rf)
  (HC: hist_closed sb rf V) (P : hbcase → Prop) :
  (∀ edge
    (IH: ∀ edge´ (EV : edge_valid lab sb rf edge´)
            (LT: happens_before_union_rf sb rf (hb_fst edge´) (hb_fst edge)),
      P edge´)
    (EV : edge_valid lab sb rf edge)
    (IN : In (hb_fst edge) V),
    P edge) →
  ∀ edge (EV : edge_valid lab sb rf edge), In (hb_fst edge) V → P edge.
Proof.
  intros until edge.
  generalize (S (depth_metric (happens_before_union_rf sb rf) V (hb_fst edge :: nil))),
             (ltnSn (depth_metric (happens_before_union_rf sb rf) V (hb_fst edge :: nil))).
  intro n´.
  revert edge; induction n´; ins.
  eapply H; ins; eapply IHn´; ins; eauto.
  2: by clear -HC LT H1; induction LT; unfold imm_happens_before in *; desf;
        eauto with hb.
  eapply ltn_len_trans, H0.
  eapply depth_lt; ins; desf; eauto; instantiate; rewrite addn0 in *;
    intro; desf; [rewrite H2 in *|]; eauto using t_step, t_trans, clos_trans_hbUrfE.
Qed.

Fixpoint find_max A (curr : A) f l :=
  match l with
    | nil ⇒ curr
    | x :: xs ⇒
      if f curr ≤ f x then find_max x f xs else find_max curr f xs
  end.

Lemma find_max_range :
  ∀ A (curr: A) f l,
    In (find_max curr f l) (curr :: l).
Proof.
  induction[curr] l; ins; desf; firstorder.
Qed.

Lemma find_max_greatest :
  ∀ A (x curr: A) f l (IN: In x (curr :: l)),
    f x ≤ f (find_max curr f l).
Proof.
  induction[x curr] l; ins; desf; eauto using len_trans, lenT.
Qed.

Lemma get_deepest :
  ∀ sb rf (ACYCLIC: IrreflexiveHBuRF sb rf)
         V (HC: hist_closed sb rf V)
         T (NNIL: T ≠ nil)
         (INCL: ∀ edge (IN: In edge T), In (hb_fst edge) V),
  ∃ edge,
    << IN: In edge T >> ∧
    << INe: In (hb_fst edge) V >> ∧
    << DEEP: ∀ edge´ (IN´: In edge´ T)
                 (HB´: happens_before_union_rf sb rf (hb_fst edge) (hb_fst edge´)),
               False >>.
Proof.
  destruct T; unfold depth_metric in *; ins; vauto.
  pose (f x := depth_metric (happens_before_union_rf sb rf) V (hb_fst x :: nil)).

  assert (IN:= find_max_range h f T).
  eexists,; unfold NW; repeat split; eauto; ins.
  assert (D := find_max_greatest f IN´); ins.
  specialize (INCL _ IN´); clear IN IN´; subst f.
  erewrite lenE, depth_lt in D; ins; desf; try intro; desf.
    by ∃ (hb_fst edge´),; vauto.
    by left; reflexivity.
    by rewrite H in *; eauto using t_step.
    by eauto using t_step, t_trans, clos_trans_hbUrfE.
Qed.

Fixpoint find_min A (curr : A) f l :=
  match l with
    | nil ⇒ curr
    | x :: xs ⇒
      if f x ≤ f curr then find_min x f xs else find_min curr f xs
  end.

Lemma find_min_range :
  ∀ A (curr: A) f l,
    In (find_min curr f l) (curr :: l).
Proof.
  induction[curr] l; ins; desf; firstorder.
Qed.

Lemma find_min_greatest :
  ∀ A (x curr: A) f l (IN: In x (curr :: l)),
    f (find_min curr f l) ≤ f x.
Proof.
  induction[x curr] l; ins; desf; eauto using len_trans, lenT.
Qed.

Lemma get_shallow :
  ∀ lab sb rf mo (ACYCLIC: AcyclicStrong lab sb rf mo)
         V (HC: hist_closed sb rf V)
         T (HC´: hist_closed sb rf (V ++ T)) (NNIL: T ≠ nil),
  ∃ e,
    << IN: In e T >> ∧
    << HC: hist_closed sb rf (e :: V) >>.
Proof.
  destruct T; unfold depth_metric in *; ins; vauto.
  pose (f x := depth_metric (hc_edge sb rf) (V ++ a :: T) (x :: nil)).

  assert (IN:= find_min_range a f T).

  eexists,; unfold NW; repeat split; eauto; ins.
  red; ins; destruct IN0; eauto; subst.
  generalize HB; eapply HC´ in HB; eauto.
  2: by destruct IN as [<-|]; eauto using In_appI1, In_appI2, In_cons, In_eq.
  rewrite In_app in HB; destruct HB as [|H]; vauto; intro.
  eapply find_min_greatest with (f:=f) in H.
  exfalso; clear IN.
  rewrite lenE in H; apply/negP in H; destruct H.
  eapply depth_lt; eauto using In_eq; ins; desf.
    by destruct HB; eauto using hc_edge with hb .
    by intro; desf; destruct HB; desf; eauto 8 with hb.
    intro H.
    assert (X: clos_trans actid (hc_edge sb rf) a0 a0) by eauto using clos_trans.
    apply (ACYCLIC a0); revert X; clear;
    generalize a0 at 1 3; induction 1; eauto using clos_trans;
    by destruct H; desf; auto with hb.
  assert (IN:= find_min_range a f T).
  by destruct IN as [<-|]; eauto using In_appI1, In_appI2, In_cons, In_eq.
Qed.

Lemma no_normals_on_rf :
  ∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
    a b (RF: rf b = Some a) hmap (VALID: hmap_valid lab sb rf hmap a)
    hfr (MAP: hmap (hb_rf a b) = Hdef hfr) l (ALL: hfr l ≠ HVnone) (NORMAL: HVlabeled (hfr l) HLnormal),
  False.
Proof.
  ins; red in VALID; desf; try (by specialize (CONS_RF b); desf; rewrite Heq in CONS_RF; desf).

  {
     desc; destruct DISJ.
     {
       desf; rewrite rEQ in MAP; inv MAP.
     }
     {
       desc; clear TYP; ins; desf.
       red in TRAN; desf.
       generalize (hplus_def_inv _ _ TRAN); intro D; desf.
       rewrite D, D0 in ×.
       symmetry in D; eapply hsum_preserves_label in D; desf; eauto.
         2: by do 2 (rewrite In_map; eexists,; eauto); rewrite rfsOK.
       symmetry in TRAN; eapply hplus_preserves_label in TRAN; desf; eauto.
       clear - TRAN4 TRAN TRAN3.
       specialize (TRAN3 l); destruct (hf0 l); desf; red in TRAN3; desf; ins; desf; red in TRAN4; desf.
     }
   }
Qed.

Lemma triangles_never_on_rf:
∀ edge lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (EV: edge_valid lab sb rf edge) hmap (VALID: hmap_valid lab sb rf hmap (hb_fst edge))
    hf (MAP: hmap edge = Hdef hf) l (ALL: hf l ≠ HVnone) (LAB: HVlabeled (hf l) HLtriangle),
  is_sb edge ∨ is_sink edge.
Proof.
  ins; apply NNPP; intro.
  apply not_or_and in H.
  destruct edge; ins; desf.
  ins; red in VALID; desf; try (by specialize (CONS_RF e´); desf; rewrite Heq in CONS_RF; desf).

  {
    desc; destruct DISJ.
     {
       desf; rewrite rEQ in MAP; inv MAP.
     }
     {
       desc; clear TYP; ins; desf.
       red in TRAN; desf.
       generalize (hplus_def_inv _ _ TRAN); intro D; desf.
       rewrite D, D0 in ×.
       symmetry in D; eapply hsum_preserves_label in D; desf; eauto.
         2: by do 2 (rewrite In_map; eexists,; eauto); rewrite rfsOK.
       symmetry in TRAN; eapply hplus_preserves_label in TRAN; desf; eauto.
       clear - TRAN4 TRAN TRAN3.
       specialize (TRAN3 l); destruct (hf1 l); desf; red in TRAN3; desf; ins; desf; red in TRAN4; desf.
     }
   }
Qed.

Lemma valid_accessD :
  ∀ lab sb rf hmap a
         (VALID : hmap_valid lab sb rf hmap a)
         (Aa : is_access (lab a)),
  ∃ pre hf,
    sb pre a ∧ hmap (hb_sb pre a) = Hdef hf
    ∧ hf (loc (lab a)) ≠ HVnone ∧ HVlabeled (hf (loc (lab a))) HLnormal.
Proof.
  ins.
  red in VALID; desf; desc; try destruct DISJ; desc; try clear TYP; red in pU; desf.

  {
    by eexists,; repeat split; eauto; ins; instantiate; rewrite IV.
  }

  {
    symmetry in pEQ´; eapply hplus_preserves_Rlabel in pEQ´; eauto; rewrite ? hupds; ins.
      eexists,; repeat split; eauto; ins.
      by intro N; rewrite N in ×.
      eby apply Rlabel_implies_label.
    vauto.
  }

  {
    eexists,; repeat split; eauto; ins.
    by intro N; rewrite N in ×.
  }

  {
    rewrite qEQ in UPD.
    rewrite hplusA in UPD; eapply hplus_preserves_Wlabel in UPD; eauto; rewrite ? hupds; ins.
      2: by instantiate (1 := HLnormal); vauto.
    eexists,; repeat split; eauto; ins.
    by intro N; unfold initialize in UPD; rewrite N, hupds in UPD.
    eby eapply Wlabel_implies_label, initialize_Wlabel.
  }
Qed.

Lemma valid_na_accessD :
  ∀ lab sb rf hmap a
         (VALID : hmap_valid lab sb rf hmap a)
         (NA : is_na (lab a)) pre
         (SB : sb pre a) hf
         (HM : hmap (hb_sb pre a) = Hdef hf),
  is_val (hf (loc (lab a))).
Proof.
  unfold hmap_valid, unique; ins; desf; desf; ins;
    match goal with H : _ |- _ ⇒ apply H in SB; subst; rewrite HM in × end;
    vauto; try (by destruct typ).
  by rewrite IV.
Qed.

Lemma valid_readD :
  ∀ lab sb rf hmap a
         (VALID : hmap_valid lab sb rf hmap a)
         (Ra : is_read (lab a)),
  ∃ pre hf,
    sb pre a ∧ hmap (hb_sb pre a) = Hdef hf
    ∧ HVlabeledR (hf (loc (lab a))) HLnormal.
Proof.
  ins.
  red in VALID; desf; desc; try destruct DISJ; desc; try clear TYP; red in pU; desf.

  {
    eexists,; repeat split; eauto; ins.
    by rewrite IV.
  }

  {
    eexists,; repeat split; eauto; ins.
    symmetry in pEQ´; eapply hplus_preserves_Rlabel in pEQ´; eauto.
    rewrite hupds; ins.
    vauto.
  }
Qed.