Module SSAfastliveprecomputeRTthm

Require Import List. Import ListNotations.
Require Import Wellfounded.
Require Import Sorted.

Require Import Coqlib.
Require Import Maps.

Require Import SSAfastliveutils.
Require Import SSAfastliveprecomputeRT.
Require Import SSAfastliveprecomputeRTproof.

Local Open Scope positive_scope.

Export Definitions.



Lemma precompute_r_t_up_r_in_g : forall g root dom_pre,
  let '(r, c, t, back) := precompute_r_t_up g root dom_pre in
  forall u,
  r ! u <> None <-> reachable g root u /\ g ! u <> None.
Proof.
  intros.
  destruct (precompute_r_t_up g root dom_pre) as (((r, c), t), back) eqn:Hprecompute_r_t_up.
  exploit precompute_r_t_up_correct_1. rewrite Hprecompute_r_t_up.
  intros (_ & H & _).
  exploit precompute_r_t_up_correct_5. rewrite Hprecompute_r_t_up.
  intros (H1 & _).
  split; intros.
  - eauto.
  - destruct H0; eauto.
Qed.

Lemma precompute_r_t_up_r_inj : forall g root dom_pre,
  let '(r, c, t, back) := precompute_r_t_up 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.
  destruct (precompute_r_t_up g root dom_pre) as (((r, c), t), back) eqn:Hprecompute_r_t_up.
  exploit precompute_r_t_up_correct_1. rewrite Hprecompute_r_t_up.
  intros (H & _). assumption.
Qed.

Lemma precompute_r_t_up_r_wf : forall g root dom_pre,
  let '(r, c, t, back) := precompute_r_t_up g root dom_pre in
  forall u n1 n2,
  r ! u = Some (n1, n2) -> Ple n1 n2.
Proof.
  intros.
  destruct (precompute_r_t_up g root dom_pre) as (((r, c), t), back) eqn:Hprecompute_r_t_up.
  exploit precompute_r_t_up_correct_1. rewrite Hprecompute_r_t_up.
  intros (_ & _ & H). assumption.
Qed.

Lemma precompute_r_t_up_r_cases : forall g root dom_pre,
  let '(r, c, t, back) := precompute_r_t_up 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.
  destruct (precompute_r_t_up g root dom_pre) as (((r, c), t), back) eqn:Hprecompute_r_t_up.
  exploit precompute_r_t_up_correct_2. rewrite Hprecompute_r_t_up.
  intros (_ & H). assumption.
Qed.


Lemma precompute_r_t_up_r_c_correct : forall g root dom_pre,
  let '(r, c, t, back) := precompute_r_t_up 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.
  destruct (precompute_r_t_up g root dom_pre) as (((r, c), t), back) eqn:Hprecompute_r_t_up.
  split; intros.
  - destruct H as (set & w & HH1 & HH2 & HH3).
    apply and_assoc. split.
    * exploit precompute_r_t_up_correct_5. rewrite Hprecompute_r_t_up.
      intros (H0 & H1 & _).
      apply H0, H1. congruence.
    * eapply reduced_reachable_trans.
      -- exploit precompute_r_t_up_correct_3. rewrite Hprecompute_r_t_up.
         intros. eapply H. eassumption. eassumption.
      -- exploit precompute_r_t_up_correct_2. rewrite Hprecompute_r_t_up.
         intros. destruct HH3 as (n1 & n2 & m1 & m2 & HH3).
         eapply H; apply HH3.
  - destruct H as (H & H0 & H1).
    exploit precompute_r_t_up_correct_4. rewrite Hprecompute_r_t_up.
    intros H2. apply H2; try assumption.
    exploit precompute_r_t_up_correct_5. rewrite Hprecompute_r_t_up.
    intros (_ & _ & H3 & _).
    inversion H1. congruence.
    intros contra. contradiction H7. eapply H3; try eassumption.
    exploit precompute_r_t_up_correct_1. rewrite Hprecompute_r_t_up. intros (_ & H9).
    apply H9. eapply reachable_trans. eassumption.
    eapply reduced_reachable_is_reachable. eassumption. congruence.
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.
  destruct (precompute_r_t_up g root dom_pre) as (((r, c), t), back) eqn:Hprecompute_r_t_up.
  exploit precompute_r_t_up_correct_4. rewrite Hprecompute_r_t_up.
  intros (_ & _ & H). assumption.
