DFS_proof.v 19.1 KB
Newer Older
charguer's avatar
init  
charguer committed
1
Set Implicit Arguments.
charguer's avatar
charguer committed
2
Require Import CFML.CFLib.
charguer's avatar
charguer committed
3 4
Require Import DFS_ml.
Require Import Stdlib.
charguer's avatar
charguer committed
5
Require Import TLC.LibListZ.
charguer's avatar
proof  
charguer committed
6 7
Require Import Array_proof.
Require Import List_proof.
charguer's avatar
charguer committed
8
Open Scope tag_scope.
charguer's avatar
charguer committed
9

charguer's avatar
charguer committed
10

charguer's avatar
charguer committed
11
Ltac auto_star ::=
charguer's avatar
charguer committed
12
  try solve [ subst; intuition eauto with maths ].
charguer's avatar
init  
charguer committed
13 14


charguer's avatar
charguer committed
15 16
(*************************************************************************)
(** Heap contains predicate : TODO: move *)
charguer's avatar
init  
charguer committed
17

charguer's avatar
charguer committed
18 19 20 21 22 23
Definition heap_contains H1 H2 :=
  exists H, H2 = H1 \* H.

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

charguer's avatar
charguer committed
24
Lemma heap_contains_intro : forall (H H1 H2 : hprop),
charguer's avatar
charguer committed
25 26 27
  (H2 ==> H1 \* H) ->
  (H1 \* H ==> H2) ->
  (H1 \c H2).
charguer's avatar
charguer committed
28
Proof using. introv M1 M2. hnf. exists H. apply* antisym_pred_incl. Qed.
charguer's avatar
charguer committed
29

charguer's avatar
charguer committed
30
Lemma heap_contains_elim : forall (H1 H2 : hprop),
charguer's avatar
charguer committed
31
  (H1 \c H2) -> exists H,
charguer's avatar
charguer committed
32
     (H2 ==> H1 \* H)
charguer's avatar
charguer committed
33 34 35 36 37
  /\ (H1 \* H ==> H2).
Proof using. introv (H&M). exists H. split*. Qed.

Global Opaque heap_contains.

charguer's avatar
charguer committed
38 39 40 41 42 43 44
(*
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).
charguer's avatar
charguer committed
45 46 47 48
Proof using.
  introv ND. splits.
   induction L1.
    constructors.
charguer's avatar
charguer committed
49
    rew_list in ND. inverts ND as ND1 ND2. rewrite mem_app_or_eq in ND1. rew_logic* in ND1.
charguer's avatar
charguer committed
50 51 52 53
   induction L1.
    rew_list~ in ND.
    rew_list in ND. inverts~ ND.
   introv (x&I1&I2). induction I1; rew_list in ND.
charguer's avatar
charguer committed
54
    inverts ND as ND1 ND2. false ND1. apply* mem_app_or.
charguer's avatar
charguer committed
55 56
    apply IHI1. inverts~ ND.
Qed.
charguer's avatar
charguer committed
57
*)
charguer's avatar
charguer committed
58 59 60 61 62 63


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

Definition set_of_list_monoid A :=
charguer's avatar
charguer committed
64
  (monoid_make (union : _ -> _ -> set A) (\{}:set A)).
charguer's avatar
charguer committed
65 66 67

Definition set_of_list A (L : list A) :=
  LibList.fold (@set_of_list_monoid A) (fun x => \{x}) L.
charguer's avatar
charguer committed
68

charguer's avatar
charguer committed
69 70 71 72 73 74 75 76 77 78 79 80
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.
charguer's avatar
charguer committed
81
Lemma set_of_list_nil :
charguer's avatar
charguer committed
82 83 84 85 86 87 88 89 90 91 92 93
  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.

charguer's avatar
charguer committed
94 95
Lemma set_of_list_mem : forall l x,
  x \in set_of_list l -> mem x l.
charguer's avatar
charguer committed
96 97 98
Proof using.
  introv. induction l; introv M.
  { false. }
