Set Implicit Arguments.
Require Import CFML.CFLib.
Require Import DFS_ml.
Require Import Stdlib.
Require Import TLC.LibListZ.
Require Import Array_proof.
Require Import List_proof.
Open Scope tag_scope.


Ltac auto_star ::=
  try solve [ subst; intuition eauto with maths ].


(*************************************************************************)
(** Heap contains predicate : TODO: move *)

Definition heap_contains H1 H2 :=
  exists H, H2 = H1 \* H.

Global Instance incl_inst : BagIncl hprop.
Proof. constructor. applys heap_contains. Defined.

Lemma heap_contains_intro : forall (H H1 H2 : hprop),
  (H2 ==> H1 \* H) ->
  (H1 \* H ==> H2) ->
  (H1 \c H2).
Proof using. introv M1 M2. hnf. exists H. apply* antisym_pred_incl. Qed.

Lemma heap_contains_elim : forall (H1 H2 : hprop),
  (H1 \c H2) -> exists H,
     (H2 ==> H1 \* H)
  /\ (H1 \* H ==> H2).
Proof using. introv (H&M). exists H. split*. Qed.

Global Opaque heap_contains.

(*
Search noduplicates.
Lemma noduplicates_app_inv : forall A (L1 L2 : list A),
  noduplicates (L1 ++ L2) ->
     noduplicates L1
  /\ noduplicates L2
  /\ (~ exists x, mem x L1 /\ mem x L2).
Proof using.
  introv ND. splits.
   induction L1.
    constructors.
    rew_list in ND. inverts ND as ND1 ND2. rewrite mem_app_or_eq in ND1. rew_logic* in ND1.
   induction L1.
    rew_list~ in ND.
    rew_list in ND. inverts~ ND.
   introv (x&I1&I2). induction I1; rew_list in ND.
    inverts ND as ND1 ND2. false ND1. apply* mem_app_or.
    apply IHI1. inverts~ ND.
Qed.
*)


(*************************************************************************)
(** Set of list predicate : TODO: move *)

Definition set_of_list_monoid A :=
  (monoid_make (union : _ -> _ -> set A) (\{}:set A)).

Definition set_of_list A (L : list A) :=
  LibList.fold (@set_of_list_monoid A) (fun x => \{x}) L.

Section SetOfList.
Variables (A:Type).
Implicit Types l : list A.

Lemma set_of_list_monoid_Monoid : Monoid (set_of_list_monoid A).
Proof using.
  unfold set_of_list_monoid. constructor.
  apply union_assoc.
  apply union_empty_l.
  apply union_empty_r.
Qed.
Local Hint Resolve set_of_list_monoid_Monoid.
Lemma set_of_list_nil :
  set_of_list (@nil A) = \{}.
Proof using. auto. Qed.
Lemma set_of_list_cons : forall x l,
  set_of_list (x::l) = \{x} \u (set_of_list l).
Proof using. intros. unfold set_of_list. rewrite~ fold_cons. Qed.
Lemma set_of_list_last : forall x l,
  set_of_list (l&x) = (set_of_list l) \u \{x}.
Proof using. intros. unfold set_of_list. rewrite~ fold_last. Qed.
Lemma set_of_list_app : forall l1 l2,
  set_of_list (l1 ++ l2) = (set_of_list l1) \u (set_of_list l2).
Proof using. intros. unfold set_of_list. rewrite~ fold_app. Qed.

Lemma set_of_list_mem : forall l x,
  x \in set_of_list l -> mem x l.
Proof using.
  introv. induction l; introv M.
  { false. }
  { rewrite set_of_list_cons in M. rew_set in M. destruct* M. }
Qed.
End SetOfList.

Hint Rewrite set_of_list_nil set_of_list_cons set_of_list_app
 set_of_list_last : rew_set_of_list.
Tactic Notation "rew_set_of_list" :=
  autorewrite with rew_set_of_list.
Tactic Notation "rew_set_of_list" "in" hyp(M) :=
  autorewrite with rew_set_of_list in M.
Tactic Notation "rew_set_of_list" "in" "*" :=
  autorewrite with rew_set_of_list in *.


