Commit f1df8cae authored by charguer's avatar charguer

ramified_frame

parent ebc91424
......@@ -18,7 +18,6 @@ Implicit Types n : int.
Implicit Types v : val.
Import TripleLowLevel. (* TODO: remove *)
(* To move and factorize *)
Notation "F 'PRE' H 'POST' Q" :=
......@@ -77,7 +76,7 @@ Lemma rule_get : forall v l,
(fun x => \[x = v] \* l ~~~> v).
Proof using.
intros. applys rule_frame_read_only_conseq (l ~~~> v).
{ hsimpl. } { applys normal_single. (* todo: normal_hsingle? *) }
{ hsimpl. } { applys normal_hsingle. (* todo: normal_hsingle? *) }
{ rew_heap. applys rule_get_ro. }
{ auto. }
Qed.
......@@ -107,7 +106,7 @@ Lemma rule_frame_conseq : forall t H1 Q1 H2 H Q,
triple t H Q.
Proof using. intros. applys* rule_consequence. applys* rule_frame. Qed.
Hint Resolve normal_single.
Hint Resolve normal_hsingle.
......
......@@ -95,6 +95,11 @@ Definition hstar (H1 H2 : hprop) : hprop :=
Definition hexists A (J : A -> hprop) : hprop :=
fun h => exists x, J x h.
(** Lifting of univerals *)
Definition hforall A (J : A -> hprop) : hprop :=
fun h => forall x, J x h.
(** The top heap predicate: [ \Top ], same as [Hexists H, H] *)
Definition htop :=
......@@ -198,6 +203,12 @@ Proof using.
{ destruct M as (x&(h1&h2&M1&M2&D&U)). exists h1 h2. splits~. exists~ x. }
Qed.
Lemma hstar_hforall : forall H A (J:A->hprop),
(hforall J) \* H ==> hforall (J \*+ H).
Proof using.
intros. intros h M. destruct M as (h1&h2&M1&M2&D&U). intros x. exists~ h1 h2.
Qed.
Lemma himpl_frame_l : forall H2 H1 H1',
H1 ==> H1' ->
(H1 \* H2) ==> (H1' \* H2).
......
......@@ -171,6 +171,9 @@ Definition hstar (H1 H2 : hprop) : hprop :=
Definition hexists A (J : A -> hprop) : hprop :=
fun h => exists x, J x h.
Definition hforall A (J : A -> hprop) : hprop :=
fun h => forall x, J x h.
Definition htop :=
hexists (fun (H:hprop) => H).
......@@ -403,6 +406,12 @@ Proof using.
{ destruct M as (x&(h1&h2&M1&M2&D&U)). exists h1 h2. splits~. exists~ x. }
Qed.
Lemma hstar_hforall : forall H A (J:A->hprop),
(hforall J) \* H ==> hforall (J \*+ H).
Proof using.
intros. intros h M. destruct M as (h1&h2&M1&M2&D&U). intros x. exists~ h1 h2.
Qed.
Lemma himpl_frame_l : forall H2 H1 H1',
H1 ==> H1' ->
(H1 \* H2) ==> (H1' \* H2).
......
......@@ -121,6 +121,9 @@ Program Definition hstar (H1 H2 : hprop) : hprop :=
Definition hexists A (J : A -> hprop) : hprop :=
fun h => exists x, J x h.
Definition hforall A (J : A -> hprop) : hprop :=
fun h => forall x, J x h.
Definition htop :=
hexists (fun (H:hprop) => H).
......@@ -545,6 +548,12 @@ Proof using.
{ destruct M as (x&(h1&h2&M1&M2&D&U)). exists h1 h2. splits~. exists~ x. }
Qed.
Lemma hstar_hforall : forall H A (J:A->hprop),
(hforall J) \* H ==> hforall (J \*+ H).
Proof using.
intros. intros h M. destruct M as (h1&h2&M1&M2&D&U). intros x. exists~ h1 h2.
Qed.
Lemma himpl_frame_l : forall H2 H1 H1',
H1 ==> H1' ->
(H1 \* H2) ==> (H1' \* H2).
......@@ -586,13 +595,6 @@ End SepROCore.
Module Export SepROTactics := SepLogicTactics SepROCore.
(* ---------------------------------------------------------------------- *)
(* ** Disjunction heap *)
Definition hor (H1 H2 : hprop) : hprop :=
fun h => H1 h \/ H2 h.
(* ---------------------------------------------------------------------- *)
(* ** Singleton heap *)
......@@ -651,34 +653,34 @@ Definition normal_post A (Q:A->hprop) :=
Arguments normal_post [A].
Lemma normal_empty :
Lemma normal_hempty :
normal \[].
Proof using.
Transparent hempty hpure.
introv M. unfolds hempty, hpure. subst. autos*.
Qed.
Lemma normal_pure : forall P,
Lemma normal_hpure : forall P,
normal \[P].
Proof using.
Transparent hpure.
introv (p&M). unfolds hempty. subst. auto.
Qed.
Lemma normal_empty' : (* simpler proof *)
Lemma normal_hempty' : (* simpler proof *)
normal \[].
Proof using.
intros. rewrite hempty_eq_hpure_true. applys~ normal_pure.
intros. rewrite hempty_eq_hpure_true. applys~ normal_hpure.
Qed.
Lemma normal_single : forall l v,
Lemma normal_hsingle : forall l v,
normal (hsingle l v).
Proof using.
Transparent hsingle.
introv M. unfolds hsingle. autos*.
Qed.
Lemma normal_star : forall H1 H2,
Lemma normal_hstar : forall H1 H2,
normal H1 ->
normal H2 ->
normal (H1 \* H2).
......@@ -695,7 +697,7 @@ Lemma normal_hexists : forall A (J:A->hprop),
normal (hexists J).
Proof using. introv M (x&N). rewrites~ (>> M N). Qed.
Lemma normal_or : forall H1 H2,
Lemma normal_hor : forall H1 H2,
normal H1 ->
normal H2 ->
normal (hor H1 H2).
......@@ -705,13 +707,25 @@ Proof using.
{ rewrites~ (>> M2 N). }
Qed.
Lemma normal_hand_l : forall H1 H2,
normal H1 ->
normal (hand H1 H2).
Proof using. introv M (N1&N2). forwards*: M N1. Qed.
Lemma normal_hand_r : forall H1 H2,
normal H2 ->
normal (hand H1 H2).
Proof using. introv M (N1&N2). forwards*: M N2. Qed.
Lemma normal_himpl : forall H1 H2,
normal H2 ->
(H1 ==> H2) ->
normal H1.
Proof using. introv HS HI M. lets: HI M. applys* HS. Qed.
Lemma normal_pure_star_hprop : forall (P:Prop) H,
(* Note: normal_hwand is not true *)
Lemma normal_hpure_star_hprop : forall (P:Prop) H,
(P -> normal H) ->
normal (\[P] \* H).
Proof using.
......@@ -829,7 +843,6 @@ Arguments RO_star : clear implicits.
(* ********************************************************************** *)
(* * Reasoning rules, low-level proofs *)
Module TripleLowLevel.
Hint Resolve heap_compat_union_l heap_compat_union_r.
Hint Resolve fmap_agree_empty_l fmap_agree_empty_r.
......@@ -1069,6 +1082,16 @@ Proof using.
{ exists~ hx hb. } }
Qed.
Lemma rule_frame : forall t H1 Q1 H2,
triple t H1 Q1 ->
normal H2 ->
triple t (H1 \* H2) (Q1 \*+ H2).
Proof using.
introv M N. applys~ rule_frame_read_only.
applys rule_consequence (H1 \* \Top). hsimpl.
applys* rule_htop_pre. auto.
Qed.
Lemma rule_red : forall t1 t2 H Q,
(forall m m' r, red m t1 m' r -> red m t2 m' r) ->
triple t1 H Q ->
......@@ -1163,7 +1186,7 @@ Proof using.
introv M. forwards~ M': M.
applys_eq (>> rule_let \[] (fun x => \[x = v1])) 2.
{ applys rule_val. rewrite <- (@hstar_hempty_r \[v1=v1]).
applys~ himpl_hprop_r. applys normal_empty. }
applys~ himpl_hprop_r. applys normal_hempty. }
{ intros X. applys rule_extract_hprop. applys M. }
{ rewrite~ hstar_hempty_l. }
Qed.
......@@ -1263,17 +1286,20 @@ Proof using.
Qed.
(* ---------------------------------------------------------------------- *)
(* ********************************************************************** *)
(* * Extension: [normally] modality *)
(* * Ramified read-only frame rule *)
Module Normally.
(* ---------------------------------------------------------------------- *)
(* ** Definition of the [normally] modality *)
Definition normally H :=
fun h => H h /\ h^r = fmap_empty.
Lemma normal_normally : forall H,
normal (normally H).
Proof using. introv (M&E). auto. Qed.
Lemma normally_erase : forall H,
normally H ==> H.
Proof using. intros H h (N&E). auto. Qed.
......@@ -1319,19 +1345,53 @@ Proof using.
{ intros h (x&(N&E)). split~. exists~ x. }
Qed.
Lemma normally_hforall : forall A `{IA:Inhab A} (J:A->hprop),
normally (hforall J) = hforall (fun x => normally (J x)).
Proof using.
intros. unfolds normally, hforall. applys himpl_antisym.
{ intros h N x. autos*. }
{ intros h N. lets (_&E): N arbitrary. split.
{ intros x. forwards*: N x. }
{ auto. } }
Qed.
Lemma normally_hstar : forall H1 H2,
normally H1 \* normally H2 = normally (H1 \* H2).
normally (H1 \* H2) = normally H1 \* normally H2.
Proof using.
intros. applys himpl_antisym.
{ intros. intros h (h1&h2&(M1&E1)&(M2&E2)&M3&M4). split.
{ exists~ h1 h2. }
{ subst h. rew_heap~. rewrite E1,E2. rew_fmap~. } }
{ intros h ((h1&h2&M1&M2&M3&M4)&E). subst h. rew_heap~ in E.
exists h1 h2. splits~.
{ split~. applys* fmap_union_eq_empty_inv_l. }
{ split~. applys* fmap_union_eq_empty_inv_r. } }
{ intros. intros h (h1&h2&(M1&E1)&(M2&E2)&M3&M4). split.
{ exists~ h1 h2. }
{ subst h. rew_heap~. rewrite E1,E2. rew_fmap~. } }
Qed.
Lemma normally_hwand : forall H1 H2,
normally (H1 \--* H2) ==> normally H1 \--* normally H2.
Proof using.
intros. unfold hwand. rewrite normally_hexists. hpull ;=> H3.
rewrite normally_hstar, normally_hpure. hsimpl (normally H3).
intros M. rewrite <- normally_hstar. applys~ normally_himpl.
Qed.
(** Alternative definition of [normal] in terms of [normally] *)
Definition normal' H :=
(H ==> normally H).
Lemma normal_eq_normal' :
normal = normal'.
Proof using.
applys pred_ext_1. intros H. unfold normal, normal', normally. iff N.
{ intros h M. split~. }
{ intros h M. forwards~ (R&E): N h. }
Qed.
(* ---------------------------------------------------------------------- *)
(* ** Read-only frame rule reformulated using normally *)
Lemma rule_frame_read_only' : forall t H1 Q1 H2,
triple t (H1 \* RO H2) Q1 ->
......@@ -1410,31 +1470,60 @@ Proof using.
{ exists~ hx hb. splits~. split~. } }
Qed.
Lemma rule_val : forall v H Q,
H ==> Q v ->
triple (trm_val v) (normally H) Q.
(** Derived rule with both frame and read-only frame, using normally *)
Lemma rule_frame_read_only_with_frame : forall t H1 H2 H3 Q1,
triple t (H1 \* RO H2) Q1 ->
triple t (H1 \* normally H2 \* normally H3) ((Q1 \*+ normally H2) \*+ normally H3).
Proof using.
introv M. intros h1 h2 D P1. destruct P1 as (P1&E1).
exists h1 v. splits~.
{ applys red_val. }
{ specializes M P1. applys~ on_rw_sub_base. }
introv M. rewrite <- hstar_assoc. applys rule_frame.
{ applys~ rule_frame_read_only'. }
{ applys normal_normally. }
Qed.
Definition normal' H :=
(H ==> normally H).
(* ---------------------------------------------------------------------- *)
(* ** Ramified read-only frame rule *)
Lemma normal_eq_normal' :
normal = normal'.
Lemma rule_ramified_frame_read_only_core : forall H2 t H Q H' Q',
triple t H' Q' ->
H = normally H2 \* (RO H2 \--* H') \* normally ((Q' \*+ normally H2) \---* Q) ->
triple t H Q.
Proof using.
applys pred_ext_1. intros H. unfold normal, normal', normally. iff N.
{ intros h M. split~. }
{ intros h M. forwards~ (R&E): N h. }
introv M W. subst H.
forwards K: rule_frame_read_only_with_frame t (RO H2 \--* H') H2 ((Q' \*+ normally H2) \---* Q) Q'.
{ applys~ rule_consequence M. hchanges (hwand_cancel (RO H2)). }
{ clear M. applys rule_consequence (rm K).
{ hsimpl. }
{ intros x. hchange (>> normally_erase (Q' \*+ normally H2 \---* Q)).
hchange (>> qwand_cancel_part (normally H2)).
hchange (qwand_himpl_hwand x). hchanges (hwand_cancel (Q' x)). } }
Qed.
Lemma rule_ramified_frame_read_only : forall t H Q H' Q',
triple t H' Q' ->
H ==> Hexists H2, normally H2
\* (RO H2 \--* (H' \* RO \Top))
\* normally ((Q' \*+ normally H2) \---* Q) ->
triple t H Q.
Proof using.
introv M W. applys~ rule_consequence Q (rm W).
applys rule_extract_hexists. intros H2.
asserts M': (triple t (H' \* RO \Top) Q').
{ applys* rule_consequence (H' \* \Top). hsimpl.
applys~ rule_htop_pre. }
clear M. applys* rule_ramified_frame_read_only_core.
Qed.
Lemma rule_ramified_frame_read_only_direct : forall H2 t H Q H' Q',
triple t H' Q' ->
H ==> normally H2 \* (RO H2 \--* (H' \* RO \Top)) \* normally ((Q' \*+ normally H2) \---* Q) ->
triple t H Q.
Proof using.
introv M W. applys rule_ramified_frame_read_only M. hchanges W.
Qed.
End Normally.
(* ---------------------------------------------------------------------- *)
......@@ -1442,4 +1531,30 @@ End Normally.
End TripleLowLevel.
......@@ -14,7 +14,7 @@ COQFLAGS:=-w -notation-overridden,-implicits-in-term
# Compilation.
# Note: double space below is important for export.sh
SRC := TLCbuffer Fmap SepFunctor SepTactics LambdaSemantics LambdaSep LambdaCFTactics LambdaCF LambdaStruct LambdaSepLifted LambdaCFLifted LambdaStructLifted Example ExampleBasicNonlifted ExampleListNonlifted ExampleQueueNonlifted ExampleBasic ExampleTrees ExampleUnionFind ExampleHigherOrder ExampleList LambdaSepCredits LambdaCFCredits LambdaSepRO ExampleRO
SRC := TLCbuffer Fmap SepFunctor SepTactics LambdaSemantics LambdaSep LambdaSepCredits LambdaSepRO LambdaCFTactics LambdaCF LambdaStruct LambdaSepLifted LambdaCFLifted LambdaStructLifted Example ExampleBasicNonlifted ExampleListNonlifted ExampleQueueNonlifted ExampleBasic ExampleTrees ExampleUnionFind ExampleHigherOrder ExampleList LambdaCFCredits ExampleRO
# LambdaCFRO
......
......@@ -184,6 +184,12 @@ Notation "Q \*+ H" := (fun x => hstar (Q x) H)
Definition hexists A (J:A->hprop) : hprop :=
fun h => exists x, J x h.
(** Universal lifted to heap predicates
(currently, no notation provided) *)
Definition hforall (A : Type) (J : A -> hprop) : hprop :=
fun h => forall x, J x h.
(** The "Top" predicate, written [\Top], which holds of any heap,
implemented as [Hexists H, H]. *)
......@@ -218,6 +224,11 @@ Parameter hstar_assoc : forall H1 H2 H3,
Parameter hstar_hexists : forall A (J:A->hprop) H,
(hexists J) \* H = hexists (fun x => (J x) \* H).
(** Extrusion of foralls out of star *)
Parameter hstar_hforall : forall H A (J:A->hprop),
(hforall J) \* H ==> hforall (J \*+ H).
(** The frame property (star on H2) holds for entailment *)
Parameter himpl_frame_l : forall H2 H1 H1',
......@@ -268,11 +279,6 @@ Definition hpure (P:Prop) : hprop :=
Notation "\[ P ]" := (hpure P)
(at level 0, P at level 99, format "\[ P ]") : heap_scope.
(** Forall *)
Definition hforall (A : Type) (J : A -> hprop) : hprop :=
fun h => forall x, J x h.
(** Disjunction *)
Definition hor (H1 H2 : hprop) : hprop :=
......@@ -448,6 +454,19 @@ Lemma himpl_hexists_r : forall A (x:A) H J,
H ==> (hexists J).
Proof using. introv W h. exists x. apply~ W. Qed.
Lemma himpl_hexists : forall A (J1 J2:A->hprop),
J1 ===> J2 ->
hexists J1 ==> hexists J2.
Proof using. introv W. intros h (x&M). exists x. applys~ W. Qed.
Lemma himpl_hforall : forall A (J1 J2:A->hprop),
J1 ===> J2 ->
hforall J1 ==> hforall J2.
Proof using. introv W. intros h M x. applys W. applys M. Qed.
(* Note: missing properties for [himpl] on [hand] and [hor].
For properties on [hwand], see file [SepTactics]. *)
(* ---------------------------------------------------------------------- *)
(* ** Properties of [htop] *)
......
......@@ -1197,13 +1197,26 @@ Proof using.
intros. unfold hwand. hsimpl ;=> H3 M. hchanges M.
Qed.
Lemma hwand_move_r : forall H1 H2 H3,
H1 ==> (H2 \--* H3) ->
H1 \* H2 ==> H3.
Proof using.
introv M. hchange (>> himpl_frame_r H2 M).
rew_heap. apply hwand_cancel.
Qed.
Lemma hwand_move_l : forall H1 H2 H3,
H1 \* H2 ==> H3 ->
H1 ==> (H2 \--* H3).
Proof using. introv M. unfold hwand. hsimpl~. Qed.
Lemma hwand_cancel_part : forall H1 H2 H3,
H1 \* ((H1 \* H2) \--* H3) ==> (H2 \--* H3).
Proof using.
intros. unfold hwand. hsimpl ;=> H4 M. hchanges M.
Qed.
Lemma hwand_cancel_part_trans : forall H1 H2 H3 H4,
Lemma hwand_move_part_r : forall H1 H2 H3 H4,
H2 ==> ((H1 \* H3) \--* H4) ->
H1 \* H2 ==> (H3 \--* H4).
Proof using.
......@@ -1211,6 +1224,13 @@ Proof using.
rew_heap. apply hwand_cancel_part.
Qed.
Lemma hwand_move_part_l : forall H1 H2 H3 H4,
H1 \* H2 ==> (H3 \--* H4) ->
H2 ==> ((H1 \* H3) \--* H4).
Proof using.
introv M. unfold hwand. hsimpl. hchanges (hwand_move_r M).
Qed.
Arguments hwand_cancel : clear implicits.
Arguments hwand_cancel_part : clear implicits.
......@@ -1234,6 +1254,14 @@ Proof using.
hchanges (hwand_cancel (Q1 x)).
Qed.
Lemma qwand_cancel_part : forall H A (Q1 Q2:A->hprop),
H \* ((Q1 \*+ H) \---* Q2) ==> (Q1 \---* Q2).
Proof using.
intros. unfold qwand. rewrite hstar_comm. hchange hstar_hforall. rew_heap.
applys himpl_hforall. intros x.
rewrite hstar_comm. rewrites (>> hstar_comm (Q1 x) H).
hchanges (hwand_cancel_part H).
Qed.
(* ********************************************************************** *)
......
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