Commit 4632198a authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Simplify local stuff.

parent 15c4ffc0
......@@ -212,31 +212,6 @@ Lemma himpl_frame_l : forall H2 H1 H1',
(H1 \* H2) ==> (H1' \* H2).
Proof using. introv W (h1&h2&?). exists* h1 h2. Qed.
Lemma local_local_aux : forall (B:Type),
let local := fun (F:(hprop->(B->hprop)->Prop)) (H:hprop) (Q:B->hprop) =>
( forall h, H h -> exists H1 H2 Q1,
(H1 \* H2) h
/\ F H1 Q1
/\ Q1 \*+ H2 ===> Q \*+ \Top) in
(\Top \* \Top = \Top) ->
forall F (H:hprop) (Q:B->hprop),
local (local F) H Q ->
local F H Q.
Proof using.
intros B local R F H Q M. introv PH.
lets (H1&H2&Q1&PH12&N&Qle): M (rm PH).
lets (h1&h2&PH1&PH2&Ph12&Fh12): (rm PH12).
lets (H1'&H2'&Q1'&PH12'&N'&Qle'): N (rm PH1).
exists H1' (H2' \* H2) Q1'. splits.
{ rewrite <- hstar_assoc. exists~ h1 h2. }
{ auto. }
{ intros x. lets R1: himpl_frame_l \Top ((rm Qle) x).
lets R2: himpl_frame_l H2 ((rm Qle') x).
rewrite <- R. repeat rewrite hstar_assoc in *.
applys himpl_trans R1. applys himpl_trans R2.
rewrite~ (@hstar_comm H2). }
Qed.
End Properties.
End SepBasicCore.
......@@ -468,14 +443,15 @@ Lemma is_local_triple : forall t,
Proof using.
intros. applys pred_ext_2. intros H Q. iff M.
{ intros h Hh. forwards (h'&v&N1&N2): M \[] h. { hhsimpl. }
exists H \[] Q. splits~. { hhsimpl. } { hsimpl. } }
exists H \[] Q. hhsimpl. splits~. hsimpl. }
{ intros H' h Hh. lets (h1&h2&N1&N2&N3&N4): Hh. hnf in M.
lets (H1&H2&Q1&R1&R2&R3): M N1.
forwards (h'&v&S1&S2): R2 (H2\*H') h.
lets (H1&H2&Q1&R): M N1. rewrite <-hstar_assoc, hstar_comm, hstar_pure in R.
lets ((R1&R2)&R3): R.
forwards (h'&v&S1&S2): R1 (H2\*H') h.
{ subst h. rewrite <- hstar_assoc. exists~ h1 h2. }
exists h' v. splits~. rewrite <- htop_hstar_htop.
applys himpl_inv S2.
hchange (R3 v). rew_heap.
hchange (R2 v). rew_heap.
rewrite (hstar_comm_assoc \Top H'). hsimpl. }
Qed.
......
......@@ -417,31 +417,6 @@ Lemma himpl_frame_l : forall H2 H1 H1',
(H1 \* H2) ==> (H1' \* H2).
Proof using. introv W (h1&h2&?). exists* h1 h2. Qed.
Lemma local_local_aux : forall (B:Type),
let local := fun (F:(hprop->(B->hprop)->Prop)) (H:hprop) (Q:B->hprop) =>
( forall h, H h -> exists H1 H2 Q1,
(H1 \* H2) h
/\ F H1 Q1
/\ Q1 \*+ H2 ===> Q \*+ \Top) in
(\Top \* \Top = \Top) ->
forall F (H:hprop) (Q:B->hprop),
local (local F) H Q ->
local F H Q.
Proof using.
intros B local R F H Q M. introv PH.
lets (H1&H2&Q1&PH12&N&Qle): M (rm PH).
lets (h1&h2&PH1&PH2&Ph12&Fh12): (rm PH12).
lets (H1'&H2'&Q1'&PH12'&N'&Qle'): N (rm PH1).
exists H1' (H2' \* H2) Q1'. splits.
{ rewrite <- hstar_assoc. exists~ h1 h2. }
{ auto. }
{ intros x. lets R1: himpl_frame_l \Top ((rm Qle) x).
lets R2: himpl_frame_l H2 ((rm Qle') x).
rewrite <- R. repeat rewrite hstar_assoc in *.
applys himpl_trans R1. applys himpl_trans R2.
rewrite~ (@hstar_comm H2). }
Qed.
End Properties.
End SepCreditsCore.
......@@ -788,15 +763,15 @@ Proof using.
intros. applys pred_ext_2. intros H Q. iff M.
{ intros h Hh. forwards (h'&v&N1&N2): M \[] h.
{ hhsimpl. }
exists H \[] Q. splits~. { hhsimpl. } { hsimpl. } }
exists H \[] Q. hhsimpl. split~. hsimpl. }
{ intros H' h Hh. lets (h1&h2&N1&N2&N3&N4): Hh. hnf in M.
lets (H1&H2&Q1&R1&R2&R3): M N1.
forwards (n&h'&v&S1&S2&S3): R2 (H2\*H') h.
lets (H1&H2&Q1&R): M N1. rewrite <-hstar_assoc, hstar_comm, hstar_pure in R.
lets ((R1&R2)&R3): R.
forwards (n&h'&v&S1&S2&S3): R1 (H2\*H') h.
{ subst h. rewrite <- hstar_assoc. exists~ h1 h2. }
exists n h' v. splits~. rewrite <- htop_hstar_htop.
applys himpl_inv S2.
hchange (R3 v). rew_heap.
rewrite (hstar_comm_assoc \Top H'). hsimpl. }
hchange (R2 v). hsimpl. }
Qed.
......
......@@ -426,22 +426,12 @@ Definition Triple (t:trm) `{EA:Enc A} (H:hprop) (Q:A->hprop) :=
Lemma is_local_Triple : forall t A `{EA:Enc A},
is_local (@Triple t A EA).
Proof using.
unfold is_local, Triple, triple. intros.
unfold is_local, Triple. intros.
applys pred_ext_2. intros H Q. iff M.
{ intros h Hh. forwards (h'&v&N1&N2): M \[] h. { hhsimpl. }
exists H \[] Q. splits~. { hhsimpl. } { hsimpl. } }
{ intros H' h Hh. lets (h1&h2&N1&N2&N3&N4): Hh. hnf in M.
lets (H1&H2&Q1&R1&R2&R3): M N1.
forwards (h'&v&S1&S2): R2 (H2\*H') h.
{ subst h. rewrite <- hstar_assoc. exists~ h1 h2. }
exists h' v. splits~. rewrite <- htop_hstar_htop.
applys himpl_inv S2.
(* MODIFIED FOR LIFTING *)
lets R3': Post_himpl R3.
do 2 rewrite Post_star in R3'.
hchange (R3' v). rew_heap.
rewrite (hstar_comm_assoc \Top H'). hsimpl. }
Qed. (* TODO: see if possible to reuse is_local_triple *)
{ unfold local. hsimpl. split*. hsimpl. }
{ rewrite is_local_triple. unfold local. hchange M. hsimpl=>H1 H2 Q1 [P1 P2].
split*. apply Post_himpl in P2. rewrite !Post_star in P2. auto. }
Qed.
(** Extension of [xlocal] tactic *)
......
......@@ -555,31 +555,6 @@ Lemma himpl_frame_l : forall H2 H1 H1',
(H1 \* H2) ==> (H1' \* H2).
Proof using. introv W (h1&h2&?). exists* h1 h2. Qed.
Lemma local_local_aux : forall (B:Type),
let local := fun (F:(hprop->(B->hprop)->Prop)) (H:hprop) (Q:B->hprop) =>
( forall h, H h -> exists H1 H2 Q1,
(H1 \* H2) h
/\ F H1 Q1
/\ Q1 \*+ H2 ===> Q \*+ \Top) in
(\Top \* \Top = \Top) ->
forall F (H:hprop) (Q:B->hprop),
local (local F) H Q ->
local F H Q.
Proof using.
intros B local R F H Q M. introv PH.
lets (H1&H2&Q1&PH12&N&Qle): M (rm PH).
lets (h1&h2&PH1&PH2&Ph12&Fh12): (rm PH12).
lets (H1'&H2'&Q1'&PH12'&N'&Qle'): N (rm PH1).
exists H1' (H2' \* H2) Q1'. splits.
{ rewrite <- hstar_assoc. exists~ h1 h2. }
{ auto. }
{ intros x. lets R1: himpl_frame_l \Top ((rm Qle) x).
lets R2: himpl_frame_l H2 ((rm Qle') x).
rewrite <- R. repeat rewrite hstar_assoc in *.
applys himpl_trans R1. applys himpl_trans R2.
rewrite~ (@hstar_comm H2). }
Qed.
End Properties.
End SepROCore.
......
......@@ -234,22 +234,6 @@ Parameter himpl_frame_l : forall H2 H1 H1',
H1 ==> H1' ->
(H1 \* H2) ==> (H1' \* H2).
(** One additional technical lemma, useful for helping with
the setup of tactics for Separation Logic goals.
It essentially asserts that the predicate called [local],
and defined later in [SepTactics.v], is idempotent. *)
Parameter local_local_aux : forall B,
let local := fun (F:(hprop->(B->hprop)->Prop)) (H:hprop) (Q:B->hprop) =>
( forall h, H h -> exists H1 H2 Q1,
(H1 \* H2) h
/\ F H1 Q1
/\ Q1 \*+ H2 ===> Q \*+ \Top) in
(\Top \* \Top = \Top) ->
forall (F:(hprop->(B->hprop)->Prop)) (H:hprop) (Q:B->hprop),
local (local F) H Q ->
local F H Q.
End SepLogicCore.
......
......@@ -1391,10 +1391,8 @@ Notation "'~~' B" := (hprop->(B->hprop)->Prop)
Definition local B (F:~~B) : ~~B :=
fun (H:hprop) (Q:B->hprop) =>
forall h, H h -> exists H1 H2 Q1,
(H1 \* H2) h
/\ F H1 Q1
/\ Q1 \*+ H2 ===> Q \*+ \Top.
H ==> Hexists H1 H2 Q1,
H1 \* H2 \* \[F H1 Q1 /\ Q1 \*+ H2 ===> Q \*+ \Top].
(** The [is_local] predicate asserts that a predicate is subject
to all the rules that the [local] predicate transformer supports. *)
......@@ -1408,7 +1406,6 @@ Definition is_local B (F:~~B) :=
Definition is_local_pred A B (S:A->~~B) :=
forall x, is_local (S x).
(* ---------------------------------------------------------------------- *)
(* ** Properties of [local] *)
......@@ -1422,8 +1419,7 @@ Lemma local_erase : forall F H Q,
F H Q ->
local F H Q.
Proof using.
intros. exists H \[] Q. splits.
rew_heap~. auto. hsimpl.
intros. unfold local. hsimpl. split. eauto. hsimpl.
Qed.
(** [local] is a covariant transformer w.r.t. predicate inclusion *)
......@@ -1432,9 +1428,8 @@ Lemma local_weaken_body : forall F F',
F ===> F' ->
local F ===> local F'.
Proof using.
introv M. intros H Q N. introv Hh.
destruct (N _ Hh) as (H1&H2&Q1&P1&P2&P3).
specializes M H1 Q1. exists___*.
unfold local. introv M. intros H Q N. eapply himpl_trans. apply N.
hsimpl;=> H1 H2 Q' [P1 P2]. split; [apply M, P1|auto].
Qed.
(** [local] is idempotent, i.e. nested applications
......@@ -1444,7 +1439,9 @@ Lemma local_local : forall F,
local (local F) = local F.
Proof using.
extens. intros H Q. iff M.
{ applys (@local_local_aux B) M. applys htop_hstar_htop. }
{ unfold local. eapply himpl_trans; [now apply M|]. hpull;=>H1 H2 Q1 [P1 P2].
unfold local in P1. hchange P1. hpull;=>H1' H2' Q1' [P1' P2'].
apply (himpl_hexists_r H1'). hsimpl. splits*. hchange P2'. hchange P2. hsimpl. }
{ apply~ local_erase. }
Qed.
......@@ -1488,8 +1485,7 @@ Lemma local_frame_htop : forall F H H1 H2 Q1 Q,
Q1 \*+ H2 ===> Q \*+ \Top ->
F H Q.
Proof using.
introv L M WH WQ. rewrite L. introv Ph.
exists H1 H2 Q1. splits; rew_heap~.
introv L M WH WQ. rewrite L. unfold local. hchange WH. hsimpl. split*.
Qed.
(** Weaken and frame properties from [local] *)
......@@ -1501,8 +1497,7 @@ Lemma local_frame : forall H1 H2 Q1 F H Q,
Q1 \*+ H2 ===> Q ->
F H Q.
Proof using.
introv L M WH WQ. rewrite L. introv Ph.
exists H1 H2 Q1. splits; rew_heap~.
introv L M WH WQ. rewrite L. unfold local. hchange WH. hsimpl. splits*.
hchange WQ. hsimpl.
Qed.
......@@ -1549,8 +1544,7 @@ Lemma local_htop_post : forall Q' F H Q,
Q' ===> Q \*+ \Top ->
F H Q.
Proof using.
introv L M W. rewrite L. introv Ph.
exists H \[] Q'. splits; rew_heap~.
introv L M W. rewrite L. unfold local. hsimpl. splits*. hchange W. hsimpl.
Qed.
(** Variant of the above, useful for tactics to specify
......@@ -1562,11 +1556,8 @@ Lemma local_htop_pre_on : forall HG H' F H Q,
F H' Q ->
F H Q.
Proof using.
introv L M W. rewrite L. introv Ph.
exists H' HG Q. splits.
rewrite hstar_comm. apply~ M.
auto.
hsimpl.
introv L M W. rewrite L. unfold local. apply (himpl_hexists_r H').
hsimpl*. splits*. hsimpl.
Qed.
(** Weakening on pre and post with gc -postfrom [local] *)
......@@ -1619,9 +1610,7 @@ Lemma local_extract_hprop : forall F H P Q,
(P -> F H Q) ->
F (\[P] \* H) Q.
Proof using.
introv L M. rewrite L. intros h Hh.
rewrite hstar_pure in Hh. destruct Hh as (HP&Hh).
exists H \[] Q. splits; rew_heap~. hsimpl.
introv L M. rewrite L. unfold local. hsimpl=>HP. splits*. hsimpl.
Qed.
(** Extraction of existentials from [local] *)
......@@ -1631,8 +1620,7 @@ Lemma local_extract_hexists_heap : forall F A (J:A->hprop) Q,
(forall x, F (J x) Q) ->
F (hexists J) Q.
Proof using.
introv L M. rewrite L. introv (x&Hx).
exists (J x) \[] Q. splits~. rew_heap~. hsimpl.
introv L M. rewrite L. unfold local. hsimpl;=>x. splits*. hsimpl.
Qed.
(** Extraction of existentials below a star from [local] *)
......@@ -1642,12 +1630,8 @@ Lemma local_extract_hexists : forall F H A (J:A->hprop) Q,
(forall x, F ((J x) \* H) Q) ->
F (hexists J \* H) Q.
Proof using.
introv L M. rewrite L. intros h Hh.
rewrite hstar_hexists in Hh.
destruct Hh as (x&Hh).
exists (J x \* H) \[] Q. splits~.
{ rew_heap~. }
{ hsimpl. }
introv L M. rewrite L. unfold local. hpull;=>x.
apply (himpl_hexists_r (J x \* H)). hsimpl. splits*. hsimpl.
Qed.
(** Extraction of heap representation from [local] *)
......@@ -1657,9 +1641,8 @@ Lemma local_name_heap : forall F H Q,
(forall h, H h -> F (= h) Q) ->
F H Q.
Proof using.
introv L M. rewrite L. introv Hh. exists (= h) \[] Q. splits~.
{ rewrite hstar_comm. rewrite hempty_eq_hpure_true. rewrite~ hstar_pure. }
{ hsimpl. }
introv L M. rewrite L. intros h Hh%M. exists (= h) \[] Q.
rewrite hstar_hempty_l, hstar_comm, hstar_pure. splits*. splits*. hsimpl.
Qed.
(** Extraction of pure facts from the pre-condition under local *)
......@@ -1681,8 +1664,7 @@ Lemma local_extract_false : forall F H Q,
(forall H' Q', F H' Q' -> False) ->
(H ==> \[False]).
Proof using.
introv M N. intros h Hh. lets (H1&H2&Q1&R1&R2&R3): (rm M) (rm Hh).
false N R2.
introv M N. hchange M. hpull=>H' H1 Q' [HF _]. edestruct N. eauto.
Qed.
End IsLocal.
......
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