Require Import Vbase Relations ClassicalDescription ClassicalChoice.
Require Import List Permutation Sorting extralib.
Require Import c11 exps.
Require Import GpsFraction GpsSepAlg GpsModel GpsModelLemmas GpsGlobal.

Set Implicit Arguments.

Ltac kill_upd_irr :=
  intros; match goal with
            | |- ?l _ = ?l _ ⇒ unfold l
            | |- ?l _ _ = ?l _ _ ⇒ unfold l
            | |- ?l _ _ _ = ?l _ _ _ ⇒ unfold l
            | |- ?l _ _ _ _ = ?l _ _ _ _ ⇒ unfold l
            | |- ?l _ _ _ _ _ = ?l _ _ _ _ _ ⇒ unfold l
            | |- ?l _ _ _ _ _ _ = ?l _ _ _ _ _ _ ⇒ unfold l
          end;
  rewrite !map_upd_irr, ?updo; ins; intro;
  repeat (rewrite ?in_map_iff, ?in_flatten_iff in *; desf);
  match goal with H : _ |- _ ⇒ by edestruct H; eauto end.

Lemma in_sb_upd_irr :
  ∀ acts L te r a,
    (∀ b, te ≠ Tsb b a) →
    in_sb acts (upd L te r) a = in_sb acts L a.
Proof. kill_upd_irr. Qed.

Lemma in_rf_upd_irr :
  ∀ acts L te r a,
    (∀ b, te ≠ Trf b a) →
    in_rf acts (upd L te r) a = in_rf acts L a.
Proof. kill_upd_irr. Qed.

Lemma in_esc_upd_irr :
  ∀ acts L te r a,
    (∀ b, te ≠ Tesc b a) →
    in_esc acts (upd L te r) a = in_esc acts L a.
Proof. kill_upd_irr. Qed.

Lemma out_sb_upd_irr :
  ∀ acts L te r a,
    (∀ b, te ≠ Tsb a b) → te ≠ TsbS a →
    out_sb acts (upd L te r) a = out_sb acts L a.
Proof. kill_upd_irr. Qed.

Lemma out_rf_upd_irr :
  ∀ acts L te r a,
    (∀ b, te ≠ Trf a b) → te ≠ TrfS a →
    out_rf acts (upd L te r) a = out_rf acts L a.
Proof. kill_upd_irr. Qed.

Lemma out_esc_upd_irr :
  ∀ acts L te r EE a,
    (∀ b, te ≠ Tesc a b) →
    (∀ sigma, te ≠ TescS sigma a) →
    out_esc acts (upd L te r) EE a = out_esc acts L EE a.
Proof. kill_upd_irr. Qed.

Lemma incoming_upd_irr :
  ∀ acts L te r a,
    te_tgt te ≠ Some a →
    incoming acts (upd L te r) a = incoming acts L a.
Proof.
  unfold incoming; ins; desf;
  rewrite ?in_sb_upd_irr, ?in_rf_upd_irr, ?in_esc_upd_irr; ins; rupd;
  intro X; desf.
Qed.

Lemma outgoing_upd_irr :
  ∀ acts L te r EE a,
    te_src te ≠ a →
    outgoing acts (upd L te r) EE a = outgoing acts L EE a.
Proof.
  unfold outgoing; ins; desf;
  rewrite ?out_sb_upd_irr, ?out_rf_upd_irr, ?out_esc_upd_irr; ins; rupd;
  intro X; desf.
Qed.

Ltac kill_upd_in r :=
  intros; match goal with
            | |- ?l _ = _ ⇒ unfold l
            | |- ?l _ _ = _ ⇒ unfold l
            | |- ?l _ _ _ = _ ⇒ unfold l
            | |- ?l _ _ _ _ = _ ⇒ unfold l
            | |- ?l _ _ _ _ _ = _ ⇒ unfold l
            | |- ?l _ _ _ _ _ _ = _ ⇒ unfold l
          end; match goal with H: In _ _ |- _ ⇒
            apply In_NoDup_Permutation in H; desf;
            rewrite ?(Permutation_rsum (Permutation_map _ (Permutation_map _ H)));
            simpl; rupd; rewrite res_plus_emp_l;
            rewrite !map_upd_irr; try (by rewrite in_map_iff; intro; desf)
          end; rewrite (res_plusC r); try done; rewrite ?res_plusA; try done.

Lemma in_sb_upd_in :
  ∀ acts L r a b (IN: In a acts) (ND: NoDup acts),
    in_sb acts (upd L (Tsb a b) r) b =
    in_sb acts (upd L (Tsb a b) res_emp) b +!+ r.
Proof.
  kill_upd_in r.
Qed.

Lemma out_sb_upd_in :
  ∀ acts L r a b (IN: In b acts) (ND: NoDup acts),
    out_sb acts (upd L (Tsb a b) r) a =
    out_sb acts (upd L (Tsb a b) res_emp) a +!+ r.
Proof.
  kill_upd_in r.
Qed.

Lemma in_rf_upd_in :
  ∀ acts L r a b (IN: In a acts) (ND: NoDup acts),
    in_rf acts (upd L (Trf a b) r) b =
    in_rf acts (upd L (Trf a b) res_emp) b +!+ r.
Proof.
  kill_upd_in r.
Qed.

Lemma out_rf_upd_in :
  ∀ acts L r a b (IN: In b acts) (ND: NoDup acts),
    out_rf acts (upd L (Trf a b) r) a =
    out_rf acts (upd L (Trf a b) res_emp) a +!+ r.
Proof.
  kill_upd_in r.
Qed.

Lemma in_esc_upd_in :
  ∀ acts L r a b (IN: In a acts) (ND: NoDup acts),
    in_esc acts (upd L (Tesc a b) r) b =
    in_esc acts (upd L (Tesc a b) res_emp) b +!+ r.
Proof.
  kill_upd_in r.
Qed.