charguer's avatar
charguer committed
99
  { rewrite set_of_list_cons in M. rew_set in M. destruct* M. }
charguer's avatar
charguer committed
100 101 102 103 104 105 106 107 108 109 110 111 112
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 *.


charguer's avatar
proof  
charguer committed
113 114 115 116 117
(********************************************************************)
(* ** TODO: Should be generated *)

Instance color__inhab : Inhab color_.
Proof. typeclass. Qed.
charguer's avatar
init  
charguer committed
118 119 120



charguer's avatar
charguer committed
121 122 123 124 125 126 127



(********************************************************************)
(********************************************************************)
(* START HERE *)
(********************************************************************)
charguer's avatar
init  
charguer committed
128
(********************************************************************)
charguer's avatar
charguer committed
129 130 131
(* ** Representation of graphs without information on the edges *)

(** Axiomatization of a graph structure *)
charguer's avatar
init  
charguer committed
132

charguer's avatar
proof  
charguer committed
133
Parameter graph : Type.
charguer's avatar
charguer committed
134 135
Parameter nodes : graph -> set int.
Parameter edges : graph -> set (int*int).
charguer's avatar
init  
charguer committed
136

charguer's avatar
charguer committed
137 138 139 140 141
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 *)

charguer's avatar
charguer committed
142
Definition out_edges G i :=
charguer's avatar
charguer committed
143
  set_st (fun j => (i,j) \in edges G).
charguer's avatar
init  
charguer committed
144

charguer's avatar
charguer committed
145 146
Definition has_edge (G:graph) x y :=
  (x,y) \in edges G.
charguer's avatar
init  
charguer committed
147

charguer's avatar
proof  
charguer committed
148 149
Definition path := list (int*int).

charguer's avatar
charguer committed
150
Inductive is_path (G:graph) : int -> int -> path -> Prop :=
charguer's avatar
charguer committed
151
  | is_path_nil : forall x,
charguer's avatar
charguer committed
152 153 154 155 156 157
      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).
charguer's avatar
init  
charguer committed
158

charguer's avatar
charguer committed
159
Definition reachable (G:graph) (i j:int) :=
charguer's avatar
proof  
charguer committed
160
  exists p, is_path G i j p.
charguer's avatar
init  
charguer committed
161 162 163



charguer's avatar
DFS_ok  
charguer committed
164
(********************************************************************)
charguer's avatar
charguer committed
165 166
(* ** Basic well-formedness facts on graphs *)

charguer's avatar
charguer committed
167
Lemma out_edges_has_edge : forall G i j,
charguer's avatar
charguer committed
168
  j \in out_edges G i <-> has_edge G i j.
charguer's avatar
charguer committed
169 170
Proof using.
  intros. unfold has_edge, out_edges. rewrite* in_set_st_eq.
charguer's avatar
charguer committed
171 172 173 174 175 176 177
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.
charguer's avatar
DFS_ok  
charguer committed
178 179 180 181 182 183 184 185 186 187 188 189

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.
charguer's avatar
charguer committed
190
  =>> (p&M). destruct M. auto. applys* has_edge_in_nodes_l.
charguer's avatar
DFS_ok  
charguer committed
191 192 193 194 195
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.
charguer's avatar
init  
charguer committed
196

charguer's avatar
charguer committed
197
Lemma reachable_self : forall G i,
charguer's avatar
charguer committed
198 199
  i \in nodes G ->
  reachable G i i.
charguer's avatar
charguer committed
200
Proof using. intros. exists (nil:path). constructor~. Qed.
charguer's avatar
charguer committed
201 202

Lemma reachable_edge : forall G i j,
charguer's avatar
charguer committed
203
  has_edge G i j ->
charguer's avatar
charguer committed
204 205 206 207 208
  reachable G i j.
Proof using. (* trivial *)
  =>> M. exists ((i,j)::nil). constructor~. constructor~.
  applys* has_edge_in_nodes_r.
Qed.
charguer's avatar
charguer committed
209

charguer's avatar
charguer committed
210 211 212 213 214 215 216 217
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. }
charguer's avatar
charguer committed
218
  { constructor~. }
