theory.int_pow

Require
  theory.naturals orders.semirings orders.integers orders.dec_fields.
Require Import
  Ring Field
  abstract_algebra interfaces.naturals interfaces.integers
  interfaces.additional_operations interfaces.orders
  theory.nat_pow theory.int_abs theory.dec_fields.

Section int_pow_properties.
Context `{DecField A} `{ x y, Decision (x = y)} `{Integers B} `{!IntPowSpec A B ipw}.

Add Field A : (dec_fields.stdlib_field_theory A).
Add Ring B : (rings.stdlib_ring_theory B).

Global Instance: Proper ((=) ==> (=) ==> (=)) (^) | 0.

Lemma int_pow_S_nonneg `{Apart B} `{!TrivialApart B} `{!FullPseudoSemiRingOrder (A:=B) Ble Blt} (x : A) (n : B) :
  0 n x ^ (1+n) = x * x ^ n.

Lemma int_pow_opp (x : A) (n : B) : x ^ (-n) = /(x ^ n).

Lemma int_pow_opp_alt (x : A) (n : B) : x ^ n = /(x ^ (-n)).

Lemma int_pow_mult (x y : A) (n : B) : (x * y) ^ n = x ^ n * y ^ n.

Lemma int_pow_mult_inv (x : A) (n : B) : (/x) ^ n = /(x ^ n).

Lemma int_pow_nat_pow `{Naturals N} `{!NatPowSpec A N pw} {f : N B} `{!SemiRing_Morphism f} (x : A) (n : N) :
  x ^ (f n) = x ^ n.

Global Instance int_pow_1: RightIdentity (^) (1:B).

Lemma int_pow_2 x : x ^ (2:B) = x * x.

Lemma int_pow_3 x : x ^ (3:B) = x * (x * x).

Lemma int_pow_4 x : x ^ (4:B) = x * (x * (x * x)).

Global Instance int_pow_base_1: LeftAbsorb (^) 1.

Lemma int_pow_exp_plus (n m : B) (x : A) :
  x 0 x ^ (n + m) = x ^ n * x ^ m.

Instance int_pow_ne_0 (x : A) (n : B) : PropHolds (x 0) PropHolds (x ^ n 0).

Lemma int_pow_exp_mult (x : A) (n m : B) :
  x ^ (n * m) = (x ^ n) ^ m.

Context `{Apart A} `{!TrivialApart A} `{!FullPseudoSemiRingOrder (A:=A) Ale Alt}.
Context `{Apart B} `{!TrivialApart B} `{!FullPseudoSemiRingOrder (A:=B) Ble Blt}.

Instance int_pow_pos (x : A) (n : B) : PropHolds (0 < x) PropHolds (0 < x ^ n).

Instance int_pow_nonneg (x : A) (n : B) : PropHolds (0 x) PropHolds (0 x ^ n).

Lemma int_pow_ge_1 (x : A) (n : B) : 1 x 0 n 1 x ^ n.

Lemma int_pow_gt_1 (x : A) (n : B) : 1 < x 0 < n 1 < x ^ n.

Instance int_pow_exp_le:
   x : A, PropHolds (1 x) OrderPreserving (x^).

Instance int_pow_exp_lt:
   x : A, PropHolds (1 < x) StrictlyOrderPreserving (x^).

Instance int_pow_exp_le_back:
   x : A, PropHolds (1 < x) OrderPreservingBack (x^).

Instance int_pow_exp_lt_back:
   x : A, PropHolds (1 < x) StrictlyOrderPreservingBack (x^).

Instance int_pow_inj:
   x : A, PropHolds (1 < x) Injective (x^).
End int_pow_properties.

Hint Extern 18 (PropHolds (_ ^ _ 0)) => eapply @int_pow_ne_0 : typeclass_instances.
Hint Extern 18 (PropHolds (0 _ ^ _)) => eapply @int_pow_nonneg : typeclass_instances.
Hint Extern 18 (PropHolds (0 < _ ^ _)) => eapply @int_pow_pos : typeclass_instances.

Section preservation.
  Context
    `{Integers B}
    `{DecField A1} `{ x y : A1, Decision (x = y)} `{!IntPowSpec A1 B ip1}
    `{DecField A2} `{ x y : A2, Decision (x = y)} `{!IntPowSpec A2 B ip2}
    {f : A1 A2} `{!SemiRing_Morphism f}.

  Add Ring B2 : (rings.stdlib_ring_theory B).

  Lemma preserves_int_pow x (n : B) : f (x ^ n) = (f x) ^ n.
End preservation.

Section exp_preservation.
  Context `{Field A} `{ x y : A, Decision (x = y)}
   `{Integers B1} `{Integers B2} `{!IntPowSpec A B1 pw1} `{!IntPowSpec A B2 pw2}
    {f : B1 B2} `{!SemiRing_Morphism f}.

  Lemma preserves_int_pow_exp x (n : B1) : x ^ (f n) = x ^ n.
End exp_preservation.

Section int_pow_default.
  Context `{DecField A} `{ x y, Decision (x = y)}
    `{Integers B} `{Apart B} `{!TrivialApart B} `{!FullPseudoSemiRingOrder (A:=B) Ble Blt}.

  Add Ring B3 : (rings.stdlib_ring_theory B).

  Global Instance int_pow_default: Pow A B | 10 := λ x n,
    match (decide_rel (≤) 0 n) with
    | left _ => x ^ int_abs B nat n
    | right _ => /x ^ int_abs B nat n
    end.

  Global Instance: IntPowSpec A B int_pow_default.
End int_pow_default.