Library Coq.ZArith.Zpow_facts



Require Import ZArith_base.
Require Import ZArithRing.
Require Import Zcomplements.
Require Export Zpower.
Require Import Zdiv.
Require Import Znumtheory.
Open Local Scope Z_scope.

Lemma Zpower_pos_1_r: forall x, Zpower_pos x 1 = x.

Lemma Zpower_pos_1_l: forall p, Zpower_pos 1 p = 1.

Lemma Zpower_pos_0_l: forall p, Zpower_pos 0 p = 0.

Lemma Zpower_pos_pos: forall x p,
  0 < x -> 0 < Zpower_pos x p.

Theorem Zpower_1_r: forall z, z^1 = z.

Theorem Zpower_1_l: forall z, 0 <= z -> 1^z = 1.

Theorem Zpower_0_l: forall z, z<>0 -> 0^z = 0.

Theorem Zpower_0_r: forall z, z^0 = 1.

Theorem Zpower_2: forall z, z^2 = z * z.

Theorem Zpower_gt_0: forall x y,
  0 < x -> 0 <= y -> 0 < x^y.

Theorem Zpower_Zabs: forall a b, Zabs (a^b) = (Zabs a)^b.

Theorem Zpower_Zsucc: forall p n, 0 <= n -> p^(Zsucc n) = p * p^n.

Theorem Zpower_mult: forall p q r, 0 <= q -> 0 <= r -> p^(q*r) = (p^q)^r.

Theorem Zpower_le_monotone: forall a b c,
 0 < a -> 0 <= b <= c -> a^b <= a^c.

Theorem Zpower_lt_monotone: forall a b c,
 1 < a -> 0 <= b < c -> a^b < a^c.

Theorem Zpower_gt_1 : forall x y,
  1 < x -> 0 < y -> 1 < x^y.

Theorem Zpower_ge_0: forall x y, 0 <= x -> 0 <= x^y.

Theorem Zpower_le_monotone2:
   forall a b c, 0 < a -> b <= c -> a^b <= a^c.

Theorem Zmult_power: forall p q r, 0 <= r ->
  (p*q)^r = p^r * q^r.

Hint Resolve Zpower_ge_0 Zpower_gt_0: zarith.

Theorem Zpower_le_monotone3: forall a b c,
 0 <= c -> 0 <= a <= b -> a^c <= b^c.

Lemma Zpower_le_monotone_inv: forall a b c,
  1 < a -> 0 < b -> a^b <= a^c -> b <= c.

Theorem Zpower_nat_Zpower: forall p q, 0 <= q ->
 p^q = Zpower_nat p (Zabs_nat q).

Theorem Zpower2_lt_lin: forall n, 0 <= n -> n < 2^n.

Theorem Zpower2_le_lin: forall n, 0 <= n -> n <= 2^n.

Lemma Zpower2_Psize :
  forall n p, Zpos p < 2^(Z_of_nat n) <-> (Psize p <= n)%nat.

Zpower and modulo


Theorem Zpower_mod: forall p q n, 0 < n ->
 (p^q) mod n = ((p mod n)^q) mod n.

A direct way to compute Zpower modulo

Fixpoint Zpow_mod_pos (a: Z)(m: positive)(n : Z) {struct m} : Z :=
  match m with
   | xH => a mod n
   | xO m' =>
      let z := Zpow_mod_pos a m' n in
      match z with
       | 0 => 0
       | _ => (z * z) mod n
      end
   | xI m' =>
      let z := Zpow_mod_pos a m' n in
      match z with
       | 0 => 0
       | _ => (z * z * a) mod n
      end
  end.

Definition Zpow_mod a m n :=
  match m with
   | 0 => 1
   | Zpos p => Zpow_mod_pos a p n
   | Zneg p => 0
  end.

Theorem Zpow_mod_pos_correct: forall a m n, 0 < n ->
 Zpow_mod_pos a m n = (Zpower_pos a m) mod n.

Theorem Zpow_mod_correct: forall a m n, 1 < n -> 0 <= m ->
 Zpow_mod a m n = (a ^ m) mod n.


Lemma Zpower_divide: forall p q, 0 < q -> (p | p ^ q).

Theorem rel_prime_Zpower_r: forall i p q, 0 < i ->
 rel_prime p q -> rel_prime p (q^i).

Theorem rel_prime_Zpower: forall i j p q, 0 <= i -> 0 <= j ->
 rel_prime p q -> rel_prime (p^i) (q^j).

Theorem prime_power_prime: forall p q n, 0 <= n ->
 prime p -> prime q -> (p | q^n) -> p = q.

Theorem Zdivide_power_2: forall x p n, 0 <= n -> 0 <= x -> prime p ->
 (x | p^n) -> exists m, x = p^m.

Zsquare: a direct definition of z^2


Fixpoint Psquare (p: positive): positive :=
  match p with
   | xH => xH
   | xO p => xO (xO (Psquare p))
   | xI p => xI (xO (Pplus (Psquare p) p))
  end.

Definition Zsquare p :=
  match p with
   | Z0 => Z0
   | Zpos p => Zpos (Psquare p)
   | Zneg p => Zpos (Psquare p)
  end.

Theorem Psquare_correct: forall p, Psquare p = (p * p)%positive.

Theorem Zsquare_correct: forall p, Zsquare p = p * p.