blob: 1b824a2c6b6c54ce5f5509a97ee6398faadc40fd (
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
|
Require Import Coq.ZArith.ZArith.
Require Import Coq.micromega.Lia.
Require Import Crypto.Util.ZUtil.Definitions.
Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
Require Import Crypto.Util.Tactics.BreakMatch.
Local Open Scope Z_scope.
Module Z.
Lemma mul_split_at_bitwidth_mod bw x y : fst (Z.mul_split_at_bitwidth bw x y) = (x * y) mod 2^bw.
Proof.
unfold Z.mul_split_at_bitwidth, LetIn.Let_In; break_innermost_match; Z.ltb_to_lt; try reflexivity;
apply Z.land_ones; lia.
Qed.
Lemma mul_split_at_bitwidth_div bw x y : snd (Z.mul_split_at_bitwidth bw x y) = (x * y) / 2^bw.
Proof.
unfold Z.mul_split_at_bitwidth, LetIn.Let_In; break_innermost_match; Z.ltb_to_lt; try reflexivity;
apply Z.shiftr_div_pow2; lia.
Qed.
Lemma mul_split_mod s x y : fst (Z.mul_split s x y) = (x * y) mod s.
Proof.
unfold Z.mul_split; break_match; Z.ltb_to_lt;
[ rewrite mul_split_at_bitwidth_mod; congruence | reflexivity ].
Qed.
Hint Rewrite mul_split_mod : to_div_mod.
Lemma mul_split_div s x y : snd (Z.mul_split s x y) = (x * y) / s.
Proof.
unfold Z.mul_split; break_match; Z.ltb_to_lt;
[ rewrite mul_split_at_bitwidth_div; congruence | reflexivity ].
Qed.
Hint Rewrite mul_split_div : to_div_mod.
End Z.
|
