diff options
| author | Timothy Bourke <tim@tbrk.org> | 2016-07-05 13:26:42 +0200 |
|---|---|---|
| committer | Lionel Rieg <lionel.rieg@univ-grenoble-alpes.fr> | 2020-04-21 01:08:58 +0200 |
| commit | 4bda31427187fce0468004738a214830191ccda5 (patch) | |
| tree | d046ca1d6ae2f90f119214accbabd0730a327ced | |
| parent | f8da0614e106a324fa6646213db68f2045070af4 (diff) | |
| download | compcert-kvx-4bda31427187fce0468004738a214830191ccda5.tar.gz compcert-kvx-4bda31427187fce0468004738a214830191ccda5.zip | |
More rewriting for Separation
| -rw-r--r-- | common/Separation.v | 48 |
1 files changed, 34 insertions, 14 deletions
diff --git a/common/Separation.v b/common/Separation.v index 2804fd73..9aee633f 100644 --- a/common/Separation.v +++ b/common/Separation.v @@ -113,6 +113,18 @@ Proof. intros P Q [[A B] [C D]]. split; auto. Qed. +Instance massert_imp_eqv_Proper: + Proper (massert_eqv ==> massert_eqv ==> iff) massert_imp. +Proof. + intros p q Hpq r s Hrs. + split; destruct 1 as [HR1 HR2]; + constructor; intros; + apply Hrs || apply Hpq; + apply HR1 || apply HR2; + apply Hpq || apply Hrs; + assumption. +Qed. + Hint Resolve massert_imp_refl massert_eqv_refl : core. Instance footprint_massert_imp_Proper: @@ -193,6 +205,15 @@ Proof. intros. rewrite <- H0, <- H1; auto. Qed. +Lemma sep_imp': + forall P P' Q Q', + massert_imp P P' -> + massert_imp Q Q' -> + massert_imp (P ** Q) (P' ** Q'). +Proof. + intros * HP HQ. rewrite HP, HQ. reflexivity. +Qed. + Lemma sep_comm_1: forall P Q, massert_imp (P ** Q) (Q ** P). Proof. @@ -272,15 +293,17 @@ Proof. Qed. Lemma sep_drop: - forall P Q m, m |= P ** Q -> m |= Q. + forall P Q, massert_imp (P ** Q) Q. Proof. - simpl; intros. tauto. + constructor. + - simpl; intros. tauto. + - intros. now constructor 2. Qed. Lemma sep_drop2: - forall P Q R m, m |= P ** Q ** R -> m |= P ** R. + forall P Q R, massert_imp (P ** Q ** R) (P ** R). Proof. - intros. rewrite sep_swap in H. eapply sep_drop; eauto. + intros. rewrite sep_swap, sep_drop. reflexivity. Qed. Lemma sep_proj1: @@ -291,7 +314,9 @@ Qed. Lemma sep_proj2: forall P Q m, m |= P ** Q -> m |= Q. -Proof sep_drop. +Proof. + apply sep_drop. +Qed. Definition sep_pick1 := sep_proj1. @@ -458,15 +483,10 @@ Lemma range_split: m |= range' p b lo hi ** P -> m |= range' p b lo mid ** range' p b mid hi ** P. Proof. - intros. rewrite <- sep_assoc. eapply sep_imp; eauto. - split; simpl; intros. -- intuition auto. -+ omega. -+ apply H5; omega. -+ omega. -+ apply H5; omega. -+ red; simpl; intros; omega. -- intuition omega. + intros. + rewrite <-sep_assoc. + rewrite range_split' with (1:=H) in H0. + assumption. Qed. Lemma range_drop_left: |