Require Import List Relations Setoid Omega Permutation.
Require Import Classical ClassicalDescription.
Require Import Vbase extralib ExtraRelations.
Set Implicit Arguments.
Remove Hints plus_n_O.

Definition actid := nat.

Inductive act :=
  | Askip
  | Async
  | Alwsync
  | Aload (l : nat) (v : nat)
  | Astore (l : nat) (v : nat).

Definition loc a :=
  match a with
    | Aload l _
    | Astore l _ ⇒ 1
    | _ ⇒ 0
  end.

Definition is_access a :=
  match a with
    | Aload _ _ | Astore _ _ ⇒ true
    | _ ⇒ false
  end.

Definition is_read a :=
  match a with
    | Aload _ _ ⇒ true
    | _ ⇒ false
  end.

Definition is_write a :=
  match a with
    | Astore _ _ ⇒ true
    | _ ⇒ false
  end.

Definition is_fence a :=
  match a with
    | Alwsync | Async ⇒ true
    | _ ⇒ false
  end.

Lemma is_read_access a : is_read a → is_access a.
Proof. by destruct a. Qed.

Lemma is_write_access a : is_write a → is_access a.
Proof. by destruct a. Qed.

Hint Resolve is_read_access is_write_access : access.

Section PowerModel.

Variable acts : list actid.
Variable lab : actid → act.
Variable po : relation actid.
Variable deps : relation actid.
Variable rmw : relation actid.
Variable ppo : relation actid.
Variable rf : actid → option actid.
Variable co : relation actid.

Definition rfe x y := rf y = Some x ∧ ¬ po x y.

Definition fr x y := ∃ z, rf x = Some z ∧ co z y.

Definition fre x y := ∃ z, rf x = Some z ∧ co z y ∧ ¬ po x y.

Definition coe x y := co x y ∧ ¬ po x y.

Definition po_loc x y :=
  po x y ∧ is_access (lab x) ∧ is_access (lab y) ∧ loc (lab x) = loc (lab y).

Definition sync x y :=
  ∃ s, po x s ∧ po s y ∧ lab s = Async ∧
   is_access (lab x) ∧ is_access (lab y).

Definition lwsync x y :=
  (∃ s, po x s ∧ po s y ∧ lab s = Alwsync)
  ∧ (is_read (lab x) ∧ is_access (lab y) ∨
      is_access (lab x) ∧ is_write (lab y)).

Definition fence := sync +++ lwsync.

Definition hb_power := ppo +++ fence +++ rfe.

Definition prop_base :=
  clos_refl rfe ;; fence ;; clos_refl_trans hb_power.

Definition chapo :=
  rfe +++ fre +++ coe +++ (fre ;; rfe) +++ (coe ;; rfe).

Definition prop :=
  restr_rel (fun x ⇒ is_write (lab x)) prop_base
  +++ (clos_refl chapo ;; clos_refl prop_base ;; sync ;; clos_refl_trans hb_power).

Definition ExecutionFinite :=
  << CLOlab: ∀ a, lab a ≠ Askip → In a acts >> ∧
  << CLOsb : ∀ a b, po a b → In a acts ∧ In b acts >>.

Definition ConsistentRF_dom :=
  ∀ a b (RF: rf b = Some a),
  ∃ l v, <<WRI: lab a = Astore l v>> ∧ <<READ: lab b = Aload l v >>.

Definition CompleteRF :=
  ∀ a (RF: rf a = None)
         (READ: is_read (lab a)), False.

Definition ConsistentMO_dom :=
  ∀ a b (MO: co a b),
    is_write (lab a) ∧ is_write (lab b) ∧ loc (lab a) = loc (lab b).

Definition ConsistentRMW_dom :=
  ∀ a b (RF: rmw a b),
  << PO: po a b >> ∧
  << READ: is_read (lab a) >> ∧
  << WRITE: is_write (lab b) >> ∧
  << LOCEQ: loc (lab a) = loc (lab b) >>.

Definition ppo_lower_bound :=
  ∀ a b,
    clos_trans (deps +++ po_loc) a b →
    is_read (lab a) →
    is_write (lab b) →
    ppo a b.

Definition ppo_upper_bound :=
  ∀ a b,
    ppo a b →
    immediate po a b →
    clos_trans (deps +++ po_loc) a b.