charguer's avatar
charguer committed
219
Qed.
charguer's avatar
init  
charguer committed
220

charguer's avatar
charguer committed
221 222
Lemma reachable_trans_edge : forall G i j k,
  reachable G i j ->
charguer's avatar
charguer committed
223
  has_edge G j k ->
charguer's avatar
charguer committed
224 225
  reachable G i k.
Proof using. (* trivial *)
charguer's avatar
charguer committed
226
  =>> M1 M2. applys* reachable_trans. applys* reachable_edge.
charguer's avatar
charguer committed
227
Qed.
charguer's avatar
charguer committed
228

charguer's avatar
charguer committed
229

charguer's avatar
init  
charguer committed
230
(********************************************************************)
charguer's avatar
charguer committed
231
(* ** Graph representation predicate in Separation Logic: [g ~> RGraph G]*)
charguer's avatar
charguer committed
232

charguer's avatar
charguer committed
233
(** [nodes_index G n] asserts that the nodes in [G] are indexed
charguer's avatar
charguer committed
234
    from [0] inclusive to [n] exclusive. *)
charguer's avatar
init  
charguer committed
235

charguer's avatar
proof  
charguer committed
236
Definition nodes_index (G:graph) (n:int) :=
charguer's avatar
charguer committed
237 238
  n >= 0 /\ (forall i, i \in nodes G <-> index n i).

charguer's avatar
charguer committed
239
(** [nodes_edges G N] asserts that [N] describes the adjacency
charguer's avatar
charguer committed
240 241 242 243
    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)) :=
charguer's avatar
charguer committed
244
  forall i, i \in nodes G ->
charguer's avatar
charguer committed
245
     set_of_list (N[i]) = out_edges G i
charguer's avatar
charguer committed
246
  /\ noduplicates (N[i]).
charguer's avatar
init  
charguer committed
247

charguer's avatar
charguer committed
248
(** [g ~> RGraph G] asserts that at pointer [g] is an imperative
charguer's avatar
init  
charguer committed
249 250
    array of pure lists that represents the adjacency lists of [G]. *)

charguer's avatar
charguer committed
251 252
Definition RGraph (G:graph) (g:loc) :=
  Hexists N, g ~> Array N
charguer's avatar
charguer committed
253
   \* \[   nodes_index G (LibListZ.length N)
charguer's avatar
charguer committed
254 255
        /\ nodes_edges G N].

charguer's avatar
charguer committed
256

charguer's avatar
charguer committed
257 258
(********************************************************************)
(** Basic lemmas about [RGraph] -- TODO: will be generated *)
charguer's avatar
charguer committed
259 260

Lemma RGraph_open : forall (g:loc) (G:graph),
charguer's avatar
charguer committed
261
  g ~> RGraph G ==>
charguer's avatar
init  
charguer committed
262
  Hexists N, g ~> Array N
charguer's avatar
charguer committed
263
   \* \[nodes_index G (LibListZ.length N)
charguer's avatar
charguer committed
264
        /\ nodes_edges G N].
charguer's avatar
charguer committed
265 266 267 268
Proof using. intros. xunfolds~ RGraph. Qed.

Lemma RGraph_close : forall (g:loc) (G:graph) N,
  nodes_index G (LibListZ.length N) ->
charguer's avatar
charguer committed
269
  nodes_edges G N ->
charguer's avatar
charguer committed
270
  g ~> Array N
charguer's avatar
charguer committed
271
  ==>
charguer's avatar
charguer committed
272 273 274
  g ~> RGraph G.
Proof using. intros. xunfolds~ RGraph. Qed.

charguer's avatar
charguer committed
275
Arguments RGraph_close : clear implicits.
charguer's avatar
charguer committed
276

charguer's avatar
charguer committed
277
Hint Extern 1 (RegisterOpen (RGraph _)) =>
charguer's avatar
charguer committed
278
  Provide RGraph_open.
charguer's avatar
charguer committed
279
Hint Extern 1 (RegisterClose (Array _)) =>
charguer's avatar
charguer committed
280 281
  Provide RGraph_close.

