diff --git a/examples/DFS/DFS_proof.v b/examples/DFS/DFS_proof.v index 9977a871832d6e74a27ce66fcc4d8682cf2b21cf..2b19811a9a5a32cde76d970005478793aab92c97 100644 --- a/examples/DFS/DFS_proof.v +++ b/examples/DFS/DFS_proof.v @@ -54,15 +54,15 @@ Global Opaque heap_contains. (* Future work: -Lemma heap_contains_intro_hexists_1 : forall A (J:A->hprop) H, +Lemma heap_contains_intro_hexists_1 : forall A (J:A->hprop) H, H \c (Hexists x, H \* J x). -Proof using. +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, +Lemma heap_contains_intro_hexists_2 : forall A1 A2 (J:A1->A2->hprop) H, H \c (Hexists x y, H \* J x y). -Proof using. +Proof using. intros. applys heap_contains_intro (Hexists x1 x2, J x1 x2); hsimpl. Qed. @@ -80,7 +80,7 @@ Lemma heap_contains_hexists2 : forall (H1 : hprop) A1 A2 (J J2:A1->A2->hprop), (forall x1 x2, (J x1 x2 ==> H1 \* J2 x1 x2)) -> (forall x1 x2, (H1 \* J2 x1 x2 ==> J x1 x2)) -> (* or just, [forall x, J x = H1 \* J2 x] *) (H1 \c (Hexists x1 x2, J x1 x2)). -Proof using. +Proof using. introv M1 M2. hnf. exists (Hexists x1 x2, J2 x1 x2). applys antisym_pred_incl. { hpull ;=> x1 x2. hchanges (M1 x1 x2). } { hpull ;=> x1 x2. hchanges (M2 x1 x2). } @@ -699,9 +699,3 @@ Qed. Hint Extern 1 (RegisterSpec dfs_main) => Provide dfs_main_spec. - - - - - -