Definition ConsistentPower :=
  << CppoL: ppo_lower_bound >> ∧

  << CrfD: ConsistentRF_dom >> ∧
  << COrf: CompleteRF >> ∧
  << Crmw: ConsistentRMW_dom >> ∧
  << CcoD: ConsistentMO_dom >> ∧
  << CcoF: ∀ l, is_total (fun a ⇒ ∃ v, lab a = Astore l v) co >> ∧
  << CcoT: transitive co >> ∧
  << CcoI: irreflexive co >> ∧
  << LOC_SC : acyclic (po_loc +++ (fun x y ⇒ rf y = Some x) +++ co +++ fr) >> ∧
  << ATOM : irreflexive (rmw ;; fre ;; coe) >> ∧
  << NTA : acyclic hb_power >> ∧
  << OBS : irreflexive (fre ;; prop ;; clos_refl_trans hb_power) >> ∧
  << PROP: acyclic (co +++ prop) >>.

Lemma loceq_rf :
  ∀ (CrfD: ConsistentRF_dom) a b (H: rf b = Some a),
    loc (lab a) = loc (lab b).
Proof.
  by ins; apply CrfD in H; desf; rewrite WRI, READ.
Qed.

Lemma loceq_co :
  ∀ (CcoD: ConsistentMO_dom) a b (H: co a b),
    loc (lab a) = loc (lab b).
Proof.
  by ins; apply CcoD in H; desf.
Qed.

Lemma loceq_fr :
  ∀ (CrfD: ConsistentRF_dom) (CcoD: ConsistentMO_dom)
         a b (H: fr a b),
    loc (lab a) = loc (lab b).
Proof.
  unfold fr; ins; desf; transitivity (loc (lab z));
  eauto using loceq_co, loceq_rf, eq_sym.
Qed.

Lemma fr_dom :
  ∀ (CrfD: ConsistentRF_dom)
         (CcoD: ConsistentMO_dom) x y
         (FR: fr x y),
  is_read (lab x) ∧ is_write (lab y) ∧ loc (lab x) = loc (lab y).
Proof.
  unfold fr; ins; desc; eapply CrfD in FR; desc.
  eapply CcoD in FR0; desc; destruct (lab x), (lab y); ins.
Qed.

Lemma rfe_dom :
  ∀ (CrfD: ConsistentRF_dom) x y
         (RFE: rfe x y),
  is_write (lab x) ∧ is_read (lab y) ∧ loc (lab x) = loc (lab y).
Proof.
  unfold rfe; ins; desc; eapply CrfD in RFE; desc.
  by rewrite WRI, READ.
Qed.

Lemma fre_dom :
  ∀
         (CrfD: ConsistentRF_dom)
         (CcoD: ConsistentMO_dom) x y
         (FRE: fre x y),
  is_read (lab x) ∧ is_write (lab y) ∧ loc (lab x) = loc (lab y).
Proof.
  unfold fre; ins; desc; eapply CrfD in FRE; desc.
  eapply CcoD in FRE0; desc; destruct (lab x), (lab y); ins.
Qed.

Definition nta_rel :=
  deps +++ po_loc
       +++ (fun x y ⇒ po x y ∧ (is_fence (lab x) ∨ is_fence (lab y)))
       +++ rfe.

Lemma acyclic_nta
      (CsbT: transitive po)
      (CsbI: irreflexive po)
      (Cdeps: inclusion deps po)
      (CrfD: ConsistentRF_dom)
      (NTA : acyclic hb_power)
      (PPO_lower : ppo_lower_bound) :
  acyclic nta_rel.