charguer's avatar
charguer committed
282

charguer's avatar
init  
charguer committed
283 284 285
(********************************************************************)
(* ** Generic hints *)

charguer's avatar
charguer committed
286
(** Hints for type-checking *)
charguer's avatar
init  
charguer committed
287

charguer's avatar
charguer committed
288 289 290 291 292
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.
charguer's avatar
init  
charguer committed
293 294 295

(** Hints for indices *)

charguer's avatar
charguer committed
296
Lemma nodes_index_index : forall G n m x,
charguer's avatar
init  
charguer committed
297
  nodes_index G n -> x \in nodes G -> n = m -> index m x.
charguer's avatar
DFS_ok  
charguer committed
298
Proof. introv (E&N) Nx L. subst. rewrite~ <- N. Qed.
charguer's avatar
init  
charguer committed
299

charguer's avatar
charguer committed
300 301 302 303 304
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
charguer's avatar
init  
charguer committed
305 306 307 308
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) =>
charguer's avatar
charguer committed
309 310
  eapply nodes_index_index;
  [ try eassumption
charguer's avatar
init  
charguer committed
311 312
  | instantiate; try eassumption
  | instantiate; try congruence ].
charguer's avatar
proof  
charguer committed
313
*)
charguer's avatar
init  
charguer committed
314 315 316



charguer's avatar
charguer committed
317 318
(*************************************************************************)
(** Verification of the Graph module, with the adjacency lists representation *)
charguer's avatar
charguer committed
319

charguer's avatar
charguer committed
320 321
Lemma nb_nodes_spec : forall (G:graph) g,
   app Graph_ml.nb_nodes [g]
charguer's avatar
charguer committed
322
    PRE (g ~> RGraph G)
charguer's avatar
charguer committed
323
    POST (fun n => g ~> RGraph G \* \[nodes_index G n]).
charguer's avatar
charguer committed
324
Proof using.
charguer's avatar
charguer committed
325 326 327
  xcf. xunfold RGraph. xpull ;=> N (HN1&HN2).
  xapp. xsimpl*.
Qed.
charguer's avatar
charguer committed
328

charguer's avatar
charguer committed
329
Hint Extern 1 (RegisterSpec Graph_ml.nb_nodes) => Provide nb_nodes_spec.
charguer's avatar
charguer committed
330

charguer's avatar
charguer committed
331 332 333
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)) ->
charguer's avatar
charguer committed
334 335
  (forall j E, j \notin E -> has_edge G i j ->
     (app f [j] (I E) (# I (\{j} \u E)))) ->
charguer's avatar
charguer committed
336
  app Graph_ml.iter_edges [f g i]
charguer's avatar
charguer committed
337
    PRE (I \{})
charguer's avatar
charguer committed
338 339 340 341 342
    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).
charguer's avatar
charguer committed
343
  forwards (GNE&GND): GN Gi. xapps~. xclose* g. xchange (rm HC).
charguer's avatar
charguer committed
344
  xfun. xapp_no_simpl (fun (L:list int) => I (set_of_list L)).
charguer's avatar
charguer committed
345 346
  { introv EN. rewrite set_of_list_last. xapp.
    xapp_spec Sf. (* TODO: xapp *)
charguer's avatar
charguer committed
347
    { intros M. rewrite EN in GND. (* trivial *)
charguer's avatar
charguer committed
348 349
      lets (_&_&N3): noduplicates_app_inv GND. applys (rm N3). (* trivial *)
      exists x. forwards*: set_of_list_mem M. } (* trivial *)
charguer's avatar
charguer committed
350
    { rewrite <- out_edges_has_edge. rewrite <- GNE. rewrite EN.  (* trivial *)
charguer's avatar
charguer committed
351
      rew_set_of_list. rew_set; eauto. } (* trivial *)
charguer's avatar
charguer committed
352 353 354
    { rewrite union_comm. xsimpl. } }
  { rew_set_of_list. xsimpl. }
  { rewrite GNE. xsimpl. }
charguer's avatar
charguer committed
355
Qed.
charguer's avatar
charguer committed
356

charguer's avatar
charguer committed
357
Hint Extern 1 (RegisterSpec Graph_ml.iter_edges) => Provide iter_edges_spec.
charguer's avatar
charguer committed
358

charguer's avatar
charguer committed
359 360


charguer's avatar
charguer committed
361 362 363 364 365 366
(********************************************************************)
(* ** 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)).
charguer's avatar
charguer committed
367 368 369 370 371 372 373 374 375 376

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.

charguer's avatar
charguer committed
377 378 379
Definition no_black_to_white G C :=
  forall i j,
  has_edge G i j ->
charguer's avatar
charguer committed
380 381 382
  C[i] = Black ->
  C[j] <> White.

charguer's avatar
charguer committed
383 384 385 386 387 388 389
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).
charguer's avatar
charguer committed
390 391 392

  (* TODO: above, might need to maintain that [R \c nodes G]
           in order to prove facts of the form [r \in nodes G] *)
