Module SSAfastliveprecomputethm

Require Import Relation_Operators.
Require Import Sorted.

Require Import Coqlib.
Require Import Maps.
Require Import Utils.

Require Import SSAfastliveutils.
Require Import SSAfastliveprecomputeRT.
Require Import SSAfastliveprecomputeRTthm.
Require Import SSAfastliveprecomputeTT.
Require Import SSAfastliveprecomputeTTthm.
Require Import SSAfastliveprecompute.
Require Import SSAfastliveprecomputeproof.

Local Open Scope positive_scope.

Lemma precompute_r_t_r_in_g : forall g root dom_pre,
  let '(r, c, t, back) := precompute_r_t g root dom_pre in
  forall u,
  r ! u <> None <-> reachable g root u /\ g ! u <> None.

Proof.

  intros.
  unfold precompute_r_t.
  destruct (precompute_r_t_up g root dom_pre)
    as (((r, c), t), back) eqn:Hprecompute_r_t_up.
  exploit precompute_r_t_up_r_in_g. rewrite Hprecompute_r_t_up. auto.
Qed.

Lemma precompute_r_t_r_inj : forall g root dom_pre,
  let '(r, c, t, back) := precompute_r_t g root dom_pre in
  forall u v m n1 n2,
  r ! u = Some (m, n1) ->
  r ! v = Some (m, n2) ->
  u = v.

Proof.

  intros.
  unfold precompute_r_t.
  destruct (precompute_r_t_up g root dom_pre)
    as (((r, c), t), back) eqn:Hprecompute_r_t_up.
  exploit precompute_r_t_up_r_inj. rewrite Hprecompute_r_t_up. auto.
Qed.

Lemma precompute_r_t_r_wf : forall g root dom_pre,
  let '(r, c, t, back) := precompute_r_t g root dom_pre in
  forall u n1 n2,
  r ! u = Some (n1, n2) -> Ple n1 n2.

Proof.

  intros.
  unfold precompute_r_t.
  destruct (precompute_r_t_up g root dom_pre)
    as (((r, c), t), back) eqn:Hprecompute_r_t_up.
  exploit precompute_r_t_up_r_wf. rewrite Hprecompute_r_t_up. auto.
Qed.

Lemma precompute_r_t_r_cases : forall g root dom_pre,
  let '(r, c, t, back) := precompute_r_t g root dom_pre in
  forall u v n1 n2 m1 m2,
  r ! u = Some (n1, n2) ->
  r ! v = Some (m1, m2) ->
  m2 < n1 \/ n2 < m1
  \/ is_included (m1, m2) (n1, n2)
  \/ is_included (n1, n2) (m1, m2) .

Proof.

  intros.
  unfold precompute_r_t.
  destruct (precompute_r_t_up g root dom_pre)
    as (((r, c), t), back) eqn:Hprecompute_r_t_up.
  exploit precompute_r_t_up_r_cases. rewrite Hprecompute_r_t_up. auto.
Qed.

Lemma precompute_r_t_r_c_correct : forall g root dom_pre,
  let '(r, c, t, back) := precompute_r_t g root dom_pre in
  forall u v,
  cross_included r c u v <->
  (reachable g root u /\ g ! u <> None /\ reduced_reachable g back u v).

Proof.

  intros.
  unfold precompute_r_t.
  destruct (precompute_r_t_up g root dom_pre)
    as (((r, c), t), back) eqn:Hprecompute_r_t_up.
  exploit precompute_r_t_up_r_c_correct. rewrite Hprecompute_r_t_up. auto.
Qed.

Lemma precompute_r_t_up_c_refl : forall g root dom_pre,
let '(r, c, t, back) := precompute_r_t_up g root dom_pre in
forall u, r ! u <> None -> exists set, c ! u = Some set /\ set ! u = Some tt.

Proof.

  intros.
  unfold precompute_r_t.
  destruct (precompute_r_t_up g root dom_pre)
    as (((r, c), t), back) eqn:Hprecompute_r_t_up.
  exploit precompute_r_t_up_c_refl. rewrite Hprecompute_r_t_up. auto.
Qed.

