Commit 98423d5a authored by charguer's avatar charguer

cleanup_with_tactic

parent a3df639d
......@@ -121,10 +121,6 @@ Notation "\# h1 h2" := (heap_disjoint h1 h2)
Notation "h1 \+ h2" := (heap_union h1 h2)
(at level 51, right associativity) : heap_scope.
Open Scope heap_scope.
Bind Scope heap_scope with hprop.
Delimit Scope heap_scope with h.
Notation "\[]" := (hprop_empty)
(at level 0) : heap_scope.
......@@ -144,7 +140,7 @@ Notation "'Hexists' x1 , H" := (hprop_exists (fun x1 => H))
(at level 39, x1 ident, H at level 50) : heap_scope.
Notation "'Hexists' x1 : T1 , H" := (hprop_exists (fun x1:T1 => H))
(at level 39, x1 ident, H at level 50, only parsing) : heap_scope.
Notation "'Hexists' ( x1 : T1 ) , H" := (Hexists x1:T1,H)
Notation "'Hexists' ( x1 : T1 ) , H" := (hprop_exists (fun x1:T1 => H))
(at level 39, x1 ident, H at level 50, only parsing) : heap_scope.
Notation "\GC" := (hprop_gc) : heap_scope.
......@@ -152,6 +148,10 @@ Notation "\GC" := (hprop_gc) : heap_scope.
Notation "'\$' n" := (hprop_credits n)
(at level 40, format "\$ n") : heap_scope.
Open Scope heap_scope.
Bind Scope heap_scope with hprop.
Delimit Scope heap_scope with h.
(********************************************************************)
(* ** Properties *)
......@@ -221,7 +221,7 @@ Lemma heap_union_comm : forall h1 h2,
h1 \+ h2 = h2 \+ h1.
Proof using.
intros [m1 n1] [m2 n2] H. simpls. fequals.
applys* state_union_comm.
applys* state_union_comm_disjoint.
math.
Qed.
......@@ -285,7 +285,7 @@ Lemma heap_union_comm_assoc : forall h1 h2 h3,
Proof using.
introv M. rewrite (@heap_union_comm h1 h2).
rewrite~ heap_union_assoc. fequals.
rewrite~ heap_union_comm. rew_disjoint*. rew_disjoint*.
rewrite~ heap_union_comm. state_disjoint. state_disjoint.
Qed.
......@@ -444,7 +444,7 @@ Proof using.
exists (state_empty,c1) (state_empty,c2). simpl. splits*.
autos* state_disjoint_empty_l.
subst. rewrite* state_union_empty_l.
inverts M4. subst*.
inverts M4. subst. split~. state_eq.
Qed.
Lemma credits_substract : forall (n m : nat),
......@@ -497,7 +497,7 @@ Lemma rule_extract_prop : forall t (P:Prop) H Q,
triple t (H \* \[P]) Q.
Proof using.
introv M D (h21&h22&N1&(HE&HP)&N3&N4). subst h22 h1.
rewrite heap_union_empty_r. applys* M. rew_disjoint*.
rewrite heap_union_empty_r. applys* M. state_disjoint.
Qed.
Lemma rule_extract_exists : forall t (J:val->hprop) Q,
......@@ -515,11 +515,11 @@ Proof using.
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*. }
{ state_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*. }
{ state_disjoint. }
{ subst. applys_eq Ra 2 4.
{ rewrite~ heap_union_assoc. }
{ fequals. rewrite (@heap_union_comm h1b h2).
......@@ -528,10 +528,10 @@ Proof using.
rewrite <- heap_union_comm_assoc.
repeat rewrite heap_union_assoc. fequals. fequals.
rewrite~ heap_union_comm.
rew_disjoint*. rew_disjoint*. rew_disjoint*. rew_disjoint*. } }
state_disjoint. state_disjoint. state_disjoint. state_disjoint. } }
{ auto. }
{ subst. rewrite heap_credits_union in *. math. }
Qed.
Qed. (* TODO: tactic for heap simplification *)
Lemma rule_consequence : forall H' Q' t H Q,
H ==> H' ->
......@@ -550,13 +550,13 @@ Lemma rule_frame : forall t H Q H',
Proof using.
introv M. intros h1 h2 D1 (h1a&h1b&H1a&H1b&D12a&E12).
lets (n&h1'a&h3a&ra&Da&Ra&Qa&Na): M h1a (h1b \+ h2).
{ subst h1. rew_disjoint*. }
{ subst h1. state_disjoint. }
{ auto. }
{ subst h1. rewrite heap_union_assoc in Ra.
exists n (h1'a \+ h1b) h3a ra. splits.
{ rew_disjoint*. }
{ state_disjoint. }
{ do 2 rewrite heap_union_assoc. auto. }
{ exists h1'a h1b. splits~. rew_disjoint*. }
{ exists h1'a h1b. splits~. state_disjoint. }
{ do 2 rewrite heap_credits_union. math. } }
Qed.
......@@ -569,7 +569,7 @@ Proof using.
introv M D H1.
exists 0%nat h1 heap_empty v. rewrite heap_union_empty_r.
splits.
{ rew_disjoint*. }
{ state_disjoint. }
{ applys redn_val. }
{ auto. }
{ math. }
......@@ -582,7 +582,7 @@ Proof using.
introv M D H1.
forwards (n&h1'&h3&r&Da&Ra&Qa&Na): M D H1.
exists n h1' h3 r. splits.
{ rew_disjoint*. }
{ state_disjoint. }
{ applys~ redn_if. }
{ auto. }
{ math. }
......@@ -597,10 +597,10 @@ Proof using.
lets (na&h1'a&h3a&ra&Da&Ra&Qa&Na): M1 D1 H1.
rew_disjoint.
forwards (nb&h1'b&h3b&rb&Db&Rb&Qb&Nb): M2 ra h1'a (h2 \+ h3a).
{ rew_disjoint*. }
{ state_disjoint. }
{ auto. }
{ exists (na+nb)%nat h1'b (h3a \+ h3b) rb. splits.
{ rew_disjoint*. }
{ state_disjoint. }
{ rewrite heap_union_assoc in Rb. constructors*. }
{ auto. }
{ math. } }
......@@ -621,9 +621,9 @@ Proof using.
introv EF M. subst F. intros h1 h2 D1 (h1a&h1b&H1a&H1b&E3&E4).
hnf in H1a. lets H1a': hprop_credits_inv (rm H1a). clear E3.
lets (na&h1'a&h3a&ra&Da&Ra&Qa&Na): M h1b h2 H1b.
{ subst. rew_disjoint*. }
{ subst. state_disjoint. }
exists (S na) h1'a h3a ra. splits.
{ rew_disjoint*. }
{ state_disjoint. }
{ applys~ redn_app. applys_eq Ra 4.
subst h1 h1a. repeat rewrite heap_state_union.
rewrite~ state_union_empty_l. }
......@@ -631,6 +631,7 @@ Proof using.
{ subst h1 h1a. rewrite heap_credits_union. simpl. math. }
Qed.
(* TODO: update
Lemma rule_fix : forall f x t1 t2 H Q,
(forall (F:val),
(forall X H' H'' Q',
......@@ -638,7 +639,7 @@ Lemma rule_fix : forall f x t1 t2 H Q,
triple (subst_trm f F (subst_trm x X t1)) H'' Q' ->
app F X H' Q') ->
triple (subst_trm f F t2) H Q) ->
triple (trm_fix f x t1 t2) H Q.
triple (trm_fun f x t1 t2) H Q.
Proof using.
introv M D H1.
forwards (n&h1'&h3&r&R1&R2&R3&R4): M (val_fix f x t1) D H1.
......@@ -647,11 +648,12 @@ Proof using.
{ applys~ rule_val_fix M. }
{ auto. } }
exists n h1' h3 r. splits.
{ rew_disjoint*. }
{ state_disjoint. }
{ applys~ redn_fix. }
{ auto. }
{ math. }
Qed.
*)
Lemma rule_new : forall v,
triple (trm_new v) \[] (fun r => Hexists l, \[r = val_loc l] \* l ~~> v).
......@@ -679,7 +681,7 @@ Proof using.
introv D H1. unfolds hprop_single.
exists 0%nat h1 heap_empty v. rewrite heap_union_empty_r.
splits.
{ rew_disjoint*. }
{ state_disjoint. }
{ rewrite heap_state_union. applys~ redn_get. (* TODO: simplify below *)
{ destruct* h1 as (m1,n1). }
{ destruct h1 as (m1,n1). destruct h2 as (m2,n2). simpl.
......
......@@ -83,7 +83,7 @@ Definition pfun_union (A B : Type) (f1 f2 : pfun A B) :=
| None => f2 x
end.
Definition pfun_compatible (A B : Type) (f1 f2 : pfun A B) :=
Definition pfun_compat (A B : Type) (f1 f2 : pfun A B) :=
forall x v1 v2,
f1 x = Some v1 ->
f2 x = Some v2 ->
......@@ -113,8 +113,8 @@ Definition state_disjoint_3 h1 h2 h3 :=
(** Compatible states *)
Definition state_compatible (g1 g2 : state) :=
pfun_compatible g1 g2.
Definition state_compat (g1 g2 : state) :=
pfun_compat g1 g2.
(** Finiteness of union *)
......@@ -283,7 +283,6 @@ Proof using.
Qed.
(*------------------------------------------------------------------*)
(* ** Properties on states *)
......@@ -340,20 +339,58 @@ Proof using. auto. Qed.
(** Compatibility *)
Lemma state_compatible_refl : forall h,
state_compatible h h.
(* LibRelation.refl state_compatible. *)
Lemma state_compat_refl : forall h,
state_compat h h.
(* LibRelation.refl state_compat. *)
Proof using.
intros h. introv M1 M2. congruence.
Qed.
Lemma state_disjoint_compatible : forall h1 h2,
Lemma state_compat_sym : forall f1 f2,
state_compat f1 f2 ->
state_compat f2 f1.
Proof using.
introv M. intros l v1 v2 E1 E2.
specializes M l E1. (* TODO: bug ?*)
Qed.
Lemma state_disjoint_compat : forall h1 h2,
state_disjoint h1 h2 ->
state_compatible h1 h2.
state_compat h1 h2.
Proof using.
introv HD. intros l v1 v2 M1 M2. destruct (HD l); false.
Qed.
Lemma state_compat_empty_l : forall h,
state_compat state_empty h.
Proof using. intros h l v1 v2 E1 E2. simpls. false. Qed.
Lemma state_compat_empty_r : forall h,
state_compat h state_empty.
Proof using.
hint state_compat_sym, state_compat_empty_l. eauto.
Qed.
Lemma state_compat_union_l : forall f1 f2 f3,
state_compat f1 f3 ->
state_compat f2 f3 ->
state_compat (f1 \+ f2) f3.
Proof using.
introv M1 M2. intros l v1 v2 E1 E2.
specializes M1 l. specializes M2 l.
simpls. unfolds pfun_union. cases (state_data f1 l).
{ inverts E1. applys* M1. }
{ applys* M2. }
Qed.
Lemma state_compat_union_r : forall f1 f2 f3,
state_compat f1 f2 ->
state_compat f1 f3 ->
state_compat f1 (f2 \+ f3).
Proof using.
hint state_compat_sym, state_compat_union_l. eauto.
Qed.
(** Union *)
Lemma state_union_idempotent : forall h,
......@@ -378,7 +415,7 @@ Proof using.
apply state_eq. intros x. destruct~ (f x).
Qed.
Lemma state_union_comm : forall h1 h2,
Lemma state_union_comm_disjoint : forall h1 h2,
\# h1 h2 ->
h1 \+ h2 = h2 \+ h1.
Proof using.
......@@ -386,6 +423,15 @@ Proof using.
intros. rewrite~ pfun_union_comm.
Qed.
Lemma state_union_comm_compat : forall h1 h2,
state_compat h1 h2 ->
h1 \+ h2 = h2 \+ h1.
Proof using.
intros [f1 F1] [f2 F2] H. simpls. apply state_eq. simpl.
intros l. specializes H l. unfolds pfun_union. simpls.
cases (f1 l); cases (f2 l); auto. fequals. applys* H.
Qed.
Lemma state_union_assoc : forall h1 h2 h3,
(h1 \+ h2) \+ h3 = h1 \+ (h2 \+ h3).
(* LibOperation.assoc state_union. *)
......@@ -394,9 +440,17 @@ Proof using.
apply state_eq. intros x. unfold pfun_union. destruct~ (f1 x).
Qed.
(** Hints and tactics *)
Hint Resolve state_union_empty_l state_union_empty_r.
(************************************************************)
(** * Tactics *)
(*------------------------------------------------------------------*)
(* ** Proving disjointness results *)
(** [state_disjoint] proves goals of the form [\# h1 h2] and
[\# h1 h2 h3] by expanding all hypotheses into binary forms
[\# h1 h2] and then exploiting symmetry and disjointness
with [state_empty]. *)
Hint Rewrite
state_disjoint_union_eq_l
......@@ -408,16 +462,157 @@ Tactic Notation "rew_disjoint" :=
Tactic Notation "rew_disjoint" "*" :=
rew_disjoint; auto_star.
(** Auxiliary lemmas *)
Tactic Notation "state_disjoint" :=
try solve [ subst; rew_disjoint; jauto_set; auto ].
Tactic Notation "state_disjoint_if_needed" :=
match goal with
| |- \# _ _ => state_disjoint
| |- \# _ _ _ => state_disjoint
end.
Lemma state_disjoint_demo : forall h1 h2 h3 h4 h5,
h1 = h2 \+ h3 ->
\# h2 h3 ->
\# h1 h4 h5 ->
\# h3 h2 h5 /\ \# h4 h5.
Proof using.
intros. dup 2.
{ subst. rew_disjoint. jauto_set. auto. auto. auto. auto. }
{ state_disjoint. }
Qed.
(*------------------------------------------------------------------*)
(* ** Proving equality of states *)
(** [state_eq] proves equalities between unions of states.
It attempts to discharge the disjointness side-conditions.
Disclaimer: cancels heaps at depth up to 4, but no more. *)
Lemma state_union_eq_cancel_1 : forall h1 h2 h2',
h2 = h2' ->
h1 \+ h2 = h1 \+ h2'.
Proof using. intros. subst. auto. Qed.
Lemma state_union_eq_cancel_1' : forall (h1:state),
h1 = h1.
Proof using. intros. auto. Qed.
Lemma state_union_eq_cancel_2 : forall h1 h1' h2 h2',
\# h1 h1' ->
h2 = h1' \+ h2' ->
h1 \+ h2 = h1' \+ h1 \+ h2'.
Proof using.
intros. subst. rewrite <- state_union_assoc.
rewrite (@state_union_comm_disjoint h1 h1').
rewrite~ state_union_assoc. auto.
Qed.
Lemma state_union_eq_cancel_2' : forall h1 h1' h2,
\# h1 h1' ->
h2 = h1' ->
h1 \+ h2 = h1' \+ h1.
Proof using.
intros. subst. apply~ state_union_comm_disjoint.
Qed.
Lemma state_union_eq_cancel_3 : forall h1 h1' h2 h2' h3',
\# h1 (h1' \+ h2') ->
h2 = h1' \+ h2' \+ h3' ->
h1 \+ h2 = h1' \+ h2' \+ h1 \+ h3'.
Proof using.
intros. subst.
rewrite <- (@state_union_assoc h1' h2' h3').
rewrite <- (@state_union_assoc h1' h2' (h1 \+ h3')).
apply~ state_union_eq_cancel_2.
Qed.
Lemma state_union_eq_cancel_3' : forall h1 h1' h2 h2',
\# h1 (h1' \+ h2') ->
h2 = h1' \+ h2' ->
h1 \+ h2 = h1' \+ h2' \+ h1.
Proof using.
intros. subst.
rewrite <- (@state_union_assoc h1' h2' h1).
apply~ state_union_eq_cancel_2'.
Qed.
Lemma state_union_eq_cancel_4 : forall h1 h1' h2 h2' h3' h4',
\# h1 ((h1' \+ h2') \+ h3') ->
h2 = h1' \+ h2' \+ h3' \+ h4' ->
h1 \+ h2 = h1' \+ h2' \+ h3' \+ h1 \+ h4'.
Proof using.
intros. subst.
rewrite <- (@state_union_assoc h1' h2' (h3' \+ h4')).
rewrite <- (@state_union_assoc h1' h2' (h3' \+ h1 \+ h4')).
apply~ state_union_eq_cancel_3.
Qed.
Lemma state_union_eq_cancel_4' : forall h1 h1' h2 h2' h3',
\# h1 (h1' \+ h2' \+ h3') ->
h2 = h1' \+ h2' \+ h3' ->
h1 \+ h2 = h1' \+ h2' \+ h3' \+ h1.
Proof using.
intros. subst.
rewrite <- (@state_union_assoc h2' h3' h1).
apply~ state_union_eq_cancel_3'.
Qed.
Hint Rewrite
state_union_assoc
state_union_empty_l
state_union_empty_r : rew_state.
Tactic Notation "rew_state" :=
autorewrite with rew_state in *.
Ltac state_eq_step tt :=
match goal with | |- ?G => match G with
| ?h1 = ?h1 => apply state_union_eq_cancel_1'
| ?h1 \+ ?h2 = ?h1 \+ ?h2' => apply state_union_eq_cancel_1
| ?h1 \+ ?h2 = ?h1' \+ ?h1 => apply state_union_eq_cancel_2'
| ?h1 \+ ?h2 = ?h1' \+ ?h1 \+ ?h2' => apply state_union_eq_cancel_2
| ?h1 \+ ?h2 = ?h1' \+ ?h2' \+ ?h1 => apply state_union_eq_cancel_3'
| ?h1 \+ ?h2 = ?h1' \+ ?h2' \+ ?h1 \+ ?h3' => apply state_union_eq_cancel_3
| ?h1 \+ ?h2 = ?h1' \+ ?h2' \+ ?h3' \+ ?h1 => apply state_union_eq_cancel_4'
| ?h1 \+ ?h2 = ?h1' \+ ?h2' \+ ?h3' \+ ?h1 \+ ?h4' => apply state_union_eq_cancel_4
end end.
Tactic Notation "state_eq" :=
subst;
rew_state;
repeat (state_eq_step tt);
try state_disjoint_if_needed.
Lemma state_eq_demo : forall h1 h2 h3 h4 h5,
\# h1 h2 h3 ->
\# (h1 \+ h2 \+ h3) h4 h5 ->
h1 = h2 \+ h3 ->
h4 \+ h1 \+ h5 = h2 \+ h5 \+ h4 \+ h3.
Proof using.
intros. dup 2.
{ subst. rew_state.
state_eq_step tt. state_disjoint.
state_eq_step tt. state_disjoint.
state_eq_step tt. state_disjoint. auto. }
{ state_eq. }
Qed.
(************************************************************)
(* DEPRECATED *)
(** Auxiliary lemmas
Lemma state_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 (@state_union_comm h1 h2).
rewrite~ state_union_assoc. fequals.
rewrite~ state_union_comm. rew_disjoint*. rew_disjoint*.
rewrite~ state_union_comm_disjoint. rew_disjoint*. rew_disjoint*.
Qed.
Lemma state_union_comm_assoc' : forall h1 h2 h3,
......@@ -425,7 +620,7 @@ Lemma state_union_comm_assoc' : forall h1 h2 h3,
(h1 \+ h2) \+ h3 = h1 \+ (h3 \+ h2).
Proof using.
introv M. rewrite state_union_assoc. fequals.
rewrite~ state_union_comm. rew_disjoint*.
rewrite~ state_union_comm_disjoint. rew_disjoint*.
Qed.
Lemma state_union_comm_comm : forall h1 h2 h3,
......@@ -436,3 +631,39 @@ Proof using.
rewrite~ (@state_union_comm h3 (h2 \+ h1)).
rew_disjoint*. rew_disjoint*.
Qed.
*)
(*
Definition state_disjoint_4 h1 h2 h3 h4 :=
state_disjoint_3 h1 h2 h3 /\
state_disjoint_3 h1 h2 h4 /\
state_disjoint h4 h3.
*)
(*
Notation "\# h1 h2" := (heap_disjoint h1 h2)
(at level 40, h1 at level 0, h2 at level 0, no associativity) : heap_scope.
Notation "\# h1 h2 h3" := (heap_disjoint_3 h1 h2 h3)
(at level 40, h1 at level 0, h2 at level 0, h3 at level 0, no associativity) : heap_scope.
Notation "\# h1 h2 h3 h4" := (heap_disjoint_4 h1 h2 h3 h4)
(at level 40, h1 at level 0, h2 at level 0, h3 at level 0, h4 at level 0, no associativity) : heap_scope.
Notation "h1 \+ h2" := (state_union h1 h2)
(at level 51, right associativity) : heap_scope.
Open Scope heap_scope.
Bind Scope heap_scope with hprop.
Delimit Scope heap_scope with h.
*)
(*
Hint Resolve state_union_empty_l state_union_empty_r.
*)
\ No newline at end of file
This diff is collapsed.
This diff is collapsed.
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