Qed.

Lemma precompute_r_t_up_c_numbering : forall g root dom_pre,
  let '(r, c, t, back) := precompute_r_t_up 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.
  exact precompute_r_t_up_correct_8.
Qed.

Lemma precompute_r_t_up_c_black : forall g root dom_pre,
  let '(r, c, t, back) := precompute_r_t_up g root dom_pre in
  forall u, c ! u <> None -> r ! u <> None.
Proof.
  intros.
  destruct (precompute_r_t_up g root dom_pre) as (((r, c), t), back) eqn:Hprecompute_r_t_up.
  exploit precompute_r_t_up_correct_5. rewrite Hprecompute_r_t_up.
  intros (_ & H & _). assumption.
Qed.

Lemma precompute_r_t_up_c_target_black : forall g root dom_pre,
  let '(r, c, t, back) := precompute_r_t_up g root dom_pre in
  forall u set v, c ! u = Some set -> set ! v = Some tt ->
  r ! v <> None.
Proof.
  intros.
  destruct (precompute_r_t_up g root dom_pre) as (((r, c), t), back) eqn:Hprecompute_r_t_up.
  exploit precompute_r_t_up_correct_4. rewrite Hprecompute_r_t_up.
  intros (_ & H & _). assumption.
Qed.


Lemma precompute_r_t_up_t_correct : 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_up g root dom_pre in
  forall u v,
    (exists set, t ! u = Some set /\ In v (map fst set))
    <-> (reachable g root u /\ is_in_t_up g back u v).
Proof.
  intros.
  destruct (precompute_r_t_up g root dom_pre) as (((r, c), t), back) eqn:Hprecompute_r_t_up.
  exploit precompute_r_t_up_correct_6; try eassumption.
  rewrite Hprecompute_r_t_up.
  intros. split; intros.
  - apply H in H0. destruct H0 as (H01 & _ & H02). split; assumption.
  - destruct H0 as (H01 & H02).
    apply H.
    split; [assumption|]. split; [|assumption].
    destruct H02 as (H021 & s & H022 & H023).
    apply reduced_reachable_equiv in H023.
    inv H023.
    + exploit precompute_r_t_up_correct_5. rewrite Hprecompute_r_t_up.
      intros (H1 & _ & _ & H2 & _ & _). eapply H1, H2, H022.
    + congruence.
Qed.

Lemma precompute_r_t_up_t_black : forall g root dom_pre,
  let '(r, c, t, back) := precompute_r_t_up g root dom_pre in
  forall u, t ! u <> None <-> r ! u <> None.
Proof.
  intros.
  destruct (precompute_r_t_up g root) as (((r, c), t), back) eqn:Hprecompute_r_t_up.
  exploit precompute_r_t_up_correct_5. rewrite Hprecompute_r_t_up.
  intros (_ & _ & _ & _ & H & _). assumption.
Qed.

Lemma precompute_r_t_up_t_target_black : 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_up g root dom_pre in
  forall u set v, t ! u = Some set -> In v (map fst set) -> g ! v <> None ->
  r ! v <> None.
Proof.
  intros.
  destruct (precompute_r_t_up g root dom_pre) as (((r, c), t), back) eqn:Hprecompute_r_t_up.
  exploit precompute_r_t_up_correct_7. rewrite Hprecompute_r_t_up.
  intros H.
  intros.
  assert (is_in_t_up g back u v) as Ha.
  { exploit precompute_r_t_up_correct_6; try eassumption. rewrite Hprecompute_r_t_up.
    intros H3. apply H3. eauto.
  }
  destruct Ha as (_ & s & Ha & _).
  destruct (H _ _ Ha H2) as (m1 & m2 & _ & _ & H3 & _ & _).
  congruence.
Qed.