Proof.
  assert (INCL: inclusion (clos_trans (deps +++ po_loc
                                            +++ (fun x y ⇒ po x y ∧
                                                            (is_fence (lab x) ∨
                                                             is_fence (lab y)))))
                          po).
    by unfold union, po_loc; induction 1; ins; desf; eauto.

  unfold nta_rel; intros x X.
  rewrite unionC in X.
  eapply cycle_ur with (adom:=fun x ⇒ is_write (lab x))
                       (bdom:=fun x ⇒ is_read (lab x)) in X;
    try solve [ins; exploit rfe_dom; eauto; ins; desf].
  desf; eauto.
  eapply NTA, clos_trans_mon; eauto; ins; clear X.
  unfold hb_power, union in *; desf; eauto.
  destruct (classic (fence a b)) as [|NF]; eauto.
  assert (Y: ∀ c, clos_refl po a c → clos_refl po c b →
                       is_fence (lab c) → False).
    by clear -H0 H1 NF; ins; apply NF;
       unfold fence, sync, lwsync, is_fence, clos_refl, union in *; desf;
       [left |right]; ins; eauto 8 with access.
  left; left; eapply PPO_lower; unfold union; ins; rename H into Z.
  clear - Z INCL CsbT Y; induction Z; desf; eauto using clos_trans;
  try solve [exfalso; eauto].
  eapply t_trans; [eapply IHZ1 | eapply IHZ2]; ins; [red in H0|red in H];
  desf; eapply Y in H1; try red; eauto.
Qed.

End PowerModel.

Definition ntb_rel i ll lab deps rf x y :=
   In x i ∧ In y (concat ll) ∨
   nta_rel lab (mk_po i ll) deps rf x y.

Lemma acyclic_ntb i ll lab deps ppo rf
      (ND: NoDup (i ++ concat ll))
      (INIT: ∀ x, is_read (lab x) → In x (concat ll))
      (Cdeps: inclusion deps (mk_po i ll))
      (CrfD: ConsistentRF_dom lab rf)
      (NTA : acyclic (hb_power lab (mk_po i ll) ppo rf))
      (PPO_lower : ppo_lower_bound lab (mk_po i ll) deps ppo) :
  acyclic (ntb_rel i ll lab deps rf).
Proof.
  ins; assert (acyclic (nta_rel lab (mk_po i ll) deps rf)).
    eapply acyclic_nta; eauto using transitive_mk_po.
    by red; eauto using mk_po_irreflexive.
  assert (N: ∀ x y, nta_rel lab (mk_po i ll) deps rf x y → In y (concat ll)).
    unfold nta_rel, union, po_loc; ins; desf; eauto using mk_po_in2.
    by eapply rfe_dom in H0; desf; eauto.
  intros x X.
  eapply cycle_ur with (adom := fun x ⇒ In x i)
                       (bdom := fun x ⇒ In x (concat ll)) in X; ins; desf.
    by eapply H, clos_trans_mon; eauto; ins; desf.
  eapply nodup_app with (a:=x0); eauto.
    rewrite t_step_rt in X; desf.
    eapply t_rt_step in X; desf.
    by exfalso; eapply nodup_app; eauto.
  rewrite t_rt_step in X; desf.
  rewrite t_rt_step in X0; desf.
  by exfalso; eapply nodup_app; eauto.
Qed.

Add Parametric Morphism : rfe with signature
  same_relation ==> eq ==> same_relation as rfe_mor.
Proof.
  unfold same_relation, inclusion, rfe; intuition; desf; eauto 8.
Qed.

Add Parametric Morphism : coe with signature
  same_relation ==> eq ==> same_relation as coe_mor.
Proof.
  unfold same_relation, inclusion, coe; intuition; desf; eauto 8.
Qed.

Add Parametric Morphism : fre with signature
  same_relation ==> eq ==> eq ==> same_relation as fre_mor.
Proof.
  unfold same_relation, inclusion, fre; intuition; desf; eauto 8.
Qed.

Add Parametric Morphism : po_loc with signature
  eq ==> same_relation ==> same_relation as po_loc_mor.
Proof.
  unfold same_relation, inclusion, po_loc; intuition; desf; eauto 8.
Qed.

Add Parametric Morphism : sync with signature
  eq ==> same_relation ==> same_relation as sync_mor.
Proof.
  unfold same_relation, inclusion, sync; intuition; desf; eauto 8.
Qed.

Add Parametric Morphism : lwsync with signature
  eq ==> same_relation ==> same_relation as lwsync_mor.
Proof.
  unfold same_relation, inclusion, lwsync; intuition; desf; eauto 8.
Qed.

Add Parametric Morphism : hb_power with signature
  eq ==> same_relation ==> eq ==> eq ==> same_relation as hb_power_mor.
Proof.
  unfold hb_power, fence; ins; rewrite H; reflexivity.
Qed.