Lemma out_esc_upd_in1 :
  ∀ acts L EE r a b (IN: In b acts) (ND: NoDup acts),
    out_esc acts (upd L (Tesc a b) r) EE a =
    out_esc acts (upd L (Tesc a b) res_emp) EE a +!+ r.
Proof.
  kill_upd_in r.
Qed.

Lemma out_esc_upd_in2 :
  ∀ acts L EE r sigma a (IN: In sigma EE) (ND: NoDup EE),
    out_esc acts (upd L (TescS sigma a) r) EE a =
    out_esc acts (upd L (TescS sigma a) res_emp) EE a +!+ r.
Proof.
  by kill_upd_in r; f_equal; apply res_plusC.
Qed.

Lemma incoming_upd_in :
  ∀ acts L r te b (TGT: te_tgt te = Some b) (IN: In (te_src te) acts) (ND: NoDup acts),
    incoming acts (upd L te r) b =
    incoming acts (upd L te res_emp) b +!+ r.
Proof.
  unfold incoming; destruct te; ins; desf;
  [ rewrite in_sb_upd_in, !in_rf_upd_irr, !in_esc_upd_irr
  | rewrite !in_sb_upd_irr, in_rf_upd_in, !in_esc_upd_irr
  | rewrite !in_sb_upd_irr, !in_rf_upd_irr, in_esc_upd_in ]; ins;
  rewrite ?(res_plusC _ r), ?res_plusA, ?(res_plusAC r); ins.
Qed.

Lemma outgoing_upd_in_alt :
  ∀ acts L te b r EE,
    (∀ sigma, te = TescS sigma b → In sigma EE ∧ NoDup EE) →
    (∀ a, te_tgt te = Some a → In a acts ∧ NoDup acts) →
    te_src te = b →
    outgoing acts (upd L te r) EE b =
    outgoing acts (upd L te res_emp) EE b +!+ r.
Proof.
  ins; desf; rewrite <- !(res_plusC r).
  unfold outgoing; destruct te; ins; desf.
  × specialize (H0 _ eq_refl); desc; apply in_split in H0; desf.
    rewrite nodup_app, nodup_cons in *; ins; desf.
    unfold out_sb; rupd;
    rewrite !out_esc_upd_irr, !out_rf_upd_irr, !map_app, !rsum_app; ins.
    by rupd; rewrite !map_upd_irr, !res_plusA, res_plus_emp_l, !(res_plusAC r);
       ins; rewrite in_map_iff; intro; desf; eauto using in_eq.
  × by unfold out_sb; rupd;
       rewrite !out_rf_upd_irr, !out_esc_upd_irr, !map_upd_irr,
             !res_plusA, res_plus_emp_l;
       ins; rewrite !in_map_iff; intro; desf.
  × specialize (H0 _ eq_refl); desc; apply in_split in H0; desf.
    rewrite nodup_app, nodup_cons in *; ins; desf.
    unfold out_rf; rupd;
    rewrite !out_esc_upd_irr, !out_sb_upd_irr, !map_app, !rsum_app; ins.
    by rupd; rewrite !map_upd_irr, !res_plusA, res_plus_emp_l, !(res_plusAC r);
       ins; rewrite in_map_iff; intro; desf; eauto using in_eq.
  × by unfold out_rf; rupd;
       rewrite !out_sb_upd_irr, !out_esc_upd_irr, !map_upd_irr,
            !res_plusA, res_plus_emp_l, !(res_plusAC r);
       ins; rewrite !in_map_iff; intro; desf.
  × specialize (H0 _ eq_refl); desc; apply in_split in H0; desf.
    rewrite nodup_app, nodup_cons in *; ins; desf.
    unfold out_esc; rupd;
    rewrite !out_rf_upd_irr, !out_sb_upd_irr, !map_app, !rsum_app; ins.
    by rupd; rewrite !map_upd_irr, ?res_plusA, res_plus_emp_l, !(res_plusAC r);
       ins; rewrite in_map_iff; intro; desf; eauto using in_eq.
  × specialize (H _ eq_refl); desc; apply in_split in H; desf.
    rewrite nodup_app, nodup_cons in *; ins; desf.
    unfold out_esc; rupd;
    rewrite !out_sb_upd_irr, !out_rf_upd_irr, !map_app, !rsum_app; ins.
    by rupd; rewrite !map_upd_irr, !res_plusA, res_plus_emp_l, !(res_plusAC r);
       ins; rewrite in_map_iff; intro; desf; eauto using in_eq.
Qed.

Lemma outgoing_upd_in :
  ∀ acts L te b r1 r EE,
    (∀ sigma, te = TescS sigma b → In sigma EE ∧ NoDup EE) →
    (∀ a, te_tgt te = Some a → In a acts ∧ NoDup acts) →
    te_src te = b →
    L te = r1 →
    outgoing acts (upd L te (r1 +!+ r)) EE b =
    outgoing acts L EE b +!+ r.
Proof.
  ins; rewrite outgoing_upd_in_alt; ins; desf.
  rewrite <- updI with (f:=L) (a:=te) at 3.
  symmetry; rewrite outgoing_upd_in_alt, res_plusA; desf.
Qed.

Lemma outgoing_upd2_acc :
  ∀ acts L te1 r1 r te2 r2 EE b,
    (∀ sigma a, te1 = TescS sigma a ∨ te2 = TescS sigma a → In sigma EE ∧ NoDup EE) →
    (∀ a, te_tgt te1 = Some a ∨ te_tgt te2 = Some a → In a acts ∧ NoDup acts) →
    te_src te1 = te_src te2 →
    te1 ≠ te2 →
    L te1 = r1 →
    outgoing acts (upd (upd L te1 (r1 +!+ r)) te2 r2) EE b =
    outgoing acts (upd L te2 (r2 +!+ r)) EE b.