charguer's avatar
charguer committed
393 394

Definition hinv G R C g c :=
charguer's avatar
charguer committed
395
     g ~> RGraph G
charguer's avatar
charguer committed
396 397 398 399 400 401
  \* c ~> Array C
  \* \[ inv G R C ].


(********************************************************************)
(* ** Auxiliary lemmas *)
charguer's avatar
DFS_ok  
charguer committed
402 403

Lemma evolution_refl : refl evolution.
charguer's avatar
charguer committed
404
Proof using. (* trivial *)
charguer's avatar
charguer committed
405 406
  => C. splits*.
Qed.
charguer's avatar
DFS_ok  
charguer committed
407 408 409 410 411 412 413

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

charguer's avatar
charguer committed
415 416 417 418 419
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].
charguer's avatar
charguer committed
420
Proof using.  (* trivial *)
charguer's avatar
charguer committed
421 422 423
  =>> (E1&E2) Ci HN. split.
  { => j Hj Ej. rew_array~. case_if~.
    { apply~ E1. rew_array~. case_if~. } }
charguer's avatar
charguer committed
424 425
  { => j Hj. rew_array~. case_if.
    { subst. rename j into i. iff; auto_false. }
charguer's avatar
charguer committed
426
    { rewrite~ <- E2. rew_array~. case_if*. } }
charguer's avatar
charguer committed
427
Qed.
charguer's avatar
charguer committed
428

charguer's avatar
charguer committed
429
Lemma no_white_in_evolution : forall C C' E,
charguer's avatar
charguer committed
430
  no_white_in E C ->
charguer's avatar
charguer committed
431
  evolution C C' ->
charguer's avatar
charguer committed
432 433
  no_white_in E C'.
Proof using.  (* trivial *)
charguer's avatar
charguer committed
434
  =>> N (H1&H2) i Hi. cases (C[i]) as Ci.
charguer's avatar
charguer committed
435 436 437 438 439
  { false* N. }
  { forwards~ (H2a&_): H2 i. rewrite~ H2a. auto_false. }
  rewrite~ H1. auto_false.
Qed.

charguer's avatar
charguer committed
440 441 442 443
Lemma no_gray_evolution : forall C C',
  no_gray C ->
  evolution C C' ->
  no_gray C'.
charguer's avatar
charguer committed
444
Proof using. (* trivial *)
charguer's avatar
charguer committed
445 446
  =>> N (H1&H2) i Hi Ci. forwards~ (_&HR): H2 i. applys~ N i.
Qed.
charguer's avatar
charguer committed
447 448 449 450 451 452 453

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.
charguer's avatar
charguer committed
454 455
Proof using.
  =>> HW HG (p&HP). induction HP; => Ci.
charguer's avatar
charguer committed
456 457 458 459 460 461 462 463
  (* trivial after induction *)
  { auto. }
  { applys IHHP. cases (C[y]).
    { false* HW. }
    { false* HG. }
    { auto. } }
Qed.

