(* *********************************************************************)
(*                                                                     *)
(*              The Compcert verified compiler                         *)
(*                                                                     *)
(*          Xavier Leroy, INRIA Paris-Rocquencourt                     *)
(*                                                                     *)
(*  Copyright Institut National de Recherche en Informatique et en     *)
(*  Automatique.  All rights reserved.  This file is distributed       *)
(*  under the terms of the GNU General Public License as published by  *)
(*  the Free Software Foundation, either version 2 of the License, or  *)
(*  (at your option) any later version.  This file is also distributed *)
(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
(*                                                                     *)
(* *********************************************************************)

(** Postorder numbering of a directed graph. *)

Require Import Wellfounded.
Require Import Permutation.
Require Import Mergesort.
Require Import Coqlib.
Require Import Maps.
Require Import Iteration.

(** The graph is presented as a finite map from nodes (of type [positive])
  to the lists of their successors. *)

Definition node: Type := positive.

Definition graph: Type := PTree.t (list node).

(** A sorting function over lists of positives.  While not necessary for
  correctness, we process the successors of a node in increasing order.
  This preserves more of the shape of the original graph and is good for
  our CFG linearization heuristic. *)

Module PositiveOrd.
  Definition t := positive.
  Definition leb (x y: t): bool := if plt y x then false else true.
(*  Infix "<=?" := leb (at level 35). *)
  Theorem leb_total : forall x y, is_true (leb x y) \/ is_true (leb y x).
  Proof.
(* Goal: forall x y : t, or (is_true (leb x y)) (is_true (leb y x)) *)
    unfold leb, is_true; intros.
(* Goal: or (@eq bool (if plt y x then false else true) true) (@eq bool (if plt x y then false else true) true) *)
    destruct (plt x y); auto. destruct (plt y x); auto.
(* Goal: or (@eq bool false true) (@eq bool false true) *)
    elim (Plt_strict x). eapply Plt_trans; eauto.
  Qed.
End PositiveOrd.

Module Sort := Mergesort.Sort(PositiveOrd).

(** The traversal is presented as an iteration that modifies the following state. *)

Record state : Type := mkstate {
  gr: graph;                    (**r current graph, without already-visited nodes *)
  wrk: list (node * list node); (**r worklist *)
  map: PTree.t positive;        (**r current mapping node -> postorder number *)
  next: positive                (**r number to use for next numbering *)
}.

Definition init_state (g: graph) (root: node) :=
  match g!root with
  | Some succs =>
     {| gr := PTree.remove root g;
        wrk := (root, Sort.sort succs) :: nil;
        map := PTree.empty positive;
        next := 1%positive |}
  | None =>
     {| gr := g;
        wrk := nil;
        map := PTree.empty positive;
        next := 1%positive |}
  end.

Definition transition (s: state) : PTree.t positive + state :=
  match s.(wrk) with
  | nil =>                              (**r empty worklist, we are done *)
      inl _ s.(map)
  | (x, nil) :: l =>                    (**r all successors of [x] are numbered; number [x] itself *)
      inr _ {| gr := s.(gr);
               wrk := l;
               map := PTree.set x s.(next) s.(map);
               next := Pos.succ s.(next) |}
  | (x, y :: succs_x) :: l =>           (**r consider [y], the next unnumbered successor of [x] *)
      match s.(gr)!y with
      | None =>                         (**r [y] is already numbered: discard from worklist *)
          inr _ {| gr := s.(gr);
                   wrk := (x, succs_x) :: l;
                   map := s.(map);
                   next := s.(next) |}
      | Some succs_y =>                 (**r push [y] on the worklist *)
          inr _ {| gr := PTree.remove y s.(gr);
                   wrk := (y, Sort.sort succs_y) :: (x, succs_x) :: l;
                   map := s.(map);
                   next := s.(next) |}
      end
  end.

Section POSTORDER.

Variable ginit: graph.
Variable root: node.

Inductive invariant (s: state) : Prop :=
  Invariant
    (* current graph is a subset of ginit *)
    (SUB: forall x y, s.(gr)!x = Some y -> ginit!x = Some y)
    (* root is not in current graph *)
    (ROOT: s.(gr)!root = None)
    (* mapped nodes have their numbers below next *)
    (BELOW: forall x y, s.(map)!x = Some y -> Plt y s.(next))
    (* mapping is injective *)
    (INJ: forall x1 x2 y, s.(map)!x1 = Some y -> s.(map)!x2 = Some y -> x1 = x2)
    (* nodes not yet visited have no number *)
    (REM: forall x y, s.(gr)!x = Some y -> s.(map)!x = None)
    (* black nodes have no white son *)
    (COLOR: forall x succs n y,
            ginit!x = Some succs -> s.(map)!x = Some n ->
            In y succs -> s.(gr)!y = None)
    (* worklist is well-formed *)
    (WKLIST: forall x l, In (x, l) s.(wrk) ->
             s.(gr)!x = None /\
             exists l', ginit!x = Some l'
                    /\ forall y, In y l' -> ~In y l -> s.(gr)!y = None)
    (* all grey nodes are on the worklist *)
    (GREY: forall x, ginit!x <> None -> s.(gr)!x = None -> s.(map)!x = None ->
           exists l, In (x,l) s.(wrk)).

Inductive postcondition (map: PTree.t positive) : Prop :=
  Postcondition
    (INJ: forall x1 x2 y, map!x1 = Some y -> map!x2 = Some y -> x1 = x2)
    (ROOT: ginit!root <> None -> map!root <> None)
    (SUCCS: forall x succs y, ginit!x = Some succs -> map!x <> None -> In y succs -> ginit!y <> None -> map!y <> None).

Remark In_sort:
  forall x l, In x l <-> In x (Sort.sort l).
Proof.
(* Goal: forall (x : positive) (l : list positive), iff (@In positive x l) (@In positive x (Sort.sort l)) *)
  intros; split; intros.
(* Goal: @In positive x (Sort.sort l) *)
(* Goal: @In positive x l *)
  apply Permutation_in with l. apply Sort.Permuted_sort. auto.
(* Goal: @Permutation positive l (Sort.sort l) *)
(* Goal: @In positive x (Sort.sort l) *)
  apply Permutation_in with (Sort.sort l). apply Permutation_sym. apply Sort.Permuted_sort. auto.
Qed.

Lemma transition_spec:
  forall s, invariant s ->
  match transition s with inr s' => invariant s' | inl m => postcondition m end.
Proof.
(* Goal: forall (g : graph) (root : node), let m := postorder g root in and (forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2) (forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive))) *)
  intros. inv H. unfold transition. destruct (wrk s) as [ | [x succ_x] l].
  (* finished *)
