Commit 9474d364 authored by charguer's avatar charguer

DFS proof fixed

parent bce17edb
(** Representation of fixed-size circular buffers. *) (** Representation of fixed-size circular buffers. *)
module Make (Capa : CapacitySig.S) (Item : InhabType.S) = module Make (Capa : CapacitySig.S) (Item : InhabType.S) =
......
Set Implicit Arguments. Set Implicit Arguments.
Require Import CFLib. Require Import CFML.CFLib.
Require Import DFS_ml. Require Import DFS_ml.
Require Import Stdlib. Require Import Stdlib.
Require Import LibListZ. Require Import TLC.LibListZ.
Require Import Array_proof. Require Import Array_proof.
Require Import List_proof. Require Import List_proof.
Open Scope tag_scope. Open Scope tag_scope.
...@@ -25,7 +25,7 @@ Lemma heap_contains_intro : forall (H H1 H2 : hprop), ...@@ -25,7 +25,7 @@ Lemma heap_contains_intro : forall (H H1 H2 : hprop),
(H2 ==> H1 \* H) -> (H2 ==> H1 \* H) ->
(H1 \* H ==> H2) -> (H1 \* H ==> H2) ->
(H1 \c H2). (H1 \c H2).
Proof using. introv M1 M2. hnf. exists H. apply* pred_le_extens. Qed. Proof using. introv M1 M2. hnf. exists H. apply* antisym_pred_incl. Qed.
Lemma heap_contains_elim : forall (H1 H2 : hprop), Lemma heap_contains_elim : forall (H1 H2 : hprop),
(H1 \c H2) -> exists H, (H1 \c H2) -> exists H,
...@@ -35,31 +35,33 @@ Proof using. introv (H&M). exists H. split*. Qed. ...@@ -35,31 +35,33 @@ Proof using. introv (H&M). exists H. split*. Qed.
Global Opaque heap_contains. Global Opaque heap_contains.
Lemma No_duplicates_app_inv : forall A (L1 L2 : list A), (*
No_duplicates (L1 ++ L2) -> Search noduplicates.
No_duplicates L1 Lemma noduplicates_app_inv : forall A (L1 L2 : list A),
/\ No_duplicates L2 noduplicates (L1 ++ L2) ->
/\ (~ exists x, Mem x L1 /\ Mem x L2). noduplicates L1
/\ noduplicates L2
/\ (~ exists x, mem x L1 /\ mem x L2).
Proof using. Proof using.
introv ND. splits. introv ND. splits.
induction L1. induction L1.
constructors. constructors.
rew_list in ND. inverts ND as ND1 ND2. rewrite Mem_app_or_eq in ND1. rew_logic* in ND1. rew_list in ND. inverts ND as ND1 ND2. rewrite mem_app_or_eq in ND1. rew_logic* in ND1.
induction L1. induction L1.
rew_list~ in ND. rew_list~ in ND.
rew_list in ND. inverts~ ND. rew_list in ND. inverts~ ND.
introv (x&I1&I2). induction I1; rew_list in ND. introv (x&I1&I2). induction I1; rew_list in ND.
inverts ND as ND1 ND2. false ND1. apply* Mem_app_or. inverts ND as ND1 ND2. false ND1. apply* mem_app_or.
apply IHI1. inverts~ ND. apply IHI1. inverts~ ND.
Qed. Qed.
*)
(*************************************************************************) (*************************************************************************)
(** Set of list predicate : TODO: move *) (** Set of list predicate : TODO: move *)
Definition set_of_list_monoid A := Definition set_of_list_monoid A :=
(monoid_ (union : _ -> _ -> set A) (\{}:set A)). (monoid_make (union : _ -> _ -> set A) (\{}:set A)).
Definition set_of_list A (L : list A) := Definition set_of_list A (L : list A) :=
LibList.fold (@set_of_list_monoid A) (fun x => \{x}) L. LibList.fold (@set_of_list_monoid A) (fun x => \{x}) L.
...@@ -89,12 +91,12 @@ Lemma set_of_list_app : forall l1 l2, ...@@ -89,12 +91,12 @@ Lemma set_of_list_app : forall l1 l2,
set_of_list (l1 ++ l2) = (set_of_list l1) \u (set_of_list 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. Proof using. intros. unfold set_of_list. rewrite~ fold_app. Qed.
Lemma set_of_list_Mem : forall l x, Lemma set_of_list_mem : forall l x,
x \in set_of_list l -> Mem x l. x \in set_of_list l -> mem x l.
Proof using. Proof using.
introv. induction l; introv M. introv. induction l; introv M.
{ false. } { false. }
{ rewrite set_of_list_cons in M. set_in M; eauto. } { rewrite set_of_list_cons in M. rew_set in M. destruct* M. }
Qed. Qed.
End SetOfList. End SetOfList.
...@@ -165,7 +167,7 @@ Definition reachable (G:graph) (i j:int) := ...@@ -165,7 +167,7 @@ Definition reachable (G:graph) (i j:int) :=
Lemma out_edges_has_edge : forall G i j, Lemma out_edges_has_edge : forall G i j,
j \in out_edges G i <-> has_edge G i j. j \in out_edges G i <-> has_edge G i j.
Proof using. Proof using.
intros. unfold has_edge, out_edges. rewrite~ in_set_st_eq. intros. unfold has_edge, out_edges. rewrite* in_set_st_eq.
Qed. Qed.
Lemma has_edge_nodes : forall (G : graph) x y, Lemma has_edge_nodes : forall (G : graph) x y,
...@@ -241,7 +243,7 @@ Definition nodes_index (G:graph) (n:int) := ...@@ -241,7 +243,7 @@ Definition nodes_index (G:graph) (n:int) :=
Definition nodes_edges (G:graph) (N:list(list int)) := Definition nodes_edges (G:graph) (N:list(list int)) :=
forall i, i \in nodes G -> forall i, i \in nodes G ->
set_of_list (N[i]) = out_edges G i set_of_list (N[i]) = out_edges G i
/\ No_duplicates (N[i]). /\ noduplicates (N[i]).
(** [g ~> RGraph 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]. *) array of pure lists that represents the adjacency lists of [G]. *)
...@@ -270,7 +272,7 @@ Lemma RGraph_close : forall (g:loc) (G:graph) N, ...@@ -270,7 +272,7 @@ Lemma RGraph_close : forall (g:loc) (G:graph) N,
g ~> RGraph G. g ~> RGraph G.
Proof using. intros. xunfolds~ RGraph. Qed. Proof using. intros. xunfolds~ RGraph. Qed.
Implicit Arguments RGraph_close []. Arguments RGraph_close : clear implicits.
Hint Extern 1 (RegisterOpen (RGraph _)) => Hint Extern 1 (RegisterOpen (RGraph _)) =>
Provide RGraph_open. Provide RGraph_open.
...@@ -340,13 +342,13 @@ Proof. ...@@ -340,13 +342,13 @@ Proof.
xchange (rm HO). xopen g. xpull ;=> N (GI&GN). xchange (rm HO). xopen g. xpull ;=> N (GI&GN).
forwards (GNE&GND): GN Gi. xapps~. xclose* g. xchange (rm HC). forwards (GNE&GND): GN Gi. xapps~. xclose* g. xchange (rm HC).
xfun. xapp_no_simpl (fun (L:list int) => I (set_of_list L)). xfun. xapp_no_simpl (fun (L:list int) => I (set_of_list L)).
{ introv EN. rewrite set_of_list_last. xapp. xapp. { introv EN. rewrite set_of_list_last. xapp.
xapp_spec Sf. (* TODO: xapp *)
{ intros M. rewrite EN in GND. (* trivial *) { intros M. rewrite EN in GND. (* trivial *)
lets (_&_&N3): No_duplicates_app_inv GND. applys (rm N3). (* trivial *) lets (_&_&N3): noduplicates_app_inv GND. applys (rm N3). (* trivial *)
exists x. forwards*: set_of_list_Mem M. } (* trivial *) exists x. forwards*: set_of_list_mem M. } (* trivial *)
{ rewrite <- out_edges_has_edge. rewrite <- GNE. rewrite EN. (* trivial *) { rewrite <- out_edges_has_edge. rewrite <- GNE. rewrite EN. (* trivial *)
rew_set_of_list. eauto. } (* trivial *) rew_set_of_list. rew_set; eauto. } (* trivial *)
{ xsimpl. }
{ rewrite union_comm. xsimpl. } } { rewrite union_comm. xsimpl. } }
{ rew_set_of_list. xsimpl. } { rew_set_of_list. xsimpl. }
{ rewrite GNE. xsimpl. } { rewrite GNE. xsimpl. }
...@@ -420,7 +422,7 @@ Proof using. (* trivial *) ...@@ -420,7 +422,7 @@ Proof using. (* trivial *)
{ => j Hj Ej. rew_array~. case_if~. { => j Hj Ej. rew_array~. case_if~.
{ apply~ E1. rew_array~. case_if~. } } { apply~ E1. rew_array~. case_if~. } }
{ => j Hj. rew_array~. case_if. { => j Hj. rew_array~. case_if.
{ rename j into i. iff; auto_false. } { subst. rename j into i. iff; auto_false. }
{ rewrite~ <- E2. rew_array~. case_if*. } } { rewrite~ <- E2. rew_array~. case_if*. } }
Qed. Qed.
...@@ -464,9 +466,9 @@ Lemma inv_empty : forall G n, ...@@ -464,9 +466,9 @@ Lemma inv_empty : forall G n,
inv G \{} (make n White). inv G \{} (make n White).
Proof using. (* trivial *) Proof using. (* trivial *)
=>> Hn. splits. =>> Hn. splits.
{ hnf in Hn. rew_arr*. } { hnf in Hn. rew_array*. auto. (* TODO: fix tactic *) }
{ =>> Hi Ci. false. rew_arr~ in Ci. false. } { =>> Hi Ci. false. rew_array~ in Ci. false. }
{ => i Hi Ci. false. rew_arr~ in Ci. false. } { => i Hi Ci. false. rew_array~ in Ci. false. }
Qed. Qed.
Lemma inv_add_root : forall G L C i, Lemma inv_add_root : forall G L C i,
...@@ -476,7 +478,8 @@ Proof using. (* trivial *) ...@@ -476,7 +478,8 @@ Proof using. (* trivial *)
=>> (I1&I2&I3). splits. =>> (I1&I2&I3). splits.
{ auto. } { auto. }
{ auto. } { auto. }
{ => j Hj Cj. forwards~ (r&Hr&Pr): I3 j. exists* r. } { => j Hj Cj. forwards~ (r&Hr&Pr): I3 j.
exists* r. splits*. rew_set. eauto. (* TODO: tactic *) }
Qed. Qed.
Lemma inv_gray_root : forall G R C i, Lemma inv_gray_root : forall G R C i,
...@@ -486,7 +489,7 @@ Lemma inv_gray_root : forall G R C i, ...@@ -486,7 +489,7 @@ Lemma inv_gray_root : forall G R C i,
inv G R (C[i := Gray]). inv G R (C[i := Gray]).
Proof using. (* trivial *) Proof using. (* trivial *)
=>> Ci Hi (I1&I2&I3). splits. =>> Ci Hi (I1&I2&I3). splits.
{ rew_arr~. } { rew_array~. }
{ => j k Hjk. rew_array~. => Cjk. case_if; auto_false. { => j k Hjk. rew_array~. => Cjk. case_if; auto_false.
case_if. applys* I2. } case_if. applys* I2. }
{ => j Hj. rew_array~. case_if; auto_false. } { => j Hj. rew_array~. case_if; auto_false. }
...@@ -499,11 +502,11 @@ Lemma inv_evolution_black : forall G R C' i, ...@@ -499,11 +502,11 @@ Lemma inv_evolution_black : forall G R C' i,
inv G R (C'[i := Black]). inv G R (C'[i := Black]).
Proof using. (* trivial *) Proof using. (* trivial *)
=>> (I1&I2&I3) Ri Wi. splits. =>> (I1&I2&I3) Ri Wi. splits.
{ rew_arr~. } { rew_array~. }
{ => j k Hjk. rew_array~. => M. case_if; auto_false. case_if. { => j k Hjk. rew_array~. => M. case_if; auto_false. case_if.
{ applys Wi. rewrite~ out_edges_has_edge. } { subst. applys Wi. rewrite~ out_edges_has_edge. }
{ applys* I2. } } { applys* I2. } }
{ => j Hj. rew_array~. case_if; [|auto]. { => j Hj. rew_array~. case_if; [subst|auto].
=> _. rename j into i. eauto. } => _. rename j into i. eauto. }
Qed. Qed.
...@@ -550,7 +553,7 @@ Proof using. ...@@ -550,7 +553,7 @@ Proof using.
{ xret. unfold hinv. xsimpl~. } } { xret. unfold hinv. xsimpl~. } }
{ unfold hinv. xpull ;=> C' I1 (F1&F2&F3). xsimpl. splits. { unfold hinv. xpull ;=> C' I1 (F1&F2&F3). xsimpl. splits.
{ auto. } (* trivial *) { auto. } (* trivial *)
{ => k Hk. set_in Hk; auto. } (* trivial *) { => k Hk. rew_set in Hk. destruct~ Hk. subst~. } (* trivial *)
{ auto. } } } (* trivial *) { auto. } } } (* trivial *)
{ clears f. unfold loop_inv, hinv. xsimpl. split. { clears f. unfold loop_inv, hinv. xsimpl. split.
{ applys evolution_refl. } { applys evolution_refl. }
...@@ -559,7 +562,7 @@ Proof using. ...@@ -559,7 +562,7 @@ Proof using.
{ unfold loop_inv, hinv. xpull ;=> C' I1 (F1&F2). { unfold loop_inv, hinv. xpull ;=> C' I1 (F1&F2).
xapps~. xsimpl. split. xapps~. xsimpl. split.
{ subst C1. applys* evolution_write_black. } { subst C1. applys* evolution_write_black. }
{ rew_arr~. } (* trivial *) { rew_array~. case_if~. } (* trivial *)
{ applys* inv_evolution_black. } } { applys* inv_evolution_black. } }
Qed. Qed.
...@@ -577,7 +580,7 @@ Proof using. ...@@ -577,7 +580,7 @@ Proof using.
xcf. xapp. => Hn. xapp. xcf. xapp. => Hn. xapp.
{ applys (proj1 Hn). } (* trivial *) { applys (proj1 Hn). } (* trivial *)
=> C0 HC0. => C0 HC0.
asserts N0: (no_gray C0). { subst. => i Hi. rew_arr; auto_false. } (* trivial *) asserts N0: (no_gray C0). { subst. => i Hi. rew_array; auto_false. } (* trivial *)
xfun as f. xfun as f.
set (loop_inv := fun L C => hinv G (set_of_list L) C g c 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 ]). \* \[ evolution C0 C /\ all_black_in (set_of_list L) C ]).
...@@ -586,26 +589,31 @@ Proof using. ...@@ -586,26 +589,31 @@ Proof using.
unfold loop_inv, hinv. xpull ;=> C HI (HC1&HC2). unfold loop_inv, hinv. xpull ;=> C HI (HC1&HC2).
xapp. clears f. xapps~. xapps~. xpolymorphic_eq. xif. xapp. clears f. xapps~. xapps~. xpolymorphic_eq. xif.
{ xapp G (\{i} \u set_of_list L) C. { xapp G (\{i} \u set_of_list L) C.
{ exists i. split~. applys* reachable_self. } (* trivial *) { exists i. split.
{ rew_set; eauto. } (* TODO: tactic *)
{ applys* reachable_self. } } (* trivial *)
{ auto. } (* trivial *) { auto. } (* trivial *)
{ unfold hinv. xsimpl*. applys* inv_add_root. } { unfold hinv. xsimpl*. applys* inv_add_root. }
{ unfold loop_inv, hinv. intros u. xpull ;=> C' I1 (F1&F2). { unfold loop_inv, hinv. intros u. xpull ;=> C' I1 (F1&F2).
rew_set_of_list. xsimpl. rew_set_of_list. xsimpl.
{ splits. (* trivial *) { splits. (* trivial *)
{ applys~ evolution_trans F1. } (* trivial *) { applys~ evolution_trans F1. } (* trivial *)
{ => j Hj. set_in Hj; eauto. applys~ (proj1 F1). } } (* trivial *) { => j Hj. rew_set in Hj. destruct Hj. (* trivial *)
{ applys~ (proj1 F1). } { subst~. } } } (* trivial *)
{ rewrite~ union_comm. } } } (* trivial *) { rewrite~ union_comm. } } } (* trivial *)
{ xret. unfold loop_inv, hinv. rew_set_of_list. xsimpl~. split. { xret. unfold loop_inv, hinv. rew_set_of_list. xsimpl~. split.
{ auto. } (* trivial *) { auto. } (* trivial *)
{ => j Hj. set_in Hj; eauto. cases (C[i]); auto_false. (* trivial *) { => j Hj. rew_set in Hj. destruct Hj.
false~ N0 i. forwards~ (_&?): (proj2 HC1). } (* trivial *) { 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 *) { cases~ (C[i]). (* trivial *)
{ false. } (* trivial *) { false. } (* trivial *)
{ false~ N0 i. forwards~ (?&?): (proj2 HC1) i. } (* trivial *) { false~ N0 i. forwards~ (?&?): (proj2 HC1) i. } (* trivial *)
{ rewrite~ union_comm. applys* inv_add_root. } } } } { rewrite~ union_comm. applys* inv_add_root. } } } }
{ unfold loop_inv, hinv. rew_set_of_list. xsimpl. split. { unfold loop_inv, hinv. rew_set_of_list. xsimpl. split.
{ applys* evolution_refl. } (* trivial *) { applys* evolution_refl. } (* trivial *)
{ => r Hr. set_in Hr. } (* trivial *) { => r Hr. rew_set in Hr. false. } (* trivial *)
{ subst C0. applys* inv_empty. } } (* trivial *) { subst C0. applys* inv_empty. } } (* trivial *)
unfold loop_inv, hinv. => C1. xpull ;=> (I1&I2&I3) (H1&H2). unfold loop_inv, hinv. => C1. xpull ;=> (I1&I2&I3) (H1&H2).
xret. xsimpl. split. xret. xsimpl. split.
......
...@@ -2,6 +2,7 @@ Set Implicit Arguments. ...@@ -2,6 +2,7 @@ Set Implicit Arguments.
Require Import CFML.CFLib. Require Import CFML.CFLib.
Require Import Demo_ml. Require Import Demo_ml.
Require Import Stdlib. Require Import Stdlib.
Require LibListZ.
Import ZsubNoSimpl. Import ZsubNoSimpl.
Open Scope tag_scope. Open Scope tag_scope.
......
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