(********************************************************************)
(* ** TODO: Should be generated *)

Instance color__inhab : Inhab color_.
Proof. typeclass. Qed.






(********************************************************************)
(********************************************************************)
(* START HERE *)
(********************************************************************)
(********************************************************************)
(* ** Representation of graphs without information on the edges *)

(** Axiomatization of a graph structure *)

Parameter graph : Type.
Parameter nodes : graph -> set int.
Parameter edges : graph -> set (int*int).

Parameter edges_in_nodes : forall (G : graph) x y,
  (x,y) \in edges G -> x \in nodes G /\ y \in nodes G.

(** Derived definition for working with graphs *)

Definition out_edges G i :=
  set_st (fun j => (i,j) \in edges G).

Definition has_edge (G:graph) x y :=
  (x,y) \in edges G.

Definition path := list (int*int).

Inductive is_path (G:graph) : int -> int -> path -> Prop :=
  | is_path_nil : forall x,
      x \in nodes G ->
      is_path G x x nil
  | is_path_cons : forall x y z p,
     has_edge G x y ->
     is_path G y z p ->
     is_path G x z ((x,y)::p).

Definition reachable (G:graph) (i j:int) :=
  exists p, is_path G i j p.



(********************************************************************)
(* ** Basic well-formedness facts on graphs *)

Lemma out_edges_has_edge : forall G i j,
  j \in out_edges G i <-> has_edge G i j.
Proof using.
  intros. unfold has_edge, out_edges. rewrite* in_set_st_eq.
Qed.

Lemma has_edge_nodes : forall (G : graph) x y,
  has_edge G x y -> x \in nodes G /\ y \in nodes G.
Proof using.
  =>> M. rewrite <- out_edges_has_edge in M. applys* edges_in_nodes.
Qed.

Lemma has_edge_in_nodes_l : forall (G : graph) x y,
  has_edge G x y -> x \in nodes G. (* trivial *)
Proof using. intros. forwards*: has_edge_nodes. Qed.

Lemma has_edge_in_nodes_r : forall (G : graph) x y,
  has_edge G x y -> y \in nodes G. (* trivial *)
Proof using. intros. forwards*: has_edge_nodes. Qed.

Lemma reachable_in_nodes_l : forall (G : graph) x y,
  reachable G x y -> x \in nodes G.
Proof using.
  =>> (p&M). destruct M. auto. applys* has_edge_in_nodes_l.
Qed.

Lemma reachable_in_nodes_r : forall (G : graph) x y,
  reachable G x y -> y \in nodes G.
Proof using. =>> (p&M). induction* M. Qed.

Lemma reachable_self : forall G i,
  i \in nodes G ->
  reachable G i i.
Proof using. intros. exists (nil:path). constructor~. Qed.

Lemma reachable_edge : forall G i j,
  has_edge G i j ->
  reachable G i j.
Proof using. (* trivial *)
  =>> M. exists ((i,j)::nil). constructor~. constructor~.
  applys* has_edge_in_nodes_r.
Qed.

Lemma reachable_trans : forall G i j k,
  reachable G i j ->
  reachable G j k ->
  reachable G i k.
Proof using. (* basic induction *)
  =>> (p1&M1) (p2&M2). exists (p1++p2).
  induction M1; rew_list.
  { auto. }
  { constructor~. }
Qed.

Lemma reachable_trans_edge : forall G i j k,
  reachable G i j ->
  has_edge G j k ->
  reachable G i k.
Proof using. (* trivial *)
  =>> M1 M2. applys* reachable_trans. applys* reachable_edge.
Qed.


(********************************************************************)
(* ** Graph representation predicate in Separation Logic: [g ~> RGraph G]*)

(** [nodes_index G n] asserts that the nodes in [G] are indexed
    from [0] inclusive to [n] exclusive. *)

Definition nodes_index (G:graph) (n:int) :=
  n >= 0 /\ (forall i, i \in nodes G <-> index n i).

(** [nodes_edges G N] asserts that [N] describes the adjacency
    lists of [G], in the sense that [N[i]] gives the list of
    neighbors of node [i] in [G]. *)