(* Goal: forall (g : graph) (root : node), let m := postorder g root in and (forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2) (forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive))) *)
  constructor; intros.
(* Goal: forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2 *)
(* Goal: forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive)) *)
  eauto.
(* Goal: forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2 *)
(* Goal: forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive)) *)
  caseEq (s.(map)!root); intros. congruence. exploit GREY; eauto. intros [? ?]; contradiction.
(* Goal: not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node))) *)
  destruct (s.(map)!x) eqn:?; try congruence.
(* Goal: not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node))) *)
  destruct (s.(map)!y) eqn:?; try congruence.
(* Goal: forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2 *)
(* Goal: forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive)) *)
  exploit COLOR; eauto. intros. exploit GREY; eauto. intros [? ?]; contradiction.
  (* not finished *)
(* Goal: match match succ_x with | nil => @inr (PTree.t positive) state (mkstate (gr s) l (@PTree.set positive x (next s) (map s)) (Pos.succ (next s))) | cons y succs_x => match @PTree.get (list node) y (gr s) with | Some succs_y => @inr (PTree.t positive) state (mkstate (@PTree.remove (list node) y (gr s)) (@cons (prod node (list positive)) (@pair node (list positive) y (Sort.sort succs_y)) (@cons (prod node (list node)) (@pair node (list node) x succs_x) l)) (map s) (next s)) | None => @inr (PTree.t positive) state (mkstate (gr s) (@cons (prod node (list node)) (@pair node (list node) x succs_x) l) (map s) (next s)) end end with | inl m => postcondition m | inr s' => invariant s' end *)
  destruct succ_x as [ | y succ_x ].
  (* all children of x were traversed *)
(* Goal: forall (g : graph) (root : node), let m := postorder g root in and (forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2) (forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive))) *)
  constructor; simpl; intros.
  (* sub *)
(* Goal: forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2 *)
(* Goal: forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive)) *)
  eauto.
  (* root *)
(* Goal: forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2 *)
(* Goal: forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive)) *)
  eauto.
  (* below *)
(* Goal: and (forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2) (forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive))) *)
  rewrite PTree.gsspec in H. destruct (peq x0 x). inv H.
(* Goal: Plt (next s) (Pos.succ (next s)) *)
(* Goal: Plt y (Pos.succ (next s)) *)
(* Goal: @eq positive x1 x2 *)
(* Goal: @eq (option positive) (@PTree.get positive x0 (@PTree.set positive x (next s) (map s))) (@None positive) *)
(* Goal: @eq (option (list node)) (@PTree.get (list node) y (gr s)) (@None (list node)) *)
(* Goal: and (@eq (option (list node)) (@PTree.get (list node) x0 (gr s)) (@None (list node))) (@ex (list node) (fun l' : list node => and (@eq (option (list node)) (@PTree.get (list node) x0 ginit) (@Some (list node) l')) (forall (y : node) (_ : @In node y l') (_ : not (@In node y l0)), @eq (option (list node)) (@PTree.get (list node) y (gr s)) (@None (list node))))) *)
(* Goal: @ex (list node) (fun l0 : list node => @In (prod positive (list node)) (@pair positive (list node) x0 l0) l) *)
(* Goal: match match @PTree.get (list node) y (gr s) with | Some succs_y => @inr (PTree.t positive) state (mkstate (@PTree.remove (list node) y (gr s)) (@cons (prod node (list positive)) (@pair node (list positive) y (Sort.sort succs_y)) (@cons (prod node (list node)) (@pair node (list node) x succ_x) l)) (map s) (next s)) | None => @inr (PTree.t positive) state (mkstate (gr s) (@cons (prod node (list node)) (@pair node (list node) x succ_x) l) (map s) (next s)) end with | inl m => postcondition m | inr s' => invariant s' end *)
  apply Plt_succ.
(* Goal: forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2 *)
(* Goal: forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive)) *)
  apply Plt_trans_succ. eauto.
  (* inj *)
(* Goal: @eq positive x1 x2 *)
(* Goal: @eq (option positive) (@PTree.get positive x0 (@PTree.set positive x (next s) (map s))) (@None positive) *)
(* Goal: @eq (option (list node)) (@PTree.get (list node) y (gr s)) (@None (list node)) *)
(* Goal: and (@eq (option (list node)) (@PTree.get (list node) x0 (gr s)) (@None (list node))) (@ex (list node) (fun l' : list node => and (@eq (option (list node)) (@PTree.get (list node) x0 ginit) (@Some (list node) l')) (forall (y : node) (_ : @In node y l') (_ : not (@In node y l0)), @eq (option (list node)) (@PTree.get (list node) y (gr s)) (@None (list node))))) *)
(* Goal: @ex (list node) (fun l0 : list node => @In (prod positive (list node)) (@pair positive (list node) x0 l0) l) *)
(* Goal: match match @PTree.get (list node) y (gr s) with | Some succs_y => @inr (PTree.t positive) state (mkstate (@PTree.remove (list node) y (gr s)) (@cons (prod node (list positive)) (@pair node (list positive) y (Sort.sort succs_y)) (@cons (prod node (list node)) (@pair node (list node) x succ_x) l)) (map s) (next s)) | None => @inr (PTree.t positive) state (mkstate (gr s) (@cons (prod node (list node)) (@pair node (list node) x succ_x) l) (map s) (next s)) end with | inl m => postcondition m | inr s' => invariant s' end *)
  rewrite PTree.gsspec in H. rewrite PTree.gsspec in H0.
(* Goal: @eq positive x1 x2 *)
(* Goal: @eq (option positive) (@PTree.get positive x0 (@PTree.set positive x (next s) (map s))) (@None positive) *)
(* Goal: @eq (option (list node)) (@PTree.get (list node) y (gr s)) (@None (list node)) *)
(* Goal: and (@eq (option (list node)) (@PTree.get (list node) x0 (gr s)) (@None (list node))) (@ex (list node) (fun l' : list node => and (@eq (option (list node)) (@PTree.get (list node) x0 ginit) (@Some (list node) l')) (forall (y : node) (_ : @In node y l') (_ : not (@In node y l0)), @eq (option (list node)) (@PTree.get (list node) y (gr s)) (@None (list node))))) *)
(* Goal: @ex (list node) (fun l0 : list node => @In (prod positive (list node)) (@pair positive (list node) x0 l0) l) *)
(* Goal: match match @PTree.get (list node) y (gr s) with | Some succs_y => @inr (PTree.t positive) state (mkstate (@PTree.remove (list node) y (gr s)) (@cons (prod node (list positive)) (@pair node (list positive) y (Sort.sort succs_y)) (@cons (prod node (list node)) (@pair node (list node) x succ_x) l)) (map s) (next s)) | None => @inr (PTree.t positive) state (mkstate (gr s) (@cons (prod node (list node)) (@pair node (list node) x succ_x) l) (map s) (next s)) end with | inl m => postcondition m | inr s' => invariant s' end *)
  destruct (peq x1 x); destruct (peq x2 x); subst.
(* Goal: forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2 *)
(* Goal: forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive)) *)
  auto.
(* Goal: forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2 *)
(* Goal: forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive)) *)
  inv H. exploit BELOW; eauto. intros. eelim Plt_strict; eauto.
(* Goal: forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2 *)
(* Goal: forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive)) *)
  inv H0. exploit BELOW; eauto. intros. eelim Plt_strict; eauto.
(* Goal: forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2 *)
(* Goal: forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive)) *)
  eauto.
  (* rem *)
