Library Coq.Numbers.Natural.Abstract.NPow


Properties of the power function

Require Import Bool NAxioms NSub NParity NZPow.

Derived properties of power, specialized on natural numbers

Module Type NPowProp
 (Import A : NAxiomsSig´)
 (Import B : NSubProp A)
 (Import C : NParityProp A B).

 Module Import Private_NZPow := Nop <+ NZPowProp A A B.

Ltac auto´ := trivial; try rewrite <- neq_0_lt_0; auto using le_0_l.
Ltac wrap l := intros; apply l; auto´.

Lemma pow_succ_r´ : forall a b, a^(S b) == a * a^b.

Power and basic constants

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

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

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

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

Power and addition, multiplication

Lemma pow_add_r : forall a b 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, a^(b*c) == (a^b)^c.

Power and nullity

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

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

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

Monotonicity

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

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

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

Lemma pow_lt_mono_r : forall a b c, 1<a -> 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, a~=0 -> b<=c -> a^b <= a^c.

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

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

Injectivity

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

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

Monotonicity results, both ways

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

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

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

Lemma pow_le_mono_r_iff : forall a b c, 1<a ->
  (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 -> 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, c~=0 ->
  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, c~=0 ->
  (a+b)^c <= 2^(pred c) * (a^c + b^c).

Power and parity

Lemma even_pow : forall a b, b~=0 -> even (a^b) = even a.

Lemma odd_pow : forall a b, b~=0 -> odd (a^b) = odd a.

End NPowProp.