Lemma precompute_r_t_up_t_dom_pre : 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_up g root dom_pre in
  forall u set, t ! u = Some set ->
  Forall (fun '(u, n) => n = dom_pre u) set.
Proof.
  intros.
  destruct (precompute_r_t_up g root dom_pre) as (((r, c), t), back) eqn:Hprecompute_r_t_up.
  exploit precompute_r_t_up_correct_9. rewrite Hprecompute_r_t_up.
  intros (H & _). assumption.
Qed.

Lemma precompute_r_t_up_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_up g root dom_pre in
  forall u set, t ! u = Some set ->
  Sorted (fun '(_, n1) '(_, n2) => n1 < n2)%Z set.
Proof.
  intros.
  destruct (precompute_r_t_up g root dom_pre) as (((r, c), t), back) eqn:Hprecompute_r_t_up.
  exploit precompute_r_t_up_correct_9. rewrite Hprecompute_r_t_up.
  intros (_ & H). assumption.
Qed.


Lemma precompute_r_t_up_back_in_g : forall g root dom_pre,
  let '(r, c, t, back) := precompute_r_t_up g root dom_pre in
  forall u v, In (u, v) back ->
  exists succs, g ! u = Some succs /\ In v succs.
Proof.
  intros.
  destruct (precompute_r_t_up g root dom_pre) as (((r, c), t), back) eqn:Hprecompute_r_t_up.
  exploit precompute_r_t_up_correct_5.
  rewrite Hprecompute_r_t_up.
  intros (_ & _ & _ & _ & _ & H). assumption.
Qed.

Lemma precompute_r_t_up_back_numbering : forall g root dom_pre,
  let '(r, c, t, back) := precompute_r_t_up g root dom_pre in
  forall u v,
    In (u, v) back -> g ! v <> None ->
    directly_included r v u.
Proof.
  exact precompute_r_t_up_correct_7.
Qed.

Lemma precompute_r_t_up_back_source_black : forall g root dom_pre,
  let '(r, c, t, back) := precompute_r_t_up g root dom_pre in
  forall u v, In (u, v) back -> r ! u <> None.
Proof.
  intros.
  destruct (precompute_r_t_up g root dom_pre) as (((r, c), t), back) eqn:Hprecompute_r_t_up.
  exploit precompute_r_t_up_correct_5. rewrite Hprecompute_r_t_up.
  intros (_ & _ & _ & H & _). assumption.
Qed.

Lemma precompute_r_t_up_back_target_black : forall g root dom_pre,
  let '(r, c, t, back) := precompute_r_t_up g root dom_pre in
  forall u v, In (u, v) back -> g ! v <> None -> r ! v <> None.
Proof.
  intros.
  destruct (precompute_r_t_up g root dom_pre) as (((r, c), t), back) eqn:Hprecompute_r_t_up.
  exploit precompute_r_t_up_correct_7. rewrite Hprecompute_r_t_up.
  intros. destruct (H _ _ H0 H1) as (m1 & m2 & _ & _ & H2 & _ & _).
  congruence.
Qed.


Lemma precompute_r_t_up_root_reduced_reachable : forall g root dom_pre,
  let '(r, c, t, back) := precompute_r_t_up g root dom_pre in
  forall u, r ! u <> None -> reduced_reachable g back root u.
Proof.
  intros.
  destruct (precompute_r_t_up g root dom_pre) as (((r, c), t), back) eqn:Hprecompute_r_t_up.
  exploit precompute_r_t_up_correct_10. rewrite Hprecompute_r_t_up.
  intros H. assumption.
Qed.



Corollary precompute_r_t_up_t_numbering : 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_up g root dom_pre in
  forall u set v, t ! u = Some set -> In v (map fst set) ->
  g ! v <> None ->
  exists n1 n2 m1 m2, r ! u = Some (n1, n2) /\ r ! v = Some (m1, m2)
    /\ m1 < n1.
Proof.
  intros.
  destruct (precompute_r_t_up g root dom_pre) as (((r, c), t), back) eqn:Hprecompute_r_t_up.
  intros.
  assert (is_in_t_up g back u v) as Ha.
  { exploit precompute_r_t_up_t_correct; try eassumption. rewrite Hprecompute_r_t_up. intros H2.
    apply H2; eauto.
  }
  destruct Ha as (Ha1 & s & Ha2 & Ha3).
  assert (cross_included r c u s) as Hb.
  { exploit precompute_r_t_up_r_c_correct. rewrite Hprecompute_r_t_up.
    intros H2. apply H2. apply and_assoc. split; [|assumption].
    exploit precompute_r_t_up_r_in_g. rewrite Hprecompute_r_t_up. intros H3. apply H3.
    exploit precompute_r_t_up_t_black. rewrite Hprecompute_r_t_up. intros H4.
    apply H4. congruence.
  }
  assert (directly_included r v s) as Hc.
  { exploit precompute_r_t_up_back_numbering. rewrite Hprecompute_r_t_up. eauto. }
  assert (~ cross_included r c u v) as Hd.
  { intros contra. apply Ha1.
    exploit precompute_r_t_up_r_c_correct. rewrite Hprecompute_r_t_up.
    intros H2. apply H2. assumption.
  }
  destruct Hb as (set' & w & H21 & H22 & H23).
  destruct (peq w u).
  - subst w.
    destruct H23 as (n1 & n2 & m1 & m2 & H231 & H232 & H233).
    destruct Hc as (o1 & o2 & m1' & m2' & Hc1 & Hc2 & Hc3).
    rewrite Hc2 in H232. inv H232.
    exploit precompute_r_t_up_r_cases. rewrite Hprecompute_r_t_up.
    intros H2. specialize (H2 _ _ _ _ _ _ H231 Hc1).
    rewrite <- or_assoc in H2.
    destruct H2 as [H2|[H2|H2]].
    + (* impossible : r ! s is included both in r ! u and r ! v.
         They thus cannot be disjoint. *)
      unfold is_included in H233, Hc3.
      exploit precompute_r_t_up_r_wf. rewrite Hprecompute_r_t_up.
      intros H3. specialize (H3 _ _ _ H231).
      exploit precompute_r_t_up_r_wf. rewrite Hprecompute_r_t_up.
      intros H4. specialize (H4 _ _ _ Hc2).
      xomega.
    + (* impossible : v is reachable from u *)
      contradiction Hd.
      exists set', u. split; [assumption|]. split; [assumption|].
      eexists _, _, _, _. split; [eassumption|]. split; [eassumption|].
      assumption.
    + (* s is reachable from u which is reachable from v, thus the result *)
      eexists _, _, _, _. split; [eassumption|]. split; [eassumption|].
      destruct H2 as (H2 & _).
      assert (o1 = n1 \/ o1 < n1) by xomega.
      destruct H3; [|assumption].
 u = v *)      subst o1.
      contradiction Hd.
      exploit precompute_r_t_up_r_inj. rewrite Hprecompute_r_t_up.
      intros H3. specialize (H3 _ _ _ _ _ H231 Hc1). subst v.
      exists set', u. split; [assumption|]. split; [assumption|].
      apply directly_included_refl; congruence.
  - destruct H23 as (m1 & m2 & o1 & o2 & H231 & H232 & H233).
    exploit precompute_r_t_up_c_numbering.
    rewrite Hprecompute_r_t_up. intros H3.
    specialize (H3 _ _ _ H21 H22 n).
    destruct H3 as (n1 & n2 & m1' & m2' & H31 & H32 & H33).
    rewrite H32 in H231. inv H231.
    destruct Hc as (p1 & p2 & o1' & o2' & Hc1 & Hc2 & Hc3).
    rewrite Hc2 in H232. inv H232.
    eexists _, _, _, _. split; [eassumption|]. split; [eassumption|].
    unfold is_included in H233, Hc3.
    exploit precompute_r_t_up_r_wf. rewrite Hprecompute_r_t_up.
    intros H4. specialize (H4 _ _ _ Hc2). xomega.
Qed.

Corollary precompute_r_t_up_c_reduced_reachable : forall g root dom_pre,
  let '(r, c, t, back) := precompute_r_t_up 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.
  destruct (precompute_r_t_up g root dom_pre) as (((r, c), t), back) eqn:Hprecompute_r_t_up.
  intros.
  exploit precompute_r_t_up_r_c_correct. rewrite Hprecompute_r_t_up.
  intros. apply H1.
  eexists _, _. split; [eassumption|]. split; [eassumption|].
  apply directly_included_refl.
  exploit precompute_r_t_up_c_target_black. rewrite Hprecompute_r_t_up. eauto.
Qed.

Corollary precompute_r_t_up_t_reachable : 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_up g root dom_pre in
  forall u set v, t ! u = Some set -> In v (map fst set) ->
  reachable g u v.
Proof.
  intros.
  destruct (precompute_r_t_up g root dom_pre) as (((r, c), t), back) eqn:Hprecompute_r_t_up.
  intros.
  exploit precompute_r_t_up_t_correct; try eassumption. rewrite Hprecompute_r_t_up.
  intros.
  exploit (proj1 (H1 u v)).
  eexists. split; eassumption.
  intros (_ & H2).
  destruct H2 as (_ & s & H21 & H22).
  exploit precompute_r_t_up_back_in_g. rewrite Hprecompute_r_t_up. intros H3.
  apply H3 in H21. destruct H21 as (succs & H211 & H212).
  apply reduced_reachable_is_reachable in H22.
  eapply reachable_trans. eassumption.
  econstructor; [constructor|eassumption..].
Qed.

Corollary precompute_r_t_up_reduced_reachable_numbering : forall g root dom_pre,
  let '(r, c, t, back) := precompute_r_t_up 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.
  destruct (precompute_r_t_up g root dom_pre) as (((r, c), t), back) eqn:Hprecompute_r_t_up.
  intros.
  exploit precompute_r_t_up_r_c_correct. rewrite Hprecompute_r_t_up.
  intros.
  exploit (proj2 (H2 u v)). repeat split; assumption.
  intros.
  destruct H3 as (set & w & H31 & H32 & H33).
  destruct (peq w u).
  - subst w.
    destruct H33 as (m1 & m2 & o1 & o2 & H331 & H332 & (_ & H333)).
    eexists _, _, _, _. split; [eassumption|]. split; [eassumption|].
    assumption.
  - destruct H33 as (m1 & m2 & o1 & o2 & H331 & H332 & (_ & H333)).
    exploit precompute_r_t_up_c_numbering. rewrite Hprecompute_r_t_up.
    intros.
    exploit H3; try eassumption.
    intros (n1 & n2 & m1' & m2' & H41 & H42 & H43).
    rewrite H42 in H331. inv H331.
    exists n1, n2, o1, o2. split; [assumption|]. split; [assumption|].
    exploit precompute_r_t_up_r_wf. rewrite Hprecompute_r_t_up.
    intros. apply H4 in H41. xomega.
Qed.

Corollary precompute_r_t_up_directly_included_cross_included :
  forall g root dom_pre,
  let '(r, c, t, back) := precompute_r_t_up g root dom_pre in
  forall u v, directly_included r u v -> cross_included r c u v.
Proof.
  intros.
  destruct (precompute_r_t_up g root dom_pre) as (((r, c), t), back) eqn:Hprecompute_r_t_up.
  intros.
  exploit precompute_r_t_up_c_refl. rewrite Hprecompute_r_t_up.
  intros. destruct (H0 u) as (set & H01 & H02).
  destruct H as (n1 & n2 & _ & _ & H & _). congruence.
  exists set, u. split; [assumption|]. split; [assumption|]. assumption.
Qed.

Corollary precompute_r_t_up_back_reduced_reachable : forall g root dom_pre,
  let '(r, c, t, back) := precompute_r_t_up g root dom_pre in
  forall u v, In (u, v) back -> g ! v <> None ->
  reduced_reachable g back v u.
Proof.
  intros.
  destruct (precompute_r_t_up g root dom_pre) as (((r, c), t), back) eqn:Hprecompute_r_t_up.
  intros.
  exploit precompute_r_t_up_back_numbering. rewrite Hprecompute_r_t_up.
  intros.
  exploit precompute_r_t_up_r_c_correct. rewrite Hprecompute_r_t_up.
  intros.
  exploit (proj1 (H2 v u)).
  exploit precompute_r_t_up_directly_included_cross_included.
  rewrite Hprecompute_r_t_up. auto.
  intros (_ & _ & H3). assumption.
Qed.
Generated by coq2html