Commit df7c5f92 authored by charguer's avatar charguer

structural_rules

parent 1617a008
(********************************************************************)
(* ** More *)
(** Substitution
Lemma subst_lemma : forall x v t H Q,
(forall (X:val), triple (subst_trm x X t) (H X) (Q X)) ->
triple (subst_trm x v t) (H v) (Q v).
Proof using.
auto.
Qed.
*)
(* BONUS
Lemma hprop_star_comm_assoc : comm_assoc hprop_star.
Proof using. apply comm_assoc_prove. apply star_comm. apply star_assoc. Qed.
Lemma hprop_star_post_neutral : forall B (Q:B->hprop),
Q \*+ \[] = Q.
Proof using. extens. intros. rewrite~ hprop_star_empty_r. Qed.
*)
(* BONUS
Notation "\[= v ]" := (fun x => \[x = v])
(at level 0) : heap_scope.
Notation "P ==+> Q" := (pred_le P%h (hprop_star P Q))
(at level 55, only parsing) : heap_scope.
*)
(*------------------------------------------------------------------*)
(* ** Normalization of [star] *)
(* BONUS
Hint Rewrite
hprop_star_empty_l hprop_star_empty_r (*hprop_star_post_neutral*) : rew_heap.
Hint Rewrite <- star_assoc : rew_heap.
Tactic Notation "rew_heap" :=
autorewrite with rew_heap.
Tactic Notation "rew_heap" "in" "*" :=
autorewrite with rew_heap in *.
Tactic Notation "rew_heap" "in" hyp(H) :=
autorewrite with rew_heap in H.
Tactic Notation "rew_heap" "~" :=
rew_heap; auto_tilde.
Tactic Notation "rew_heap" "~" "in" "*" :=
rew_heap in *; auto_tilde.
Tactic Notation "rew_heap" "~" "in" hyp(H) :=
rew_heap in H; auto_tilde.
Tactic Notation "rew_heap" "*" :=
rew_heap; auto_star.
Tactic Notation "rew_heap" "*" "in" "*" :=
rew_heap in *; auto_star.
Tactic Notation "rew_heap" "*" "in" hyp(H) :=
rew_heap in H; auto_star.
*)
......@@ -309,7 +309,7 @@ Qed.
(** Disjointness *)
Lemma state_disjoint_sym : forall h1 h2,
state_disjoint h1 h2 -> state_disjoint h2 h1.
\# h1 h2 -> \# h2 h1.
Proof using. intros [f1 F1] [f2 F2]. apply pfun_disjoint_sym. Qed.
Lemma state_disjoint_comm : forall h1 h2,
......@@ -317,18 +317,18 @@ Lemma state_disjoint_comm : forall h1 h2,
Proof using. lets: state_disjoint_sym. extens*. Qed.
Lemma state_disjoint_empty_l : forall h,
state_disjoint state_empty h.
\# state_empty h.
Proof using. intros [f F] x. simple~. Qed.
Lemma state_disjoint_empty_r : forall h,
state_disjoint h state_empty.
\# h state_empty.
Proof using. intros [f F] x. simple~. Qed.
Hint Resolve state_disjoint_sym state_disjoint_empty_l state_disjoint_empty_r.
Lemma state_disjoint_union_eq_r : forall h1 h2 h3,
state_disjoint h1 (state_union h2 h3) =
(state_disjoint h1 h2 /\ state_disjoint h1 h3).
\# h1 (h2 \+ h3) =
(\# h1 h2 /\ \# h1 h3).
Proof using.
intros [f1 F1] [f2 F2] [f3 F3].
unfolds state_disjoint, state_union. simpls.
......@@ -340,15 +340,15 @@ Proof using.
Qed.
Lemma state_disjoint_union_eq_l : forall h1 h2 h3,
state_disjoint (state_union h2 h3) h1 =
(state_disjoint h1 h2 /\ state_disjoint h1 h3).
\# (h2 \+ h3) h1 =
(\# h1 h2 /\ \# h1 h3).
Proof using.
intros. rewrite state_disjoint_comm.
apply state_disjoint_union_eq_r.
Qed.
Lemma state_single_same_loc_disjoint : forall (l:loc) (v1 v2:val),
state_disjoint (state_single l v1) (state_single l v2) -> False.
\# (state_single l v1) (state_single l v2) -> False.
Proof using.
introv D. specializes D l. simpls. case_if. destruct D; tryfalse.
Qed.
......@@ -359,43 +359,48 @@ Proof using. auto. Qed.
(** Compatibility *)
Lemma state_compatible_refl : refl state_compatible.
Lemma state_compatible_refl : forall h,
state_compatible h h.
(* LibRelation.refl state_compatible. *)
Proof using.
intros h. introv M1 M2. congruence.
Qed.
(** Union *)
Lemma ostate_union_idempotent : idempotent2 state_union.
Lemma state_union_idempotent : forall h,
h \+ h = h.
(* LibRelation.idempotent2 state_union. *)
Proof using.
intros [f F]. apply~ state_eq. simpl. intros x.
unfold pfun_union. cases~ (f x).
Qed.
Lemma state_union_empty_l : forall h,
state_union state_empty h = h.
state_empty \+ h = h.
Proof using.
intros [f F]. unfold state_union, pfun_union, state_empty. simpl.
apply~ state_eq.
Qed.
Lemma state_union_empty_r : forall h,
state_union h state_empty = h.
h \+ state_empty = h.
Proof using.
intros [f F]. unfold state_union, pfun_union, state_empty. simpl.
apply state_eq. intros x. destruct~ (f x).
Qed.
Lemma state_union_comm : forall h1 h2,
state_disjoint h1 h2 ->
state_union h1 h2 = state_union h2 h1.
\# h1 h2 ->
h1 \+ h2 = h2 \+ h1.
Proof using.
intros [f1 F1] [f2 F2] H. simpls. apply state_eq. simpl.
intros. rewrite~ pfun_union_comm.
Qed.
Lemma state_union_assoc :
LibOperation.assoc state_union.
Lemma state_union_assoc : forall h1 h2 h3,
(h1 \+ h2) \+ h3 = h1 \+ (h2 \+ h3).
(* LibOperation.assoc state_union. *)
Proof using.
intros [f1 F1] [f2 F2] [f3 F3]. unfolds state_union. simpls.
apply state_eq. intros x. unfold pfun_union. destruct~ (f1 x).
......
......@@ -165,8 +165,9 @@ Lemma heap_union_comm : forall h1 h2,
h1 \+ h2 = h2 \+ h1.
Proof using. intros. applys~ state_union_comm. Qed.
Lemma heap_union_assoc :
LibOperation.assoc heap_union.
Lemma heap_union_assoc : forall h1 h2 h3,
(h1 \+ h2) \+ h3 = h1 \+ (h2 \+ h3).
(* LibOperation.assoc heap_union. *)
Proof using. intros. applys~ state_union_assoc. Qed.
(** Disjoint3 *)
......@@ -198,6 +199,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] *)
......@@ -264,7 +277,7 @@ 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.
......@@ -346,18 +359,45 @@ Proof using.
exists~ 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 (h1'&h3&r&Da&Ra&Qa): M (h1b \+ h2) (rm H1a).
{ subst. rew_disjoint*. }
lets Qa': IQ (rm Qa).
lets (h1a'&h1b'&H1a'&H1b'&D1ab'&E12'): (rm Qa').
exists h1a' (h1b' \+ h1b \+ h3) r. splits.
{ subst. rew_disjoint*. }
{ subst. applys_eq Ra 2 4.
{ rewrite~ heap_union_assoc. }
{ 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. }
Qed.
Lemma rule_frame : 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).
introv M. intros h1 h2 D1 (h1a&h1b&H1a&H1b&D1ab&E12).
lets (h1'a&h3a&ra&Da&Ra&Qa): 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 (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*. } }
Qed.
......@@ -400,7 +440,7 @@ Proof using.
{ auto. }
{ exists h1'b (h3a \+ h3b) rb. splits.
{ rew_disjoint*. }
{ rewrite <- heap_union_assoc in Rb. constructors*. }
{ rewrite heap_union_assoc in Rb. constructors*. }
{ auto. } }
Qed.
......@@ -480,80 +520,3 @@ Proof using.
{ exists heap_empty (state_single l w). splits~. }
Qed.
(* TODO: add to hint extern "rew_disjoint" the jauto_set. *)
(********************************************************************)
(* ** More *)
(** Substitution
Lemma subst_lemma : forall x v t H Q,
(forall (X:val), triple (subst_trm x X t) (H X) (Q X)) ->
triple (subst_trm x v t) (H v) (Q v).
Proof using.
auto.
Qed.
*)
(* BONUS
Lemma hprop_star_comm_assoc : comm_assoc hprop_star.
Proof using. apply comm_assoc_prove. apply star_comm. apply star_assoc. Qed.
Lemma hprop_star_post_neutral : forall B (Q:B->hprop),
Q \*+ \[] = Q.
Proof using. extens. intros. rewrite~ hprop_star_empty_r. Qed.
*)
(* BONUS
Notation "\[= v ]" := (fun x => \[x = v])
(at level 0) : heap_scope.
Notation "P ==+> Q" := (pred_le P%h (hprop_star P Q))
(at level 55, only parsing) : heap_scope.
*)
(*------------------------------------------------------------------*)
(* ** Normalization of [star] *)
(* BONUS
Hint Rewrite
hprop_star_empty_l hprop_star_empty_r (*hprop_star_post_neutral*) : rew_heap.
Hint Rewrite <- star_assoc : rew_heap.
Tactic Notation "rew_heap" :=
autorewrite with rew_heap.
Tactic Notation "rew_heap" "in" "*" :=
autorewrite with rew_heap in *.
Tactic Notation "rew_heap" "in" hyp(H) :=
autorewrite with rew_heap in H.
Tactic Notation "rew_heap" "~" :=
rew_heap; auto_tilde.
Tactic Notation "rew_heap" "~" "in" "*" :=
rew_heap in *; auto_tilde.
Tactic Notation "rew_heap" "~" "in" hyp(H) :=
rew_heap in H; auto_tilde.
Tactic Notation "rew_heap" "*" :=
rew_heap; auto_star.
Tactic Notation "rew_heap" "*" "in" "*" :=
rew_heap in *; auto_star.
Tactic Notation "rew_heap" "*" "in" hyp(H) :=
rew_heap in H; auto_star.
*)
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