Module SSAfastliveprecomputeproof

Require Import Relation_Operators.

Require Import Coqlib.
Require Import Maps.

Require Import SSAfastliveprecomputeRT.
Require Import SSAfastliveprecomputeRTthm.
Require Import SSAfastliveprecomputeTT.
Require Import SSAfastliveprecomputeTTthm.

Local Open Scope positive_scope.

Corollary precompute_t_from_t_up_precompute_r_t_up :
  forall g root dom_pre
  (g_reachable_closed : forall u, 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_up, back) := precompute_r_t_up g root dom_pre in
  let pre u := match r ! u with | Some (n, _) => n | None => 1 end in
  forall u (u_reachable : reachable g root u) v,
  t_linked (precompute_t_from_t_up dom_pre pre t_up back) u v
  <-> clos_refl_trans _ (t_linked' t_up) u v.

Proof.

  intros.
  destruct (precompute_r_t_up g root dom_pre)
    as (((r, c), t_up), back) eqn:Hprecompute_r_t_up.
  intros.
  rewrite precompute_t_from_t_up_correct.
  - reflexivity.
  - intros.
    eapply dom_pre_inj; try assumption.
    + destruct H as [H|H].
      * exploit precompute_r_t_up_t_black. rewrite Hprecompute_r_t_up.
        intros. apply H2 in H.
        exploit precompute_r_t_up_r_in_g. rewrite Hprecompute_r_t_up.
        intros. apply H3 in H. destruct H as (H & _). assumption.
      * apply in_map_iff in H. destruct H as ((s, u0') & H' & H).
        simpl in H'. subst.
        exploit precompute_r_t_up_back_in_g. rewrite Hprecompute_r_t_up.
        intros. apply H2 in H as H3.
        destruct H3 as (succs & H31 & H32).
        exploit precompute_r_t_up_back_source_black.
        rewrite Hprecompute_r_t_up.
        intros. apply H3 in H.
        exploit precompute_r_t_up_r_in_g. rewrite Hprecompute_r_t_up.
        intros. apply H4 in H. destruct H as (H & _).
        eapply reachable_succ; eassumption.
    + destruct H0 as [H0|H0].
      * exploit precompute_r_t_up_t_black. rewrite Hprecompute_r_t_up.
        intros. apply H2 in H0.
        exploit precompute_r_t_up_r_in_g. rewrite Hprecompute_r_t_up.
        intros. apply H3 in H0. destruct H0 as (H0 & _). assumption.
      * apply in_map_iff in H0. destruct H0 as ((s, v0') & H0' & H0).
        simpl in H0'. subst.
        exploit precompute_r_t_up_back_in_g. rewrite Hprecompute_r_t_up.
        intros. apply H2 in H0 as H3.
        destruct H3 as (succs & H31 & H32).
        exploit precompute_r_t_up_back_source_black.
        rewrite Hprecompute_r_t_up.
        intros. apply H3 in H0.
        exploit precompute_r_t_up_r_in_g. rewrite Hprecompute_r_t_up.
        intros. apply H4 in H0. destruct H0 as (H0 & _).
        eapply reachable_succ; eassumption.
  - intros. exploit precompute_r_t_up_t_dom_pre; try eassumption. rewrite Hprecompute_r_t_up.
    intros. eapply H0; eassumption.
  - intros. exploit precompute_r_t_up_t_sorted; try eassumption. rewrite Hprecompute_r_t_up.
    intros. eapply H0; eassumption.
  - intros. exploit precompute_r_t_up_t_numbering; try eassumption. rewrite Hprecompute_r_t_up.
    intros. destruct H as (set & HH0 & HH1).
    destruct (H0 _ _ _ HH0 HH1) as (n1 & n2 & m1 & m2 & H11 & H12 & H13).
    + apply g_reachable_closed.
      exploit precompute_r_t_up_t_reachable; try eassumption. rewrite Hprecompute_r_t_up.
      intros.
      eapply reachable_trans; try (eapply H; eassumption).
      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 H1 H2. apply H1, H2. congruence.
    + unfold pre. rewrite H11, H12. assumption.
  - intros. exploit precompute_r_t_up_t_correct; try eassumption. rewrite Hprecompute_r_t_up.
    intros. apply H0 in H.
    destruct H as (_ & (_ & s & H & _)).
    apply in_map_iff. eexists (_, _); split; [reflexivity|eassumption].
  - intros.
    assert (r ! u0 <> None) as Ha.
    { apply in_map_iff in H. destruct H as ((s, u0') & H' & H).
      simpl in H'. 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 H 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 H.
      exploit precompute_r_t_up_r_in_g. rewrite Hprecompute_r_t_up.
      intros. apply H5 in H. destruct H as (H & _).
      eapply reachable_succ; eassumption.
    }
    assert (r ! v0 <> None) as Hb.
    { apply in_map_iff in H0. destruct H0 as ((s, v0') & H0' & H0).
      simpl in H0'. 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 H0 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 H0.
      exploit precompute_r_t_up_r_in_g. rewrite Hprecompute_r_t_up.
      intros. apply H5 in H0. destruct H0 as (H0 & _).
      eapply reachable_succ; eassumption.
    }
    exploit precompute_r_t_up_r_inj. rewrite Hprecompute_r_t_up.
    intros.
    destruct (r ! u0) as [(n1, n2)|] eqn:Hru0; [|contradiction].
    destruct (r ! v0) as [(m1, m2)|] eqn:Hrv0; [|contradiction].
    unfold pre in H1. rewrite Hru0, Hrv0 in H1. subst m1.
    eapply H2; eassumption.
  - exploit precompute_r_t_up_t_black. rewrite Hprecompute_r_t_up.
    intros. apply H.
    exploit precompute_r_t_up_r_in_g. rewrite Hprecompute_r_t_up.
    intros. apply H0. split; auto.
Qed.