Add Parametric Morphism : prop_base with signature
  eq ==> same_relation ==> eq ==> eq ==> same_relation as prop_base_mor.
Proof.
  unfold prop_base, fence; ins; rewrite H; reflexivity.
Qed.

Add Parametric Morphism : prop with signature
  eq ==> same_relation ==> eq ==> eq ==> eq ==> same_relation as prop_mor.
Proof.
  unfold prop, fence, chapo; ins; rewrite H; reflexivity.
Qed.

Add Parametric Morphism : ppo_lower_bound with signature
  eq ==> same_relation ==> eq ==> eq ==> iff as ppo_lower_mor.
Proof.
  by unfold ppo_lower_bound; split; ins; eapply H0; eauto; rewrite H in ×.
Qed.

Add Parametric Morphism : ConsistentRMW_dom with signature
  eq ==> same_relation ==> eq ==> iff as ConsistentRMW_dom_mor.
Proof.
  unfold same_relation, inclusion, ConsistentRMW_dom; split; ins;
  apply H0 in RF; clear H0; desc; unnw; eauto.
Qed.

Add Parametric Morphism : ConsistentPower with signature
  eq ==> same_relation ==> eq ==> eq ==> eq ==> eq ==> eq ==> iff as ConsistentPower_mor.
Proof.
  unfold ConsistentPower; unnw; ins; rewrite H; eauto; tauto.
Qed.

Add Parametric Morphism : nta_rel with signature
  eq ==> same_relation ==> eq ==> eq ==> same_relation as nta_rel_mor.
Proof.
  unfold nta_rel; ins; rewrite H at 1 2.
  unfold same_relation, inclusion, union in *; intuition; eauto.
Qed.

Lemma po_loc_reorder lab po a b
   (LOC: loc (lab a) ≠ loc (lab b)) :
  po_loc lab (reorder po a b) <--> po_loc lab po.
Proof.
  unfold po_loc, reorder; split; red; ins; desf; eauto; try congruence.
  split; ins; left; split; ins; intro; desf.
Qed.

Lemma rfe_reorder lab po rf a b
      (Crf: ConsistentRF_dom lab rf)
      (LOC: loc (lab a) ≠ loc (lab b)) :
  rfe (reorder po b a) rf <--> rfe po rf.
Proof.
  unfold rfe, reorder; split; red; ins; intuition; desf; eauto;
  eapply loceq_rf in H0; eauto.
  apply H3; intro; desf; eauto.
Qed.

Lemma fre_reorder lab po rf co a b
      (Crf: ConsistentRF_dom lab rf)
      (Cco: ConsistentMO_dom lab co)
      (LOC: loc (lab a) ≠ loc (lab b)) :
  fre (reorder po b a) rf co <--> fre po rf co.
Proof.
  split; red; ins; exploit fre_dom; eauto; ins; desf;
  unfold fre, reorder in *; desf; repeat eexists; eauto;
  intro; desf; apply H1; left; split; ins; intro; desf; congruence.
Qed.

Lemma coe_reorder lab po co a b
      (Cco: ConsistentMO_dom lab co)
      (LOC: loc (lab a) ≠ loc (lab b)) :
  coe (reorder po b a) co <--> coe po co.
Proof.
  unfold coe, reorder; split; red; ins; desf; split; ins; intro; desf;
  apply Cco in H; desf.
  destruct H0; eauto; left; split; ins; intro; desf; congruence.
Qed.

Lemma sync_reorder lab (po : relation actid) a b
      (NFa: ¬ is_fence (lab a)) (NFb: ¬ is_fence (lab b)) :
  sync lab (reorder po a b) <--> sync lab po.
Proof.
  split; red; ins; unfold sync, reorder in *; desf; eauto 8;
    try (by destruct (lab a)); try (by destruct (lab b)).
  ∃ s; repeat split; ins; left; split; ins; intro; desf;
    try (by destruct (lab a)); try (by destruct (lab b)).
Qed.

Lemma lwsync_reorder lab (po : relation actid) a b
      (NFa: ¬ is_fence (lab a)) (NFb: ¬ is_fence (lab b)) :
  lwsync lab (reorder po a b) <--> lwsync lab po.