charguer's avatar
charguer committed
464 465 466 467 468
Lemma inv_empty : forall G n,
  nodes_index G n ->
  inv G \{} (make n White).
Proof using. (* trivial *)
  =>> Hn. splits.
charguer's avatar
charguer committed
469 470 471
  { 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. }
charguer's avatar
proof  
charguer committed
472 473
Qed.

charguer's avatar
charguer committed
474 475 476
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.
charguer's avatar
charguer committed
477
Proof using. (* trivial *)
charguer's avatar
charguer committed
478 479 480
  =>> (I1&I2&I3). splits.
  { auto. }
  { auto. }
charguer's avatar
charguer committed
481 482
  { => j Hj Cj. forwards~ (r&Hr&Pr): I3 j.
    exists* r. splits*. rew_set. eauto. (* TODO: tactic *) }
charguer's avatar
charguer committed
483 484
Qed.

charguer's avatar
charguer committed
485 486 487 488 489
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]).
charguer's avatar
charguer committed
490
Proof using. (* trivial *)
charguer's avatar
charguer committed
491
  =>> Ci Hi (I1&I2&I3). splits.
charguer's avatar
charguer committed
492
  { rew_array~. }
charguer's avatar
charguer committed
493
  { => j k Hjk. rew_array~. => Cjk. case_if; auto_false.
charguer's avatar
charguer committed
494 495
   case_if. applys* I2. }
  { => j Hj. rew_array~. case_if; auto_false. }
charguer's avatar
charguer committed
496 497
Qed.

charguer's avatar
charguer committed
498 499 500 501 502 503 504
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.
charguer's avatar
charguer committed
505 506 507
  { rew_array~. }
  { => j k Hjk. rew_array~. => M. case_if; auto_false. case_if.
    { subst. applys Wi. rewrite~ out_edges_has_edge. }
charguer's avatar
charguer committed
508
    { applys* I2. } }
charguer's avatar
charguer committed
509 510
  { => j Hj. rew_array~. case_if; [subst|auto].
    => _. rename j into i. eauto. }
charguer's avatar
charguer committed
511 512 513
Qed.


charguer's avatar
charguer committed
514 515 516
(*************************************************************************)
(** Verification of DFS *)

charguer's avatar
proof  
charguer committed
517
Lemma dfs_from_spec : forall G R C g c i,
charguer's avatar
charguer committed
518
  reachable_from G R i ->
charguer's avatar
charguer committed
519
  C[i] = White ->
charguer's avatar
proof  
charguer committed
520
  app dfs_from [g c i]
charguer's avatar
charguer committed
521
    PRE (hinv G R C g c)
charguer's avatar
proof  
charguer committed
522
    POST (# Hexists C', hinv G R C' g c
charguer's avatar
charguer committed
523
       \* \[ evolution C C' /\ C'[i] = Black ]).
charguer's avatar
charguer committed
524
Proof using.
charguer's avatar
charguer committed
525
  skip_goal IH. hide IH. (* TODO: set up the decreasing measure to prove termination *)
charguer's avatar
charguer committed
526
  => G R C0. =>> Ri Wi.
charguer's avatar
DFS_ok  
charguer committed
527 528
  asserts Hi: (i \in nodes G).
    { destruct Ri as (r&Hr&Mr). applys* reachable_in_nodes_r. } (* trivial *)
charguer's avatar
charguer committed
529
  xcf. unfold hinv. xpull ;=> HI. xapps~. sets_eq C1: (C0[i:=Gray]).
charguer's avatar
charguer committed
530
  xfun as f. set (loop_inv := fun L C => hinv G R C g c
charguer's avatar
charguer committed
531
         \* \[ evolution C1 C /\ no_white_in L C ]).
charguer's avatar
charguer committed
532 533
  xseq. xapp_no_simpl (>> (fun L => Hexists C, loop_inv L C) G).
  { auto. }
charguer's avatar
charguer committed
534
  { => L. unfold loop_inv, hinv. applys heap_contains_intro
charguer's avatar
DFS_ok  
charguer committed
535
    (Hexists C, c ~> Array C \* \[ inv G R C] \*  (* ideally, should be computed *)
charguer's avatar
charguer committed
536
     \[ evolution C1 C /\ no_white_in L C]); xsimpl~. }
