Commit 58cfc3c9 authored by charguer's avatar charguer
Browse files

app_local

parent 939f25ce
......@@ -2367,6 +2367,23 @@ Definition weakenable B (F:~~B) :=
(*------------------------------------------------------------------*)
(* ** Properties of [local] *)
(** A definition whose head is [local] satisfies [is_local] *)
Lemma local_is_local : forall B (F:~~B),
is_local (local F).
Proof using. intros. unfolds. rewrite~ local_local. Qed.
Hint Resolve local_is_local.
(** A introduction rule to establish [is_local] *)
Lemma is_local_prove : forall B (F:~~B),
(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.
(** The [local] operator can be freely erased from a conclusion *)
Lemma local_erase : forall B (F:~~B),
......@@ -2394,14 +2411,6 @@ Proof using.
apply~ local_erase.
Qed.
(** A definition whose head is [local] satisfies [is_local] *)
Lemma local_is_local : forall B (F:~~B),
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_wgframe : forall B (F:~~B) H H1 H2 Q1 Q,
......@@ -2462,6 +2471,13 @@ Proof using.
introv LF H1 H2. applys~ local_wgframe H2.
Qed.
Lemma local_weaken_post : forall B Q' (F:~~B) H Q,
is_local F ->
F H Q' ->
Q' ===> Q ->
F H Q.
Proof using. intros. apply* local_weaken. Qed.
(** Garbage collection on post-condition from [local] *)
Lemma local_gc_post : forall B Q' (F:~~B) H Q,
......
......@@ -6,37 +6,58 @@ Open Local Scope heap_scope_advanced.
Hint Extern 1 (_ ===> _) => apply rel_le_refl.
Lemma local_weaken_post : forall B Q' (F:~~B) H Q,
is_local F ->
F H Q' ->
Q' ===> Q ->
F H Q.
Proof using. intros. apply* local_weaken. Qed.
Lemma local_prove : forall B (F:~~B),
(forall H Q, F H Q = local F H Q) -> is_local F.
Proof using.
intros. unfold is_local. apply func_ext_2. applys H.
Qed.
(********************************************************************)
(* ** Overview *)
(**
CFML exports an axiomatic operation [eval f v h v' h'] which describes th
e big-step evaluation of a one-argument function on the entire heap.
Based on [eval], we define [app_basic f x H Q], which is a like [eval]
modulo frame and weakening and garbage collection.
On top of [app_basic], we define [App f xs H Q], which describes the
evaluation of a call to [f] on the arguments described by the list [xs].
We also define a predicate [curried n f] which asserts that the function
[f] is a curried function with [n] arguments, hence its [n-1] first
applications are partial.
The characteristic formula generated for a function application
[f x y z] is "App f [x y z]".
The characteristic formula generated for a function definition
[let f x y z = t] is:
[curried 3 f /\ (forall x y z H Q, CF(t) H Q -> App f [x y z] H Q)].
These definitions are correct and sufficient to reasoning about all
function calls, including partial and over applications.
*)
(********************************************************************)
(* ** Axioms of CFML *)
(** Note: these axioms could in theory be realized by constructing
a deep embedding of the target programming language. See
Arthur Chargueraud's thesis for full details. *)
a deep embedding of the target programming language.
See Arthur Chargueraud's PhD thesis for full details. *)
(** The type Func *)
(** The type Func, used to represent functions *)
Axiom func : Type.
(** The type Func is inhabited *)
Axiom func_inhab : Inhab func.
Existing Instance func_inhab.
(** The evaluation predicate for functions: [eval f v h v' h'] *)
(** The evaluation predicate for functions: [eval f v h v' h'],
asserts that the evaluation of the application of [f] to [v]
in a heap [h] terminates and produces a value [v'] in a heap [h']. *)
Axiom eval : forall A B, func -> A -> heap -> B -> heap -> Prop.
......@@ -45,14 +66,15 @@ Axiom eval : forall A B, func -> A -> heap -> B -> heap -> Prop.
(********************************************************************)
(* ** Definition and properties of the primitive App predicate *)
(** The primitive predicate App *)
(** The primitive predicate [app_basic], which makes a [local]
version of [eval]. *)
Definition app_basic (f:func) A (x:A) B (H:hprop) (Q:B->hprop) :=
forall h i, \# h i -> H h ->
exists v' h' g, \# h' g i /\ Q v' h' /\
eval f x (h \+ i) v' (h' \+ g \+ i).
(** AppReturns is a local property *)
(** [app_basic f x] is a local formula *)
Lemma app_basic_local : forall A B f (x:A),
is_local (@app_basic f A x B).
......@@ -89,38 +111,37 @@ Proof using.
Admitted. (* faster *)
(*
Qed.
*)
Hint Resolve app_basic_local.
(** AppReturns with frame -- TODO: needed?
Lemma app_frame_1 : forall B A1 (x1:A1) f H (Q:B->hprop) H',
app_1 f x1 H Q -> app_1 f x1 (H \* H') (Q \*+ H').
Proof using. intros. applys* local_wframe. Qed.
Hint Resolve app_basic_local.
*)
(********************************************************************)
(* ** Generic notation for list of args *)
(* ** Generic notation for list of dyns *)
Notation "'Dyn' x" := (@dyn _ x) (at level 0).
Notation "[ x1 ]" := ((dyn x1)::nil)
(at level 0, x1 at level 00) : arglist.
(at level 0, x1 at level 00) : dynlist.
Notation "[ x1 x2 ]" := ((dyn x1)::(dyn x2)::nil)
(at level 0, x1 at level 0, x2 at level 0) : arglist.
(at level 0, x1 at level 0, x2 at level 0) : dynlist.
Notation "[ x1 x2 x3 ]" := ((dyn x1)::(dyn x2)::(dyn x3)::nil)
(at level 0, x1 at level 0, x2 at level 0, x3 at level 0) : arglist.
(at level 0, x1 at level 0, x2 at level 0, x3 at level 0) : dynlist.
Notation "[ x1 x2 x3 x4 ]" := ((dyn x1)::(dyn x2)::(dyn x3)::(dyn x4)::nil)
(at level 0, x1 at level 0, x2 at level 0, x3 at level 0, x4 at level 0) : dynlist.
Notation "[ x1 x2 x3 x4 x5 ]" := ((dyn x1)::(dyn x2)::(dyn x3)::(dyn x4)::(dyn x5)::nil)
(at level 0, x1 at level 0, x2 at level 0, x3 at level 0, x4 at level 0, x5 at level 0) : dynlist.
Delimit Scope arglist with arglist.
Bind Scope dynlist with dyn list.
Delimit Scope dynlist with dyns.
(********************************************************************)
(* ** Definition of [App] and properties *)
(** Definition of [App f xs], recursive. *)
Fixpoint AppDef (f:func) (xs:list dynamic) B (H:hprop) (Q:B->hprop) : Prop :=
match xs with
| nil => False
......@@ -130,14 +151,20 @@ Fixpoint AppDef (f:func) (xs:list dynamic) B (H:hprop) (Q:B->hprop) : Prop :=
(fun g => Hexists H', H' \* \[ AppDef g xs H' Q])
end.
(** Notation [App f [x y z]] *)
Notation "'App' f xs" :=
(@AppDef f (xs)%arglist _)
(at level 68, f at level 0, xs at level 0) : charac.
Open Scope charac.
(@AppDef f xs _) (* (@AppDef f (xs)%dynlist _) *)
(at level 80, f at level 0, xs at level 0) : charac.
Open Scope charac.
Definition demo_arglist :=
forall f (xs:list int) (x y:int) B H (Q:B->hprop),
App f [ x y ] H Q.
(* TODO: find a way that the parentheses are not printed around "App" *)
(* Print demo_arglist. *)
(** Reformulation of the definition *)
Lemma App_ge_2_unfold :
forall (f:func) A (x:A) (xs:list dynamic) B (H:hprop) (Q:B->hprop),
......@@ -161,6 +188,54 @@ Proof using.
introv N. false.
Qed.
Lemma App_ge_2_unfold_extens :
forall (f:func) A (x:A) (xs:list dynamic) B,
(xs <> nil) ->
AppDef f ((dyn x)::xs) (B:=B)
= (fun H Q => app_basic f x H
(fun g => Hexists H', H' \* \[ AppDef g xs H' Q])).
Proof using.
introv N. applys func_ext_2. intros H Q. rewrite~ App_ge_2_unfold.
Qed.
(** Weaken-frame-gc for [App] -- auxiliary lemma for [App_local]. *)
Lemma App_wgframe : forall B f xs H H1 H2 (Q1 Q:B->hprop),
App f xs H1 Q1 ->
H ==> (H1 \* H2) ->
(Q1 \*+ H2) ===> (Q \*+ (Hexists H', H')) ->
App f xs H Q.
Proof using.
intros B f xs. gen f. induction xs as [|[A x] xs]; introv M WH WQ. false.
tests E: (xs = nil).
simpls. applys~ local_wgframe M.
rewrite~ App_ge_2_unfold. rewrite~ App_ge_2_unfold in M.
applys~ local_wframe M. intros g.
hextract as HR LR. hsimpl (HR \* H2). applys* IHxs LR.
Qed.
Lemma App_weaken : forall B f xs H (Q Q':B->hprop),
App f xs H Q ->
Q ===> Q' ->
App f xs H Q'.
Proof using.
introv M W. applys* App_wgframe. hsimpl. intros r. hsimpl~ \[].
Qed.
(* DEPRECATED
Lemma App_frame : forall B f xs H H' (Q:B->hprop),
App f xs H Q ->
App f xs (H \* H') (Q \*+ H').
Proof using.
intros B f xs. gen f. induction xs as [|[A x] xs]; introv M. false.
tests E: (xs = nil).
simpls. applys~ local_wframe M.
rewrite~ App_ge_2_unfold. rewrite~ App_ge_2_unfold in M.
applys~ local_wframe M. intros g.
hextract as HR LR. hsimpl (HR \* H'). applys* IHxs.
Qed.
Lemma App_weaken : forall B f xs H (Q Q':B->hprop),
App f xs H Q ->
Q ===> Q' ->
......@@ -173,10 +248,35 @@ Proof using.
applys~ local_weaken_post M. intros g. hsimpl. rew_heap. applys* IHxs.
Qed.
*)
(** Local property for [App] *)
Lemma App_local : forall f xs B,
xs <> nil -> is_local (AppDef f xs (B:=B)).
Proof using.
introv N. apply is_local_prove. intros H Q.
destruct xs as [|[A1 x1] xs]; tryfalse.
destruct xs as [|[A2 x2] xs].
{ simpl. rewrite~ <- app_basic_local. iff*. }
{ rewrite App_ge_2_unfold_extens; auto_false.
iff M.
apply local_erase. auto.
rewrite app_basic_local.
intros h Hh. specializes M Hh.
destruct M as (H1&H2&Q1&R1&R2&R3). exists___. splits.
eauto. eauto.
intros g. hextract as H' L. hsimpl (H' \* H2).
applys App_wgframe L. hsimpl. hchange R3. hsimpl. }
Qed.
(********************************************************************)
(* ** Definition of [curried] *)
(** [curried n f] asserts that [n-1] first applications of [f] are total *)
Fixpoint curried (n:nat) (f:func) : Prop :=
match n with
| O => False
......@@ -188,6 +288,8 @@ Fixpoint curried (n:nat) (f:func) : Prop :=
App f ((dyn x)::xs) H Q -> App g xs H Q])
end.
(** Unfolding lemma for [curried] *)
Lemma curried_ge_2_unfold : forall n f,
(n > 1)%nat ->
curried n f
......@@ -203,6 +305,9 @@ Qed.
(********************************************************************)
(* ** Lemma for over-applications *)
(** [App f (xs++ys)] can be expressed as [App f xs] that returns
a function [g] such that the behavior is that of [App g ys]. *)
Lemma App_over_app : forall xs ys f B H (Q:B->hprop),
(length xs > 0)%nat -> (length ys > 0)%nat ->
App f (xs++ys) H Q
......@@ -220,6 +325,8 @@ Proof using.
fequal. fequal. apply IHxs. subst. rew_list. math. math.
Qed.
(** Alternative formulation *)
Lemma App_over_take : forall n xs f B H (Q:B->hprop),
(0 < n < length xs)%nat ->
App f xs H Q
......@@ -236,6 +343,10 @@ Qed.
(********************************************************************)
(* ** Lemma for partial-applications *)
(** When [curried n f] holds and the number of the arguments [xs]
is less than [n], then [App f xs] is a function [g] such that
[App g ys] has the same behavior as [App f (xs++ys)]. *)
Lemma App_partial : forall n xs f,
curried n f -> (0 < length xs < n)%nat ->
App f xs \[] (fun g => \[
......@@ -252,8 +363,7 @@ Proof using.
rew_list. applys_eq M1 2. math.
introv E AK. rew_list in *. applys M2. math. auto. }
{ asserts Pzs: (0 < length zs). { destruct zs. tryfalse. rew_list. math. }
rew_list in N.
rewrite~ App_ge_2_unfold'.
rew_list in N. rewrite~ App_ge_2_unfold.
eapply local_weaken_post. auto. applys (rm C). clear C. (* todo: make work rm *)
intros h. hextract as [M1 M2]. hsimpl.
applys App_weaken. applys (rm IH) M1. math. math. clear IH.
......@@ -271,34 +381,7 @@ Qed.
(********************************************************************)
(*
Lemma App_local : forall f xs B,
xs <> nil -> is_local (AppDef f xs (B:=B)).
Proof using.
introv N. apply local_prove. intros H Q.
destruct xs as [|[A1 x1] xs]; tryfalse.
destruct xs as [|[A2 x2] xs].
simpl. rewrite~ <- app_basic_local.
rewrite App_ge_2_unfold. rewrite app_basic_local.
apply func_equal_1.
*)
(********************************************************************)
(* ** CF GENERATOR *)
(* Characteristic formula for "f x y z" is "App f [x y z]".
Hypothesis for function declaration "let f x y z = t" is:
"curried 3 f /\ (forall x y z H Q, CF(t) H Q -> App f [x y z] H Q)"
*)
......
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