(* Goal: forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2 *)
(* Goal: forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive)) *)
  intros. rewrite PTree.gso; eauto. red; intros; subst x0.
(* Goal: not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node))) *)
  exploit (WKLIST x nil); auto with coqlib. intros [A B]. congruence.
  (* color *)
(* Goal: @ex (list node) (fun l0 : list node => @In (prod positive (list node)) (@pair positive (list node) x0 l0) l) *)
(* Goal: match match @PTree.get (list node) y (gr s) with | Some succs_y => @inr (PTree.t positive) state (mkstate (@PTree.remove (list node) y (gr s)) (@cons (prod node (list positive)) (@pair node (list positive) y (Sort.sort succs_y)) (@cons (prod node (list node)) (@pair node (list node) x succ_x) l)) (map s) (next s)) | None => @inr (PTree.t positive) state (mkstate (gr s) (@cons (prod node (list node)) (@pair node (list node) x succ_x) l) (map s) (next s)) end with | inl m => postcondition m | inr s' => invariant s' end *)
  rewrite PTree.gsspec in H0. destruct (peq x0 x).
(* Goal: @eq (option (list node)) (@PTree.get (list node) y (gr s)) (@None (list node)) *)
(* Goal: @eq (option (list node)) (@PTree.get (list node) y (gr s)) (@None (list node)) *)
(* Goal: and (@eq (option (list node)) (@PTree.get (list node) x0 (gr s)) (@None (list node))) (@ex (list node) (fun l' : list node => and (@eq (option (list node)) (@PTree.get (list node) x0 ginit) (@Some (list node) l')) (forall (y : node) (_ : @In node y l') (_ : not (@In node y l0)), @eq (option (list node)) (@PTree.get (list node) y (gr s)) (@None (list node))))) *)
(* Goal: @ex (list node) (fun l0 : list node => @In (prod positive (list node)) (@pair positive (list node) x0 l0) l) *)
(* Goal: match match @PTree.get (list node) y (gr s) with | Some succs_y => @inr (PTree.t positive) state (mkstate (@PTree.remove (list node) y (gr s)) (@cons (prod node (list positive)) (@pair node (list positive) y (Sort.sort succs_y)) (@cons (prod node (list node)) (@pair node (list node) x succ_x) l)) (map s) (next s)) | None => @inr (PTree.t positive) state (mkstate (gr s) (@cons (prod node (list node)) (@pair node (list node) x succ_x) l) (map s) (next s)) end with | inl m => postcondition m | inr s' => invariant s' end *)
  inv H0.  exploit (WKLIST x nil); auto with coqlib.
(* Goal: forall _ : and (@eq (option (list node)) (@PTree.get (list node) x0 (gr s)) (@None (list node))) (@ex (list node) (fun l' : list node => and (@eq (option (list node)) (@PTree.get (list node) x0 ginit) (@Some (list node) l')) (forall (y0 : node) (_ : @In node y0 l') (_ : not (@In node y0 (@cons node y l0))), @eq (option (list node)) (@PTree.get (list node) y0 (gr s)) (@None (list node))))), and (@eq (option (list node)) (@PTree.get (list node) x0 (gr s)) (@None (list node))) (@ex (list node) (fun l' : list node => and (@eq (option (list node)) (@PTree.get (list node) x0 ginit) (@Some (list node) l')) (forall (y : node) (_ : @In node y l') (_ : not (@In node y l0)), @eq (option (list node)) (@PTree.get (list node) y (gr s)) (@None (list node))))) *)
(* Goal: and (@eq (option (list node)) (@PTree.get (list node) x0 (gr s)) (@None (list node))) (@ex (list node) (fun l' : list node => and (@eq (option (list node)) (@PTree.get (list node) x0 ginit) (@Some (list node) l')) (forall (y : node) (_ : @In node y l') (_ : not (@In node y l0)), @eq (option (list node)) (@PTree.get (list node) y (gr s)) (@None (list node))))) *)
(* Goal: @ex (list node) (fun l0 : list node => or (@eq (prod positive (list node)) (@pair node (list node) x succ_x) (@pair positive (list node) x0 l0)) (@In (prod positive (list node)) (@pair positive (list node) x0 l0) l)) *)
  intros [A [l' [B C]]].
(* Goal: not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node))) *)
  assert (l' = succs) by congruence. subst l'.
(* Goal: forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2 *)
(* Goal: forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive)) *)
  apply C; auto.
(* Goal: forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2 *)
(* Goal: forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive)) *)
  eauto.
  (* wklist *)
(* Goal: and (@eq (option (list node)) (@PTree.get (list node) x0 (gr s)) (@None (list node))) (@ex (list node) (fun l' : list node => and (@eq (option (list node)) (@PTree.get (list node) x0 ginit) (@Some (list node) l')) (forall (y : node) (_ : @In node y l') (_ : not (@In node y l0)), @eq (option (list node)) (@PTree.get (list node) y (gr s)) (@None (list node))))) *)
(* Goal: @ex (list node) (fun l0 : list node => @In (prod positive (list node)) (@pair positive (list node) x0 l0) l) *)
(* Goal: match match @PTree.get (list node) y (gr s) with | Some succs_y => @inr (PTree.t positive) state (mkstate (@PTree.remove (list node) y (gr s)) (@cons (prod node (list positive)) (@pair node (list positive) y (Sort.sort succs_y)) (@cons (prod node (list node)) (@pair node (list node) x succ_x) l)) (map s) (next s)) | None => @inr (PTree.t positive) state (mkstate (gr s) (@cons (prod node (list node)) (@pair node (list node) x succ_x) l) (map s) (next s)) end with | inl m => postcondition m | inr s' => invariant s' end *)
  apply WKLIST. auto with coqlib.
  (* grey *)
(* Goal: @ex (list node) (fun l0 : list node => @In (prod positive (list node)) (@pair positive (list node) x0 l0) l) *)
(* Goal: match match @PTree.get (list node) y (gr s) with | Some succs_y => @inr (PTree.t positive) state (mkstate (@PTree.remove (list node) y (gr s)) (@cons (prod node (list positive)) (@pair node (list positive) y (Sort.sort succs_y)) (@cons (prod node (list node)) (@pair node (list node) x succ_x) l)) (map s) (next s)) | None => @inr (PTree.t positive) state (mkstate (gr s) (@cons (prod node (list node)) (@pair node (list node) x succ_x) l) (map s) (next s)) end with | inl m => postcondition m | inr s' => invariant s' end *)
  rewrite PTree.gsspec in H1. destruct (peq x0 x). inv H1.
(* Goal: forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2 *)
(* Goal: forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive)) *)
  exploit GREY; eauto. intros [l' A]. simpl in A; destruct A.
(* Goal: not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node))) *)
  congruence.
(* Goal: forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2 *)
(* Goal: forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive)) *)
  exists l'; auto.

  (* children y needs traversing *)
