ZPow.v

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 ZAxioms ZMulOrder ZParity ZSgnAbs NZPow.

Module Type ZPowProp
 (Import A : ZAxiomsSig')
 (Import B : ZMulOrderProp A)
 (Import C : ZParityProp A B)
 (Import D : ZSgnAbsProp A B).

 Include NZPowProp A A B.

A particular case of pow_add_r, with no precondition

Lemma pow_twice_r a b : a^(2*b) == a^b * a^b.a, b:t
a ^ (2 * b) == a ^ b * a ^ b
Proof.a, b:t
a ^ (2 * b) == a ^ b * a ^ b
 rewrite two_succ.a, b:t
a ^ (S 1 * b) == a ^ b * a ^ b nzsimpl.a, b:t
a ^ (b + b) == a ^ b * a ^ b
 destruct (le_gt_cases 0 b).a, b:t
H:0 <= b
a ^ (b + b) == a ^ b * a ^ b
a, b:t
H:b < 0
a ^ (b + b) == a ^ b * a ^ b
 -a, b:t
H:0 <= b
a ^ (b + b) == a ^ b * a ^ b now rewrite pow_add_r.
 -a, b:t
H:b < 0
a ^ (b + b) == a ^ b * a ^ b rewrite !pow_neg_r.a, b:t
H:b < 0
0 == 0 * 0
a, b:t
H:b < 0
b < 0
a, b:t
H:b < 0
b + b < 0 now nzsimpl.a, b:t
H:b < 0
b < 0
a, b:t
H:b < 0
b + b < 0 trivial.a, b:t
H:b < 0
b + b < 0
   now apply add_neg_neg.
Qed.

Parity of power

Lemma even_pow : forall a b, 0<b -> even (a^b) = even a.forall a b : t, 0 < b -> even (a ^ b) = even a
Proof.forall a b : t, 0 < b -> even (a ^ b) = even a
 intros a b Hb.a, b:t
Hb:0 < b
even (a ^ b) = even a apply lt_ind with (4:=Hb).a, b:t
Hb:0 < b
Proper (eq ==> iff)
  (fun b0 : t => even (a ^ b0) = even a)
a, b:t
Hb:0 < b
even (a ^ S 0) = even a
a, b:t
Hb:0 < b
forall m : t,
0 < m ->
even (a ^ m) = even a -> even (a ^ S m) = even a solve_proper.a, b:t
Hb:0 < b
even (a ^ S 0) = even a
a, b:t
Hb:0 < b
forall m : t,
0 < m ->
even (a ^ m) = even a -> even (a ^ S m) = even a
 now nzsimpl.a, b:t
Hb:0 < b
forall m : t,
0 < m ->
even (a ^ m) = even a -> even (a ^ S m) = even a
 clear b Hb.a:t
forall m : t,
0 < m ->
even (a ^ m) = even a -> even (a ^ S m) = even a intros b Hb IH.a, b:t
Hb:0 < b
IH:even (a ^ b) = even a
even (a ^ S b) = even a nzsimpl; [|order].a, b:t
Hb:0 < b
IH:even (a ^ b) = even a
even (a * a ^ b) = even a
 rewrite even_mul, IH.a, b:t
Hb:0 < b
IH:even (a ^ b) = even a
even a || even a = even a now destruct (even a).
Qed.

Lemma odd_pow : forall a b, 0<b -> odd (a^b) = odd a.forall a b : t, 0 < b -> odd (a ^ b) = odd a
Proof.forall a b : t, 0 < b -> odd (a ^ b) = odd a
 intros.a, b:t
H:0 < b
odd (a ^ b) = odd a now rewrite <- !negb_even, even_pow.
Qed.

Properties of power of negative numbers

Lemma pow_opp_even : forall a b, Even b -> (-a)^b == a^b.forall a b : t, Even b -> (- a) ^ b == a ^ b
Proof.forall a b : t, Even b -> (- a) ^ b == a ^ b
 intros a b (c,H).a, b, c:t
H:b == 2 * c
(- a) ^ b == a ^ b rewrite H.a, b, c:t
H:b == 2 * c
(- a) ^ (2 * c) == a ^ (2 * c)
 destruct (le_gt_cases 0 c).a, b, c:t
H:b == 2 * c
H0:0 <= c
(- a) ^ (2 * c) == a ^ (2 * c)
a, b, c:t
H:b == 2 * c
H0:c < 0
(- a) ^ (2 * c) == a ^ (2 * c)
 rewrite 2 pow_mul_r by order'.a, b, c:t
H:b == 2 * c
H0:0 <= c
((- a) ^ 2) ^ c == (a ^ 2) ^ c
a, b, c:t
H:b == 2 * c
H0:c < 0
(- a) ^ (2 * c) == a ^ (2 * c)
 rewrite 2 pow_2_r.a, b, c:t
H:b == 2 * c
H0:0 <= c
(- a * - a) ^ c == (a * a) ^ c
a, b, c:t
H:b == 2 * c
H0:c < 0
(- a) ^ (2 * c) == a ^ (2 * c)
 now rewrite mul_opp_opp.a, b, c:t
H:b == 2 * c
H0:c < 0
(- a) ^ (2 * c) == a ^ (2 * c)
 assert (2*c < 0) by (apply mul_pos_neg; order').a, b, c:t
H:b == 2 * c
H0:c < 0
H1:2 * c < 0
(- a) ^ (2 * c) == a ^ (2 * c)
 now rewrite !pow_neg_r.
Qed.

Lemma pow_opp_odd : forall a b, Odd b -> (-a)^b == -(a^b).forall a b : t, Odd b -> (- a) ^ b == - a ^ b
Proof.forall a b : t, Odd b -> (- a) ^ b == - a ^ b
 intros a b (c,H).a, b, c:t
H:b == 2 * c + 1
(- a) ^ b == - a ^ b rewrite H.a, b, c:t
H:b == 2 * c + 1
(- a) ^ (2 * c + 1) == - a ^ (2 * c + 1)
 destruct (le_gt_cases 0 c) as [LE|GT].a, b, c:t
H:b == 2 * c + 1
LE:0 <= c
(- a) ^ (2 * c + 1) == - a ^ (2 * c + 1)
a, b, c:t
H:b == 2 * c + 1
GT:c < 0
(- a) ^ (2 * c + 1) == - a ^ (2 * c + 1)
 assert (0 <= 2*c) by (apply mul_nonneg_nonneg; order').a, b, c:t
H:b == 2 * c + 1
LE:0 <= c
H0:0 <= 2 * c
(- a) ^ (2 * c + 1) == - a ^ (2 * c + 1)
a, b, c:t
H:b == 2 * c + 1
GT:c < 0
(- a) ^ (2 * c + 1) == - a ^ (2 * c + 1)
 rewrite add_1_r, !pow_succ_r; trivial.a, b, c:t
H:b == 2 * c + 1
LE:0 <= c
H0:0 <= 2 * c
- a * (- a) ^ (2 * c) == - (a * a ^ (2 * c))
a, b, c:t
H:b == 2 * c + 1
GT:c < 0
(- a) ^ (2 * c + 1) == - a ^ (2 * c + 1)
 rewrite pow_opp_even by (now exists c).a, b, c:t
H:b == 2 * c + 1
LE:0 <= c
H0:0 <= 2 * c
- a * a ^ (2 * c) == - (a * a ^ (2 * c))
a, b, c:t
H:b == 2 * c + 1
GT:c < 0
(- a) ^ (2 * c + 1) == - a ^ (2 * c + 1)
 apply mul_opp_l.a, b, c:t
H:b == 2 * c + 1
GT:c < 0
(- a) ^ (2 * c + 1) == - a ^ (2 * c + 1)
 apply double_above in GT.a, b, c:t
H:b == 2 * c + 1
GT:2 * c + 1 < 2 * 0
(- a) ^ (2 * c + 1) == - a ^ (2 * c + 1) rewrite mul_0_r in GT.a, b, c:t
H:b == 2 * c + 1
GT:2 * c + 1 < 0
(- a) ^ (2 * c + 1) == - a ^ (2 * c + 1)
 rewrite !pow_neg_r by trivial.a, b, c:t
H:b == 2 * c + 1
GT:2 * c + 1 < 0
0 == - 0 now rewrite opp_0.
Qed.

Lemma pow_even_abs : forall a b, Even b -> a^b == (abs a)^b.forall a b : t, Even b -> a ^ b == abs a ^ b
Proof.forall a b : t, Even b -> a ^ b == abs a ^ b
 intros.a, b:t
H:Even b
a ^ b == abs a ^ b destruct (abs_eq_or_opp a) as [EQ|EQ]; rewrite EQ.a, b:t
H:Even b
EQ:abs a == a
a ^ b == a ^ b
a, b:t
H:Even b
EQ:abs a == - a
a ^ b == (- a) ^ b
 reflexivity.a, b:t
H:Even b
EQ:abs a == - a
a ^ b == (- a) ^ b
 symmetry.a, b:t
H:Even b
EQ:abs a == - a
(- a) ^ b == a ^ b now apply pow_opp_even.
Qed.

Lemma pow_even_nonneg : forall a b, Even b -> 0 <= a^b.forall a b : t, Even b -> 0 <= a ^ b
Proof.forall a b : t, Even b -> 0 <= a ^ b
 intros.a, b:t
H:Even b
0 <= a ^ b rewrite pow_even_abs by trivial.a, b:t
H:Even b
0 <= abs a ^ b
 apply pow_nonneg, abs_nonneg.
Qed.

Lemma pow_odd_abs_sgn : forall a b, Odd b -> a^b == sgn a * (abs a)^b.forall a b : t, Odd b -> a ^ b == sgn a * abs a ^ b
Proof.forall a b : t, Odd b -> a ^ b == sgn a * abs a ^ b
 intros a b H.a, b:t
H:Odd b
a ^ b == sgn a * abs a ^ b
 destruct (sgn_spec a) as [(LT,EQ)|[(EQ',EQ)|(LT,EQ)]]; rewrite EQ.a, b:t
H:Odd b
LT:0 < a
EQ:sgn a == 1
a ^ b == 1 * abs a ^ b
a, b:t
H:Odd b
EQ':0 == a
EQ:sgn a == 0
a ^ b == 0 * abs a ^ b
a, b:t
H:Odd b
LT:a < 0
EQ:sgn a == -1
a ^ b == -1 * abs a ^ b
 nzsimpl.a, b:t
H:Odd b
LT:0 < a
EQ:sgn a == 1
a ^ b == abs a ^ b
a, b:t
H:Odd b
EQ':0 == a
EQ:sgn a == 0
a ^ b == 0 * abs a ^ b
a, b:t
H:Odd b
LT:a < 0
EQ:sgn a == -1
a ^ b == -1 * abs a ^ b
 rewrite abs_eq; order.a, b:t
H:Odd b
EQ':0 == a
EQ:sgn a == 0
a ^ b == 0 * abs a ^ b
a, b:t
H:Odd b
LT:a < 0
EQ:sgn a == -1
a ^ b == -1 * abs a ^ b
 rewrite <- EQ'.a, b:t
H:Odd b
EQ':0 == a
EQ:sgn a == 0
0 ^ b == 0 * abs 0 ^ b
a, b:t
H:Odd b
LT:a < 0
EQ:sgn a == -1
a ^ b == -1 * abs a ^ b nzsimpl.a, b:t
H:Odd b
EQ':0 == a
EQ:sgn a == 0
0 ^ b == 0
a, b:t
H:Odd b
LT:a < 0
EQ:sgn a == -1
a ^ b == -1 * abs a ^ b
 destruct (le_gt_cases 0 b).a, b:t
H:Odd b
EQ':0 == a
EQ:sgn a == 0
H0:0 <= b
0 ^ b == 0
a, b:t
H:Odd b
EQ':0 == a
EQ:sgn a == 0
H0:b < 0
0 ^ b == 0
a, b:t
H:Odd b
LT:a < 0
EQ:sgn a == -1
a ^ b == -1 * abs a ^ b
 apply pow_0_l.a, b:t
H:Odd b
EQ':0 == a
EQ:sgn a == 0
H0:0 <= b
0 < b
a, b:t
H:Odd b
EQ':0 == a
EQ:sgn a == 0
H0:b < 0
0 ^ b == 0
a, b:t
H:Odd b
LT:a < 0
EQ:sgn a == -1
a ^ b == -1 * abs a ^ b
 assert (b~=0) by (contradict H; now rewrite H, <-odd_spec, odd_0).a, b:t
H:Odd b
EQ':0 == a
EQ:sgn a == 0
H0:0 <= b
H1:b ~= 0
0 < b
a, b:t
H:Odd b
EQ':0 == a
EQ:sgn a == 0
H0:b < 0
0 ^ b == 0
a, b:t
H:Odd b
LT:a < 0
EQ:sgn a == -1
a ^ b == -1 * abs a ^ b
 order.a, b:t
H:Odd b
EQ':0 == a
EQ:sgn a == 0
H0:b < 0
0 ^ b == 0
a, b:t
H:Odd b
LT:a < 0
EQ:sgn a == -1
a ^ b == -1 * abs a ^ b
 now rewrite pow_neg_r.a, b:t
H:Odd b
LT:a < 0
EQ:sgn a == -1
a ^ b == -1 * abs a ^ b
 rewrite abs_neq by order.a, b:t
H:Odd b
LT:a < 0
EQ:sgn a == -1
a ^ b == -1 * (- a) ^ b
 rewrite pow_opp_odd; trivial.a, b:t
H:Odd b
LT:a < 0
EQ:sgn a == -1
a ^ b == -1 * - a ^ b
 now rewrite mul_opp_opp, mul_1_l.
Qed.

Lemma pow_odd_sgn : forall a b, 0<=b -> Odd b -> sgn (a^b) == sgn a.forall a b : t,
0 <= b -> Odd b -> sgn (a ^ b) == sgn a
Proof.forall a b : t,
0 <= b -> Odd b -> sgn (a ^ b) == sgn a
 intros a b Hb H.a, b:t
Hb:0 <= b
H:Odd b
sgn (a ^ b) == sgn a
 destruct (sgn_spec a) as [(LT,EQ)|[(EQ',EQ)|(LT,EQ)]]; rewrite EQ.a, b:t
Hb:0 <= b
H:Odd b
LT:0 < a
EQ:sgn a == 1
sgn (a ^ b) == 1
a, b:t
Hb:0 <= b
H:Odd b
EQ':0 == a
EQ:sgn a == 0
sgn (a ^ b) == 0
a, b:t
Hb:0 <= b
H:Odd b
LT:a < 0
EQ:sgn a == -1
sgn (a ^ b) == -1
 apply sgn_pos.a, b:t
Hb:0 <= b
H:Odd b
LT:0 < a
EQ:sgn a == 1
0 < a ^ b
a, b:t
Hb:0 <= b
H:Odd b
EQ':0 == a
EQ:sgn a == 0
sgn (a ^ b) == 0
a, b:t
Hb:0 <= b
H:Odd b
LT:a < 0
EQ:sgn a == -1
sgn (a ^ b) == -1 apply pow_pos_nonneg; trivial.a, b:t
Hb:0 <= b
H:Odd b
EQ':0 == a
EQ:sgn a == 0
sgn (a ^ b) == 0
a, b:t
Hb:0 <= b
H:Odd b
LT:a < 0
EQ:sgn a == -1
sgn (a ^ b) == -1
 rewrite <- EQ'.a, b:t
Hb:0 <= b
H:Odd b
EQ':0 == a
EQ:sgn a == 0
sgn (0 ^ b) == 0
a, b:t
Hb:0 <= b
H:Odd b
LT:a < 0
EQ:sgn a == -1
sgn (a ^ b) == -1 rewrite pow_0_l.a, b:t
Hb:0 <= b
H:Odd b
EQ':0 == a
EQ:sgn a == 0
sgn 0 == 0
a, b:t
Hb:0 <= b
H:Odd b
EQ':0 == a
EQ:sgn a == 0
0 < b
a, b:t
Hb:0 <= b
H:Odd b
LT:a < 0
EQ:sgn a == -1
sgn (a ^ b) == -1 apply sgn_0.a, b:t
Hb:0 <= b
H:Odd b
EQ':0 == a
EQ:sgn a == 0
0 < b
a, b:t
Hb:0 <= b
H:Odd b
LT:a < 0
EQ:sgn a == -1
sgn (a ^ b) == -1
 assert (b~=0) by (contradict H; now rewrite H, <-odd_spec, odd_0).a, b:t
Hb:0 <= b
H:Odd b
EQ':0 == a
EQ:sgn a == 0
H0:b ~= 0
0 < b
a, b:t
Hb:0 <= b
H:Odd b
LT:a < 0
EQ:sgn a == -1
sgn (a ^ b) == -1
 order.a, b:t
Hb:0 <= b
H:Odd b
LT:a < 0
EQ:sgn a == -1
sgn (a ^ b) == -1
 apply sgn_neg.a, b:t
Hb:0 <= b
H:Odd b
LT:a < 0
EQ:sgn a == -1
a ^ b < 0
 rewrite <- (opp_involutive a).a, b:t
Hb:0 <= b
H:Odd b
LT:a < 0
EQ:sgn a == -1
(- - a) ^ b < 0 rewrite pow_opp_odd by trivial.a, b:t
Hb:0 <= b
H:Odd b
LT:a < 0
EQ:sgn a == -1
- (- a) ^ b < 0
 apply opp_neg_pos.a, b:t
Hb:0 <= b
H:Odd b
LT:a < 0
EQ:sgn a == -1
0 < (- a) ^ b
 apply pow_pos_nonneg; trivial.a, b:t
Hb:0 <= b
H:Odd b
LT:a < 0
EQ:sgn a == -1
0 < - a
 now apply opp_pos_neg.
Qed.

Lemma abs_pow : forall a b, abs (a^b) == (abs a)^b.forall a b : t, abs (a ^ b) == abs a ^ b
Proof.forall a b : t, abs (a ^ b) == abs a ^ b
 intros a b.a, b:t
abs (a ^ b) == abs a ^ b
 destruct (Even_or_Odd b).a, b:t
H:Even b
abs (a ^ b) == abs a ^ b
a, b:t
H:Odd b
abs (a ^ b) == abs a ^ b
 rewrite pow_even_abs by trivial.a, b:t
H:Even b
abs (abs a ^ b) == abs a ^ b
a, b:t
H:Odd b
abs (a ^ b) == abs a ^ b
 apply abs_eq, pow_nonneg, abs_nonneg.a, b:t
H:Odd b
abs (a ^ b) == abs a ^ b
 rewrite pow_odd_abs_sgn by trivial.a, b:t
H:Odd b
abs (sgn a * abs a ^ b) == abs a ^ b
 rewrite abs_mul.a, b:t
H:Odd b
abs (sgn a) * abs (abs a ^ b) == abs a ^ b
 destruct (lt_trichotomy 0 a) as [Ha|[Ha|Ha]].a, b:t
H:Odd b
Ha:0 < a
abs (sgn a) * abs (abs a ^ b) == abs a ^ b
a, b:t
H:Odd b
Ha:0 == a
abs (sgn a) * abs (abs a ^ b) == abs a ^ b
a, b:t
H:Odd b
Ha:a < 0
abs (sgn a) * abs (abs a ^ b) == abs a ^ b
 rewrite (sgn_pos a), (abs_eq 1), mul_1_l by order'.a, b:t
H:Odd b
Ha:0 < a
abs (abs a ^ b) == abs a ^ b
a, b:t
H:Odd b
Ha:0 == a
abs (sgn a) * abs (abs a ^ b) == abs a ^ b
a, b:t
H:Odd b
Ha:a < 0
abs (sgn a) * abs (abs a ^ b) == abs a ^ b
 apply abs_eq, pow_nonneg, abs_nonneg.a, b:t
H:Odd b
Ha:0 == a
abs (sgn a) * abs (abs a ^ b) == abs a ^ b
a, b:t
H:Odd b
Ha:a < 0
abs (sgn a) * abs (abs a ^ b) == abs a ^ b
 rewrite <- Ha, sgn_0, abs_0, mul_0_l.a, b:t
H:Odd b
Ha:0 == a
0 == 0 ^ b
a, b:t
H:Odd b
Ha:a < 0
abs (sgn a) * abs (abs a ^ b) == abs a ^ b
 symmetry.a, b:t
H:Odd b
Ha:0 == a
0 ^ b == 0
a, b:t
H:Odd b
Ha:a < 0
abs (sgn a) * abs (abs a ^ b) == abs a ^ b apply pow_0_l'.a, b:t
H:Odd b
Ha:0 == a
b ~= 0
a, b:t
H:Odd b
Ha:a < 0
abs (sgn a) * abs (abs a ^ b) == abs a ^ b intro Hb.a, b:t
H:Odd b
Ha:0 == a
Hb:b == 0
False
a, b:t
H:Odd b
Ha:a < 0
abs (sgn a) * abs (abs a ^ b) == abs a ^ b rewrite Hb in H.a, b:t
H:Odd 0
Ha:0 == a
Hb:b == 0
False
a, b:t
H:Odd b
Ha:a < 0
abs (sgn a) * abs (abs a ^ b) == abs a ^ b
 apply (Even_Odd_False 0); trivial.a, b:t
H:Odd 0
Ha:0 == a
Hb:b == 0
Even 0
a, b:t
H:Odd b
Ha:a < 0
abs (sgn a) * abs (abs a ^ b) == abs a ^ b exists 0; now nzsimpl.a, b:t
H:Odd b
Ha:a < 0
abs (sgn a) * abs (abs a ^ b) == abs a ^ b
 rewrite (sgn_neg a), abs_opp, (abs_eq 1), mul_1_l by order'.a, b:t
H:Odd b
Ha:a < 0
abs (abs a ^ b) == abs a ^ b
 apply abs_eq, pow_nonneg, abs_nonneg.
Qed.

End ZPowProp.