Proof.
  split; red; ins; unfold lwsync, reorder in *; desf;
  split; ins; eauto 8;
    try (by destruct (lab a)); try (by destruct (lab b));
  ∃ s; repeat split; ins; left; split; ins; intro; desf;
    try (by destruct (lab a)); try (by destruct (lab b)).
Qed.

Lemma hbp_reorder lab po ppo rf a b
      (Crf: ConsistentRF_dom lab rf)
      (NFa: ¬ is_fence (lab a)) (NFb: ¬ is_fence (lab b))
      (LOC: loc (lab a) ≠ loc (lab b)) :
  hb_power lab (reorder po a b) ppo rf <--> hb_power lab po ppo rf.
Proof.
  unfold hb_power, fence.
  rewrite rfe_reorder, sync_reorder, lwsync_reorder; eauto; reflexivity.
Qed.

Lemma base_reorder lab po ppo rf a b
      (Crf: ConsistentRF_dom lab rf)
      (NFa: ¬ is_fence (lab a)) (NFb: ¬ is_fence (lab b))
      (LOC: loc (lab a) ≠ loc (lab b)) :
  prop_base lab (reorder po a b) ppo rf <--> prop_base lab po ppo rf.
Proof.
  unfold prop_base, fence.
  rewrite hbp_reorder, rfe_reorder, sync_reorder, lwsync_reorder;
    eauto; reflexivity.
Qed.

Lemma prop_reorder lab po ppo rf co a b
      (Crf: ConsistentRF_dom lab rf)
      (Cmo: ConsistentMO_dom lab co)
      (NFa: ¬ is_fence (lab a)) (NFb: ¬ is_fence (lab b))
      (LOC: loc (lab a) ≠ loc (lab b)) :
  prop lab (reorder po a b) ppo rf co <--> prop lab po ppo rf co.
Proof.
  unfold prop, chapo.
  rewrite hbp_reorder, rfe_reorder, fre_reorder, sync_reorder, coe_reorder, base_reorder;
    eauto 2; reflexivity.
Qed.

Lemma nta_rel_reorder lab po ppo rf a b
      (Crf: ConsistentRF_dom lab rf)
      (NFa: ¬ is_fence (lab a)) (NFb: ¬ is_fence (lab b))
      (LOC: loc (lab a) ≠ loc (lab b)) :
  nta_rel lab (reorder po a b) ppo rf <--> nta_rel lab po ppo rf.
Proof.
  unfold nta_rel.
  rewrite po_loc_reorder, rfe_reorder; eauto; ins; unfold union, reorder.
  split; red; ins; repeat split; ins; desf; eauto;
  left; right; split; eauto; left; split; ins; intro; desf.
Qed.

Lemma ntb_rel_reorder i ll1 l1 a b l2 ll2 lab ppo rf
      (WF: NoDup (i ++ concat (ll1 ++ (l1 ++ a :: b :: l2) :: ll2)))
      (Crf: ConsistentRF_dom lab rf)
      (NFa: ¬ is_fence (lab a)) (NFb: ¬ is_fence (lab b))
      (LOC: loc (lab a) ≠ loc (lab b)) :
  ntb_rel i (ll1 ++ (l1 ++ a :: b :: l2) :: ll2) lab ppo rf <-->
  ntb_rel i (ll1 ++ (l1 ++ b :: a :: l2) :: ll2) lab ppo rf.
Proof.
  unfold same_relation, inclusion, ntb_rel; split; ins; desf;
  eauto using Permutation_in, Permutation_app_inv_l, (Permutation_reord i);
  right;
  eapply nta_rel_mor; try symmetry; try eapply mk_po_reorder;
    eauto using Permutation_reord, Permutation_nodup;
    eapply nta_rel_reorder; eauto.
Qed.

Lemma ConsistentRMW_dom_reorder lab po rmw x y
      (LOC: loc (lab x) ≠ loc (lab y)) :
  ConsistentRMW_dom lab (reorder po x y) rmw ↔
  ConsistentRMW_dom lab po rmw.
Proof.
  unfold ConsistentRMW_dom, reorder; split; ins; desf;
  apply H in RF; clear H; desc; unnw; desf; intuition; eauto; ins; try congruence.
  left; split; ins; desf.
Qed.