Definition nodes_edges (G:graph) (N:list(list int)) :=
  forall i, i \in nodes G ->
     set_of_list (N[i]) = out_edges G i
  /\ noduplicates (N[i]).

(** [g ~> RGraph G] asserts that at pointer [g] is an imperative
    array of pure lists that represents the adjacency lists of [G]. *)

Definition RGraph (G:graph) (g:loc) :=
  Hexists N, g ~> Array N
   \* \[   nodes_index G (LibListZ.length N)
        /\ nodes_edges G N].


(********************************************************************)
(** Basic lemmas about [RGraph] -- TODO: will be generated *)

Lemma RGraph_open : forall (g:loc) (G:graph),
  g ~> RGraph G ==>
  Hexists N, g ~> Array N
   \* \[nodes_index G (LibListZ.length N)
        /\ nodes_edges G N].
Proof using. intros. xunfolds~ RGraph. Qed.

Lemma RGraph_close : forall (g:loc) (G:graph) N,
  nodes_index G (LibListZ.length N) ->
  nodes_edges G N ->
  g ~> Array N
  ==>
  g ~> RGraph G.
Proof using. intros. xunfolds~ RGraph. Qed.

Arguments RGraph_close : clear implicits.

Hint Extern 1 (RegisterOpen (RGraph _)) =>
  Provide RGraph_open.
Hint Extern 1 (RegisterClose (Array _)) =>
  Provide RGraph_close.


(********************************************************************)
(* ** Generic hints *)

(** Hints for type-checking *)

Implicit Types G : graph.
Implicit Types i j k : int.
Implicit Types p : path.
Implicit Types C : list color_.
Implicit Types R E F : set int.

(** Hints for indices *)

Lemma nodes_index_index : forall G n m x,
  nodes_index G n -> x \in nodes G -> n = m -> index m x.
Proof. introv (E&N) Nx L. subst. rewrite~ <- N. Qed.

Hint Extern 1 (index ?n ?x) => skip.
(* TODO: for now, we skip these trivial goals
   about indices being in the bounds of the array *)

(* Hints for solving [index n x] goals automatically
Hint Resolve @index_array_length_eq @index_make @index_update.
Hint Immediate has_edge_in_nodes_l has_edge_in_nodes_r.
Hint Extern 1 (nodes_index _ _) => congruence.
Hint Extern 1 (index ?n ?x) =>
  eapply nodes_index_index;
  [ try eassumption
  | instantiate; try eassumption
  | instantiate; try congruence ].
*)



(*************************************************************************)
(** Verification of the Graph module, with the adjacency lists representation *)

Lemma nb_nodes_spec : forall (G:graph) g,
   app Graph_ml.nb_nodes [g]
    PRE (g ~> RGraph G)
    POST (fun n => g ~> RGraph G \* \[nodes_index G n]).
Proof using.
  xcf. xunfold RGraph. xpull ;=> N (HN1&HN2).
  xapp. xsimpl*.
Qed.

Hint Extern 1 (RegisterSpec Graph_ml.nb_nodes) => Provide nb_nodes_spec.

