DFS_proof.v 8.18 KB
Newer Older
charguer's avatar
init  
charguer committed
1
Set Implicit Arguments.
charguer's avatar
charguer committed
2
3
4
Require Import CFLib.
Require Import DFS_ml.
Require Import Stdlib.
charguer's avatar
proof    
charguer committed
5
6
7
Require Import LibListZ.
Require Import Array_proof.
Require Import List_proof.
charguer's avatar
charguer committed
8
9
Open Scope tag_scope.
Ltac auto_star ::= subst; intuition eauto with maths.
charguer's avatar
init  
charguer committed
10
11
12



charguer's avatar
proof    
charguer committed
13
14
15
16
17
(********************************************************************)
(* ** TODO: Should be generated *)

Instance color__inhab : Inhab color_.
Proof. typeclass. Qed.
charguer's avatar
init  
charguer committed
18
19
20
21
22




(********************************************************************)
charguer's avatar
charguer committed
23
(* ** TLC Graph without information on edges *)
charguer's avatar
init  
charguer committed
24

charguer's avatar
proof    
charguer committed
25
Parameter graph : Type.
charguer's avatar
charguer committed
26
27
Parameter nodes : graph -> set int.
Parameter edges : graph -> set (int*int).
charguer's avatar
init  
charguer committed
28

charguer's avatar
charguer committed
29
Parameter out_edges : graph -> int -> set int.
charguer's avatar
init  
charguer committed
30

charguer's avatar
charguer committed
31
32
Definition has_edge (G:graph) x y :=
  (x,y) \in edges G.
charguer's avatar
init  
charguer committed
33

charguer's avatar
charguer committed
34
35
Parameter has_edge_nodes : forall (G : graph) x y,
  has_edge G x y -> x \in nodes G /\ y \in nodes G.
charguer's avatar
init  
charguer committed
36

charguer's avatar
charguer committed
37
38
39
Lemma has_edge_in_nodes_l : forall (G : graph) x y,
  has_edge G x y -> x \in nodes G.
Proof using. intros. forwards*: has_edge_nodes. Qed.
charguer's avatar
init  
charguer committed
40

charguer's avatar
charguer committed
41
42
43
Lemma has_edge_in_nodes_r : forall (G : graph) x y,
  has_edge G x y -> y \in nodes G.
Proof using. intros. forwards*: has_edge_nodes. Qed.
charguer's avatar
init  
charguer committed
44
45


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

charguer's avatar
charguer committed
48
Inductive is_path (G:graph) : int -> int -> path -> Prop :=
charguer's avatar
init  
charguer committed
49
  | is_path_nil : forall x, 
charguer's avatar
charguer committed
50
51
52
53
54
55
      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
56

charguer's avatar
charguer committed
57
Definition reachable (G:graph) (i j:int) :=
charguer's avatar
proof    
charguer committed
58
  exists p, is_path G i j p.
charguer's avatar
init  
charguer committed
59

charguer's avatar
charguer committed
60
Definition reachables (G:graph) (E F:set int) :=
charguer's avatar
proof    
charguer committed
61
  forall j, j \in F -> exists i, i \in E /\ reachable G i j.
charguer's avatar
init  
charguer committed
62
63
64



charguer's avatar
charguer committed
65
66
(********************************************************************)
(* ** Facts *)
charguer's avatar
init  
charguer committed
67

charguer's avatar
proof    
charguer committed
68
69
70
71
72
73
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
charguer committed
74
75
76
77
78
79
80
81
Lemma reachable_edge : forall G i j,
  has_edge G i j -> 
  reachable G i j.
Proof using.
  skip.
Qed.
 
Lemma reachable_trans : forall G i j k,
charguer's avatar
proof    
charguer committed
82
83
  reachable G i j ->
  reachable G j k ->
charguer's avatar
charguer committed
84
85
86
87
  reachable G i k.
Proof using.
  skip.
Qed.
charguer's avatar
init  
charguer committed
88

charguer's avatar
charguer committed
89
90
91
92
93
94
Lemma reachables_monotone : forall G E1 E2 F1 F2,
  reachables G E1 F1 ->
  E1 \c E2 ->
  F2 \c F1 ->
  reachables G E2 F2.
