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
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
|
Require Import Coq.ZArith.ZArith Coq.micromega.Lia.
Require Import Crypto.Util.ZUtil.Tactics.CompareToSgn.
Require Import Crypto.Util.ZUtil.Hints.Core.
Require Import Crypto.Util.ZUtil.Hints.ZArith.
Require Import Crypto.Util.ZUtil.Hints.PullPush.
Require Import Crypto.Util.ZUtil.ZSimplify.Core.
Local Open Scope Z_scope.
Module Z.
Lemma div_mul' : forall a b : Z, b <> 0 -> (b * a) / b = a.
Proof. intros. rewrite Z.mul_comm. apply Z.div_mul; auto. Qed.
Hint Rewrite div_mul' using zutil_arith : zsimplify.
Local Ltac replace_to_const c :=
repeat match goal with
| [ H : ?x = ?x |- _ ] => clear H
| [ H : ?x = c, H' : context[?x] |- _ ] => rewrite H in H'
| [ H : c = ?x, H' : context[?x] |- _ ] => rewrite <- H in H'
| [ H : ?x = c |- context[?x] ] => rewrite H
| [ H : c = ?x |- context[?x] ] => rewrite <- H
end.
Lemma lt_div_0 n m : n / m < 0 <-> ((n < 0 < m \/ m < 0 < n) /\ 0 < -(n / m)).
Proof.
Z.compare_to_sgn; rewrite Z.sgn_opp; simpl.
pose proof (Zdiv_sgn n m) as H.
pose proof (Z.sgn_spec (n / m)) as H'.
repeat first [ progress intuition auto
| progress simpl in *
| congruence
| lia
| progress replace_to_const (-1)
| progress replace_to_const 0
| progress replace_to_const 1
| match goal with
| [ x : Z |- _ ] => destruct x
end ].
Qed.
Lemma div_add' a b c : c <> 0 -> (a + c * b) / c = a / c + b.
Proof. intro; rewrite <- Z.div_add, (Z.mul_comm c); try lia. Qed.
Lemma div_add_l' a b c : b <> 0 -> (b * a + c) / b = a + c / b.
Proof. intro; rewrite <- Z.div_add_l, (Z.mul_comm b); lia. Qed.
Hint Rewrite div_add_l' div_add' using zutil_arith : zsimplify.
Lemma div_sub a b c : c <> 0 -> (a - b * c) / c = a / c - b.
Proof. intros; rewrite <- !Z.add_opp_r, <- Z.div_add by lia; apply f_equal2; lia. Qed.
Lemma div_sub' a b c : c <> 0 -> (a - c * b) / c = a / c - b.
Proof. intro; rewrite <- div_sub, (Z.mul_comm c); try lia. Qed.
Hint Rewrite div_sub div_sub' using zutil_arith : zsimplify.
Lemma div_add_sub_l a b c d : b <> 0 -> (a * b + c - d) / b = a + (c - d) / b.
Proof. rewrite <- Z.add_sub_assoc; apply Z.div_add_l. Qed.
Lemma div_add_sub_l' a b c d : b <> 0 -> (b * a + c - d) / b = a + (c - d) / b.
Proof. rewrite <- Z.add_sub_assoc; apply Z.div_add_l'. Qed.
Lemma div_add_sub a b c d : c <> 0 -> (a + b * c - d) / c = (a - d) / c + b.
Proof. rewrite (Z.add_comm _ (_ * _)), (Z.add_comm (_ / _)); apply Z.div_add_sub_l. Qed.
Lemma div_add_sub' a b c d : c <> 0 -> (a + c * b - d) / c = (a - d) / c + b.
Proof. rewrite (Z.add_comm _ (_ * _)), (Z.add_comm (_ / _)); apply Z.div_add_sub_l'. Qed.
Hint Rewrite Z.div_add_sub Z.div_add_sub' Z.div_add_sub_l Z.div_add_sub_l' using zutil_arith : zsimplify.
Lemma div_mul_skip a b k : 0 < b -> 0 < k -> a * b / k / b = a / k.
Proof.
intros; rewrite Z.div_div, (Z.mul_comm k), <- Z.div_div by lia.
autorewrite with zsimplify. reflexivity.
Qed.
Lemma div_mul_skip' a b k : 0 < b -> 0 < k -> b * a / k / b = a / k.
Proof.
intros; rewrite Z.div_div, (Z.mul_comm k), <- Z.div_div by lia.
autorewrite with zsimplify; reflexivity.
Qed.
Hint Rewrite Z.div_mul_skip Z.div_mul_skip' using zutil_arith : zsimplify.
Lemma div_mul_skip_pow base e0 e1 x y : 0 < y -> 0 < base -> 0 <= e1 <= e0 -> x * base^e0 / y / base^e1 = x * base^(e0 - e1) / y.
Proof.
intros.
assert (0 < base^e1) by auto with zarith.
replace (base^e0) with (base^(e0 - e1) * base^e1) by (autorewrite with pull_Zpow zsimplify; reflexivity).
rewrite !Z.mul_assoc.
autorewrite with zsimplify; lia.
Qed.
Hint Rewrite div_mul_skip_pow using zutil_arith : zsimplify.
Lemma div_mul_skip_pow' base e0 e1 x y : 0 < y -> 0 < base -> 0 <= e1 <= e0 -> base^e0 * x / y / base^e1 = base^(e0 - e1) * x / y.
Proof.
intros.
rewrite (Z.mul_comm (base^e0) x), div_mul_skip_pow by lia.
auto using f_equal2 with lia.
Qed.
Hint Rewrite div_mul_skip_pow' using zutil_arith : zsimplify.
Lemma div_le_mono_nonneg a b c : 0 <= c -> a <= b -> a / c <= b / c.
Proof.
destruct (Z_zerop c).
{ subst; simpl; autorewrite with zsimplify; reflexivity. }
{ intros; apply Z.div_le_mono; omega. }
Qed.
Hint Resolve div_le_mono_nonneg : zarith.
Lemma div_le_mono_pow_pos a b c e : a <= b -> a / Z.pos c ^ e <= b / Z.pos c ^ e.
Proof. auto with zarith. Qed.
Lemma div_nonneg a b : 0 <= a -> 0 <= b -> 0 <= a / b.
Proof.
destruct (Z_zerop b); subst; rewrite ?Zdiv_0_r; [ reflexivity | ].
intros; apply Z.div_pos; omega.
Qed.
Hint Resolve div_nonneg : zarith.
Lemma div_add_exact x y d : d <> 0 -> x mod d = 0 -> (x + y) / d = x / d + y / d.
Proof.
intros; rewrite (Z_div_exact_full_2 x d) at 1 by assumption.
rewrite Z.div_add_l' by assumption; lia.
Qed.
Hint Rewrite div_add_exact using zutil_arith : zsimplify.
Lemma Z_divide_div_mul_exact' a b c : b <> 0 -> (b | a) -> a * c / b = c * (a / b).
Proof. intros. rewrite Z.mul_comm. auto using Z.divide_div_mul_exact. Qed.
Lemma div_sub_mod_exact a b : b <> 0 -> a / b = (a - a mod b) / b.
Proof.
intro.
rewrite (Z.div_mod a b) at 2 by lia.
autorewrite with zsimplify.
reflexivity.
Qed.
Lemma div_sub_mod_cond x y d
: d <> 0
-> (x - y) / d
= x / d + ((x mod d - y) / d).
Proof. clear.
intro.
replace (x - y) with ((x - x mod d) + (x mod d - y)) by lia.
rewrite Z.div_add_exact by (autorewrite with pull_Zmod zsimplify; auto).
rewrite <- Z.div_sub_mod_exact by lia; lia.
Qed.
Hint Resolve div_sub_mod_cond : zarith.
Lemma div_add_mod_cond_l : forall x y d, d <> 0 -> (x + y) / d = (x mod d + y) / d + x / d.
Proof.
intros. replace (x + y) with ((x - x mod d) + (x mod d + y)) by lia.
rewrite Z.div_add_exact by (autorewrite with pull_Zmod zsimplify; auto).
rewrite <- Z.div_sub_mod_exact by lia; lia.
Qed.
Lemma div_add_mod_cond_r : forall x y d, d <> 0 -> (x + y) / d = (x + y mod d) / d + y / d.
Proof.
intros. rewrite Z.add_comm, div_add_mod_cond_l by auto. repeat (f_equal; try ring).
Qed.
End Z.
|
