diff options
| author | Timothy Bourke <tim@tbrk.org> | 2017-02-12 21:46:35 +0100 |
|---|---|---|
| committer | Lionel Rieg <lionel.rieg@univ-grenoble-alpes.fr> | 2020-04-21 01:08:58 +0200 |
| commit | d87ea150694745a1efee967285ee68845ac66f05 (patch) | |
| tree | fa7e6fc92df1c5e1dac2a1b2da74a10729d1497f | |
| parent | 4f6dcb643f804fb9736b65ce58b6e0ddc1a0ca1a (diff) | |
| download | compcert-kvx-d87ea150694745a1efee967285ee68845ac66f05.tar.gz compcert-kvx-d87ea150694745a1efee967285ee68845ac66f05.zip | |
Rewrites in disjoint_footprint
| -rw-r--r-- | common/Separation.v | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/common/Separation.v b/common/Separation.v index 0f40e65b..0aebb3c7 100644 --- a/common/Separation.v +++ b/common/Separation.v @@ -160,6 +160,21 @@ Proof. - intuition auto. Qed. +Add Morphism disjoint_footprint + with signature massert_eqv ==> massert_eqv ==> iff + as disjoint_footprint_morph_1. +Proof. + intros p q Hpq r s Hrs. + unfold disjoint_footprint. + split; intro HH; intros b ofs Hf1 Hf2. + - rewrite <-Hpq in Hf1. + rewrite <-Hrs in Hf2. + now specialize (HH _ _ Hf1 Hf2). + - rewrite Hpq in Hf1. + rewrite Hrs in Hf2. + now specialize (HH _ _ Hf1 Hf2). +Qed. + Add Morphism sepconj with signature massert_eqv ==> massert_eqv ==> massert_eqv as sepconj_morph_2. |