diff options
author | Jason Gross <jagro@google.com> | 2016-07-21 13:51:35 -0700 |
---|---|---|
committer | Jason Gross <jagro@google.com> | 2016-07-21 13:51:35 -0700 |
commit | 002b5e36e5e3fdeb62deec7eea0a8b05c217c8ba (patch) | |
tree | f899cbf1376ee88177e6d80e911d999ec60b2cec | |
parent | f4e35faa34145ab24aad021025b7d0d6e7f2214c (diff) |
Fix broken proofs
-rw-r--r-- | src/Util/ZUtil.v | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index d0aa12e58..00e227e2d 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -990,16 +990,17 @@ Module Z. intro H; rewrite <- (Z.opp_involutive x). rewrite Z.div_opp_l_complete by lia. generalize dependent (-x); clear x; intros x H. - autorewrite with zsimplify; break_match; lia. + autorewrite with zsimplify; edestruct Z_zerop; lia. Qed. Hint Rewrite div_small_neg using lia : zsimplify. Lemma div_sub_small x y z : 0 <= x < z -> 0 <= y < z -> (x - y) / z = if x <? y then -1 else 0. Proof. pose proof (Zlt_cases x y). - intros; break_match; autorewrite with zsimplify; lia. + (destruct (x <? y) eqn:?); + intros; autorewrite with zsimplify; lia. Qed. - Hint Rewrite div_small_neg using lia : zsimplify. + Hint Rewrite div_sub_small using lia : zsimplify. End Z. Module Export BoundsTactics. |