Commit b6c3bb91 authored by charguer's avatar charguer

modelcredits

parent 1b32911d
(** We give two definitions equivalent to [triple], called
[triple'] and [triple'']. *)
Definition triple' t H Q :=
forall h1 h2,
\# h1 h2 ->
H h1 ->
exists n h1' v,
\# h1' h2
/\ redn n (h1 \u h2) t (h1' \u h2) v
/\ on_sub (Q v) h1'
/\ (heap_credits h1 >= n + heap_credits h1')%nat.
Lemma triple_eq_triple' : triple = triple'.
Proof using.
applys func_ext_3. intros t H Q. extens.
unfold triple, triple', credits. iff M.
{ introv D P1. forwards (n&h1'&v&R1&R2&R3&R4): M D P1.
exists n h1' v. splits~. math. }
{ introv D P1. forwards (n&h1'&v&R1&R2&R3&R4): M D P1.
exists n (h1' \u (state_empty,(h1^c - n - h1'^c)%nat)) v. splits~.
{ state_red. }
{ applys~ on_sub_union_r. }
{ simpl. math. } }
Qed.
(* DEPRECATED
(*------------------------------------------------------------------*)
(* ** Properties of [heap_empty] *)
Lemma heap_empty_state : heap_state heap_empty = state_empty.
Proof. auto. Qed.
Hint Rewrite heap_empty_state : rew_heap.
*)
(* TODO: DEPRECATED *)
Lemma heap_union_comm_assoc : forall h1 h2 h3,
\# h1 h2 h3 ->
(h1 \u h2) \u h3 = h2 \u (h3 \u h1).
Proof using.
introv M. rewrite (@heap_union_comm h1 h2).
rewrite~ heap_union_assoc. fequals.
rewrite~ heap_union_comm. state_disjoint.
Qed.
(** Disjoint3 *) (* TODO: DEPRECATED *)
Definition heap_disjoint_3 h1 h2 h3 :=
\# h1 h2 /\ \# h2 h3 /\ \# h1 h3.
Notation "\# h1 h2 h3" := (heap_disjoint_3 h1 h2 h3)
(at level 40, h1 at level 0, h2 at level 0, h3 at level 0, no associativity).
Hint Extern 1 (\# _ _ _) => state_disjoint_pre.
Lemma heap_disjoint_3_unfold : forall h1 h2 h3,
\# h1 h2 h3 = (\# h1 h2 /\ \# h2 h3 /\ \# h1 h3).
Proof using. auto. Qed.
Hint Rewrite
heap_disjoint_3_unfold : rew_disjoint.
(* DEPRECATED
| redn_new : forall ma mb v l,
mb = (state_single l v) ->
\# ma mb ->
redn 0 ma (trm_new v) (mb \+ ma) (val_loc l)
| redn_get : forall ma mb l v,
ma = (state_single l v) ->
\# ma mb ->
redn 0 (ma \+ mb) (trm_get (val_loc l)) (ma \+ mb) v
| redn_set : forall ma1 ma2 mb l v1 v2,
ma1 = (state_single l v1) ->
ma2 = (state_single l v2) ->
\# ma1 mb ->
redn 0 (ma1 \+ mb) (trm_set (val_loc l) v2) (ma2 \+ mb) val_unit.
Lemma rule_new : forall v,
triple (trm_new v) \[] (fun r => Hexists l, \[r = val_loc l] \* l ~~> v).
Proof using.
Transparent hprop_single.
introv D H1. unfolds hprop_single.
lets: hprop_empty_inv H1. subst h1. rewrite heap_union_empty_l.
asserts (l&Hl): (exists l, (state_data h2) l = None).
{ skip. } (* infinitely many locations -- TODO *)
asserts Fr: (state_disjoint h2 (state_single l v)).
{ unfolds state_disjoint, pfun_disjoint, state_single. simpls.
intros x. case_if~. }
exists 0%nat ((state_single l v),0%nat) heap_empty (val_loc l).
rewrite heap_union_empty_r. splits.
{ rew_disjoint. splits*. destruct h2 as (m2,n2). split~. }
{ rewrite heap_union_state. applys* redn_new. }
{ exists l heap_empty ((state_single l v),0%nat). splits~. }
{ simpl. math. }
Qed.
Lemma rule_get : forall v l,
triple (trm_get (val_loc l)) (l ~~> v) (fun x => \[x = v] \* l ~~> v).
Proof using.
Transparent hprop_single.
introv D H1. unfolds hprop_single.
exists 0%nat h1 heap_empty v. rewrite heap_union_empty_r.
splits.
{ state_disjoint. }
{ rewrite heap_union_state. applys~ redn_get. (* TODO: simplify below *)
{ destruct* h1 as (m1,n1). }
{ destruct h1 as (m1,n1). destruct h2 as (m2,n2). simpl.
unfold heap_disjoint in D. hnf in D. autos*. } }
{ exists heap_empty h1. splits~. }
{ math. }
Qed.
Lemma rule_set : forall l v w,
triple (trm_set (val_loc l) w) (l ~~> v) (fun r => \[r = val_unit] \* l ~~> w).
Proof using.
Transparent hprop_single.
introv D H1. unfolds hprop_single.
exists 0%nat (state_single l w, 0%nat) heap_empty val_unit.
rewrite heap_union_empty_r.
splits.
{ rew_disjoint. splits*.
destruct h1 as (m1,n1). destruct h2 as (m2,n2). destruct H1. subst m1.
unfolds heap_disjoint, state_disjoint, pfun_disjoint, state_single. simpls.
split~. destruct D as [D _].
intros x. specializes D x. case_if; intuition auto_false. }
{ do 2 rewrite heap_union_state. applys~ redn_set v. (* TODO: simplify below *)
{ destruct* h1 as (m1,n1). }
{ destruct h1 as (m1,n1). destruct h2 as (m2,n2). simpl.
unfold heap_disjoint in D. hnf in D. autos*. } }
{ exists heap_empty (state_single l w, 0%nat). splits~. }
{ simpl. math. }
Qed.
*)
(* DEPRECATED equivalent formulation
Lemma rule_val_fix : forall f x F V t1 H Q,
F = (val_fix f x t1) ->
triple (subst_trm f F (subst_trm x V t1)) H Q ->
triple (trm_app F V) ((\$ 1%nat) \* H) Q.
Proof using.
introv EF M. subst F. intros h1 h2 D1 (h1a&h1b&H1a&H1b&E3&E4).
hnf in H1a. lets H1a': hprop_credits_inv (rm H1a). clear E3.
lets~ (na&h1'a&v&Da&Ra&Qa&Na): M h1b h2 H1b.
exists (S na) h1'a v. splits~.
{ applys~ redn_app. state_red. }
{ subst. simpl. math. }
Qed.
*)
(* DEPRECATED
Definition app f v H Q :=
triple (trm_app f v) H Q.
Lemma rule_app_shorthand : forall f v H Q,
app f v H Q ->
triple (trm_app f v) H Q.
Proof using.
auto.
Qed.
Lemma rule_let_fix' : forall f x t1 t2 H Q,
(forall (F:val),
(forall X H' H'' Q',
pay_one H' H'' ->
triple (subst_trm f F (subst_trm x X t1)) H'' Q' ->
app F X H' Q') ->
triple (subst_trm f F t2) H Q) ->
triple (trm_let f (trm_val (val_fix f x t1)) t2) H Q.
*)
(* DEPRECATED
Lemma rule_consequence_gc : forall t H Q H' Q',
......
......@@ -295,6 +295,13 @@ Notation "vr '~~~>' v" := (hprop_single_val vr v)
(********************************************************************)
(* ** Characteristic formula generator *)
(*------------------------------------------------------------------*)
(* ** Definition of the [app] predicate *)
Definition app f v H Q :=
triple (trm_app f v) H Q.
(*------------------------------------------------------------------*)
(* ** Definition of CF blocks *)
......
This diff is collapsed.
......@@ -76,13 +76,13 @@ Definition hprop := heap -> Prop.
(** Lifting of predicates *)
Definition hprop_empty_st (P:Prop) : hprop :=
Definition hprop_pure (P:Prop) : hprop :=
fun h => h^f = state_empty /\ h^r = state_empty /\ P.
(** Empty heap *)
Definition hprop_empty : hprop :=
hprop_empty_st True.
hprop_pure True.
(** Singleton heap *)
......@@ -117,7 +117,7 @@ Definition hprop_or (H1 H2 : hprop) : hprop :=
Definition hprop_gc : hprop :=
hprop_exists (fun H => H).
Global Opaque hprop_empty hprop_empty_st hprop_single
Global Opaque hprop_empty hprop_pure hprop_single
hprop_star hprop_exists hprop_gc.
......@@ -127,7 +127,7 @@ Global Opaque hprop_empty hprop_empty_st hprop_single
Notation "\[]" := (hprop_empty)
(at level 0) : heap_scope.
Notation "\[ P ]" := (hprop_empty_st P)
Notation "\[ P ]" := (hprop_pure P)
(at level 0, P at level 99) : heap_scope.
Notation "r '~~>' v" := (hprop_single r v)
......@@ -505,17 +505,17 @@ Proof using. intros. apply (prove_Inhab hprop_empty). Qed.
Section HeapProp.
Implicit Types H : hprop.
Transparent hprop_empty hprop_empty_st hprop_single hprop_star hprop_gc.
Transparent hprop_empty hprop_pure hprop_single hprop_star hprop_gc.
Lemma hprop_empty_prove :
\[] heap_empty.
Proof using. hnfs~. Qed.
Lemma hprop_empty_st_prove : forall (P:Prop),
Lemma hprop_pure_prove : forall (P:Prop),
P -> \[P] heap_empty.
Proof using. intros. hnfs~. Qed.
Lemma hprop_empty_st_inv : forall h (P:Prop),
Lemma hprop_pure_inv : forall h (P:Prop),
\[P] h -> h = heap_empty /\ P.
Proof using.
intros ((f,g)&D) P (M1&M2&M3). simpls. subst. split~. fequals.
......@@ -538,7 +538,7 @@ Lemma hprop_star_empty_l : forall H,
Proof using.
intro. unfold hprop, hprop_star. extens. intros h.
iff (h1&h2&D0&D1&D2&D3) M.
{ subst. lets (E1&E2): hprop_empty_st_inv D1.
{ subst. lets (E1&E2): hprop_pure_inv D1.
subst. rew_heap~. }
{ exists heap_empty h. splits~. applys hprop_empty_prove. heap_eq. }
Qed.
......@@ -574,7 +574,7 @@ Lemma hprop_star_prop_elim : forall (P:Prop) H h,
(\[P] \* H) h -> P /\ H h.
Proof using.
introv (h1&h2&M1&M2&M3&M4). subst.
lets (E&R): hprop_empty_st_inv M2.
lets (E&R): hprop_pure_inv M2.
split~. subst. rew_heap~.
Qed.
......@@ -608,7 +608,7 @@ Lemma himpl_inst_prop : forall (P:Prop) H H',
P -> H ==> H' -> H ==> (\[P] \* H').
Proof using.
introv HP W. intros h M. exists heap_empty h. splits~.
{ applys~ hprop_empty_st_prove. }
{ applys~ hprop_pure_prove. }
{ rew_heap~. }
Qed.
......@@ -634,8 +634,8 @@ Implicit Arguments normal_post [A].
Lemma normal_empty :
normal hprop_empty.
Proof using.
Transparent hprop_empty hprop_empty_st.
introv M. unfolds hprop_empty, hprop_empty_st. autos*.
Transparent hprop_empty hprop_pure.
introv M. unfolds hprop_empty, hprop_pure. autos*.
Qed.
Lemma normal_single : forall l v,
......@@ -865,7 +865,7 @@ Lemma rule_extract_prop : forall t (P:Prop) H Q,
triple t (\[P] \* H) Q.
Proof using.
introv M. intros h1 (h11&h12&R1&P1&P2&R2) h2 D.
lets (E&HP): hprop_empty_st_inv (rm P1). subst h11.
lets (E&HP): hprop_pure_inv (rm P1). subst h11.
rew_heap in R2. subst h12. applys* M.
Qed.
......@@ -1116,7 +1116,7 @@ Lemma rule_new : forall v,
triple (trm_new v) \[] (fun r => Hexists l, \[r = val_loc l] \* l ~~> v).
Proof using.
intros. intros h1 P1 h2 _.
lets (E&_): hprop_empty_st_inv P1. subst h1.
lets (E&_): hprop_pure_inv P1. subst h1.
lets (l&Dl): (state_disjoint_new (heap_state h2) v).
lets~ (h1'&E1&E2): heap_make (state_single l v) state_empty.
asserts E3: (heap_state h1' = state_single l v).
......@@ -1145,7 +1145,7 @@ Proof using.
{ rew_state; auto. applys red_get. simpl.
rewrite E1,E2,E1'. simpl. unfold pfun_union. case_if~. }
{ exists heap_empty h1. splits~. heap_eq.
applys~ hprop_empty_st_prove. }
applys~ hprop_pure_prove. }
Qed.
Lemma rule_set : forall l v w,
......
......@@ -41,7 +41,7 @@ Definition hprop_empty : hprop :=
(** Lifting of predicates *)
Definition hprop_empty_st (H:Prop) : hprop :=
Definition hprop_pure (H:Prop) : hprop :=
fun h => h = state_empty /\ H.
(** Singleton heap *)
......@@ -67,7 +67,7 @@ Definition hprop_exists A (Hof : A -> hprop) : hprop :=
Definition hprop_gc : hprop :=
hprop_exists (fun H => H).
Global Opaque hprop_empty hprop_empty_st hprop_single
Global Opaque hprop_empty hprop_pure hprop_single
hprop_star hprop_exists hprop_gc.
......@@ -77,7 +77,7 @@ Global Opaque hprop_empty hprop_empty_st hprop_single
Notation "\[]" := (hprop_empty)
(at level 0) : heap_scope.
Notation "\[ L ]" := (hprop_empty_st L)
Notation "\[ L ]" := (hprop_pure L)
(at level 0, L at level 99) : heap_scope.
Notation "r '~~>' v" := (hprop_single r v)
......@@ -115,7 +115,7 @@ Proof using. intros. apply (prove_Inhab hprop_empty). Qed.
Section HeapProp.
Implicit Types H : hprop.
Transparent hprop_empty hprop_empty_st hprop_single hprop_star hprop_gc.
Transparent hprop_empty hprop_pure hprop_single hprop_star hprop_gc.
Lemma hprop_empty_prove :
\[] state_empty.
......@@ -125,12 +125,12 @@ Lemma hprop_empty_inv : forall h,
\[] h -> h = state_empty.
Proof using. auto. Qed.
Lemma hprop_empty_st_prove : forall (P:Prop),
Lemma hprop_pure_prove : forall (P:Prop),
P ->
\[P] state_empty.
Proof using. intros. hnfs~. Qed.
Lemma hprop_empty_st_inv : forall h (P:Prop),
Lemma hprop_pure_inv : forall h (P:Prop),
\[P] h ->
h = state_empty /\ P.
Proof using. intros. auto. Qed.
......@@ -223,7 +223,7 @@ Lemma himpl_inst_prop : forall (P:Prop) H H',
P -> H ==> H' -> H ==> (\[P] \* H').
Proof using.
introv HP W. intros h Hh. exists state_empty h.
splits*. applys* hprop_empty_st_prove. state_eq.
splits*. applys* hprop_pure_prove. state_eq.
Qed.
Lemma himpl_inst_exists : forall A (x:A) H J,
......@@ -240,7 +240,7 @@ Qed.
End HeapProp.
Hint Resolve hprop_empty_prove hprop_empty_st_prove.
Hint Resolve hprop_empty_prove hprop_pure_prove.
......
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