proof

examples/DFS/DFS_proof.v

@@ -2,11 +2,19 @@ Set Implicit Arguments.
 Require Import CFLib.
 Require Import DFS_ml.
 Require Import Stdlib.
+Require Import LibListZ.
+Require Import Array_proof.
+Require Import List_proof.
 Open Scope tag_scope.
 Ltac auto_star ::= subst; intuition eauto with maths.
 
 
 
+(********************************************************************)
+(* ** TODO: Should be generated *)
+
+Instance color__inhab : Inhab color_.
+Proof. typeclass. Qed.
 
 
 
@@ -14,7 +22,7 @@ Ltac auto_star ::= subst; intuition eauto with maths.
 (********************************************************************)
 (* ** TLC Graph without information on edges *)
 
-Parameter graph : Type -> Type.
+Parameter graph : Type.
 Parameter nodes : graph -> set int.
 Parameter edges : graph -> set (int*int).
 
@@ -35,6 +43,8 @@ Lemma has_edge_in_nodes_r : forall (G : graph) x y,
 Proof using. intros. forwards*: has_edge_nodes. Qed.
 
 
+Definition path := list (int*int).
+
 Inductive is_path (G:graph) : int -> int -> path -> Prop :=
   | is_path_nil : forall x, 
       x \in nodes G ->
@@ -45,16 +55,22 @@ Inductive is_path (G:graph) : int -> int -> path -> Prop :=
      is_path G x z ((x,y)::p).
 
 Definition reachable (G:graph) (i j:int) :=
-  exists p, path G i j p.
+  exists p, is_path G i j p.
 
 Definition reachables (G:graph) (E F:set int) :=
-  forall j, j \in F -> exists i, i in E, reachable G i j.
+  forall j, j \in F -> exists i, i \in E /\ reachable G i j.
 
 
 
 (********************************************************************)
 (* ** Facts *)
 
+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.
+
 Lemma reachable_edge : forall G i j,
   has_edge G i j -> 
   reachable G i j.
@@ -63,8 +79,8 @@ Proof using.
 Qed.
  
 Lemma reachable_trans : forall G i j k,
-  reachable G i j.
-  reachable G j k.
+  reachable G i j ->
+  reachable G j k ->
   reachable G i k.
 Proof using.
   skip.
@@ -91,20 +107,22 @@ Qed.
 Definition no_black_to_while G C := 
   forall i j, 
   has_edge G i j -> 
-  C[i] = Black -> 
+  C[i] = Black ->
   C[j] <> White.
     (* i \in blacks C -> j \in (blacks C \u grays C). *)
     (* i \in blacks C -> j \in (blacks C) \/ j \in grays C). *)
 
-
-Lemma black_to_while_path_goes_through_gray : forall G C,
+Lemma black_to_white_path_goes_through_gray : forall G C,
   no_black_to_while G C ->
   forall i j p, 
-  path G i j p -> 
+  is_path G i j p -> 
   C[i] = Black -> (*i \in blacks C *)
   C[i] = White -> (*i \notin (blacks C \u grays C) *)
-  exists k, k \in p /\ C[k] = Gray. (* TODO: what exactly do we need about k? *)
-
+  exists i' j', Mem (i',j') p /\ C[i'] = Gray /\ C[j'] = White. 
+    (* TODO: what exactly do we need about i' and j'? *)
+Proof using.
+  skip.
+Qed.
 
 
 (********************************************************************)
@@ -114,15 +132,15 @@ Lemma black_to_while_path_goes_through_gray : forall G C,
 (** [nodes_index G n] holds if the nodes in [G] are indexed from
     [0] inclusive to [n] exclusive. *)
 
-Definition nodes_index A (G:graph A) (n:int) :=
+Definition nodes_index (G:graph) (n:int) :=
   forall i, i \in nodes G = index n i.
 
 (** [g ~> GraphAdj G] asserts that at pointer [g] is an imperative
     array of pure lists that represents the adjacency lists of [G]. *)
 
-Definition GraphAdj A (G:graph A) (g:loc) :=
+Definition GraphAdj (G:graph) (g:loc) :=
   Hexists N, g ~> Array N
