Module SSAfastliveprecomputeTTthm

Require Import Relation_Operators.
Require Import Sorted.

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

Require Import SSAfastliveprecomputeRT.
Require Import SSAfastliveprecomputeTT.
Require Import SSAfastliveprecomputeTTproof.

Local Open Scope positive_scope.

Export Definitions.

Lemma star_trans_eq : forall A (R1 R2:A->A->Prop),
(forall i j, R1 i j -> R2** i j) ->
forall i j, R1** i j -> R2** i j.

Proof.

  induction 2.
  eauto.
  constructor 2.
  econstructor 3; eassumption.
Qed.

Theorem precompute_t_from_t_up_correct :
  forall (dom_pre : node -> Z) (pre : node -> positive)
    (t : PTree.t (list (node * Z))) (back : list (node * node))
  (dom_pre_inj : forall (u v : node),
    t ! u <> None \/ In u (map snd back) ->
    t ! v <> None \/ In v (map snd back) ->
    dom_pre u = dom_pre v -> u = v)
  (t_dom_pre : forall (u : node) set, t ! u = Some set ->
    Forall (fun '(u, n) => n = dom_pre u) set)
  (t_sorted : forall (u : node) set, t ! u = Some set ->
    Sorted (fun '(_, n1) '(_, n2) => n1 < n2)%Z set)
  (t_pre : forall u v, t_linked' t u v -> pre v < pre u)
  (t_in_back : forall u v, t_linked' t u v -> In v (map snd back))
  (pre_inj : forall u v, In u (map snd back) -> In v (map snd back) ->
    pre u = pre v -> u = v)
  (u : node) (u_in_t : t ! u <> None) v,
  t_linked (precompute_t_from_t_up dom_pre pre t back) u v
  <-> clos_refl_trans _ (t_linked' t) u v.

Proof.

  intros. unfold precompute_t_from_t_up. unfold Time.time.
  rewrite precompute_t_from_t_up_2_correct with (back:=back).
  - (* the proof is a bit long because the correction theorem
       of precompute_t_from_t_up_2 treats identically the cases
       "u in back" and "u not in back"
    *)
    clear u_in_t. split; revert u v.
    + apply star_trans_eq. intros.
      destruct (in_dec peq i (List.map snd back)).
      * eapply precompute_t_from_t_up_1_back; eauto.
      * destruct H as (set & H1 & H2). apply rt_step.
        rewrite precompute_t_from_t_up_1_not_back in H1
          by assumption.
        eexists; split; eassumption.
    + apply star_eq. intros.
      destruct (in_dec peq i (List.map snd back)).
      * apply precompute_t_from_t_up_1_back; eauto.
      * destruct H as (set & H1 & H2). exists set. split; [|assumption].
        rewrite precompute_t_from_t_up_1_not_back by assumption.
        assumption.
  - intros.
    destruct (in_dec peq u0 (map snd back)).
    + destruct (in_dec peq v0 (map snd back)).
      * auto.
      * destruct H0 as [H0|H0]; [|contradiction].
        rewrite precompute_t_from_t_up_1_not_back in H0 by assumption.
        auto.
    + destruct H as [H|H]; [|contradiction].
      rewrite precompute_t_from_t_up_1_not_back in H by assumption.
      destruct (in_dec peq v0 (map snd back)).
      * auto.
      * destruct H0 as [H0|H0]; [|contradiction].
        rewrite precompute_t_from_t_up_1_not_back in H0 by assumption.
        auto.
  - apply Precompute_t_from_t_up_back_targets.precompute_t_from_t_up_1_dom_pre; eauto.
  - intros.
    destruct (in_dec peq u0 (List.map snd back)).
    + apply -> precompute_t_from_t_up_1_back in H; eauto.
      apply Operators_Properties.clos_rt_rtn1_iff in H. inv H; eauto.
    + destruct H as (set & H1 & H2).
      rewrite precompute_t_from_t_up_1_not_back in H1
        by assumption.
      eapply t_in_back. eexists; split; eassumption.
  - intros.
    apply <- precompute_t_from_t_up_1_back; eauto.
  - intros. apply precompute_t_from_t_up_1_back in H0; eauto.
    apply -> precompute_t_from_t_up_1_back in H1; eauto.
    apply <- precompute_t_from_t_up_1_back; eauto.
    apply -> Operators_Properties.clos_rt_rtn1_iff in H0.
    inv H0; eauto.
  - apply precompute_t_from_t_up_1_black. assumption.
Qed.

Theorem precompute_t_from_t_up_black : forall dom_pre pre t back u,
t ! u <> None ->
(precompute_t_from_t_up dom_pre pre t back) ! u <> None.

Proof.

  intros.
  unfold precompute_t_from_t_up. unfold Time.time.
  apply precompute_t_from_t_up_2_black,
        precompute_t_from_t_up_1_black.
  assumption.
Qed.

Theorem precompute_t_from_t_up_black_2 : forall dom_pre pre t back u,
  (precompute_t_from_t_up dom_pre pre t back) ! u <> None ->
  t ! u = None ->
  In u (map snd back).

Proof.

  intros.
  unfold precompute_t_from_t_up in H. unfold Time.time in H.
  apply precompute_t_from_t_up_2_black,
        precompute_t_from_t_up_1_black_2 in H;
    assumption.
Qed.

Theorem precompute_t_from_t_up_sorted : forall dom_pre pre t back
  (t_dom_pre : forall u set, t ! u = Some set ->
    Forall (fun '(u, n) => n = dom_pre u) set)
  (t_sorted : forall u set, t ! u = Some set ->
    Sorted (fun '(_, n1) '(_, n2) => n1 < n2)%Z set)
  u set,
  (precompute_t_from_t_up dom_pre pre t back) ! u = Some set ->
  Sorted (fun u v => dom_pre u < dom_pre v)%Z set.

Proof.

  intros.
  unfold precompute_t_from_t_up in H. unfold Time.time in H.
  revert u set H.
  apply precompute_t_from_t_up_2_sorted.
  - apply precompute_t_from_t_up_1_dom_pre; assumption.
  - apply precompute_t_from_t_up_1_sorted; assumption.
Qed.