Commit deeb1d12 authored by Armaël Guéneau's avatar Armaël Guéneau

DFS_proof: whitespace cleanup

parent 6c57d34b
......@@ -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.
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