Commit 3a3ccc8b authored by charguer's avatar charguer

array

parent 134bd8ff
......@@ -762,21 +762,18 @@ Tactic Notation "fmap_red" "*" :=
(* ---------------------------------------------------------------------- *)
(** ** Existence of fresh locations *)
Fixpoint nat_fold A (f:nat->A->A) (k:nat) (z:A) : A :=
Fixpoint fmap_conseq (B:Type) (l:nat) (k:nat) (v:B) : fmap nat B :=
match k with
| O => z
| S k' => f k' (nat_fold f k' z)
| O => fmap_empty
| S k' => (fmap_single l v) \+ (fmap_conseq (S l) k' v)
end.
Definition fmap_conseq B (l:nat) (k:nat) (v:B) : fmap nat B :=
nat_fold (fun i m => (fmap_single (l+i)%nat v) \+ m) k fmap_empty.
Lemma fmap_conseq_zero : forall B (l:nat) (v:B),
fmap_conseq l O v = fmap_empty.
Proof using. auto. Qed.
Lemma fmap_conseq_succ : forall B (l:nat) (k:nat) (v:B),
fmap_conseq l (S k) v = (fmap_single (l+k)%nat v) \+ (fmap_conseq l k v).
fmap_conseq l (S k) v = (fmap_single l v) \+ (fmap_conseq (S l) k v).
Proof using. auto. Qed.
Opaque fmap_conseq.
......@@ -843,24 +840,27 @@ Proof using.
unfold fmap_disjoint, map_disjoint. simpl.
lets (l&F): (loc_fresh_nat_ge (null::L)).
exists l. split.
{ intros l'. induction k. { simple~. }
{ rewrite fmap_conseq_succ. destruct IHk as [E|?].
{ intros l'. gen l. induction k; intros.
{ simple~. }
{ rewrite fmap_conseq_succ.
destruct (IHk (S l)%nat) as [E|?].
{ intros i N. applys F (S i). applys_eq N 2. math. }
{ simpl. unfold map_union. case_if~.
{ right. applys not_not_elim. intros H. applys F k.
constructor. applys~ M. } }
{ right. applys not_not_elim. intros H. applys F 0%nat.
constructor. math_rewrite (l'+0 = l')%nat. applys~ M. } }
{ auto. } } }
{ intro_subst. applys~ F 0%nat. rew_nat. auto. }
Qed.
Lemma fmap_disjoint_single_conseq : forall B l l' k (v:B),
(l' >= l + k)%nat ->
\# (fmap_single l' v) (fmap_conseq l k v).
(l < l')%nat \/ (l >= l'+k)%nat ->
\# (fmap_single l v) (fmap_conseq l' k v).
Proof using.
intros. induction k.
introv N. gen l'. induction k; intros.
{ rewrite~ fmap_conseq_zero. }
{ rewrite fmap_conseq_succ. rew_disjoint. split.
{ applys fmap_disjoint_single_single. math. }
{ applys IHk. math. } }
{ applys fmap_disjoint_single_single. destruct N; math. }
{ applys IHk. destruct N. { left; math. } { right; math. } } }
Qed.
End FmapFresh.
......
......@@ -70,7 +70,7 @@ Hint Extern 1 (measure trm_size _ _) =>
associated with each term construct. *)
Definition cf_val v : formula := fun H Q =>
H ==> Q v.
H ==> Q v \* \Top.
Definition cf_seq (F1 : formula) (F2 : formula) : formula := fun H Q =>
exists H1,
......@@ -195,7 +195,7 @@ Proof using.
rewrite cf_unfold. destruct t; simpl;
applys sound_for_local; intros H Q P.
{ false. }
{ applys~ rule_val. }
{ applys~ rule_val_htop. }
{ false. }
{ destruct P as (Q1&P1&P2). applys rule_if.
{ applys* IH. }
......@@ -414,20 +414,11 @@ Tactic Notation "xcf_depth" constr(depth) :=
(* ---------------------------------------------------------------------- *)
(* ** Tactic [xval] and [xvals] *)
Lemma xval_lemma : forall v H Q,
H ==> Q v \* \Top ->
local (cf_val v) H Q.
Proof using.
intros v H Q M. unfold cf_val.
applys~ local_htop_post (Q \*+ \Top).
applys local_erase. applys M.
Qed.
Tactic Notation "xval_notop" :=
Ltac xval_core tt :=
applys local_erase; unfold cf_val.
Tactic Notation "xval" :=
apply xval_lemma.
xval_core tt.
Tactic Notation "xvals" :=
xval; hsimpl.
......@@ -438,31 +429,50 @@ Tactic Notation "xvals" "*" :=
(* ---------------------------------------------------------------------- *)
(* ** Tactic [xseq] and [xlet] *)
(* ** Tactic [xseq] *)
Ltac xseq_core tt :=
applys local_erase; esplit; split.
Tactic Notation "xseq" :=
xseq_core tt.
(* ---------------------------------------------------------------------- *)
(* ** Tactic [xlet] *)
Ltac xlet_core tt :=
applys local_erase; esplit; split.
Tactic Notation "xlet" :=
applys local_erase; esplit; split.
xlet_core tt.
Tactic Notation "xlet" simple_intropattern(X) :=
Ltac xlet_as_core X :=
applys local_erase; esplit; split; [ | intros X ].
Tactic Notation "xlet" simple_intropattern(X) :=
xlet_as_core X.
(* ---------------------------------------------------------------------- *)
(* ** Tactic [xif] *)
Tactic Notation "xif" :=
Ltac xif_core tt :=
applys local_erase; split.
Tactic Notation "xif" :=
xif_core tt.
(* ---------------------------------------------------------------------- *)
(* ** Tactic [xfail] *)
Tactic Notation "xfail" :=
Ltac xfail_core tt :=
applys local_erase; unfold cf_fail.
Tactic Notation "xfail" :=
xfail_core tt.
(* ---------------------------------------------------------------------- *)
(* * [xapp] and [xapps] and [xapp as] *)
......
......@@ -26,42 +26,92 @@ Implicit Types n : int.
(*
Ltac hcancel_hook H ::=
match H with
| hsingle _ _ => hcancel_try_same tt
| hfield _ _ _ => hcancel_try_same tt
| Alloc _ _ => hcancel_try_same tt
end.
*)
Lemma hcancel_hempty_hstar_evar : forall H,
H ==> \[] \* H.
Proof using. intros. rew_heap~. Qed.
Lemma hcancel_evar_hstar_hempty : forall H,
H ==> H \* \[].
Proof using. intros. rew_heap~. Qed.
Ltac hcancel_cleanup tt ::=
try apply hcancel_stop;
try apply hcancel_stop;
try apply pred_le_refl;
try hcancel_hint_remove tt;
try remove_empty_heaps_right tt;
try remove_empty_heaps_left tt;
try apply hcancel_htop;
try apply hcancel_hempty_hstar_evar;
try apply hcancel_evar_hstar_hempty;
try apply hcancel_htop_hstar_evar;
try apply hcancel_evar_hstar_htop.
(* ********************************************************************** *)
(* * Arrays *)
(*
(* ---------------------------------------------------------------------- *)
(** Representation *)
Fixpoint ArrayAux (L:list val) (l:loc) (f:field) : hprop :=
Fixpoint Array (L:list val) (p:loc) : hprop :=
match L with
| nil => \[]
| x::L' => l`.`f ~~> x \* ArrayAux L' l (f+1)%nat
| x::L' => (p ~~> x) \* (Array L' (S p))
end.
Definition Array (L:list val) (l:loc) : hprop :=
ArrayAux L l 0%nat.
Lemma Array_nil_eq : forall p,
Array nil p = \[].
Proof using. auto. Qed.
Ltac rew_alloc_post_core tt ::=
try simpl_abs; (* TODO: this line will be removed once [abs] computes *)
autorewrite with rew_alloc_post.
Lemma Array_cons_eq : forall p x L,
Array (x::L) p = (p ~~> x) \* Array L (S p).
Proof using. auto. Qed.
(* TODO
Lemma alloc_post_inv_array : forall p k k',
alloc_post p k ==>
Hexists (L : list val), \[length L = k] \* ArrayAux L p k'.
Lemma Array_one_eq : forall p x,
Array (x::nil) p = (p ~~> x).
Proof using. intros. rewrite Array_cons_eq, Array_nil_eq. rew_heap~. Qed.
Lemma Array_concat_eq : forall p L1 L2,
Array (L1++L2) p = Array L1 p \* Array L2 (p + length L1)%nat.
Proof using.
intros. unfold Array. induction k.
{ rew_alloc_post. hsimpl.
Transparent loc.
intros. gen p. induction L1; intros; rew_list.
{ rewrite Array_nil_eq. rew_heap. fequals. unfold loc; math. }
{ do 2 rewrite Array_cons_eq. rewrite IHL1. rew_heap. do 3 fequals.
unfold loc; math. }
Qed.
*)
Lemma Array_last_eq : forall p x L,
Array (L&x) p = Array L p \* ((p + length L)%nat ~~> x).
Proof using. intros. rewrite Array_concat_eq. rewrite~ Array_one_eq. Qed.
Lemma rule_alloc_array_nat : forall k,
triple (prim_alloc (my_Z_of_nat k))
\[]
(fun r => Hexists (p:loc) (L:list val), \[r = val_loc p] \*
\[length L = k] \* Array L p).
Global Opaque Array.
(* ---------------------------------------------------------------------- *)
(** Allocation *)
Lemma Array_of_Alloc : forall k l,
Alloc k l ==>
Hexists (L : list val), \[length L = k] \* Array L l.
Proof using.
intros. xapp. math. intros r. hpull. intros. subst.
hsimpl~.
intros. gen l. induction k; intros.
{ rew_Alloc. hsimpl (@nil val). rew_list~. }
{ rew_Alloc. hpull ;=> v. hchange IHk. hpull ;=> L E.
hsimpl (v::L).
{ rewrite Array_cons_eq. hsimpl~. }
{ rew_list. math. } }
Qed.
Lemma rule_alloc_array : forall n,
......@@ -71,10 +121,12 @@ Lemma rule_alloc_array : forall n,
(fun r => Hexists (p:loc) (L:list val), \[r = val_loc p] \*
\[length L = n :> int] \* Array L p).
Proof using.
introv N. rewrite~ <- (@abs_pos n). xapplys~ rule_alloc_array_nat.
introv N. xapp. math.
intros r. hpull ;=> l E. subst r.
hchange Array_of_Alloc. hpull ;=> L HL.
hsimpl~. rewrite HL. rewrite~ abs_pos.
Qed.
*)
(* ********************************************************************** *)
......@@ -93,7 +145,7 @@ Definition N : var := 8%nat.
Definition P : var := 9%nat.
Definition Q : var := 10%nat.
Definition R : var := 11%nat.
Definition S : var := 12%nat.
(*Definition S : var := 12%nat.*)
Definition T : var := 13%nat.
Definition U : var := 14%nat.
Definition V : var := 15%nat.
......@@ -369,9 +421,7 @@ Proof using.
intros. applys rule_app_fun. reflexivity. simpl.
applys rule_let. { xapplys rule_add_loc. }
intros r. simpl. xpull. intro_subst.
xchange hsingle_of_hfield. xpull ;=> N.
xapply rule_get. hsimpl.
hchanges~ hfield_of_hsingle.
rewrite hfield_eq_fun_hsingle. xapp. hsimpl~.
Qed.
Lemma rule_set_field : forall v' l f v,
......@@ -382,9 +432,7 @@ Proof using.
intros. applys rule_app_fun2. reflexivity. auto. simpl.
applys rule_let. { xapplys rule_add_loc. }
intros r. simpl. xpull. intro_subst.
xchange hsingle_of_hfield. xpull ;=> N.
xapply rule_set. hsimpl.
hchanges~ hfield_of_hsingle.
rewrite hfield_eq_fun_hsingle. xapp. hsimpl~.
Qed.
Implicit Arguments rule_set_field [].
......@@ -518,8 +566,11 @@ Lemma rule_alloc_cell :
Proof using.
xapply rule_alloc. { math. } { hsimpl. }
{ intros r. hpull. intros l E. subst.
rew_alloc_post. hpull ;=> v1 v2.
unfold MCell. unfold hd, tl. hsimpl~. }
simpl_abs. rew_Alloc. hpull ;=> v1 v2.
unfold MCell. rewrite hfield_eq_fun_hsingle.
unfold hd, tl. hsimpl~ l v1 v2.
math_rewrite (l + 1 = S l)%nat.
math_rewrite (l+0 = l)%nat. hsimpl. }
Qed.
Lemma rule_new_cell : forall v q,
......@@ -890,7 +941,9 @@ Lemma rule_create :
Proof using.
xcf. unfold MQueue.
xapp rule_alloc_cell as r. intros p v1 v2. intro_subst.
xapp~. rewrite MListSeg_nil_eq. hsimpl~.
xapp~. intros r. hpull. intros. subst. hsimpl~.
{ rewrite MListSeg_nil_eq. hsimpl~. }
(* todo: simplify ? *)
Qed.
......
(*
Definition hfield (l:loc) (f:field) (v:val) : hprop :=
(l+f)%nat ~~> v \* \[l <> null].
Notation "l `.` f '~~>' v" := (hfield l f v)
(at level 32, f at level 0, no associativity,
format "l `.` f '~~>' v") : heap_scope.
Lemma hstar_hfield_same_loc_disjoint : forall l f v1 v2,
(l`.`f~~> v1) \* (l`.`f ~~> v2) ==> \[False].
Proof using.
intros. unfold hfield.
hchanges hstar_hsingle_same_loc_disjoint.
Qed.
Lemma hfield_not_null : forall l f v,
f = 0%nat ->
(l`.`f ~~> v) ==> (l`.`f ~~> v) \* \[l <> null].
Proof using.
introv E. subst. unfold hfield. hsimpl~.
Qed.
Implicit Arguments hfield_not_null [].
Lemma hfield_eq_hsingle : forall l f v,
l <> null ->
(l`.`f ~~> v) = ((l+f)%nat ~~> v).
Proof using.
Transparent hfield.
introv N. unfold hfield.
applys himpl_antisym; hsimpl~.
Qed.
(* ---------------------------------------------------------------------- *)
(* ** Configuration of [hsimpl] *)
(* ** Configure [hsimpl] to make it aware of [hsingle] *)
Ltac hcancel_hook H ::=
match H with
| hsingle _ _ => hcancel_try_same tt
| hfield _ _ _ => hcancel_try_same tt
end.
(* ---------------------------------------------------------------------- *)
(* ** Conversion between [hfield] and [hsingle] *)
Lemma hsingle_of_hfield : forall l f v,
(l`.`f ~~> v) ==> ((l+f)%nat ~~> v) \* \[l <> null].
Proof using. intros. unfold hfield. hsimpl~. Qed.
Lemma hfield_of_hsingle : forall l f v,
l <> null ->
((l+f)%nat ~~> v) ==> (l`.`f ~~> v).
Proof using. intros. unfold hfield. hsimpl~. Qed.
Lemma xval_lemma : forall v H Q,
H ==> Q v \* \Top ->
local (cf_val v) H Q.
Proof using.
intros v H Q M. unfold cf_val.
applys~ local_htop_post (Q \*+ \Top).
applys local_erase. applys M.
Qed.
Tactic Notation "xval_notop" :=
applys local_erase; unfold cf_val.
*)
(* Capturing bound names
Fixpoint nat_fold A (f:nat->A->A) (k:nat) (z:A) : A :=
match k with
| O => z
| S k' => f k' (nat_fold f k' z)
end.
(** Recovering variable names in ltac *)
......
......@@ -142,6 +142,13 @@ Section Properties.
Hint Resolve hempty_intro.
Lemma hstar_intro : forall H1 H2 h1 h2,
H1 h1 ->
H2 h2 ->
\# h1 h2 ->
(H1 \* H2) (h1 \+ h2).
Proof using. intros. exists~ h1 h2. Qed.
Lemma hstar_hempty_l : forall H,
hempty \* H = H.
Proof using.
......@@ -258,7 +265,7 @@ Global Opaque hsingle.
(** l `.` f ~> v *)
Definition hfield (l:loc) (f:field) (v:val) : hprop :=
(l+f)%nat ~~> v \* \[l <> null].
(l+f)%nat ~~> v.
Notation "l `.` f '~~>' v" := (hfield l f v)
(at level 32, f at level 0, no associativity,
......@@ -266,20 +273,35 @@ Notation "l `.` f '~~>' v" := (hfield l f v)
Lemma hstar_hfield_same_loc_disjoint : forall l f v1 v2,
(l`.`f~~> v1) \* (l`.`f ~~> v2) ==> \[False].
Proof using.
intros. unfold hfield.
hchanges hstar_hsingle_same_loc_disjoint.
Qed.
Proof using. intros. applys hstar_hsingle_same_loc_disjoint. Qed.
Lemma hfield_not_null : forall l f v,
f = 0%nat ->
(l`.`f ~~> v) ==> (l`.`f ~~> v) \* \[l <> null].
Proof using.
introv E. subst. unfold hfield. hsimpl~.
introv E. subst. unfold hfield.
math_rewrite ((l + 0)%nat = l).
applys hsingle_not_null.
Qed.
Implicit Arguments hfield_not_null [].
Lemma hfield_eq_hsingle : forall l f v,
(l`.`f ~~> v) = ((l+f)%nat ~~> v).
Proof using. intros. auto. Qed.
Lemma hfield_eq_fun_hsingle :
hfield = (fun l f v => ((l+f)%nat ~~> v)).
Proof using. intros. auto. Qed.
(* needed? *)
Lemma hsingle_eq_fun_hfield :
hsingle = (fun l v => (l`.`(0%nat) ~~> v)).
Proof using.
intros. applys func_ext_2. intros. unfold hfield. fequals.
Transparent loc. unfold loc. math.
Qed.
(* ---------------------------------------------------------------------- *)
(* ** Configuration of [hsimpl] *)
......@@ -293,50 +315,41 @@ Ltac hcancel_hook H ::=
end.
(* ---------------------------------------------------------------------- *)
(* ** Conversion between [hfield] and [hsingle] *)
Lemma hsingle_of_hfield : forall l f v,
(l`.`f ~~> v) ==> ((l+f)%nat ~~> v) \* \[l <> null].
Proof using. intros. unfold hfield. hsimpl~. Qed.
Lemma hfield_of_hsingle : forall l f v,
l <> null ->
((l+f)%nat ~~> v) ==> (l`.`f ~~> v).
Proof using. intros. unfold hfield. hsimpl~. Qed.
Global Opaque hfield.
(* ---------------------------------------------------------------------- *)
(* ** Auxiliary definitions for [rule_alloc] *)
Definition alloc_post (l:loc) (k:nat) :=
nat_fold (fun i H => (Hexists v, l`.`i ~~> v) \* H) k \[].
Fixpoint Alloc (k:nat) (l:loc) :=
match k with
| O => \[]
| S k' => (Hexists v, l ~~> v) \* (Alloc k' (S l)%nat)
end.
Lemma alloc_post_zero : forall l,
alloc_post l O = \[].
Lemma Alloc_zero_eq : forall l,
Alloc O l = \[].
Proof using. auto. Qed.
Lemma alloc_post_succ : forall l k,
alloc_post l (S k) = (Hexists v, l`.`k ~~> v) \* alloc_post l k.
Lemma Alloc_succ_eq : forall l k,
Alloc (S k) l = (Hexists v, l ~~> v) \* Alloc k (S l)%nat.
Proof using. auto. Qed.
Global Opaque alloc_post.
Global Opaque Alloc.
Hint Rewrite alloc_post_succ alloc_post_zero : rew_alloc_post.
Hint Rewrite Alloc_zero_eq Alloc_succ_eq : rew_Alloc.
Lemma alloc_post_fmap_conseq : forall l k v,
Tactic Notation "rew_Alloc" :=
autorewrite with rew_Alloc.
Lemma Alloc_fmap_conseq : forall l k v,
l <> null ->
alloc_post l k (fmap_conseq l k v).
(Alloc k l) (fmap_conseq l k v).
Proof using.
Transparent loc null.
introv N. induction k; simpl.
{ rewrite fmap_conseq_zero, alloc_post_zero. applys~ hempty_intro. }
{ rewrite fmap_conseq_succ, alloc_post_succ.
exists (fmap_single (l + k)%nat v) (fmap_conseq l k v). splits~.
{ applys hexists_intro. applys~ hfield_of_hsingle. split~.
unfolds loc, null. math. }
introv N. gen l. induction k; intros; rew_Alloc.
{ rewrite fmap_conseq_zero. applys~ hempty_intro. }
{ rewrite fmap_conseq_succ. applys hstar_intro.
{ applys hexists_intro. split~. }
{ applys IHk. unfolds loc, null. math. }
{ applys~ fmap_disjoint_single_conseq. } }
Qed.
......@@ -350,14 +363,6 @@ Ltac simpl_abs := (* TODO: will be removed once [abs] computes *)
| |- context [ abs 3 ] => change (abs 3) with 3%nat
end.
Ltac rew_alloc_post_core tt :=
simpl_abs; (* TODO: this line will be removed once [abs] computes *)
autorewrite with rew_alloc_post.
Tactic Notation "rew_alloc_post" :=
rew_alloc_post_core tt.
(* ********************************************************************** *)
(* * Reasoning Rules *)
......@@ -682,7 +687,7 @@ Lemma rule_alloc : forall n,
n >= 0 ->
triple (prim_alloc n)
\[]
(fun r => Hexists l, \[r = val_loc l] \* alloc_post l (abs n)).
(fun r => Hexists l, \[r = val_loc l] \* Alloc (abs n) l).
Proof using. (* Note: [abs n] currently does not compute in Coq. *)
introv N Hh.
forwards~ (l&Dl&Nl): (fmap_conseq_fresh null h (abs n) val_unit).
......@@ -691,12 +696,13 @@ Proof using. (* Note: [abs n] currently does not compute in Coq. *)
{ applys (red_alloc (abs n)); eauto.
rewrite~ abs_pos. }
{ exists h1' h. split.
{ exists l. applys~ himpl_hprop_r. applys~ alloc_post_fmap_conseq. }
{ exists l. applys~ himpl_hprop_r. applys~ Alloc_fmap_conseq. }
{ splits~. hhsimpl~. } }
Qed.
End RulesStateOps.
(* ---------------------------------------------------------------------- *)
(** Other primitive functions *)
......@@ -796,7 +802,20 @@ Qed.
(* ---------------------------------------------------------------------- *)
(* ** Combination of frame and consequence *)
(* ** Practical additional rules *)
(** Combination of val and garbage *)
Lemma rule_val_htop : forall v H Q,
H ==> Q v \* \Top ->
triple (trm_val v) H Q.
Proof using.
introv M. applys local_htop_pre M.
{ applys is_local_triple. }
{ applys~ rule_val. }
Qed.
(** Combination of frame and consequence *)
Lemma rule_frame' : forall H2 H1 Q1 t H Q,
H ==> H1 \* H2 ->
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment