Module SSAfastliveprecomputeRTproof

Require Import SetoidList.

Require Import Coqlib.
Require Import Maps.
Require Import Iteration.

Require Import SSAfastliveutils.
Require Import SSAfastliveprecomputeRT.

Local Open Scope positive_scope.

Module Import Definitions.

Inductive reachable (g: graph) (root: positive) : positive -> Prop :=
  | reachable_root:
      reachable g root root
  | reachable_succ: forall x succs y,
      reachable g root x -> g!x = Some succs -> In y succs ->
      reachable g root y.

Lemma reachable_trans : forall g u1 u2 u3,
  reachable g u1 u2 ->
  reachable g u2 u3 ->
  reachable g u1 u3.

Inductive reduced_reachable (g: graph) (back : list (positive * positive))
  (root: positive) : positive -> Prop :=
  | reduced_reachable_root:
      reduced_reachable g back root root
  | reduced_reachable_succ: forall x succs y,
      reduced_reachable g back root x -> g!x = Some succs -> In y succs ->
      ~ In (x, y) back ->
      reduced_reachable g back root y.

Lemma reduced_reachable_trans : forall g back u1 u2 u3,
  reduced_reachable g back u1 u2 ->
  reduced_reachable g back u2 u3 ->
  reduced_reachable g back u1 u3.

Lemma reduced_reachable_pred : forall g back u v,
  reduced_reachable g back u v <->
  u = v \/ exists succs w,
  g ! u = Some succs /\ In w succs /\ ~ In (u, w) back /\ reduced_reachable g back w v.

Lemma reduced_reachable_is_reachable : forall g back u v,
  reduced_reachable g back u v ->
  reachable g u v.

Inductive reduced_reachable_bis (g: graph) (back : list (node * node))
  : positive -> positive -> Prop :=
  | reduced_reachable_bis_root:
      forall root, reduced_reachable_bis g back root root
  | reduced_reachable_bis_pred: forall root succs x y,
      g ! root = Some succs -> In x succs -> ~ In (root, x) back ->
      reduced_reachable_bis g back x y ->
      reduced_reachable_bis g back root y.

Lemma reduced_reachable_bis_succ :
  forall g back u v,
  reduced_reachable_bis g back u v <->
  u = v \/ exists w succs,
  reduced_reachable_bis g back u w /\ g!w = Some succs /\ In v succs /\
  ~ In (w, v) back.

Lemma reduced_reachable_equiv : forall g back u v,
  reduced_reachable g back u v <-> reduced_reachable_bis g back u v.

Definition is_in_t_up g back u v :=
  ~ reduced_reachable g back u v
  /\ exists s,
     In (s, v) back
     /\ reduced_reachable g back u s.

Definition directly_included r u v :=
  exists n1 n2 m1 m2,
  r ! u = Some (n1, n2) /\ r ! v = Some (m1, m2) /\
  is_included (m1, m2) (n1, n2).

Lemma directly_included_refl : forall r u,
  r ! u <> None ->
  directly_included r u u.

Lemma directly_included_trans : forall r u v w,
  directly_included r u v ->
  directly_included r v w ->
  directly_included r u w.

Lemma directly_included_dec : forall r u v,
  directly_included r u v \/ ~ directly_included r u v.

Definition cross_included r c u v :=
  exists set w, c ! u = Some set /\ set ! w = Some tt /\ directly_included r w v.

Lemma can_reach_spec : forall r c u v
  (r_defined : r ! u <> None),
  can_reach r c u v = true <-> cross_included r c u v.

End Definitions.


Section POSTORDER.

Variable ginit: graph.
Variable root: node.

