From fab2ae5293e09dbb38c796002794cb3ca7d37eba Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Besson?= Date: Tue, 29 Oct 2019 11:54:43 +0100 Subject: [PATCH] More robust proof of `size_and` The proposed proof only uses `zify` for closing the goal. This is needed for PR #10982 which changes the inner working of `zify`. --- lib/Integers.v | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/lib/Integers.v b/lib/Integers.v index 3b6c35ebc2..8990c78d47 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: