Module SSAfastliveprecomputeTTproof

Require Import Relation_Operators.
Require Import Sorted.
Import List.ListNotations.

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

Require Import SSAfastliveutils.
Require Import SSAfastliveprecomputeRT.
Require Import SSAfastliveprecomputeRTthm.
Require Import SSAfastliveprecomputeTT.

Local Open Scope positive_scope.
Local Opaque ZSortWithIndex.merge.

Module Import Definitions.

Definition is_in_t g back := clos_refl_trans _ (is_in_t_up g back).

Definition t_linked t (u v : node) := exists set, t ! u = Some set /\ In v set.
Definition t_linked' t (u v : node) := exists (set : list (node * Z)), t ! u = Some set /\ In v (List.map fst set).

End Definitions.

Lemma precompute_t_from_t_up_1_not_back :
  forall dom_pre pre t back u
  (u_not_target : ~ In u (List.map snd back)),
  (precompute_t_from_t_up_1 dom_pre pre t back) ! u =
  t ! u.

Proof.

  intros. unfold precompute_t_from_t_up_1.
  apply fold_invariant.
  - reflexivity.
  - intros.
    rewrite PTree.gso.
    assumption.
    intros contra. subst x.
    apply PosSortWithIndex.incl_sort in H.
    apply in_map_iff in H. destruct H as ((s, u') & H' & H).
    simpl in H'. subst u'.
    contradiction u_not_target.
    apply in_map_iff. eexists (_, _); split; [reflexivity|eassumption].
Qed.

Lemma equation1 : forall g back u v,
is_in_t g back u v <-> u = v \/ exists w, is_in_t_up g back u w /\ is_in_t g back w v.

Proof.

  split; intros.
  - apply Utils.Rstar_left_case in H. assumption.
  - destruct H.
    + subst. apply rt_refl.
    + destruct H as (w & H1 & H2).
      eapply rt_trans. apply rt_step. eassumption.
      assumption.
Qed.

Lemma precompute_t_from_t_up_1_back_1 :
  forall dom_pre pre t back u v,
  t_linked' (precompute_t_from_t_up_1 dom_pre pre t back) u v ->
  clos_refl_trans _ (t_linked' t) u v.

Proof.

  intros.
  revert u v H.
  unfold precompute_t_from_t_up_1.
  apply fold_invariant; intros.
  - apply rt_step. assumption.
  - unfold t_linked' in H1.
    rewrite PTree.gsspec in H1.
    destruct (peq u x); [|eauto].
    destruct H1 as (set' & H11 & H12).
    inv H11.
    apply in_map_iff in H12. destruct H12 as ((v', n_v) & H12' & H12).
    simpl in H12'. subst.
    destruct (t0 ! x) as [set|] eqn:Ht0.
    + apply ZSortWithIndex.incl_merge in H12. simpl in H12.
      destruct H12 as [H12|H12].
      * inv H12. apply rt_refl.
      * revert H12.
        apply fold_invariant.
        -- intros [].
        -- intros (w, n_w) set'. intros.
           destruct (t0 ! w) as [set''|] eqn:Ht0'.
           ++ apply ZSortWithIndex.incl_merge in H12.
              rewrite in_app_iff in H12. destruct H12 as [H12|H12].
              ** eapply rt_trans.
                 --- apply H0. exists set. split; [assumption|].
                     apply in_map_iff.
                     eexists (_, _); split; [reflexivity|eassumption].
                 --- apply H0. exists set''. split; [assumption|].
                     apply in_map_iff.
                     eexists (_, _); split; [reflexivity|eassumption].
              ** apply H2. assumption.
           ++ auto.
    + destruct H12 as [H12|[]].
      inv H12. apply rt_refl.
Qed.

Module Precompute_t_from_t_up_back_targets.

Module Import Postorder.

Module Import State.

Record state : Type := mkstate {
  l: list node; (* current list, without already-visited nodes *)
  t : PTree.t (list (node * Z)) (* current result *)
}.

End State.

Definition init_state t back :=
  {| l := back; t := t |}.

Definition transition dom_pre (s: state) : PTree.t (list (node * Z)) + state :=
  match s.(l) with
  | nil => inl _ s.(t)
  | u :: m =>
    let set :=
      match s.(t) ! u with
      | None => [(u, dom_pre u)]
      | Some set =>
        let set := List.fold_left (fun acc '((u, _) : node * Z) =>
          match s.(t) ! u with
          | None => acc
          | Some s => ZSortWithIndex.merge s acc
          end) set []
        in
        ZSortWithIndex.merge [(u, dom_pre u)] set
      end
    in
    let t' := PTree.set u set s.(t) in
    inr _ {| l := m; t := t' |}
  end.

Definition f (dom_pre : node -> Z)
  : PTree.t (list (node * Z)) -> node -> PTree.t (list (node * Z))
  := (fun t u =>
    let s :=
      match t ! u with
      | None => [(u, dom_pre u)]
      | Some s =>
        let s := List.fold_left (fun acc '(u, _) =>
          match t ! u with
          | None => acc
          | Some s => ZSortWithIndex.merge s acc
          end) s []
        in
        ZSortWithIndex.merge [(u, dom_pre u)] s
      end
    in
    PTree.set u s t
  ).

Section POSTORDER.

Variable dom_pre : node -> Z.
Variable pre : node -> positive.
Variable tinit : PTree.t (list (node * Z)).
Variable back_targets: list node.

Hypothesis dom_pre_inj : forall u v,
  In u back_targets -> In v back_targets ->
  dom_pre u = dom_pre v -> u = v.
Hypothesis t_pre : forall u v, t_linked' tinit u v -> pre v < pre u.
Hypothesis t_in_back_targets : forall u v, t_linked' tinit u v -> In v back_targets.

Inductive invariant (s: state) : Prop :=
  Invariant
    (SORTED : Sorted (fun u v => pre u < pre v) s.(l))
    (SORTED_DONE : forall u v, In u back_targets -> ~ In u s.(l) -> In v s.(l) -> pre u < pre v)
    (INCL : incl s.(l) back_targets)
    (T_TODO : forall u, In u s.(l) -> s.(t) ! u = tinit ! u)
    (T_IN_BACK : forall u v, t_linked' s.(t) u v -> In v back_targets)
    (T_REFL : forall u, In u back_targets -> ~ In u s.(l) -> t_linked' s.(t) u u)
    (T_TRANS : forall u v w, In u back_targets -> ~ In u s.(l) -> t_linked' tinit u v ->
      t_linked' s.(t) v w -> t_linked' s.(t) u w)
    (T_DOM_PRE : forall u set, s.(t) ! u = Some set ->
      Forall (fun '(u, n) => n = dom_pre u) set)
    (T_SORTED : forall u set, s.(t) ! u = Some set ->
      Sorted (fun '(_, n1) '(_, n2) => n1 < n2)%Z set)
    (FOLD : fold_left (f dom_pre) s.(l) s.(t) = fold_left (f dom_pre) back_targets tinit).

Inductive postcondition (t: PTree.t (list (node *Z))) : Prop :=
  Postcondition
    (T_REFL : forall u, In u back_targets -> t_linked' t u u)
    (T_TRANS : forall u v w, In u back_targets -> t_linked' tinit u v ->
      t_linked' t v w -> t_linked' t u w)
    (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)
    (FOLD : t = fold_left (f dom_pre) back_targets tinit).

Lemma transition_spec:
  forall s, invariant s ->
  match transition dom_pre s with inr s' => invariant s' | inl m => postcondition m end.

Proof.

  intros. inv H. unfold transition. destruct (l s) as [ | u m].
  - constructor; simpl; intros.
    + auto.
    + eauto.
    + eauto.
    + eauto.
    + assumption.
  - constructor; simpl; intros.

    + inv SORTED; assumption.
    + destruct (peq u0 u).
      * subst. apply Sorted_StronglySorted in SORTED.
        -- inv SORTED. rewrite Forall_forall in H5. apply H5. assumption.
        -- intros x1 x2 x3 H2 H3. rewrite H2. assumption.
      * eapply SORTED_DONE; try eassumption.
        -- intros [contra|contra]; congruence.
        -- right; assumption.
    + apply incl_cons_inv in INCL. assumption.
    + rewrite PTree.gso. eauto.
      intros contra. subst u0.
      apply Sorted_StronglySorted in SORTED.
      -- inv SORTED. rewrite Forall_forall in H3. specialize (H3 _ H). xomega.
      -- intros x1 x2 x3 H2 H3. rewrite H2. assumption.
    + unfold t_linked' in H. rewrite PTree.gsspec in H.
      destruct (peq u0 u).
      * subst u0. destruct H as (set & H1 & H2). inv H1.
        destruct (s.(t) ! u) as [set|] eqn:Ht.
        -- apply in_map_iff in H2. destruct H2 as ((v', n_v) & H2' & H2).
           simpl in H2'. subst.
           apply ZSortWithIndex.incl_merge in H2. simpl in H2.
           destruct H2 as [H2|H2].
           ++ inv H2. apply INCL. left; reflexivity.
           ++ revert H2. apply fold_invariant.
              ** intros [].
              ** intros (x, n_x) set'. intros.
                 destruct (s.(t) ! x) as [set''|] eqn:Ht'.
                 --- apply ZSortWithIndex.incl_merge in H2.
                     rewrite in_app_iff in H2.
                     destruct H2 as [H2|H2].
                     +++ eapply T_IN_BACK. eexists; split; [eassumption|].
                         apply in_map_iff.
                         eexists (_, _); split; [reflexivity|eassumption].
                     +++ auto.
                 --- auto.
        -- simpl in H2. destruct H2 as [H2|[]]. subst.
           apply INCL. left; reflexivity.
      * eauto.
    + unfold t_linked'. rewrite PTree.gsspec.
      destruct (peq u0 u).
      * subst u0.
        eexists; split; [reflexivity|].
        destruct (s.(t) ! u) as [set|] eqn:Ht.
        -- apply in_map_iff. eexists (_, _); split; [reflexivity|].
           apply ZSortWithIndex.incl_merge_2_inj.
           { intros x1 x2 N Hx1 Hx2.
             assert (N = dom_pre x1) as Ha.
             { simpl in Hx1. destruct Hx1 as [Hx1|[]].
               inv Hx1. reflexivity.
             }
             assert (N = dom_pre x2) as Hb.
             { revert Hx2.
               apply fold_invariant.
               - intros [].
               - intros (x2', n_x2') set''. intros.
                 destruct (s.(t) ! x2') eqn:Ht'.
                 + apply ZSortWithIndex.incl_merge in Hx2.
                   rewrite in_app_iff in Hx2. destruct Hx2 as [Hx2|Hx2].
                   * exploit T_DOM_PRE; try eassumption.
                     intros HForall. rewrite Forall_forall in HForall.
                      apply (HForall _ Hx2).
                   * eauto.
                + eauto.
             }
             assert (In x1 back_targets) as Hc.
             { destruct Hx1 as [Hx1|[]].
                inv Hx1. eauto.
             }
             assert (In x2 back_targets) as Hd.
             { revert Hx2.
               apply fold_invariant.
               - intros [].
               - intros (x2', n_x2') set'. intros.
                 destruct (s.(t) ! x2') as [set''|] eqn:Ht'.
                 + apply ZSortWithIndex.incl_merge in Hx2.
                   rewrite in_app_iff in Hx2. destruct Hx2 as [Hx2|Hx2].
                   * eapply T_IN_BACK.
                     eexists; split; [eassumption|].
                     apply in_map_iff.
                     eexists (_, _); split; [reflexivity|eassumption].
                   * auto.
                 + auto.
             }
             eapply dom_pre_inj; eauto. congruence.
           }
           simpl. left; reflexivity.
        -- simpl. left; reflexivity.
      * apply T_REFL; try assumption.
        intros [contra|contra]; congruence.
    + unfold t_linked' in H2. rewrite PTree.gso in H2.
      * unfold t_linked'. rewrite PTree.gsspec.
        destruct (peq u0 u).
        -- subst u0. eexists; split; [reflexivity|].
           destruct H1 as (set & H11 & H12).
           rewrite <- T_TODO in H11 by (left; reflexivity).
           rewrite H11.
           apply in_map_iff in H12. destruct H12 as ((v', n_v) & H12' & H12).
           simpl in H12'. subst.
           destruct H2 as (set' & H21 & H22).
           apply in_map_iff in H22. destruct H22 as ((w', n_w) & H22' & H22).
           simpl in H22'. subst.
           apply in_map_iff. eexists (_, _); split; [reflexivity|].
           apply ZSortWithIndex.incl_merge_2_inj.
           { intros x1 x2 N Hx1 Hx2.
             assert (N = dom_pre x1) as Ha.
             { simpl in Hx1. destruct Hx1 as [Hx1|[]].
               inv Hx1. reflexivity.
             }
             assert (N = dom_pre x2) as Hb.
             { revert Hx2.
               apply fold_invariant.
               - intros [].
               - intros (x2', n_x2') set''. intros.
                 destruct (s.(t) ! x2') eqn:Ht'.
                 + apply ZSortWithIndex.incl_merge in Hx2.
                   rewrite in_app_iff in Hx2. destruct Hx2 as [Hx2|Hx2].
                   * exploit T_DOM_PRE; try eassumption.
                     intros HForall. rewrite Forall_forall in HForall.
                      apply (HForall _ Hx2).
                   * eauto.
                + eauto.
             }
             assert (In x1 back_targets) as Hc.
             { destruct Hx1 as [Hx1|[]].
                inv Hx1. eauto.
             }
             assert (In x2 back_targets) as Hd.
             { revert Hx2.
               apply fold_invariant.
               - intros [].
               - intros (x2', n_x2') set''. intros.
                 destruct (s.(t) ! x2') as [set'''|] eqn:Ht'.
                 + apply ZSortWithIndex.incl_merge in Hx2.
                   rewrite in_app_iff in Hx2. destruct Hx2 as [Hx2|Hx2].
                   * eapply T_IN_BACK.
                     eexists; split; [eassumption|].
                     apply in_map_iff.
                     eexists (_, _); split; [reflexivity|eassumption].
                   * auto.
                 + auto.
             }
             eapply dom_pre_inj; eauto. congruence.
           }
           simpl. right.
           apply fold_becomes_true_growing_with_invariant
             with
               (P0 := fun l => forall x n_x, In (x, n_x) l ->
                        exists x' set, s.(t) ! x' = Some set /\ In (x, n_x) set).
           ++ intros ? ? [].
           ++ intros (x, n_x) set''. intros.
              destruct (s.(t) ! x) as [set'''|] eqn:Ht.
              ** apply ZSortWithIndex.incl_merge in H3.
                 rewrite in_app_iff in H3. destruct H3 as [H3|H3].
                 --- exists x, set'''.
                     split; assumption.
                 --- auto.
              ** auto.
           ++ apply Exists_exists. eexists (_, _); split; [eassumption|].
              intros set''. intros. rewrite H21.
              apply ZSortWithIndex.incl_merge_2_inj.
              { intros x1 x2 N Hx1 Hx2.
                assert (N = dom_pre x1) as Ha.
                { exploit T_DOM_PRE; try eassumption.
                  intros HForall. rewrite Forall_forall in HForall.
                  apply (HForall _ Hx1).
                }
                assert (N = dom_pre x2) as Hb.
                { exploit H1; try eassumption.
                  intros (x2' & set''' & Hx2' & Hx2'').
                  exploit T_DOM_PRE; try eassumption.
                  intros HForall. rewrite Forall_forall in HForall.
                  apply (HForall _ Hx2'').
                }
                assert (In x1 back_targets) as Hc.
                { eapply T_IN_BACK.
                  eexists; split; [eassumption|].
                  apply in_map_iff.
                  eexists (_, _); split; [reflexivity|eassumption].
                }
                assert (In x2 back_targets) as Hd.
                { exploit H1; try eassumption.
                  intros (x2' & set''' & Hx2' & Hx2'').
                  eapply T_IN_BACK.
                  eexists; split; [eassumption|].
                  apply in_map_iff.
                  eexists (_, _); split; [reflexivity|eassumption].
                }
                eapply dom_pre_inj; eauto. congruence.
              }
              rewrite in_app_iff. left; eassumption.
           ++ intros (x, n_x) set''. intros.
              destruct (s.(t) ! x) as [set'''|] eqn:Ht.
              ** apply ZSortWithIndex.incl_merge_2_inj.
                 { intros x1 x2 N Hx1 Hx2.
                   assert (N = dom_pre x1) as Ha.
                   { exploit T_DOM_PRE; try eassumption.
                     intros HForall. rewrite Forall_forall in HForall.
                     apply (HForall _ Hx1).
                   }
                   assert (N = dom_pre x2) as Hb.
                   { exploit H2; try eassumption.
                     intros (x2' & set'''' & Hx2' & Hx2'').
                     exploit T_DOM_PRE; try eassumption.
                     intros HForall. rewrite Forall_forall in HForall.
                     apply (HForall _ Hx2'').
                   }
                   assert (In x1 back_targets) as Hc.
                   { eapply T_IN_BACK.
                     eexists; split; [eassumption|].
                     apply in_map_iff.
                     eexists (_, _); split; [reflexivity|eassumption].
                   }
                   assert (In x2 back_targets) as Hd.
                   { exploit H2; try eassumption.
                     intros (x2' & set'''' & Hx2' & Hx2'').
                     eapply T_IN_BACK.
                     eexists; split; [eassumption|].
                     apply in_map_iff.
                     eexists (_, _); split; [reflexivity|eassumption].
                   }
                   eapply dom_pre_inj; eauto. congruence.
                 }
                 rewrite in_app_iff. right; assumption.
              ** assumption.
        -- eapply T_TRANS; eauto.
           intros [contra|contra]; congruence.
      * intros contra. subst.
        apply t_pre in H1.
        exploit SORTED_DONE; eauto.
        intros [contra|contra]; [subst; xomega|contradiction].
        xomega.
    + rewrite PTree.gsspec in H.
      destruct (peq u0 u); [|eauto].
      subst u0. inv H.
      destruct (s.(t) ! u) as [set|] eqn:Ht.
      * rewrite Forall_forall.
        intros (x, n_x). intros.
        apply ZSortWithIndex.incl_merge in H. simpl in H.
        destruct H as [H|H].
        -- inv H. reflexivity.
        -- revert H. apply fold_invariant.
           ++ intros [].
           ++ intros (x', n_x') set'. intros.
              destruct (s.(t) ! x') as [set''|] eqn:Heqt.
              ** apply ZSortWithIndex.incl_merge in H1.
                 rewrite in_app_iff in H1.
                 destruct H1 as [H1|H1].
                 --- exploit T_DOM_PRE; try eassumption.
                     intros HForall. rewrite Forall_forall in HForall.
                     apply (HForall _ H1).
                 --- auto.
              ** auto.
      * constructor; [reflexivity|constructor].
    + rewrite PTree.gsspec in H.
      destruct (peq u0 u); [|eauto].
      subst u0. inv H.
      destruct (s.(t) ! u) as [set|] eqn:Ht.
      * apply Sorted_LocallySorted_iff.
        apply ZSortWithIndex.Sorted_merge.
        -- constructor.
        -- apply fold_invariant.
           ++ constructor.
           ++ intros (x, n_x) set'. intros.
              destruct (s.(t) ! x) as [set''|] eqn:Ht'.
              ** apply ZSortWithIndex.Sorted_merge.
                 --- apply Sorted_LocallySorted_iff. eauto.
                 --- assumption.
              ** assumption.
      * constructor; constructor.
    + rewrite <- FOLD.
      simpl. f_equal.
Qed.

Hypothesis t_dom_pre : forall u set, tinit ! u = Some set ->
  Forall (fun '(u, n) => n = dom_pre u) set.
Hypothesis t_sorted : forall u set, tinit ! u = Some set ->
  Sorted (fun '(_, n1) '(_, n2) => n1 < n2)%Z set.
Hypothesis back_targets_sorted : Sorted (fun u v => pre u < pre v) back_targets.

Lemma initial_state_spec:
  invariant (init_state tinit back_targets).

Proof.

  unfold init_state.
  constructor; simpl; intros.
  - assumption.
  - contradiction.
  - apply incl_refl.
  - reflexivity.
  - eauto.
  - contradiction.
  - contradiction.
  - eauto.
  - eauto.
  - reflexivity.
Qed.

Termination criterion.

Definition lt_state (s1 s2: state) : Prop :=
(length s1.(l) < length s2.(l))%nat.

Lemma lt_state_wf: well_founded lt_state.

Proof.

  set (f := fun s => length s.(l)).
  change (well_founded (fun s1 s2 => (f s1) < (f s2)))%nat.
  apply well_founded_ltof.
Qed.

Lemma transition_decreases:
forall dom_tre s s', transition dom_tre s = inr _ s' -> lt_state s' s.

Proof.

  unfold transition, lt_state; intros.
  destruct (l s) as [ | u m].
  - discriminate.
  - destruct (s.(t) ! u) as [set|].
    + inv H; simpl. apply le_n.
    + inv H; simpl. apply le_n.
Qed.

End POSTORDER.

Definition postorder dom_pre t back_targets :=
  Iteration.WfIter.iterate _ _
    (transition dom_pre) lt_state lt_state_wf (transition_decreases dom_pre) (init_state t back_targets).

End Postorder.

Lemma precompute_t_from_t_up_1_back_2 :
  forall dom_pre pre t back
  (dom_pre_inj : forall u v, In u (map snd back) -> In v (map snd back) ->
    dom_pre u = dom_pre v -> u = v)
  (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)
  (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 (u_target : In u (map snd back)) v,
  clos_refl_trans _ (t_linked' t) u v ->
  t_linked' (precompute_t_from_t_up_1 dom_pre pre t back) u v.

Proof.

  intros.
  set (back_targets := PosSortWithIndex.sort pre (List.map snd back)).
  assert (postcondition dom_pre t back_targets (postorder dom_pre t back_targets)).
    unfold postorder.
    apply Iteration.WfIter.iterate_prop with (P := invariant dom_pre pre t back_targets).
    { apply transition_spec; try assumption.
      intros. eapply dom_pre_inj; try assumption.
      - eapply PosSortWithIndex.incl_sort. eassumption.
      - eapply PosSortWithIndex.incl_sort. eassumption.
    }
    { apply initial_state_spec; try assumption.
      intros. eapply PosSortWithIndex.incl_sort_2_inj; eauto.
      apply PosSortWithIndex.LocallySorted_sort.
    }
  inv H0.
  change (precompute_t_from_t_up_1 dom_pre pre t back)
    with (fold_left (f dom_pre) back_targets t).
  rewrite <- FOLD.
  apply Operators_Properties.clos_rt_rt1n_iff in H.
  induction H.
  - apply T_REFL. apply PosSortWithIndex.incl_sort_2_inj; assumption.
  - eapply T_TRANS.
    + apply PosSortWithIndex.incl_sort_2_inj; assumption.
    + eassumption.
    + apply IHclos_refl_trans_1n. eapply t_in_back; eassumption.
Qed.

Lemma precompute_t_from_t_up_1_dom_pre :
  forall dom_pre pre t back
  (dom_pre_inj : forall u v, In u (map snd back) -> In v (map snd back) ->
    dom_pre u = dom_pre v -> u = v)
  (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)
  (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 set,
  (precompute_t_from_t_up_1 dom_pre pre t back) ! u = Some set ->
  Forall (fun '(u, n) => n = dom_pre u) set.

Proof.

Lemma precompute_t_from_t_up_1_sorted :
  forall dom_pre pre t back
  (dom_pre_inj : forall u v, In u (map snd back) -> In v (map snd back) ->
    dom_pre u = dom_pre v -> u = v)
  (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)
  (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 set,
  (precompute_t_from_t_up_1 dom_pre pre t back) ! u = Some set ->
  Sorted (fun '(_, n1) '(_, n2) => n1 < n2)%Z set.

Proof.

End Precompute_t_from_t_up_back_targets.

Lemma precompute_t_from_t_up_1_dom_pre :
  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)
  u set,
  (precompute_t_from_t_up_1 dom_pre pre t back) ! u = Some set ->
  Forall (fun '(u, n) => n = dom_pre u) set.

Proof.

  intros. revert u set H.
  unfold precompute_t_from_t_up_1.
  apply fold_invariant; intros.
  - eauto.
  - rewrite PTree.gsspec in H1.
    destruct (peq u x); [|eauto].
    inv H1.
    destruct (t0 ! x) as [set|]; [|auto].
    rewrite Forall_forall.
    intros (x', n_x'). intros.
    apply ZSortWithIndex.incl_merge in H1. simpl in H1.
    destruct H1 as [H1|H1].
    + inv H1; reflexivity.
    + revert H1. apply fold_invariant.
      * intros [].
      * intros (x'', n_x'') set'. intros.
        destruct (t0 ! x'') as [set''|] eqn:Ht; [|auto].
        apply ZSortWithIndex.incl_merge in H3. rewrite in_app_iff in H3.
        destruct H3 as [H3|H3]; [|auto].
        exploit H0; try eassumption.
        intros HForall. rewrite Forall_forall in HForall.
        apply (HForall _ H3).
Qed.

Lemma precompute_t_from_t_up_1_sorted :
  forall dom_pre pre t back
  (t_sorted : forall u set, t ! u = Some set ->
    Sorted (fun '(_, n1) '(_, n2) => n1 < n2)%Z set)
  u set,
  (precompute_t_from_t_up_1 dom_pre pre t back) ! u = Some set ->
  Sorted (fun '(_, n1) '(_, n2) => n1 < n2)%Z set.

Proof.

  intros. revert u set H.
  unfold precompute_t_from_t_up_1.
  apply fold_invariant; intros.
  - eauto.
  - rewrite PTree.gsspec in H1.
    destruct (peq u x); [|eauto].
    inv H1.
    destruct (t0 ! x) as [set|]; [|auto].
    apply Sorted_LocallySorted_iff.
    apply ZSortWithIndex.Sorted_merge.
    constructor.
    apply fold_invariant.
    + constructor.
    + intros (x', n_x') set'. intros.
      destruct (t0 ! x') as [set''|] eqn:Ht; [|auto].
      apply ZSortWithIndex.Sorted_merge.
      apply Sorted_LocallySorted_iff. eauto.
      assumption.
Qed.

Theorem precompute_t_from_t_up_1_back :
  forall dom_pre pre t back
  (dom_pre_inj : forall u v, In u (map snd back) -> In v (map snd back) ->
    dom_pre u = dom_pre v -> u = v)
  (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)
  (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 (u_target : In u (map snd back)) v,
  t_linked' (precompute_t_from_t_up_1 dom_pre pre t back) u v
  <-> clos_refl_trans _ (t_linked' t) u v.

Proof.

  split; intros.
  - apply precompute_t_from_t_up_1_back_1 in H; assumption.
  - apply Precompute_t_from_t_up_back_targets.precompute_t_from_t_up_1_back_2; assumption.
Qed.

Lemma precompute_t_from_t_up_1_black :
  forall dom_pre pre t back u,
  t ! u <> None ->
  (precompute_t_from_t_up_1 dom_pre pre t back) ! u <> None.

Proof.

  intros. unfold precompute_t_from_t_up_1.
  apply fold_invariant.
  - assumption.
  - intros. rewrite PTree.gsspec.
    destruct (peq u x).
    + discriminate.
    + assumption.
Qed.

Lemma precompute_t_from_t_up_1_black_2 :
  forall dom_pre pre t back u,
  (precompute_t_from_t_up_1 dom_pre pre t back) ! u <> None ->
  t ! u = None ->
  In u (map snd back).

Proof.

  intros. revert H. unfold precompute_t_from_t_up_1.
  apply fold_invariant.
  - contradiction.
  - intros. rewrite PTree.gsspec in H2. destruct (peq u x).
    + subst. apply PosSortWithIndex.incl_sort in H. assumption.
    + auto.
Qed.

Lemma precompute_t_from_t_up_2_correct_1 :
  forall dom_pre t u v,
  t_linked (precompute_t_from_t_up_2 dom_pre t) u v ->
  clos_refl_trans _ (t_linked' t) u v.

Proof.

  intros. unfold precompute_t_from_t_up_2 in H.
  destruct H as (set' & H1 & H2).
  rewrite PTree.gmap in H1. unfold option_map in H1.
  destruct (t ! u) as [set|] eqn:Ht; [|discriminate].
  inv H1.
  apply in_map_iff in H2. destruct H2 as ((v', n_v) & H2' & H2).
  simpl in H2'. subst.
  apply ZSortWithIndex.incl_merge in H2. simpl in H2.
  destruct H2 as [H2|H2].
  - inv H2. apply rt_refl.
  - revert H2. apply fold_invariant.
    + intros [].
    + intros (x, n_x) set'. intros.
      destruct (t ! x) as [set''|] eqn:Ht'.
      * apply ZSortWithIndex.incl_merge in H2. rewrite in_app_iff in H2.
        destruct H2 as [H2|H2].
        -- eapply rt_trans.
           ++ apply rt_step. eexists; split; [eassumption|].
              apply in_map_iff.
              eexists (_, _); split; [reflexivity|eassumption].
           ++ apply rt_step. eexists; split; [eassumption|].
              apply in_map_iff.
              eexists (_, _); split; [reflexivity|eassumption].
        -- auto.
      * auto.
Qed.

Lemma precompute_t_from_t_up_2_refl :
  forall dom_pre (t : PTree.t (list (node * Z)))
  (dom_pre_inj : forall u v,
    t ! u <> None \/ (exists u', t_linked' t u' u) ->
    t ! v <> None \/ (exists v', t_linked' t v' v) ->
    dom_pre u = dom_pre v -> u = v)
  (t_dom_pre : forall u set, t ! u = Some set ->
    Forall (fun '(u, n) => n = dom_pre u) set)
  u,
  t ! u <> None ->
  t_linked (precompute_t_from_t_up_2 dom_pre t) u u.

Proof.

  intros.
  unfold t_linked. unfold precompute_t_from_t_up_2.
  rewrite PTree.gmap. unfold option_map.
  destruct (t ! u) as [set|] eqn:Ht; [|contradiction].
  eexists; split; [reflexivity|].
  apply in_map_iff. eexists (_, _); split; [reflexivity|].
  apply ZSortWithIndex.incl_merge_2_inj.
  { intros x1 x2 N Hx1 Hx2.
    assert (N = dom_pre x1) as Ha.
    { simpl in Hx1. destruct Hx1 as [Hx1|[]].
      inv Hx1. reflexivity.
    }
    assert (N = dom_pre x2) as Hb.
    { revert Hx2.
      apply fold_invariant.
      - intros [].
      - intros (x2', n_x2') set'. intros.
        destruct (t ! x2') eqn:Ht'.
        + apply ZSortWithIndex.incl_merge in Hx2.
          rewrite in_app_iff in Hx2. destruct Hx2 as [Hx2|Hx2].
          * exploit t_dom_pre; try eassumption.
            intros HForall. rewrite Forall_forall in HForall.
            apply (HForall _ Hx2).
          * eauto.
       + eauto.
    }
    assert (t ! x1 <> None) as Hc.
    { destruct Hx1 as [Hx1|[]].
       inv Hx1. congruence.
    }
    assert (exists x2', t_linked' t x2' x2) as Hd.
    { revert Hx2.
      apply fold_invariant.
      - intros [].
      - intros (x2', n_x2') set'. intros.
        destruct (t ! x2') as [set''|] eqn:Ht'.
        + apply ZSortWithIndex.incl_merge in Hx2.
          rewrite in_app_iff in Hx2. destruct Hx2 as [Hx2|Hx2].
          * exists x2'.
            eexists; split; [eassumption|].
            apply in_map_iff.
            eexists (_, _); split; [reflexivity|eassumption].
          * auto.
        + auto.
    }
    eapply dom_pre_inj; eauto. congruence.
  }
  simpl. left; reflexivity.
Qed.

Lemma precompute_t_from_t_up_2_trans :
  forall dom_pre (t : PTree.t (list (node * Z))) back_targets
  (dom_pre_inj : forall u v,
    t ! u <> None \/ In u back_targets ->
    t ! v <> None \/ In v back_targets ->
    dom_pre u = dom_pre v -> u = v)
  (t_dom_pre : forall u set, t ! u = Some set ->
    Forall (fun '(u, n) => n = dom_pre u) set)
  (t_in_back : forall u v, t_linked' t u v -> In v back_targets)
  (t_back_targets_refl : forall u, In u back_targets -> t_linked' t u u)
  (t_back_targets_trans : forall u v w, In u back_targets ->
    t_linked' t u v -> t_linked' t v w ->
    t_linked' t u w)
  u v w,
  t_linked' t u v ->
  t_linked (precompute_t_from_t_up_2 dom_pre t) v w ->
  t_linked (precompute_t_from_t_up_2 dom_pre t) u w.

Proof.

  intros. unfold t_linked, precompute_t_from_t_up_2 in H0 |- *.
  rewrite PTree.gmap in H0 |- *.
  unfold option_map in H0 |- *.
  destruct H as (set & H1 & H2).
  apply in_map_iff in H2. destruct H2 as ((v', n_v) & H2' & H2).
  simpl in H2'. subst.
  rewrite H1.
  eexists; split; [reflexivity|].
  destruct H0 as (set'' & H01 & H02).
  destruct (t ! v) as [set'|] eqn:Ht; [|discriminate]. inv H01.
  apply in_map_iff in H02. destruct H02 as ((w', n_w) & H02' & H02).
  simpl in H02'. subst.
  apply in_map_iff. exists (w, n_w); split; [reflexivity|].
  apply ZSortWithIndex.incl_merge_2_inj.
  { intros x1 x2 N Hx1 Hx2.
    assert (N = dom_pre x1) as Ha.
    { simpl in Hx1. destruct Hx1 as [Hx1|[]].
      inv Hx1. reflexivity.
    }
    assert (N = dom_pre x2) as Hb.
    { revert Hx2.
      apply fold_invariant.
      - intros [].
      - intros (x2', n_x2') set''. intros.
        destruct (t ! x2') eqn:Ht'.
        + apply ZSortWithIndex.incl_merge in Hx2.
          rewrite in_app_iff in Hx2. destruct Hx2 as [Hx2|Hx2].
          * exploit t_dom_pre; try eassumption.
            intros HForall. rewrite Forall_forall in HForall.
            apply (HForall _ Hx2).
          * eauto.
       + eauto.
    }
    assert (t ! x1 <> None) as Hc.
    { destruct Hx1 as [Hx1|[]].
       inv Hx1. congruence.
    }
    assert (In x2 back_targets) as Hd.
    { revert Hx2.
      apply fold_invariant.
      - intros [].
      - intros (x2', n_x2') set''. intros.
        destruct (t ! x2') as [set'''|] eqn:Ht'.
        + apply ZSortWithIndex.incl_merge in Hx2.
          rewrite in_app_iff in Hx2. destruct Hx2 as [Hx2|Hx2].
          * apply (t_in_back x2' x2).
            eexists; split; [eassumption|].
            apply in_map_iff.
            eexists (_, _); split; [reflexivity|eassumption].
          * auto.
        + auto.
    }
    eapply dom_pre_inj; eauto. congruence.
  }
  simpl. right.
  apply fold_becomes_true_growing_with_invariant
    with
     (P0 := fun l => forall x n_x, In (x, n_x) l ->
              exists x' set, t ! x' = Some set /\ In (x, n_x) set).
  - intros ? ? [].
  - intros (x, n_x) set''. intros.
    destruct (t ! x) as [set'''|] eqn:Ht'.
    ** apply ZSortWithIndex.incl_merge in H3.
       rewrite in_app_iff in H3. destruct H3 as [H3|H3].
       --- exists x, set'''.
           split; assumption.
       --- auto.
    ** auto.
  - apply Exists_exists.
    eexists (_, _); split; [eassumption|].
    intros set''. intros. rewrite Ht.
    apply ZSortWithIndex.incl_merge_2_inj.
    { intros x1 x2 N Hx1 Hx2.
      assert (N = dom_pre x1) as Ha.
      { exploit t_dom_pre; try eassumption.
        intros HForall. rewrite Forall_forall in HForall.
        apply (HForall _ Hx1).
      }
      assert (N = dom_pre x2) as Hb.
      { exploit H; try eassumption.
        intros (x2' & set''' & Hx2' & Hx2'').
        exploit t_dom_pre; try eassumption.
        intros HForall. rewrite Forall_forall in HForall.
        apply (HForall _ Hx2'').
      }
      assert (In x1 back_targets) as Hc.
      { eapply t_in_back.
        eexists; split; [eassumption|].
        apply in_map_iff.
        eexists (_, _); split; [reflexivity|eassumption].
      }
      assert (In x2 back_targets) as Hd.
      { exploit H; try eassumption.
        intros (x2' & set''' & Hx2' & Hx2'').
        eapply t_in_back.
        eexists; split; [eassumption|].
        apply in_map_iff.
        eexists (_, _); split; [reflexivity|eassumption].
      }
      eapply dom_pre_inj; eauto. congruence.
    }
    rewrite in_app_iff. left.
    apply ZSortWithIndex.incl_merge in H02. simpl in H02.
    destruct H02 as [H02|H02].
    + inv H02. exploit (t_back_targets_refl w).
      apply (t_in_back u w). eexists; split; [eassumption|].
      apply in_map_iff. eexists (_, _); split; [reflexivity|eassumption].
      intros. destruct H0 as (set''' & H01 & H02).
      apply in_map_iff in H02. destruct H02 as ((w', n_w') & H02' & H02).
      simpl in H02'. subst.
      rewrite H01 in Ht. inv Ht.
      exploit t_dom_pre; eauto. intros HForall.
      rewrite Forall_forall in HForall. rewrite <- (HForall _ H02).
      assumption.
    + revert H02. apply fold_invariant.
      * intros [].
      * intros (x, n_x) set'''. intros.
        destruct (t ! x) as [set''''|] eqn:Ht'.
        -- apply ZSortWithIndex.incl_merge in H02. rewrite in_app_iff in H02.
           destruct H02 as [H02|H02].
           ++ exploit (t_back_targets_trans v x w).
              apply (t_in_back u v). eexists; split; [eassumption|].
              apply in_map_iff. eexists (_, _); split; [reflexivity|eassumption].
              eexists; split; [eassumption|].
              apply in_map_iff. eexists (_, _); split; [reflexivity|eassumption].
              eexists; split; [eassumption|].
              apply in_map_iff. eexists (_, _); split; [reflexivity|eassumption].
              intros. destruct H4 as (set''''' & H31 & H32).
              apply in_map_iff in H32.
              destruct H32 as ((w', n_w') & H32' & H32).
              simpl in H32'. subst.
              rewrite H31 in Ht. inv Ht.
              exploit t_dom_pre; eauto. intros HForall.
              rewrite Forall_forall in HForall.
              rewrite (HForall _ H32) in H32.
              exploit t_dom_pre. apply Ht'. intros HForall'.
              rewrite Forall_forall in HForall'.
              rewrite (HForall' _ H02).
              assumption.
           ++ auto.
        -- auto.
  - intros (x, n_x) set''. intros.
    destruct (t ! x) as [set'''|] eqn:Ht'; [|assumption].
    apply ZSortWithIndex.incl_merge_2_inj.
    { intros x1 x2 N Hx1 Hx2.
      assert (N = dom_pre x1) as Ha.
      { exploit t_dom_pre; try eassumption.
        intros HForall. rewrite Forall_forall in HForall.
        apply (HForall _ Hx1).
      }
      assert (N = dom_pre x2) as Hb.
      { exploit H0; try eassumption.
        intros (x2' & set'''' & Hx2' & Hx2'').
        exploit t_dom_pre; try eassumption.
        intros HForall. rewrite Forall_forall in HForall.
        apply (HForall _ Hx2'').
      }
      assert (In x1 back_targets) as Hc.
      { eapply t_in_back.
        eexists; split; [eassumption|].
        apply in_map_iff.
        eexists (_, _); split; [reflexivity|eassumption].
      }
      assert (In x2 back_targets) as Hd.
      { exploit H0; try eassumption.
        intros (x2' & set'''' & Hx2' & Hx2'').
        eapply t_in_back.
        eexists; split; [eassumption|].
        apply in_map_iff.
        eexists (_, _); split; [reflexivity|eassumption].
      }
      eapply dom_pre_inj; eauto. congruence.
    }
    rewrite in_app_iff. right; assumption.
Qed.

Lemma precompute_t_from_t_up_2_correct_2 :
  forall dom_pre (t : PTree.t (list (node * Z))) (back : list (node * node))
  (dom_pre_inj : forall u v,
    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 set, t ! u = Some set ->
    Forall (fun '(u, n) => n = dom_pre u) set)
  (t_in_back : forall u v, t_linked' t u v -> In v (map snd back))
  (t_back_targets_refl : forall u, In u (map snd back) -> t_linked' t u u)
  (t_back_targets_trans : forall u v w, In u (map snd back) ->
    t_linked' t u v -> t_linked' t v w ->
    t_linked' t u w)
  u (u_in_t : t ! u <> None) v,
  clos_refl_trans _ (t_linked' t) u v ->
  t_linked (precompute_t_from_t_up_2 dom_pre t) u v.

Proof.

  intros.
  apply Operators_Properties.clos_rt_rt1n_iff in H.
  induction H.
  - apply precompute_t_from_t_up_2_refl; auto.
    intros. eapply dom_pre_inj; try assumption.
    destruct H as [H|[u' H]]. left; assumption. right; eauto.
    destruct H0 as [H0|[v' H0]]. left; assumption. right; eauto.
  - eapply precompute_t_from_t_up_2_trans; eauto.
    apply IHclos_refl_trans_1n.
    exploit t_back_targets_refl; eauto.
    intros. destruct H1 as (set & H1 & _). congruence.
Qed.

Theorem precompute_t_from_t_up_2_correct :
  forall dom_pre (t : PTree.t (list (node * Z))) (back : list (node * node))
  (dom_pre_inj : forall u v,
    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 set, t ! u = Some set ->
    Forall (fun '(u, n) => n = dom_pre u) set)
  (t_in_back : forall u v, t_linked' t u v -> In v (map snd back))
  (t_back_targets_refl : forall u, In u (map snd back) -> t_linked' t u u)
  (t_back_targets_trans : forall u v w, In u (map snd back) ->
    t_linked' t u v -> t_linked' t v w ->
    t_linked' t u w)
  u (u_in_t : t ! u <> None) v,
  t_linked (precompute_t_from_t_up_2 dom_pre t) u v <->
  clos_refl_trans _ (t_linked' t) u v.

Proof.

  split; intros.
  - apply precompute_t_from_t_up_2_correct_1 in H; assumption.
  - eapply precompute_t_from_t_up_2_correct_2; eassumption.
Qed.

Lemma precompute_t_from_t_up_2_black :
  forall dom_pre t u,
  (precompute_t_from_t_up_2 dom_pre t) ! u <> None
  <-> t ! u <> None.

Proof.

  intros. unfold precompute_t_from_t_up_2.
  rewrite PTree.gmap. unfold option_map.
  destruct (t ! u) as [set|].
  - split; discriminate.
  - split; contradiction.
Qed.

Lemma precompute_t_from_t_up_2_sorted :
  forall dom_pre (t : PTree.t (list (node * Z)))
  (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_2 dom_pre t) ! u = Some set ->
  Sorted (fun u v => dom_pre u < dom_pre v)%Z set.

Proof.

  intros. unfold precompute_t_from_t_up_2 in H.
  rewrite PTree.gmap in H. unfold option_map in H.
  destruct (t ! u) as [set'|]; [|discriminate].
  inv H.
  set (set'' := ZSortWithIndex.merge _ _).
  assert (Sorted (fun '(_, n1) '(_, n2) => n1 < n2)%Z set'') as Ha.
  { apply Sorted_LocallySorted_iff.
    apply ZSortWithIndex.Sorted_merge.
    - constructor.
    - apply fold_invariant.
      + constructor.
      + intros (x, n_x) set'''. intros.
        destruct (t ! x) as [set''''|] eqn:Ht.
        * apply ZSortWithIndex.Sorted_merge.
          -- apply Sorted_LocallySorted_iff. eauto.
          -- assumption.
        * assumption.
  }
  assert (Forall (fun '(u, n) => n = dom_pre u) set'') as Hb.
  { unfold set''. rewrite Forall_forall. intros (x, n_x). intros.
    apply ZSortWithIndex.incl_merge in H.
    simpl in H. destruct H as [H|H].
    - inv H. reflexivity.
    - revert H. apply fold_invariant.
      + intros [].
      + intros (x', n_x') set'''. intros.
        destruct (t ! x') as [set''''|] eqn:Ht.
        * apply ZSortWithIndex.incl_merge in H1. rewrite in_app_iff in H1.
          destruct H1 as [H1|H1].
          -- exploit t_dom_pre; try eassumption.
             intros HForall. rewrite Forall_forall in HForall.
             apply (HForall _ H1).
          -- auto.
        * auto.
  }
  generalize dependent set''.
  induction set'' as [|(x, n_x) set'']; intros.
  - constructor.
  - simpl in Ha. inv Ha.
    simpl in Hb. inv Hb.
    simpl. constructor.
    + auto.
    + destruct set'' as [|(x', n_x') set''].
      * constructor.
      * simpl in H2. inv H2. simpl in H4. inv H4.
        simpl. constructor. assumption.
Qed.