Proof using.
charguer's avatar
charguer committed
95
  introv R HE HF. rewrite incl_in_eq in HE,HF. skip.
charguer's avatar
charguer committed
96
97
98
99
100
101
102
103
104
Qed.
 
Lemma reachables_trans : forall G E1 E2 E3,
  reachables G E1 E2 ->
  reachables G E2 E3 ->
  reachables G E1 E3.
Proof using.
  skip.
Qed.
charguer's avatar
init  
charguer committed
105
106


charguer's avatar
charguer committed
107
108
109
Definition no_black_to_while G C := 
  forall i j, 
  has_edge G i j -> 
charguer's avatar
proof    
charguer committed
110
  C[i] = Black ->
charguer's avatar
charguer committed
111
112
113
  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). *)
charguer's avatar
init  
charguer committed
114

charguer's avatar
proof    
charguer committed
115
Lemma black_to_white_path_goes_through_gray : forall G C,
charguer's avatar
charguer committed
116
117
  no_black_to_while G C ->
  forall i j p, 
charguer's avatar
proof    
charguer committed
118
  is_path G i j p -> 
charguer's avatar
charguer committed
119
120
  C[i] = Black -> (*i \in blacks C *)
  C[i] = White -> (*i \notin (blacks C \u grays C) *)
charguer's avatar
proof    
charguer committed
121
122
123
124
125
  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.
charguer's avatar
init  
charguer committed
126
127
128


(********************************************************************)
charguer's avatar
charguer committed
129
130
(* ** Graph representation predicate *)

charguer's avatar
init  
charguer committed
131
132
133
134

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

charguer's avatar
proof    
charguer committed
135
Definition nodes_index (G:graph) (n:int) :=
charguer's avatar
init  
charguer committed
136
137
  forall i, i \in nodes G = index n i.

charguer's avatar
charguer committed
138
(** [g ~> GraphAdj G] asserts that at pointer [g] is an imperative
charguer's avatar
init  
charguer committed
139
140
    array of pure lists that represents the adjacency lists of [G]. *)

charguer's avatar
proof    
charguer committed
141
Definition GraphAdj (G:graph) (g:loc) :=
charguer's avatar
init  
charguer committed
142
  Hexists N, g ~> Array N
charguer's avatar
proof    
charguer committed
143
   \* \[nodes_index G (LibListZ.length N) 
charguer's avatar
charguer committed
144
145
146
   /\ forall i j, i \in nodes G -> 
        Mem j (N[i]) = has_edge G i j].

charguer's avatar
init  
charguer committed
147
148
149
150
151
152
153
154
155
156
157
158
159



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

(** Hints for lists *)

Hint Constructors Forall.
Hint Resolve Forall_last.

(** Hints for indices *)

charguer's avatar
proof    
charguer committed
160
Lemma graph_adj_index : forall (G:graph) n m x,
charguer's avatar
init  
charguer committed
161
162
163
  nodes_index G n -> x \in nodes G -> n = m -> index m x.
Proof. introv N Nx L. subst. rewrite~ <- N. Qed.

charguer's avatar
proof    
charguer committed
164
(*
charguer's avatar
init  
charguer committed
165
166
167
168
169
170
171
172
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 graph_adj_index; 
  [ try eassumption 
  | instantiate; try eassumption
  | instantiate; try congruence ].
charguer's avatar
proof    
charguer committed
173
174
175
*)
Hint Extern 1 (nodes_index _ _) => skip. (* TODO *)
Hint Extern 1 (index ?n ?x) => skip. (* TODO *)
charguer's avatar
init  
charguer committed
176
177
178



