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
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
|
Require Coq.Logic.Eqdep_dec.
Require Import Coq.Numbers.Natural.Peano.NPeano Coq.omega.Omega.
Require Import Coq.micromega.Psatz.
Import Nat.
Create HintDb natsimplify discriminated.
Hint Resolve mod_bound_pos plus_le_compat : arith.
Hint Resolve (fun x y p q => proj1 (@Nat.mod_bound_pos x y p q)) (fun x y p q => proj2 (@Nat.mod_bound_pos x y p q)) : arith.
Hint Rewrite @mod_small @mod_mod @mod_1_l @mod_1_r succ_pred using omega : natsimplify.
Local Open Scope nat_scope.
Lemma min_def {x y} : min x y = x - (x - y).
Proof. apply Min.min_case_strong; omega. Qed.
Lemma max_def {x y} : max x y = x + (y - x).
Proof. apply Max.max_case_strong; omega. Qed.
Ltac coq_omega := omega.
Ltac handle_min_max_for_omega_gen min max :=
repeat match goal with
| [ H : context[min _ _] |- _ ] => rewrite !min_def in H || setoid_rewrite min_def in H
| [ H : context[max _ _] |- _ ] => rewrite !max_def in H || setoid_rewrite max_def in H
| [ |- context[min _ _] ] => rewrite !min_def || setoid_rewrite min_def
| [ |- context[max _ _] ] => rewrite !max_def || setoid_rewrite max_def
end.
Ltac handle_min_max_for_omega_case_gen min max :=
repeat match goal with
| [ H : context[min _ _] |- _ ] => revert H
| [ H : context[max _ _] |- _ ] => revert H
| [ |- context[min _ _] ] => apply Min.min_case_strong
| [ |- context[max _ _] ] => apply Max.max_case_strong
end;
intros.
Ltac handle_min_max_for_omega := handle_min_max_for_omega_gen min max.
Ltac handle_min_max_for_omega_case := handle_min_max_for_omega_case_gen min max.
(* In 8.4, Nat.min is a definition, so we need to unfold it *)
Ltac handle_min_max_for_omega_compat_84 :=
let min := (eval cbv [min] in min) in
let max := (eval cbv [max] in max) in
handle_min_max_for_omega_gen min max.
Ltac handle_min_max_for_omega_case_compat_84 :=
let min := (eval cbv [min] in min) in
let max := (eval cbv [max] in max) in
handle_min_max_for_omega_case_gen min max.
Ltac omega_with_min_max :=
handle_min_max_for_omega;
try handle_min_max_for_omega_compat_84;
omega.
Ltac omega_with_min_max_case :=
handle_min_max_for_omega_case;
try handle_min_max_for_omega_case_compat_84;
omega.
Tactic Notation "omega" := coq_omega.
Tactic Notation "omega" "*" := omega_with_min_max_case.
Tactic Notation "omega" "**" := omega_with_min_max.
Lemma div_minus : forall a b, b <> 0 -> (a + b) / b = a / b + 1.
Proof.
intros.
assert (b = 1 * b) by omega.
rewrite H0 at 1.
rewrite <- Nat.div_add by auto.
reflexivity.
Qed.
Lemma pred_mod : forall m, (0 < m)%nat -> ((pred m) mod m)%nat = pred m.
Proof.
intros; apply Nat.mod_small.
destruct m; try omega; rewrite Nat.pred_succ; auto.
Qed.
Lemma div_add_l' : forall a b c, a <> 0 -> (a * b + c) / a = b + c / a.
Proof.
intros; rewrite Nat.mul_comm; auto using div_add_l.
Qed.
Lemma mod_add_l : forall a b c, b <> 0 -> (a * b + c) mod b = c mod b.
Proof.
intros; rewrite Nat.add_comm; auto using mod_add.
Qed.
Lemma mod_add_l' : forall a b c, b <> 0 -> (b * a + c) mod b = c mod b.
Proof.
intros; rewrite Nat.mul_comm; auto using mod_add_l.
Qed.
Lemma mod_div_eq0 : forall a b, b <> 0 -> a mod b / b = 0.
Proof.
intros; apply Nat.div_small, mod_bound_pos; omega.
Qed.
Lemma divide2_1mod4_nat : forall c x, c = x / 4 -> x mod 4 = 1 -> exists y, 2 * y = (x / 2).
Proof.
assert (4 <> 0) as ne40 by omega.
induction c; intros; pose proof (div_mod x 4 ne40); rewrite <- H in H1. {
rewrite H0 in H1.
simpl in H1.
rewrite H1.
exists 0; auto.
} {
rewrite mult_succ_r in H1.
assert (4 <= x) as le4x by (apply Nat.div_str_pos_iff; omega).
rewrite <- Nat.add_1_r in H.
replace x with ((x - 4) + 4) in H by omega.
rewrite div_minus in H by auto.
apply Nat.add_cancel_r in H.
replace x with ((x - 4) + (1 * 4)) in H0 by omega.
rewrite Nat.mod_add in H0 by auto.
pose proof (IHc _ H H0).
destruct H2.
exists (x0 + 1).
rewrite <- (Nat.sub_add 4 x) in H1 at 1 by auto.
replace (4 * c + 4 + x mod 4) with (4 * c + x mod 4 + 4) in H1 by omega.
apply Nat.add_cancel_r in H1.
replace (2 * (x0 + 1)) with (2 * x0 + 2)
by (rewrite Nat.mul_add_distr_l; auto).
rewrite H2.
rewrite <- Nat.div_add by omega.
f_equal.
simpl.
apply Nat.sub_add; auto.
}
Qed.
Lemma Nat2N_inj_lt : forall n m, (N.of_nat n < N.of_nat m)%N <-> n < m.
Proof.
split; intros. {
rewrite nat_compare_lt.
rewrite Nnat.Nat2N.inj_compare.
rewrite N.compare_lt_iff; auto.
} {
rewrite <- N.compare_lt_iff.
rewrite <- Nnat.Nat2N.inj_compare.
rewrite <- nat_compare_lt; auto.
}
Qed.
Lemma lt_min_l : forall x a b, (x < min a b)%nat -> (x < a)%nat.
Proof.
intros ? ? ? lt_min.
apply Nat.min_glb_lt_iff in lt_min.
destruct lt_min; assumption.
Qed.
(* useful for hints *)
Lemma eq_le_incl_rev : forall a b, a = b -> b <= a.
Proof.
intros; omega.
Qed.
Lemma beq_nat_eq_nat_dec {R} (x y : nat) (a b : R)
: (if EqNat.beq_nat x y then a else b) = (if eq_nat_dec x y then a else b).
Proof.
destruct (eq_nat_dec x y) as [H|H];
[ rewrite (proj2 (@beq_nat_true_iff _ _) H); reflexivity
| rewrite (proj2 (@beq_nat_false_iff _ _) H); reflexivity ].
Qed.
Lemma pow_nonzero a k : a <> 0 -> a ^ k <> 0.
Proof.
intro; induction k; simpl; nia.
Qed.
Hint Resolve pow_nonzero : arith.
Lemma S_pred_nonzero : forall a, (a > 0 -> S (pred a) = a)%nat.
Proof.
destruct a; simpl; omega.
Qed.
Hint Rewrite S_pred_nonzero using omega : natsimplify.
Lemma mod_same_eq a b : a <> 0 -> a = b -> b mod a = 0.
Proof. intros; subst; apply mod_same; assumption. Qed.
Hint Rewrite @mod_same_eq using omega : natsimplify.
Hint Resolve mod_same_eq : arith.
Lemma mod_mod_eq a b c : a <> 0 -> b = c mod a -> b mod a = b.
Proof. intros; subst; autorewrite with natsimplify; reflexivity. Qed.
Hint Rewrite @mod_mod_eq using (reflexivity || omega) : natsimplify.
Local Arguments minus !_ !_.
Lemma S_mod_full a b : a <> 0 -> (S b) mod a = if eq_nat_dec (S (b mod a)) a
then 0
else S (b mod a).
Proof.
change (S b) with (1+b); intros.
pose proof (mod_bound_pos b a).
rewrite add_mod by assumption.
destruct (eq_nat_dec (S (b mod a)) a) as [H'|H'];
destruct a as [|[|a]]; autorewrite with natsimplify in *;
try congruence; try reflexivity.
Qed.
Hint Rewrite S_mod_full using omega : natsimplify.
Lemma S_mod a b : a <> 0 -> S (b mod a) <> a -> (S b) mod a = S (b mod a).
Proof.
intros; rewrite S_mod_full by assumption.
edestruct eq_nat_dec; omega.
Qed.
Hint Rewrite S_mod using (omega || autorewrite with natsimplify; omega) : natsimplify.
Lemma eq_nat_dec_refl x : eq_nat_dec x x = left (Logic.eq_refl x).
Proof.
edestruct eq_nat_dec; try congruence.
apply f_equal, Eqdep_dec.UIP_dec, eq_nat_dec.
Qed.
Hint Rewrite eq_nat_dec_refl : natsimplify.
(** Helper to get around the lack of function extensionality *)
Definition eq_nat_dec_right_val n m (pf0 : n <> m) : { pf | eq_nat_dec n m = right pf }.
Proof.
revert dependent n; induction m; destruct n as [|n]; simpl;
intro pf0;
[ (exists pf0; exfalso; abstract congruence)
| eexists; reflexivity
| eexists; reflexivity
| ].
{ specialize (IHm n).
destruct IHm as [? IHm]; [ omega | ].
eexists; rewrite IHm; reflexivity. }
Qed.
Lemma eq_nat_dec_S_n n : eq_nat_dec (S n) n = right (proj1_sig (@eq_nat_dec_right_val _ _ (@neq_succ_diag_l n))).
Proof.
edestruct eq_nat_dec_right_val; assumption.
Qed.
Hint Rewrite eq_nat_dec_S_n : natsimplify.
Lemma eq_nat_dec_n_S n : eq_nat_dec n (S n) = right (proj1_sig (@eq_nat_dec_right_val _ _ (n_Sn n))).
Proof.
edestruct eq_nat_dec_right_val; assumption.
Qed.
Hint Rewrite eq_nat_dec_n_S : natsimplify.
Hint Rewrite Max.max_0_l Max.max_0_r Max.max_idempotent Min.min_0_l Min.min_0_r Min.min_idempotent : natsimplify.
(** Helper to get around the lack of function extensionality *)
Definition le_dec_right_val n m (pf0 : ~n <= m) : { pf | le_dec n m = right pf }.
Proof.
destruct (le_dec n m) eqn:Heq; [ | eexists; reflexivity ].
exfalso; clear Heq; apply pf0; assumption.
Qed.
(** Helper to get around the lack of function extensionality *)
Definition lt_dec_right_val n m (pf0 : ~n < m) : { pf | lt_dec n m = right pf }
:= @le_dec_right_val _ _ pf0.
Lemma lt_dec_irrefl n : lt_dec n n = right (proj1_sig (@lt_dec_right_val _ _ (lt_irrefl n))).
Proof. edestruct lt_dec_right_val; assumption. Qed.
Hint Rewrite lt_dec_irrefl : natsimplify.
Lemma not_lt_n_pred_n n : ~n < pred n.
Proof. destruct n; simpl; omega. Qed.
Lemma lt_dec_n_pred_n n : lt_dec n (pred n) = right (proj1_sig (@lt_dec_right_val _ _ (not_lt_n_pred_n n))).
Proof. edestruct lt_dec_right_val; assumption. Qed.
Hint Rewrite lt_dec_n_pred_n : natsimplify.
Lemma le_dec_refl n : le_dec n n = left (le_refl n).
Proof.
edestruct le_dec; try omega.
apply f_equal, le_unique.
Qed.
Hint Rewrite le_dec_refl : natsimplify.
Lemma le_dec_pred_l n : le_dec (pred n) n = left (le_pred_l n).
Proof.
edestruct le_dec; [ | destruct n; simpl in *; omega ].
apply f_equal, le_unique.
Qed.
Hint Rewrite le_dec_pred_l : natsimplify.
Lemma le_pred_plus_same n : n <= pred (n + n).
Proof. destruct n; simpl; omega. Qed.
Lemma le_dec_pred_plus_same n : le_dec n (pred (n + n)) = left (le_pred_plus_same n).
Proof.
edestruct le_dec; [ | destruct n; simpl in *; omega ].
apply f_equal, le_unique.
Qed.
Hint Rewrite le_dec_pred_plus_same : natsimplify.
|