-   \* \[nodes_index G (LibArray.length N) 
+   \* \[nodes_index G (LibListZ.length N) 
    /\ forall i j, i \in nodes G -> 
         Mem j (N[i]) = has_edge G i j].
 
@@ -139,10 +157,11 @@ Hint Resolve Forall_last.
 
 (** Hints for indices *)
 
-Lemma graph_adj_index : forall B (G:graph B) n m x,
+Lemma graph_adj_index : forall (G:graph) n m x,
   nodes_index G n -> x \in nodes G -> n = m -> index m x.
 Proof. introv N Nx L. subst. rewrite~ <- N. Qed.
 
+(*
 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.
@@ -151,109 +170,147 @@ Hint Extern 1 (index ?n ?x) =>
   [ try eassumption 
   | instantiate; try eassumption
   | instantiate; try congruence ].
+*)
+Hint Extern 1 (nodes_index _ _) => skip. (* TODO *)
+Hint Extern 1 (index ?n ?x) => skip. (* TODO *)
 
 
 
+(*************************************************************************)
+(** Set of list predicate : TODO: move *)
+
+Definition set_of_list A (L : list A) :=
+  LibList.fold (monoid_ (union : _ -> _ -> set A) (\{}:set A)) (fun x => \{x}) L.
+
+Section SetOfList.
+Variables (A:Type).
+Implicit Types l : list A.
+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. skip. (* TODO *) Qed.
+
+(*
+Lemma fold_app : forall l1 l2,
+  Monoid m ->
+  fold m f (l1 ++ l2) = monoid_oper m (fold m f l1) (fold m f l2).
+Proof using.
+  unfold fold. intros. rewrite fold_right_app. gen l2.
+  induction l1; intros.
+  repeat rewrite fold_right_nil. rewrite~ monoid_neutral_l.
+  repeat rewrite fold_right_cons. rewrite <- monoid_assoc. fequals.
+Qed.
+Lemma fold_last : forall x l,
+  Monoid m ->
+  fold m f (l & x) = monoid_oper m (fold m f l) (f x).
+Proof using.
+  intros. rewrite~ fold_app. rewrite fold_cons.
+  rewrite fold_nil. rewrite monoid_neutral_r. auto.
+Qed.
+*)
+End SetOfList.
+
+
 
 (*************************************************************************)
 (** Graph representation by adjacency lists *)
 
+(* Import Graph_ml. *)
 
-Lemma nb_nodes_spec : forall (G:graph),
-  app_keep nb_nodes [g] 
+Lemma nb_nodes_spec : forall (G:graph) g,
+  app Graph_ml.nb_nodes [g]
     PRE (g ~> GraphAdj G) 
     POST (fun n => \[nodes_index G n]).
-
 Proof using.
-  xcf. instantiate (1:=A). (* todo: fix instantiation *)
-  intros. unfold GraphAdj. hdata_simpl.
-  xextract as N [GI GN]. xapp. hsimpl~. 
-Admitted. (*faster*)
-
-Hint Extern 1 (RegisterSpec nb_nodes) => Provide nb_nodes_spec.
-
-Lemma iter_edges_spec : forall (I:set int->hprop) (G:graph) g f,
-  (forall i, i \in nodes G ->
-    (forall j js, j \notin js -> has_edge G i j -> 
-      (app f j (I js) (# I (\{j} \u js)))) -> 
-  app iter_edges [f g]
-    PRE (g ~> GraphAdj G \* I \{}) 
-    POST (# g ~> GraphAdj G \* I (out_edges_target G i)).
-Proof.
-(*---TODO---
-  xcf. introv Gi Sf. (* todo: fix instantiation *)
-  unfold GraphAdj. hdata_simpl. xextract as N [GI GN]. 
-  xfun_mg. xapps*.
-  xapp_spec ml_list_iter_spec' (fun l:list(int*unit) => I (List.map fst l)).
-  intros [j w] t. simpls. eapply S_f0. 
-  intros_all. applys H0. applys H. (* todo: xbody/xisspec *)
-  clear j w. intros [j w]. xcase. 
-  --- TODO ---*)
-Admitted. 
-
-Hint Extern 1 (RegisterSpec iter_edges_target_of) => Provide iter_edges_target_of_spec.
-
-
-Lemma iter_nodes_spec : forall (I:set int->hprop) (G:graph) g f,
-  (forall i N, i \in nodes G -> i \notin N ->
-     (app f [i] (I N) (# I (\{i}\u N)))) -> 
-  app iter_nodes [f g]
+  xcf. xunfold GraphAdj. 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 j js, j \notin js -> has_edge G i j -> 
+     (app f [j] (I js) (# I (\{j} \u js)))) -> 
+  app Graph_ml.iter_edges [f g i]
     PRE (g ~> GraphAdj G \* I \{}) 
-    POST (# g ~> GraphAdj G \* I (nodes G)).
+    POST (# g ~> GraphAdj G \* I (out_edges G i)).
 Proof.
-  (* -- TODO -- *)
-Admitted. 
+  introv Gi Sf. xcf. xunfold GraphAdj. xpull ;=> N (GI&GN).
+  xapps~. xfun. xapp (fun (L:list int) => I (set_of_list L)).
+  { introv EN. rewrite set_of_list_last. xapp. xapp.
+    { skip. (* needs no duplicate *) }
+    { rewrite~ <- GN. rewrite EN. skip. (* mem *) }
+    { xsimpl. }
+    { rewrite union_comm. xsimpl. } }
+  { xsimpl.
+    { skip. (* set_of_list // out_edges *) }
+    { split~. } }
+Qed. 
+   
+Hint Extern 1 (RegisterSpec Graph_ml.iter_edges) => Provide iter_edges_spec.
 
-Hint Extern 1 (RegisterSpec iter_nodes) => Provide iter_nodes_spec.
 
 
 
 (*************************************************************************)
 (** DFS *)
 
-Parameter set_of_list : forall A, list A -> set A.
-
+(* TODO / FIX
+Open Scope set_scope.
+Notation "\aset{ x : A | P }" := (@set_st A (fun x => P))
+ (at level 0, x ident, A at level 0, P at level 200) : set_scope.
+*)
 
 Definition blacks C :=
-  \set{ i:int | index i C /\ C[i] = Black }.
+  set_st (fun i:int => index C i /\ C[i] = Black).
+  (* \set{ i:int | index C i /\ C[i] = Black }. *)
 
 Definition grays C :=
-  \set{ i:int | index i C /\ C[i] = Gray }.
+  set_st (fun i:int => index C i /\ C[i] = Gray).
+
 
 Definition inv G R C :=
-     length C = nb_nodes G
+     length C = card (nodes G)
   /\ R \c nodes G
   /\ no_black_to_while G C
-  /\ reachables (R \u blacks C) (blacks C).
+  /\ reachables G (R \u blacks C) (blacks C).
 
-Definition hinv G C :=
+Definition hinv G R C g c :=
      g ~> GraphAdj G 
-  \* c ~> Array C
-  \* \[ inv G C ].
+  \* c ~> Array C
+  \* \[ inv G R C ].
 
-Lemma dfs_from_spec : forall (R:set int) (G:graph) C g c i,
+Lemma dfs_from_spec : forall G R C g c i,
   C[i] = White ->
-  app_keep dfs_from [g c i] 
-    PRE (hinv G R C) 
-    POST (# Hexists C', hinv G R C'
-       \* \[ C'[x] = Black
+  app dfs_from [g c i]
+    PRE (hinv G R C g c) 
+    POST (# Hexists C', hinv G R C' g c
+       \* \[ C'[i] = Black
           /\ (blacks C) \c (blacks C') ]).
 Proof using.
-
+  xcf. skip.
 Qed.
 
 Hint Extern 1 (RegisterSpec dfs_from) => Provide dfs_from_spec.
 
 Lemma dfs_main_spec : forall (G:graph) g (r:list int),
-  app_keep dfs_main [g r] 
+  app dfs_main [g r] 
     PRE (g ~> GraphAdj G) 
     POST (fun c => Hexists C,
       c ~> Array C \* 
-      \[ reachables G (set_of_list r) (blacks c) ])
-Proof using.
-
+      g ~> GraphAdj G \*
+      \[ reachables G (set_of_list r) (blacks C) ]).
+Proof using.  
+  xcf. skip. (* xunfold GraphAdj at 1. xpull ;=> HI. *)
+  
 Qed.
-      
+
 Hint Extern 1 (RegisterSpec dfs_main) => Provide dfs_main_spec.
 
 
@@ -262,3 +319,36 @@ Hint Extern 1 (RegisterSpec dfs_main) => Provide dfs_main_spec.
 
 
 
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+

examples/DFS/Makefile

 
 # Possible to define "ML" to be the list of source files to consider
 
+ML := DFS.ml
 
 include ../Makefile.example
 

examples/DFS/OtherAlgo.ml

 
+Lemma iter_nodes_spec : forall (I:set int->hprop) (G:graph) g f,
+  (forall i N, i \in nodes G -> i \notin N ->
+     (app f [i] (I N) (# I (\{i}\u N)))) -> 
+  app iter_nodes [f g]
+    PRE (g ~> GraphAdj G \* I \{}) 
+    POST (# g ~> GraphAdj G \* I (nodes G)).
+Proof.
+  (* -- TODO -- *)
+Admitted. 
+
+Hint Extern 1 (RegisterSpec iter_nodes) => Provide iter_nodes_spec.
+
+
 
 (*
 let iter_nodes (f:int->unit) (g:t) =