Lemma iter_edges_spec : forall (I:set int->hprop) (G:graph) g f i,
  i \in nodes G ->
  (forall L, (g ~> RGraph G) \c (I L)) ->
  (forall j E, j \notin E -> has_edge G i j ->
     (app f [j] (I E) (# I (\{j} \u E)))) ->
  app Graph_ml.iter_edges [f g i]
    PRE (I \{})
    POST (# I (out_edges G i)).
Proof.
  introv Gi Ginc Sf. xcf.
  forwards (H&HO&HC): heap_contains_elim ((rm Ginc) \{}).
  xchange (rm HO). xopen g. xpull ;=> N (GI&GN).
  forwards (GNE&GND): GN Gi. xapps~. xclose* g. xchange (rm HC).
  xfun. xapp_no_simpl (fun (L:list int) => I (set_of_list L)).
  { introv EN. rewrite set_of_list_last. xapp.
    xapp_spec Sf. (* TODO: xapp *)
    { intros M. rewrite EN in GND. (* trivial *)
      lets (_&_&N3): noduplicates_app_inv GND. applys (rm N3). (* trivial *)
      exists x. forwards*: set_of_list_mem M. } (* trivial *)
    { rewrite <- out_edges_has_edge. rewrite <- GNE. rewrite EN.  (* trivial *)
      rew_set_of_list. rew_set; eauto. } (* trivial *)
    { rewrite union_comm. xsimpl. } }
  { rew_set_of_list. xsimpl. }
  { rewrite GNE. xsimpl. }
Qed.

Hint Extern 1 (RegisterSpec Graph_ml.iter_edges) => Provide iter_edges_spec.



(********************************************************************)
(* ** Auxiliary definitions for the invariants of DFS *)

Definition evolution C C' :=
     (forall i, index C i -> C[i] = Black -> C'[i] = Black)
  /\ (forall i, index C i -> (C[i] = Gray <-> C'[i] = Gray)).

Definition no_white_in E C :=
  forall i, i \in E -> C[i] <> White.

Definition all_black_in E C :=
  forall i, i \in E -> C[i] = Black.

Definition no_gray C :=
  forall i, index C i -> C[i] <> Gray.

Definition no_black_to_white G C :=
  forall i j,
  has_edge G i j ->
  C[i] = Black ->
  C[j] <> White.

Definition reachable_from G R i :=
  exists r, r \in R /\ reachable G r i.

Definition inv G R C :=
     (nodes_index G (length C))
  /\ (no_black_to_white G C)
  /\ (forall j, j \in nodes G -> C[j] = Black -> reachable_from G R j).

  (* TODO: above, might need to maintain that [R \c nodes G]
           in order to prove facts of the form [r \in nodes G] *)

Definition hinv G R C g c :=
     g ~> RGraph G
  \* c ~> Array C
  \* \[ inv G R C ].


(********************************************************************)
(* ** Auxiliary lemmas *)

Lemma evolution_refl : refl evolution.
Proof using. (* trivial *)
  => C. splits*.
Qed.

Lemma evolution_trans : trans evolution.
Proof using. (* trivial *)
  =>> (F1&G1) (F2&G2). unfolds evolution. splits.
  autos*.
  intros. rewrite~ G1.
Qed.

Lemma evolution_write_black : forall G i C C',
  evolution (C[i := Gray]) C' ->
  C[i] = White ->
  no_white_in (out_edges G i) C' ->
  evolution C C'[i := Black].
Proof using.  (* trivial *)
  =>> (E1&E2) Ci HN. split.
  { => j Hj Ej. rew_array~. case_if~.
    { apply~ E1. rew_array~. case_if~. } }
  { => j Hj. rew_array~. case_if.
    { subst. rename j into i. iff; auto_false. }
    { rewrite~ <- E2. rew_array~. case_if*. } }
Qed.

Lemma no_white_in_evolution : forall C C' E,
  no_white_in E C ->
  evolution C C' ->
  no_white_in E C'.
Proof using.  (* trivial *)
  =>> N (H1&H2) i Hi. cases (C[i]) as Ci.
  { false* N. }
  { forwards~ (H2a&_): H2 i. rewrite~ H2a. auto_false. }
  rewrite~ H1. auto_false.
Qed.

Lemma no_gray_evolution : forall C C',
  no_gray C ->
  evolution C C' ->
  no_gray C'.
Proof using. (* trivial *)
  =>> N (H1&H2) i Hi Ci. forwards~ (_&HR): H2 i. applys~ N i.
Qed.

Lemma no_black_to_white_no_gray_elim : forall G C i j,
  no_black_to_white G C ->
  no_gray C ->
  reachable G i j ->
  C[i] = Black ->
  C[j] = Black.
Proof using.
  =>> HW HG (p&HP). induction HP; => Ci.
  (* trivial after induction *)
  { auto. }
  { applys IHHP. cases (C[y]).
    { false* HW. }
    { false* HG. }
    { auto. } }
Qed.

Lemma inv_empty : forall G n,
  nodes_index G n ->
  inv G \{} (make n White).
Proof using. (* trivial *)
  =>> Hn. splits.
  { hnf in Hn. rew_array*. auto. (* TODO: fix tactic *) }
  { =>> Hi Ci. false. rew_array~ in Ci. false. }
  { => i Hi Ci. false. rew_array~ in Ci. false. }
Qed.

Lemma inv_add_root : forall G L C i,
  inv G (set_of_list L) C ->
  inv G ('{i} \u set_of_list L) C.
Proof using. (* trivial *)
  =>> (I1&I2&I3). splits.
  { auto. }
  { auto. }
  { => j Hj Cj. forwards~ (r&Hr&Pr): I3 j.
    exists* r. splits*. rew_set. eauto. (* TODO: tactic *) }
Qed.

Lemma inv_gray_root : forall G R C i,
  C[i] = White ->
  i \in nodes G ->
  inv G R C ->
  inv G R (C[i := Gray]).
Proof using. (* trivial *)
  =>> Ci Hi (I1&I2&I3). splits.
  { rew_array~. }
  { => j k Hjk. rew_array~. => Cjk. case_if; auto_false.
   case_if. applys* I2. }
  { => j Hj. rew_array~. case_if; auto_false. }
Qed.

Lemma inv_evolution_black : forall G R C' i,
  inv G R C' ->
  reachable_from G R i ->
  no_white_in (out_edges G i) C' ->
  inv G R (C'[i := Black]).
Proof using.  (* trivial *)
  =>> (I1&I2&I3) Ri Wi. splits.
  { rew_array~. }
  { => j k Hjk. rew_array~. => M. case_if; auto_false. case_if.
    { subst. applys Wi. rewrite~ out_edges_has_edge. }
    { applys* I2. } }
  { => j Hj. rew_array~. case_if; [subst|auto].
    => _. rename j into i. eauto. }
Qed.


(*************************************************************************)
(** Verification of DFS *)

Lemma dfs_from_spec : forall G R C g c i,
  reachable_from G R i ->
  C[i] = White ->
  app dfs_from [g c i]
    PRE (hinv G R C g c)
    POST (# Hexists C', hinv G R C' g c
       \* \[ evolution C C' /\ C'[i] = Black ]).
Proof using.
  skip_goal IH. hide IH. (* TODO: set up the decreasing measure to prove termination *)
  => G R C0. =>> Ri Wi.
  asserts Hi: (i \in nodes G).
    { destruct Ri as (r&Hr&Mr). applys* reachable_in_nodes_r. } (* trivial *)
  xcf. unfold hinv. xpull ;=> HI. xapps~. sets_eq C1: (C0[i:=Gray]).
  xfun as f. set (loop_inv := fun L C => hinv G R C g c
         \* \[ evolution C1 C /\ no_white_in L C ]).
  xseq. xapp_no_simpl (>> (fun L => Hexists C, loop_inv L C) G).
  { auto. }
  { => L. unfold loop_inv, hinv. applys heap_contains_intro
    (Hexists C, c ~> Array C \* \[ inv G R C] \*  (* ideally, should be computed *)
     \[ evolution C1 C /\ no_white_in L C]); xsimpl~. }
  { => j js Hj Eij. unfold loop_inv, hinv.
    xpull ;=> C I0 (H1&H2). xapp. clears f.
    xapps~. xapps~. xpolymorphic_eq.
    xpost (Hexists C', hinv G R C' g c
         \* \[ evolution C1 C' /\ no_white_in js C' /\ C'[j] <> White ]).
    { xif.
      { show IH. xapply (>> IH G R C).
        { destruct Ri as (r&Pr&Mr). exists r. split~. (* trivial *)
          applys* reachable_trans_edge. } (* trivial *)
        { auto. } (* trivial *)
        { unfold hinv. xsimpl~. }
        unfold hinv. xpull ;=> C' I1 (F1&F2). xsimpl. splits.
        { applys* evolution_trans. }
        { applys* no_white_in_evolution. } (* trivial *)
        { auto_false. }  (* trivial *)
        { auto. } } (* trivial *)
      { xret. unfold hinv. xsimpl~. } }
    { unfold hinv. xpull ;=> C' I1 (F1&F2&F3). xsimpl. splits.
      { auto. } (* trivial *)
      { => k Hk. rew_set in Hk. destruct~ Hk. subst~. } (* trivial *)
      { auto. } } } (* trivial *)
  { clears f. unfold loop_inv, hinv. xsimpl. split.
    { applys evolution_refl. }
    { => j Hj. rew_array~. } (* trivial *)
    { subst C1. applys* inv_gray_root. } }
  { unfold loop_inv, hinv. xpull ;=> C' I1 (F1&F2).
    xapps~. xsimpl. split.
    { subst C1. applys* evolution_write_black. }
    { rew_array~. case_if~. } (* trivial *)
    { applys* inv_evolution_black. } }
Qed.

Hint Extern 1 (RegisterSpec dfs_from) => Provide dfs_from_spec.

Lemma dfs_main_spec : forall (G:graph) g (rs:list int),
  app dfs_main [g rs]
    PRE (g ~> RGraph G)
    POST (fun c => Hexists C,
      c ~> Array C \*
      g ~> RGraph G \*
      \[ forall i, i \in nodes G ->
         (C[i] = Black <-> exists r, r \in set_of_list rs /\ reachable G r i)]).
Proof using.
  xcf. xapp. => Hn. xapp.
  { applys (proj1 Hn). } (* trivial *)
  => C0 HC0.
  asserts N0: (no_gray C0). { subst. => i Hi. rew_array; auto_false. } (* trivial *)
  xfun as f.
  set (loop_inv := fun L C => hinv G (set_of_list L) C g c
         \* \[ evolution C0 C /\ all_black_in (set_of_list L) C ]).
  xapp (fun L => Hexists C, loop_inv L C).
  { => i L T HL. lets (_&Hi): (proj2 Hn) i.
    unfold loop_inv, hinv. xpull ;=> C HI (HC1&HC2).
    xapp. clears f. xapps~. xapps~. xpolymorphic_eq. xif.
    { xapp G (\{i} \u set_of_list L) C.
      { exists i. split.
        { rew_set; eauto. } (* TODO: tactic *)
        { applys* reachable_self. } } (* trivial *)
      { auto. } (* trivial *)
      { unfold hinv. xsimpl*. applys* inv_add_root. }
      { unfold loop_inv, hinv. intros u. xpull ;=> C' I1 (F1&F2).
        rew_set_of_list. xsimpl.
        { splits. (* trivial *)
          { applys~ evolution_trans F1. } (* trivial *)
          { => j Hj. rew_set in Hj. destruct Hj. (* trivial *)
           { applys~ (proj1 F1). } { subst~. } } } (* trivial *)
        { rewrite~ union_comm. } } } (* trivial *)
    { xret. unfold loop_inv, hinv. rew_set_of_list. xsimpl~. split.
      { auto. } (* trivial *)
      { => j Hj. rew_set in Hj. destruct Hj.
        { cases (C[i]); auto_false. } (* trivial *)
        { subst. cases (C[i]); auto_false.  (* TODO: cleanup here *)
          false~ N0 i. forwards* (_&?): (proj2 HC1). } } (* trivial *)
      { cases~ (C[i]). (* trivial *)
        { false. } (* trivial *)
        { false~ N0 i. forwards~ (?&?): (proj2 HC1) i. } (* trivial *)
        { rewrite~ union_comm. applys* inv_add_root. } } } }
    { unfold loop_inv, hinv. rew_set_of_list. xsimpl. split.
      { applys* evolution_refl. } (* trivial *)
      { => r Hr. rew_set in Hr. false. } (* trivial *)
      { subst C0. applys* inv_empty. } } (* trivial *)
  unfold loop_inv, hinv. => C1. xpull ;=> (I1&I2&I3) (H1&H2).
  xret. xsimpl. split.
  { => M. applys~ I3. } (* trivial *)
  { => (r&Hr&Mr). applys* no_black_to_white_no_gray_elim.
    applys* no_gray_evolution. }
Qed.


Hint Extern 1 (RegisterSpec dfs_main) => Provide dfs_main_spec.