diff options
Diffstat (limited to 'src/Util/ZUtil/Modulo/Bootstrap.v')
| -rw-r--r-- | src/Util/ZUtil/Modulo/Bootstrap.v | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/src/Util/ZUtil/Modulo/Bootstrap.v b/src/Util/ZUtil/Modulo/Bootstrap.v new file mode 100644 index 000000000..668aaa331 --- /dev/null +++ b/src/Util/ZUtil/Modulo/Bootstrap.v @@ -0,0 +1,22 @@ +(** Basic lemmas about [Z.modulo] for bootstrapping various tactics *) +Require Import Coq.ZArith.ZArith. +Require Import Coq.micromega.Lia. +Require Import Crypto.Util.ZUtil.Hints.Core. +Local Open Scope Z_scope. + +Module Z. + Lemma mod_0_r_eq a b : b = 0 -> a mod b = 0. + Proof. intro; subst; auto with zarith. Qed. + Hint Resolve mod_0_r_eq : zarith. + Hint Rewrite mod_0_r_eq using assumption : zsimplify. + + Lemma div_mod_cases x y : ((x = y * (x / y) + x mod y /\ (y < x mod y <= 0 \/ 0 <= x mod y < y)) + \/ (y = 0 /\ x / y = 0 /\ x mod y = 0)). + Proof. + destruct (Z_zerop y); [ right; subst; auto with zarith | left ]; subst. + split; [ apply Z.div_mod; assumption | ]. + destruct (Z_dec' y 0) as [ [H|H] | H]; [ left | right | congruence ]. + { apply Z.mod_neg_bound; assumption. } + { apply Z.mod_pos_bound; assumption. } + Qed. +End Z. |