charguer's avatar
proof    
charguer committed
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
(*************************************************************************)
(** 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.


charguer's avatar
init  
charguer committed
219

charguer's avatar
charguer committed
220
221
(*************************************************************************)
(** Graph representation by adjacency lists *)
charguer's avatar
init  
charguer committed
222

charguer's avatar
proof    
charguer committed
223
(* Import Graph_ml. *)
charguer's avatar
init  
charguer committed
224

charguer's avatar
proof    
charguer committed
225
226
Lemma nb_nodes_spec : forall (G:graph) g,
  app Graph_ml.nb_nodes [g]
charguer's avatar
charguer committed
227
228
229
    PRE (g ~> GraphAdj G) 
    POST (fun n => \[nodes_index G n]).
Proof using.
charguer's avatar
proof    
charguer committed
230
231
232
233
234
235
236
237
238
239
240
  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]
charguer's avatar
charguer committed
241
    PRE (g ~> GraphAdj G \* I \{}) 
charguer's avatar
proof    
charguer committed
242
    POST (# g ~> GraphAdj G \* I (out_edges G i)).
charguer's avatar
init  
charguer committed
243
Proof.
charguer's avatar
proof    
charguer committed
244
245
246
247
248
249
250
251
252
253
254
255
256
  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.
charguer's avatar
init  
charguer committed
257
258
259
260




charguer's avatar
charguer committed
261
262
(*************************************************************************)
(** DFS *)
charguer's avatar
init  
charguer committed
263

charguer's avatar
proof    
charguer committed
264
265
266
267
268
(* 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.
*)
charguer's avatar
init  
charguer committed
269

charguer's avatar
charguer committed
270
Definition blacks C :=
charguer's avatar
proof    
charguer committed
271
272
  set_st (fun i:int => index C i /\ C[i] = Black).
  (* \set{ i:int | index C i /\ C[i] = Black }. *)
charguer's avatar
init  
charguer committed
273

charguer's avatar
charguer committed
274
Definition grays C :=
charguer's avatar
proof    
charguer committed
275
276
  set_st (fun i:int => index C i /\ C[i] = Gray).

charguer's avatar
init  
charguer committed
277

charguer's avatar
charguer committed
278
Definition inv G R C :=
charguer's avatar
proof    
charguer committed
279
     length C = card (nodes G)
charguer's avatar
charguer committed
280
281
  /\ R \c nodes G
  /\ no_black_to_while G C
charguer's avatar
proof    
charguer committed
282
  /\ reachables G (R \u blacks C) (blacks C).
charguer's avatar
init  
charguer committed
283

charguer's avatar
proof    
charguer committed
284
Definition hinv G R C g c :=
charguer's avatar
charguer committed
285
     g ~> GraphAdj G 
charguer's avatar
proof    
charguer committed
286
287
  \* c ~> Array C
  \* \[ inv G R C ].
charguer's avatar
init  
charguer committed
288

charguer's avatar
proof    
charguer committed
289
Lemma dfs_from_spec : forall G R C g c i,
charguer's avatar
charguer committed
290
  C[i] = White ->
charguer's avatar
proof    
charguer committed
291
292
293
294
  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
charguer's avatar
charguer committed
295
296
          /\ (blacks C) \c (blacks C') ]).
Proof using.
charguer's avatar
proof    
charguer committed
297
  xcf. skip.
charguer's avatar
init  
charguer committed
298
299
Qed.

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

charguer's avatar
charguer committed
302
Lemma dfs_main_spec : forall (G:graph) g (r:list int),
charguer's avatar
proof    
charguer committed
303
  app dfs_main [g r] 
charguer's avatar
charguer committed
304
305
306
    PRE (g ~> GraphAdj G) 
    POST (fun c => Hexists C,
      c ~> Array C \* 
charguer's avatar
proof    
charguer committed
307
308
309
310
311
      g ~> GraphAdj G \*
      \[ reachables G (set_of_list r) (blacks C) ]).
Proof using.  
  xcf. skip. (* xunfold GraphAdj at 1. xpull ;=> HI. *)
  
charguer's avatar
init  
charguer committed
312
Qed.
charguer's avatar
proof    
charguer committed
313

charguer's avatar
charguer committed
314
Hint Extern 1 (RegisterSpec dfs_main) => Provide dfs_main_spec.
charguer's avatar
init  
charguer committed
315
316
317
318
319
320
321







charguer's avatar
proof    
charguer committed
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354