Commit 90a9b46c authored by charguer's avatar charguer
Browse files

ro_frame

parent 1950967d
......@@ -360,13 +360,13 @@ Qed.
(********************************************************************)
(* ** Triple *)
Definition triple t H Q :=
Definition triple t (H:hprop) (Q:val->hprop) :=
forall h1 g1 h2, \# h1 g1 h2 ->
H (h1,g1) ->
exists h1' h3 r,
\# h1' h2 h3
/\ red (h1 \+ g1 \+ h2) t (h1' \+ g1 \+ h2 \+ h3) r
/\ Q r h1'.
/\ Q r (h1',state_empty).
......@@ -507,6 +507,8 @@ Tactic Notation "rew_disjoint" "*" :=
(*------------------------------------------------------------------*)
(* ** Properties on heaps *)
(*
(** Disjointness *)
Lemma heap_disjoint_sym : forall h1 h2,
......@@ -621,7 +623,7 @@ Tactic Notation "rew_disjoint" :=
Tactic Notation "rew_disjoint" "*" :=
rew_disjoint; auto_star.
*)
(********************************************************************)
(* ** Predicate on Heaps *)
......@@ -634,6 +636,7 @@ Global Opaque heap_is_empty_st heap_is_single.
(*------------------------------------------------------------------*)
(* ** Properties of heap empty *)
(*
Section HeapEmpty.
Transparent heap_is_empty_st.
......@@ -648,35 +651,49 @@ Proof using. intros. hnfs~. Qed.
End HeapEmpty.
Hint Resolve heap_is_empty_prove heap_is_empty_st_prove.
*)
(*------------------------------------------------------------------*)
(* ** Properties of [star] and [pack] *)
Section HeapStar.
Transparent heap_is_star heap_union.
(* Transparent heap_is_star heap_union. *)
(* TODO; move *)
Axiom state_compatible_sym : sym state_compatible.
Lemma star_comm : comm heap_is_star.
Proof using.
intros H1 H2. unfold hprop, heap_is_star. extens. intros h.
iff (h1&h2&M1&M2&D&U); rewrite~ heap_union_comm in U; exists* h2 h1.
intros H1 H2. unfold hprop, heap_is_star. extens. intros (h,g).
iff (h1&g1&h2&g2&M1&M2&M3&M4&M5&M6);
rewrite state_union_comm in M4, M6; auto;
applys_to M5 state_compatible_sym.
exists* h2 g2 h1 g1.
(*lets: disjoint_sym. *) skip.
exists* h2 g2 h1 g1.
(*lets: disjoint_sym. *) skip.
Qed.
Lemma star_neutral_l : neutral_l heap_is_star \[].
Proof using.
Proof using. Admitted.
(*
intros H. unfold hprop, heap_is_star. extens. intros h.
iff (h1&h2&M1&M2&D&U) M.
hnf in M1. subst h1 h. rewrite~ heap_union_neutral_l.
exists heap_empty h. splits~.
Qed.
Qed.*)
Lemma star_neutral_r : neutral_r heap_is_star \[].
Proof using.
Proof using. Admitted.
(*
apply neutral_r_from_comm_neutral_l.
apply star_comm. apply star_neutral_l.
Qed.
*)
Lemma star_assoc : LibOperation.assoc heap_is_star.
Proof using.
Proof using. Admitted.
(*
intros H1 H2 H3. unfold hprop, heap_is_star. extens. intros h. split.
intros (h1&h'&M1&(h2&h3&M3&M4&D'&U')&D&U). subst h'.
exists (heap_union h1 h2) h3. rewrite heap_disjoint_union_eq_r in D.
......@@ -693,6 +710,7 @@ Proof using.
rewrite* heap_disjoint_union_eq_r.
rewrite~ heap_union_assoc.
Qed. (* later: exploit symmetry in the proof *)
*)
Lemma star_comm_assoc : comm_assoc heap_is_star.
Proof using. apply comm_assoc_prove. apply star_comm. apply star_assoc. Qed.
......@@ -703,23 +721,32 @@ Proof using. extens. intros. (* unfold starpost. *) rewrite~ star_neutral_r. Qed
Lemma star_cancel : forall H1 H2 H2',
H2 ==> H2' -> H1 \* H2 ==> H1 \* H2'.
(*
Proof using. introv W (h1&h2&?). exists* h1 h2. Qed.
*)
Admitted.
Lemma star_is_single_same_loc : forall (l:loc) (v1 v2:val),
(heap_is_single l v1) \* (heap_is_single l v2) ==> \[False].
Proof using.
(*
Transparent heap_is_single state_single.
intros. intros h ((m1&n1)&(m2&n2)&E1&E2&D&E).
unfolds heap_disjoint, state_disjoint, prod_st2, pfun_disjoint.
specializes D l. rewrite E1, E2 in D.
unfold state_single in D. simpls. case_if. destruct D; tryfalse.
Qed.
*)
Admitted.
Lemma heap_star_prop_elim : forall (P:Prop) H h,
(\[P] \* H) h -> P /\ H h.
Proof using.
Admitted.
(*
introv (?&?&N&?&?&?). destruct N. subst. rewrite~ heap_union_neutral_l.
Qed.
*)
Lemma heap_extract_prop : forall (P:Prop) H H',
(P -> H ==> H') -> (\[P] \* H) ==> H'.
......@@ -772,39 +799,69 @@ Tactic Notation "rew_heap" "*" "in" hyp(H) :=
Implicit Types H : hprop.
Implicit Types Q : val -> hprop.
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.
Lemma seq_rule : forall x t1 t2 H1 H2 Q Q1,
triple t1 H1 Q1 ->
(forall (X:val), triple (subst_trm x X t2) (Q1 X \* H2) Q) ->
triple (trm_let x t1 t2) (H1 \* H2) Q.
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. } }
introv M1 M2.
intros h1 g1 h2 D1 (h11&g11&h12&g12&R1&R2&R3&R4&R5&R6).
lets~ (h1'a&h3a&ra&Da&Ra&Qa): M1 h11 g11 (h12 \+ g12 \+ h2).
{ skip. }
forwards (h1'b&h3b&rb&Db&Rb&Qb):
M2 ra (h1'a \+ h12) g12 (h2 \+ g11 \+ h3a).
{ skip. }
hnf. exists h1'a state_empty (h12) (g12). splits~.
{ skip. }
{ skip. }
exists h1'b (h3a \+ h3b) rb. splits.
{ subst. skip. (* rew_disjoint. jauto. *) }
{ rewrite <- state_union_assoc in Rb.
applys red_let (h1'a \+ g11 \+ (h12 \+ g12 \+ h2) \+ h3a) ra.
{ applys_eq Ra 4. subst. skip. }
{ applys_eq Rb 2 4. subst. skip. subst. skip. } }
{ auto. }
Qed.
Lemma frame_rule : forall t H Q H',
triple t H Q ->
triple t (H \* H') (Q \*+ H').
Lemma frame_rule : forall t H1 Q1 H2,
triple t H1 Q1 ->
storable H2 ->
triple t (H1 \* H2) (Q1 \*+ H2).
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. }
introv M1 SH2.
intros h1 g1 h2 D1 (h1a&g1a&h1b&g1b&R1&R2&R3&R4&R5&R6).
lets E: SH2 R2. subst g1b.
lets (h1'a&h3a&ra&Da&Ra&Qa): M1 h1a g1a (h1b \+ h2).
{ subst h1. rew_disjoint. jauto. skip. }
{ auto. }
{ subst h1. rewrite <- heap_union_assoc in Ra.
{ subst h1. rewrite <- state_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. } }
{ do 2 rewrite <- state_union_assoc. applys_eq Ra 2 4.
{ subst. skip. }
{ subst. skip. } }
{ exists h1'a state_empty h1b state_empty. splits~.
{ skip. }
{ skip. } }
Qed.
(*
H ==> Q v /\ Storable H
----------------------------- [val]
{ H } v { Q }
H ==> Q v \* GC /\ Storable Q
----------------------------------- [val-gc]
{ H } v { Q }
*)
(* 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