diff options
| author | Frédéric Besson <frederic.besson@inria.fr> | 2019-10-30 09:38:01 +0100 |
|---|---|---|
| committer | Xavier Leroy <xavierleroy@users.noreply.github.com> | 2019-10-30 09:38:01 +0100 |
| commit | a0844a9b6eb88f9e75f7305e8d1505cf502fb81a (patch) | |
| tree | 3e41306b371d2fcab33a6bf6fa057d139f81e026 /lib/Integers.v | |
| parent | 1c1a4d86a22dd04fc92e61d4bd5c35e047c8b772 (diff) | |
| download | compcert-kvx-a0844a9b6eb88f9e75f7305e8d1505cf502fb81a.tar.gz compcert-kvx-a0844a9b6eb88f9e75f7305e8d1505cf502fb81a.zip | |
More robust proof of `size_and` (#320)
The proposed proof only uses `zify` for closing the goal. This is
needed for Coq PR #10982 which changes the inner working of `zify`.
Diffstat (limited to 'lib/Integers.v')
| -rw-r--r-- | lib/Integers.v | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/lib/Integers.v b/lib/Integers.v index 3b6c35eb..8990c78d 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -3322,10 +3322,11 @@ Proof. assert (0 <= Z.min (size a) (size b)). generalize (size_range a) (size_range b). zify; omega. apply bits_size_3. auto. intros. - rewrite bits_and. zify. subst z z0. destruct H1. - rewrite (bits_size_2 a). auto. omega. - rewrite (bits_size_2 b). apply andb_false_r. omega. - omega. + rewrite bits_and by omega. + rewrite andb_false_iff. + generalize (bits_size_2 a i). + generalize (bits_size_2 b i). + zify; intuition. Qed. Corollary and_interval: |