More powerful replace_neg_with_pos

1 files changed, 40 insertions, 17 deletions

diff --git a/src/Util/ZUtil/Tactics/ReplaceNegWithPos.v b/src/Util/ZUtil/Tactics/ReplaceNegWithPos.v
index 67b5397aa..27c8fb244 100644
--- a/src/Util/ZUtil/Tactics/ReplaceNegWithPos.v
+++ b/src/Util/ZUtil/Tactics/ReplaceNegWithPos.v
@@ -2,23 +2,46 @@ Require Import Coq.omega.Omega Coq.ZArith.ZArith.
 Local Open Scope Z_scope.
 
 Module Z.
-  Ltac clean_neg :=
-    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 *
-           | [ H : 0 <= ?x, H' : 0 <= ?y, H'' : -?x <= ?y |- _ ] => clear H''
-           | [ H : 0 < ?x, H' : 0 <= ?y, H'' : -?x <= ?y |- _ ] => clear H''
-           | [ H : 0 <= ?x, H' : 0 < ?y, H'' : -?x <= ?y |- _ ] => clear H''
-           | [ H : 0 < ?x, H' : 0 < ?y, H'' : -?x <= ?y |- _ ] => clear H''
-           | [ H : 0 < ?x, H' : 0 <= ?y, H'' : -?x < ?y |- _ ] => clear H''
-           | [ H : 0 <= ?x, H' : 0 < ?y, H'' : -?x < ?y |- _ ] => clear H''
-           | [ H : 0 < ?x, H' : 0 < ?y, H'' : -?x < ?y |- _ ] => clear H''
-           end.
+  Lemma push_minus_add a b : -(-a + b) = a + -b. Proof. omega. Qed.
+
+  Ltac clean_neg_step _ :=
+    match goal with
+    | [ H : (-?x) < 0 |- _ ] => assert (0 < x) by omega; clear H
+    | [ H : 0 > (-?x) |- _ ] => assert (0 < x) by omega; clear H
+    | [ H : 0 <> -?x |- _ ] => assert (0 <> x) by omega; clear H
+    | [ H : -?x <> 0 |- _ ] => assert (x <> 0) 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 |- _ ] => rewrite <- Z.opp_le_mono in H
+    | [ |- -?x <= -?y ] => rewrite <- Z.opp_le_mono
+    | [ H : -?x < -?y |- _ ] => rewrite <- Z.opp_lt_mono in H
+    | [ |- -?x < -?y ] => rewrite <- Z.opp_lt_mono
+    | _ => progress rewrite <- Z.opp_le_mono in *
+    | [ H : context[_ * _] |- _ ]
+      => first [ rewrite !Z.mul_opp_opp in H
+               | rewrite !Z.mul_opp_l in H
+               | rewrite !Z.mul_opp_r in H ]
+    | [ |- context[_ * _] ]
+      => first [ rewrite !Z.mul_opp_opp
+               | rewrite !Z.mul_opp_l
+               | rewrite !Z.mul_opp_r ]
+    | [ H : context[- - _] |- _ ] => rewrite !Z.opp_involutive in H
+    | [ |- context[- - _] ] => rewrite !Z.opp_involutive
+    | [ H : context[-_ + -_] |- _ ] => rewrite <- !Z.opp_add_distr in H
+    | [ |- context[-_ + -_] ] => rewrite <- !Z.opp_add_distr
+    | [ H : context[-(-?a + ?b)] |- _ ] => rewrite !push_minus_add in H
+    | [ |- context[-(-?a + ?b)] ] => rewrite !push_minus_add
+    | [ H : 0 <= ?x, H' : 0 <= ?y, H'' : -?x <= ?y |- _ ] => clear H''
+    | [ H : 0 < ?x, H' : 0 <= ?y, H'' : -?x <= ?y |- _ ] => clear H''
+    | [ H : 0 <= ?x, H' : 0 < ?y, H'' : -?x <= ?y |- _ ] => clear H''
+    | [ H : 0 < ?x, H' : 0 < ?y, H'' : -?x <= ?y |- _ ] => clear H''
+    | [ H : 0 < ?x, H' : 0 <= ?y, H'' : -?x < ?y |- _ ] => clear H''
+    | [ H : 0 <= ?x, H' : 0 < ?y, H'' : -?x < ?y |- _ ] => clear H''
+    | [ H : 0 < ?x, H' : 0 < ?y, H'' : -?x < ?y |- _ ] => clear H''
+    | [ |- -_ = -_ ] => rewrite Z.opp_inj_wd
+    | [ H : -_ = -_ |- _ ] => rewrite Z.opp_inj_wd in H
+    end.
+  Ltac clean_neg := repeat clean_neg_step ().
   Ltac replace_with_neg x :=
     assert (x = -(-x)) by (symmetry; apply Z.opp_involutive); generalize dependent (-x);
     let x' := fresh in