Commit 245cfb14 authored by charguer's avatar charguer

heap contains

parent a2fdd18a
......@@ -8,625 +8,700 @@ 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 [g i f]
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.
(* TLC BUFFER *)
Lemma remove_empty : forall A (E: set A),
E \- \{} = E.
Proof. intros. rew_set. intros. rew_set. tauto. Qed.
Lemma remove_all : forall A (E: set A),
E \- E = \{}.
Proof. intros. rew_set. intros. rew_set. tauto. Qed.
(* TODO: "rew_set*" *)
(*************************************************************************)
(** Automation *)
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.
(* Future work:
Lemma heap_contains_intro_hexists_1 : forall A (J:A->hprop) H,
H \c (Hexists x, H \* J x).
Proof using.
intros. applys heap_contains_intro (Hexists x, J x); hsimpl.
Qed.
Lemma heap_contains_intro_hexists_2 : forall A1 A2 (J:A1->A2->hprop) H,
H \c (Hexists x y, H \* J x y).