(* Goal: match match @PTree.get (list node) y (gr s) with | Some succs_y => @inr (PTree.t positive) state (mkstate (@PTree.remove (list node) y (gr s)) (@cons (prod node (list positive)) (@pair node (list positive) y (Sort.sort succs_y)) (@cons (prod node (list node)) (@pair node (list node) x succ_x) l)) (map s) (next s)) | None => @inr (PTree.t positive) state (mkstate (gr s) (@cons (prod node (list node)) (@pair node (list node) x succ_x) l) (map s) (next s)) end with | inl m => postcondition m | inr s' => invariant s' end *)
  destruct ((gr s)!y) as [ succs_y | ] eqn:?.
  (* y has children *)
(* Goal: forall (g : graph) (root : node), let m := postorder g root in and (forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2) (forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive))) *)
  constructor; simpl; intros.
  (* sub *)
(* Goal: forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2 *)
(* Goal: forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive)) *)
  rewrite PTree.grspec in H. destruct (PTree.elt_eq x0 y); eauto. inv H.
  (* root *)
(* Goal: forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2 *)
(* Goal: forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive)) *)
  rewrite PTree.gro. auto. congruence.
  (* below *)
(* Goal: forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2 *)
(* Goal: forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive)) *)
  eauto.
  (* inj *)
(* Goal: forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2 *)
(* Goal: forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive)) *)
  eauto.
  (* rem *)
(* Goal: forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2 *)
(* Goal: forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive)) *)
  rewrite PTree.grspec in H. destruct (PTree.elt_eq x0 y); eauto. inv H.
  (* color *)
(* Goal: forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2 *)
(* Goal: forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive)) *)
  rewrite PTree.grspec. destruct (PTree.elt_eq y0 y); eauto.
  (* wklist *)
(* Goal: and (@eq (option (list node)) (@PTree.get (list node) x0 (gr s)) (@None (list node))) (@ex (list node) (fun l' : list node => and (@eq (option (list node)) (@PTree.get (list node) x0 ginit) (@Some (list node) l')) (forall (y : node) (_ : @In node y l') (_ : not (@In node y l0)), @eq (option (list node)) (@PTree.get (list node) y (gr s)) (@None (list node))))) *)
(* Goal: @ex (list node) (fun l0 : list node => or (@eq (prod positive (list node)) (@pair node (list node) x succ_x) (@pair positive (list node) x0 l0)) (@In (prod positive (list node)) (@pair positive (list node) x0 l0) l)) *)
  destruct H.
(* Goal: forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2 *)
(* Goal: forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive)) *)
  inv H. split. apply PTree.grs. exists succs_y; split. eauto.
(* Goal: forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2 *)
(* Goal: forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive)) *)
  intros. rewrite In_sort in H. tauto.
