Commit 7cbc8b04 authored by charguer's avatar charguer

model_credits_structural

parent 09b0d0e5
Set Implicit Arguments.
Require Import LibCore Shared ModelLambda.
(* Ltac auto_star ::= jauto. -- not strong enough *)
(*------------------------------------------------------------------*)
(** Predicate over pairs *)
......@@ -232,7 +230,7 @@ Proof using.
Qed.
Lemma heap_union_assoc : forall h1 h2 h3,
h1 \+ (h2 \+ h3) = (h1 \+ h2) \+ h3.
(h1 \+ h2) \+ h3 = h1 \+ (h2 \+ h3).
(* LibOperation.assoc heap_union. *)
Proof using.
intros [m1 n1] [m2 n2] [m3 n3]. unfolds heap_union. simpls.
......@@ -282,6 +280,18 @@ Tactic Notation "rew_disjoint" :=
Tactic Notation "rew_disjoint" "*" :=
rew_disjoint; auto_star.
(** Auxiliary lemma *)
Lemma heap_union_comm_assoc : forall h1 h2 h3,
\# h1 h2 h3 ->
(h1 \+ h2) \+ h3 = h2 \+ (h3 \+ h1).
(* LibOperation.assoc heap_union. *)
Proof using.
introv M. rewrite (@heap_union_comm h1 h2).
rewrite~ heap_union_assoc. fequals.
rewrite~ heap_union_comm. rew_disjoint*. rew_disjoint*.
Qed.
(*------------------------------------------------------------------*)
(* ** Properties of [hprop] *)
......@@ -352,14 +362,14 @@ Proof using.
{ exists h1 h2. splits*. }
{ auto. }
{ rewrite* heap_disjoint_union_eq_l. }
{ rewrite~ <- heap_union_assoc. } }
{ rewrite~ heap_union_assoc. } }
{ intros (h'&h3&(h1&h2&M3&M4&D'&U')&M2&D&U). subst h'.
exists h1 (heap_union h2 h3). rewrite heap_disjoint_union_eq_l in D.
splits.
{ auto. }
{ exists h2 h3. splits*. }
{ rewrite* heap_disjoint_union_eq_r. }
{ rewrite~ heap_union_assoc. } }
{ rewrite~ <- heap_union_assoc. } }
Qed.
Lemma hprop_star_cancel : forall H1 H2 H2',
......@@ -485,6 +495,34 @@ Proof using.
exists~ n h1' h3 r.
Qed.
Lemma rule_consequence_gc : forall t H Q H' Q',
H ==> H' \* \GC ->
triple t H' Q' ->
Q' ===> Q \*+ \GC ->
triple t H Q.
Proof using.
introv IH M IQ. intros h1 h2 D1 H1.
lets H1': IH (rm H1).
lets (h1a&h1b&H1a&H1b&D1ab&E12): (rm H1').
lets (n&h1'&h3&r&Da&Ra&Qa&Ca): M (h1b \+ h2) (rm H1a).
{ subst. rew_disjoint*. }
lets Qa': IQ (rm Qa).
lets (h1a'&h1b'&H1a'&H1b'&D1ab'&E12'): (rm Qa').
exists n h1a' (h1b' \+ h1b \+ h3) r. splits.
{ subst. rew_disjoint*. }
{ subst. applys_eq Ra 2 4.
{ rewrite~ heap_union_assoc. }
{ fequals. rewrite (@heap_union_comm h1b h2).
repeat rewrite heap_union_assoc. fequals.
rewrite <- heap_union_comm_assoc.
rewrite <- heap_union_comm_assoc.
repeat rewrite heap_union_assoc. fequals. fequals.
rewrite~ heap_union_comm.
rew_disjoint*. rew_disjoint*. rew_disjoint*. rew_disjoint*. } }
{ auto. }
{ subst. rewrite heap_credits_union in *. math. }
Qed.
Lemma rule_frame : forall t H Q H',
triple t H Q ->
triple t (H \* H') (Q \*+ H').
......@@ -493,10 +531,10 @@ Proof using.
lets (n&h1'a&h3a&ra&Da&Ra&Qa&Na): M h1a (h1b \+ h2).
{ subst h1. rew_disjoint*. }
{ auto. }
{ subst h1. rewrite <- heap_union_assoc in Ra.
{ subst h1. rewrite heap_union_assoc in Ra.
exists n (h1'a \+ h1b) h3a ra. splits.
{ rew_disjoint*. }
{ do 2 rewrite <- heap_union_assoc. auto. }
{ do 2 rewrite heap_union_assoc. auto. }
{ exists h1'a h1b. splits~. rew_disjoint*. }
{ do 2 rewrite heap_credits_union. math. } }
Qed.
......@@ -542,7 +580,7 @@ Proof using.
{ auto. }
{ exists (na+nb)%nat h1'b (h3a \+ h3b) rb. splits.
{ rew_disjoint*. }
{ rewrite <- heap_union_assoc in Rb. constructors*. }
{ rewrite heap_union_assoc in Rb. constructors*. }
{ auto. }
{ math. } }
Qed.
......
......@@ -284,7 +284,7 @@ Proof using.
{ auto. }
{ exists h2 h3. splits*. }
{ rewrite* heap_disjoint_union_eq_r. }
{ rewrite~ heap_union_assoc. } }
{ rewrite~ <- heap_union_assoc. } }
Qed. (* later: exploit symmetry in the proof *)
Lemma hprop_star_cancel : forall H1 H2 H2',
......
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