blob: 06ce2187b4e6f26044f7ed3dd0a2ba83ea6a864e (
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
|
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 base_pow_neg b n : n < 0 -> b^n = 0.
Proof.
destruct n; intro H; try reflexivity; compute in H; congruence.
Qed.
Hint Rewrite base_pow_neg using zutil_arith : zsimplify.
Lemma nonneg_pow_pos a b : 0 < a -> 0 < a^b -> 0 <= b.
Proof.
destruct (Z_lt_le_dec b 0); intros; auto.
erewrite Z.pow_neg_r in * by eassumption.
omega.
Qed.
Hint Resolve nonneg_pow_pos (fun n => nonneg_pow_pos 2 n Z.lt_0_2) : zarith.
Lemma nonneg_pow_pos_helper a b dummy : 0 < a -> 0 <= dummy < a^b -> 0 <= b.
Proof. eauto with zarith omega. Qed.
Hint Resolve nonneg_pow_pos_helper (fun n dummy => nonneg_pow_pos_helper 2 n dummy Z.lt_0_2) : zarith.
Lemma div_pow2succ : forall n x, (0 <= x) ->
n / 2 ^ Z.succ x = Z.div2 (n / 2 ^ x).
Proof.
intros.
rewrite Z.pow_succ_r, Z.mul_comm by auto.
rewrite <- Z.div_div by (try apply Z.pow_nonzero; omega).
rewrite Zdiv2_div.
reflexivity.
Qed.
Definition pow_sub_r'
:= fun a b c y H0 H1 => @Logic.eq_trans _ _ _ y (@Z.pow_sub_r a b c H0 H1).
Definition pow_sub_r'_sym
:= fun a b c y p H0 H1 => Logic.eq_sym (@Logic.eq_trans _ y _ _ (Logic.eq_sym p) (@Z.pow_sub_r a b c H0 H1)).
Hint Resolve pow_sub_r' pow_sub_r'_sym Z.eq_le_incl : zarith.
Hint Resolve (fun b => f_equal (fun e => b ^ e)) (fun e => f_equal (fun b => b ^ e)) : zarith.
Lemma two_p_two_eq_four : 2^(2) = 4.
Proof. reflexivity. Qed.
Hint Rewrite <- two_p_two_eq_four : push_Zpow.
End Z.
|