(* Goal: and (@eq (option (list node)) (@PTree.get (list node) x0 (gr s)) (@None (list node))) (@ex (list node) (fun l' : list node => and (@eq (option (list node)) (@PTree.get (list node) x0 ginit) (@Some (list node) l')) (forall (y : node) (_ : @In node y l') (_ : not (@In node y l0)), @eq (option (list node)) (@PTree.get (list node) y (gr s)) (@None (list node))))) *)
(* Goal: @ex (list node) (fun l0 : list node => or (@eq (prod positive (list node)) (@pair node (list node) x succ_x) (@pair positive (list node) x0 l0)) (@In (prod positive (list node)) (@pair positive (list node) x0 l0) l)) *)
  destruct H.
(* Goal: and (forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2) (forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive))) *)
  inv H. exploit WKLIST; eauto with coqlib. intros [A [l' [B C]]].
(* Goal: forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2 *)
(* Goal: forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive)) *)
  split. rewrite PTree.grspec. destruct (PTree.elt_eq x0 y); auto.
(* Goal: forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2 *)
(* Goal: forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive)) *)
  exists l'; split. auto. intros. rewrite PTree.grspec. destruct (PTree.elt_eq y0 y); auto.
(* Goal: forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2 *)
(* Goal: forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive)) *)
  apply C; auto. simpl. intuition congruence.
(* Goal: forall _ : and (@eq (option (list node)) (@PTree.get (list node) x0 (gr s)) (@None (list node))) (@ex (list node) (fun l' : list node => and (@eq (option (list node)) (@PTree.get (list node) x0 ginit) (@Some (list node) l')) (forall (y0 : node) (_ : @In node y0 l') (_ : not (@In node y0 (@cons node y l0))), @eq (option (list node)) (@PTree.get (list node) y0 (gr s)) (@None (list node))))), and (@eq (option (list node)) (@PTree.get (list node) x0 (gr s)) (@None (list node))) (@ex (list node) (fun l' : list node => and (@eq (option (list node)) (@PTree.get (list node) x0 ginit) (@Some (list node) l')) (forall (y : node) (_ : @In node y l') (_ : not (@In node y l0)), @eq (option (list node)) (@PTree.get (list node) y (gr s)) (@None (list node))))) *)
(* Goal: and (@eq (option (list node)) (@PTree.get (list node) x0 (gr s)) (@None (list node))) (@ex (list node) (fun l' : list node => and (@eq (option (list node)) (@PTree.get (list node) x0 ginit) (@Some (list node) l')) (forall (y : node) (_ : @In node y l') (_ : not (@In node y l0)), @eq (option (list node)) (@PTree.get (list node) y (gr s)) (@None (list node))))) *)
(* Goal: @ex (list node) (fun l0 : list node => or (@eq (prod positive (list node)) (@pair node (list node) x succ_x) (@pair positive (list node) x0 l0)) (@In (prod positive (list node)) (@pair positive (list node) x0 l0) l)) *)
  exploit (WKLIST x0 l0); eauto with coqlib. intros [A [l' [B C]]].
(* Goal: forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2 *)
(* Goal: forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive)) *)
  split. rewrite PTree.grspec. destruct (PTree.elt_eq x0 y); auto.
(* Goal: forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2 *)
(* Goal: forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive)) *)
  exists l'; split; auto. intros.
(* Goal: forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2 *)
(* Goal: forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive)) *)
  rewrite PTree.grspec. destruct (PTree.elt_eq y0 y); auto.
  (* grey *)
(* Goal: @ex (list node) (fun l : list node => or (@eq (prod positive (list node)) (@pair node (list positive) root (Sort.sort succs)) (@pair positive (list node) x l)) False) *)
(* Goal: invariant (mkstate ginit (@nil (prod node (list node))) (PTree.empty positive) xH) *)
  rewrite PTree.grspec in H0. destruct (PTree.elt_eq x0 y) in H0.
(* Goal: @In (prod node (list node)) (@pair node (list node) x0 l0) (@cons (prod node (list node)) (@pair node (list node) x (@nil node)) l) *)
(* Goal: @ex (list node) (fun l0 : list node => @In (prod positive (list node)) (@pair positive (list node) x0 l0) l) *)
(* Goal: match match @PTree.get (list node) y (gr s) with | Some succs_y => @inr (PTree.t positive) state (mkstate (@PTree.remove (list node) y (gr s)) (@cons (prod node (list positive)) (@pair node (list positive) y (Sort.sort succs_y)) (@cons (prod node (list node)) (@pair node (list node) x succ_x) l)) (map s) (next s)) | None => @inr (PTree.t positive) state (mkstate (gr s) (@cons (prod node (list node)) (@pair node (list node) x succ_x) l) (map s) (next s)) end with | inl m => postcondition m | inr s' => invariant s' end *)
  subst. exists (Sort.sort succs_y); auto with coqlib.
(* Goal: forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2 *)
(* Goal: forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive)) *)
  exploit GREY; eauto. simpl. intros [l1 A]. destruct A.
(* Goal: forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2 *)
(* Goal: forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive)) *)
  inv H2. exists succ_x; auto.
(* Goal: forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2 *)
(* Goal: forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive)) *)
  exists l1; auto.

  (* y has no children *)
(* Goal: forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2 *)
(* Goal: forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive)) *)
  constructor; simpl; intros; eauto.
  (* wklist *)
(* Goal: and (forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2) (forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive))) *)
  destruct H. inv H.
(* Goal: forall _ : and (@eq (option (list node)) (@PTree.get (list node) x0 (gr s)) (@None (list node))) (@ex (list node) (fun l' : list node => and (@eq (option (list node)) (@PTree.get (list node) x0 ginit) (@Some (list node) l')) (forall (y0 : node) (_ : @In node y0 l') (_ : not (@In node y0 (@cons node y l0))), @eq (option (list node)) (@PTree.get (list node) y0 (gr s)) (@None (list node))))), and (@eq (option (list node)) (@PTree.get (list node) x0 (gr s)) (@None (list node))) (@ex (list node) (fun l' : list node => and (@eq (option (list node)) (@PTree.get (list node) x0 ginit) (@Some (list node) l')) (forall (y : node) (_ : @In node y l') (_ : not (@In node y l0)), @eq (option (list node)) (@PTree.get (list node) y (gr s)) (@None (list node))))) *)
(* Goal: and (@eq (option (list node)) (@PTree.get (list node) x0 (gr s)) (@None (list node))) (@ex (list node) (fun l' : list node => and (@eq (option (list node)) (@PTree.get (list node) x0 ginit) (@Some (list node) l')) (forall (y : node) (_ : @In node y l') (_ : not (@In node y l0)), @eq (option (list node)) (@PTree.get (list node) y (gr s)) (@None (list node))))) *)
(* Goal: @ex (list node) (fun l0 : list node => or (@eq (prod positive (list node)) (@pair node (list node) x succ_x) (@pair positive (list node) x0 l0)) (@In (prod positive (list node)) (@pair positive (list node) x0 l0) l)) *)
  exploit (WKLIST x0); eauto with coqlib. intros [A [l' [B C]]].
(* Goal: forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2 *)
(* Goal: forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive)) *)
  split. auto. exists l'; split. auto.
(* Goal: forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2 *)
(* Goal: forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive)) *)
  intros. destruct (peq y y0). congruence. apply C; auto. simpl. intuition congruence.
(* Goal: @In (prod node (list node)) (@pair node (list node) x0 l0) (@cons (prod node (list node)) (@pair node (list node) x (@nil node)) l) *)
(* Goal: @ex (list node) (fun l0 : list node => @In (prod positive (list node)) (@pair positive (list node) x0 l0) l) *)
(* Goal: match match @PTree.get (list node) y (gr s) with | Some succs_y => @inr (PTree.t positive) state (mkstate (@PTree.remove (list node) y (gr s)) (@cons (prod node (list positive)) (@pair node (list positive) y (Sort.sort succs_y)) (@cons (prod node (list node)) (@pair node (list node) x succ_x) l)) (map s) (next s)) | None => @inr (PTree.t positive) state (mkstate (gr s) (@cons (prod node (list node)) (@pair node (list node) x succ_x) l) (map s) (next s)) end with | inl m => postcondition m | inr s' => invariant s' end *)
  eapply WKLIST; eauto with coqlib.
  (* grey *)
(* Goal: forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2 *)
(* Goal: forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive)) *)
  exploit GREY; eauto. intros [l1 A]. simpl in A. destruct A.
(* Goal: forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2 *)
(* Goal: forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive)) *)
  inv H2. exists succ_x; auto.
(* Goal: forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2 *)
(* Goal: forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive)) *)
  exists l1; auto.
Qed.

Lemma initial_state_spec:
  invariant (init_state ginit root).
Proof.
(* Goal: invariant (init_state ginit root) *)
  unfold init_state. destruct (ginit!root) as [succs|] eqn:?.
  (* root has succs *)
(* Goal: forall (g : graph) (root : node), let m := postorder g root in and (forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2) (forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive))) *)
  constructor; simpl; intros.
  (* sub *)
(* Goal: forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2 *)
(* Goal: forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive)) *)
  rewrite PTree.grspec in H. destruct (PTree.elt_eq x root). inv H. auto.
  (* root *)
(* Goal: @eq (option (list node)) (@PTree.get (list node) x (@PTree.remove (list node) x ginit)) (@None (list node)) *)
(* Goal: @ex (list node) (fun l' : list node => and (@eq (option (list node)) (@PTree.get (list node) x ginit) (@Some (list node) l')) (forall (y : node) (_ : @In node y l') (_ : not (@In node y (Sort.sort succs))), @eq (option (list node)) (@PTree.get (list node) y (@PTree.remove (list node) x ginit)) (@None (list node)))) *)
(* Goal: @ex (list node) (fun l : list node => or (@eq (prod positive (list node)) (@pair node (list positive) root (Sort.sort succs)) (@pair positive (list node) x l)) False) *)
(* Goal: invariant (mkstate ginit (@nil (prod node (list node))) (PTree.empty positive) xH) *)
  apply PTree.grs.
  (* below *)
(* Goal: and (forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2) (forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive))) *)
  rewrite PTree.gempty in H; inv H.
  (* inj *)
(* Goal: and (forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2) (forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive))) *)
  rewrite PTree.gempty in H; inv H.
  (* rem *)
