From f7734b2d0f4dffb46c50fa89985b926377ec5e96 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 9 Apr 2017 16:32:06 -0400 Subject: Make replace_with_neg more powerful --- src/Util/ZUtil.v | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'src/Util/ZUtil.v') diff --git a/src/Util/ZUtil.v b/src/Util/ZUtil.v index d905cc1f2..2f354ff1a 100644 --- a/src/Util/ZUtil.v +++ b/src/Util/ZUtil.v @@ -2693,6 +2693,8 @@ Module Z. repeat match goal with | [ H : (-?x) < 0 |- _ ] => assert (0 < x) by omega; clear H | [ H : 0 > (-?x) |- _ ] => assert (0 < x) by omega; clear H + | [ H : (-?x) <= 0 |- _ ] => assert (0 <= x) by omega; clear H + | [ H : 0 >= (-?x) |- _ ] => assert (0 <= x) by omega; clear H | [ H : -?x <= -?y |- _ ] => apply Z.opp_le_mono in H | [ |- -?x <= -?y ] => apply Z.opp_le_mono | _ => progress rewrite <- Z.opp_le_mono in * @@ -2713,6 +2715,8 @@ Module Z. repeat match goal with | [ H : ?x < 0 |- _ ] => replace_with_neg x | [ H : 0 > ?x |- _ ] => replace_with_neg x + | [ H : ?x <= 0 |- _ ] => replace_with_neg x + | [ H : 0 >= ?x |- _ ] => replace_with_neg x end. Lemma shiftl_le_Proper2 y -- cgit v1.2.3