blob: 75d27dcafe5781f335551898516314890e5f2d77 (
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
|
Require Import Coq.ZArith.ZArith Coq.micromega.Lia.
Local Open Scope Z_scope.
Module Z2Nat.
Definition inj_nonpos n : n <= 0 -> Z.to_nat n = 0%nat.
Proof.
destruct n; try reflexivity; lia.
Qed.
End Z2Nat.
Module Z.
Lemma pos_pow_nat_pos : forall x n,
Z.pos x ^ Z.of_nat n > 0.
Proof. intros; apply Z.lt_gt, Z.pow_pos_nonneg; lia. Qed.
Lemma pow_Z2N_Zpow : forall a n, 0 <= a ->
((Z.to_nat a) ^ n = Z.to_nat (a ^ Z.of_nat n)%Z)%nat.
Proof.
intros a n H; induction n as [|n IHn]; try reflexivity.
rewrite Nat2Z.inj_succ.
rewrite Nat.pow_succ_r by apply le_0_n.
rewrite Z.pow_succ_r by apply Zle_0_nat.
rewrite IHn.
rewrite Z2Nat.inj_mul; auto using Z.pow_nonneg.
Qed.
Lemma pow_Zpow : forall a n : nat, Z.of_nat (a ^ n) = Z.of_nat a ^ Z.of_nat n.
Proof with auto using Zle_0_nat, Z.pow_nonneg.
intros; apply Z2Nat.inj...
rewrite <- pow_Z2N_Zpow, !Nat2Z.id...
Qed.
Hint Rewrite pow_Zpow : push_Zof_nat.
Hint Rewrite <- pow_Zpow : pull_Zof_nat.
Lemma Zpow_sub_1_nat_pow a v
: (Z.pos a^Z.of_nat v - 1 = Z.of_nat (Z.to_nat (Z.pos a)^v - 1))%Z.
Proof.
rewrite <- (Z2Nat.id (Z.pos a)) at 1 by lia.
change 2%Z with (Z.of_nat 2); change 1%Z with (Z.of_nat 1);
autorewrite with pull_Zof_nat.
rewrite Nat2Z.inj_sub
by (change 1%nat with (Z.to_nat (Z.pos a)^0)%nat; apply Nat.pow_le_mono_r; simpl; lia).
reflexivity.
Qed.
Hint Rewrite Zpow_sub_1_nat_pow : pull_Zof_nat.
Hint Rewrite <- Zpow_sub_1_nat_pow : push_Zof_nat.
End Z.
|