charguer's avatar
charguer committed
537
  { => j js Hj Eij. unfold loop_inv, hinv.
charguer's avatar
charguer committed
538
    xpull ;=> C I0 (H1&H2). xapp. clears f.
charguer's avatar
charguer committed
539
    xapps~. xapps~. xpolymorphic_eq.
charguer's avatar
charguer committed
540
    xpost (Hexists C', hinv G R C' g c
charguer's avatar
charguer committed
541
         \* \[ evolution C1 C' /\ no_white_in js C' /\ C'[j] <> White ]).
charguer's avatar
charguer committed
542
    { xif.
charguer's avatar
charguer committed
543
      { show IH. xapply (>> IH G R C).
charguer's avatar
DFS_ok  
charguer committed
544 545
        { destruct Ri as (r&Pr&Mr). exists r. split~. (* trivial *)
          applys* reachable_trans_edge. } (* trivial *)
charguer's avatar
charguer committed
546
        { auto. } (* trivial *)
charguer's avatar
charguer committed
547
        { unfold hinv. xsimpl~. }
charguer's avatar
charguer committed
548
        unfold hinv. xpull ;=> C' I1 (F1&F2). xsimpl. splits.
charguer's avatar
charguer committed
549
        { applys* evolution_trans. }
charguer's avatar
charguer committed
550 551 552
        { applys* no_white_in_evolution. } (* trivial *)
        { auto_false. }  (* trivial *)
        { auto. } } (* trivial *)
charguer's avatar
charguer committed
553
      { xret. unfold hinv. xsimpl~. } }
charguer's avatar
charguer committed
554
    { unfold hinv. xpull ;=> C' I1 (F1&F2&F3). xsimpl. splits.
charguer's avatar
charguer committed
555 556 557
      { auto. } (* trivial *)
      { => k Hk. rew_set in Hk. destruct~ Hk. subst~. } (* trivial *)
      { auto. } } } (* trivial *)
charguer's avatar
charguer committed
558 559
  { clears f. unfold loop_inv, hinv. xsimpl. split.
    { applys evolution_refl. }
charguer's avatar
charguer committed
560
    { => j Hj. rew_array~. } (* trivial *)
charguer's avatar
charguer committed
561
    { subst C1. applys* inv_gray_root. } }
charguer's avatar
charguer committed
562 563
  { unfold loop_inv, hinv. xpull ;=> C' I1 (F1&F2).
    xapps~. xsimpl. split.
charguer's avatar
charguer committed
564
    { subst C1. applys* evolution_write_black. }
charguer's avatar
charguer committed
565
    { rew_array~. case_if~. } (* trivial *)
charguer's avatar
charguer committed
566
    { applys* inv_evolution_black. } }
charguer's avatar
init  
charguer committed
567 568
Qed.

charguer's avatar
charguer committed
569
Hint Extern 1 (RegisterSpec dfs_from) => Provide dfs_from_spec.
charguer's avatar
init  
charguer committed
570

charguer's avatar
charguer committed
571
Lemma dfs_main_spec : forall (G:graph) g (rs:list int),
charguer's avatar
charguer committed
572 573
  app dfs_main [g rs]
    PRE (g ~> RGraph G)
charguer's avatar
charguer committed
574
    POST (fun c => Hexists C,
charguer's avatar
charguer committed
575
      c ~> Array C \*
charguer's avatar
charguer committed
576
      g ~> RGraph G \*
charguer's avatar
charguer committed
577
      \[ forall i, i \in nodes G ->
charguer's avatar
charguer committed
578
         (C[i] = Black <-> exists r, r \in set_of_list rs /\ reachable G r i)]).
charguer's avatar
charguer committed
579
Proof using.
charguer's avatar
charguer committed
580 581
  xcf. xapp. => Hn. xapp.
  { applys (proj1 Hn). } (* trivial *)
charguer's avatar
charguer committed
582
  => C0 HC0.
charguer's avatar
charguer committed
583
  asserts N0: (no_gray C0). { subst. => i Hi. rew_array; auto_false. } (* trivial *)
charguer's avatar
charguer committed
584 585
  xfun as f.
  set (loop_inv := fun L C => hinv G (set_of_list L) C g c
charguer's avatar
charguer committed
586
         \* \[ evolution C0 C /\ all_black_in (set_of_list L) C ]).
charguer's avatar
charguer committed
587
  xapp (fun L => Hexists C, loop_inv L C).
charguer's avatar
DFS_ok  
charguer committed
588
  { => i L T HL. lets (_&Hi): (proj2 Hn) i.
charguer's avatar
charguer committed
589
    unfold loop_inv, hinv. xpull ;=> C HI (HC1&HC2).
charguer's avatar
DFS_ok  
charguer committed
590 591
    xapp. clears f. xapps~. xapps~. xpolymorphic_eq. xif.
    { xapp G (\{i} \u set_of_list L) C.
charguer's avatar
charguer committed
592 593 594 595
      { exists i. split.
        { rew_set; eauto. } (* TODO: tactic *)
        { applys* reachable_self. } } (* trivial *)
      { auto. } (* trivial *)
charguer's avatar
charguer committed
596
      { unfold hinv. xsimpl*. applys* inv_add_root. }
charguer's avatar
DFS_ok  
charguer committed
597 598 599 600
      { unfold loop_inv, hinv. intros u. xpull ;=> C' I1 (F1&F2).
        rew_set_of_list. xsimpl.
        { splits. (* trivial *)
          { applys~ evolution_trans F1. } (* trivial *)
charguer's avatar
charguer committed
601 602
          { => j Hj. rew_set in Hj. destruct Hj. (* trivial *)
           { applys~ (proj1 F1). } { subst~. } } } (* trivial *)
charguer's avatar
charguer committed
603
        { rewrite~ union_comm. } } } (* trivial *)
charguer's avatar
DFS_ok  
charguer committed
604 605
    { xret. unfold loop_inv, hinv. rew_set_of_list. xsimpl~. split.
      { auto. } (* trivial *)
charguer's avatar
charguer committed
606 607 608 609
      { => 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 *)
charguer's avatar
DFS_ok  
charguer committed
610 611 612
      { cases~ (C[i]). (* trivial *)
        { false. } (* trivial *)
        { false~ N0 i. forwards~ (?&?): (proj2 HC1) i. } (* trivial *)
charguer's avatar
charguer committed
613
        { rewrite~ union_comm. applys* inv_add_root. } } } }
charguer's avatar
DFS_ok  
charguer committed
614
    { unfold loop_inv, hinv. rew_set_of_list. xsimpl. split.
charguer's avatar
charguer committed
615
      { applys* evolution_refl. } (* trivial *)
charguer's avatar
charguer committed
616
      { => r Hr. rew_set in Hr. false. } (* trivial *)
charguer's avatar
charguer committed
617
      { subst C0. applys* inv_empty. } } (* trivial *)
charguer's avatar
DFS_ok  
charguer committed
618
  unfold loop_inv, hinv. => C1. xpull ;=> (I1&I2&I3) (H1&H2).
charguer's avatar
charguer committed
619
  xret. xsimpl. split.
charguer's avatar
DFS_ok  
charguer committed
620
  { => M. applys~ I3. } (* trivial *)
charguer's avatar
charguer committed
621 622
  { => (r&Hr&Mr). applys* no_black_to_white_no_gray_elim.
    applys* no_gray_evolution. }
charguer's avatar
init  
charguer committed
623
Qed.
charguer's avatar
DFS_ok  
charguer committed
624

charguer's avatar
proof  
charguer committed
625

charguer's avatar
charguer committed
626
Hint Extern 1 (RegisterSpec dfs_main) => Provide dfs_main_spec.
charguer's avatar
init  
charguer committed
627 628


charguer's avatar
proof  
charguer committed
629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657