Proof.
  ins; destruct (eqP b (te_src te1)); clarify.
  2: rewrite !outgoing_upd_irr in *; congruence.
  rewrite updC, outgoing_upd_in; rupd; ins; desf; ins; eauto.
  do 2 (rewrite outgoing_upd_in_alt; ins; desf; ins; eauto; symmetry).
  apply res_plusA.
Qed.

Lemma outgoing_upd2_swap :
  ∀ acts L te1 r1 te2 r2 EE b,
    (∀ sigma a, te1 = TescS sigma a ∨ te2 = TescS sigma a → In sigma EE ∧ NoDup EE) →
    (∀ a, te_tgt te1 = Some a ∨ te_tgt te2 = Some a → In a acts ∧ NoDup acts) →
    te_src te1 = te_src te2 →
    te1 ≠ te2 →
    outgoing acts (upd (upd L te1 (r1 +!+ L te2)) te2 r2) EE b =
    outgoing acts (upd L te1 (r1 +!+ r2)) EE b.
Proof.
  ins; destruct (eqP b (te_src te1)); clarify.
  2: rewrite !outgoing_upd_irr in *; congruence.
  rewrite outgoing_upd_in_alt; ins; desf; eauto.
  rewrite updC, outgoing_upd_in_alt; ins; desf; eauto.
  rewrite <- (res_plusC (L te2)), <- res_plusA.
  rewrite updC, <- outgoing_upd_in_alt, updC, updI,
          res_plusA, <- outgoing_upd_in_alt; ins; desf; eauto.
Qed.

Lemma in_rf_upds acts L a b r :
  NoDup acts →
  In a acts →
  in_rf acts L b = res_emp →
  in_rf acts (upd L (Trf a b) r) b = r.
Proof.
  unfold in_rf; intros ND H.
  eapply In_NoDup_Permutation in H; desf.
  rewrite !(Permutation_rsum (Permutation_map _ (Permutation_map _ H))); simpl; rupd.
  rewrite map_upd_irr; try (by rewrite in_map_iff; intro; desf).
  by intro X; apply res_plus_eq_empD, proj2 in X; rewrite X, res_plus_emp_r.
Qed.

Lemma replace_out_rf :
  ∀ a b c L acts
    (NEQ: c ≠ b)
    (ND: NoDup acts)
    (EMP: L (Trf a b) = res_emp),
  out_rf acts (upd L (Trf a b) (res_strip (out_rf acts L a))) c = out_rf acts L c.
Proof.
  ins; unfold out_rf.
  destruct (classic (In b acts)); desf.
    destruct (classic (a = c)); desf.
      eapply In_NoDup_Permutation in H; eauto; desf.
      rewrite !(Permutation_rsum (Permutation_map _ (Permutation_map _ H))); ins.
      rewrite ?upds, !map_upd_irr, ?updo; ins; try by rewrite in_map_iff; intro; desf.
      by rewrite EMP, res_plus_emp_l, res_plusAC, res_plusC, res_plus_strip_idemp.
    by rewrite map_upd_irr, updo; ins; rewrite in_map_iff; intro; desf.
  by rewrite map_upd_irr, updo; ins; rewrite in_map_iff; intro; desf.
Qed.

Lemma replace_out_rf2 :
  ∀ a b acts c L
    (ND: NoDup acts)
    (INa: In a acts)
    (INb: In b acts)
    (EQ: L (TrfS a) = out_rf acts L a),
    out_rf (acts)
           (upd (upd L (TrfS a) (res_strip (out_rf acts L a)))
           (Trf a b) (out_rf acts L a)) c =
    out_rf acts L c.
Proof.
  ins; unfold out_rf in ×.
  destruct (classic (a = c)); desf.
  2: by rewrite !map_upd_irr; rupd; ins; try rewrite in_map_iff; intro; desf.
  eapply In_NoDup_Permutation in INb; eauto; desf.
  revert EQ.
  rewrite !(Permutation_rsum (Permutation_map _ (Permutation_map _ INb))); ins.
  rewrite !map_upd_irr; rupd; try by rewrite in_map_iff; intro; desf.
  rewrite <- res_plusA, res_plus_strip_l.
  case (classic (L (TrfS c) = Rundef)); [intros → | intro D]; ins.
  exploit res_plus_ubound; eauto; intro X; rewrite rknow_plusE in X; desf.
    by rewrite X0 at 2; rewrite !res_plusA, res_plus_strip_idemp.
  intro M; rewrite M in *; destruct (L (TrfS c)); ins.
Qed.

Lemma replace_edge_emp :
  ∀ A (a : A) f pi l
    (EMP: f a = res_emp)
    (ND: NoDup l)
    (IN : In a l),
  rsum (map (upd f a pi) l) = pi +!+ rsum (map f l).
Proof.
  ins; induction ND; ins.
  desf; rewrite ?upds, ?updo, ?EMP, ?res_plus_emp_l; try congruence.
    by rewrite map_upd_irr.
  by rewrite IHND, res_plusAC.
Qed.

Lemma helper2 A f (x : A) l :
  NoDup l →
  res_strip (f x) +!+ rsum (map f l) = Rundef →
  rsum (map f (undup (x :: l))) = Rundef.
Proof.
  ins; desf; rewrite undup_nodup; ins.
    eapply In_NoDup_Permutation in i; desf.
    rewrite (Permutation_rsum (Permutation_map f i)) in *; ins.
    by rewrite res_plusAC, <- res_plusA, res_plus_strip_idemp in H0.
  by rewrite <- (res_plus_strip_idemp (f x)), res_plusA, H0, res_plusC.
Qed.

Lemma replace_out_sb :
  ∀ a b c L r1 r2 acts (ND: NoDup acts) (IN : In b acts)
    (EMP: L (Tsb a b) +!+ L (TsbS a) = r1 +!+ r2),
  out_sb acts (upd (upd L (Tsb a b) r1) (TsbS a) r2) c = out_sb acts L c.