Inductive invariant (s: state) : Prop :=
  Invariant
    (SUB: forall x y, s.(gr)!x = Some y -> ginit!x = Some y)
    (ROOT: s.(gr)!root = None)
    (BELOW1 : forall x n l post, In (x, n, l, post) s.(wrk) ->
              Plt n s.(next))
    (BELOW2: forall u n1 n2, s.(r)!u = Some (n1, n2) -> Ple n1 n2 /\
             Plt n2 s.(next))
    (BELOW3 : forall u n l post, In (u, n, l, post) s.(wrk) ->
              forall v m, s.(r) ! v <> Some (n, m))
    (BELOW4 : NoDupA (fun '(_, n1, _, _) '(_, n2, _, _) => n1 = n2) s.(wrk))
    (INJ: forall u v m n1 n2, s.(r)!u = Some (m, n1) ->
          s.(r)!v = Some (m, n2) -> u = v)
    (REM: forall u l, s.(gr)!u = Some l -> s.(r)!u = None)
    (COLOR: forall u succs n1 n2 v,
            ginit!u = Some succs -> s.(r)!u = Some (n1, n2) ->
            In v succs -> s.(gr)!v = None)
    (WKLIST: forall u n l post, In (u, n, l, post) s.(wrk) ->
             s.(gr)!u = None /\
             exists l', ginit!u = Some l'
                    /\ (forall v, In v l' -> ~In v l -> s.(gr)!v = None)
                    /\ incl l l')
    (GREY: forall u, ginit!u <> None -> s.(gr)!u = None -> s.(r)!u = None ->
           exists n l post, In (u,n,l, post) s.(wrk)).

Inductive postcondition
  (acc : PTree.t (positive * positive)
       * PTree.t (PTree.t unit)
       * PTree.t (list (node * Z))
       * list (node * node))
  : Prop :=
  Postcondition
    (INJ: let '(r, c, t, back) := acc in forall u v m n1 n2, r!u = Some (m, n1) ->
          r!v = Some (m, n2) -> u = v)
    (ROOT: let '(r, c, t, back) := acc in ginit!root <> None -> r!root <> None)
    (SUCCS: let '(r, c, t, back) := acc in
       forall x succs y, ginit!x = Some succs -> r!x <> None ->
       In y succs -> ginit!y <> None -> r!y <> None)
    (BELOW : let '(r, c, t, back) := acc in
      forall u n1 n2, r ! u = Some (n1, n2) -> Ple n1 n2).

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

Lemma initial_state_spec:
  invariant (init_state ginit root).

Inductive black_reduced_reachable_bis (g: graph)
  (r:PTree.t (positive * positive)) (back : list (node * node))
  : node -> node -> Prop :=
  | black_reduced_reachable_bis_root:
      forall root, black_reduced_reachable_bis g r back root root
  | black_reduced_reachable_bis_pred: forall root succs x y,
      g ! root = Some succs -> In x succs -> r ! x <> None -> ~ In (root, x) back ->
      black_reduced_reachable_bis g r back x y ->
      black_reduced_reachable_bis g r back root y.

Lemma black_reduced_reachable_bis_succ :
  forall g r back u v,
  black_reduced_reachable_bis g r back u v <->
  u = v \/ exists w succs,
  black_reduced_reachable_bis g r back u w /\ g!w = Some succs /\ In v succs /\
  r ! v <> None /\ ~ In (w, v) back.

Lemma black_reduced_reachable_bis_is_reduced_reachable : forall g r back u v,
  black_reduced_reachable_bis g r back u v ->
  reduced_reachable g back u v.

Lemma black_reduced_reachable_bis_monotone : forall g r back u v w n1 n2,
  black_reduced_reachable_bis g r back u v ->
  black_reduced_reachable_bis g (PTree.set w (n1, n2) r) back u v.

Lemma black_reduced_reachable_bis_back : forall g r back u v x y,
  black_reduced_reachable_bis g r back u v ->
  r ! y = None ->
  black_reduced_reachable_bis g r ((x, y) :: back) u v.

Inductive invariant4 (s:state) : Prop :=
  Invariant4
    (WRK_NO_DUP : NoDupA (fun '(u, _, _, _) '(v, _, _, _) => u = v) s.(wrk))
    (WRK_NOT_BLACK : forall u n l post, In (u, n, l, post) s.(wrk) ->
      s.(r) ! u = None)
    (WRK_DONE : forall u n l s_c s_t, In (u, n, l, (s_c, s_t)) s.(wrk) ->
      exists l', ginit!u = Some l' /\
      (forall v, In v l' -> ~In v l ->
      s.(r) ! v <> None \/ In (u, v) s.(back)))
    (CLASSIFY_BLACK : forall u succs v, ginit ! u = Some succs ->
      s.(r)!u <> None -> In v succs ->
      In (u, v) s.(back)
      \/ (exists set, s.(c) ! u = Some set /\ set ! v = Some tt)
      \/ directly_included s.(r) u v)
    (CLASSIFY_GRAY : forall u n l s_c s_t, In (u, n, l, (s_c, s_t)) s.(wrk) ->
      exists l', ginit!u = Some l' /\
      (forall v, In v l' -> ~In v l ->
      In (u, v) s.(back)
      \/ (s_c ! v = Some tt)
      \/ exists n1 n2, s.(r) ! v = Some (n1, n2) /\ n <= n1))

    (CROSS_TARGETS_BLACK_GRAY : forall u n l s_c s_t w, In (u, n, l, (s_c, s_t)) s.(wrk) ->
      s_c ! w = Some tt -> s.(r) ! w <> None)
    (CROSS_TARGETS_BLACK_BLACK : forall u set v, s.(c) ! u = Some set -> set ! v = Some tt ->
      s.(r) ! v <> None)
    (CROSS_UPWARDS_GRAY : forall u n l s_c s_t, In (u, n, l, (s_c, s_t)) s.(wrk) ->
      exists l', ginit!u = Some l' /\
      (forall v set w, In v l' -> ~In v l -> ~ In (u, v) s.(back) ->
       s.(c) ! v = Some set -> set ! w = Some tt -> s_c ! w = Some tt))
    (CROSS_UPWARDS_BLACK : forall u succs v set w, ginit ! u = Some succs ->
      s.(r) ! u <> None ->
      In v succs -> ~ In (u, v) s.(back) -> s.(c) ! v = Some set -> set ! w = Some tt ->
      ~ directly_included s.(r) u w -> exists set', s.(c) ! u = Some set' /\ set' ! w = Some tt)

    (CROSS_REFL : forall u, s.(r) ! u <> None -> exists set, s.(c) ! u = Some set /\ set ! u = Some tt).

Inductive postcondition4
  (acc : PTree.t (positive * positive)
       * PTree.t (PTree.t unit)
       * PTree.t (list (node * Z))
       * list (node * node))
  : Prop :=
  Postcondition4
    (CLASSIFY: let '(r, c, t, back) := acc in
      forall u succs v, ginit ! u = Some succs -> r ! u <> None ->
      In v succs ->
      In (u, v) back \/
      (exists set, c ! u = Some set /\ set ! v = Some tt) \/
      directly_included r u v)
    (CROSS_UPWARDS: let '(r, c, t, back) := acc in
      forall u succs v set w, ginit ! u = Some succs -> r ! u <> None ->
      In v succs -> ~ In (u, v) back -> c ! v = Some set -> set ! w = Some tt ->
      ~ directly_included r u w -> exists set', c ! u = Some set' /\ set' ! w = Some tt)
    (CROSS_TARGETS_BLACK : let '(r, c, t, back) := acc in
      forall u set v, c ! u = Some set -> set ! v = Some tt ->
      r ! v <> None)
    (CROSS_REFL : let '(r, c, t, back) := acc in
      forall u, r ! u <> None -> exists set, c ! u = Some set /\ set ! u = Some tt).

Lemma transition_spec4:
  forall dom_pre s (INVARIANT : invariant s),
  invariant4 s ->
  match transition dom_pre s with inr s' => invariant4 s' | inl m => postcondition4 m end.

Lemma initial_state_spec4:
  invariant4 (init_state ginit root).

Inductive invariant2 (s:state) : Prop :=
  Invariant2
    (REACHABLE_GRAY_GRAY : Sorted (fun '(u, _, _, _) '(v, _, _, _) => exists succs,
      ginit ! v = Some succs /\ In u succs /\ ~ In (v, u) s.(back)) s.(wrk))
    (REACHABLE_GRAY_BLACK: Sorted (fun '(_, n, _, _) '(u, m, _, _) =>
      forall v n1 n2, s.(r) ! v = Some (n1, n2) -> m <= n1 < n ->
      black_reduced_reachable_bis ginit s.(r) s.(back) u v) s.(wrk))
    (REACHABLE_GRAY_BLACK_LAST: forall u n l post v n1 n2 wrk',
      s.(wrk) = (u, n, l, post) :: wrk' ->
      s.(r) ! v = Some (n1, n2) -> (n <= n1)%positive ->
      black_reduced_reachable_bis ginit s.(r) s.(back) u v)
    (REACHABLE: forall u v n1 n2 m1 m2, s.(r) ! u = Some (n1, n2) ->
      s.(r) ! v = Some (m1, m2) -> is_included (m1, m2) (n1, n2) ->
      black_reduced_reachable_bis ginit s.(r) s.(back) u v)
    (PREORDER_GRAY_GRAY :
      Sorted (fun '(_, n, _, _) '(_, m, _, _) => (m < n)%positive) s.(wrk))
    (PREORDER_GRAY_BLACK : forall u n l post v n1 n2, In (u, n, l, post) s.(wrk) ->
      s.(r) ! v = Some (n1, n2) -> (n < n1 \/ n2 < n)%positive)
    (CASES:
      forall u v n1 n2 m1 m2, s.(r) ! u = Some (n1, n2) ->
      s.(r) ! v = Some (m1, m2) ->
      m2 < n1 \/ n2 < m1
      \/ is_included (m1, m2) (n1, n2) \/ is_included (n1, n2) (m1, m2))

    (BACK_NOT_WHITE : forall u v, In (u, v) s.(back) ->
      s.(gr) ! u = None /\ s.(gr) ! v = None).

Inductive postcondition2
  (acc : PTree.t (positive * positive)
       * PTree.t (PTree.t unit)
       * PTree.t (list (node * Z))
       * list (node * node))
  : Prop :=
  Postcondition2
    (REACHABLE: let '(r, c, t, back) := acc in
      forall u v n1 n2 m1 m2, r ! u = Some (n1, n2) ->
      r ! v = Some (m1, m2) -> is_included (m1, m2) (n1, n2) ->
      reduced_reachable ginit back u v)
    (CASES: let '(r, c, t, back) := acc 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)) .

Lemma HdRel_impl : forall {A} (R1 R2 : A -> A -> Prop) a (l : list A)
  (R_impl : forall y, In y l -> R1 a y -> R2 a y) (l_Sorted : HdRel R1 a l),
  HdRel R2 a l.

Lemma Sorted_impl : forall {A} (R1 R2 : A -> A -> Prop) (l : list A)
  (R_impl : forall x y, In x l -> In y l -> R1 x y -> R2 x y) (l_Sorted : Sorted R1 l),
  Sorted R2 l.

Lemma Forall_impl_in : forall {A} (P Q:A->Prop) l,
  (forall a : A, In a l -> P a -> Q a) -> Forall P l -> Forall Q l.

Lemma StronglySorted_impl : forall {A} (R1 R2 : A -> A -> Prop) (l : list A)
  (R_impl : forall x y, In x l -> In y l -> R1 x y -> R2 x y) (l_Sorted : StronglySorted R1 l),
  StronglySorted R2 l.

Lemma Sorted_proj : forall {A B} (f : A -> B) (R : A -> A -> Prop) (l1 l2 : list A),
  (forall a1 a2 a3 a4, f a1 = f a2 -> f a3 = f a4 -> R a1 a3 -> R a2 a4) ->
  eqlistA (fun x y => f x = f y) l1 l2 ->
  Sorted R l1 ->
  Sorted R l2.

Lemma eqlistA_refl : forall {A} (eqA : A -> A -> Prop) l,
  Reflexive eqA ->
  eqlistA eqA l l.

Lemma transition_spec2:
  forall dom_pre s (INVARIANT : invariant s) (INVARIANT4 : invariant4 s),
  invariant2 s ->
  match transition dom_pre s with inr s' => invariant2 s' | inl m => postcondition2 m end.

Lemma initial_state_spec2:
  invariant2 (init_state ginit root).

Inductive invariant3 (s:state) : Prop :=
  Invariant3
    (CROSS_GRAY : forall u n l s_c s_t v, In (u, n, l, (s_c, s_t)) s.(wrk) ->
      s_c ! v = Some tt -> black_reduced_reachable_bis ginit s.(r) s.(back) u v)
    (CROSS: forall u set v, s.(c) ! u = Some set -> set ! v = Some tt ->
      black_reduced_reachable_bis ginit s.(r) s.(back) u v)

    (BACK_REVERSE_WRK :
      StronglySorted (fun '(u, _, _, _) '(v, _, _, _) => ~ In (v, u) s.(back)) s.(wrk))
    (WRK_BACK_NOT_BLACK : forall u n l post, In (u, n, l, post) s.(wrk) ->
      exists l', ginit!u = Some l' /\
      (forall v, In v l' ->
      In (u, v) s.(back) -> s.(r) ! v = None)).

Inductive postcondition3
  (acc : PTree.t (positive * positive)
       * PTree.t (PTree.t unit)
       * PTree.t (list (node * Z))
       * list (node * node))
  : Prop :=
  Postcondition3
    (CROSS: let '(r, c, t, back) := acc in
      forall u set v, c ! u = Some set -> set ! v = Some tt ->
      reduced_reachable ginit back u v).

Lemma transition_spec3:
  forall dom_pre s (INVARIANT : invariant s)
                (INVARIANT2 : invariant2 s)
                (INVARIANT4 : invariant4 s),
  invariant3 s ->
  match transition dom_pre s with inr s' => invariant3 s' | inl m => postcondition3 m end.

Lemma initial_state_spec3:
  invariant3 (init_state ginit root).

Inductive invariant5 (s:state) : Prop :=
  Invariant5
    (BLACK_IN_GRAPH : forall u, s.(r) ! u <> None -> ginit ! u <> None)
    (BLACK_REACHABLE_GRAY : forall u n l post, In (u, n, l, post) s.(wrk) ->
      reachable ginit root u)
    (BLACK_REACHABLE_BLACK :
      forall u, s.(r) ! u <> None -> reachable ginit root u)
    (OUT_NODES_BACK_GRAY : forall u n l post, In (u, n, l, post) s.(wrk) ->
      exists l', ginit ! u = Some l' /\
      forall v, In v l' -> ~ In v l -> ginit ! v = None ->
      In (u, v) s.(back))
    (CROSS_BLACK : forall u, s.(c) ! u <> None -> s.(r) ! u <> None)
    (OUT_NODES_BACK_BLACK : forall u succs v, s.(r) ! u <> None ->
      ginit ! u = Some succs -> In v succs -> ginit ! v = None ->
      In (u, v) s.(back))
    (BACK_SOURCE_GRAY_OR_BLACK : forall u v, In (u, v) s.(back) ->
      (exists n l post, In (u, n, l, post) s.(wrk)) \/ s.(r) ! u <> None)
    (BACK_BLACK : forall u, s.(t) ! u <> None <-> s.(r) ! u <> None)
    (BACK_IN_GRAPH : forall u v, In (u, v) s.(back) -> exists succs,
       ginit ! u = Some succs /\ In v succs).

Inductive postcondition5
  (acc : PTree.t (positive * positive)
       * PTree.t (PTree.t unit)
       * PTree.t (list (node * Z))
       * list (node * node))
  : Prop :=
  Postcondition5
    (BLACK_IN_GRAPH : let '(r, c, t, back) := acc in
      forall u, r ! u <> None -> ginit ! u <> None)
    (BLACK_REACHABLE : let '(r, c, t, back) := acc in
      forall u, r ! u <> None -> reachable ginit root u)
    (CROSS_BLACK : let '(r, c, t, back) := acc in
      forall u, c ! u <> None -> r ! u <> None)
    (OUT_NODES_BACK : let '(r, c, t, back) := acc in
      forall u succs v, ginit ! u = Some succs ->
      In v succs -> ginit ! v = None -> r ! u <> None -> In (u, v) back)
    (BACK_SOURCE_BLACK : let '(r, c, t, back) := acc in
      forall u v, In (u, v) back -> r ! u <> None)
    (BACK_BLACK : let '(r, c, t, back) := acc in
      forall u, t ! u <> None <-> r ! u <> None)
    (BACK_IN_GRAPH : let '(r, c, t, back) := acc in
      forall u v, In (u, v) back -> exists succs,
       ginit ! u = Some succs /\ In v succs).

Lemma transition_spec5:
  forall dom_pre s (INVARIANT : invariant s),
  invariant5 s ->
  match transition dom_pre s with inr s' => invariant5 s' | inl m => postcondition5 m end.

Lemma initial_state_spec5:
  invariant5 (init_state ginit root).


Section DOM_PRE.

Variable dom_pre : node -> Z.

Local Opaque ZSortWithIndex.merge.

Inductive invariant9 (s:state) : Prop :=
  Invariant9
    (T_DOM_PRE_GRAY : forall u n l s_c s_t, In (u, n, l, (s_c, s_t)) s.(wrk) ->
      Forall (fun '(u, n) => n = dom_pre u) s_t)
    (T_DOM_PRE_BLACK : forall u set, s.(t) ! u = Some set ->
      Forall (fun '(u, n) => n = dom_pre u) set)

    (T_SORTED_GRAY : forall u n l s_c s_t, In (u, n, l, (s_c, s_t)) s.(wrk) ->
      Sorted (fun '(_, n1) '(_, n2) => n1 < n2)%Z s_t)
    (T_SORTED_BLACK : forall u set, s.(t) ! u = Some set ->
      Sorted (fun '(_, n1) '(_, n2) => n1 < n2)%Z set).

Inductive postcondition9
  (acc : PTree.t (positive * positive)
       * PTree.t (PTree.t unit)
       * PTree.t (list (node * Z))
       * list (node * node))
  : Prop :=
  Postcondition9
    (T_DOM_PRE : let '(r, c, t, back) := acc in
      forall u set, t ! u = Some set ->
      Forall (fun '(u, n) => n = dom_pre u) set)

    (T_SORTED : let '(r, c, t, back) := acc in
      forall u set, t ! u = Some set ->
      Sorted (fun '(_, n1) '(_, n2) => n1 < n2)%Z set).

Lemma transition_spec9:
  forall s,
  invariant9 s ->
  match transition dom_pre s with inr s' => invariant9 s' | inl m => postcondition9 m end.

Lemma initial_state_spec9:
  invariant9 (init_state ginit root).

Section DOM_PRE_HYPS.

Hypothesis dom_pre_inj : forall u v,
  reachable ginit root u ->
  reachable ginit root v ->
  dom_pre u = dom_pre v ->
  u = v.

Inductive invariant6 (s:state) : Prop :=
  Invariant6
    (BACK_SOURCE_GRAY : forall u n l s_c s_t v, In (u, n, l, (s_c, s_t)) s.(wrk) ->
      In v (List.map fst s_t) ->
      exists w, In (w, v) s.(back)
      /\ black_reduced_reachable_bis ginit s.(r) s.(back) u w)
    (BACK_SOURCE : forall u set v, s.(t) ! u = Some set -> In v (List.map fst set) ->
      exists w, In (w, v) s.(back)
      /\ black_reduced_reachable_bis ginit s.(r) s.(back) u w)

    (BACK_TARGETS : forall u set v, s.(t) ! u = Some set -> In v (map fst set) ->
      ~ cross_included s.(r) s.(c) u v)

    (BACK_UPWARDS_GRAY : forall u n l s_c s_t, In (u, n, l, (s_c, s_t)) s.(wrk) ->
      exists l', ginit!u = Some l' /\
      (forall v set w, In v l' -> ~In v l -> ~ In (u, v) s.(back) ->
       s.(t) ! v = Some set -> In w (map fst set) -> In w (map fst s_t)))
    (BACK_UPWARDS_BLACK : forall u succs v set w, ginit ! u = Some succs ->
      s.(r) ! u <> None ->
      In v succs -> ~ In (u, v) s.(back) -> s.(t) ! v = Some set -> In w (map fst set) ->
      ~ cross_included s.(r) s.(c) u w -> exists set', s.(t) ! u = Some set' /\ In w (map fst set'))

    (CLASSIFY_BACK_GRAY : forall u n l s_c s_t, In (u, n, l, (s_c, s_t)) s.(wrk) ->
      exists l', ginit!u = Some l' /\
      (forall v, In v l' -> ~In v l ->
      In (u, v) s.(back) -> In v (map fst s_t)))
    (CLASSIFY_BACK_BLACK : forall u v, In (u, v) s.(back) -> s.(r)!u <> None ->
      u = v \/ exists set, s.(t) ! u = Some set /\ In v (map fst set)).

Inductive postcondition6
  (acc : PTree.t (positive * positive)
       * PTree.t (PTree.t unit)
       * PTree.t (list (node * Z))
       * list (node * node))
  : Prop :=
  Postcondition6
    (BACK_SOURCE : let '(r, c, t, back) := acc in
      forall u set v,
      t ! u = Some set -> In v (map fst set) ->
      exists w, In (w, v) back
      /\ reduced_reachable ginit back u w)
    (BACK_TARGETS : let '(r, c, t, back) := acc in
      forall u set v, t ! u = Some set -> In v (map fst set) ->
      ~ cross_included r c u v)
    (BACK_UPWARDS: let '(r, c, t, back) := acc in
      forall u succs v set w, ginit ! u = Some succs -> r ! u <> None ->
      In v succs -> ~ In (u, v) back -> t ! v = Some set -> In w (map fst set) ->
      ~ cross_included r c u w -> exists set', t ! u = Some set' /\ In w (map fst set'))
    (CLASSIFY_BACK : let '(r, c, t, back) := acc in
      forall u v, In (u, v) back -> r ! u <> None ->
      u = v \/ exists set, t ! u = Some set /\ In v (List.map fst set)).

Lemma transition_spec6:
  forall s (INVARIANT : invariant s) (INVARIANT2 : invariant2 s)
  (INVARIANT3 : invariant3 s) (INVARIANT4 : invariant4 s)
  (INVARIANT5 : invariant5 s) (INVARIANT9 : invariant9 s),
  invariant6 s ->
  match transition dom_pre s with inr s' => invariant6 s' | inl m => postcondition6 m end.

End DOM_PRE_HYPS.

End DOM_PRE.

Lemma initial_state_spec6:
  invariant6 (init_state ginit root).


Inductive invariant7 (s:state) : Prop :=
  Invariant7
    (BACK_NUMBERS_DECREASE_GRAY : forall u n l post v m1 m2,
      In (u, n, l, post) s.(wrk) ->
      s.(r) ! v = Some (m1, m2) ->
      In (v, u) s.(back) ->
      n < m1)
    (BACK_NUMBERS_DECREASE : forall u v n1 n2 m1 m2, In (u, v) s.(back) ->
      s.(r) ! u = Some (n1, n2) -> s.(r) ! v = Some (m1, m2) ->
      is_included (n1, n2) (m1, m2)).

Inductive postcondition7
  (acc : PTree.t (positive * positive)
       * PTree.t (PTree.t unit)
       * PTree.t (list (node * Z))
       * list (node * node))
  : Prop :=
  Postcondition7
    (BACK_NUMBERS_DECREASE : let '(r, c, t, back) := acc in
      forall u v n1 n2 m1 m2, In (u, v) back ->
      r ! u = Some (n1, n2) -> r ! v = Some (m1, m2) ->
      is_included (n1, n2) (m1, m2)).

Lemma transition_spec7:
  forall dom_pre s (INVARIANT : invariant s) (INVARIANT2 : invariant2 s)
  (INVARIANT3 : invariant3 s) (INVARIANT4 : invariant4 s) (INVARIANT5 : invariant5 s),
  invariant7 s ->
  match transition dom_pre s with inr s' => invariant7 s' | inl m => postcondition7 m end.

Lemma initial_state_spec7:
  invariant7 (init_state ginit root).


Inductive invariant8 (s:state) : Prop :=
  Invariant8
    (CROSS_NUMBERS_DECREASE_BLACK : forall u set v,
      s.(c) ! u = Some set -> set ! v = Some tt ->
      v <> u ->
      exists n1 n2 m1 m2,
        s.(r) ! u = Some (n1, n2) /\ s.(r) ! v = Some (m1, m2) /\
        m2 < n1).

Inductive postcondition8
  (acc : PTree.t (positive * positive)
       * PTree.t (PTree.t unit)
       * PTree.t (list (node * Z))
       * list (node * node))
  : Prop :=
  Postcondition8
    (CROSS_NUMBERS_DECREASE : let '(r, c, t, back) := acc 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).

Lemma transition_spec8:
  forall dom_pre s (INVARIANT : invariant s) (INVARIANT2 : invariant2 s)
  (INVARIANT4 : invariant4 s) (INVARIANT5 : invariant5 s),
  invariant8 s ->
  match transition dom_pre s with inr s' => invariant8 s' | inl m => postcondition8 m end.

Lemma initial_state_spec8:
  invariant8 (init_state ginit root).


Inductive invariant10 (s:state) : Prop :=
  Invariant10
    (ROOT_LAST_WRK : exists l post, last s.(wrk) (root, 1, l, post) = (root, 1, l, post))
    (ROOT_REACHABLE : s.(wrk) = nil ->
      forall u, s.(r) ! u <> None -> reduced_reachable ginit s.(back) root u).

Inductive postcondition10
  (acc : PTree.t (positive * positive)
       * PTree.t (PTree.t unit)
       * PTree.t (list (node * Z))
       * list (node * node))
  : Prop :=
  Postcondition10
    (ROOT_REACHABLE : let '(r, c, t, back) := acc in
      forall u, r ! u <> None ->
      reduced_reachable ginit back root u).

Lemma transition_spec10:
  forall dom_pre s (INVARIANT2 : invariant2 s),
  invariant10 s ->
  match transition dom_pre s with inr s' => invariant10 s' | inl m => postcondition10 m end.

Lemma initial_state_spec10:
  invariant10 (init_state ginit root).

End POSTORDER.


Theorem precompute_r_t_up_correct_1:
  forall g root dom_pre,
  let '(r, c, t, back) := precompute_r_t_up g root dom_pre in
  (forall x1 x2 m n1 n2, r!x1 = Some (m, n1) -> r!x2 = Some (m, n2) -> x1 = x2)
  /\ (forall x, reachable g root x -> g!x <> None -> r!x <> None)
  /\ (forall x n1 n2, r ! x = Some (n1, n2) -> Ple n1 n2).

Lemma precompute_r_t_up_correct_2 :
  forall g root dom_pre,
  let '(r, c, t, back) := precompute_r_t_up g root dom_pre in
  (forall x1 x2 n1 n2 m1 m2, r ! x1 = Some (n1, n2) -> r!x2 = Some (m1, m2) ->
  is_included (m1, m2) (n1, n2) -> reduced_reachable g back x1 x2)
  /\ (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)) .

Lemma precompute_r_t_up_correct_3 :
  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.

Lemma precompute_r_t_up_correct_4 :
  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 -> reduced_reachable g back u v ->
    g ! v <> None -> cross_included r c u v)
  /\ (forall u set v, c ! u = Some set -> set ! v = Some tt ->
      r ! v <> None)
  /\ (forall u, r ! u <> None ->
      exists set, c ! u = Some set /\ set ! u = Some tt).

Lemma precompute_r_t_up_correct_5 :
  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)
  /\ (forall u, c ! u <> None -> r ! u <> None)
  /\ (forall u succs v, g ! u = Some succs -> In v succs ->
     g ! v = None -> r ! u <> None -> In (u, v) back)
  /\ (forall u v, In (u, v) back -> r ! u <> None)
  /\ (forall u, t ! u <> None <-> r ! u <> None)
  /\ (forall u v, In (u, v) back -> exists succs,
       g ! u = Some succs /\ In v succs).

Lemma precompute_r_t_up_correct_6 : 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,
    (reachable g root u /\ g ! u <> None /\ is_in_t_up g back u v)
    <-> exists set, t ! u = Some set /\ In v (map fst set)).

Lemma precompute_r_t_up_correct_7 : 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.

Lemma precompute_r_t_up_correct_8 : 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.

Lemma precompute_r_t_up_correct_9 : forall g root dom_pre,
  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)
  /\ (forall u set, t ! u = Some set ->
       Sorted (fun '(_, n1) '(_, n2) => n1 < n2)%Z set).

Lemma precompute_r_t_up_correct_10 : 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.