Commit 99a3d3fe authored by charguer's avatar charguer

credits_new_rule

parent 8757d403
......@@ -301,7 +301,7 @@ Proof using. intros. apply (prove_Inhab hprop_empty). Qed.
Section HeapProp.
Transparent hprop_empty hprop_empty_st hprop_single hprop_star heap_union.
Transparent hprop_empty hprop_empty_st hprop_single hprop_star hprop_gc heap_union.
Lemma hprop_empty_prove :
\[] heap_empty.
......@@ -398,6 +398,15 @@ Lemma hprop_exists_witness : forall A (x:A) H J,
(H ==> J x) -> H ==> (hprop_exists J).
Proof using. introv W h. exists x. apply~ W. Qed.
Lemma hprop_gc_remove : forall H H',
H ==> H' ->
H ==> H' \* \GC.
Proof using.
introv M. intros h Hh. exists h heap_empty. splits*.
exists \[]. auto.
Qed.
End HeapProp.
Hint Resolve hprop_empty_prove hprop_empty_st_prove.
......@@ -523,6 +532,17 @@ Proof using.
{ subst. rewrite heap_credits_union in *. math. }
Qed.
Lemma rule_consequence : forall H' Q' t H Q,
H ==> H' ->
triple t H' Q ->
Q ===> Q' ->
triple t H Q'.
Proof using.
introv WH M WQ. applys rule_consequence_gc M.
{ applys~ hprop_gc_remove. }
{ intros r. applys~ hprop_gc_remove. }
Qed.
Lemma rule_frame : forall t H Q H',
triple t H Q ->
triple t (H \* H') (Q \*+ H').
......@@ -592,6 +612,24 @@ Proof using.
auto.
Qed.
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&h3a&ra&Da&Ra&Qa&Na): M h1b h2 H1b.
{ subst. rew_disjoint*. }
exists (S na) h1'a h3a ra. splits.
{ rew_disjoint*. }
{ applys~ redn_app. applys_eq Ra 4.
subst h1 h1a. repeat rewrite heap_state_union.
rewrite~ state_union_empty_l. }
{ auto. }
{ subst h1 h1a. rewrite heap_credits_union. simpl. math. }
Qed.
Lemma rule_fix : forall f x t1 t2 H Q,
(forall (F:val),
(forall X H' H'' Q',
......@@ -604,17 +642,9 @@ Proof using.
introv M D H1.
forwards (n&h1'&h3&r&R1&R2&R3&R4): M (val_fix f x t1) D H1.
{ clears h1 h2 H Q. intros X H H' Q K M. unfolds.
introv D H1. lets (h1a&h1b&H1a&H1b&E3&E4): K H1.
lets H1a': hprop_credits_inv (rm H1a). clear E3.
forwards (n&h1'&h3&r&R1&R2&R3&R4): M h2 H1b.
{ subst h1 h1a. rew_disjoint*. }
exists (S n) h1' h3 r. splits.
{ rew_disjoint*. }
{ applys~ redn_app. applys_eq R2 4.
subst h1 h1a. repeat rewrite heap_state_union.
rewrite~ state_union_empty_l. }
{ auto. }
{ subst h1 h1a. rewrite heap_credits_union. simpl. math. } }
applys rule_consequence K.
{ applys~ rule_val_fix M. }
{ auto. } }
exists n h1' h3 r. splits.
{ rew_disjoint*. }
{ applys~ redn_fix. }
......
......@@ -220,7 +220,7 @@ Proof using. intros. apply (prove_Inhab hprop_empty). Qed.
Section HeapProp.
Transparent hprop_empty hprop_empty_st hprop_single hprop_star heap_union.
Transparent hprop_empty hprop_empty_st hprop_single hprop_star hprop_gc heap_union.
Lemma hprop_empty_prove :
\[] heap_empty.
......@@ -312,6 +312,14 @@ Lemma hprop_exists_witness : forall A (x:A) H J,
(H ==> J x) -> H ==> (hprop_exists J).
Proof using. introv W h. exists x. apply~ W. Qed.
Lemma hprop_gc_remove : forall H H',
H ==> H' ->
H ==> H' \* \GC.
Proof using.
introv M. intros h Hh. exists h heap_empty. splits*.
exists \[]. auto.
Qed.
End HeapProp.
Hint Resolve hprop_empty_prove hprop_empty_st_prove.
......@@ -386,6 +394,17 @@ Proof using.
{ auto. }
Qed.
Lemma rule_consequence : forall H' Q' t H Q,
H ==> H' ->
triple t H' Q ->
Q ===> Q' ->
triple t H Q'.
Proof using.
introv WH M WQ. applys rule_consequence_gc M.
{ applys~ hprop_gc_remove. }
{ intros r. applys~ hprop_gc_remove. }
Qed.
Lemma rule_frame : forall t H Q H',
triple t H Q ->
triple t (H \* H') (Q \*+ H').
......@@ -451,30 +470,37 @@ Proof using.
auto.
Qed.
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) H Q.
Proof using.
introv EF M. subst F. intros h1 h2 D1 H1.
lets (h1'a&h3a&ra&Da&Ra&Qa): M D1 H1.
exists h1'a h3a ra. splits.
{ rew_disjoint*. }
{ applys~ red_app. }
{ auto. }
Qed.
Lemma rule_fix : forall f x t1 t2 H Q,
(forall (F:val),
(forall X H' Q', triple (subst_trm f F (subst_trm x X t1)) H' Q'
-> app F X H' Q') ->
(forall X H' Q',
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_fix f x t1 t2) H Q.
Proof using.
introv M D H1.
forwards (h1'&h3&r&R1&R2&R3): M (val_fix f x t1) D H1.
{ clears h1 h2 H Q. intros X H Q M. unfolds.
introv D H1.
forwards (h1'&h3&r&R1&R2&R3): M D H1.
exists h1' h3 r. splits.
{ rew_disjoint*. }
{ applys~ red_app. }
{ auto. } }
applys~ rule_val_fix M. }
exists h1' h3 r. splits.
{ rew_disjoint*. }
{ applys~ red_fix. }
{ auto. }
Qed.
(* TODO: redo the proofs with opaque hprop_single *)
Lemma rule_new : forall v,
triple (trm_new v) \[] (fun r => Hexists l, \[r = val_loc l] \* l ~~> v).
Proof using.
......
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