Commit 97978996 authored by Armaël Guéneau's avatar Armaël Guéneau

Improve the [affine] tactic; add more hints for heap data

parent 51d922ae
......@@ -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 :=
......
......@@ -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.
......
......@@ -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.
(* -------------------------------------------------------------------------- *)
......
......@@ -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]
......
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