(* Goal: @eq (option positive) (@PTree.get positive x (PTree.empty positive)) (@None positive) *)
(* Goal: @eq (option (list node)) (@PTree.get (list node) y ginit) (@None (list node)) *)
(* Goal: and (@eq (option (list node)) (@PTree.get (list node) x ginit) (@None (list node))) (@ex (list node) (fun l' : list node => and (@eq (option (list node)) (@PTree.get (list node) x ginit) (@Some (list node) l')) (forall (y : node) (_ : @In node y l') (_ : not (@In node y l)), @eq (option (list node)) (@PTree.get (list node) y ginit) (@None (list node))))) *)
(* Goal: @ex (list node) (fun _ : list node => False) *)
  apply PTree.gempty.
  (* color *)
(* Goal: @eq (option (list node)) (@PTree.get (list node) y (gr s)) (@None (list node)) *)
(* Goal: @eq (option (list node)) (@PTree.get (list node) y (gr s)) (@None (list node)) *)
(* Goal: and (@eq (option (list node)) (@PTree.get (list node) x0 (gr s)) (@None (list node))) (@ex (list node) (fun l' : list node => and (@eq (option (list node)) (@PTree.get (list node) x0 ginit) (@Some (list node) l')) (forall (y : node) (_ : @In node y l') (_ : not (@In node y l0)), @eq (option (list node)) (@PTree.get (list node) y (gr s)) (@None (list node))))) *)
(* Goal: @ex (list node) (fun l0 : list node => @In (prod positive (list node)) (@pair positive (list node) x0 l0) l) *)
(* Goal: match match @PTree.get (list node) y (gr s) with | Some succs_y => @inr (PTree.t positive) state (mkstate (@PTree.remove (list node) y (gr s)) (@cons (prod node (list positive)) (@pair node (list positive) y (Sort.sort succs_y)) (@cons (prod node (list node)) (@pair node (list node) x succ_x) l)) (map s) (next s)) | None => @inr (PTree.t positive) state (mkstate (gr s) (@cons (prod node (list node)) (@pair node (list node) x succ_x) l) (map s) (next s)) end with | inl m => postcondition m | inr s' => invariant s' end *)
  rewrite PTree.gempty in H0; inv H0.
  (* wklist *)
(* Goal: and (forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2) (forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive))) *)
  destruct H; inv H.
(* Goal: forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2 *)
(* Goal: forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive)) *)
  split. apply PTree.grs. exists succs; split; auto.
(* Goal: forall (g : graph) (root : node), let m := postorder g root in and (forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2) (forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive))) *)
  intros. rewrite In_sort in H. intuition.
  (* grey *)
(* Goal: @ex (list node) (fun l : list node => or (@eq (prod positive (list node)) (@pair node (list positive) root (Sort.sort succs)) (@pair positive (list node) x l)) False) *)
(* Goal: invariant (mkstate ginit (@nil (prod node (list node))) (PTree.empty positive) xH) *)
  rewrite PTree.grspec in H0. destruct (PTree.elt_eq x root).
(* Goal: forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2 *)
(* Goal: forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive)) *)
  subst. exists (Sort.sort succs); auto.
(* Goal: @ex (list node) (fun _ : list node => False) *)
  contradiction.

  (* root has no succs *)
(* Goal: forall (g : graph) (root : node), let m := postorder g root in and (forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2) (forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive))) *)
  constructor; simpl; intros.
  (* sub *)
(* Goal: forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2 *)
(* Goal: forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive)) *)
  auto.
  (* root *)
(* Goal: forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2 *)
(* Goal: forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive)) *)
  auto.
  (* below *)
(* Goal: and (forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2) (forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive))) *)
  rewrite PTree.gempty in H; inv H.
  (* inj *)
(* Goal: and (forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2) (forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive))) *)
  rewrite PTree.gempty in H; inv H.
  (* rem *)