Proof.
  ins; unfold out_sb.
  destruct (classic (a = c)); desf; rupd; try congruence.
  2: by rewrite !map_upd_irr; ins; try by rewrite in_map_iff; intro; desf.
  eapply In_NoDup_Permutation in IN; eauto; desf.
  rewrite !(Permutation_rsum (Permutation_map _ (Permutation_map _ IN))); ins; rupd.
  rewrite !map_upd_irr; ins; try by rewrite in_map_iff; intro; desf.
  by rewrite <- !res_plusA; f_equal; rewrite res_plusC, <- EMP, res_plusC.
Qed.

Lemma out_esc_upd_in :
  ∀ acts L sigma b r1 r EE,
    In sigma EE →
    NoDup EE →
    L (TescS sigma b) = r1 →
    out_esc acts (upd L (TescS sigma b) (r1 +!+ r)) EE b =
    out_esc acts L EE b +!+ r.
Proof.
  ins; unfold out_esc; eapply in_split in H; desf;
  rewrite !map_app, !rsum_app; ins.
  rewrite nodup_app, nodup_cons in *; desf.
  unfold disjoint in *; ins.
  rupd; rewrite !map_upd_irr, !res_plusA; rewrite ?in_map_iff;
    try intro; desf; eauto.
  by rewrite (res_plusC _ r), !(res_plusAC r).
Qed.

