Commit 7fc3c32d authored by charguer's avatar charguer
Browse files

frame_proof

parent b1b14570
......@@ -1558,14 +1558,55 @@ Tactic Notation "hchange" constr(E1) constr(E2) constr(E3) :=
Implicit Types H : hprop.
Implicit Types Q : val -> hprop.
Lemma frame_rule : forall t H Q H',
triple t H Q ->
triple t (H \* H') (Q \*+ H').
Proof using. Qed.
Lemma seq_rule : forall t H Q Q1,
Lemma seq_rule : forall x t1 t2 H Q Q1,
triple t1 H Q1 ->
(forall (X:val), triple (subst_trm x X t2) (Q1 X) Q) ->
triple (trm_let x t1 t2) H Q.
Proof using. Qed.
Proof using.
introv M1 M2. intros h1 h2 D1 H1.
lets (h1'a&h3a&ra&Da&Ra&Qa): M1 D1 H1.
rew_disjoint.
forwards (h1'b&h3b&rb&Db&Rb&Qb): M2 ra h1'a (h2 \+ h3a).
{ rew_disjoint. jauto. }
{ auto. }
{ exists h1'b (h3a \+ h3b) rb. splits.
{ rew_disjoint. jauto. }
{ rewrite <- heap_union_assoc in Rb. constructors*. }
{ auto. } }
Qed.
Lemma frame_rule : forall t H Q H',
triple t H Q ->
triple t (H \* H') (Q \*+ H').
Proof using.
introv M. intros h1 h2 D1 (h1a&h1b&H1a&H1b&D12a&E12).
lets (h1'a&h3a&ra&Da&Ra&Qa): M h1a (h1b \+ h2).
{ subst h1. rew_disjoint. jauto. }
{ auto. }
{ subst h1. rewrite <- heap_union_assoc in Ra.
exists (h1'a \+ h1b) h3a ra. splits.
{ rew_disjoint. jauto. }
{ do 2 rewrite <- heap_union_assoc. eauto. }
{ exists h1'a h1b. splits~. rew_disjoint. jauto. } }
Qed.
(* TODO: add to hint extern "rew_disjoint" the jauto_set. *)
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