Commit a38811b7 authored by charguer's avatar charguer

ModelCF1

parent 7cbc8b04
Set Implicit Arguments.
Require Import LibCore Shared ModelLambda ModelSep.
(** *)
Lemma hprop_gc_prove : forall h,
\GC h.
Proof using. Transparent hprop_gc.
intros. exists~ (= h). Qed.
Lemma himpl_trans : forall (H1' H1 H2 H3:hprop),
H1 ==> H1' ->
H1' \* H2 ==> H3 ->
H1 \* H2 ==> H3.
Proof using.
introv M N. intros h (ha&hb&Ha&Hb&Dab&Eab).
applys N. lets Ha': M Ha. exists ha hb. splits~.
Qed.
Lemma qimpl_gc_instantiate : forall (Q Q':val->hprop) (H:hprop),
Q ===> Q' ->
Q \*+ H ===> Q' \*+ \GC.
Proof using.
introv IQ. intros x h (ha&hb&Ha&Hb&Dab&Eab).
exists ha hb. splits~.
{ applys~ IQ. }
{ apply~ hprop_gc_prove. }
Qed.
(********************************************************************)
(* ** Type of a formula *)
Definition formula := hprop -> (val -> hprop) -> Prop.
(********************************************************************)
(* ** The [local] predicate *)
(*------------------------------------------------------------------*)
(* ** Definition of [local] and [is_local] *)
(** Definition *)
Definition local (F:formula) : formula :=
fun (H:hprop) (Q:val->hprop) =>
forall h, H h -> exists H1 H2 Q1,
(H1 \* H2) h
/\ F H1 Q1
/\ Q1 \*+ H2 ===> Q \*+ \GC.
(** Characterization of "local" judgments *)
Definition is_local (F:formula) :=
F = local F.
(** The [local] operator can be freely erased from a conclusion *)
Lemma local_erase : forall (F:formula),
forall H Q, F H Q -> local F H Q.
Proof using.
intros. exists H \[] Q. splits.
{ rewrite~ hprop_star_empty_r. }
{ auto. }
{ apply* qimpl_gc_instantiate. }
Qed.
(** Nested applications [local] are redundant *)
Lemma local_local : forall (F:formula),
local (local F) = local F.
Proof using.
unfold formula. extens. intros H Q. iff 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 <- hprop_star_assoc. exists~ h1 h2. }
{ auto. }
{ intros x. specializes Qle x. specializes Qle' x.
rewrite <- hprop_star_assoc.
applys himpl_trans Qle'.
rewrite hprop_star_assoc.
rewrite (@hprop_star_comm (\GC) H2).
rewrite <- hprop_star_assoc.
applys himpl_trans Qle.
rewrite hprop_star_assoc.
apply* qimpl_gc_instantiate. }
(* shorter proof:
hchange (Qle' x). hchange~ (Qle x).
set (H' := \GC) at 1 2. hsimpl. *)
{ apply~ local_erase. }
Qed.
(*------------------------------------------------------------------*)
(* ** Lemmas for introduction and elimination of [is_local] *)
(** A definition whose head is [local] satisfies [is_local] *)
Lemma local_is_local : forall (F:formula),
is_local (local F).
Proof using. intros. unfolds. rewrite~ local_local. Qed.
Hint Resolve local_is_local.
(** Weaken and frame and gc property [local] *)
Lemma local_frame_gc : forall (F:formula) H H1 H2 Q1 Q,
is_local F ->
F H1 Q1 ->
H ==> H1 \* H2 ->
Q1 \*+ H2 ===> Q \*+ \GC ->
F H Q.
Proof using.
introv L M WH WQ. rewrite L. introv Ph.
exists H1 H2 Q1. splits~.
Qed.
(** Weakening on pre and post from [local] *)
Lemma local_weaken : forall H' Q' (F:formula) H Q,
is_local F ->
F H' Q' ->
H ==> H' ->
Q' ===> Q ->
F H Q.
Proof using.
intros. eapply local_frame_gc with (H2 := \[]); eauto.
rewrite~ hprop_star_empty_r.
apply* qimpl_gc_instantiate.
Qed.
(** Weakening on pre from [local] *)
Lemma local_weaken_pre : forall H' (F:formula) H Q,
is_local F ->
F H' Q ->
H ==> H' ->
F H Q.
Proof using. intros. apply* local_weaken. Qed.
(** Weakening on post from [local] *)
Lemma local_weaken_post : forall Q' (F:formula) H Q,
is_local F ->
F H Q' ->
Q' ===> Q ->
F H Q.
Proof using. intros. apply* local_weaken. Qed.
(** Garbage collection on precondition from [local] *)
Lemma local_gc_pre : forall H' (F:formula) H Q,
is_local F ->
H ==> H' \* \GC ->
F H' Q ->
F H Q.
Proof using.
introv LF H1 H2. applys~ local_frame_gc H2.
Qed.
(** Variant of the above, useful for tactics to specify
the garbage collected part *)
Lemma local_gc_pre_on : forall HG H' (F:formula) H Q,
is_local F ->
H ==> HG \* H' ->
F H' Q ->
F H Q.
Proof using.
introv L M W. rewrite L. introv Ph.
exists H' HG Q. splits.
{ rewrite hprop_star_comm. apply~ M. }
{ auto. }
{ apply* qimpl_gc_instantiate. }
Qed.
(** Garbage collection on post-condition from [local] *)
Lemma local_gc_post : forall Q' (F:formula) H Q,
is_local F ->
F H Q' ->
Q' ===> Q \*+ \GC ->
F H Q.
Proof using.
introv L M W. rewrite L. introv Ph.
exists H \[] Q'. splits~.
{ rewrite~ hprop_star_empty_r. }
{ intros x. rewrite~ hprop_star_empty_r. }
Qed.
(** Extraction of pure facts from [local] *)
Lemma local_extract_prop : forall (F:formula) H (P:Prop) Q,
is_local F ->
(P -> F H Q) ->
F (\[P] \* H) Q.
Proof using.
introv L M. rewrite L. introv (h1&h2&(PH1&HP)&PH2&?&?).
subst h1. rewrite heap_union_empty_l in H1. subst h2.
exists H \[] Q. splits~.
{ rewrite~ hprop_star_empty_r. }
{ apply* qimpl_gc_instantiate. }
Qed.
(** Extraction of existentials from [local] *)
Lemma local_extract_exists : forall (F:formula) A (J:A->hprop) Q,
is_local F ->
(forall x, F (J x) Q) ->
F (hprop_exists J) Q.
Proof using.
introv L M. rewrite L. introv (x&Hx).
exists (J x) \[] Q. splits~.
{ rewrite~ hprop_star_empty_r. }
{ apply* qimpl_gc_instantiate. }
Qed.
(*------------------------------------------------------------------*)
(* NOT USED
(** A introduction rule to establish [is_local] *)
Lemma is_local_prove : forall B (F:formula),
(forall H Q, F H Q <-> local F H Q) -> is_local F.
Proof using.
intros. unfold is_local. apply func_ext_2.
intros. applys prop_ext. applys H.
Qed.
(** Weaken and frame properties from [local] *)
Lemma local_frame : forall H1 H2 Q1 (F:formula) H Q,
is_local F ->
F H1 Q1 ->
H ==> H1 \* H2 ->
Q1 \*+ H2 ===> Q ->
F H Q.
Proof using.
introv L M WH WQ. rewrite L. introv Ph.
exists H1 H2 Q1. splits~.
skip. (* hchange WQ. hsimpl. *)
Qed.
(** Frame property from [local] *)
Lemma local_frame_direct : forall H' H Q (F:formula),
is_local F ->
F H Q ->
F (H \* H') (Q \*+ H').
Proof using. intros. apply* local_frame. Qed.
(** Extraction of existentials below a star from [local] *)
Lemma local_intro_exists : forall B (F:formula) H A (J:A->hprop) Q,
is_local F ->
(forall x, F ((J x) \* H) Q) ->
F (heap_is_pack J \* H) Q.
Proof using.
introv L M. rewrite L. introv (h1&h2&(X&HX)&PH2&?&?).
exists (J X \* H) \[] Q. splits.
rew_heap~. exists~ h1 h2.
auto.
hsimpl.
Qed.
*)
(********************************************************************)
(* ** Characteristic formula generator *)
(*------------------------------------------------------------------*)
(* ** Definition of CF blocks *)
Definition cf_val v : formula := fun H Q =>
H ==> Q v.
Definition cf_if v (F1 F2 : formula) : formula := fun H Q =>
If (v = val_int 0) then F2 H Q else F1 H Q.
Definition cf_let (F1 : formula) (F2of : val -> formula) : formula := fun H Q =>
exists Q1,
F1 H Q1
/\ (forall (X:val), (F2of X) (Q1 X) Q).
Definition cf_app f v : formula := fun H Q =>
app f v H Q.
Definition cf_fix (F1of : val -> val -> formula) (F2of : val -> formula) : formula := fun H Q =>
forall (F:val),
(forall X H' Q', (F1of F X) H' Q' -> app F X H' Q') ->
(F2of F) H Q.
Definition cf_new v : formula := fun H Q =>
(fun r => Hexists l, \[r = val_loc l] \* l ~~> v) \*+ H ===> Q.
Definition cf_get l : formula := fun H Q =>
exists H' v,
H ==> (l ~~> v) \* H'
/\ (fun x => \[x = v] \* l ~~> v) \*+ H' ===> Q.
Definition cf_set l w : formula := fun H Q =>
exists H' v,
H ==> (l ~~> v) \* H'
/\ (fun x => \[x = val_unit] \* l ~~> w) \*+ H' ===> Q.
(*------------------------------------------------------------------*)
(* ** Definition of CF generator *)
......@@ -267,17 +267,10 @@ Proof using.
Qed.
Lemma hprop_star_assoc : forall H1 H2 H3,
H1 \* (H2 \* H3) = (H1 \* H2) \* H3.
(H1 \* H2) \* H3 = H1 \* (H2 \* H3).
(* LibOperation.assoc hprop_star. *)
Proof using.
intros H1 H2 H3. unfold hprop, hprop_star. extens. intros h. split.
{ intros (h1&h'&M1&(h2&h3&M3&M4&D'&U')&D&U). subst h'.
exists (heap_union h1 h2) h3. rewrite heap_disjoint_union_eq_r in D.
splits.
{ exists h1 h2. splits*. }
{ auto. }
{ rewrite* heap_disjoint_union_eq_l. }
{ rewrite~ heap_union_assoc. } }
{ intros (h'&h3&(h1&h2&M3&M4&D'&U')&M2&D&U). subst h'.
exists h1 (heap_union h2 h3). rewrite heap_disjoint_union_eq_l in D.
splits.
......@@ -285,6 +278,13 @@ Proof using.
{ exists h2 h3. splits*. }
{ rewrite* heap_disjoint_union_eq_r. }
{ rewrite~ <- heap_union_assoc. } }
{ intros (h1&h'&M1&(h2&h3&M3&M4&D'&U')&D&U). subst h'.
exists (heap_union h1 h2) h3. rewrite heap_disjoint_union_eq_r in D.
splits.
{ exists h1 h2. splits*. }
{ auto. }
{ rewrite* heap_disjoint_union_eq_l. }
{ rewrite~ heap_union_assoc. } }
Qed. (* later: exploit symmetry in the proof *)
Lemma hprop_star_cancel : forall H1 H2 H2',
......
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