blob: a52798d200f85f1a096f0c6ae59398d15c09d4cb (
plain)
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
|
Require Import Coq.ZArith.ZArith.
Require Import Crypto.Util.ZUtil.Div.Bootstrap.
Require Import Crypto.Util.ZUtil.Modulo.Bootstrap.
Require Import Crypto.Util.ZUtil.Hints.Core.
Local Open Scope Z_scope.
Module Z.
(** [div_mod_to_quot_rem] replaces [x / y] and [x mod y] with new
variables [q] and [r] while simultaneously adding facts that
uniquely specify [q] and [r] to the context (roughly, that [y *
q + r = x] and that [0 <= r < y]. *)
Ltac div_mod_to_quot_rem_inequality_solver :=
zutil_arith_more_inequalities.
Ltac generalize_div_eucl x y :=
let H := fresh in
let H' := fresh in
first
[ assert (H' : y <> 0) by div_mod_to_quot_rem_inequality_solver;
generalize (Z.div_mod x y H'); clear H';
first [ assert (H' : 0 < y) by div_mod_to_quot_rem_inequality_solver;
generalize (Z.mod_pos_bound x y H'); clear H'
| assert (H' : y < 0) by div_mod_to_quot_rem_inequality_solver;
generalize (Z.mod_neg_bound x y H'); clear H'
| assert (H' : y = 0) by div_mod_to_quot_rem_inequality_solver;
generalize (Z.div_0_r_eq x y H') (Z.mod_0_r_eq x y H'); clear H'
| assert (H' : y < 0 \/ 0 < y) by (apply Z.neg_pos_cases; div_mod_to_quot_rem_inequality_solver);
let H'' := fresh in
assert (H'' : y < x mod y <= 0 \/ 0 <= x mod y < y)
by (destruct H'; [ left; apply Z.mod_neg_bound; assumption
| right; apply Z.mod_pos_bound; assumption ]);
clear H'; revert H'' ]
| generalize (Z.div_mod_cases x y) ];
let q := fresh "q" in
let r := fresh "r" in
set (q := x / y) in *;
set (r := x mod y) in *;
clearbody q r.
Ltac div_mod_to_quot_rem_step :=
match goal with
| [ |- context[?x / ?y] ] => generalize_div_eucl x y
| [ |- context[?x mod ?y] ] => generalize_div_eucl x y
end.
Ltac div_mod_to_quot_rem_hyps_step :=
match goal with
| [ H : context[?x / ?y] |- _ ] => generalize_div_eucl x y
| [ H : context[?x mod ?y] |- _ ] => generalize_div_eucl x y
end.
Ltac div_mod_to_quot_rem := repeat first [ div_mod_to_quot_rem_step | div_mod_to_quot_rem_hyps_step ]; intros.
Ltac div_mod_to_quot_rem_in_goal := repeat div_mod_to_quot_rem_step; intros.
End Z.
|
