Commit 939de4c3 authored by charguer's avatar charguer

simplification

parent e80bd62d
Set Implicit Arguments. Set Implicit Arguments.
Require Export LibInt CFSpec CFPrint. Require Export LibInt CFApp CFPrint.
(********************************************************************)
(* ** Lemmas for tactics *)
(** Lemma used by [xframe] *)
Lemma xframe_lemma : forall H1 H2 B Q1 (F:~~B) H Q,
is_local F ->
H ==> H1 \* H2 ->
F H1 Q1 ->
Q1 \*+ H2 ===> Q ->
F H Q.
Proof using. intros. apply* local_wframe. Qed.
(** Lemma used by [xchange] *)
Lemma xchange_lemma : forall H1 H1' H2 B H Q (F:~~B),
is_local F ->
(H1 ==> H1') ->
(H ==> H1 \* H2) ->
F (H1' \* H2) Q ->
F H Q.
Proof using.
introv W1 L W2 M. applys local_wframe __ \[]; eauto.
hsimpl. hchange~ W2. hsimpl~. rew_heap~.
Qed.
(** Lemma used by [xgc_all],
to remove everything from the pre-condition *)
Lemma local_gc_pre_all : forall B Q (F:~~B) H,
is_local F ->
F \[] Q ->
F H Q.
Proof using. intros. apply* (@local_gc_pre H). hsimpl. Qed.
(** Lemma used by [xret] and [xret_no_gc]
for when post-condition unifies trivially *)
Lemma xret_lemma_unify : forall B (v:B) H,
local (fun H' Q' => H' ==> Q' v) H (fun x => \[x = v] \* H).
Proof using.
intros. apply~ local_erase. hsimpl. auto.
Qed.
(** Lemma used by [xret] *)
Lemma xret_lemma : forall HG B (v:B) H (Q:B->hprop),
H ==> Q v \* HG ->
local (fun H' Q' => H' ==> Q' v) H Q.
Proof using.
introv W. eapply (@local_gc_pre HG).
auto. rewrite star_comm. apply W.
apply~ local_erase.
Qed.
(** Lemma used by [xret_no_gc] *)
Lemma xret_no_gc_lemma : forall B (v:B) H (Q:B->hprop),
H ==> Q v ->
local (fun H' Q' => H' ==> Q' v) H Q.
Proof using.
introv W. apply~ local_erase.
Qed.
(** Lemma used by [xpost],
for introducing an evar for the post-condition *)
Lemma xpost_lemma : forall B Q' Q (F:~~B) H,
is_local F ->
F H Q' ->
Q' ===> Q ->
F H Q.
Proof using. intros. applys* local_weaken. Qed.
(********************************************************************)
(* ** Local parameterized formulae *)
(** [is_local_pred S] asserts that [is_local (S x)] holds for any [x].
It is useful for describing loop invariants. *)
Definition is_local_pred A1 B (S:A1->~~B) :=
forall x, is_local (S x).
(********************************************************************)
(* ** While-loops *)
Lemma while_loop_cf_inv_measure :
forall (I:bool->int->hprop),
forall (F1:~~bool) (F2:~~unit) H (Q:unit->hprop),
(exists b m, H ==> I b m \* (Hexists G, G)) ->
(forall b m, F1 (I b m) (fun b' => I b' m)) ->
(forall m, F2 (I true m) (# Hexists b m', \[0 <= m' < m] \* I b m')) ->
(Q = fun _ => Hexists m, I false m) ->
(_While F1 _Do F2 _Done) H Q.
Proof using.
introv (bi&mi&Hi) Hc Hs He. applys~ local_weaken_gc_pre (I bi mi). xlocal.
xextract as HG. clear Hi. apply local_erase. introv LR HR.
gen bi. induction_wf IH: (int_downto_wf 0) mi. intros.
applys (rm HR). xlet. applys Hc. simpl. xif.
xseq. applys Hs. xextract as b m' E. xapplys IH. applys E. hsimpl. hsimpl.
xret_no_gc. subst Q. hsimpl.
Qed.
(********************************************************************)
(* ** For-loops *)
Lemma for_loop_cf_to_inv :
forall I H',
forall (a:int) (b:int) (F:int->~~unit) H (Q:unit->hprop),
(a > (b)%Z -> H ==> (Q tt)) ->
(a <= (b)%Z ->
(H ==> I a \* H')
/\ (forall i, a <= i /\ i <= (b)%Z -> F i (I i) (# I(i+1)))
/\ (I ((b)%Z+1) \* H' ==> Q tt)) ->
(For i = a To b Do F i _Done) H Q.
Proof.
introv M1 M2. apply local_erase. intros S LS HS.
tests C: (a > b).
apply (rm HS). split; intros C'. math. xret_no_gc~.
forwards (Ma&Mb&Mc): (rm M2). math.
cuts P: (forall i, a <= i <= b+1 -> S i (I i) (# I (b+1))).
xapply P. math. hchanges Ma. hchanges Mc.
intros i. induction_wf IH: (int_upto_wf (b+1)) i. intros Bnd.
applys (rm HS). split; intros C'.
xseq. eapply Mb. math. xapply IH; auto with maths; hsimpl.
xret_no_gc. math_rewrite~ (i = b +1).
Qed.
Lemma for_loop_cf_to_inv_gen' :
forall I H',
forall (a:int) (b:int) (F:int->~~unit) H,
(a <= (b)%Z ->
(H ==> I a \* H')
/\ (forall i, a <= i /\ i <= (b)%Z -> F i (I i) (# I(i+1)))) ->
(a > (b)%Z -> H ==> I ((b)%Z+1) \* H') ->
(For i = a To b Do F i _Done) H (# I ((b)%Z+1) \* H').
Proof. intros. applys* for_loop_cf_to_inv. Qed.
Lemma for_loop_cf_to_inv_gen :
forall I H',
forall (a:int) (b:int) (F:int->~~unit) H Q,
(a <= (b)%Z -> H ==> I a \* H') ->
(forall i, a <= i <= (b)%Z -> F i (I i) (# I(i+1))) ->
(a > (b)%Z -> H ==> I ((b)%Z+1) \* H') ->
(# (I ((b)%Z+1) \* H')) ===> Q ->
(For i = a To b Do F i _Done) H Q.
Proof. intros. applys* for_loop_cf_to_inv. intros C. hchange (H2 C). hchange (H3 tt). hsimpl. Qed.
Lemma for_loop_cf_to_inv_up :
forall I H',
forall (a:int) (b:int) (F:int->~~unit) H (Q:unit->hprop),
(a <= (b)%Z) ->
(H ==> I a \* H') ->
(forall i, a <= i /\ i <= (b)%Z -> F i (I i) (# I(i+1))) ->
((# I ((b)%Z+1) \* H') ===> Q) ->
(For i = a To b Do F i _Done) H Q.
Proof. intros. applys* for_loop_cf_to_inv. intros. math. Qed.
(********************************************************************) (********************************************************************)
......
(************************************************************)
(* ** [xgo] *)
Inductive Xhint_cmd :=
| Xstop : Xhint_cmd
| XstopNoclear : Xhint_cmd
| XstopAfter : Xhint_cmd
| XstopInside : Xhint_cmd
| Xtactic : Xhint_cmd
| XtacticNostop : Xhint_cmd
| XtacticNoclear : Xhint_cmd
| XsubstAlias : Xhint_cmd
| XspecArgs : list Boxer -> list Boxer -> Xhint_cmd
| Xargs : forall A, A -> Xhint_cmd
| Xlet : forall A, A -> Xhint_cmd
| Xlets : forall A, A -> Xhint_cmd
| Xsimple : Xhint_cmd.
Inductive Xhint (a : tag_name) (h : Xhint_cmd) :=
| Xhint_intro : Xhint a h.
Ltac add_hint a h :=
let H := fresh "Hint" in
lets H: (Xhint_intro a h).
Ltac clear_hint a :=
match goal with H: Xhint a _ |- _ => clear H end.
Ltac clears_hint tt :=
repeat match goal with H: Xhint _ _ |- _ => clear H end.
Ltac find_hint a :=
match goal with H: Xhint a ?h |- _ => constr:(h) end.
Ltac xgo_default solver cont :=
match ltac_get_tag tt with
| tag_ret => xret; cont tt
| tag_fail => xfail; cont tt
| tag_done => xdone; cont tt
| tag_apply => xapp
| tag_seq => xseq; cont tt
| tag_let_val => xval; cont tt
| tag_let_trm => xlet; cont tt
| tag_let_fun => fail
| tag_body => fail
| tag_letrec => fail
| tag_case => xcases_real; cont tt
| tag_casewhen => fail
| tag_if => xif; cont tt
| tag_alias => xalias; cont tt
| tag_match ?n => xmatch; cont tt
| tag_top_val => fail
| tag_top_trm => fail
| tag_top_fun => fail
| tag_for => fail
| tag_while => fail
end.
Ltac xtactic tag := idtac.
Ltac run_hint h cont :=
let tag := ltac_get_tag tt in
match h with
| Xstop => clears_hint tt; idtac
| XstopNoclear => idtac
| XstopAfter =>
match tag with
| tag_let_trm => fail (* todo: xlet_with cont ltac:(fun _ => idtac)*)
| _ => xgo_default ltac:(fun _ => idtac) ltac:(fun _ => idtac)
end
| XstopInside =>
match tag with
| tag_let_trm => fail (*todo: xlet_with ltac:(fun _ => idtac) cont *)
end
| Xtactic => clears_hint tt; xtactic tag
| XtacticNostop => xtactic tag; cont tt
| XtacticNoclear => xtactic tag
| XsubstAlias => xmatch_subst_alias; cont tt
| Xargs ?E =>
match tag with
| tag_let_trm => fail (* todo!!*)
| tag_apply => xapp E (*todo: not needed?*)
end
| XspecArgs (>> ?S) ?E =>
match tag with
| tag_let_trm => fail (* todo!!*)
| tag_apply => xapp_spec S E (*todo: not needed?*)
end
| Xlet ?S =>
match tag with
| tag_let_trm => xlet S; cont tt
| tag_let_fun => xfun_noxbody S
end
| Xsimple => xmatch_simple; cont tt
(* todo : generalize
| tag_case => xcases_real
| tag_if => xif
| tag_match ?n => xmatch
*)
end.
Ltac find_and_run_hint cont :=
let a := ltac_get_label tt in
let h := find_hint a in
clear_hint a;
first [ run_hint h cont | fail 1 ].
Tactic Notation "xhint" :=
find_and_run_hint ltac:(fun _ => idtac).
Ltac xgo_core solver cont :=
first [ find_and_run_hint cont
| xgo_default solver cont ].
Ltac xgo_core_once solver :=
xgo_core solver ltac:(fun _ => idtac).
Ltac xgo_core_repeat solver :=
xgo_core solver ltac:(fun _ => instantiate; try solve [ solver tt ];
instantiate; try xgo_core_repeat solver).
Ltac xgo_pre tt :=
first [ xcf; repeat progress(intros)
| repeat progress(intros)
| idtac ].
Ltac xgo_base solver :=
xgo_pre tt; xgo_core_repeat solver.
Tactic Notation "xgo1" :=
xgo_core_once ltac:(fun _ => idtac).
Tactic Notation "xgo" :=
xgo_base ltac:(fun tt => idtac).
Tactic Notation "xgo" "~" :=
xgo_base ltac:(fun tt => xauto~ ); instantiate; xauto~.
Tactic Notation "xgo" "*" :=
xgo_base ltac:(fun tt => xauto* ); instantiate; xauto*.
Tactic Notation "xgo" constr(a1) constr(h1) :=
add_hint a1 h1; xgo.
Tactic Notation "xgo" constr(a1) constr(h1) "," constr(a2) constr(h2) :=
add_hint a1 h1; add_hint a2 h2; xgo.
Tactic Notation "xgo" constr(a1) constr(h1) "," constr(a2) constr(h2) ","
constr(a3) constr(h3) :=
add_hint a1 h1; add_hint a2 h2; add_hint a3 h3; xgo.
Tactic Notation "xgo" constr(a1) constr(h1) "," constr(a2) constr(h2) ","
constr(a3) constr(h3) "," constr(a4) constr(h4) :=
add_hint a1 h1; add_hint a2 h2; add_hint a3 h3; add_hint a4 h4; xgo.
Tactic Notation "xgo" "~" constr(a1) constr(h1) :=
add_hint a1 h1; xgo~.
Tactic Notation "xgo" "~" constr(a1) constr(h1) "," constr(a2) constr(h2) :=
add_hint a1 h1; add_hint a2 h2; xgo~.
Tactic Notation "xgo" "~" constr(a1) constr(h1) "," constr(a2) constr(h2) ","
constr(a3) constr(h3) :=
add_hint a1 h1; add_hint a2 h2; add_hint a3 h3; xgo~.
Tactic Notation "xgo" "~" constr(a1) constr(h1) "," constr(a2) constr(h2) ","
constr(a3) constr(h3) "," constr(a4) constr(h4) :=
add_hint a1 h1; add_hint a2 h2; add_hint a3 h3; add_hint a4 h4; xgo~.
Tactic Notation "xgos" :=
xgo; hsimpl.
Tactic Notation "xgos" "~" :=
xgos; auto_tilde.
Tactic Notation "xgos" "*" :=
xgos; auto_star.
let f x = x
\ No newline at end of file
open NullPointers open NullPointers
let g x = Aux.f x let g x = Auxi.f x
Require Export CFLib Main_ml. Require Export CFLib Main_ml.
Require Import Aux_ml Aux_proof Extra. Require Import Auxi_ml Auxi_proof Extra.
Lemma g_spec : Lemma g_spec :
Spec g (x:int) |R>> R \[] (fun y => \[same x y]). Spec g (x:int) |R>> R \[] (fun y => \[same x y]).
......
Set Implicit Arguments. Set Implicit Arguments.
Require Export LibCore LibEpsilon Shared. Require Export LibCore LibEpsilon Shared.
Require Export CFHeaps CFApp. Require Export CFHeaps.
Open Local Scope heap_scope_advanced. Open Local Scope heap_scope_advanced.
Hint Extern 1 (_ ===> _) => apply rel_le_refl. Hint Extern 1 (_ ===> _) => apply rel_le_refl.
...@@ -17,7 +17,7 @@ Hint Extern 1 (_ ===> _) => apply rel_le_refl. ...@@ -17,7 +17,7 @@ Hint Extern 1 (_ ===> _) => apply rel_le_refl.
Based on [eval], we define [app_basic f x H Q], which is a like [eval] Based on [eval], we define [app_basic f x H Q], which is a like [eval]
modulo frame and weakening and garbage collection. modulo frame and weakening and garbage collection.
On top of [app_basic], we define [App f xs H Q], which describes the 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]. 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 We also define a predicate [curried n f] which asserts that the function
...@@ -25,11 +25,11 @@ Hint Extern 1 (_ ===> _) => apply rel_le_refl. ...@@ -25,11 +25,11 @@ Hint Extern 1 (_ ===> _) => apply rel_le_refl.
applications are partial. applications are partial.
The characteristic formula generated for a function application The characteristic formula generated for a function application
[f x y z] is "App f [x y z]". [f x y z] is "app f [x y z]".
The characteristic formula generated for a function definition The characteristic formula generated for a function definition
[let f x y z = t] is: [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)]. [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 These definitions are correct and sufficient to reasoning about all
function calls, including partial and over applications. function calls, including partial and over applications.
...@@ -63,7 +63,7 @@ Axiom eval : forall A B, func -> A -> heap -> B -> heap -> Prop. ...@@ -63,7 +63,7 @@ Axiom eval : forall A B, func -> A -> heap -> B -> heap -> Prop.
(********************************************************************) (********************************************************************)
(* ** Definition and properties of the primitive App predicate *) (* ** Definition and properties of the primitive app predicate *)
(** The primitive predicate [app_basic], which makes a [local] (** The primitive predicate [app_basic], which makes a [local]
version of [eval]. *) version of [eval]. *)
...@@ -132,133 +132,139 @@ Notation "[ x1 x2 x3 x4 ]" := ((dyn x1)::(dyn x2)::(dyn x3)::(dyn x4)::nil) ...@@ -132,133 +132,139 @@ Notation "[ x1 x2 x3 x4 ]" := ((dyn x1)::(dyn x2)::(dyn x3)::(dyn x4)::nil)
Notation "[ x1 x2 x3 x4 x5 ]" := ((dyn x1)::(dyn x2)::(dyn x3)::(dyn x4)::(dyn x5)::nil) 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. (at level 0, x1 at level 0, x2 at level 0, x3 at level 0, x4 at level 0, x5 at level 0) : dynlist.
Bind Scope dynlist with dyn list. (*Bind Scope dynlist with list.*)
Delimit Scope dynlist with dyns. Delimit Scope dynlist with dynlist.
(********************************************************************) (********************************************************************)
(* ** Definition of [App] and properties *) (* ** Definition of [app] and properties *)
(** Definition of [App f xs], recursive. *) (** Definition of [app f xs], recursive.
Can be written, e.g. Notation [app f [x y z] H Q] *)
Fixpoint AppDef (f:func) (xs:list dynamic) B (H:hprop) (Q:B->hprop) : Prop := Fixpoint app_def (f:func) (xs:list dynamic) {B} (H:hprop) (Q:B->hprop) : Prop :=
match xs with match xs with
| nil => False | nil => False
| (dyn x)::nil => app_basic f x H Q | (dyn x)::nil => app_basic f x H Q
| (dyn x)::xs => | (dyn x)::xs =>
app_basic f x H app_basic f x H
(fun g => Hexists H', H' \* \[ AppDef g xs H' Q]) (fun g => Hexists H', H' \* \[ app_def g xs H' Q])
end. end.
(** Notation [App f [x y z]] *) (*
TODO: does not seem to work, hence the work-around using the notation below
Arguments app f%dummy_scope xs%dynlist B%type_scope H%heap_scope Q%heap_scope.
*)
Notation "'App' f xs" := Notation "'app' f xs" :=
(@AppDef f xs _) (* (@AppDef f (xs)%dynlist _) *) (@app_def f (xs)%dynlist _) (* (@app_def f (xs)%dynlist _) *)
(at level 80, f at level 0, xs at level 0) : charac. (at level 80, f at level 0, xs at level 0) : charac.
Open Scope charac. Open Scope charac.
Definition demo_arglist := Definition demo_arglist :=
forall f (xs:list int) (x y:int) B H (Q:B->hprop), forall f (xs:list int) (x y:int) B H (Q:B->hprop),
App f [ x y ] H Q. app f [ x y ] H Q.
(* TODO: find a way that the parentheses are not printed around "App" *)
(* Print demo_arglist. *) (* Print demo_arglist. *)
(* TODO: find a way that the parentheses are not printed around "app" *)
(** Reformulation of the definition *) (** Reformulation of the definition *)
Lemma App_ge_2_unfold : Lemma app_ge_2_unfold :
forall (f:func) A (x:A) (xs:list dynamic) B (H:hprop) (Q:B->hprop), forall (f:func) A (x:A) (xs:list dynamic) B (H:hprop) (Q:B->hprop),
(xs <> nil) -> (xs <> nil) ->
App f ((dyn x)::xs) H Q app f ((dyn x)::xs) H Q
= app_basic f x H = app_basic f x H
(fun g => Hexists H', H' \* \[ AppDef g xs H' Q]). (fun g => Hexists H', H' \* \[ app_def g xs H' Q]).
Proof using. Proof using.
intros. destruct xs. false. auto. intros. destruct xs. false. auto.
Qed. Qed.
Lemma App_ge_2_unfold' : Lemma app_ge_2_unfold' :
forall (f:func) A (x:A) (xs:list dynamic) B (H:hprop) (Q:B->hprop), forall (f:func) A (x:A) (xs:list dynamic) B (H:hprop) (Q:B->hprop),
(length xs >= 1)%nat -> (length xs >= 1)%nat ->
App f ((dyn x)::xs) H Q app f ((dyn x)::xs) H Q
= app_basic f x H = app_basic f x H
(fun g => Hexists H', H' \* \[ AppDef g xs H' Q]). (fun g => Hexists H', H' \* \[ app_def g xs H' Q]).
Proof using. Proof using.
intros. rewrite~ App_ge_2_unfold. destruct xs; rew_list in *. intros. rewrite~ app_ge_2_unfold. destruct xs; rew_list in *.
math. math.
introv N. false. introv N. false.
Qed. Qed.
Lemma App_ge_2_unfold_extens : Lemma app_ge_2_unfold_extens :
forall (f:func) A (x:A) (xs:list dynamic) B, forall (f:func) A (x:A) (xs:list dynamic) B,
(xs <> nil) -> (xs <> nil) ->
AppDef f ((dyn x)::xs) (B:=B) app_def f ((dyn x)::xs) (B:=B)
= (fun H Q => app_basic f x H = (fun H Q => app_basic f x H
(fun g => Hexists H', H' \* \[ AppDef g xs H' Q])). (fun g => Hexists H', H' \* \[ app_def g xs H' Q])).
Proof using. Proof using.
introv N. applys func_ext_2. intros H Q. rewrite~ App_ge_2_unfold. introv N. applys func_ext_2. intros H Q. rewrite~ app_ge_2_unfold.
Qed. Qed.
(** Weaken-frame-gc for [App] -- auxiliary lemma for [App_local]. *) (** Weaken-frame-gc for [app] -- auxiliary lemma for [app_local]. *)
Lemma App_wgframe : forall B f xs H H1 H2 (Q1 Q:B->hprop), Lemma app_wgframe : forall B f xs H H1 H2 (Q1 Q:B->hprop),
App f xs H1 Q1 -> app f xs H1 Q1 ->
H ==> (H1 \* H2) -> H ==> (H1 \* H2) ->
(Q1 \*+ H2) ===> (Q \*+ (Hexists H', H')) -> (Q1 \*+ H2) ===> (Q \*+ (Hexists H', H')) ->
App f xs H Q. app f xs H Q.
Proof using. Proof using.
intros B f xs. gen f. induction xs as [|[A x] xs]; introv M WH WQ. false. intros B f xs. gen f. induction xs as [|[A x] xs]; introv M WH WQ. false.
tests E: (xs = nil). tests E: (xs = nil).
simpls. applys~ local_wgframe M. simpls. applys~ local_wgframe M.
rewrite~ App_ge_2_unfold. rewrite~ App_ge_2_unfold in M. rewrite~ app_ge_2_unfold. rewrite~ app_ge_2_unfold in M.
applys~ local_wframe M. intros g. applys~ local_wframe M. intros g.
hextract as HR LR. hsimpl (HR \* H2). applys* IHxs LR. hextract as HR LR. hsimpl (HR \* H2). applys* IHxs LR.
Qed. Qed.
Lemma App_weaken : forall B f xs H (Q Q':B->hprop), Lemma app_weaken : forall B f xs H (Q Q':B->hprop),
App f xs H Q -> app f xs H Q ->
Q ===> Q' -> Q ===> Q' ->
App f xs H Q'. app f xs H Q'.
Proof using. Proof using.
introv M W. applys* App_wgframe. hsimpl. intros r. hsimpl~ \[]. introv M W. applys* app_wgframe. hsimpl. intros r. hsimpl~ \[].