Module HeapF
From SLF Require Export LibString LibCore.
From SLF Require Export LibSepTLCbuffer.
From SLF Require LibSepSimpl.
From Staged Require Import LibFmap.
Module Type Params.
Parameter value :
Type.
End Params.
Module HeapSetup (
V :
Params).
Import V.
Local Notation val :=
V.value.
Set Implicit Arguments.
Definition loc :
Type :=
nat.
Definition null :
loc := 0%
nat.
Definition heap :
Type :=
fmap loc val.
Notation "h1 \u h2" := (
Fmap.union h1 h2)
(
at level 37,
right associativity).
Heap Predicates
We next define heap predicates and establish their properties. All this
material is wrapped in a module, allowing us to instantiate the functor from
chapter LibSepSimpl that defines the tactic xsimpl.
Module SepSimplArgs.
Hprop and Entailment
Declare Scope hprop_scope.
Open Scope hprop_scope.
The type of heap predicates is named hprop.
Definition hprop :=
heap ->
Prop.
Implicit types for meta-variables.
Implicit Types P :
Prop.
Implicit Types H :
hprop.
Implicit Types Q :
val->
hprop.
Entailment for heap predicates, written H1 ==> H2. This entailment
is linear.
Definition himpl (
H1 H2:
hprop) :
Prop :=
forall h,
H1 h ->
H2 h.
Notation "H1 ==> H2" := (
himpl H1 H2) (
at level 55) :
hprop_scope.
Entailment between postconditions, written Q1 ===> Q2.
Definition qimpl A (
Q1 Q2:
A->
hprop) :
Prop :=
forall (
v:
A),
Q1 v ==>
Q2 v.
Notation "Q1 ===> Q2" := (
qimpl Q1 Q2) (
at level 55) :
hprop_scope.
Definition of Heap Predicates
The core heap predicates are defined next, together with the
associated notation:
- \[] denotes the empty heap predicate
- \[P] denotes a pure fact
- \Top denotes the true heap predicate (affine)
- p ~~> v denotes a singleton heap
- H1 \* H2 denotes the separating conjunction
- Q1 \*+ H2 denotes the separating conjunction extending a postcondition
- \exists x, H denotes an existential quantifier
- \forall x, H denotes a universal quantifier
- H1 \-* H2 denotes a magic wand between heap predicates
- Q1 \--* Q2 denotes a magic wand between postconditions.
Definition hempty :
hprop :=
fun h => (
h =
Fmap.empty).
Definition hsingle (
p:
loc) (
v:
val) :
hprop :=
fun h => (
h =
Fmap.single p v).
Definition hstar (
H1 H2 :
hprop) :
hprop :=
fun h =>
exists h1 h2,
H1 h1
/\
H2 h2
/\
Fmap.disjoint h1 h2
/\
h =
Fmap.union h1 h2.
Definition hexists A (
J:
A->
hprop) :
hprop :=
fun h =>
exists x,
J x h.
Definition hforall (
A :
Type) (
J :
A ->
hprop) :
hprop :=
fun h =>
forall x,
J x h.
Notation "\[]" := (
hempty)
(
at level 0) :
hprop_scope.
Notation "p '~~>' v" := (
hsingle p v) (
at level 32) :
hprop_scope.
Notation "H1 '\*' H2" := (
hstar H1 H2)
(
at level 41,
right associativity) :
hprop_scope.
Notation "'\exists' x1 .. xn , H" :=
(
hexists (
fun x1 => .. (
hexists (
fun xn =>
H)) ..))
(
at level 39,
x1 binder,
H at level 50,
right associativity,
format "'[' '\exists' '/ ' x1 .. xn , '/ ' H ']'") :
hprop_scope.
Notation "'\forall' x1 .. xn , H" :=
(
hforall (
fun x1 => .. (
hforall (
fun xn =>
H)) ..))
(
at level 39,
x1 binder,
H at level 50,
right associativity,
format "'[' '\forall' '/ ' x1 .. xn , '/ ' H ']'") :
hprop_scope.
The remaining operators are defined in terms of the preivous above,
rather than directly as functions over heaps. Doing so reduces the
amount of proofs, by allowing to better leverage the tactic xsimpl.
Definition hpure (
P:
Prop) :
hprop :=
\
exists (
p:
P), \[].
Definition htop :
hprop :=
\
exists (
H:
hprop),
H.
Definition hwand (
H1 H2 :
hprop) :
hprop :=
\
exists H0,
H0 \*
hpure ((
H1 \*
H0) ==>
H2).
Definition qwand A (
Q1 Q2:
A->
hprop) :
hprop :=
\
forall x,
hwand (
Q1 x) (
Q2 x).
Notation "\[ P ]" := (
hpure P)
(
at level 0,
format "\[ P ]") :
hprop_scope.
Notation "\Top" := (
htop) :
hprop_scope.
Notation "Q \*+ H" := (
fun x =>
hstar (
Q x)
H)
(
at level 40) :
hprop_scope.
Notation "H1 \-* H2" := (
hwand H1 H2)
(
at level 43,
right associativity) :
hprop_scope.
Notation "Q1 \--* Q2" := (
qwand Q1 Q2)
(
at level 43) :
hprop_scope.
Basic Properties of Separation Logic Operators
Tactic for Automation
We set up auto to process goals of the form h1 = h2 by calling
fmap_eq, which proves equality modulo associativity and commutativity.
#[
global]
Hint Extern 1 (_ = _ :>
heap) =>
fmap_eq.
We also set up auto to process goals of the form Fmap.disjoint h1 h2
by calling the tactic fmap_disjoint, which essentially normalizes all
disjointness goals and hypotheses, split all conjunctions, and invokes
proof search with a base of hints specified in LibSepFmap.v.
Import Fmap.DisjointHints.
Tactic Notation "fmap_disjoint_pre" :=
subst;
rew_disjoint;
jauto_set.
#[
global]
Hint Extern 1 (
Fmap.disjoint _ _) =>
fmap_disjoint_pre.
Properties of himpl and qimpl
Lemma himpl_refl :
forall H,
H ==>
H.
Proof using.
introv M.
auto. Qed.
#[global] Hint Resolve himpl_refl.
Lemma himpl_trans : forall H2 H1 H3,
(H1 ==> H2) ->
(H2 ==> H3) ->
(H1 ==> H3).
Proof using. introv M1 M2. unfolds* himpl. Qed.
Lemma himpl_trans_r : forall H2 H1 H3,
H2 ==> H3 ->
H1 ==> H2 ->
H1 ==> H3.
Proof using. introv M1 M2. applys* himpl_trans M2 M1. Qed.
Lemma himpl_antisym : forall H1 H2,
(H1 ==> H2) ->
(H2 ==> H1) ->
(H1 = H2).
Proof using. introv M1 M2. applys pred_ext_1. intros h. iff*. Qed.
Lemma hprop_op_comm : forall (op:hprop->hprop->hprop),
(forall H1 H2, op H1 H2 ==> op H2 H1) ->
(forall H1 H2, op H1 H2 = op H2 H1).
Proof using. introv M. intros. applys himpl_antisym; applys M. Qed.
Lemma qimpl_refl : forall A (Q:A->hprop),
Q ===> Q.
Proof using. intros. unfolds*. Qed.
#[global] Hint Resolve qimpl_refl.
Properties of hempty
Lemma hempty_intro :
\[] Fmap.empty.
Proof using. unfolds*. Qed.
Lemma hempty_inv : forall h,
\[] h ->
h = Fmap.empty.
Proof using. auto. Qed.
Properties of hstar
Lemma hstar_intro : forall H1 H2 h1 h2,
H1 h1 ->
H2 h2 ->
Fmap.disjoint h1 h2 ->
(H1 \* H2) (Fmap.union h1 h2).
Proof using. intros. exists~ h1 h2. Qed.
Lemma hstar_inv : forall H1 H2 h,
(H1 \* H2) h ->
exists h1 h2, H1 h1 /\ H2 h2 /\ Fmap.disjoint h1 h2 /\ h = Fmap.union h1 h2.
Proof using. introv M. applys M. Qed.
Lemma hstar_comm : forall H1 H2,
H1 \* H2 = H2 \* H1.
Proof using.
applys hprop_op_comm. unfold hprop, hstar. intros H1 H2.
intros h (h1&h2&M1&M2&D&U). rewrite~ Fmap.union_comm_of_disjoint in U.
exists* h2 h1.
Qed.
Lemma hstar_assoc : forall H1 H2 H3,
(H1 \* H2) \* H3 = H1 \* (H2 \* H3).
Proof using.
intros H1 H2 H3. applys himpl_antisym; intros h.
{ intros (h'&h3&(h1&h2&M3&M4&D'&U')&M2&D&U). subst h'.
exists h1 (h2 \+ h3). splits~. { applys* hstar_intro. } }
{ intros (h1&h'&M1&(h2&h3&M3&M4&D'&U')&D&U). subst h'.
exists (h1 \+ h2) h3. splits~. { applys* hstar_intro. } }
Qed.
Lemma hstar_hempty_l : forall H,
\[] \* H = H.
Proof using.
intros. applys himpl_antisym; intros h.
{ intros (h1&h2&M1&M2&D&U). forwards E: hempty_inv M1. subst.
rewrite~ Fmap.union_empty_l. }
{ intros M. exists (Fmap.empty:heap) h. splits~. { applys hempty_intro. } }
Qed.
Lemma hstar_hempty_r : forall H,
H \* \[] = H.
Proof using.
applys neutral_r_of_comm_neutral_l. applys~ hstar_comm. applys~ hstar_hempty_l.
Qed.
Lemma hstar_hexists : forall A (J:A->hprop) H,
(hexists J) \* H = hexists (fun x => (J x) \* H).
Proof using.
intros. applys himpl_antisym; intros h.
{ intros (h1&h2&(x&M1)&M2&D&U). exists~ x h1 h2. }
{ intros (x&(h1&h2&M1&M2&D&U)). exists h1 h2. splits~. { exists~ x. } }
Qed.
Lemma hstar_hforall : forall H A (J:A->hprop),
(hforall J) \* H ==> hforall (J \*+ H).
Proof using.
intros. intros h M. destruct M as (h1&h2&M1&M2&D&U). intros x. exists~ h1 h2.
Qed.
Lemma himpl_frame_l : forall H2 H1 H1',
H1 ==> H1' ->
(H1 \* H2) ==> (H1' \* H2).
Proof using. introv W (h1&h2&?). exists* h1 h2. Qed.
Lemma himpl_frame_r : forall H1 H2 H2',
H2 ==> H2' ->
(H1 \* H2) ==> (H1 \* H2').
Proof using.
introv M. do 2 rewrite (@hstar_comm H1). applys~ himpl_frame_l.
Qed.
Lemma himpl_frame_lr : forall H1 H1' H2 H2',
H1 ==> H1' ->
H2 ==> H2' ->
(H1 \* H2) ==> (H1' \* H2').
Proof using.
introv M1 M2. applys himpl_trans. applys~ himpl_frame_l M1. applys~ himpl_frame_r.
Qed.
Lemma himpl_hstar_trans_l : forall H1 H2 H3 H4,
H1 ==> H2 ->
H2 \* H3 ==> H4 ->
H1 \* H3 ==> H4.
Proof using.
introv M1 M2. applys himpl_trans_r M2. applys himpl_frame_l M1.
Qed.
Lemma himpl_hstar_trans_r : forall H1 H2 H3 H4,
H1 ==> H2 ->
H3 \* H2 ==> H4 ->
H3 \* H1 ==> H4.
Proof using.
introv M1 M2. applys himpl_trans_r M2. applys himpl_frame_r M1.
Qed.
Properties of hpure
Lemma hpure_intro : forall P,
P ->
\[P] Fmap.empty.
Proof using. introv M. exists M. unfolds*. Qed.
Lemma hpure_inv : forall P h,
\[P] h ->
P /\ h = Fmap.empty.
Proof using. introv (p&M). split~. Qed.
Lemma hstar_hpure_l : forall P H h,
(\[P] \* H) h = (P /\ H h).
Proof using.
intros. apply prop_ext. unfold hpure.
rewrite hstar_hexists. rewrite* hstar_hempty_l.
iff (p&M) (p&M). { split~. } { exists~ p. }
Qed.
Lemma hstar_hpure_r : forall P H h,
(H \* \[P]) h = (H h /\ P).
Proof using.
intros. rewrite hstar_comm. rewrite hstar_hpure_l. apply* prop_ext.
Qed.
Lemma himpl_hstar_hpure_r : forall P H H',
P ->
(H ==> H') ->
H ==> (\[P] \* H').
Proof using. introv HP W. intros h K. rewrite* hstar_hpure_l. Qed.
Lemma hpure_inv_hempty : forall P h,
\[P] h ->
P /\ \[] h.
Proof using.
introv M. rewrite <- hstar_hpure_l. rewrite~ hstar_hempty_r.
Qed.
Lemma hpure_intro_hempty : forall P h,
\[] h ->
P ->
\[P] h.
Proof using.
introv M N. rewrite <- (hstar_hempty_l \[P]). rewrite~ hstar_hpure_r.
Qed.
Lemma himpl_hempty_hpure : forall P,
P ->
\[] ==> \[P].
Proof using. introv HP. intros h Hh. applys* hpure_intro_hempty. Qed.
Lemma himpl_hstar_hpure_l : forall P H H',
(P -> H ==> H') ->
(\[P] \* H) ==> H'.
Proof using.
introv W Hh. rewrite hstar_hpure_l in Hh. applys* W.
Qed.
Lemma hempty_eq_hpure_true :
\[] = \[True].
Proof using.
applys himpl_antisym; intros h M.
{ applys* hpure_intro_hempty. }
{ forwards*: hpure_inv_hempty M. }
Qed.
Lemma hfalse_hstar_any : forall H,
\[False] \* H = \[False].
Proof using.
intros. applys himpl_antisym; intros h; rewrite hstar_hpure_l; intros M.
{ false*. } { lets: hpure_inv_hempty M. false*. }
Qed.
Properties of hexists
Lemma hexists_intro : forall A (x:A) (J:A->hprop) h,
J x h ->
(hexists J) h.
Proof using. intros. exists~ x. Qed.
Lemma hexists_inv : forall A (J:A->hprop) h,
(hexists J) h ->
exists x, J x h.
Proof using. intros. destruct H as [x H]. exists~ x. Qed.
Lemma himpl_hexists_l : forall A H (J:A->hprop),
(forall x, J x ==> H) ->
(hexists J) ==> H.
Proof using. introv W. intros h (x&Hh). applys* W. Qed.
Lemma himpl_hexists_r : forall A (x:A) H J,
(H ==> J x) ->
H ==> (hexists J).
Proof using. introv W. intros h. exists x. apply~ W. Qed.
Lemma himpl_hexists : forall A (J1 J2:A->hprop),
J1 ===> J2 ->
hexists J1 ==> hexists J2.
Proof using.
introv W. applys himpl_hexists_l. intros x. applys himpl_hexists_r W.
Qed.
Properties of hforall
Lemma hforall_intro : forall A (J:A->hprop) h,
(forall x, J x h) ->
(hforall J) h.
Proof using. introv M. applys* M. Qed.
Lemma hforall_inv : forall A (J:A->hprop) h,
(hforall J) h ->
forall x, J x h.
Proof using. introv M. applys* M. Qed.
Lemma himpl_hforall_r : forall A (J:A->hprop) H,
(forall x, H ==> J x) ->
H ==> (hforall J).
Proof using. introv M. intros h Hh x. apply~ M. Qed.
Lemma himpl_hforall_l : forall A x (J:A->hprop) H,
(J x ==> H) ->
(hforall J) ==> H.
Proof using. introv M. intros h Hh. apply~ M. Qed.
Lemma hforall_specialize : forall A (x:A) (J:A->hprop),
(hforall J) ==> (J x).
Proof using. intros. applys* himpl_hforall_l x. Qed.
Lemma himpl_hforall : forall A (J1 J2:A->hprop),
J1 ===> J2 ->
hforall J1 ==> hforall J2.
Proof using.
introv W. applys himpl_hforall_r. intros x. applys himpl_hforall_l W.
Qed.
Properties of hwand
Lemma hwand_equiv : forall H0 H1 H2,
(H0 ==> H1 \-* H2) <-> (H1 \* H0 ==> H2).
Proof using.
unfold hwand. iff M.
{ rewrite hstar_comm. applys himpl_hstar_trans_l (rm M).
rewrite hstar_hexists. applys himpl_hexists_l. intros H.
rewrite (hstar_comm H). rewrite hstar_assoc.
rewrite (hstar_comm H H1). applys~ himpl_hstar_hpure_l. }
{ applys himpl_hexists_r H0.
rewrite <- (hstar_hempty_r H0) at 1.
applys himpl_frame_r. applys himpl_hempty_hpure M. }
Qed.
Lemma himpl_hwand_r : forall H1 H2 H3,
H2 \* H1 ==> H3 ->
H1 ==> (H2 \-* H3).
Proof using. introv M. rewrite~ hwand_equiv. Qed.
Lemma himpl_hwand_r_inv : forall H1 H2 H3,
H1 ==> (H2 \-* H3) ->
H2 \* H1 ==> H3.
Proof using. introv M. rewrite~ <- hwand_equiv. Qed.
Lemma hwand_cancel : forall H1 H2,
H1 \* (H1 \-* H2) ==> H2.
Proof using. intros. applys himpl_hwand_r_inv. applys himpl_refl. Qed.
Arguments hwand_cancel : clear implicits.
Lemma himpl_hempty_hwand_same : forall H,
\[] ==> (H \-* H).
Proof using. intros. apply himpl_hwand_r. rewrite~ hstar_hempty_r. Qed.
Lemma hwand_hempty_l : forall H,
(\[] \-* H) = H.
Proof using.
intros. applys himpl_antisym.
{ rewrite <- hstar_hempty_l at 1. applys hwand_cancel. }
{ rewrite hwand_equiv. rewrite~ hstar_hempty_l. }
Qed.
Lemma hwand_hpure_l : forall P H,
P ->
(\[P] \-* H) = H.
Proof using.
introv HP. applys himpl_antisym.
{ lets K: hwand_cancel \[P] H. applys himpl_trans_r K.
applys* himpl_hstar_hpure_r. }
{ rewrite hwand_equiv. applys* himpl_hstar_hpure_l. }
Qed.
Lemma hwand_curry : forall H1 H2 H3,
(H1 \* H2) \-* H3 ==> H1 \-* (H2 \-* H3).
Proof using.
intros. apply himpl_hwand_r. apply himpl_hwand_r.
rewrite <- hstar_assoc. rewrite (hstar_comm H1 H2).
applys hwand_cancel.
Qed.
Lemma hwand_uncurry : forall H1 H2 H3,
H1 \-* (H2 \-* H3) ==> (H1 \* H2) \-* H3.
Proof using.
intros. rewrite hwand_equiv. rewrite (hstar_comm H1 H2).
rewrite hstar_assoc. applys himpl_hstar_trans_r.
{ applys hwand_cancel. } { applys hwand_cancel. }
Qed.
Lemma hwand_curry_eq : forall H1 H2 H3,
(H1 \* H2) \-* H3 = H1 \-* (H2 \-* H3).
Proof using.
intros. applys himpl_antisym.
{ applys hwand_curry. }
{ applys hwand_uncurry. }
Qed.
Lemma hwand_inv : forall h1 h2 H1 H2,
(H1 \-* H2) h2 ->
H1 h1 ->
Fmap.disjoint h1 h2 ->
H2 (h1 \u h2).
Proof using.
introv M2 M1 D. unfolds hwand. lets (H0&M3): hexists_inv M2.
lets (h0&h3&P1&P3&D'&U): hstar_inv M3. lets (P4&E3): hpure_inv P3.
subst h2 h3. rewrite union_empty_r in *. applys P4. applys* hstar_intro.
Qed.
Properties of qwand
Lemma qwand_equiv : forall H A (Q1 Q2:A->hprop),
H ==> (Q1 \--* Q2) <-> (Q1 \*+ H) ===> Q2.
Proof using.
unfold qwand. iff M.
{ intros x. rewrite hstar_comm. applys himpl_hstar_trans_l (rm M).
applys himpl_trans. applys hstar_hforall. simpl.
applys himpl_hforall_l x. rewrite hstar_comm. applys hwand_cancel. }
{ applys himpl_hforall_r. intros x. rewrite* hwand_equiv. }
Qed.
Lemma qwand_cancel : forall A (Q1 Q2:A->hprop),
Q1 \*+ (Q1 \--* Q2) ===> Q2.
Proof using. intros. rewrite <- qwand_equiv. applys qimpl_refl. Qed.
Lemma himpl_qwand_r : forall A (Q1 Q2:A->hprop) H,
Q1 \*+ H ===> Q2 ->
H ==> (Q1 \--* Q2).
Proof using. introv M. rewrite~ qwand_equiv. Qed.
Arguments himpl_qwand_r [A].
Lemma qwand_specialize : forall A (x:A) (Q1 Q2:A->hprop),
(Q1 \--* Q2) ==> (Q1 x \-* Q2 x).
Proof using. intros. applys* himpl_hforall_l x. Qed.
Arguments qwand_specialize [ A ].
Properties of htop
Lemma htop_intro : forall h,
\Top h.
Proof using. intros. exists~ (=h). Qed.
Lemma himpl_htop_r : forall H,
H ==> \Top.
Proof using. intros. intros h Hh. applys* htop_intro. Qed.
Lemma htop_eq :
\Top = (\exists H, H).
Proof using. auto. Qed.
Lemma hstar_htop_htop :
\Top \* \Top = \Top.
Proof using.
applys himpl_antisym.
{ applys himpl_htop_r. }
{ rewrite <- hstar_hempty_r at 1. applys himpl_frame_r. applys himpl_htop_r. }
Qed.
Properties of hsingle
Lemma hsingle_intro : forall p v,
(p ~~> v) (Fmap.single p v).
Proof using. intros. hnfs*. Qed.
Lemma hsingle_inv: forall p v h,
(p ~~> v) h ->
h = Fmap.single p v.
Proof using. auto. Qed.
Lemma hstar_hsingle_same_loc : forall p w1 w2,
(p ~~> w1) \* (p ~~> w2) ==> \[False].
Proof using.
intros. unfold hsingle. intros h (h1&h2&E1&E2&D&E). false.
subst. applys* Fmap.disjoint_single_single_same_inv.
Qed.
Arguments hstar_hsingle_same_loc : clear implicits.
Definition and Properties of haffine and hgc
Definition haffine (H:hprop) :=
True.
Lemma haffine_hany : forall (H:hprop),
haffine H.
Proof using. unfold haffine. auto. Qed.
Lemma haffine_hempty :
haffine \[].
Proof using. applys haffine_hany. Qed.
Definition hgc :=
htop.
Notation "\GC" := (hgc) : hprop_scope.
Lemma haffine_hgc :
haffine \GC.
Proof using. applys haffine_hany. Qed.
Lemma himpl_hgc_r : forall H,
haffine H ->
H ==> \GC.
Proof using. introv M. applys himpl_htop_r. Qed.
Lemma hstar_hgc_hgc :
\GC \* \GC = \GC.
Proof using. applys hstar_htop_htop. Qed.
Functor Instantiation to Obtain xsimpl
End SepSimplArgs.
We are now ready to instantiate the functor that defines xsimpl.
Demos of xsimpl are presented in chapter Himpl.v.
Module Export HS := LibSepSimpl.XsimplSetup(SepSimplArgs).
Export SepSimplArgs.
From now on, all operators have opaque definitions.
Global Opaque hempty hpure hstar hsingle hexists hforall
hwand qwand htop hgc haffine.
At this point, the tactic xsimpl is defined. There remains to customize
the tactic so that it recognizes the predicate p ~~> v in a special way
when performing simplifications.
The tactic xsimpl_hook_hsingle p v operates as part of xsimpl.
The specification that follows makes sense only in the context of the
presentation of the invariants of xsimpl described in LibSepSimpl.v.
This tactic is invoked on goals of the form Xsimpl (Hla, Hlw, Hlt) HR,
where Hla is of the form H1 \* .. \* Hn \* \[]. The tactic
xsimpl_hook_hsingle p v searches among the Hi for a heap predicate
of the form p ~~> v'. If it finds one, it moves this Hi to the front,
just before H1. Then, it cancels it out with the p ~~> v that occurs
in HR. Otherwise, the tactic fails.
Ltac xsimpl_hook_hsingle p :=
xsimpl_pick_st ltac:(fun H' =>
match H' with (hsingle p ?v') =>
constr:(true) end);
apply xsimpl_lr_cancel_eq;
[ xsimpl_lr_cancel_eq_repr_post tt | ].
The tactic xsimpl_hook handles cancellation of heap predicates of the
form p ~~> v. It forces their cancellation against heap predicates of
the form p ~~> w, by asserting the equality v = w. Note: this tactic
is later refined to also handle records.
Ltac xsimpl_hook H ::=
match H with
| hsingle ?p ?v => xsimpl_hook_hsingle p
end.
One last hack is to improve the math tactic so that it is able
to handle the val_int coercion in goals and hypotheses of the
form val_int ?n = val_int ?m, and so that it is able to process
the well-founded relations dowto and upto for induction on
integers.
Specification of Record Operations
The chapter Struct shows how to these specifications may be
realized.
Implicit Types k : nat.
Representation of Records
A field name is implemented as a natural number
Definition field : Type := nat.
A record field is described as the pair of a field and a value stored
in that field.
Definition hrecord_field : Type := (field * val).
A record consists of a list of fields.
Definition hrecord_fields : Type := list hrecord_field.
Implicit Types kvs : hrecord_fields.
Lemma hstar_hpure_conj : forall H1 H2,
(\[H1] \* \[H2]) = \[H1 /\ H2].
Proof.
intros.
apply fun_ext_dep. intros h.
rewrite hstar_hpure_l.
apply prop_ext.
split; intros.
{ destruct H. apply hpure_inv in H0. destruct H0. subst. apply hpure_intro. intuition. }
{ apply hpure_inv in H. destruct H as ((?&?)&?). subst. intuition. now apply hpure_intro. }
Qed.
Lemma hstar_pure_post_pure : forall (P:val->Prop) P1,
(fun r => \[P r]) \*+ \[P1] = (fun r => \[P r /\ P1]).
Proof.
intros.
apply fun_ext_dep. intros h.
apply hstar_hpure_conj.
Qed.
Ltac hinv H :=
lazymatch type of H with
| \[] _ => apply hempty_inv in H
| \[_] _ => apply hpure_inv in H as (?&?)
| (_~~>_) _ => apply hsingle_inv in H
| (_ \* _) _ => apply hstar_inv in H as (?&?&?&?&?&?)
| (\[_] \* _) _ => rewrite hstar_hpure_l
| (_ \* \[_]) _ => rewrite hstar_hpure_r
end.
Ltac hintro :=
lazymatch goal with
| |- \[] _ => apply hempty_intro
| |- \[_] _ => apply hpure_intro
| |- (_ \* _) (_ \u _) => apply hstar_intro
| |- (\[_] \* _) _ => rewrite hstar_hpure_l
| |- (_ \* \[_]) _ => rewrite hstar_hpure_r
end.
End HeapSetup.