1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
|
Require Import Coq.omega.Omega Coq.ZArith.ZArith.
Local Open Scope Z_scope.
Module Z.
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
rename x into x'; intro x; intros; subst x';
clean_neg.
Ltac replace_all_neg_with_pos :=
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.
End Z.
|
