Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
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'.forall a b : t, a ^ S b == a * a ^ bwrap pow_succ_r. Qed.forall a b : t, a ^ S b == a * a ^ b
Power and basic constants
forall a : t, a ~= 0 -> 0 ^ a == 0wrap pow_0_l. Qed. Definition pow_1_r : forall a, a^1 == a := pow_1_r.forall a : t, a ~= 0 -> 0 ^ a == 0forall a : t, 1 ^ a == 1wrap pow_1_l. Qed. Definition pow_2_r : forall a, a^2 == a*a := pow_2_r.forall a : t, 1 ^ a == 1
Power and addition, multiplication
forall a b c : t, a ^ (b + c) == a ^ b * a ^ cwrap pow_add_r. Qed.forall a b c : t, a ^ (b + c) == a ^ b * a ^ cforall a b c : t, (a * b) ^ c == a ^ c * b ^ cwrap pow_mul_l. Qed.forall a b c : t, (a * b) ^ c == a ^ c * b ^ cforall a b c : t, a ^ (b * c) == (a ^ b) ^ cwrap pow_mul_r. Qed.forall a b c : t, a ^ (b * c) == (a ^ b) ^ c
Power and nullity
forall a b : t, b ~= 0 -> a ^ b == 0 -> a == 0forall a b : t, b ~= 0 -> a ^ b == 0 -> a == 0a, b:tH:b ~= 0H0:a ^ b == 0a == 0auto'. Qed.a, b:tH:b ~= 0H0:a ^ b == 00 <= bforall a b : t, a ~= 0 -> a ^ b ~= 0wrap pow_nonzero. Qed.forall a b : t, a ~= 0 -> a ^ b ~= 0forall a b : t, a ^ b == 0 <-> b ~= 0 /\ a == 0forall a b : t, a ^ b == 0 <-> b ~= 0 /\ a == 0a, b:ta ^ b == 0 <-> b ~= 0 /\ a == 0a, b:ta ^ b == 0 -> b ~= 0 /\ a == 0a, b:tb ~= 0 /\ a == 0 -> a ^ b == 0a, b:tb < 0 \/ 0 < b /\ a == 0 -> b ~= 0 /\ a == 0a, b:tb ~= 0 /\ a == 0 -> a ^ b == 0a, b:tH:b < 0b ~= 0 /\ a == 0a, b:tH:0 < bH':a == 0b ~= 0 /\ a == 0a, b:tb ~= 0 /\ a == 0 -> a ^ b == 0a, b:tH:0 < bH':a == 0b ~= 0 /\ a == 0a, b:tb ~= 0 /\ a == 0 -> a ^ b == 0a, b:tb ~= 0 /\ a == 0 -> a ^ b == 0a, b:tHb:b ~= 0Ha:a == 0a ^ b == 0now apply pow_0_l'. Qed.a, b:tHb:b ~= 0Ha:a == 00 ^ b == 0
Monotonicity
forall a b c : t, c ~= 0 -> a < b -> a ^ c < b ^ cwrap pow_lt_mono_l. Qed.forall a b c : t, c ~= 0 -> a < b -> a ^ c < b ^ cforall a b c : t, a <= b -> a ^ c <= b ^ cwrap pow_le_mono_l. Qed.forall a b c : t, a <= b -> a ^ c <= b ^ cforall a b : t, 1 < a -> b ~= 0 -> 1 < a ^ bwrap pow_gt_1. Qed.forall a b : t, 1 < a -> b ~= 0 -> 1 < a ^ bforall a b c : t, 1 < a -> b < c -> a ^ b < a ^ cwrap pow_lt_mono_r. Qed.forall a b c : t, 1 < a -> b < c -> a ^ b < a ^ c
NB: since 0^0 > 0^1, the following result isn't valid with a=0
forall a b c : t, a ~= 0 -> b <= c -> a ^ b <= a ^ cwrap pow_le_mono_r. Qed.forall a b c : t, a ~= 0 -> b <= c -> a ^ b <= a ^ cforall a b c d : t, a ~= 0 -> a <= c -> b <= d -> a ^ b <= c ^ dwrap pow_le_mono. Qed. Definition pow_lt_mono : forall a b c d, 0<a<c -> 0<b<d -> a^b < c^d := pow_lt_mono.forall a b c d : t, a ~= 0 -> a <= c -> b <= d -> a ^ b <= c ^ d
Injectivity
forall a b c : t, c ~= 0 -> a ^ c == b ^ c -> a == bintros; eapply pow_inj_l; eauto; auto'. Qed.forall a b c : t, c ~= 0 -> a ^ c == b ^ c -> a == bforall a b c : t, 1 < a -> a ^ b == a ^ c -> b == cintros; eapply pow_inj_r; eauto; auto'. Qed.forall a b c : t, 1 < a -> a ^ b == a ^ c -> b == c
Monotonicity results, both ways
forall a b c : t, c ~= 0 -> a < b <-> a ^ c < b ^ cwrap pow_lt_mono_l_iff. Qed.forall a b c : t, c ~= 0 -> a < b <-> a ^ c < b ^ cforall a b c : t, c ~= 0 -> a <= b <-> a ^ c <= b ^ cwrap pow_le_mono_l_iff. Qed.forall a b c : t, c ~= 0 -> a <= b <-> a ^ c <= b ^ cforall a b c : t, 1 < a -> b < c <-> a ^ b < a ^ cwrap pow_lt_mono_r_iff. Qed.forall a b c : t, 1 < a -> b < c <-> a ^ b < a ^ cforall a b c : t, 1 < a -> b <= c <-> a ^ b <= a ^ cwrap pow_le_mono_r_iff. Qed.forall a b c : t, 1 < a -> b <= c <-> a ^ b <= a ^ c
For any a>1, the a^x function is above the identity function
forall a b : t, 1 < a -> b < a ^ bwrap pow_gt_lin_r. Qed.forall a b : t, 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.
forall a b c : t, c ~= 0 -> a ^ c + b ^ c <= (a + b) ^ cwrap pow_add_lower. Qed.forall a b c : t, 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
forall a b c : t, c ~= 0 -> (a + b) ^ c <= 2 ^ P c * (a ^ c + b ^ c)wrap pow_add_upper. Qed.forall a b c : t, c ~= 0 -> (a + b) ^ c <= 2 ^ P c * (a ^ c + b ^ c)
Power and parity
forall a b : t, b ~= 0 -> even (a ^ b) = even aforall a b : t, b ~= 0 -> even (a ^ b) = even aa, b:tHb:b ~= 0even (a ^ b) = even aa, b:tHb:0 < beven (a ^ b) = even aa, b:tHb:0 < bProper (eq ==> iff) (fun b0 : t => even (a ^ b0) = even a)a, b:tHb:0 < beven (a ^ S 0) = even aa, b:tHb:0 < bforall m : t, 0 < m -> even (a ^ m) = even a -> even (a ^ S m) = even aa, b:tHb:0 < beven (a ^ S 0) = even aa, b:tHb:0 < bforall m : t, 0 < m -> even (a ^ m) = even a -> even (a ^ S m) = even aa, b:tHb:0 < bforall m : t, 0 < m -> even (a ^ m) = even a -> even (a ^ S m) = even aa:tforall m : t, 0 < m -> even (a ^ m) = even a -> even (a ^ S m) = even aa, b:tHb:0 < bIH:even (a ^ b) = even aeven (a ^ S b) = even anow destruct (even a). Qed.a, b:tHb:0 < bIH:even (a ^ b) = even aeven a || even a = even aforall a b : t, b ~= 0 -> odd (a ^ b) = odd aforall a b : t, b ~= 0 -> odd (a ^ b) = odd anow rewrite <- !negb_even, even_pow. Qed. End NPowProp.a, b:tH:b ~= 0odd (a ^ b) = odd a