From 4a3579b212af99559be3c0df724521ab14edcbe4 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Arma=C3=ABl=20Gu=C3=A9neau?= <armael.gueneau@ens-lyon.fr> Date: Mon, 8 Jan 2018 16:21:12 +0100 Subject: [PATCH 1/6] Whitespace cleanup --- lib/coq/CFApp.v | 203 ++++++++++++++++------------------ lib/coq/CFHeaps.v | 10 +- lib/coq/CFLibCredits.v | 135 +++++++++++----------- lib/coq/CFLibCreditsNat.v | 7 -- lib/coq/CFTactics.v | 20 ++-- lib/stdlib/Pervasives_proof.v | 48 ++++---- 6 files changed, 202 insertions(+), 221 deletions(-) delete mode 100644 lib/coq/CFLibCreditsNat.v diff --git a/lib/coq/CFApp.v b/lib/coq/CFApp.v index b203076..3f7e674 100644 --- a/lib/coq/CFApp.v +++ b/lib/coq/CFApp.v @@ -11,14 +11,14 @@ Hint Extern 1 (_ ===> _) => apply refl_rel_incl'. (********************************************************************) (* ** Overview *) -(** +(** - CFML exports an axiomatic operation [eval f v h v' h'] which describes th + 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]. @@ -46,20 +46,20 @@ Hint Extern 1 (_ ===> _) => apply refl_rel_incl'. (* ** Axioms for applications *) (** Note: these axioms could in theory be realized by constructing - a deep embedding of the target programming language. + a deep embedding of the target programming language. See Arthur Chargueraud's PhD thesis for full details. *) (** The type Func, used to represent functions *) -Axiom func : Type. +Axiom func : Type. (** The type Func is inhabited *) -Axiom func_inhab : Inhab func. +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']. *) @@ -72,8 +72,8 @@ Axiom eval : forall A B, func -> A -> heap -> B -> heap -> Prop. (** 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 -> +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). @@ -83,7 +83,7 @@ Lemma app_basic_local : forall A B f (x:A), is_local (@app_basic f A x B). Proof using. asserts Hint1: (forall h1 h2, \# h1 h2 -> \# h2 h1). - intros. auto. + intros. auto. asserts Hint2: (forall h1 h2 h3, \# h1 h2 -> \# h1 h3 -> \# h1 (heap_union h2 h3)). intros. rew_disjoint*. asserts Hint3: (forall h1 h2 h3, \# h1 h2 -> \# h2 h3 -> \# h1 h3 -> \# h1 h2 h3) . @@ -97,11 +97,11 @@ Proof using. forwards Hh': (HQ v' h'). subst h'. exists h1' h2. rew_disjoint*. destruct Hh' as (h3'&h4'&?&?&?&?). (* todo: optimize the assertions *) - asserts Hint4: (forall h : heap, \# h h1' -> \# h h2 -> \# h h3'). - intros h0 H01 H02. asserts K: (\# h0 h'). unfold h'. + asserts Hint4: (forall h : heap, \# h h1' -> \# h h2 -> \# h h3'). + intros h0 H01 H02. asserts K: (\# h0 h'). unfold h'. rew_disjoint*. rewrite H10 in K. rew_disjoint*. - asserts Hint5: (forall h : heap, \# h h1' -> \# h h2 -> \# h h4'). - intros h0 H01 H02. asserts K: (\# h0 h'). unfold h'. + asserts Hint5: (forall h : heap, \# h h1' -> \# h h2 -> \# h h4'). + intros h0 H01 H02. asserts K: (\# h0 h'). unfold h'. rew_disjoint*. rewrite H10 in K. rew_disjoint*. exists v' h3' (heap_union h4' i'). splits. subst h h'. rew_disjoint*. @@ -149,7 +149,7 @@ Fixpoint app_def (f:func) (xs:list dynamic) {B} (H:hprop) (Q:B->hprop) : Prop := match xs with | nil => False | (dyn x)::nil => app_basic f x H Q - | (dyn x)::xs => + | (dyn x)::xs => app_basic f x H (fun g => Hexists H', H' \* \[ app_def g xs H' Q]) end. @@ -173,41 +173,41 @@ Notation "'app_keep' f xs H Q" := (** 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), (xs <> nil) -> - app f ((dyn x)::xs) H Q + app f ((dyn x)::xs) H Q = app_basic f x H (fun g => Hexists H', H' \* \[ app_def g xs H' Q]). -Proof using. +Proof using. intros. destruct xs. false. auto. 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), (length xs >= 1)%nat -> - app f ((dyn x)::xs) H Q + app f ((dyn x)::xs) H Q = app_basic f x H (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 *. math. introv N. false. Qed. -Lemma app_ge_2_unfold_extens : +Lemma app_ge_2_unfold_extens : forall (f:func) A (x:A) (xs:list dynamic) B, (xs <> nil) -> app_def f ((dyn x)::xs) (B:=B) = (fun H Q => app_basic f x H (fun g => Hexists H', H' \* \[ app_def g xs H' Q])). -Proof using. +Proof using. introv N. applys fun_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), +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')) -> @@ -215,13 +215,13 @@ Lemma app_wgframe : forall B f xs H H1 H2 (Q1 Q:B->hprop), 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_frame_gc M. + simpls. applys~ local_frame_gc M. rewrite~ app_ge_2_unfold. rewrite~ app_ge_2_unfold in M. applys~ local_frame M. intros g. hpull as HR LR. hsimpl (HR \* H2). applys* IHxs LR. 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 -> Q ===> Q' -> app f xs H Q'. @@ -231,7 +231,7 @@ Qed. (* DEPRECATED -Lemma app_frame : forall B f xs H H' (Q:B->hprop), +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. @@ -240,19 +240,19 @@ Proof using. simpls. applys~ local_frame M. rewrite~ app_ge_2_unfold. rewrite~ app_ge_2_unfold in M. applys~ local_frame M. intros g. - hpull as HR LR. hsimpl (HR \* H'). applys* IHxs. + hpull as HR LR. hsimpl (HR \* H'). applys* IHxs. 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 -> - Q ===> Q' -> + Q ===> Q' -> app f xs H Q'. Proof using. intros B f xs. gen f. induction xs as [|[A x] xs]; introv M W. false. tests E: (xs = nil). simpls. applys~ local_weaken_post M. rewrite~ app_ge_2_unfold'. rewrite~ app_ge_2_unfold' in M. - applys~ local_weaken_post M. intros g. hsimpl. rew_heap. applys* IHxs. + applys~ local_weaken_post M. intros g. hsimpl. rew_heap. applys* IHxs. Qed. *) @@ -270,7 +270,7 @@ Proof using. iff M. apply local_erase. auto. rewrite app_basic_local. - intros h Hh. specializes M Hh. + intros h Hh. specializes M Hh. destruct M as (H1&H2&Q1&R1&R2&R3). exists___. splits. eauto. eauto. intros g. hpull as H' L. hsimpl (H' \* H2). @@ -299,10 +299,10 @@ Fixpoint curried (n:nat) (f:func) : Prop := (** Unfolding lemma for [curried] *) Lemma curried_ge_2_unfold : forall n f, - (n > 1)%nat -> + (n > 1)%nat -> curried n f = forall A (x:A), app_basic f x \[] - (fun g => \[ curried (pred n) g + (fun g => \[ curried (pred n) g /\ forall xs B H (Q:B->hprop), length xs = (pred n) -> app f ((dyn x)::xs) H Q -> app g xs H Q]). Proof using. @@ -313,12 +313,12 @@ Qed. (********************************************************************) (* ** Lemma for over-applications *) -(** [app f (xs++ys)] can be expressed as [app f xs] that returns +(** [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), +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 + app f (xs++ys) H Q = app f xs H (fun g => Hexists H', H' \* \[ app g ys H' Q ]). Proof using. @@ -328,20 +328,20 @@ Proof using. rew_list. simpl. destruct ys. rew_list in *. math. auto. sets_eq xs': (d :: xs). do 2 (rewrite app_ge_2_unfold; [ | subst; rew_list; auto_false ]). - fequal. apply fun_ext_1. intros g. + fequal. apply fun_ext_1. intros g. apply args_eq_1. auto. apply fun_ext_1. intros H'. fequal. fequal. apply IHxs. subst. rew_list. math. math. -Qed. +Qed. (** Alternative formulation *) -Lemma app_over_take : forall n xs f B H (Q:B->hprop), +Lemma app_over_take : forall n xs f B H (Q:B->hprop), (0 < n < length xs)%nat -> - app f xs H Q + app f xs H Q = app f (take n xs) H (fun g => Hexists H', H' \* \[ app g (drop n xs) H' Q ]). Proof using. - introv N. + introv N. forwards* (M&E1&E2): take_app_drop_spec n xs. math. set (xs' := xs) at 1. change xs with xs' in M. rewrite M. subst xs'. rewrite app_over_app; try math. auto. @@ -358,17 +358,17 @@ Qed. Lemma app_partial : forall n xs f, curried n f -> (0 < length xs < n)%nat -> - app f xs \[] (fun g => \[ + app f xs \[] (fun g => \[ curried (n - length xs)%nat g /\ forall ys B H (Q:B->hprop), (length xs + length ys = n)%nat -> app f (xs++ys) H Q -> app g ys H Q]). Proof using. intros n. induction_wf IH: lt_wf n. introv C N. destruct xs as [|[A x] zs]. rew_list in N. math. - rewrite curried_ge_2_unfold in C; [|math]. + rewrite curried_ge_2_unfold in C; [|math]. tests E: (zs = nil). { unfold app_def at 1. eapply local_weaken_post. auto. applys (rm C). - intros g. hpull as [M1 M2]. hsimpl. split. + intros g. hpull as [M1 M2]. hsimpl. split. 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. } @@ -376,9 +376,9 @@ Proof using. eapply local_weaken_post. auto. applys (rm C). clear C. (* todo: make work rm *) intros h. hpull as [M1 M2]. hsimpl. applys app_weaken. applys (rm IH) M1. math. math. clear IH. - intros g. hpull as [N1 N2]. hsimpl. split. + intros g. hpull as [N1 N2]. hsimpl. split. { rew_list. applys_eq N1 2. math. } - { introv P1 P2. rew_list in P1. + { introv P1 P2. rew_list in P1. applys N2. math. applys M2. rew_list; math. rew_list in P2. applys P2. } } @@ -389,8 +389,8 @@ Qed. (* ** Packaging *) -(** [spec f n P] asserts that [curried f n] is true and that - the proposition [P] is a valid specification for [f]. +(** [spec f n P] asserts that [curried f n] is true and that + the proposition [P] is a valid specification for [f]. This formulation is useful for conciseness and tactics. *) Definition spec (f:func) (n:nat) (P:Prop) := @@ -415,11 +415,11 @@ Fixpoint record_repr (L:record_descr) (r:loc) : hprop := match L with | nil => \[] | (f, dyn v)::L' => r ~> record_repr_one f v \* r ~> record_repr L' - end. + end. (* DEPRECATED - Axiom record_repr : record_descr -> loc -> hprop. - Definition record_repr_one (f:nat) A (v:A) (r:loc) : hprop := + Axiom record_repr : record_descr -> loc -> hprop. + Definition record_repr_one (f:nat) A (v:A) (r:loc) : hprop := r ~> record_repr ((f, dyn v)::nil). *) @@ -433,11 +433,11 @@ Definition app_record_new (L:record_descr) : ~~loc := (* Remark: taking the definition below would be a bit of a hack, and it turns out that Coq rejects the definition for universe reasons, because a value of type [dynamic] cannot be stored - into a heap cell, which is itself made of a dynamic value. + into a heap cell, which is itself made of a dynamic value. Axiom record_new : func. Axiom record_new_spec : forall (r:loc) (L:record_descr), - app record_new [L] \[] (# r ~> record_repr L). + app record_new [L] \[] (# r ~> record_repr L). *) (* Axiomatic specification of [get] on a single-field *) @@ -445,8 +445,8 @@ Definition app_record_new (L:record_descr) : ~~loc := Axiom record_get : func. Axiom record_get_spec : forall (r:loc) (f:nat) A (v:A), - app_keep record_get [r f] - (r ~> record_repr_one f v) + app_keep record_get [r f] + (r ~> record_repr_one f v) \[= v]. (* Axiomatic specification of [set] on a single-field *) @@ -454,8 +454,8 @@ Axiom record_get_spec : forall (r:loc) (f:nat) A (v:A), Axiom record_set : func. Axiom record_set_spec : forall (r:loc) (f:nat) A B (v:A) (w:B), - app record_set [r f w] - (r ~> record_repr_one f v) + app record_set [r f w] + (r ~> record_repr_one f v) (# r ~> record_repr_one f w). @@ -466,17 +466,17 @@ Axiom record_set_spec : forall (r:loc) (f:nat) A B (v:A) (w:B), (** Notation for the contents of the fields *) -Notation "`{ f1 := x1 }'" := +Notation "`{ f1 := x1 }'" := ((f1, dyn x1)::nil) - (at level 0, f1 at level 0) + (at level 0, f1 at level 0) : record_scope. Notation "`{ f1 := x1 ; f2 := x2 }'" := ((f1, dyn x1)::(f2, dyn x2)::nil) - (at level 0, f1 at level 0, f2 at level 0) + (at level 0, f1 at level 0, f2 at level 0) : record_scope. Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 }'" := ((f1, dyn x1)::(f2, dyn x2)::(f3, dyn x3)::nil) - (at level 0, f1 at level 0, f2 at level 0, f3 at level 0) + (at level 0, f1 at level 0, f2 at level 0, f3 at level 0) : record_scope. Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 }'" := ((f1, dyn x1)::(f2, dyn x2)::(f3, dyn x3)::(f4, dyn x4)::nil) @@ -484,25 +484,25 @@ Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 }'" := : record_scope. Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 ; f5 := x5 }'" := ((f1, dyn x1)::(f2, dyn x2)::(f3, dyn x3)::(f4, dyn x4)::(f5, dyn x5)::nil) - (at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0, + (at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0, f5 at level 0) : record_scope. Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 ; f5 := x5 ; f6 := x6 }'" := ((f1, dyn x1)::(f2, dyn x2)::(f3, dyn x3)::(f4, dyn x4)::(f5, dyn x5):: (f6, dyn x6)::nil) - (at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0, + (at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0, f5 at level 0, f6 at level 0) : record_scope. Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 ; f5 := x5 ; f6 := x6 ; f7 := x7 }'" := ((f1, dyn x1)::(f2, dyn x2)::(f3, dyn x3)::(f4, dyn x4)::(f5, dyn x5):: (f6, dyn x6)::(f7, dyn x7)::nil) - (at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0, + (at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0, f5 at level 0, f6 at level 0, f7 at level 0) : record_scope. Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 ; f5 := x5 ; f6 := x6 ; f7 := x7 ; f8 := x8 }'" := ((f1, dyn x1)::(f2, dyn x2)::(f3, dyn x3)::(f4, dyn x4)::(f5, dyn x5):: (f6, dyn x6)::(f7, dyn x7)::(f8, dyn x8)::nil) - (at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0, + (at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0, f5 at level 0, f6 at level 0, f7 at level 0, f8 at level 0) : record_scope. @@ -519,11 +519,11 @@ Open Scope charac. Notation "`{ f1 := x1 }" := (rec `{ f1 := x1 }') - (at level 0, f1 at level 0) + (at level 0, f1 at level 0) : charac. Notation "`{ f1 := x1 ; f2 := x2 }" := (rec `{ f1 := x1 ; f2 := x2 }') - (at level 0, f1 at level 0, f2 at level 0) + (at level 0, f1 at level 0, f2 at level 0) : charac. Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 }" := (rec `{ f1 := x1 ; f2 := x2 ; f3 := x3 }') @@ -535,25 +535,25 @@ Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 }" := : charac. Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 ; f5 := x5 }" := (rec `{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 ; f5 := x5 }') - (at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0, + (at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0, f5 at level 0) : charac. Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 ; f5 := x5 ; f6 := x6 }" := - (rec `{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 ; f5 := x5; + (rec `{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 ; f5 := x5; f6 := x6 }') - (at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0, + (at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0, f5 at level 0, f6 at level 0) : charac. Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 ; f5 := x5 ; f6 := x6 ; f7 := x7 }" := (rec `{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 ; f5 := x5; - f6 := x6 ; f7 := x7 }') - (at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0, + f6 := x6 ; f7 := x7 }') + (at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0, f5 at level 0, f6 at level 0, f7 at level 0) : charac. Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 ; f5 := x5 ; f6 := x6 ; f7 := x7 ; f8 := x8 }" := (rec `{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 ; f5 := x5; - f6 := x6 ; f7 := x7 ; f8 := x8 }') - (at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0, + f6 := x6 ; f7 := x7 ; f8 := x8 }') + (at level 0, f1 at level 0, f2 at level 0, f3 at level 0, f4 at level 0, f5 at level 0, f6 at level 0, f7 at level 0, f8 at level 0) : charac. @@ -564,15 +564,15 @@ Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 ; f5 := x5 ; f6 := x6 ; f Fixpoint record_get_compute_dyn (f:nat) (L:record_descr) : option dynamic := match L with | nil => None - | (f',d')::T' => - if Nat.eq_dec f f' - then Some d' + | (f',d')::T' => + if Nat.eq_dec f f' + then Some d' else record_get_compute_dyn f T' end. Definition record_get_compute_spec (f:nat) (L:record_descr) : option Prop := match record_get_compute_dyn f L with - | None => None + | None => None | Some (dyn v) => Some (forall r, app_keep record_get [r f] (r ~> record_repr L) \[= v]) end. @@ -580,23 +580,23 @@ Definition record_get_compute_spec (f:nat) (L:record_descr) : option Prop := Lemma record_get_compute_spec_correct : forall f L (P:Prop), record_get_compute_spec f L = Some P -> P. Proof using. - introv M. unfolds record_get_compute_spec. + introv M. unfolds record_get_compute_spec. sets_eq <- do E: (record_get_compute_dyn f L). destruct do as [[T v]|]; inverts M. - induction L as [|[f' [D' d']] T']; [false|]. + induction L as [|[f' [D' d']] T']; [false|]. simpl in E. intros r. do 2 xunfold record_repr at 1. simpl. case_if in E. (* todo: fix cases_if *) { subst. inverts E. - eapply local_frame. + eapply local_frame. { apply app_local. auto_false. } { apply record_get_spec. } - { hsimpl. } + { hsimpl. } { hsimpl~. } } { specializes IHT' (rm E). - eapply local_frame. + eapply local_frame. { apply app_local. auto_false. } { apply IHT'. } - { hsimpl. } + { hsimpl. } { hsimpl~. } } Qed. (* todo: could use xapply in this proof *) @@ -604,9 +604,9 @@ Qed. (* todo: could use xapply in this proof *) Fixpoint record_set_compute_dyn (f:nat) (d:dynamic) (L:record_descr) : option record_descr := match L with | nil => None - | (f',d')::T' => - if Nat.eq_dec f f' - then Some ((f,d)::T') + | (f',d')::T' => + if Nat.eq_dec f f' + then Some ((f,d)::T') else match record_set_compute_dyn f d T' with | None => None | Some L' => Some ((f',d')::L') @@ -615,7 +615,7 @@ Fixpoint record_set_compute_dyn (f:nat) (d:dynamic) (L:record_descr) : option re Definition record_set_compute_spec (f:nat) A (w:A) (L:record_descr) : option Prop := match record_set_compute_dyn f (dyn w) L with - | None => None + | None => None | Some L' => Some (forall r, app record_set [r f w] (r ~> record_repr L) (# r ~> record_repr L')) end. @@ -623,31 +623,31 @@ Definition record_set_compute_spec (f:nat) A (w:A) (L:record_descr) : option Pro Lemma record_set_compute_spec_correct : forall f A (w:A) L (P:Prop), record_set_compute_spec f w L = Some P -> P. Proof using. - introv M. unfolds record_set_compute_spec. + introv M. unfolds record_set_compute_spec. sets_eq <- do E: (record_set_compute_dyn f (dyn w) L). - destruct do as [L'|]; inverts M. + destruct do as [L'|]; inverts M. gen L'. induction L as [|[f' [T' v']] T]; intros; [false|]. simpl in E. xunfold record_repr at 1. simpl. case_if. (* todo: fix cases_if *) { subst. inverts E. - eapply local_frame. + eapply local_frame. { apply app_local. auto_false. } { apply record_set_spec. } - { hsimpl. } + { hsimpl. } { xunfold record_repr at 2. simpl. hsimpl~. } } { cases (record_set_compute_dyn f Dyn (w) T) as C'; [|false]. inverts E. specializes~ IHT r. - eapply local_frame. + eapply local_frame. { apply app_local. auto_false. } { apply IHT. } - { hsimpl. } + { hsimpl. } { xunfold record_repr at 2. simpl. hsimpl~. } } Qed. (* todo: could use xapply in this proof *) (* DEPRECATED Lemma record_get_compute_spec_correct' : forall f L, - match record_get_compute_spec f L with + match record_get_compute_spec f L with | None => True | Some P => P end. @@ -659,14 +659,3 @@ Qed. (* todo: could use xapply in this proof *) Global Opaque record_repr. - - - - - - - - - - - diff --git a/lib/coq/CFHeaps.v b/lib/coq/CFHeaps.v index d8e448f..e98a9e1 100644 --- a/lib/coq/CFHeaps.v +++ b/lib/coq/CFHeaps.v @@ -108,7 +108,7 @@ Definition null : loc := 0%nat. Definition field : Type := nat. (** Representation of the address of a memory cell, - as a pair of the location at which the object + as a pair of the location at which the object is allocated and the field within this object. *) Definition address : Type := (loc * field)%type. @@ -193,7 +193,7 @@ Proof using. intros [f1 F1] [f2 F2] [f3 F3]. unfolds state_disjoint, state_union. simpls. unfolds pfun_disjoint, pfun_union. extens. iff M [M1 M2]. - split; intros x; specializes M x; + split; intros x; specializes M x; destruct (f2 x); destruct M; auto_false. intros x. specializes M1 x. specializes M2 x. destruct (f2 x); destruct M1; auto_false. @@ -687,8 +687,8 @@ Proof using. Qed. (* later: exploit symmetry in the proof *) Lemma star_comm_assoc : comm_assoc heap_is_star. -Proof using. - apply comm_assoc_of_comm_and_assoc. apply star_comm. apply star_assoc. +Proof using. + apply comm_assoc_of_comm_and_assoc. apply star_comm. apply star_assoc. Qed. Lemma starpost_neutral : forall B (Q:B->hprop), @@ -2443,7 +2443,7 @@ Proof using. asserts: (M \-- x \# x \:= M[x]). rewrite LibMap.disjoint_eq_disjoint_dom. rewrite dom_single. rewrite dom_remove. rewrite disjoint_single_r_eq. - unfold notin. rewrite in_remove_eq. + unfold notin. rewrite in_remove_eq. rewrite notin_single_eq. rew_logic*. applys pred_incl_antisym. (* left to right *) diff --git a/lib/coq/CFLibCredits.v b/lib/coq/CFLibCredits.v index 5c87cee..530638b 100644 --- a/lib/coq/CFLibCredits.v +++ b/lib/coq/CFLibCredits.v @@ -8,8 +8,8 @@ Require Export CFLib. (*---todo : same as in CFLib (why needed?)-- Ltac xlocal_core tt ::= first [ assumption - | apply local_is_local - | apply app_local_1 + | apply local_is_local + | apply app_local_1 | match goal with H: is_local_1 ?S |- is_local (?S _) => apply H end | apply app_local_1 ]. *) @@ -51,42 +51,42 @@ Proof. intros. subst. apply credits_int_zero_eq. Qed. Section SimplIneq. -Lemma ineq_le_refl : forall x, +Lemma ineq_le_refl : forall x, x <= x. Proof using. intros. math. Qed. -Lemma ineq_add_assoc : forall x y z, +Lemma ineq_add_assoc : forall x y z, x + (y + z) = (x + y) + z. Proof using. intros. math. Qed. -Lemma ineq_le_to_ge : forall x y, - x <= y -> +Lemma ineq_le_to_ge : forall x y, + x <= y -> y >= x. Proof using. intros. math. Qed. -Lemma ineq_ge_to_le : forall x y, - x >= y -> +Lemma ineq_ge_to_le : forall x y, + x >= y -> y <= x. Proof using. intros. math. Qed. -Lemma ineq_sub_to_add : forall x y, +Lemma ineq_sub_to_add : forall x y, x - y = x + (-y). Proof using. intros. math. Qed. -Lemma ineq_remove_zero_r : forall x, +Lemma ineq_remove_zero_r : forall x, x + 0 = x. Proof using. intros. math. Qed. -Lemma ineq_remove_zero_l : forall x, +Lemma ineq_remove_zero_l : forall x, 0 + x = x. Proof using. intros. math. Qed. -Lemma simpl_ineq_start_1 : forall x1 y, +Lemma simpl_ineq_start_1 : forall x1 y, 0 + x1 <= y -> x1 <= y. Proof using. intros. math. Qed. -Lemma simpl_ineq_start_2 : forall x1 x2 y, +Lemma simpl_ineq_start_2 : forall x1 x2 y, 0 + x1 + x2 <= y -> x1 + x2 <= y. Proof using. intros. math. Qed. @@ -101,65 +101,65 @@ Lemma simpl_ineq_start_4 : forall x1 x2 x3 x4 y, x1 + x2 + x3 + x4 <= y. Proof using. intros. math. Qed. -Lemma simpl_ineq_zero_r1 : forall x y1, +Lemma simpl_ineq_zero_r1 : forall x y1, x <= y1 + 0 -> x <= y1. Proof using. intros. math. Qed. -Lemma simpl_ineq_zero_r2 : forall x y1 y2, +Lemma simpl_ineq_zero_r2 : forall x y1 y2, x <= 0 + y1 + y2 -> x <= y1 + y2. Proof using. intros. math. Qed. -Lemma simpl_ineq_next : forall x y1 y2 y3, +Lemma simpl_ineq_next : forall x y1 y2 y3, x <= y1 + (y2 + y3) -> x <= (y1 + y2) + y3. Proof using. intros. math. Qed. -Lemma simpl_ineq_zero : forall x y1 y3, +Lemma simpl_ineq_zero : forall x y1 y3, x <= y1 + y3 -> x <= (y1 + 0) + y3. Proof using. intros. math. Qed. -Lemma simpl_ineq_cancel_00 : forall y1 y2 y3, +Lemma simpl_ineq_cancel_00 : forall y1 y2 y3, 0 <= y1 + y3 -> y2 <= y1 + y2 + y3. Proof using. intros. math. Qed. -Lemma simpl_ineq_cancel_0 : forall x1 y1 y2 y3, +Lemma simpl_ineq_cancel_0 : forall x1 y1 y2 y3, x1 <= y1 + y3 -> y2 + x1 <= y1 + y2 + y3. Proof using. intros. math. Qed. -Lemma simpl_ineq_cancel_1 : forall x0 y1 y2 y3, +Lemma simpl_ineq_cancel_1 : forall x0 y1 y2 y3, x0 <= y1 + y3 -> x0 + y2 <= y1 + y2 + y3. Proof using. intros. math. Qed. -Lemma simpl_ineq_cancel_2 : forall x0 x1 y1 y2 y3, +Lemma simpl_ineq_cancel_2 : forall x0 x1 y1 y2 y3, x0 + x1 <= y1 + y3 -> x0 + y2 + x1 <= y1 + y2 + y3. Proof using. intros. math. Qed. -Lemma simpl_ineq_cancel_3 : forall x0 x1 x2 y1 y2 y3, +Lemma simpl_ineq_cancel_3 : forall x0 x1 x2 y1 y2 y3, x0 + x1 + x2 <= y1 + y3 -> x0 + y2 + x1 + x2 <= y1 + y2 + y3. Proof using. intros. math. Qed. -Lemma simpl_ineq_cancel_4 : forall x0 x1 x2 x3 y1 y2 y3, +Lemma simpl_ineq_cancel_4 : forall x0 x1 x2 x3 y1 y2 y3, x0 + x1 + x2 + x3 <= y1 + y3 -> x0 + y2 + x1 + x2 + x3 <= y1 + y2 + y3. Proof using. intros. math. Qed. Lemma int_le_mul_pos_l : forall x y z, - z >= 0 -> - x <= y -> + z >= 0 -> + x <= y -> z * x <= z * y. Proof using. intros. applys~ Z.mul_le_mono_nonneg_l. Qed. Lemma int_le_mul_pos_r : forall x y z, - z >= 0 -> - x <= y -> + z >= 0 -> + x <= y -> x * z <= y * z. Proof using. intros. applys~ Z.mul_le_mono_nonneg_r. Qed. @@ -190,7 +190,7 @@ Hint Rewrite ineq_remove_zero_r ineq_remove_zero_l ineq_add_assoc Ltac simpl_ineq_cleanup tt := autorewrite with simpl_ineq_clean_rew; autorewrite with ineq_add_to_sub_rew; - try apply ineq_le_refl. + try apply ineq_le_refl. Ltac simpl_ineq_find_same Y VL := match VL with @@ -225,7 +225,7 @@ Tactic Notation "simpl_ineq" "*" := simpl_ineq; auto_star. Ltac simpl_ineq_mul_core := try apply ineq_le_to_ge; - repeat (first + repeat (first [ apply int_le_mul_pos_r | apply int_le_mul_pos_l ]). @@ -247,7 +247,7 @@ Ltac simpl_ineq_step tt ::= end end. *) -Lemma simpl_ineq_demo : forall (n:nat) (x y z : int), +Lemma simpl_ineq_demo : forall (n:nat) (x y z : int), ((x + (n * x)%I)%I + y)%I >= ((x + z)%I + (n * x)%I)%I. Proof. intros. dup. @@ -256,7 +256,7 @@ Proof. simpl_ineq_step tt. simpl_ineq_step tt. simpl_ineq_step tt. - simpl_ineq_cleanup tt. + simpl_ineq_cleanup tt. demo. (* fast: *) simpl_ineq. demo. @@ -270,88 +270,88 @@ Qed. (** [rew_ineq H] where H is of the form [x <= y] applies to a goal of the form [a1 + x + a2 <= b] and replaces it with [a1 + y + a2 <= b]. (works also with >= in the other direction; [rew_ineq <- H] also works) *) - + Section RewIneq. -Lemma rew_ineq_l0 : forall x0 x0', +Lemma rew_ineq_l0 : forall x0 x0', x0 <= x0' -> forall y, x0' <= y -> x0 <= y. Proof using. intros. math. Qed. -Lemma rew_ineq_l1f : forall x0 x0', +Lemma rew_ineq_l1f : forall x0 x0', x0 <= x0' -> forall x1 y, x0' + x1 <= y -> x0 + x1 <= y. Proof using. intros. math. Qed. -Lemma rew_ineq_l2f : forall x0 x0', +Lemma rew_ineq_l2f : forall x0 x0', x0 <= x0' -> forall x1 x2 y, x0' + x1 + x2 <= y -> x0 + x1 + x2 <= y. Proof using. intros. math. Qed. -Lemma rew_ineq_l3f : forall x0 x0', +Lemma rew_ineq_l3f : forall x0 x0', x0 <= x0' -> forall x1 x2 x3 y, x0' + x1 + x2 + x3 <= y -> x0 + x1 + x2 + x3 <= y. Proof using. intros. math. Qed. -Lemma rew_ineq_l1 : forall x0 x0', +Lemma rew_ineq_l1 : forall x0 x0', x0 <= x0' -> forall x1 y, x1 + x0' <= y -> x1 + x0 <= y. Proof using. intros. math. Qed. -Lemma rew_ineq_l2 : forall x0 x0', +Lemma rew_ineq_l2 : forall x0 x0', x0 <= x0' -> forall x1 x2 y, x1 + x0' + x2 <= y -> x1 + x0 + x2 <= y. Proof using. intros. math. Qed. -Lemma rew_ineq_l3 : forall x0 x0', +Lemma rew_ineq_l3 : forall x0 x0', x0 <= x0' -> forall x1 x2 x3 y, x1 + x0' + x2 + x3 <= y -> x1 + x0 + x2 + x3 <= y. Proof using. intros. math. Qed. -Lemma rew_ineq_r0 : forall x0 x0', +Lemma rew_ineq_r0 : forall x0 x0', x0 <= x0' -> forall y, y <= x0 -> y <= x0'. Proof using. intros. math. Qed. -Lemma rew_ineq_r1f : forall x0 x0', +Lemma rew_ineq_r1f : forall x0 x0', x0 <= x0' -> forall x1 y, y <= x0 + x1 -> y <= x0' + x1. Proof using. intros. math. Qed. -Lemma rew_ineq_r2f : forall x0 x0', +Lemma rew_ineq_r2f : forall x0 x0', x0 <= x0' -> forall x1 x2 y, y <= x0 + x1 + x2 -> y <= x0' + x1 + x2. Proof using. intros. math. Qed. -Lemma rew_ineq_r3f : forall x0 x0', +Lemma rew_ineq_r3f : forall x0 x0', x0 <= x0' -> forall x1 x2 x3 y, y <= x0 + x1 + x2 + x3 -> y <= x0' + x1 + x2 + x3. Proof using. intros. math. Qed. -Lemma rew_ineq_r1 : forall x0 x0', +Lemma rew_ineq_r1 : forall x0 x0', x0 <= x0' -> forall x1 y, y <= x1 + x0 -> y <= x1 + x0'. Proof using. intros. math. Qed. -Lemma rew_ineq_r2 : forall x0 x0', +Lemma rew_ineq_r2 : forall x0 x0', x0 <= x0' -> forall x1 x2 y, y <= x1 + x0 + x2 -> y <= x1 + x0' + x2. Proof using. intros. math. Qed. -Lemma rew_ineq_r3 : forall x0 x0', +Lemma rew_ineq_r3 : forall x0 x0', x0 <= x0' -> forall x1 x2 x3 y, y <= x1 + x0 + x2 + x3 -> y <= x1 + x0' + x2 + x3. @@ -369,9 +369,9 @@ Ltac ineq_ensure_le H := end. Ltac rew_ineq_l H' := - ineq_ensure_goal_le tt; + ineq_ensure_goal_le tt; let H := ineq_ensure_le H' in - first + first [ apply (@rew_ineq_l0 _ _ H) | apply (@rew_ineq_l1 _ _ H) | apply (@rew_ineq_l2 _ _ H) @@ -382,9 +382,9 @@ Ltac rew_ineq_l H' := ]. Ltac rew_ineq_r H' := - ineq_ensure_goal_le tt; + ineq_ensure_goal_le tt; let H := ineq_ensure_le H' in - first + first [ apply (@rew_ineq_r0 _ _ H) | apply (@rew_ineq_r1 _ _ H) | apply (@rew_ineq_r2 _ _ H) @@ -446,7 +446,7 @@ Lemma rew_ineq_demo : forall x1 x2 x3 x4 x5 x6 x7 x8, x5 + x1 + x6 <= x7 + x4 + x8. Proof. introv H1 H2. rew_ineq H1. rew_ineq <- H2. - demo. + demo. Qed. End Ineq_demos. @@ -509,7 +509,7 @@ Lemma int_add_assoc : forall x y z, x + (y+z) = x + y + z. Proof using. math. Qed. -Lemma int_mul_plus_one_l : forall n x, +Lemma int_mul_plus_one_l : forall n x, (1+n) * x = x + n*x. Proof using. intros. math_setup. ring. Qed. @@ -520,7 +520,7 @@ Proof using. intros. math_setup. ring. Qed. Hint Rewrite int_mul_assoc int_add_assoc int_mul_zero_l int_mul_one_l int_mul_zero_nat_l int_mul_one_nat_l int_mul_zero_r int_mul_one_r int_mul_zero_nat_r int_mul_one_nat_r - int_add_nat int_mul_succ_nat int_mul_plus_one_nat + int_add_nat int_mul_succ_nat int_mul_plus_one_nat int_mul_plus_one_l int_mul_plus_one_r : rew_nat_to_int. Tactic Notation "rew_nat_to_int" := @@ -533,14 +533,14 @@ Tactic Notation "rew_nat_to_int" := (** [simpl_credits] to simplify an expression or inequality involving credits *) Ltac simpl_credits_core := - rew_nat_to_int; + rew_nat_to_int; match goal with | |- (_ <= _)%I => try simpl_ineq | |- (_ >= _)%I => try simpl_ineq | |- (_ = _ :> int) => idtac end. -Tactic Notation "simpl_credits" := +Tactic Notation "simpl_credits" := simpl_credits_core. Tactic Notation "simpl_credits" "~" := simpl_credits; auto_tilde. @@ -549,9 +549,9 @@ Tactic Notation "simpl_credits" "*" := (** Demo *) -Lemma simpl_credits_demo : forall (n:nat) (x y z : int), +Lemma simpl_credits_demo : forall (n:nat) (x y z : int), (1+n)%nat * x + y >= x + z + n * x. -Proof. intros. simpl_credits. demo. Qed. +Proof. intros. simpl_credits. demo. Qed. @@ -564,17 +564,17 @@ Proof. intros. simpl_credits. demo. Qed. Section SimplNonneg. -Lemma nonneg_nat : forall (n:nat), +Lemma nonneg_nat : forall (n:nat), (0 <= n)%I. Proof using. intros. math. Qed. -Lemma nonneg_add : forall x y, +Lemma nonneg_add : forall x y, 0 <= x -> 0 <= y -> 0 <= (x + y). Proof using. intros. math. Qed. -Lemma nonneg_mul : forall x y, +Lemma nonneg_mul : forall x y, 0 <= x -> 0 <= y -> 0 <= (x * y). @@ -606,7 +606,7 @@ Tactic Notation "simpl_nonneg" "~" := simpl_nonneg; xauto~. Tactic Notation "simpl_nonneg" "*" := simpl_nonneg; xauto*. - + Hint Resolve nonneg_nat ineq_le_to_ge nonneg_add nonneg_mul : nonneg. @@ -619,10 +619,10 @@ Hint Resolve nonneg_nat ineq_le_to_ge nonneg_add nonneg_mul : nonneg. or [math]. *) Ltac csimpl_core := - try hsimpl_credits; try simpl_credits; + try hsimpl_credits; try simpl_credits; try solve [ simpl_nonneg | math ]. - -Tactic Notation "csimpl" := + +Tactic Notation "csimpl" := csimpl_core. @@ -631,10 +631,9 @@ Tactic Notation "csimpl" := (********************************************************************) (** Tactic [ximpl_credits] *) -Tactic Notation "xsimpl_credits" := +Tactic Notation "xsimpl_credits" := hsimpl_credits_core. -Tactic Notation "xsimpl_credits" "~" := +Tactic Notation "xsimpl_credits" "~" := xsimpl_credits; auto_tilde. -Tactic Notation "xsimpl_credits" "*" := +Tactic Notation "xsimpl_credits" "*" := xsimpl_credits; auto_star. - diff --git a/lib/coq/CFLibCreditsNat.v b/lib/coq/CFLibCreditsNat.v deleted file mode 100644 index 835324b..0000000 --- a/lib/coq/CFLibCreditsNat.v +++ /dev/null @@ -1,7 +0,0 @@ -Require Export CFLibCredits. - -Ltac xpay_core tt ::= xpay_nat_core tt. - -Notation "'\$' x" := (\$_nat x) - (at level 40, format "\$ x") : heap_scope. - diff --git a/lib/coq/CFTactics.v b/lib/coq/CFTactics.v index 1578842..7bd5022 100644 --- a/lib/coq/CFTactics.v +++ b/lib/coq/CFTactics.v @@ -1067,7 +1067,7 @@ Qed. Ltac xlet_core cont0 cont1 cont2 := apply local_erase; - match goal with |- cf_let ?F1 (fun x => _) ?H ?Q => + match goal with |- cf_let ?F1 (fun x => _) ?H ?Q => cont0 tt; split; [ | cont1 x; cont2 tt ]; xtag_pre_post @@ -3853,10 +3853,10 @@ Ltac xcredit goal := (** [xpay] applys to a goal of the form [(Pay_ ;; F1) H Q]. It is used to eliminate the call to Pay, by spending one credit. - + [xpay (n + m)] where [n] and [m] are numbers such that: where [n] denotes the remainder, and [m] denotes the - payment that need to be performed (e.g. 1). + payment that need to be performed (e.g. 1). WARNING: the interface of the latter might change. LATER: add demos for this tactic. *) @@ -3886,8 +3886,8 @@ Tactic Notation "xpay" constr(goal) := (* ** [xpay_skip] *) (** [xpay_skip] is used to skip the paying of one credit; - use it for development purposes only. - + use it for development purposes only. + LATER: add demos for this tactic. *) Ltac xpay_fake tt := @@ -3903,11 +3903,11 @@ Tactic Notation "xpay_skip" := xpay_fake tt. (*--------------------------------------------------------*) (* ** [xgc_credit] *) -(* [xgc_credit_core HP] applies to a term [HP] that is an inequality - between two credit expressions, e.g. [m <= n]. +(* [xgc_credit_core HP] applies to a term [HP] that is an inequality + between two credit expressions, e.g. [m <= n]. This inequality is used to change [\$n] to [\$m] in the precondition of the goal. - + LATER: add demos for this tactic. *) Ltac xgc_credit_core HP := @@ -3927,8 +3927,8 @@ Tactic Notation "xgc_credit" constr(HP) := in the goal, by replacing [\$ x] with the empty heap predicate \[]. Implementing using [skip_credits] then [hsimpl]. - Should only be used for development purpose. - + Should only be used for development purpose. + LATER: add demos for this tactic. *) Ltac xskip_credits_base := diff --git a/lib/stdlib/Pervasives_proof.v b/lib/stdlib/Pervasives_proof.v index d68ec3a..2ef585b 100644 --- a/lib/stdlib/Pervasives_proof.v +++ b/lib/stdlib/Pervasives_proof.v @@ -25,8 +25,8 @@ Hint Extern 1 (RegisterSpec not) => Provide not_spec. - [==] at type [loc] implements comparison of locations - [==] in general, if it returns true, then implies logical equality. - The first specification is used by default. - Use [xapp_spec infix_eq_eq_gen_spec] for the latter. + The first specification is used by default. + Use [xapp_spec infix_eq_eq_gen_spec] for the latter. *) Parameter infix_eq_eq_loc_spec : curried 2%nat infix_eq_eq__ /\ @@ -142,9 +142,9 @@ Hint Extern 1 (RegisterSpec infix_star__) => Provide infix_star_spec. Hint Extern 1 (RegisterSpec infix_slash__) => Provide infix_slash_spec. Hint Extern 1 (RegisterSpec Pervasives_ml.mod) => Provide mod_spec. -Notation "x `/` y" := (Z.quot x y) +Notation "x `/` y" := (Z.quot x y) (at level 69, right associativity) : charac. -Notation "x `mod` y" := (Z.rem x y) +Notation "x `mod` y" := (Z.rem x y) (at level 69, no associativity) : charac. (* TODO: check levels for these notations *) @@ -240,7 +240,7 @@ Hint Extern 1 (RegisterSpec asr) => Provide asr_spec. (************************************************************) (** References *) -Definition Ref {A} (v:A) (r:loc) := +Definition Ref {A} (v:A) (r:loc) := r ~> `{ contents' := v }. Axiom Ref_Heapdata : forall A, @@ -251,9 +251,9 @@ Existing Instance Ref_Heapdata. (* Proof using. intros. applys Heapdata_prove. intros x X1 X2. - xunfold @Ref. + xunfold @Ref. lets: star_is_single_same_loc. - hchange (@star_is_single_same_loc x). hsimpl. + hchange (@star_is_single_same_loc x). hsimpl. Qed. *) @@ -261,13 +261,13 @@ Notation "r '~~>' v" := (hdata (Ref v) r) (at level 32, no associativity) : heap_scope. Lemma ref_spec : forall A (v:A), - app ref [v] - PRE \[] + app ref [v] + PRE \[] POST (fun r => r ~~> v). Proof using. xcf_go~. Qed. Lemma infix_emark_spec : forall A (v:A) r, - app infix_emark__ [r] + app infix_emark__ [r] INV (r ~~> v) POST \[= v]. Proof using. xunfold @Ref. xcf_go~. Qed. @@ -289,8 +289,8 @@ Notation "'App'' r `:= x" := (App infix_colon_eq__ r x;) format "'App'' r `:= x") : charac. Lemma incr_spec : forall (n:int) r, - app incr [r] - PRE (r ~~> n) + app incr [r] + PRE (r ~~> n) POST (# r ~~> (n+1)). Proof using. xcf_go~. Qed. @@ -309,7 +309,7 @@ Hint Extern 1 (RegisterSpec decr) => Provide decr_spec. (** Group of References *) Axiom ref_spec_group : forall A (M:map loc A) (v:A), - app Pervasives_ml.ref [v] + app Pervasives_ml.ref [v] PRE (Group Ref M) POST (fun (r:loc) => Group Ref (M[r:=v]) \* \[r \notindom M]). (* TODO: proof *) @@ -325,10 +325,10 @@ Qed. Lemma infix_colon_eq_spec_group : forall `{Inhab A} (M:map loc A) (v:A) r, r \indom M -> - app Pervasives_ml.infix_colon_eq__ [r v] + app Pervasives_ml.infix_colon_eq__ [r v] PRE (Group Ref M) POST (# Group Ref (M[r:=v])). -Proof using. +Proof using. intros. rewrite~ (Group_rem r M). xapp. intros tt. hchanges~ (Group_add' r M). Qed. @@ -338,14 +338,14 @@ Qed. (** Pairs *) Lemma fst_spec : forall A B (x:A) (y:B), - app fst [(x,y)] - PRE \[] + app fst [(x,y)] + PRE \[] POST \[= x]. Proof using. xcf_go~. Qed. Lemma snd_spec : forall A B (x:A) (y:B), - app snd [(x,y)] - PRE \[] + app snd [(x,y)] + PRE \[] POST \[= y]. Proof using. xcf_go~. Qed. @@ -356,9 +356,9 @@ Hint Extern 1 (RegisterSpec snd) => Provide snd_spec. (************************************************************) (** Unit *) -Lemma ignore_spec : - app ignore [tt] - PRE \[] +Lemma ignore_spec : + app ignore [tt] + PRE \[] POST \[= tt]. Proof using. xcf_go~. Qed. @@ -392,7 +392,7 @@ Instance Ref_Heapdata : forall a A (T:htype A a), Proof using. intros. applys Heapdata_prove. intros x X1 X2. unfold Ref. hdata_simpl. hextract as x1 x2. - hchange (@star_is_single_same_loc x). hsimpl. + hchange (@star_is_single_same_loc x). hsimpl. Qed. Open Local Scope heap_scope_advanced. @@ -402,7 +402,7 @@ Notation "'~~>' v" := (~> Ref (@Id _) v) (* Notation "l '~~>' v" := (r ~> Ref (@Id _) v) - (at level 32, no associativity) : heap_scope. + (at level 32, no associativity) : heap_scope. *) Notation "l '~~>' v" := (hdata (@Ref _ _ (@Id _) v) r) (at level 32, no associativity) : heap_scope. -- GitLab From cfcd372f8852a29bc5bee3624de2119e36f5e750 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Arma=C3=ABl=20Gu=C3=A9neau?= <armael.gueneau@ens-lyon.fr> Date: Mon, 8 Jan 2018 16:21:47 +0100 Subject: [PATCH 2/6] Credits are now a linear resource We can now have a negative number of credits (and this doesn't imply False), but garbage-collection of resources has been restricted: only a positive number of credits can be discarded. --- lib/coq/CFApp.v | 11 +- lib/coq/CFHeaps.v | 441 +++++++++++++++------------------- lib/coq/CFLibCredits.v | 13 +- lib/coq/CFTactics.v | 30 ++- lib/stdlib/Array_proof.v | 4 + lib/stdlib/Pervasives_proof.v | 4 + 6 files changed, 236 insertions(+), 267 deletions(-) diff --git a/lib/coq/CFApp.v b/lib/coq/CFApp.v index 3f7e674..5f85c87 100644 --- a/lib/coq/CFApp.v +++ b/lib/coq/CFApp.v @@ -210,7 +210,7 @@ Qed. 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')) -> + (Q1 \*+ H2) ===> (Q \*+ \GC) -> app f xs H Q. Proof using. intros B f xs. gen f. induction xs as [|[A x] xs]; introv M WH WQ. false. @@ -223,10 +223,11 @@ 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~ \[]. + Q ===> Q' -> + app f xs H Q'. +Proof using. + introv M W. applys* app_wgframe. hsimpl. intros r. + hchange W. hsimpl. Qed. (* DEPRECATED diff --git a/lib/coq/CFHeaps.v b/lib/coq/CFHeaps.v index e98a9e1..dbcbb4d 100644 --- a/lib/coq/CFHeaps.v +++ b/lib/coq/CFHeaps.v @@ -275,17 +275,25 @@ Tactic Notation "rew_disjoint" "*" := (** Representation of credits *) -Definition credits_type : Type := nat. +Definition credits_type : Type := int. (** Zero and one credits *) -Definition credits_zero : credits_type := 0%nat. -Definition credits_one : credits_type := 1%nat. +Definition credits_zero : credits_type := 0. +Definition credits_one : credits_type := 1. (** Representation of heaps *) Definition heap : Type := (state * credits_type)%type. +(** Projections *) + +Definition heap_state (h:heap) : state := + match h with (m,_) => m end. + +Definition heap_credits (h:heap) : credits_type := + match h with (_,c) => c end. + (** Predicate over pairs *) Definition prod_st A B (v:A*B) (P:A->Prop) (Q:B->Prop) := (* todo move to TLC *) @@ -312,7 +320,7 @@ Notation "\# h1 h2" := (heap_disjoint h1 h2) (** Union of heaps *) Definition heap_union (h1 h2 : heap) : heap := - prod_func state_union (fun a b => (a + b)%nat) h1 h2. + prod_func state_union (fun a b => (a + b)) h1 h2. Notation "h1 \+ h2" := (heap_union h1 h2) (at level 51, right associativity). @@ -320,8 +328,12 @@ Notation "h1 \+ h2" := (heap_union h1 h2) (** Empty heap *) Definition heap_empty : heap := - (state_empty, 0%nat). + (state_empty, 0). +(** Affine heaps *) + +Definition heap_affine (h: heap) : Prop := + 0 <= heap_credits h. (*------------------------------------------------------------------*) (* ** Properties on heaps *) @@ -411,6 +423,31 @@ Proof using. fequals. applys state_union_assoc. math. Qed. +(** Affine *) + +Lemma heap_affine_empty : + heap_affine heap_empty. +Proof. + unfold heap_affine, heap_empty. simpl. + math. +Qed. + +Lemma heap_affine_union : forall h1 h2, + heap_affine h1 -> + heap_affine h2 -> + heap_affine (h1 \+ h2). +Proof. + intros (m1 & c1) (m2 & c2) HA1 HA2. + unfold heap_affine, heap_union, prod_func in *. simpl in *. + math. +Qed. + +Lemma heap_affine_credits : forall c, + 0 <= c -> + heap_affine (state_empty, c). +Proof. auto. Qed. + + (** Hints and tactics *) Hint Resolve heap_union_neutral_l heap_union_neutral_r. @@ -455,6 +492,11 @@ Definition heap_is_star (H1 H2 : hprop) : hprop := /\ heap_disjoint h1 h2 /\ h = heap_union h1 h2. +(** Affine heap predicates *) + +Definition affine (H : hprop) : Prop := + forall h, H h -> heap_affine h. + (** Lifting of existentials *) Definition heap_is_pack A (Hof : A -> hprop) : hprop := @@ -465,21 +507,18 @@ Definition heap_is_pack A (Hof : A -> hprop) : hprop := Definition heap_is_empty_st (H:Prop) : hprop := fun h => h = heap_empty /\ H. -(** Garbage collection predicate: [Hexists H, H]. *) +(** Garbage collection predicate: equivalent to [Hexists H, H \* \[affine H]]. *) Definition heap_is_gc : hprop := - heap_is_pack (fun H => H). + fun h => heap_affine h /\ exists H, H h. (** Credits *) -Definition heap_is_credits_nat (n:nat) : hprop := - fun h => let (m,n') := h in m = state_empty /\ n' = n. - -Definition heap_is_credits_int (x:int) : hprop := - heap_is_star (heap_is_credits_nat (abs x)) (heap_is_empty_st (x >= 0)%I). +Definition heap_is_credits (x:int) : hprop := + fun h => let (m,x') := h in m = state_empty /\ x' = x. Opaque heap_union state_single heap_is_star heap_is_pack - heap_is_credits_nat heap_is_credits_int. + heap_is_gc heap_is_credits heap_affine affine. (** Hprop is inhabited *) @@ -505,10 +544,7 @@ Notation "H1 '\*' H2" := (heap_is_star H1 H2) Notation "\GC" := (heap_is_gc) : heap_scope. -Notation "'\$_nat' n" := (heap_is_credits_nat n) - (at level 40, format "\$_nat n") : heap_scope. - -Notation "'\$' x" := (heap_is_credits_int x) +Notation "'\$' x" := (heap_is_credits x) (at level 40, format "\$ x") : heap_scope. Notation "'Hexists' x1 , H" := (heap_is_pack (fun x1 => H)) @@ -781,24 +817,24 @@ Tactic Notation "rew_heap" "*" "in" hyp(H) := (* ** Properties of heap credits *) Section Credits. -Transparent heap_is_credits_nat heap_is_credits_int +Transparent heap_is_credits heap_is_empty heap_is_empty_st heap_is_star heap_union heap_disjoint. Definition pay_one H H' := - H ==> \$ 1%I \* H'. + H ==> \$ 1 \* H'. -Lemma credits_nat_zero_eq : \$_nat 0 = \[]. +Lemma credits_zero_eq : \$ 0 = \[]. Proof using. - unfold heap_is_credits_nat, heap_is_empty, heap_empty. + unfold heap_is_credits, heap_is_empty, heap_empty. applys pred_ext_1. intros [m n]. iff [M1 M2] M. (* todo: extens should work *) subst*. inverts* M. Qed. -Lemma credits_nat_split_eq : forall (n m : nat), - \$_nat (n+m) = \$_nat n \* \$_nat m. +Lemma credits_split_eq : forall (n m : int), + \$ (n+m) = \$ n \* \$ m. Proof using. - intros c1 c2. unfold heap_is_credits_nat, heap_is_star, heap_union, heap_disjoint. + intros c1 c2. unfold heap_is_credits, heap_is_star, heap_union, heap_disjoint. applys pred_ext_1. intros [m n]. (* todo: extens should work *) iff [M1 M2] ([m1 n1]&[m2 n2]&(M1&E1)&(M2&E2)&M3&M4). exists (state_empty,c1) (state_empty,c2). simpl. splits*. @@ -807,60 +843,39 @@ Proof using. inverts M4. subst*. Qed. -Lemma credits_nat_le : forall (n m : nat), - (n >= m)%nat -> \$_nat n ==> \$_nat m \* \$_nat (n-m). -Proof using. - introv M. rewrite <- credits_nat_split_eq. - math_rewrite (m + (n-m) = n)%nat. auto. -Qed. - -Lemma credits_nat_le_rest : forall (n m : nat), (* todo: move later, inverse hyp *) - (n <= m)%nat -> exists H', \$_nat m ==> \$_nat n \* H'. -Proof using. - introv M. exists (\$_nat (m - n)). rewrite <- credits_nat_split_eq. - math_rewrite (n + (m-n) = m)%nat. auto. -Qed. - -Lemma credits_int_zero_eq : \$ 0%I = \[]. +Lemma credits_le_rest : forall (n m : int), (* todo: move later, inverse hyp *) + n <= m -> exists H', affine H' /\ \$ m ==> \$ n \* H'. Proof using. - unfold heap_is_credits_int. change (abs 0) with (0%nat). - rewrite credits_nat_zero_eq. (* hsimpl would prove the goal here *) - unfold heap_is_star, heap_is_empty, heap_is_empty_st. - applys pred_ext_1. iff (h1&h2&H1&(H2&E)&D&U) E. - subst. autos* state_disjoint_empty_l. - subst. exists heap_empty heap_empty. splits~. splits~. math. + introv M. exists (\$ (m - n)). rewrite <- credits_split_eq. + math_rewrite (n + (m-n) = m). + splits~. + Local Transparent affine. unfold affine, heap_is_credits. + intros (? & ?) (? & ?); subst. apply heap_affine_credits. + math. Qed. -Lemma credits_int_split_eq : forall (x y : int), - (x >= 0) -> (y >= 0) -> - \$(x+y) = \$ x \* \$ y. +Lemma credits_join_eq : forall x y, + \$ x \* \$ y = \$(x+y). Proof using. - introv Px Py. unfold heap_is_credits_int. rew_heap. - rewrite (star_comm \[x >= 0]). rew_heap. - rewrite star_assoc. rewrite <- credits_nat_split_eq. - rewrite~ abs_plus. (* hsimpl would prove the goal here *) - unfold heap_is_star, heap_is_empty_st. - applys pred_ext_1. iff (h1&h2&H1&(H2&E)&D&U). - subst. exists h1 heap_empty. splits~. exists heap_empty heap_empty. splits~. - subst. destruct E as (h3&(E3&P3)&(E4&P4)&D'&U'). - subst. exists h1 heap_empty. splits~. splits~. math. fequal. - autos* state_disjoint_empty_r. -Qed. + introv. unfold heap_is_credits. + applys pred_ext_1. intros h. splits. + { intros ([m1 c1] & [m2 c2] & ([? ?] & [? ?] & [[? ?] ?])). + subst. unfold heap_union. simpl. + rewrite state_union_neutral_r. splits~. } + { destruct h as [m c]. intros (? & ?). subst. + unfold heap_is_star. + exists (state_empty, x) (state_empty, y). + splits~. + { unfold heap_disjoint. simpl. + splits~. apply state_disjoint_empty_l. } + { unfold heap_union. simpl. + rewrite~ state_union_neutral_r. } } + Qed. -Lemma credits_int_le : forall (x y : int), - (x >= y)%I -> (y >= 0)%I -> \$ x ==> \$ y \* \$ (x-y). +Lemma credits_join_eq_rest : forall x y (H:hprop), + \$ x \* \$ y \* H = \$(x+y) \* H. Proof using. - introv M N. unfold heap_is_credits_int. rew_heap. - unfold heap_is_star, heap_is_empty_st. - intros h (h1&h2&H1&(H2&E)&D&U). destruct h1 as [c1 n1]. - destruct H1 as [C1 N1]. subst. - exists (state_empty,abs y). exists (state_empty,abs (x-y)). - splits~. constructors~. exists heap_empty. - exists (state_empty,abs (x-y)). splits~. - esplit. esplit. splits~. constructors~. splits~. math. - simpl. fequals. rewrite~ <- abs_plus. rewrite LibNat.plus_zero_r. - fequals. math. - math. + introv. rewrite star_assoc. rewrite~ credits_join_eq. Qed. End Credits. @@ -871,7 +886,7 @@ End Credits. (** Tactic [credits_split] converts [\$(x+y) \* ...] into [\$x \* \$y \* ...] *) -Hint Rewrite credits_int_split_eq credits_nat_split_eq : credits_split_rew. +Hint Rewrite credits_split_eq : credits_split_rew. Ltac credits_split := autorewrite with credits_split_rew. @@ -882,38 +897,11 @@ Lemma credits_swap : forall x (H:hprop), H \* (\$ x) = (\$ x) \* H. Proof using. intros. rewrite~ star_comm. Qed. -(* need additional nonnegativity hypotheses - -Lemma credits_join_eq : forall x y, - \$ x \* \$ y = \$(x+y). -Proof using. .... Qed. - -Lemma credits_join_eq_rest : forall x y (H:hprop), - \$ x \* \$ y \* H = \$(x+y) \* H. -Proof using. ..... Qed. - -*) - -(* TODO: above should be rewritten with pre-condition x>=0 and y>=0 - which can be extracted from left-hand-side *) - -Lemma credits_nat_join_eq : forall x y, - \$_nat x \* \$_nat y = \$_nat(x+y). -Proof using. intros. rewrite~ credits_nat_split_eq. Qed. - -Lemma credits_nat_join_eq_rest : forall x y (H:hprop), - \$_nat x \* \$_nat y \* H = \$_nat(x+y) \* H. -Proof using. intros. rewrite~ credits_nat_split_eq. rewrite~ star_assoc. Qed. - Ltac credits_join_in H := match H with - | \$_nat ?x \* \$_nat ?y => rewrite (@credits_nat_join_eq x y) - | \$_nat ?x \* \$_nat ?y \* ?H' => rewrite (@credits_nat_join_eq_rest x y H') -(* TODO: activate these once lemmas are proved | \$ ?x \* \$ ?y => rewrite (@credits_join_eq x y) | \$ ?x \* \$ ?y \* ?H' => rewrite (@credits_join_eq_rest x y H') -*) | _ \* ?H' => credits_join_in H' end. @@ -1037,6 +1025,70 @@ Definition Group a A (G:htype A a) (M:map a A) := \* \[LibMap.finite M]. +(*------------------------------------------------------------------*) +(* ** Properties of [affine] *) + +Section Affine. +Transparent affine. + +Lemma affine_empty : + affine \[]. +Proof. + unfold affine, heap_is_empty. intros; subst. + apply heap_affine_empty. +Qed. + +Lemma affine_star : forall H1 H2, + affine H1 -> + affine H2 -> + affine (H1 \* H2). +Proof. + Transparent heap_is_star. + introv HA1 HA2. unfold affine, heap_is_star in *. + intros h (? & ? & ? & ? & ? & ?). subst. + apply~ heap_affine_union. +Qed. + +Lemma affine_credits : forall c, + 0 <= c -> + affine (\$ c). +Proof. + Transparent heap_is_credits. + introv N. unfold affine, heap_is_credits. + intros (m & c'). intros (? & ?). subst. + apply~ heap_affine_credits. +Qed. + +Lemma affine_empty_st : forall P, + affine \[P]. +Proof. + Transparent heap_is_empty_st. + introv. unfold affine, heap_is_empty_st. + introv (? & ?); subst. + apply heap_affine_empty. +Qed. + +Lemma affine_gc : + affine \GC. +Proof. + Transparent heap_is_gc. + unfold affine, heap_is_gc. + tauto. +Qed. + +(* affine_hdata? *) + +End Affine. + +Hint Resolve + affine_empty affine_star affine_credits affine_empty_st + affine_gc +: affine. + +Ltac affine := + match goal with |- affine _ => eauto with affine zarith end. + + (********************************************************************) (* ** [xunfold] tactics *) @@ -1551,8 +1603,14 @@ Proof using. Qed. Lemma hsimpl_gc : forall H, + affine H -> H ==> \GC. -Proof using. intros. unfold heap_is_gc. introv M. exists~ H. Qed. +Proof using. + Local Transparent affine heap_is_gc. + introv HA. unfold heap_is_gc, pred_incl. + intros h Hh. unfold affine in HA. + splits~. eauto. +Qed. Lemma hsimpl_cancel_1 : forall H HA HR HT, HT ==> HA \* HR -> H \* HT ==> HA \* (H \* HR). @@ -1603,128 +1661,61 @@ Lemma hsimpl_cancel_10 : forall H HA HR H1 H2 H3 H4 H5 H6 H7 H8 H9 HT, Proof using. intros. rewrite (star_comm_assoc H9). apply~ hsimpl_cancel_9. Qed. -Lemma hsimpl_cancel_credits_nat_1 : forall (n m : nat) HA HR HT, - (n >= m)%nat -> - \$_nat (n - m) \* HT ==> HA \* HR -> - \$_nat n \* HT ==> HA \* (\$_nat m \* HR). +Lemma hsimpl_cancel_credits_1 : forall (n m : int) HA HR HT, + \$ (n - m) \* HT ==> HA \* HR -> + \$ n \* HT ==> HA \* (\$ m \* HR). Proof using. - introv L E. math_rewrite (n = (n - m) + m)%nat. - rewrite credits_nat_split_eq. rewrite <- star_assoc. + introv E. math_rewrite (n = (n - m) + m). + rewrite credits_split_eq. rewrite <- star_assoc. applys~ hsimpl_cancel_2. Qed. -Lemma hsimpl_cancel_credits_nat_2 : forall (n m : nat) HA HR H1 HT, - (n >= m)%nat -> \$_nat (n - m) \* H1 \* HT ==> HA \* HR -> - H1 \* \$_nat n \* HT ==> HA \* (\$_nat m \* HR). -Proof using. - intros. rewrite (star_comm_assoc H1). apply~ hsimpl_cancel_credits_nat_1. -Qed. - -Lemma hsimpl_cancel_credits_nat_3 : forall (n m : nat) HA HR H1 H2 HT, - (n >= m)%nat -> \$_nat (n - m) \* H1 \* H2 \* HT ==> HA \* HR -> - H1 \* H2 \* \$_nat n \* HT ==> HA \* (\$_nat m \* HR). -Proof using. intros. rewrite (star_comm_assoc H2). apply~ hsimpl_cancel_credits_nat_2. Qed. - -Lemma hsimpl_cancel_credits_nat_4 : forall (n m : nat) HA HR H1 H2 H3 HT, - (n >= m)%nat -> \$_nat (n - m) \* H1 \* H2 \* H3 \* HT ==> HA \* HR -> - H1 \* H2 \* H3 \* \$_nat n \* HT ==> HA \* (\$_nat m \* HR). -Proof using. intros. rewrite (star_comm_assoc H3). apply~ hsimpl_cancel_credits_nat_3. Qed. - -Lemma hsimpl_cancel_credits_nat_5 : forall (n m : nat) HA HR H1 H2 H3 H4 HT, - (n >= m)%nat -> \$_nat (n - m) \* H1 \* H2 \* H3 \* H4 \* HT ==> HA \* HR -> - H1 \* H2 \* H3 \* H4 \* \$_nat n \* HT ==> HA \* (\$_nat m \* HR). -Proof using. intros. rewrite (star_comm_assoc H4). apply~ hsimpl_cancel_credits_nat_4. Qed. - -Lemma hsimpl_cancel_credits_nat_6 : forall (n m : nat) HA HR H1 H2 H3 H4 H5 HT, - (n >= m)%nat -> \$_nat (n - m) \* H1 \* H2 \* H3 \* H4 \* H5 \* HT ==> HA \* HR -> - H1 \* H2 \* H3 \* H4 \* H5 \* \$_nat n \* HT ==> HA \* (\$_nat m \* HR). -Proof using. intros. rewrite (star_comm_assoc H5). apply~ hsimpl_cancel_credits_nat_5. Qed. - -Lemma hsimpl_cancel_credits_nat_7 : forall (n m : nat) HA HR H1 H2 H3 H4 H5 H6 HT, - (n >= m)%nat -> \$_nat (n - m) \* H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* HT ==> HA \* HR -> - H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* \$_nat n \* HT ==> HA \* (\$_nat m \* HR). -Proof using. intros. rewrite (star_comm_assoc H6). apply~ hsimpl_cancel_credits_nat_6. Qed. - -Lemma hsimpl_cancel_credits_nat_8 : forall (n m : nat) HA HR H1 H2 H3 H4 H5 H6 H7 HT, - (n >= m)%nat -> \$_nat (n - m) \* H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* HT ==> HA \* HR -> - H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* \$_nat n \* HT ==> HA \* (\$_nat m \* HR). -Proof using. intros. rewrite (star_comm_assoc H7). apply~ hsimpl_cancel_credits_nat_7. Qed. - -Lemma hsimpl_cancel_credits_nat_9 : forall (n m : nat) HA HR H1 H2 H3 H4 H5 H6 H7 H8 HT, - (n >= m)%nat -> \$_nat (n - m) \* H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* H8 \* HT ==> HA \* HR -> - H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* H8 \* \$_nat n \* HT ==> HA \* (\$_nat m \* HR). -Proof using. intros. rewrite (star_comm_assoc H8). apply~ hsimpl_cancel_credits_nat_8. Qed. - -Lemma hsimpl_cancel_credits_nat_10 : forall (n m : nat) HA HR H1 H2 H3 H4 H5 H6 H7 H8 H9 HT, - (n >= m)%nat -> \$_nat (n - m) \* H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* H8 \* H9 \* HT ==> HA \* HR -> - H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* H8 \* H9 \* \$_nat n \* HT ==> HA \* (\$_nat m \* HR). -Proof using. intros. rewrite (star_comm_assoc H9). apply~ hsimpl_cancel_credits_nat_9. Qed. - - -Lemma hsimpl_cancel_credits_int_1 : forall n m HA HR HT, - n >= m -> m >= 0 -> - \$ (n - m) \* HT ==> HA \* HR -> \$ n \* HT ==> HA \* (\$ m \* HR). -Proof using. - introv L R E. math_rewrite (n = (n - m) + m). - rewrite credits_int_split_eq. rewrite <- star_assoc. - applys~ hsimpl_cancel_2. math. math. -Qed. - -Lemma hsimpl_cancel_credits_int_2 : forall n m HA HR H1 HT, - n >= m -> m >= 0 -> +Lemma hsimpl_cancel_credits_2 : forall (n m : int) HA HR H1 HT, \$ (n - m) \* H1 \* HT ==> HA \* HR -> H1 \* \$ n \* HT ==> HA \* (\$ m \* HR). Proof using. - intros. rewrite (star_comm_assoc H1). apply~ hsimpl_cancel_credits_int_1. + intros. rewrite (star_comm_assoc H1). apply~ hsimpl_cancel_credits_1. Qed. -Lemma hsimpl_cancel_credits_int_3 : forall n m HA HR H1 H2 HT, - n >= m -> m >= 0 -> +Lemma hsimpl_cancel_credits_3 : forall (n m : int) HA HR H1 H2 HT, \$ (n - m) \* H1 \* H2 \* HT ==> HA \* HR -> H1 \* H2 \* \$ n \* HT ==> HA \* (\$ m \* HR). -Proof using. intros. rewrite (star_comm_assoc H2). apply~ hsimpl_cancel_credits_int_2. Qed. +Proof using. intros. rewrite (star_comm_assoc H2). apply~ hsimpl_cancel_credits_2. Qed. -Lemma hsimpl_cancel_credits_int_4 : forall n m HA HR H1 H2 H3 HT, - n >= m -> m >= 0 -> +Lemma hsimpl_cancel_credits_4 : forall (n m : int) HA HR H1 H2 H3 HT, \$ (n - m) \* H1 \* H2 \* H3 \* HT ==> HA \* HR -> H1 \* H2 \* H3 \* \$ n \* HT ==> HA \* (\$ m \* HR). -Proof using. intros. rewrite (star_comm_assoc H3). apply~ hsimpl_cancel_credits_int_3. Qed. +Proof using. intros. rewrite (star_comm_assoc H3). apply~ hsimpl_cancel_credits_3. Qed. -Lemma hsimpl_cancel_credits_int_5 : forall n m HA HR H1 H2 H3 H4 HT, - n >= m -> m >= 0 -> +Lemma hsimpl_cancel_credits_5 : forall (n m : int) HA HR H1 H2 H3 H4 HT, \$ (n - m) \* H1 \* H2 \* H3 \* H4 \* HT ==> HA \* HR -> H1 \* H2 \* H3 \* H4 \* \$ n \* HT ==> HA \* (\$ m \* HR). -Proof using. intros. rewrite (star_comm_assoc H4). apply~ hsimpl_cancel_credits_int_4. Qed. +Proof using. intros. rewrite (star_comm_assoc H4). apply~ hsimpl_cancel_credits_4. Qed. -Lemma hsimpl_cancel_credits_int_6 : forall n m HA HR H1 H2 H3 H4 H5 HT, - n >= m -> m >= 0 -> +Lemma hsimpl_cancel_credits_6 : forall (n m : int) HA HR H1 H2 H3 H4 H5 HT, \$ (n - m) \* H1 \* H2 \* H3 \* H4 \* H5 \* HT ==> HA \* HR -> H1 \* H2 \* H3 \* H4 \* H5 \* \$ n \* HT ==> HA \* (\$ m \* HR). -Proof using. intros. rewrite (star_comm_assoc H5). apply~ hsimpl_cancel_credits_int_5. Qed. +Proof using. intros. rewrite (star_comm_assoc H5). apply~ hsimpl_cancel_credits_5. Qed. -Lemma hsimpl_cancel_credits_int_7 : forall n m HA HR H1 H2 H3 H4 H5 H6 HT, - n >= m -> m >= 0 -> +Lemma hsimpl_cancel_credits_7 : forall (n m : int) HA HR H1 H2 H3 H4 H5 H6 HT, \$ (n - m) \* H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* HT ==> HA \* HR -> H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* \$ n \* HT ==> HA \* (\$ m \* HR). -Proof using. intros. rewrite (star_comm_assoc H6). apply~ hsimpl_cancel_credits_int_6. Qed. +Proof using. intros. rewrite (star_comm_assoc H6). apply~ hsimpl_cancel_credits_6. Qed. -Lemma hsimpl_cancel_credits_int_8 : forall n m HA HR H1 H2 H3 H4 H5 H6 H7 HT, - n >= m -> m >= 0 -> +Lemma hsimpl_cancel_credits_8 : forall (n m : int) HA HR H1 H2 H3 H4 H5 H6 H7 HT, \$ (n - m) \* H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* HT ==> HA \* HR -> H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* \$ n \* HT ==> HA \* (\$ m \* HR). -Proof using. intros. rewrite (star_comm_assoc H7). apply~ hsimpl_cancel_credits_int_7. Qed. +Proof using. intros. rewrite (star_comm_assoc H7). apply~ hsimpl_cancel_credits_7. Qed. -Lemma hsimpl_cancel_credits_int_9 : forall n m HA HR H1 H2 H3 H4 H5 H6 H7 H8 HT, - n >= m -> m >= 0 -> +Lemma hsimpl_cancel_credits_9 : forall (n m : int) HA HR H1 H2 H3 H4 H5 H6 H7 H8 HT, \$ (n - m) \* H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* H8 \* HT ==> HA \* HR -> H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* H8 \* \$ n \* HT ==> HA \* (\$ m \* HR). -Proof using. intros. rewrite (star_comm_assoc H8). apply~ hsimpl_cancel_credits_int_8. Qed. +Proof using. intros. rewrite (star_comm_assoc H8). apply~ hsimpl_cancel_credits_8. Qed. -Lemma hsimpl_cancel_credits_int_10 : forall n m HA HR H1 H2 H3 H4 H5 H6 H7 H8 H9 HT, - n >= m -> m >= 0 -> +Lemma hsimpl_cancel_credits_10 : forall (n m : int) HA HR H1 H2 H3 H4 H5 H6 H7 H8 H9 HT, \$ (n - m) \* H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* H8 \* H9 \* HT ==> HA \* HR -> H1 \* H2 \* H3 \* H4 \* H5 \* H6 \* H7 \* H8 \* H9 \* \$ n \* HT ==> HA \* (\$ m \* HR). -Proof using. intros. rewrite (star_comm_assoc H9). apply~ hsimpl_cancel_credits_int_9. Qed. +Proof using. intros. rewrite (star_comm_assoc H9). apply~ hsimpl_cancel_credits_9. Qed. Lemma hsimpl_cancel_eq_1 : forall H H' HA HR HT, @@ -1874,7 +1865,8 @@ Ltac hsimpl_cleanup tt := try hsimpl_hint_remove tt; try remove_empty_heaps_right tt; try remove_empty_heaps_left tt; - try apply hsimpl_gc. + try apply hsimpl_gc; + try affine. Ltac hsimpl_try_same tt := first @@ -1918,32 +1910,18 @@ Ltac hsimpl_find_data l HL cont := | _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* hdata _ l \* _ => apply hsimpl_cancel_eq_10 end; [ cont tt | ]. -Ltac hsimpl_find_credits_nat HL := - match HL with - | \$_nat _ \* _ => apply hsimpl_cancel_credits_nat_1 - | _ \* \$_nat _ \* _ => apply hsimpl_cancel_credits_nat_2 - | _ \* _ \* \$_nat _ \* _ => apply hsimpl_cancel_credits_nat_3 - | _ \* _ \* _ \* \$_nat _ \* _ => apply hsimpl_cancel_credits_nat_4 - | _ \* _ \* _ \* _ \* \$_nat _ \* _ => apply hsimpl_cancel_credits_nat_5 - | _ \* _ \* _ \* _ \* _ \* \$_nat _ \* _ => apply hsimpl_cancel_credits_nat_6 - | _ \* _ \* _ \* _ \* _ \* _ \* \$_nat _ \* _ => apply hsimpl_cancel_credits_nat_7 - | _ \* _ \* _ \* _ \* _ \* _ \* _ \* \$_nat _ \* _ => apply hsimpl_cancel_credits_nat_8 - | _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* \$_nat _ \* _ => apply hsimpl_cancel_credits_nat_9 - | _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* \$_nat _ \* _ => apply hsimpl_cancel_credits_nat_10 - end. - -Ltac hsimpl_find_credits_int HL := +Ltac hsimpl_find_credits HL := match HL with - | \$ _ \* _ => apply hsimpl_cancel_credits_int_1 - | _ \* \$ _ \* _ => apply hsimpl_cancel_credits_int_2 - | _ \* _ \* \$ _ \* _ => apply hsimpl_cancel_credits_int_3 - | _ \* _ \* _ \* \$ _ \* _ => apply hsimpl_cancel_credits_int_4 - | _ \* _ \* _ \* _ \* \$ _ \* _ => apply hsimpl_cancel_credits_int_5 - | _ \* _ \* _ \* _ \* _ \* \$ _ \* _ => apply hsimpl_cancel_credits_int_6 - | _ \* _ \* _ \* _ \* _ \* _ \* \$ _ \* _ => apply hsimpl_cancel_credits_int_7 - | _ \* _ \* _ \* _ \* _ \* _ \* _ \* \$ _ \* _ => apply hsimpl_cancel_credits_int_8 - | _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* \$ _ \* _ => apply hsimpl_cancel_credits_int_9 - | _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* \$ _ \* _ => apply hsimpl_cancel_credits_int_10 + | \$ _ \* _ => apply hsimpl_cancel_credits_1 + | _ \* \$ _ \* _ => apply hsimpl_cancel_credits_2 + | _ \* _ \* \$ _ \* _ => apply hsimpl_cancel_credits_3 + | _ \* _ \* _ \* \$ _ \* _ => apply hsimpl_cancel_credits_4 + | _ \* _ \* _ \* _ \* \$ _ \* _ => apply hsimpl_cancel_credits_5 + | _ \* _ \* _ \* _ \* _ \* \$ _ \* _ => apply hsimpl_cancel_credits_6 + | _ \* _ \* _ \* _ \* _ \* _ \* \$ _ \* _ => apply hsimpl_cancel_credits_7 + | _ \* _ \* _ \* _ \* _ \* _ \* _ \* \$ _ \* _ => apply hsimpl_cancel_credits_8 + | _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* \$ _ \* _ => apply hsimpl_cancel_credits_9 + | _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* _ \* \$ _ \* _ => apply hsimpl_cancel_credits_10 end. Ltac hsimpl_extract_exists tt := @@ -2031,8 +2009,7 @@ Ltac hsimpl_step process_credits := | ?H => (* should be check_noevar3 on the next line TODO *) first [ is_evar H; fail 1 | idtac ]; hsimpl_find_same H HL (* may fail *) - | \$_nat _ => check_arg_true process_credits; hsimpl_find_credits_nat HL - | \$ _ => check_arg_true process_credits; hsimpl_find_credits_int HL + | \$ _ => check_arg_true process_credits; hsimpl_find_credits HL | hdata _ ?l => hsimpl_find_data l HL ltac:(hsimpl_find_data_post) (* may fail *) | ?x ~> Id _ => check_noevar2 x; apply hsimpl_id (* may fail *) | ?x ~> ?T _ => check_noevar2 x; @@ -2062,8 +2039,7 @@ idtac HN; | ?H => idtac "find"; first [ has_evar H; idtac "has evar"; fail 1 | idtac "has no evar" ]; hsimpl_find_same H HL (* may fail *) - | \$_nat _ => check_arg_true process_credits; idtac "credits_nat"; hsimpl_find_credits_nat HL - | \$ _ => check_arg_true process_credits; idtac "credits_int"; hsimpl_find_credits_int HL + | \$ _ => check_arg_true process_credits; idtac "credits"; hsimpl_find_credits HL | hdata _ ?l => idtac "hdata"; hsimpl_find_data l HL ltac:(hsimpl_find_data_post) (* may fail *) | ?x ~> Id _ => idtac "id"; check_noevar x; apply hsimpl_id (* todo: why is this requiring a fail 2 ? *) | ?x ~> _ _ => idtac "some"; check_noevar2 x; apply hsimpl_id_unify @@ -2173,24 +2149,6 @@ Tactic Notation "chsimpl" "~" := chsimpl; auto_tilde. Tactic Notation "chsimpl" "*" := chsimpl; auto_star. -(********************************************************************) -(* ** Derived lemmas using hsimpl *) - -Section Facts. -Transparent heap_is_credits_int. - -Lemma pay_one_nat : forall H H', - pay_one H H' = (H ==> \$_nat 1%nat \* H'). -Proof using. - intros. unfolds. fequals. - unfold heap_is_credits_int. - asserts_rewrite ((Z.abs_nat 1%Z) = 1%nat). - forwards~: succ_abs_eq_abs_one_plus 0. math. - apply pred_incl_antisym. hsimpl. hsimpl. math. -Qed. - -End Facts. - (********************************************************************) (* ** Other stuff *) @@ -2669,11 +2627,12 @@ Qed. Lemma local_gc_pre_on : forall HG H' B (F:~~B) H Q, is_local F -> + affine HG -> H ==> HG \* H' -> F H' Q -> F H Q. Proof using. - introv L M W. rewrite L. introv Ph. + introv L HA M W. rewrite L. introv Ph. exists H' HG Q. splits. rewrite star_comm. apply~ M. auto. @@ -2699,7 +2658,7 @@ Lemma local_weaken_gc_pre : forall B H' Q' (F:~~B) (H:hprop) Q, Q' ===> Q -> F H Q. Proof using. - intros. apply* (@local_gc_pre_on (\GC) H'). hchange H2. hsimpl. + intros. apply* (@local_gc_pre_on (\GC) H'). affine. hchange H2. hsimpl. applys* local_weaken. Qed. diff --git a/lib/coq/CFLibCredits.v b/lib/coq/CFLibCredits.v index 530638b..2764898 100644 --- a/lib/coq/CFLibCredits.v +++ b/lib/coq/CFLibCredits.v @@ -28,17 +28,14 @@ Implicit Types x y z : int. (********************************************************************) (** Additional lemmas on credits *) -Definition credits_nat_eq := - args_eq_1 heap_is_credits_nat. - (* todo: state as a lemma instead *) - -Lemma credits_nat_zero_eq_prove : forall (n:nat), - n = 0%nat -> \$_nat n = \[]. -Proof. intros. subst. apply credits_nat_zero_eq. Qed. +Lemma credits_eq : forall x y, + x = y -> + \$ x = \$ y. +Proof. apply (args_eq_1 heap_is_credits). Qed. Lemma credits_int_zero_eq_prove : forall (x:int), x = 0 -> \$ x = \[]. -Proof. intros. subst. apply credits_int_zero_eq. Qed. +Proof. intros. subst. apply credits_zero_eq. Qed. diff --git a/lib/coq/CFTactics.v b/lib/coq/CFTactics.v index 7bd5022..1bf8e5b 100644 --- a/lib/coq/CFTactics.v +++ b/lib/coq/CFTactics.v @@ -505,6 +505,7 @@ Tactic Notation "xpull" "as" simple_intropattern(I1) simple_intropattern(I2) Ltac xgc_remove_hprop H := eapply (@local_gc_pre_on H); [ try xlocal + | try affine | hsimpl | xtag_pre_post ]. @@ -557,6 +558,7 @@ Ltac xgc_post_if_not_evar_then cont := Lemma local_gc_pre_all : forall B Q (F:~~B) H, is_local F -> + affine H -> F \[] Q -> F H Q. Proof using. intros. apply* (@local_gc_pre_on H). hsimpl. Qed. @@ -1618,7 +1620,7 @@ Lemma xret_lemma : forall B (v:B) H (Q:B->hprop), local (fun H' Q' => H' ==> Q' v) H Q. Proof using. introv W. eapply (@local_gc_pre_on (\GC)). - auto. hchanges W. apply~ local_erase. hsimpl. + auto. affine. hchanges W. apply~ local_erase. hsimpl. Qed. (* Lemma used by [xret] and [xret_no_gc] @@ -3832,15 +3834,11 @@ Tactic Notation "xname_post" ident(X) := used before a credit split operation, e.g. to replace [$n] with [$a \* $b], when [n = a + b]. - LATER: add demos for this tactic. + LATER: add demos for this tactic. *) Ltac xcredit goal := match goal with - | |- context[\$_nat goal] => - idtac (* no need to rewrite *) - | |- context[\$_nat ?n] => - math_rewrite (n = goal :> nat) | |- context[\$ goal] => idtac (* no need to rewrite *) | |- context[\$ ?n] => @@ -3867,15 +3865,11 @@ Ltac xpay_start tt := Ltac xpay_core tt := xpay_start tt; [ unfold pay_one; hsimpl | ]. -Ltac xpay_nat_core tt := - xpay_start tt; [ rewrite pay_one_nat; hsimpl | ]. - Tactic Notation "xpay" := xpay_core tt. Ltac xpay_on_impl goal := xcredit goal; - first [ rewrite credits_int_split_eq - | rewrite credits_nat_split_eq ]; + first [ rewrite credits_split_eq ]; xpay. Tactic Notation "xpay" constr(goal) := @@ -3913,12 +3907,22 @@ Tactic Notation "xpay_skip" := xpay_fake tt. Ltac xgc_credit_core HP := let H := fresh in let E := fresh in - destruct (credits_nat_le_rest HP) as (H&E); - xchange E; [ chsimpl | xgc H; clear H E ]. + destruct (credits_le_rest HP) as (H&HA&E); + xchange E; [ xgc H; clear H HA E; hclean ]. Tactic Notation "xgc_credit" constr(HP) := xgc_credit_core HP. +Goal forall m n B (F : ~~B) Q, + m <= n -> + is_local F -> + F (\$m) Q -> + F (\$n) Q. +Proof. + introv H L HH. + xgc_credit_core H. + assumption. +Qed. (*--------------------------------------------------------*) (* ** [xskip_credits] *) diff --git a/lib/stdlib/Array_proof.v b/lib/stdlib/Array_proof.v index a373b3e..5a463da 100644 --- a/lib/stdlib/Array_proof.v +++ b/lib/stdlib/Array_proof.v @@ -32,6 +32,10 @@ Parameter Array : forall A, list A -> loc -> hprop. the ownership of single cells, each of which being described using heap_is_single. *) +Parameter Array_affine : forall A t (L: list A), affine (t ~> Array L). + (* TODO: prove this *) +Hint Resolve Array_affine : affine. + (* -------------------------------------------------------------------------- *) (* The length of an array is at most [Sys.max_array_length]. This could be diff --git a/lib/stdlib/Pervasives_proof.v b/lib/stdlib/Pervasives_proof.v index 2ef585b..8f0bd6c 100644 --- a/lib/stdlib/Pervasives_proof.v +++ b/lib/stdlib/Pervasives_proof.v @@ -260,6 +260,10 @@ Qed. Notation "r '~~>' v" := (hdata (Ref v) r) (at level 32, no associativity) : heap_scope. +(* TODO: prove it and/or generalize wrt Heapdata *) +Parameter Ref_affine : forall A r (v: A), affine (r ~~> v). +Hint Resolve Ref_affine : affine. + Lemma ref_spec : forall A (v:A), app ref [v] PRE \[] -- GitLab From 51d922aeedea2b4c745dcd84fc180873c3d90df7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Arma=C3=ABl=20Gu=C3=A9neau?= <armael.gueneau@ens-lyon.fr> Date: Tue, 16 Jan 2018 17:09:51 +0100 Subject: [PATCH 3/6] Use [field] instead of its definition [nat] in type annotations --- lib/coq/CFApp.v | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/lib/coq/CFApp.v b/lib/coq/CFApp.v index 5f85c87..6b05067 100644 --- a/lib/coq/CFApp.v +++ b/lib/coq/CFApp.v @@ -407,9 +407,9 @@ Global Opaque app_def curried. is an association list from fields (natural numbers) to dependent pairs (a value accompanied with its type). *) -Definition record_descr := list (nat * dynamic). +Definition record_descr := list (field * dynamic). -Definition record_repr_one (f:nat) A (v:A) (r:loc) : hprop := +Definition record_repr_one (f:field) A (v:A) (r:loc) : hprop := heap_is_single r f v. Fixpoint record_repr (L:record_descr) (r:loc) : hprop := @@ -445,7 +445,7 @@ Definition app_record_new (L:record_descr) : ~~loc := Axiom record_get : func. -Axiom record_get_spec : forall (r:loc) (f:nat) A (v:A), +Axiom record_get_spec : forall (r:loc) (f:field) A (v:A), app_keep record_get [r f] (r ~> record_repr_one f v) \[= v]. @@ -454,7 +454,7 @@ Axiom record_get_spec : forall (r:loc) (f:nat) A (v:A), Axiom record_set : func. -Axiom record_set_spec : forall (r:loc) (f:nat) A B (v:A) (w:B), +Axiom record_set_spec : forall (r:loc) (f:field) A B (v:A) (w:B), app record_set [r f w] (r ~> record_repr_one f v) (# r ~> record_repr_one f w). @@ -562,7 +562,7 @@ Notation "`{ f1 := x1 ; f2 := x2 ; f3 := x3 ; f4 := x4 ; f5 := x5 ; f6 := x6 ; f (********************************************************************) (* ** Computated derived specifications for [get] and [set] on records *) -Fixpoint record_get_compute_dyn (f:nat) (L:record_descr) : option dynamic := +Fixpoint record_get_compute_dyn (f:field) (L:record_descr) : option dynamic := match L with | nil => None | (f',d')::T' => @@ -571,7 +571,7 @@ Fixpoint record_get_compute_dyn (f:nat) (L:record_descr) : option dynamic := else record_get_compute_dyn f T' end. -Definition record_get_compute_spec (f:nat) (L:record_descr) : option Prop := +Definition record_get_compute_spec (f:field) (L:record_descr) : option Prop := match record_get_compute_dyn f L with | None => None | Some (dyn v) => Some (forall r, @@ -602,7 +602,7 @@ Proof using. Qed. (* todo: could use xapply in this proof *) -Fixpoint record_set_compute_dyn (f:nat) (d:dynamic) (L:record_descr) : option record_descr := +Fixpoint record_set_compute_dyn (f:field) (d:dynamic) (L:record_descr) : option record_descr := match L with | nil => None | (f',d')::T' => @@ -614,7 +614,7 @@ Fixpoint record_set_compute_dyn (f:nat) (d:dynamic) (L:record_descr) : option re end end. -Definition record_set_compute_spec (f:nat) A (w:A) (L:record_descr) : option Prop := +Definition record_set_compute_spec (f:field) A (w:A) (L:record_descr) : option Prop := match record_set_compute_dyn f (dyn w) L with | None => None | Some L' => Some (forall r, -- GitLab From 97978996f5f58a4d922b639f6b99de2ddb35e619 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Arma=C3=ABl=20Gu=C3=A9neau?= <armael.gueneau@ens-lyon.fr> Date: Tue, 16 Jan 2018 17:49:30 +0100 Subject: [PATCH 4/6] Improve the [affine] tactic; add more hints for heap data --- lib/coq/CFApp.v | 18 ++++++++++++++ lib/coq/CFHeaps.v | 46 ++++++++++++++++++++++++++++++++--- lib/stdlib/Array_proof.v | 7 ++++-- lib/stdlib/Pervasives_proof.v | 10 +++++--- 4 files changed, 72 insertions(+), 9 deletions(-) diff --git a/lib/coq/CFApp.v b/lib/coq/CFApp.v index 6b05067..a51e005 100644 --- a/lib/coq/CFApp.v +++ b/lib/coq/CFApp.v @@ -412,12 +412,30 @@ Definition record_descr := list (field * dynamic). Definition record_repr_one (f:field) A (v:A) (r:loc) : hprop := heap_is_single r f v. +Lemma affine_record_repr_one : forall f A (v:A) r, + affine (record_repr_one f v r). +Proof. + intros. unfold record_repr_one. affine. +Qed. + +Hint Transparent field : affine. +Hint Resolve affine_record_repr_one : affine. + Fixpoint record_repr (L:record_descr) (r:loc) : hprop := match L with | nil => \[] | (f, dyn v)::L' => r ~> record_repr_one f v \* r ~> record_repr L' end. +Lemma affine_record_repr : forall L r, + affine (record_repr L r). +Proof. + induction L as [| [? [? ?]] ?]; intros; simpl; affine. +Qed. + +Hint Transparent record_descr : affine. +Hint Resolve affine_record_repr : affine. + (* DEPRECATED Axiom record_repr : record_descr -> loc -> hprop. Definition record_repr_one (f:nat) A (v:A) (r:loc) : hprop := diff --git a/lib/coq/CFHeaps.v b/lib/coq/CFHeaps.v index dbcbb4d..54f3188 100644 --- a/lib/coq/CFHeaps.v +++ b/lib/coq/CFHeaps.v @@ -447,6 +447,9 @@ Lemma heap_affine_credits : forall c, heap_affine (state_empty, c). Proof. auto. Qed. +Lemma heap_affine_single : forall l f A (v:A), + heap_affine (state_single l f v, 0). +Proof. intros. unfold heap_affine. simpl. math. Qed. (** Hints and tactics *) @@ -964,6 +967,8 @@ Notation "'~>' S" := (hdata S) Notation "x '~>' S" := (hdata S x) (at level 33, no associativity) : heap_scope. +Hint Transparent hdata : affine. + (** Specification of pure functions: [pure F P] is equivalent to [F [] (fun x => [P x])] *) @@ -1076,17 +1081,50 @@ Proof. tauto. Qed. -(* affine_hdata? *) +Lemma affine_single : forall l f A (v:A), + affine (heap_is_single l f v). +Proof. + Transparent heap_is_single. + intros. unfold affine, heap_is_single. + intros (m & c). intros (? & ? & ?). subst. + apply heap_affine_single. +Qed. + +Lemma affine_pack : forall A (J : A -> hprop), + (forall x, affine (J x)) -> + affine (heap_is_pack J). +Proof. + Transparent heap_is_pack. + intros. unfold affine, heap_is_pack in *. + intros h [x HJx]. eauto. +Qed. End Affine. Hint Resolve affine_empty affine_star affine_credits affine_empty_st - affine_gc + affine_gc affine_single affine_pack : affine. +(* Split a [affine _] goal, following the base operators of the logic *) +Ltac affine_base := + repeat + match goal with + | |- affine (_ \* _) => apply affine_star + | |- affine \[] => apply affine_empty + | |- affine (\$ _) => apply affine_credits; auto with zarith + | |- affine (\[_]) => apply affine_empty_st + | |- affine \GC => apply affine_gc + | |- affine (heap_is_pack _) => apply affine_pack + end. + +(* After using the rules for the standard operators of the logic with +[affine_base], try proving the remaining subgoals using the [affine] hint base. +*) Ltac affine := - match goal with |- affine _ => eauto with affine zarith end. + match goal with + | |- affine _ => affine_base; typeclasses eauto with affine + end. (********************************************************************) @@ -2536,7 +2574,7 @@ Proof using. rewrite star_assoc. exists~ h1 h2. auto. intros x. hchange (Qle' x). hchange~ (Qle x). - set (H' := \GC) at 1 2. hsimpl. + set (H' := \GC) at 1 2. hsimpl. subst H'. affine. apply~ local_erase. Qed. diff --git a/lib/stdlib/Array_proof.v b/lib/stdlib/Array_proof.v index 5a463da..922b730 100644 --- a/lib/stdlib/Array_proof.v +++ b/lib/stdlib/Array_proof.v @@ -32,9 +32,12 @@ Parameter Array : forall A, list A -> loc -> hprop. the ownership of single cells, each of which being described using heap_is_single. *) -Parameter Array_affine : forall A t (L: list A), affine (t ~> Array L). +Parameter affine_Array : forall A t (L: list A), affine (t ~> Array L). (* TODO: prove this *) -Hint Resolve Array_affine : affine. +Hint Resolve affine_Array : affine. + +(* Expose that [array A] (defined in Array_ml) is defined as [loc]. *) +Hint Transparent array : affine. (* -------------------------------------------------------------------------- *) diff --git a/lib/stdlib/Pervasives_proof.v b/lib/stdlib/Pervasives_proof.v index 8f0bd6c..232fba4 100644 --- a/lib/stdlib/Pervasives_proof.v +++ b/lib/stdlib/Pervasives_proof.v @@ -260,9 +260,13 @@ Qed. Notation "r '~~>' v" := (hdata (Ref v) r) (at level 32, no associativity) : heap_scope. -(* TODO: prove it and/or generalize wrt Heapdata *) -Parameter Ref_affine : forall A r (v: A), affine (r ~~> v). -Hint Resolve Ref_affine : affine. +Lemma affine_Ref : forall A r (v: A), affine (r ~~> v). +Proof. intros. unfold Ref, hdata. affine. Qed. + +Hint Resolve affine_Ref : affine. + +(* Expose that [ref_ A] (defined in Pervasives_ml) is defined as [loc] *) +Hint Transparent ref_ : affine. Lemma ref_spec : forall A (v:A), app ref [v] -- GitLab From 1aa50cba7c6da877bcff4f6383da422095f2f88a Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Arma=C3=ABl=20Gu=C3=A9neau?= <armael.gueneau@ens-lyon.fr> Date: Tue, 16 Jan 2018 17:50:42 +0100 Subject: [PATCH 5/6] Fix demo --- lib/coq/CFHeaps.v | 1 + lib/coq/CFTactics.v | 7 +++---- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/lib/coq/CFHeaps.v b/lib/coq/CFHeaps.v index 54f3188..5aee0fb 100644 --- a/lib/coq/CFHeaps.v +++ b/lib/coq/CFHeaps.v @@ -846,6 +846,7 @@ Proof using. inverts M4. subst*. Qed. +(* Used by xgc_credit *) Lemma credits_le_rest : forall (n m : int), (* todo: move later, inverse hyp *) n <= m -> exists H', affine H' /\ \$ m ==> \$ n \* H'. Proof using. diff --git a/lib/coq/CFTactics.v b/lib/coq/CFTactics.v index 1bf8e5b..a5d6f92 100644 --- a/lib/coq/CFTactics.v +++ b/lib/coq/CFTactics.v @@ -3901,8 +3901,7 @@ Tactic Notation "xpay_skip" := xpay_fake tt. between two credit expressions, e.g. [m <= n]. This inequality is used to change [\$n] to [\$m] in the precondition of the goal. - - LATER: add demos for this tactic. *) +*) Ltac xgc_credit_core HP := let H := fresh in @@ -3913,14 +3912,14 @@ Ltac xgc_credit_core HP := Tactic Notation "xgc_credit" constr(HP) := xgc_credit_core HP. -Goal forall m n B (F : ~~B) Q, +Lemma demo_xgc_credit_core : forall m n B (F : ~~B) Q, m <= n -> is_local F -> F (\$m) Q -> F (\$n) Q. Proof. introv H L HH. - xgc_credit_core H. + xgc_credit H. assumption. Qed. -- GitLab From b82651fb5d13b523bba27f9e0c4e835f78c3448d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Arma=C3=ABl=20Gu=C3=A9neau?= <armael.gueneau@ens-lyon.fr> Date: Tue, 16 Jan 2018 22:50:26 +0100 Subject: [PATCH 6/6] Small fix --- lib/coq/CFHeaps.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/lib/coq/CFHeaps.v b/lib/coq/CFHeaps.v index 5aee0fb..c0707ad 100644 --- a/lib/coq/CFHeaps.v +++ b/lib/coq/CFHeaps.v @@ -1124,7 +1124,7 @@ Ltac affine_base := *) Ltac affine := match goal with - | |- affine _ => affine_base; typeclasses eauto with affine + | |- affine _ => affine_base; try (typeclasses eauto with affine) end. @@ -2575,7 +2575,7 @@ Proof using. rewrite star_assoc. exists~ h1 h2. auto. intros x. hchange (Qle' x). hchange~ (Qle x). - set (H' := \GC) at 1 2. hsimpl. subst H'. affine. + set (H' := \GC) at 1 2. hsimpl; subst H'; affine. apply~ local_erase. Qed. -- GitLab