(* Goal: @eq (option positive) (@PTree.get positive x (PTree.empty positive)) (@None positive) *)
(* Goal: @eq (option (list node)) (@PTree.get (list node) y ginit) (@None (list node)) *)
(* Goal: and (@eq (option (list node)) (@PTree.get (list node) x ginit) (@None (list node))) (@ex (list node) (fun l' : list node => and (@eq (option (list node)) (@PTree.get (list node) x ginit) (@Some (list node) l')) (forall (y : node) (_ : @In node y l') (_ : not (@In node y l)), @eq (option (list node)) (@PTree.get (list node) y ginit) (@None (list node))))) *)
(* Goal: @ex (list node) (fun _ : list node => False) *)
  apply PTree.gempty.
  (* color *)
(* Goal: @eq (option (list node)) (@PTree.get (list node) y (gr s)) (@None (list node)) *)
(* Goal: @eq (option (list node)) (@PTree.get (list node) y (gr s)) (@None (list node)) *)
(* Goal: and (@eq (option (list node)) (@PTree.get (list node) x0 (gr s)) (@None (list node))) (@ex (list node) (fun l' : list node => and (@eq (option (list node)) (@PTree.get (list node) x0 ginit) (@Some (list node) l')) (forall (y : node) (_ : @In node y l') (_ : not (@In node y l0)), @eq (option (list node)) (@PTree.get (list node) y (gr s)) (@None (list node))))) *)
(* Goal: @ex (list node) (fun l0 : list node => @In (prod positive (list node)) (@pair positive (list node) x0 l0) l) *)
(* Goal: match match @PTree.get (list node) y (gr s) with | Some succs_y => @inr (PTree.t positive) state (mkstate (@PTree.remove (list node) y (gr s)) (@cons (prod node (list positive)) (@pair node (list positive) y (Sort.sort succs_y)) (@cons (prod node (list node)) (@pair node (list node) x succ_x) l)) (map s) (next s)) | None => @inr (PTree.t positive) state (mkstate (gr s) (@cons (prod node (list node)) (@pair node (list node) x succ_x) l) (map s) (next s)) end with | inl m => postcondition m | inr s' => invariant s' end *)
  rewrite PTree.gempty in H0; inv H0.
  (* wklist *)
(* Goal: @ex (list node) (fun _ : list node => False) *)
  contradiction.
  (* grey *)
(* Goal: @ex (list node) (fun _ : list node => False) *)
  contradiction.

Qed.

(** Termination criterion. *)

Fixpoint size_worklist (w: list (positive * list positive)) : nat :=
  match w with
  | nil => 0%nat
  | (x, succs) :: w' => (S (List.length succs) + size_worklist w')%nat
  end.

Definition lt_state (s1 s2: state) : Prop :=
  lex_ord lt lt (PTree_Properties.cardinal s1.(gr), size_worklist s1.(wrk))
                (PTree_Properties.cardinal s2.(gr), size_worklist s2.(wrk)).

Lemma lt_state_wf: well_founded lt_state.
Proof.
(* Goal: @well_founded state lt_state *)
  set (f := fun s => (PTree_Properties.cardinal s.(gr), size_worklist s.(wrk))).
(* Goal: @well_founded state lt_state *)
  change (well_founded (fun s1 s2 => lex_ord lt lt (f s1) (f s2))).
(* Goal: @well_founded state (fun s1 s2 : state => @lex_ord nat nat lt lt (f s1) (f s2)) *)
  apply wf_inverse_image.
(* Goal: @well_founded (prod nat nat) (@lex_ord nat nat lt lt) *)
  apply wf_lex_ord.
(* Goal: @well_founded nat lt *)
  apply lt_wf. apply lt_wf.
Qed.

Lemma transition_decreases:
  forall s s', transition s = inr _ s' -> lt_state s' s.
Proof.
(* Goal: forall (g : graph) (root : node), let m := postorder g root in and (forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2) (forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive))) *)
  unfold transition, lt_state; intros.
(* Goal: @lex_ord nat nat lt lt (@pair nat nat (@PTree_Properties.cardinal (list node) (gr s')) (size_worklist (wrk s'))) (@pair nat nat (@PTree_Properties.cardinal (list node) (gr s)) (size_worklist (wrk s))) *)
  destruct (wrk s) as [ | [x succs] l].
(* Goal: @lex_ord nat nat lt lt (@pair nat nat (@PTree_Properties.cardinal (list node) (gr s')) (size_worklist (wrk s'))) (@pair nat nat (@PTree_Properties.cardinal (list node) (gr s)) (size_worklist (@nil (prod node (list node))))) *)
(* Goal: @lex_ord nat nat lt lt (@pair nat nat (@PTree_Properties.cardinal (list node) (gr s')) (size_worklist (wrk s'))) (@pair nat nat (@PTree_Properties.cardinal (list node) (gr s)) (size_worklist (@cons (prod node (list node)) (@pair node (list node) x succs) l))) *)
  discriminate.
(* Goal: @lex_ord nat nat lt lt (@pair nat nat (@PTree_Properties.cardinal (list node) (gr s')) (size_worklist (wrk s'))) (@pair nat nat (@PTree_Properties.cardinal (list node) (gr s)) (size_worklist (@cons (prod node (list node)) (@pair node (list node) x succs) l))) *)
  destruct succs as [ | y succs ].
(* Goal: and (forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2) (forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive))) *)
  inv H. simpl. apply lex_ord_right. omega.
(* Goal: @lex_ord nat nat lt lt (@pair nat nat (@PTree_Properties.cardinal (list node) (gr s')) (size_worklist (wrk s'))) (@pair nat nat (@PTree_Properties.cardinal (list node) (gr s)) (size_worklist (@cons (prod node (list node)) (@pair node (list node) x (@cons node y succs)) l))) *)
  destruct ((gr s)!y) as [succs'|] eqn:?.
(* Goal: forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2 *)
(* Goal: forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive)) *)
  inv H. simpl. apply lex_ord_left. eapply PTree_Properties.cardinal_remove; eauto.
(* Goal: and (forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2) (forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive))) *)
  inv H. simpl. apply lex_ord_right. omega.
Qed.

End POSTORDER.

Definition postorder (g: graph) (root: node) :=
  WfIter.iterate _ _ transition lt_state lt_state_wf transition_decreases (init_state g root).

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.

Theorem postorder_correct:
  forall g root,
  let m := postorder g root in
  (forall x1 x2 y, m!x1 = Some y -> m!x2 = Some y -> x1 = x2)
  /\ (forall x, reachable g root x -> g!x <> None -> m!x <> None).
Proof.
(* Goal: forall (g : graph) (root : node), let m := postorder g root in and (forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2) (forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive))) *)
  intros.
(* Goal: and (forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2) (forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive))) *)
  assert (postcondition g root m).
(* Goal: postcondition g root m *)
(* Goal: and (forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2) (forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive))) *)
    unfold m. unfold postorder.
(* Goal: postcondition g root (WfIter.iterate state (PTree.t positive) transition lt_state lt_state_wf transition_decreases (init_state g root)) *)
(* Goal: and (forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2) (forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive))) *)
    apply WfIter.iterate_prop with (P := invariant g root).
(* Goal: forall (a : state) (_ : invariant g root a), match transition a with | inl b => postcondition g root b | inr a' => invariant g root a' end *)
(* Goal: invariant g root (init_state g root) *)
(* Goal: and (forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2) (forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive))) *)
    apply transition_spec.
(* Goal: invariant g root (init_state g root) *)
(* Goal: and (forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2) (forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive))) *)
    apply initial_state_spec.
(* Goal: and (forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2) (forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive))) *)
  inv H.
(* Goal: forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2 *)
(* Goal: forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive)) *)
  split. auto.
(* Goal: forall (g : graph) (root : node), let m := postorder g root in and (forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2) (forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive))) *)
  induction 1; intros.
  (* root case *)
(* Goal: forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2 *)
(* Goal: forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive)) *)
  apply ROOT; auto.
  (* succ case *)
(* Goal: forall (x1 x2 y : positive) (_ : @eq (option positive) (@PTree.get positive x1 m) (@Some positive y)) (_ : @eq (option positive) (@PTree.get positive x2 m) (@Some positive y)), @eq positive x1 x2 *)
(* Goal: forall (x : positive) (_ : reachable g root x) (_ : not (@eq (option (list node)) (@PTree.get (list node) x g) (@None (list node)))), not (@eq (option positive) (@PTree.get positive x m) (@None positive)) *)
  eapply SUCCS; eauto. apply IHreachable. congruence.
Qed.