Lemma replace_outgoing :
  ∀ te1 te2 b
    (S : te_src te1 = te_src te2)
    (T : te_tgt te1 = None)
    (S : te_tgt te2 = Some b)
    acts (ND: NoDup acts) (IN' : In b acts)
    EE (NDE: NoDup EE)
    (IN1: ∀ sigma, te1 = TescS sigma (te_src te1) → In sigma EE)
    L r1 r2 (EQ: L te1 +!+ L te2 = r1 +!+ r2) c,
  outgoing acts (upd (upd L te1 r1) te2 r2) EE c =
  outgoing acts L EE c.
Proof.
  ins; destruct (eqP c (te_src te1)); clarify.
  2: rewrite !outgoing_upd_irr; congruence.
  unfold outgoing.
  destruct te2; ins; desf;
    [ rewrite out_rf_upd_irr, out_esc_upd_irr; ins
    | rewrite out_sb_upd_irr, out_esc_upd_irr; ins
    | rewrite out_sb_upd_irr, out_rf_upd_irr; ins ];
  rewrite updC; ins; try (by intro; destruct te1; desf);
  (destruct te1; ins; desf;
    [ rewrite out_rf_upd_irr, out_esc_upd_irr; ins
    | rewrite out_sb_upd_irr, out_esc_upd_irr; ins
    | rewrite out_sb_upd_irr, out_rf_upd_irr; ins ]).
by rewrite replace_out_sb; ins; rewrite res_plusC, EQ, res_plusC.

rewrite <- (updI L (Tsb a b)) at 4.
rewrite out_sb_upd_in; ins; symmetry; rewrite out_sb_upd_in; ins.
rewrite !res_plusA; f_equal.
rewrite <- !res_plusA; f_equal.
unfold out_rf; rupd; rewrite !map_upd_irr; ins; try by rewrite in_map_iff; intro; desf.
by rewrite <- res_plusAC, <- res_plusA, EQ, res_plusA, res_plusAC.

rewrite res_plusAC; symmetry; rewrite res_plusAC; f_equal.
rewrite <- (updI L (Tsb a b)) at 1; do 2 (rewrite out_sb_upd_in; ins; symmetry).
rewrite <- (updI L (TescS sigma a)) at 3; do 2 (rewrite out_esc_upd_in2; auto; symmetry).
rewrite res_plusAC; symmetry; rewrite res_plusAC; f_equal.
by rewrite !res_plusA; f_equal; do 2 (rewrite res_plusC; symmetry).

rewrite <- !res_plusA; f_equal.
rewrite <- (updI L (Trf a b)) at 4.
rewrite out_rf_upd_in; ins; symmetry; rewrite out_rf_upd_in; ins.
rewrite res_plusAC; symmetry; rewrite res_plusAC; f_equal.
unfold out_sb; rupd; rewrite !map_upd_irr; ins; try by rewrite in_map_iff; intro; desf.
by rewrite ?res_plusA, res_plusAC; symmetry; rewrite res_plusAC; f_equal.

f_equal; f_equal.
rewrite <- (updI L (Trf a b)) at 2.
rewrite updC; ins.
do 2 (rewrite out_rf_upd_in; ins; symmetry).
rewrite updC; ins; unfold out_rf; rupd.
rewrite map_upd_irr; ins; try (by rewrite in_map_iff; intro; desf).
by rewrite ?res_plusA, res_plusAC; symmetry; rewrite res_plusAC; f_equal.

f_equal.
rewrite <- (updI L (Trf a b)) at 3; do 2 (rewrite out_rf_upd_in; ins; symmetry).
rewrite !res_plusA; f_equal.
rewrite <- (updI L (TescS sigma a)) at 3; do 2 (rewrite out_esc_upd_in2; auto; symmetry).
do 2 (rewrite res_plusAC; symmetry); f_equal.
by do 2 (rewrite res_plusC; symmetry).

rewrite ?res_plusA; do 2 (rewrite res_plusAC; symmetry); f_equal.
rewrite <- (updI L (Tesc a b)) at 4; do 2 (rewrite out_esc_upd_in1; ins; symmetry).
rewrite ?res_plusA; do 2 (rewrite res_plusAC; symmetry); f_equal.
unfold out_sb; rupd; rewrite map_upd_irr; ins; try (by rewrite in_map_iff; intro; desf).
by rewrite ?res_plusA; do 2 (rewrite res_plusAC; symmetry); f_equal.

f_equal.
rewrite <- (updI L (Tesc a b)) at 4; do 2 (rewrite out_esc_upd_in1; ins; symmetry).
rewrite ?res_plusA; do 2 (rewrite res_plusAC; symmetry); f_equal.
unfold out_rf; rupd; rewrite map_upd_irr; ins; try (by rewrite in_map_iff; intro; desf).
by rewrite ?res_plusA; do 2 (rewrite res_plusAC; symmetry); f_equal.

f_equal; f_equal.
rewrite <- (updI L (TescS sigma a)) at 2; do 2 (rewrite out_esc_upd_in2; auto; symmetry).
rewrite <- (updI L (Tesc a b)) at 2; do 2 (rewrite updC; ins; symmetry).
do 2 (rewrite out_esc_upd_in1; auto; symmetry).
by rewrite ?res_plusA; f_equal; do 2 (rewrite res_plusC; symmetry).
Qed.

Lemma safe_mon IE n e QQ r m : safe IE n e QQ r → m ≤ n → safe IE m e QQ r.
Proof.
  induction[m e QQ r] n; ins; desf; destruct m; ins; unfold NW;
  repeat split; ins; desf; try (by inversion H0); apply le_S_n in H0.
    exploit FORK; eauto; intro; desf; eauto 10.
  exploit STEP; eauto; intro M; desf.
  eexists; split; eauto; ins; exploit M0; eauto; desf; intro; desf; eauto.
Qed.

Lemma helper_plus_insb_rfS_def :
  ∀ a b acts amap sb rf mo sc L E
    (CONS: Consistent (b::acts) amap sb rf mo sc)
    (ND: NoDup (b :: acts))
    (PC : prefix_closed sb rf acts)
    (CC: compat amap sb rf L)
    (IN: In a acts)
    (NIN: ¬ In b acts)
    (LR : label_restr (b::acts) amap sb rf L E),
  in_sb (b :: acts) L b +!+ L (TrfS a) ≠ Rundef.
Proof.
  ins; assert (NEQ: a ≠ b) by congruence.
  replace (in_sb (b :: acts) L b) with
    (rsum (map L (map (Tsb^~ b) (filter (mydecf (sb^~ b)) acts)))).
  unfold in_sb; rewrite res_plusC.
  intro; eapply (CC (TrfS a :: map (Tsb^~ b) (filter (mydecf (sb^~ b)) acts))).
      constructor; [by rewrite in_map_iff; intro; desf|].
      by eapply nodup_map; try eapply nodup_filter; ins; try solve [by inv ND|congruence].
    by ins; desf; ins; try rewrite in_map_iff, mhbE in *; desf; ins; desf;
       try rewrite filter_In in *; desf; eauto using prefix_closed_hb.
    by ins; rewrite in_map_iff; intro; desf.
  unfold in_sb; ins.
  rewrite (proj1 LR), res_plus_emp_l, rsum_map_map_filter; auto.
    by ins; apply LR; ins.
  by intro; red in CONS; desc; edestruct ACYC; vauto.
Qed.

Lemma helper_plus_inc_escS_def :
  ∀ a b acts amap sb rf mo sc L E sigma
    (CONS: Consistent (b::acts) amap sb rf mo sc)
    (ND: NoDup (b :: acts))
    (PC : prefix_closed sb rf acts)
    (CC: compat amap sb rf L)
    (IN: In a acts)
    (NIN: ¬ In b acts)
    (LR : label_restr (b::acts) amap sb rf L E),
  incoming (b :: acts) L b +!+ L (TescS sigma a) ≠ Rundef.
Proof.
  ins; assert (NEQ: a ≠ b) by congruence.
  intro; eapply (CC (TescS sigma a :: map (Tsb^~ b) acts ++ map (Trf^~ b) acts ++ map (Tesc^~ b) acts)).
      constructor; [by rewrite ?in_app_iff, ?in_map_iff; intro; desf|].
      inv ND; rewrite !nodup_app; intuition; try eapply nodup_map; eauto;
      ins; try congruence;
      unfold disjoint; ins; rewrite ?in_app_iff, ?in_map_iff in *; desf.
    by ins; desf; ins; rewrite ?in_app_iff, ?in_map_iff, mhbE in *; desf; ins; desf;
       try rewrite filter_In in *; desf; eauto using prefix_closed_hb.
  ins; rewrite !map_app, !rsum_app.
  rewrite res_plusC, <- H; unfold incoming, in_sb, in_rf, in_esc; ins.
  red in CONS; desc.
  rewrite (proj1 LR), (proj1 (proj2 LR)), (proj1 (proj2 (proj2 LR))), !res_plus_emp_l; ins;
  intro; edestruct ACYC; vauto; eauto using hb_in_ct.
Qed.

Lemma helper_plus_inc_sbS_back_def :
  ∀ a b acts amap sb rf mo sc L E
    (CONS: Consistent acts amap sb rf mo sc)
    (ND: NoDup acts)
    (CC: compat amap sb rf L)
    (MO: mo b a)
    (LR : label_restr acts amap sb rf L E),
  incoming acts L a +!+ L (TsbS b) ≠ Rundef.
Proof.
  ins .
  intro; eapply (CC (TsbS b ::
      map (Tsb^~ a) (filter (mydecf (fun c ⇒ happens_before amap sb rf c a)) (acts)) ++
      map (Trf^~ a) (filter (mydecf (fun c ⇒ happens_before amap sb rf c a)) (acts)) ++
      map (Tesc^~ a) (filter (mydecf (fun c ⇒ happens_before amap sb rf c a)) (acts)))).
      constructor; [by rewrite ?in_app_iff, ?in_map_iff; intro; desf|].
      rewrite !nodup_app; intuition; try eapply nodup_map; eauto; ins; try congruence;
      unfold disjoint; ins; rewrite ?in_app_iff, ?in_map_iff in *; desf; eauto using nodup_filter.
    red in CONS; desf.
    ins.
    assert (b0 = a).
      by clear IN; ins; desf; ins; rewrite ?in_app_iff, ?in_map_iff in *; desf; ins; desf.
    desf; ins.
      red in Cmo; desc; rewrite mhbE in *; desf; destruct (Cmo _ _ MO) as (?&?&?).
        eby eapply Cmo2.
      by eapply Cmo2, Cmo0, Cmo3; try eapply HB; eauto.
    assert (HB': happens_before amap sb rf (te_src te) a).
      by clear IN'; ins; desf; ins; rewrite ?in_app_iff, ?in_map_iff in *; desf; ins; desf;
         rewrite ?filter_In in *; desf; unfold mydecf in *; desf.
    by clear IN; desf; rewrite ?in_app_iff, ?in_map_iff, mhbE in *; desf; ins; desf;
       try rewrite filter_In in *; desf; unfold mydecf in *; desf;
       edestruct ACYC; eauto using hb_trans, hb_in_ct.
  red in CONS; desc; ins.
  rewrite res_plusC, !map_app, !rsum_app, <- H; unfold incoming, in_sb, in_rf, in_esc; ins.
  by rewrite !rsum_map_map_filter; ins; apply LR; intro; desf; eauto.
Qed.

Lemma compat_upd1 :
  ∀ amap sb rf L
    (CC : compat amap sb rf L) te r
    (LT : res_lt r (L te)),
  compat amap sb rf (upd L te r).
Proof.
  red; ins.
  destruct (classic (In te E)) as [P|];
    [eapply In_NoDup_Permutation in P; desf;
     rewrite (Permutation_rsum (Permutation_map _ P)); ins |];
    rewrite !map_upd_irr; ins; rupd; eauto.
  intro; eapply (CC E); eauto.
  rewrite (Permutation_rsum (Permutation_map _ P)); ins.
  by red in LT; desf; rewrite <- LT, res_plusA, res_plusAC, H, res_plusC.
Qed.

Lemma compat_upd2 :
  ∀ amap sb rf L
    (CC : compat amap sb rf L) te1 te2
    (S : te_src te1 = te_src te2)
    (T : te_tgt te1 = None)
    (NEQ : te1 ≠ te2) r1
    (LT1 : res_lt r1 (L te1)) r2
    (LT2 : res_lt (r1 +!+ r2) (L te1 +!+ L te2)),
  compat amap sb rf (upd (upd L te1 r1) te2 r2).
Proof.
  red; ins.
  destruct (classic (In te2 E)) as [P|].
  2: by rewrite map_upd_irr; ins; eapply compat_upd1; eauto.
  eapply In_NoDup_Permutation in P; desf.
  red in LT2; desf.
  destruct (classic (In te1 l')) as [P'|].
    intro; eapply (CC E); ins; revert H.
    eapply In_NoDup_Permutation in P'; desf;
      eauto using Permutation_nodup, Permutation_sym, nodup_consD.
    rewrite !(Permutation_rsum (Permutation_map _ P)); simpl; try done; rupd.
    rewrite !(Permutation_rsum (Permutation_map _ P')); simpl; try done; rupd.
    rewrite !map_upd_irr; ins.
    2: by unfold not in *; eauto using Permutation_in, Permutation_sym, in_cons.
    by rewrite res_plusAC in *;
       rewrite <- res_plusA, <- LT2, res_plusA, res_plusAC, !res_plusA, H, res_plusC.
  intro; eapply (CC (te1 :: E)); ins; desf; desf; eauto.
    by econstructor; eauto;
       intro; destruct H; eapply (Permutation_in _ P) in H1; ins; desf.
    by rewrite S in *; eauto using Permutation_in, Permutation_sym, in_eq.
  revert H0;
  rewrite !(Permutation_rsum (Permutation_map _ P)); simpl; try done; rupd.
  rewrite !map_upd_irr, <- res_plusA, <- LT2; ins.
  by rewrite res_plusA, res_plusAC, res_plusA, H0, <- res_plusA, res_plusC.
Qed.

Lemma compat_upd2_bot :
  ∀ amap sb rf L
    (CC : compat amap sb rf L) te1 te2
    (T1 : te_tgt te1 = None)
    (T2 : te_tgt te2 = None)
    (HB : happens_before amap sb rf (te_src te1) (te_src te2))
    (NEQ : te1 ≠ te2) r1
    (LT1 : res_lt r1 (L te1)) r2
    (LT2 : res_lt (r1 +!+ r2) (L te1 +!+ L te2)),
  compat amap sb rf (upd (upd L te1 r1) te2 r2).
Proof.
  red; ins.
  destruct (classic (In te2 E)) as [P|].
  2: by rewrite map_upd_irr; ins; eapply compat_upd1; eauto.
  eapply In_NoDup_Permutation in P; desf.
  red in LT2; desf.
  destruct (classic (In te1 l')) as [P'|].
    intro; eapply (CC E); ins; revert H.
    eapply In_NoDup_Permutation in P'; desf;
      eauto using Permutation_nodup, Permutation_sym, nodup_consD.
    rewrite !(Permutation_rsum (Permutation_map _ P)); simpl; try done; rupd.
    rewrite !(Permutation_rsum (Permutation_map _ P')); simpl; try done; rupd.
    rewrite !map_upd_irr; ins.
    2: by unfold not in *; eauto using Permutation_in, Permutation_sym, in_cons.
    by rewrite res_plusAC in *;
       rewrite <- res_plusA, <- LT2, res_plusA, res_plusAC, !res_plusA, H, res_plusC.
  intro; eapply (CC (te1 :: E)); ins; desf; desf; eauto.
    by econstructor; eauto;
       intro; destruct H; eapply (Permutation_in _ P) in H1; ins; desf.
    eapply IND with (te:=te2) (te':=te');
    eauto using Permutation_in, Permutation_sym, in_eq, in_cons.
    by rewrite mhbE in *; desf; eauto using hb_trans.
  revert H0;
  rewrite !(Permutation_rsum (Permutation_map _ P)); simpl; try done; rupd.
  rewrite !map_upd_irr, <- res_plusA, <- LT2; ins.
  by rewrite res_plusA, res_plusAC, res_plusA, H0, <- res_plusA, res_plusC.
Qed.

Lemma compat_upd2_acc :
  ∀ amap sb rf L te1 r1 r
    (CC : compat amap sb rf (upd L te1 (r1 +!+ r))) te2
    (S : te_src te1 = te_src te2)
    (T1: te_tgt te1 = None)
    (T2: te_tgt te2 = None)
    (NEQ : te1 ≠ te2) r2
    (L2 : r2 = L te2 +!+ r),
  compat amap sb rf (upd (upd L te1 r1) te2 r2).
Proof.
  red; ins.
  destruct (classic (In te2 E)) as [P|].
  2: by rewrite map_upd_irr; ins; erewrite <- updss;
        eapply compat_upd1; eauto; rupd; vauto.
  eapply In_NoDup_Permutation in P; desf.
  destruct (classic (In te1 l')) as [P'|].
    intro; eapply (CC E); ins; revert H.
    eapply In_NoDup_Permutation in P'; desf;
      eauto using Permutation_nodup, Permutation_sym, nodup_consD.
    rewrite !(Permutation_rsum (Permutation_map _ P)); simpl; try done; rupd; try congruence.
    rewrite !(Permutation_rsum (Permutation_map _ P')); simpl; try done; rupd.
    rewrite !map_upd_irr; ins.
    2: by unfold not in *; eauto using Permutation_in, Permutation_sym, in_cons.
    by rewrite res_plusA in *; rewrite (res_plusAC r).
  intro; eapply (CC (te1 :: E)); ins; desf; desf; eauto.
    by econstructor; eauto;
       intro; destruct H; eapply (Permutation_in _ P) in H1; ins; desf.
    by rewrite S in *; eauto using Permutation_in, Permutation_sym, in_eq.
  revert H0;
  rewrite !(Permutation_rsum (Permutation_map _ P)); simpl; try done; rupd; try congruence.
  rewrite !map_upd_irr, !res_plusA; ins.
  by rewrite (res_plusAC (L te2)), H0, res_plusC.
Qed.

Lemma compat_upd2_swap :
  ∀ amap sb rf L te1 r1 r2
    (CC : compat amap sb rf (upd L te1 (r1 +!+ r2))) te2
    (S : te_src te1 = te_src te2)
    (T1: te_tgt te1 = None)
    (T2: te_tgt te2 = None)
    (NEQ : te1 ≠ te2),
  compat amap sb rf (upd (upd L te1 (r1 +!+ L te2)) te2 r2).
Proof.
  red; ins.
  destruct (classic (In te2 E)) as [P|];
   [eapply In_NoDup_Permutation in P; desf;
    rewrite !(Permutation_rsum (Permutation_map _ P)); simpl; try done;
    rupd; try congruence|];
    rewrite map_upd_irr; ins.

  destruct (classic (In te1 l')) as [P'|].
    intro; eapply (CC E); ins; revert H.
    eapply In_NoDup_Permutation in P'; desf;
      eauto using Permutation_nodup, Permutation_sym, nodup_consD.
    rewrite !(Permutation_rsum (Permutation_map _ P)); simpls; rupd;
      try congruence.
    rewrite !(Permutation_rsum (Permutation_map _ P')); simpls; rupd.
    rewrite !map_upd_irr; ins.
    by revert H; rewrite !res_plusA, !(res_plusAC (L te2)), !(res_plusAC r1).
  intro; eapply (CC (te1 :: E)); ins; desf; desf; eauto.
    by econstructor; eauto;
       intro; destruct H; eapply (Permutation_in _ P) in H1; ins; desf.
    by rewrite S in *; eauto using Permutation_in, Permutation_sym, in_eq.
  revert H0;
  rewrite !(Permutation_rsum (Permutation_map _ P)); simpls; rupd; try congruence.
  rewrite !map_upd_irr, !res_plusA; ins.
  by rewrite (res_plusAC (L te2)), H0, !res_plus_undef.

  destruct (classic (In te1 E)) as [P'|].
  2: by intro; eapply (CC E); eauto; rewrite map_upd_irr in *; ins.
  intro; eapply (CC (te2 :: E)); ins; rupd; desf; desf; eauto.
    by econstructor; eauto;
       intro; destruct H; eapply (Permutation_in _ P) in H1; ins; desf.
    by rewrite <- S in *; eauto.
  eapply In_NoDup_Permutation in P'; desf.
  revert H0;
  rewrite !(Permutation_rsum (Permutation_map _ P')); simpls; rupd.
  rewrite !map_upd_irr, !res_plusA; ins.
  by rewrite res_plusAC, !(res_plusAC r2), H0, !res_plus_undef.
Qed.

Lemma compat_upd3 :
  ∀ amap sb rf L te3 rr
    (CC : compat amap sb rf (upd L te3 rr)) te1 te2
    (S : te_src te1 = te_src te2)
    (T : te_tgt te1 = None)
    (TS : te_tgt te2 = Some (te_src te3))
    (T' : te_tgt te3 = None)
    (HB : happens_before amap sb rf (te_src te1) (te_src te3))
    (NEQ : te1 ≠ te2)
    (NEQ' : te1 ≠ te3) r1
    (LT1 : res_lt r1 (L te1)) r2 r3
    (LT2 : res_lt (r1 +!+ r2) (L te1 +!+ L te2))
    (LT3 : res_lt (r1 +!+ r3) (L te1 +!+ rr)),
  compat amap sb rf (upd (upd (upd L te1 r1) te2 r2) te3 r3).
Proof.
  red; ins.
  assert (NEQ'' : te2 ≠ te3) by congruence.
  destruct (classic (In te3 E)) as [P|].
  2: erewrite <- updss, map_upd_irr; ins.
  2: by rewrite !(updC (l':=te3)); ins; eapply compat_upd2; eauto; rupd.
  assert (¬ In te2 E) by (intro X; eapply (IND _ P _ X); eauto; vauto).
  rewrite updC, map_upd_irr; ins.
  clear te2 r2 LT2 H S TS NEQ NEQ''.
  erewrite <- updss, (updC (l:=te1)); ins.
  eapply compat_upd2_bot; eauto; rupd.
Qed.

Lemma compat_guar1 amap sb rf L sigma b r :
  compat amap sb rf (upd L (TescS sigma b) (L (TescS sigma b) +!+ r)) →
  compat amap sb rf (upd L (TsbS b) r).
Proof.
  intros.
  erewrite <- (updI L (TescS sigma b)), <- (updss L).
  eapply compat_upd2; eauto; ins; rupd; vauto.
Qed.

Lemma compat_guar2 amap sb rf L te r l pi :
  (res_get r l = p_uninit ∨ ∃ v, res_get r l = p_na pe_full v) →
  compat amap sb rf (upd L te r) →
  compat amap sb rf (upd L te (res_upd r l pi)).
Proof.
  repeat red; intros.
  exploit H0; eauto.
  revert H1.
  destruct (classic (In te E)) as [P|];
    [eapply In_NoDup_Permutation in P; desc; clarify;
     rewrite !(Permutation_rsum (Permutation_map _ P)); try done |]; simpl;
    rewrite !map_upd_irr; try done; rupd; eauto.
  destruct r; ins; desf;
  eapply lift_plus_none_inv in Heq2; desc; inv_lplus l0; desf; desf;
  rewrite H in *; destruct pi; ins; desf; desf.
Qed.

Lemma compat_mon_upd amap sb rf L a r :
  compat amap sb rf (upd L a (L a +!+ r)) →
  compat amap sb rf L.
Proof.
  repeat red; ins; apply (H E); auto.
  destruct (classic (In a E)) as [N|N];
   [apply In_NoDup_Permutation in N; desf;
    revert H0; rewrite !(Permutation_rsum (Permutation_map _ N)); ins|];
  rewrite map_upd_irr, ?upds, ?res_plusA; ins.
  by rewrite res_plusAC, H0, res_plusC.
Qed.

Lemma conform_upd_irr :
  ∀ acts amap mo L acts',
    conform acts amap mo L acts' →
    ∀ b r,
      conform acts amap mo (upd L (TsbS b) r) acts'.
Proof.
  unfold conform, out_rf; intros; rewrite !map_upd_irr; rupd; auto;
  rewrite in_map_iff; intro; desf.
Qed.

Lemma conform_ext_irr :
  ∀ acts amap sb rf mo sc L acts',
    Consistent acts amap sb rf mo sc →
    conform acts amap mo L acts' →
    ∀ b,
      (∀ l, ¬ is_writeL (amap b) l) →
      conform acts amap mo L (b::acts').
Proof.
  unfold conform; intros.
  red in H; desf.
  assert (M := proj1 Cmo _ _ MO); desf.
  ins; desf; eauto; try by edestruct H1; eauto.
Qed.

Lemma valid_node_upd_irr :
  ∀ IE acts amap rf L E te a r
    (S: a ≠ te_src te)
    (T: te_tgt te ≠ Some a)
    (V: valid_node IE acts acts amap rf L E a),
  valid_node IE acts acts amap rf (upd L te r) E a.
Proof.
  intros; red in V; desf; red; unfold NW.
  eexists r0.
  unfold incoming, in_sb, in_rf, in_esc, out_esc, out_rf, out_sb in ×.
  rewrite !map_upd_irr; rupd; try (by ins; intro; desf);
    try (by rewrite in_map_iff; intro; desf).
  repeat (split; ins; rupd); eauto; try (by ins; intro; desf).
Qed.

Lemma valid_node_upd_esc :
  ∀ IE acts amap rf L EE a
    (V : valid_node IE acts acts amap rf L EE a)
    sigma (INs : In sigma EE) (ND': NoDup EE)
    b (INb: In b acts) (ND: NoDup acts) (NEQ : a ≠ b),
  valid_node IE acts acts amap rf
     (upd (upd L (TescS sigma a) res_emp) (Tesc a b)
        (L (TescS sigma a) +!+ L (Tesc a b))) EE a.
Proof.
  unfold valid_node; ins; desf; unnw.
  rewrite !incoming_upd_irr; ins; try congruence.
  unfold in_sb, in_rf, out_sb, out_rf.
  rewrite !map_upd_irr; ins; rewrite ?in_map_iff; try intro; desf; rupd.
  ∃ r; repeat (apply conj; ins; rupd; eauto).

  apply In_NoDup_Permutation in INb; desf.
  apply In_NoDup_Permutation in INs; desf.
  revert VG; unfold out_esc.
  rewrite !(Permutation_rsum (Permutation_map _ (Permutation_map _ INb))).
  rewrite !(Permutation_rsum (Permutation_map _ (Permutation_map _ INs))).
  simpl; rupd; rewrite res_plus_emp_l, !res_plusA.
  rewrite !map_upd_irr, !(res_plusAC (L (TescS sigma a))); ins;
  rewrite ?in_map_iff; intro; desf; rupd.
Qed.

Lemma valid_node_ext_helper :
  ∀ IE acts N amap rf L E a
    (V : valid_node IE acts N amap rf L E a) b,
    is_rmw (amap b) = false →
    valid_node IE acts (b :: N) amap rf L E a.
Proof.
  red; unfold NW; intros.
  red in V; desf.
  ∃ r; repeat (split; try done); ins; desf; eauto.
Qed.

Lemma valid_node_ext_helper2 :
  ∀ IE acts N amap rf L E a
    (V : valid_node IE acts N amap rf L E a) b,
    rf b ≠ Some a →
    valid_node IE acts (b :: N) amap rf L E a.
Proof.
  red; unfold NW; intros.
  red in V; desf.
  ∃ r; repeat (split; try done); ins; desf; eauto.
Qed.