Commit 6b75aae1 authored by charguer's avatar charguer
Browse files

dfs_proress

parent 4f37b123
- xapp_rm
- generate inhab instance for algebraic
- xwhile needs to call tag_pre_post in branches
......
......@@ -27,10 +27,10 @@ type color = White | Gray | Black
then dfs_from g c j) g i;
c.(i) <- Black
let dfs_main g r =
let dfs_main g rs =
let n = Graph.nb_nodes g in
let c = Array.make n White in
List.iter (fun i ->
if c.(i) = White then
dfs_from g c i) r;
dfs_from g c i) rs;
c
......@@ -6,7 +6,9 @@ Require Import LibListZ.
Require Import Array_proof.
Require Import List_proof.
Open Scope tag_scope.
Ltac auto_star ::= subst; intuition eauto with maths.
Ltac auto_star ::=
try solve [ subst; intuition eauto with maths ].
......@@ -57,72 +59,8 @@ Inductive is_path (G:graph) : int -> int -> path -> Prop :=
Definition reachable (G:graph) (i j:int) :=
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.
(********************************************************************)
(* ** 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.
Proof using.
skip.
Qed.
Lemma reachable_trans : forall G i j k,
reachable G i j ->
reachable G j k ->
reachable G i k.
Proof using.
skip.
Qed.
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.
introv R HE HF. rewrite incl_in_eq in HE,HF. skip.
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.
Definition no_black_to_while G C :=
forall i j,
has_edge G i j ->
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_white_path_goes_through_gray : forall G C,
no_black_to_while G C ->
forall 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 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.
(********************************************************************)
......@@ -133,16 +71,41 @@ Qed.
[0] inclusive to [n] exclusive. *)
Definition nodes_index (G:graph) (n:int) :=
forall i, i \in nodes G = index n i.
forall i, i \in nodes G <-> index n i.
(** [g ~> GraphAdj G] asserts that at pointer [g] is an imperative
(** [g ~> RGraph G] asserts that at pointer [g] is an imperative
array of pure lists that represents the adjacency lists of [G]. *)
Definition GraphAdj (G:graph) (g:loc) :=
Definition RGraph (G:graph) (g:loc) :=
Hexists N, g ~> Array N
\* \[nodes_index G (LibListZ.length N)
/\ forall i j, i \in nodes G ->
Mem j (N[i]) = has_edge G i j].
Lemma RGraph_open : forall (g:loc) (G:graph),
g ~> RGraph G ==>
Hexists N, g ~> Array N
\* \[nodes_index G (LibListZ.length N)
/\ forall i j, i \in nodes G ->
Mem j (N[i]) = has_edge G i j].
Proof using. intros. xunfolds~ RGraph. Qed.
Lemma RGraph_close : forall (g:loc) (G:graph) N,
nodes_index G (LibListZ.length N) ->
(forall i j, i \in nodes G -> Mem j (N[i]) = has_edge G i j) ->
g ~> Array N
==>
g ~> RGraph G.
Proof using. intros. xunfolds~ RGraph. Qed.
Implicit Arguments RGraph_close [].
Hint Extern 1 (RegisterOpen (RGraph _)) =>
Provide RGraph_open.
Hint Extern 1 (RegisterClose (Array _)) =>
Provide RGraph_close.
......@@ -176,6 +139,105 @@ Hint Extern 1 (index ?n ?x) => skip. (* TODO *)
(********************************************************************)
(* ** 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.
Proof using.
skip.
Qed.
Lemma reachable_trans : forall G i j k,
reachable G i j ->
reachable G j k ->
reachable G i k.
Proof using.
skip.
Qed.
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)).
(* 1 <-> (blacks C) \c (blacks C')
2 <-> (grays C) = (grays C') *)
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.
Lemma all_black_in_evolution : forall C C' E,
all_black_in E C ->
evolution C C' ->
all_black_in E C'.
Proof using. =>> N (H1&H2) i Hi. auto. Qed. (* trivial *)
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. =>> N (H1&H2) i Hi Ci. forwards~ (_&HR): H2 i. applys~ N i. Qed. (* trivial *)
Lemma evolution_trans : trans evolution.
Proof using. (* trivial *)
=>> (F1&G1) (F2&G2). unfolds evolution. splits.
autos*.
intros. rewrite~ G1.
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.
(* 2 <-> grays C = \{}
5 <-> i \in blacks C
6 <-> j \notin white C <-> j \in (blacks C \u grays C) *)
(*************************************************************************)
(** Set of list predicate : TODO: move *)
......@@ -223,11 +285,11 @@ End SetOfList.
(* Import Graph_ml. *)
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. xunfold GraphAdj. xpull ;=> N (HN1&HN2).
app Graph_ml.nb_nodes [g]
PRE (g ~> RGraph G)
POST (fun n => g ~> RGraph G \* \[nodes_index G n]).
Proof using. (* TODO: app_keep *)
xcf. xunfold RGraph. xpull ;=> N (HN1&HN2).
xapp. xsimpl*.
Qed.
......@@ -238,10 +300,10 @@ Lemma iter_edges_spec : forall (I:set int->hprop) (G:graph) g f i,
(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 (out_edges G i)).
PRE (g ~> RGraph G \* I \{})
POST (# g ~> RGraph G \* I (out_edges G i)).
Proof.
introv Gi Sf. xcf. xunfold GraphAdj. xpull ;=> N (GI&GN).
introv Gi Sf. xcf. xunfold RGraph. 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 *) }
......@@ -256,8 +318,6 @@ Qed.
Hint Extern 1 (RegisterSpec Graph_ml.iter_edges) => Provide iter_edges_spec.
(*************************************************************************)
(** DFS *)
......@@ -267,49 +327,92 @@ 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_st (fun i:int => index C i /\ C[i] = Black).
(* \set{ i:int | index C i /\ C[i] = Black }. *)
Definition grays C :=
set_st (fun i:int => index C i /\ C[i] = Gray).
Definition inv G R C :=
length C = card (nodes G)
/\ R \c nodes G
/\ no_black_to_while G C
/\ reachables G (R \u blacks C) (blacks C).
(nodes_index G (length C))
/\ (forall r, r \in R -> C[r] = Black)
/\ (no_black_to_white G C)
/\ (forall i, i \in nodes G -> C[i] = Black -> exists r, r \in R /\ reachable G r i).
(* 2 <-> R \c (blacks C)
4 <-> reachables G R (blacks C). *)
Definition hinv G R C g c :=
g ~> GraphAdj G
g ~> RGraph G
\* c ~> Array C
\* \[ inv G R C ].
Lemma dfs_from_spec : forall G R C g c 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
\* \[ C'[i] = Black
/\ (blacks C) \c (blacks C') ]).
/\ evolution C 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 dfs_main [g r]
PRE (g ~> GraphAdj G)
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 ~> GraphAdj G \*
\[ reachables G (set_of_list r) (blacks 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. skip. (* xunfold GraphAdj at 1. xpull ;=> HI. *)
xcf.
xapp. => Hn.
xapp. skip. => C0 HC0.
xfun as f.
set (loop_inv := fun L C => hinv G (set_of_list L) C g c
\* \[ evolution C0 C /\ no_gray C /\ all_black_in (set_of_list L) C ]).
xapp (fun L => Hexists C, loop_inv L C).
{ intros i L k HL. unfold loop_inv, hinv. xpull ;=> C HI (HC1&HC2&HC3).
xapp. clears f.
xapps~.
xapps~. xpolymorphic_eq.
xpost (Hexists C', loop_inv L C' \* \[C'[i] = Black]). xif.
{ xapp (set_of_list L) C.
{ auto. } (* trivial *)
{ unfold hinv. xsimpl*. } (* trivial *)
{ unfold loop_inv. intros u. xpull ;=> C' (H1&H2). xsimpl.
{ auto_false. } (* trivial *)
{ splits. (* trivial *)
{ applys~ evolution_trans H2. } (* trivial *)
{ applys~ no_gray_evolution H2. } (* trivial *)
{ applys~ all_black_in_evolution H2. } } } } (* trivial *)
{ xret. unfold loop_inv, hinv. xsimpl~.
{ cases~ (C[i]). false. false* HC2. } } (* trivial *)
{ unfold loop_inv, hinv. => u. xpull ;=> C' HI' (H1&H2&H3) Hi.
rewrite set_of_list_last. xsimpl~.
{ splits~. { => j Rj. set_in Rj; auto. } } (* trivial *)
{ destruct HI' as (I1&I2&I3&I4). splits.
{ auto. } (* trivial *)
{ => r Hr. set_in Hr; auto. } (* trivial *)
{ auto. } (* trivial *)
{ => j Hj Cj. forwards~ (r&?&?): I4 Cj. exists* r. } } } } (* trivial *)
{ unfold loop_inv, hinv. xsimpl.
{ split. (* trivial *)
{ hnfs*. } (* trivial *)
{ split. (* trivial *)
{ => j Hj. subst C0. rew_arr; auto_false. } (* trivial *)
{ => i Hi. false. } } } (* trivial *)
{ splits.
{ subst C0. rew_arr. hnf in Hn. skip. skip. } (* trivial *)
{ => r Hr. rewrite set_of_list_nil in Hr. false. } (* trivial *)
{ =>> Hi Ci. false. subst C0. rew_arr~ in Ci. false. } (* trivial *)
{ => i Hi Ci. false. subst C0. rew_arr~ in Ci. false. } } } (* trivial *)
unfold loop_inv, hinv. => C1. xpull ;=> (F1&F2&F3&F4) (H1&H2&H3).
xret. xsimpl. split.
{ => M. applys~ F4. } (* trivial *)
{ => (r&Hr&Mr). applys* no_black_to_white_no_gray_elim. }
Qed.
(* conclusion <-> reachables G (set_of_list r) (blacks C) *)
Hint Extern 1 (RegisterSpec dfs_main) => Provide dfs_main_spec.
......
(*
Definition reachables (G:graph) (E F:set int) :=
forall j, j \in F -> exists i, i \in E /\ reachable G i j.
*)
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.
introv R HE HF. rewrite incl_in_eq in HE,HF. skip.
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.
Definition blacks C :=
set_st (fun i:int => index C i /\ C[i] = Black).
(* \set{ i:int | index C i /\ C[i] = Black }. *)
Definition grays C :=
set_st (fun i:int => index C i /\ C[i] = Gray).
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)))) ->
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment