Commit 99934ca2 authored by charguer's avatar charguer

cf_sound_progress

parent 66fdc1e0
......@@ -213,7 +213,7 @@ Lemma local_extract_prop : forall (F:formula) H (P:Prop) Q,
F (\[P] \* H) Q.
Proof using.
introv L M. rewrite L. introv (h1&h2&(PH1&HP)&PH2&?&?).
subst h1. rewrite heap_union_empty_l in H1. subst h2.
subst h1. rew_state. subst h2.
exists H \[] Q. splits~.
{ rewrite~ hprop_star_empty_r. }
{ apply* qimpl_gc_instantiate. }
......@@ -256,7 +256,7 @@ Lemma local_frame : forall H1 H2 Q1 (F:formula) H Q,
Proof using.
introv L M WH WQ. rewrite L. introv Ph.
exists H1 H2 Q1. splits~.
skip. (* hchange WQ. hsimpl. *)
---. (* hchange WQ. hsimpl. *)
Qed.
(** Frame property from [local] *)
......@@ -545,6 +545,8 @@ Axiom Trm_size_subst_Trm_value : forall y (w:val) (t:Trm),
Trm_size (subst_Trm y w t) = Trm_size t.
(*--to move --*)
Lemma rule_consequence_frame : forall H2 H1 Q1 t H Q,
H ==> H1 \* H2 ->
triple t H1 Q1 ->
......@@ -554,7 +556,6 @@ Proof using.
introv HH Ht HQ. applys* rule_consequence HH. applys* rule_frame Ht.
Qed.
Lemma himpl_extract_prop : forall (P:Prop) H H',
(P -> H ==> H') -> (\[P] \* H) ==> H'.
Proof using.
......@@ -578,6 +579,8 @@ Lemma himpl_inst_exists : forall A (x:A) H J,
Proof using. introv W h. exists x. apply~ W. Qed.
Lemma cf_sound : forall (t:Trm),
sound_for t (cf t).
Proof using.
......@@ -595,8 +598,10 @@ Proof using.
{ forwards N: rule_new v. applys rule_consequence_frame H N.
{ rewrite~ hprop_star_empty_l. }
{ intros r. applys P r. } }
{ skip. }
{ skip. }
{ destruct P as (H'&l&w&R1&R2&R3). forwards N: rule_get w l.
rewrite R1. applys~ rule_consequence_frame H' N. }
{ destruct P as (H'&l&w&R1&R2&R3). forwards N: rule_set l w v0.
rewrite R1. applys~ rule_consequence_frame H' N. }
Qed.
......
......@@ -677,7 +677,7 @@ Proof using.
{ exists h1 heap_empty. splits~. { exists~ heap_empty h1. } }
Qed.
Lemma rule_set : forall l v w,
Lemma rule_set : forall l v w, (* todo: changer order of arguments *)
triple (trm_set (val_loc l) w) (l ~~> v) (fun r => \[r = val_unit] \* l ~~> w).
Proof using.
intros. intros h1 h2 D P1.
......
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