Lemma precompute_r_t_c_numbering : forall g root dom_pre,
  let '(r, c, t, back) := precompute_r_t g root dom_pre in
  forall u set v, c ! u = Some set -> set ! v = Some tt ->
  v <> u ->
  exists n1 n2 m1 m2,
  r ! u = Some (n1, n2) /\ r ! v = Some (m1, m2) /\
  m2 < n1.

Proof.

  intros.
  unfold precompute_r_t.
  destruct (precompute_r_t_up g root dom_pre)
    as (((r, c), t), back) eqn:Hprecompute_r_t_up.
  exploit precompute_r_t_up_c_numbering. rewrite Hprecompute_r_t_up. auto.
Qed.

Lemma precompute_r_t_c_black : forall g root dom_pre,
let '(r, c, t, back) := precompute_r_t g root dom_pre in
forall u, c ! u <> None -> r ! u <> None.

Proof.

  intros.
  unfold precompute_r_t.
  destruct (precompute_r_t_up g root)
    as (((r, c), t), back) eqn:Hprecompute_r_t_up.
  exploit precompute_r_t_up_c_black. rewrite Hprecompute_r_t_up. auto.
Qed.

Lemma precompute_r_t_c_target_black : forall g root dom_pre,
  let '(r, c, t, back) := precompute_r_t g root dom_pre in
  forall u set v, c ! u = Some set -> set ! v = Some tt ->
  r ! v <> None.

Proof.

  intros.
  unfold precompute_r_t.
  destruct (precompute_r_t_up g root dom_pre)
    as (((r, c), t), back) eqn:Hprecompute_r_t_up.
  exploit precompute_r_t_up_c_target_black. rewrite Hprecompute_r_t_up. auto.
Qed.

Lemma precompute_r_t_t_correct : forall g root dom_pre
  (g_reachable_closed : forall u : positive, reachable g root u -> g ! u <> None)
  (dom_pre_inj : forall u v,
    reachable g root u -> reachable g root v ->
    dom_pre u = dom_pre v -> u = v),
  let '(_, _, t, back) := precompute_r_t g root dom_pre in
  forall u v, t_linked t u v <-> reachable g root u /\ is_in_t g back u v.