Lemma ppo_lower_bound_reorder lab po deps ppo a b
      (LOC: loc (lab a) ≠ loc (lab b)) :
  ppo_lower_bound lab (reorder po a b) deps ppo ↔
  ppo_lower_bound lab po deps ppo.
Proof.
  by split; repeat red; ins; eapply H; ins; rewrite po_loc_reorder in ×.
Qed.

Lemma ConsistentPower_reorder :
  ∀ lab po deps rmw ppo rf co a b
      (NFa: ¬ is_fence (lab a)) (NFb: ¬ is_fence (lab b))
      (LOC: loc (lab a) ≠ loc (lab b)),
    ConsistentPower lab po deps rmw ppo rf co ↔
    ConsistentPower lab (reorder po a b) deps rmw ppo rf co.
Proof.
  ins; unfold ConsistentPower; split; ins; desc; unnw;
  revert CppoL Crmw LOC_SC ATOM NTA OBS PROP;
  rewrite po_loc_reorder, fre_reorder, coe_reorder, hbp_reorder, prop_reorder,
          ppo_lower_bound_reorder, ConsistentRMW_dom_reorder; eauto 2; ins; intuition.
Qed.

Definition Power_reorder lab init deps (ll ll' : list (list actid)) :=
 ∃ ll1 l1 a b l2 ll2,
     << NFa: ¬ is_fence (lab a) >> ∧
     << NFb: ¬ is_fence (lab b) >> ∧
     << LOC: loc (lab a) ≠ loc (lab b) >> ∧
     << Nab: ¬ deps a b >> ∧
     << WF: NoDup (init ++ concat (ll1 ++ (l1 ++ a :: b :: l2) :: ll2)) >> ∧
     << EQ : ll = ll1 ++ (l1 ++ a :: b :: l2) :: ll2 >> ∧
     << EQ': ll' = ll1 ++ (l1 ++ b :: a :: l2) :: ll2 >>.

Fixpoint metric (ord: relation actid) (ll : list actid) :=
  match ll with
    | nil ⇒ 0
    | a :: ll ⇒
      length (filter (fun x ⇒ if excluded_middle_informative (ord x a)
                               then true else false) ll) +
      metric ord ll
  end.

Add Parametric Morphism : metric with signature
  same_relation ==> eq ==> eq as metric_mor.
Proof.
  unfold same_relation; desc; induction y0; ins; f_equal; eauto.
  clear - H; induction y0; ins; desf; ins; try congruence;
  exfalso; eauto.
Qed.

Lemma reorder_metric (ord : relation actid)
      (T: transitive ord) (IRR: irreflexive ord) ll1 l1 a b (ORD: ord b a) l2 ll2 :
  metric ord (concat (ll1 ++ (l1 ++ b :: a :: l2) :: ll2)) <
  metric ord (concat (ll1 ++ (l1 ++ a :: b :: l2) :: ll2)).
Proof.
  rewrite !concat_app, !concat_cons, <- !app_assoc; ins.
  rewrite !app_assoc.
  induction (concat ll1 ++ l1); ins; desf; ins;
    try (solve [exfalso; eauto]); try omega.
  rewrite perm_swap at 1; omega.
Qed.

Theorem Power_alternative :
  ∀ lab init ll (ND: NoDup (init ++ concat ll)) deps
         (WF: inclusion deps (mk_po init ll))
         (INIT: ∀ x, is_read (lab x) → In x (concat ll))
         (MAIN: ∀ x, In x (concat ll) → is_access (lab x))
         rmw ppo rf co,
    ConsistentPower lab (mk_po init ll) deps rmw ppo rf co
    ↔
    ∃ ll',
      clos_refl_trans (Power_reorder lab init deps) ll ll' ∧
      ConsistentPower lab (mk_po init ll') deps rmw ppo rf co ∧
      acyclic (mk_po init ll' +++ (fun x y ⇒ rf y = Some x)).
Proof.
  split; ins; desf; cycle 1.
     rename H into J; clear H1 ND; induction J using clos_refl_trans_ind_left; eauto.
     unfold Power_reorder in *; desf; apply IHJ; clear IHJ.
     by rewrite <- mk_po_reorder, <- ConsistentPower_reorder; eauto.

  induction ll using
            (well_founded_ind (well_founded_ltof _
               (fun p ⇒ metric (tot_ext_nat (ntb_rel init p lab deps rf))
                                (concat p)))); unfold ltof in ×.
  destruct (classic (∃ ll1 l1 a b l2 ll2,
     << NFa: ¬ is_fence (lab a) >> ∧
     << NFb: ¬ is_fence (lab b) >> ∧
     << LOC: loc (lab a) ≠ loc (lab b) >> ∧
     << Nab: ¬ deps a b >> ∧
     << EQ : ll = ll1 ++ (l1 ++ a :: b :: l2) :: ll2 >> ∧
     << ORD: ¬ tot_ext_nat (ntb_rel init ll lab deps rf) a b >> )).
   desf.
   exploit (H0 (ll1 ++ (l1 ++ b :: a :: l2) :: ll2));
     eauto using Permutation_reord, Permutation_nodup.
   red in H; desc.
   rewrite ntb_rel_reorder;
     eauto using Permutation_nodup, Permutation_reord.
   eapply reorder_metric; eauto using tot_ext_nat_trans, tot_ext_nat_extends.
   eapply tot_ext_nat_irr, acyclic_ntb;
   eauto using Permutation_nodup, Permutation_reord.

  by destruct (eqP a b) as [|NEQ]; desf;
     eapply tot_ext_nat_total in NEQ; desf; eauto; desf.

  rewrite <- mk_po_reorder; eauto using Permutation_reord, Permutation_nodup.
  by red; ins; unfold reorder; left; split; eauto; intro; desf.

  by eauto using Permutation_in, Permutation_app_inv_l, (Permutation_reord init).
  by eauto using Permutation_in, Permutation_app_inv_l, (Permutation_reord init).

  rewrite <- mk_po_reorder, <- ConsistentPower_reorder in H;
  eauto using Permutation_reord, Permutation_nodup.
  intro X; desc; eexists; split; eauto; eapply rt_trans; eauto.
  apply rt_step; ins.
  eauto using clos_refl_trans; red; unnw; repeat eexists; eauto.

  clear H0; ∃ ll; split; [|split]; eauto using rt_refl; intros x X.

  assert (Z: ∀ ll1 l1 a b l2 ll2,
            ll = ll1 ++ (l1 ++ a :: b :: l2) :: ll2 →
            is_fence (lab a) ∨
            is_fence (lab b) ∨
            is_access (lab a) ∧ is_access (lab b) ∧ loc (lab a) = loc (lab b) ∨
            deps a b ∨
            tot_ext_nat (ntb_rel init ll lab deps rf) a b).
  { ins; unnw; desf; apply NNPP; intro; destruct H1; desf; ∃ ll1, l1, a, b.
    do 7 try eexists; eauto; first [intro|apply NNPP; intro]; desf; destruct H0; eauto 8.
    right; right; left; repeat split; ins; eapply MAIN;
    rewrite concat_app, concat_cons, <- app_assoc; ins; eauto 6 using in_or_app, in_eq, in_cons.
  }
  clear H1.

  eapply clos_trans_mon with (r' := mk_po init ll +++ rfe (mk_po init ll) rf) in X.
    2: by unfold union, rfe; ins; tauto.
  cut (clos_trans (immediate (mk_po init ll) +++ rfe (mk_po init ll) rf) x x);
    [clear X; intro X|]; cycle 1.
    revert X; generalize x at 1 3; unfold union.
    induction 1; desf; eauto using clos_trans.
    eapply clos_trans_mon; [eapply clos_trans_imm, H0|];
    eauto using transitive_mk_po, mk_po_in1; red; eauto using mk_po_irreflexive.

  red in H; desc; unnw.
  eapply tot_ext_nat_irr.
  eapply acyclic_ntb; eauto.
  instantiate (1:=x); revert X; generalize x at 1 3;
  induction 1; [|eby eapply tot_ext_nat_trans].
  revert H;
  unfold ntb_rel, nta_rel, union, po_loc; ins; desf; eauto 10 using tot_ext_nat_extends.
  destruct (classic (In x init)).
    by apply proj1, mk_po_in2 in H; eauto using tot_ext_nat_extends.
  eapply mk_po_immediateD in H; desf.
  specialize (Z _ _ _ _ _ _ eq_refl); desf;
  eauto 10 using tot_ext_nat_extends, mk_po_trivial.
Qed.