# Library Coq.Numbers.NatInt.NZPow

Power Function

Require Import NZAxioms NZMulOrder.

Interface of a power function, then its specification on naturals

Module Type Pow (Import A : Typ).
Parameters Inline pow : t -> t -> t.
End Pow.

Module Type PowNotation (A : Typ)(Import B : Pow A).
Infix "^" := pow.
End PowNotation.

Module Type Pow' (A : Typ) := Pow A <+ PowNotation A.

Module Type NZPowSpec (Import A : NZOrdAxiomsSig')(Import B : Pow' A).
Declare Instance pow_wd : Proper (eq==>eq==>eq) pow.
Axiom pow_0_r : forall a, a^0 == 1.
Axiom pow_succ_r : forall a b, 0<=b -> a^(succ b) == a * a^b.
Axiom pow_neg_r : forall a b, b<0 -> a^b == 0.
End NZPowSpec.

The above pow_neg_r specification is useless (and trivially provable) for N. Having it here already allows deriving some slightly more general statements.

Module Type NZPow (A : NZOrdAxiomsSig) := Pow A <+ NZPowSpec A.
Module Type NZPow' (A : NZOrdAxiomsSig) := Pow' A <+ NZPowSpec A.

Derived properties of power

Module Type NZPowProp
(Import A : NZOrdAxiomsSig')
(Import B : NZPow' A)
(Import C : NZMulOrderProp A).

Hint Rewrite pow_0_r pow_succ_r : nz.

Power and basic constants

Lemma pow_0_l : forall a, 0<a -> 0^a == 0.

Lemma pow_0_l' : forall a, a~=0 -> 0^a == 0.

Lemma pow_1_r : forall a, a^1 == a.

Lemma pow_1_l : forall a, 0<=a -> 1^a == 1.

Hint Rewrite pow_1_r pow_1_l : nz.

Lemma pow_2_r : forall a, a^2 == a*a.

Hint Rewrite pow_2_r : nz.

Power and nullity

Lemma pow_eq_0 : forall a b, 0<=b -> a^b == 0 -> a == 0.

Lemma pow_nonzero : forall a b, a~=0 -> 0<=b -> a^b ~= 0.

Lemma pow_eq_0_iff : forall a b, a^b == 0 <-> b<0 \/ (0<b /\ a==0).

Lemma pow_add_r : forall a b c, 0<=b -> 0<=c ->
a^(b+c) == a^b * a^c.

Lemma pow_mul_l : forall a b c,
(a*b)^c == a^c * b^c.

Lemma pow_mul_r : forall a b c, 0<=b -> 0<=c ->
a^(b*c) == (a^b)^c.

Positivity

Lemma pow_nonneg : forall a b, 0<=a -> 0<=a^b.

Lemma pow_pos_nonneg : forall a b, 0<a -> 0<=b -> 0<a^b.

Monotonicity

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

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

Lemma pow_gt_1 : forall a b, 1<a -> (0<b <-> 1<a^b).

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

NB: since 0^0 > 0^1, the following result isn't valid with a=0

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

Lemma pow_le_mono : forall a b c d, 0<a<=c -> b<=d ->
a^b <= c^d.

Lemma pow_lt_mono : forall a b c d, 0<a<c -> 0<b<d ->
a^b < c^d.

Injectivity

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

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

Monotonicity results, both ways

Lemma pow_lt_mono_l_iff : forall a b c, 0<=a -> 0<=b -> 0<c ->
(a<b <-> a^c < b^c).

Lemma pow_le_mono_l_iff : forall a b c, 0<=a -> 0<=b -> 0<c ->
(a<=b <-> a^c <= b^c).

Lemma pow_lt_mono_r_iff : forall a b c, 1<a -> 0<=c ->
(b<c <-> a^b < a^c).

Lemma pow_le_mono_r_iff : forall a b c, 1<a -> 0<=c ->
(b<=c <-> a^b <= a^c).

For any a>1, the a^x function is above the identity function

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

Someday, we should say something about the full Newton formula. In the meantime, we can at least provide some inequalities about (a+b)^c.

Lemma pow_add_lower : forall a b c, 0<=a -> 0<=b -> 0<c ->
a^c + b^c <= (a+b)^c.

This upper bound can also be seen as a convexity proof for x^c : image of (a+b)/2 is below the middle of the images of a and b

Lemma pow_add_upper : forall a b c, 0<=a -> 0<=b -> 0<c ->
(a+b)^c <= 2^(pred c) * (a^c + b^c).

End NZPowProp.