Proof.

  intros.
  unfold precompute_r_t. unfold Time.time.
  destruct (precompute_r_t_up g root dom_pre)
    as (((r, c), t_up), back) eqn:Hprecompute_r_t_up.
  exploit precompute_t_from_t_up_precompute_r_t_up; try eassumption. rewrite Hprecompute_r_t_up.
  set (pre := fun u => match r ! u with | Some (n, _) => n | None => 1 end).
  simpl. intros.
  exploit precompute_r_t_up_t_correct; try eassumption. rewrite Hprecompute_r_t_up.
  intros.
  split; intros.
  - assert (reachable g root u) as Ha.
    { exploit precompute_r_t_up_t_black. rewrite Hprecompute_r_t_up.
      exploit precompute_r_t_up_r_in_g. rewrite Hprecompute_r_t_up.
      intros H2 H3. apply H2, H3.
      destruct H1 as (set & H1 &_).
      intros contra.
      exploit precompute_t_from_t_up_black_2; try eassumption.
      rewrite H1. discriminate.
      intros. apply in_map_iff in H4. destruct H4 as ((s, u') & H4' & H4).
      simpl in H4'. subst.
      exploit precompute_r_t_up_back_target_black. rewrite Hprecompute_r_t_up.
      intros. apply H5, H3 in H4. contradiction.
      apply g_reachable_closed.
      exploit precompute_r_t_up_back_in_g. rewrite Hprecompute_r_t_up.
      intros. apply H6 in H4 as H7.
      destruct H7 as (succs & H71 & H72).
      exploit precompute_r_t_up_back_source_black. rewrite Hprecompute_r_t_up.
      intros. apply H7, H2 in H4. destruct H4 as (H4 & _).
      eapply reachable_succ; eassumption.
    }
    split; [assumption|].
    apply H in H1; try assumption.
    revert H1. apply star_eq.
    intros. apply H0. assumption.
  - destruct H1 as (H11 & H12).
    apply H; try assumption.
    apply Operators_Properties.clos_rt_rt1n_iff in H12.
    induction H12.
    + apply rt_refl.
    + eapply rt_trans. eapply rt_step. apply H0. split; eassumption.
      apply IHclos_refl_trans_1n.
      destruct H1 as (_ & s & H1' & H1'').
      exploit precompute_r_t_up_back_in_g. rewrite Hprecompute_r_t_up.
      intros H2. apply H2 in H1'. destruct H1' as (succs & H11' & H12').
      eapply reachable_trans. apply H11.
      apply reduced_reachable_is_reachable in H1''.
      econstructor; eassumption.
Qed.

Lemma precompute_r_t_t_black : forall g root dom_pre
  (g_reachable_closed : forall u : positive, reachable g root u -> g ! u <> None),
  let '(r, c, t, back) := precompute_r_t g root dom_pre in
  forall u, t ! u <> None <-> r ! u <> None.

Proof.

  intros. unfold precompute_r_t. unfold Time.time.
  destruct (precompute_r_t_up g root dom_pre)
    as (((r, c), t), back) eqn:Hprecompute_r_t_up.
  set (pre := fun u => match r ! u with | Some (n, _) => n | None => 1 end).
  intros.
  exploit precompute_r_t_up_t_black. rewrite Hprecompute_r_t_up.
  intros. rewrite <- H.
  split; intros.
  - intros contra.
    assert (r ! u = None) as Ha.
    { destruct (r ! u) eqn:Hr.
      - apply H in contra; try congruence. contradiction.
      - reflexivity.
    }
    exploit precompute_t_from_t_up_black_2; eauto.
    intros. apply in_map_iff in H1.
    destruct H1 as ((s, u') & H1' & H1). simpl in H1'. subst.
    exploit precompute_r_t_up_back_target_black. rewrite Hprecompute_r_t_up.
    intros.
    eapply H2; try eassumption.
    apply g_reachable_closed.
    exploit precompute_r_t_up_back_in_g. rewrite Hprecompute_r_t_up.
    intros. apply H3 in H1 as H4.
    destruct H4 as (succs & H41 & H42).
    exploit precompute_r_t_up_back_source_black. rewrite Hprecompute_r_t_up.
    intros. apply H4 in H1.
    exploit precompute_r_t_up_r_in_g. rewrite Hprecompute_r_t_up.
    intros. apply H5 in H1. destruct H1 as (H1 & _).
    eapply reachable_succ; eassumption.
  - apply precompute_t_from_t_up_black. assumption.
Qed.

Lemma precompute_r_t_t_target_black : forall g root dom_pre
  (g_reachable_closed : forall u : positive, reachable g root u -> g ! u <> None)
  (dom_pre_inj : forall u v,
    reachable g root u -> reachable g root v ->
    dom_pre u = dom_pre v -> u = v),
  let '(r, c, t, back) := precompute_r_t g root dom_pre in
  forall u v, t_linked t u v -> r ! v <> None.

Proof.

  intros.
  unfold precompute_r_t. unfold Time.time.
  destruct (precompute_r_t_up g root dom_pre)
    as (((r, c), t_up), back) eqn:Hprecompute_r_t_up.
  exploit precompute_t_from_t_up_precompute_r_t_up; try eassumption. rewrite Hprecompute_r_t_up.
  set (pre := fun u => match r ! u with | Some (n, _) => n | None => 1 end).
  simpl. intros.
  assert (reachable g root u) as Ha.
  { exploit precompute_r_t_up_t_black. rewrite Hprecompute_r_t_up.
    exploit precompute_r_t_up_r_in_g. rewrite Hprecompute_r_t_up.
    intros H2 H3. apply H2, H3.
    destruct H0 as (set & H0 &_).
    intros contra.
    exploit precompute_t_from_t_up_black_2; try eassumption.
    rewrite H0. discriminate.
    intros. apply in_map_iff in H1. destruct H1 as ((s, u') & H1' & H1).
    simpl in H1'. subst.
    exploit precompute_r_t_up_back_target_black. rewrite Hprecompute_r_t_up.
    intros. apply H4, H3 in H1. contradiction.
    apply g_reachable_closed.
    exploit precompute_r_t_up_back_in_g. rewrite Hprecompute_r_t_up.
    intros. apply H5 in H1 as H6.
    destruct H6 as (succs & H61 & H62).
    exploit precompute_r_t_up_back_source_black. rewrite Hprecompute_r_t_up.
    intros. apply H6, H2 in H1. destruct H1 as (H1 & _).
    eapply reachable_succ; eassumption.
  }
  apply H in H0; try assumption.
  apply Operators_Properties.clos_rt_rtn1_iff in H0.
  inv H0.
  - exploit precompute_r_t_up_r_in_g. rewrite Hprecompute_r_t_up.
    intros. apply H0. eauto.
  - exploit precompute_r_t_up_t_target_black; try eassumption. rewrite Hprecompute_r_t_up.
    intros. destruct H1 as (set & H11 & H12).
    eapply H0; try eassumption.
    apply g_reachable_closed.
    apply reachable_trans with y.
    + exploit precompute_r_t_up_r_in_g. rewrite Hprecompute_r_t_up.
      intros.
      exploit precompute_r_t_up_t_black. rewrite Hprecompute_r_t_up.
      intros.
      apply H1, H3. congruence.
    + exploit precompute_r_t_up_t_reachable; try eassumption. rewrite Hprecompute_r_t_up.
      intros.
      eauto.
Qed.

Lemma precompute_r_t_t_sorted : forall g root dom_pre
  (dom_pre_inj : forall u v,
    reachable g root u -> reachable g root v ->
    dom_pre u = dom_pre v -> u = v),
  let '(r, c, t, back) := precompute_r_t g root dom_pre in
  forall u set, t ! u = Some set ->
  Sorted (fun u v => dom_pre u < dom_pre v)%Z set.

Proof.

  intros.
  unfold precompute_r_t. unfold Time.time.
  destruct (precompute_r_t_up g root dom_pre)
    as (((r, c), t), back) eqn:Hprecompute_r_t_up.
  set (pre := fun u => match r ! u with | Some (n, _) => n | None => 1 end).
  apply precompute_t_from_t_up_sorted.
  - exploit precompute_r_t_up_t_dom_pre; try eassumption. rewrite Hprecompute_r_t_up. auto.
  - exploit precompute_r_t_up_t_sorted; try eassumption. rewrite Hprecompute_r_t_up. auto.
Qed.

Lemma precompute_r_t_back_in_g : forall g root dom_pre,
  let '(r, c, t, back) := precompute_r_t g root dom_pre in
  forall u v, In (u, v) back ->
  exists succs, g ! u = Some succs /\ In v succs.

Proof.

  intros.
  unfold precompute_r_t.
  destruct (precompute_r_t_up g root dom_pre)
    as (((r, c), t), back) eqn:Hprecompute_r_t_up.
  exploit precompute_r_t_up_back_in_g. rewrite Hprecompute_r_t_up. auto.
Qed.

Lemma precompute_r_t_back_numbering : forall g root dom_pre,
  let '(r, c, t, back) := precompute_r_t g root dom_pre in
  forall u v,
    In (u, v) back -> g ! v <> None ->
    directly_included r v u.

Proof.

  intros.
  unfold precompute_r_t.
  destruct (precompute_r_t_up g root dom_pre)
    as (((r, c), t), back) eqn:Hprecompute_r_t_up.
  exploit precompute_r_t_up_back_numbering. rewrite Hprecompute_r_t_up. auto.
Qed.

Lemma precompute_r_t_back_source_black : forall g root dom_pre,
let '(r, c, t, back) := precompute_r_t g root dom_pre in
forall u v, In (u, v) back -> r ! u <> None.

Proof.

  intros.
  unfold precompute_r_t.
  destruct (precompute_r_t_up g root dom_pre)
    as (((r, c), t), back) eqn:Hprecompute_r_t_up.
  exploit precompute_r_t_up_back_source_black. rewrite Hprecompute_r_t_up. auto.
Qed.

Lemma precompute_r_t_back_target_black : forall g root dom_pre,
let '(r, c, t, back) := precompute_r_t g root dom_pre in
forall u v, In (u, v) back -> g ! v <> None -> r ! v <> None.

Proof.

  intros.
  unfold precompute_r_t.
  destruct (precompute_r_t_up g root)
    as (((r, c), t), back) eqn:Hprecompute_r_t_up.
  exploit precompute_r_t_up_back_target_black. rewrite Hprecompute_r_t_up. auto.
Qed.

Lemma precompute_r_t_root_reduced_reachable : forall g root dom_pre,
let '(r, c, t, back) := precompute_r_t g root dom_pre in
forall u, r ! u <> None -> reduced_reachable g back root u.

Proof.

  intros.
  unfold precompute_r_t.
  destruct (precompute_r_t_up g root dom_pre)
    as (((r, c), t), back) eqn:Hprecompute_r_t_up.
  exploit precompute_r_t_up_root_reduced_reachable. rewrite Hprecompute_r_t_up.
  intros H. assumption.
Qed.

Corollary precompute_r_t_t_numbering : forall g root dom_pre
  (g_reachable_closed : forall u : positive, reachable g root u -> g ! u <> None)
  (dom_pre_inj : forall u v,
    reachable g root u -> reachable g root v ->
    dom_pre u = dom_pre v -> u = v),
  let '(r, c, t, back) := precompute_r_t g root dom_pre in
  forall u v, t_linked t u v ->
  exists n1 n2 m1 m2, r ! u = Some (n1, n2) /\ r ! v = Some (m1, m2)
    /\ m1 <= n1.

Proof.

  intros.
  unfold precompute_r_t. unfold Time.time.
  destruct (precompute_r_t_up g root dom_pre)
    as (((r, c), t_up), back) eqn:Hprecompute_r_t_up.
  exploit precompute_t_from_t_up_precompute_r_t_up; try eassumption. rewrite Hprecompute_r_t_up.
  set (pre := fun u => match r ! u with | Some (n, _) => n | None => 1 end).
  simpl. intros.
  assert (reachable g root u) as Ha.
  { exploit precompute_r_t_up_t_black. rewrite Hprecompute_r_t_up.
    exploit precompute_r_t_up_r_in_g. rewrite Hprecompute_r_t_up.
    intros H2 H3. apply H2, H3.
    destruct H0 as (set & H0 &_).
    intros contra.
    exploit precompute_t_from_t_up_black_2; try eassumption.
    rewrite H0. discriminate.
    intros. apply in_map_iff in H1. destruct H1 as ((s, u') & H1' & H1).
    simpl in H1'. subst.
    exploit precompute_r_t_up_back_target_black. rewrite Hprecompute_r_t_up.
    intros. apply H4, H3 in H1. contradiction.
    apply g_reachable_closed.
    exploit precompute_r_t_up_back_in_g. rewrite Hprecompute_r_t_up.
    intros. apply H5 in H1 as H6.
    destruct H6 as (succs & H61 & H62).
    exploit precompute_r_t_up_back_source_black. rewrite Hprecompute_r_t_up.
    intros. apply H6, H2 in H1. destruct H1 as (H1 & _).
    eapply reachable_succ; eassumption.
  }
  apply H in H0; try assumption.
  apply Operators_Properties.clos_rt_rt1n_iff in H0. induction H0.
  - exploit precompute_r_t_up_r_in_g. rewrite Hprecompute_r_t_up.
    intros.
    destruct (r ! x) as [(n1, n2)|] eqn:Hr.
    + eexists _, _, _, _. split; [reflexivity|]. split; [reflexivity|].
      reflexivity.
    + contradiction (proj2 (H0 x)); eauto.
  - assert (reachable g root y) as Hb.
    { exploit precompute_r_t_up_t_reachable; try eassumption. rewrite Hprecompute_r_t_up.
      intros. destruct H0 as (set & H01 & H02).
      eapply reachable_trans; eauto.
    }
    destruct (IHclos_refl_trans_1n Hb) as (m1 & m2 & o1 & o2 & H11 & H12 & H13).
    exploit precompute_r_t_up_t_numbering; try eassumption. rewrite Hprecompute_r_t_up.
    intros.
    destruct H0 as (set & H01 & H02).
    destruct (H2 _ _ _ H01 H02) as (n1 & n2 & m1' & m2' & H21 & H22 & H23).
    + eauto.
    + rewrite H22 in H11. inv H11. exists n1, n2, o1, o2.
      split; [assumption|]. split; [assumption|]. xomega.
Qed.

Corollary precompute_r_t_c_reduced_reachable : forall g root dom_pre,
  let '(r, c, t, back) := precompute_r_t g root dom_pre in
  forall u set v, c ! u = Some set -> set ! v = Some tt ->
  reduced_reachable g back u v.

Proof.

  intros.
  unfold precompute_r_t.
  destruct (precompute_r_t_up g root dom_pre)
    as (((r, c), t), back) eqn:Hprecompute_r_t_up.
  exploit precompute_r_t_up_c_reduced_reachable. rewrite Hprecompute_r_t_up. auto.
Qed.

Corollary precompute_r_t_t_reachable : forall g root dom_pre
  (g_reachable_closed : forall u : positive, reachable g root u -> g ! u <> None)
  (dom_pre_inj : forall u v,
    reachable g root u -> reachable g root v ->
    dom_pre u = dom_pre v -> u = v),
  let '(r, c, t, back) := precompute_r_t g root dom_pre in
  forall u v, t_linked t u v -> reachable g u v.

Proof.

  intros.
  unfold precompute_r_t. unfold Time.time.
  destruct (precompute_r_t_up g root dom_pre)
    as (((r, c), t_up), back) eqn:Hprecompute_r_t_up.
  exploit precompute_t_from_t_up_precompute_r_t_up; try eassumption. rewrite Hprecompute_r_t_up.
  set (pre := fun u => match r ! u with | Some (n, _) => n | None => 1 end).
  simpl. intros.
  assert (reachable g root u) as Ha.
  { exploit precompute_r_t_up_t_black. rewrite Hprecompute_r_t_up.
    exploit precompute_r_t_up_r_in_g. rewrite Hprecompute_r_t_up.
    intros H2 H3. apply H2, H3.
    destruct H0 as (set & H0 &_).
    intros contra.
    exploit precompute_t_from_t_up_black_2; try eassumption.
    rewrite H0. discriminate.
    intros. apply in_map_iff in H1. destruct H1 as ((s, u') & H1' & H1).
    simpl in H1'. subst.
    exploit precompute_r_t_up_back_target_black. rewrite Hprecompute_r_t_up.
    intros. apply H4, H3 in H1. contradiction.
    apply g_reachable_closed.
    exploit precompute_r_t_up_back_in_g. rewrite Hprecompute_r_t_up.
    intros. apply H5 in H1 as H6.
    destruct H6 as (succs & H61 & H62).
    exploit precompute_r_t_up_back_source_black. rewrite Hprecompute_r_t_up.
    intros. apply H6, H2 in H1. destruct H1 as (H1 & _).
    eapply reachable_succ; eassumption.
  }
  apply H in H0; try assumption.
  apply Operators_Properties.clos_rt_rt1n_iff in H0. induction H0.
  - constructor.
  - assert (reachable g x y) as Hb.
    { exploit precompute_r_t_up_t_reachable; try eassumption. rewrite Hprecompute_r_t_up.
      intros. destruct H0 as (set & H01 & H02).
      eauto.
    }
    apply reachable_trans with y.
    + assumption.
    + apply IHclos_refl_trans_1n. eapply reachable_trans; eassumption.
Qed.

Corollary precompute_r_t_reduced_reachable_numbering : forall g root dom_pre,
  let '(r, c, t, back) := precompute_r_t g root dom_pre in
  forall u v, reachable g root u -> g ! u <> None -> reduced_reachable g back u v ->
  exists n1 n2 m1 m2, r ! u = Some (n1, n2) /\ r ! v = Some (m1, m2)
    /\ m2 <= n2.

Proof.

  intros.
  unfold precompute_r_t.
  destruct (precompute_r_t_up g root dom_pre)
    as (((r, c), t), back) eqn:Hprecompute_r_t_up.
  exploit precompute_r_t_up_reduced_reachable_numbering. rewrite Hprecompute_r_t_up. auto.
Qed.

Corollary precompute_r_t_directly_included_cross_included :
  forall g root dom_pre,
  let '(r, c, t, back) := precompute_r_t g root dom_pre in
  forall u v, directly_included r u v -> cross_included r c u v.

Proof.

  intros.
  unfold precompute_r_t.
  destruct (precompute_r_t_up g root dom_pre)
    as (((r, c), t), back) eqn:Hprecompute_r_t_up.
  exploit precompute_r_t_up_directly_included_cross_included.
  rewrite Hprecompute_r_t_up. auto.
Qed.

Corollary precompute_r_t_back_reduced_reachable : forall g root dom_pre,
  let '(r, c, t, back) := precompute_r_t g root dom_pre in
  forall u v, In (u, v) back -> g ! v <> None ->
  reduced_reachable g back v u.

Proof.

  intros.
  unfold precompute_r_t.
  destruct (precompute_r_t_up g root dom_pre)
    as (((r, c), t), back) eqn:Hprecompute_r_t_up.
  exploit precompute_r_t_up_back_reduced_reachable. rewrite Hprecompute_r_t_up. auto.
Qed.

Lemma reduced_reachable_antisym : forall g root dom_pre,
  let '(r, c, t, back) := precompute_r_t g root dom_pre in
  forall u v,
  reachable g root u -> g ! u <> None ->
  reduced_reachable g back u v ->
  reduced_reachable g back v u ->
  u = v.

Proof.

  intros.
  destruct (precompute_r_t g root dom_pre)
    as (((r, c), t), back) eqn:Hprecompute_r_t.
  intros.
  exploit precompute_r_t_r_c_correct. rewrite Hprecompute_r_t. intros C_correct.
  assert (cross_included r c u v) as Ha.
  { apply C_correct. repeat split; assumption. }
  assert (reachable g root v) as Hb'.
  { eapply reachable_trans. eassumption.
    eapply reduced_reachable_is_reachable. eassumption.
  }
  assert (g ! v <> None) as Hb''.
  { apply reduced_reachable_equiv in H2. inv H2.
    - assumption.
    - congruence.
  }
  assert (cross_included r c v u) as Hb.
  { apply C_correct. repeat split; assumption. }
  exploit precompute_r_t_r_inj. rewrite Hprecompute_r_t. intros R_inj.
  exploit precompute_r_t_c_numbering. rewrite Hprecompute_r_t. intros C_numbering.
  exploit precompute_r_t_r_wf. rewrite Hprecompute_r_t. intros R_wf.
  destruct Ha as (set & w & Ha1 & Ha2 & Ha3).
  destruct (peq w u).
  - subst w.
    destruct Hb as (set' & w & Hb1 & Hb2 & Hb3).
    destruct (peq w v).
    + subst w.
      destruct Ha3 as (n1 & n2 & m1 & m2 & Ha31 & Ha32 & (Ha33 & _)).
      destruct Hb3 as (m1' & m2' & n1' & n2' & Hb31 & Hb32 & (Hb33 & _)).
      rewrite Hb31 in Ha32. inv Ha32.
      rewrite Hb32 in Ha31. inv Ha31.
      pose proof (Pos.le_antisym _ _ Ha33 Hb33). subst.
      eapply R_inj; eassumption.
    + destruct Ha3 as (n1 & n2 & m1 & m2 & Ha31 & Ha32 & (_ & Ha33)).
      destruct Hb3 as (o1 & o2 & n1' & n2' & Hb31 & Hb32 & (_ & Hb33)).
      rewrite Hb32 in Ha31. inv Ha31.
      exploit C_numbering; try eassumption.
      intros (m1' & m2' & o1' & o2' & H21 & H22 & H23).
      rewrite H21 in Ha32. inv Ha32.
      rewrite H22 in Hb31. inv Hb31.
      apply R_wf in H21. xomega.
  - destruct Ha3 as (o1 & o2 & m1 & m2 & Ha31 & Ha32 & (_ & Ha33)).
    exploit C_numbering; try eassumption.
    intros (n1 & n2 & o1' & o2' & H31 & H32 & H33).
    rewrite H32 in Ha31. inv Ha31.
    exploit precompute_r_t_reduced_reachable_numbering. rewrite Hprecompute_r_t.
    intros.
    apply H3 in H2; try assumption.
    destruct H2 as (m1' & m2' & n1' & n2' & H21 & H22 & H23).
    rewrite H21 in Ha32. inv Ha32.
    rewrite H22 in H31. inv H31.
    apply R_wf in H22. xomega.
Qed.