Auxiliary lemmas for the soundness proof


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.

Various helper lemmas


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 bhappens_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 bhappens_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 bhappens_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 ahappens_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 : Tbool) (IMP : x, f1 xf2 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 ]; ins; desc.
     by nil, nil.
  case eqP; ins; subst; [|eby do 2 eexists; eapply Permutation_cons].
  destruct hb; ins.
  × ( :: posts_sb), posts_rf; simpl.
    by apply Permutation_cons_app.
  × posts_sb, ( :: 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 : hbcasehb_fst x != a) T)
          else (filter (fun x : hbcasehb_fst x != a) T)).
    Proof.
      ins; induction T as [ | edge ]; 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 xmydec (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 xmydec (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 : Anat) :
  well_founded (fun x yf x < f y).
Proof.
  by apply Wf_nat.well_founded_lt_compat with f; intros x y; case ltP.
Qed.

A few lemmas about Permutations

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

Lemma Permutation_count A l (P : Permutation (A:=A) l ) f :
  count f l = count f .
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 ) , <- 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 (P : Permutation l ) lab sb rf hmap,
    hmap_valids lab sb rf hmap l
    hmap_valids lab sb rf hmap .
Proof.
  by red; ins; apply H, Permutation_in with (l := ); [eapply Permutation_sym | ].
Qed.

Lemma Permutation_hmap_valids_strong :
   l (P : Permutation l ) lab sb rf hmap,
    hmap_valids_strong lab sb rf hmap l
    hmap_valids_strong lab sb rf hmap .
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 (P : Permutation l ) sb rf,
    hist_closed sb rf l
    hist_closed sb rf .
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 (P : Permutation l ) :
  Permutation (A:=A) (flatten l) (flatten ).
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 moIrreflexiveHBuRF 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.

Depth metric


Definition is_pred A (rel : AAProp) B a :=
  has (fun bmydec (clos_refl_trans A rel a b)) B.

Definition depth_metric A (rel: AAProp) 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 ba = 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 BIn b V) :
  depth_metric rel V A < depth_metric rel V B.
Proof.
  unfold depth_metric; ins.
  assert (IMP: x, is_pred rel A xis_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.

A useful induction principle for happens-before graphs.

Lemma edge_depth_ind lab sb rf V
  (ACYCLIC: IrreflexiveHBuRF sb rf)
  (HC: hist_closed sb rf V) (P : hbcaseProp) :
  ( 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) VP 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 .
  revert edge; induction ; 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
    | nilcurr
    | 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.

Given a non-empty set of edges, T, there is always an edge whose source node does not happen before any of the sources of the other edges.

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
    | nilcurr
    | 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.

Some lemmas about validly annotated nodes

RF-edges carry only HLnabla labels

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 ); 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.

Every validly annotated memory access contains the accessed location in the domain of the heap of its incoming sb-edge

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.

The heap of every validly annotated non-atomic memory access maps the accessed location to some value.

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.


This page has been generated by coqdoc