theory.nat_pow

Require
  theory.naturals orders.naturals.
Require Import
  Ring
  abstract_algebra interfaces.naturals interfaces.orders interfaces.additional_operations.

Section nat_pow_properties.
Context `{SemiRing A} `{Naturals B} `{!NatPowSpec A B pw}.

Add Ring A: (rings.stdlib_semiring_theory A).
Add Ring B: (rings.stdlib_semiring_theory B).

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

Lemma nat_pow_base_0 (n : B) : n 0 0 ^ n = 0.

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

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

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

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

Global Instance nat_pow_base_1: LeftAbsorb (^) 1.

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

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

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

Instance nat_pow_ne_0 `{!NoZeroDivisors A} `{!PropHolds ((1:A) 0)} (x : A) (n : B) :
  PropHolds (x 0) PropHolds (x ^ n 0).

Context `{Apart A} `{!FullPseudoSemiRingOrder Ale Alt} `{PropHolds (1 0)}.

Instance: StrongSetoid A := pseudo_order_setoid.

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

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

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

Lemma nat_pow_ge_1 (x : A) (n : B) : 1 x 0 n 1 x ^ n.
End nat_pow_properties.

Hint Extern 18 (PropHolds (_ ^ _ 0)) => eapply @nat_pow_ne_0 : typeclass_instances.
Hint Extern 18 (PropHolds (_ ^ _ 0)) => eapply @nat_pow_apart_0 : typeclass_instances.
Hint Extern 18 (PropHolds (0 _ ^ _)) => eapply @nat_pow_nonneg : typeclass_instances.
Hint Extern 18 (PropHolds (0 < _ ^ _)) => eapply @nat_pow_pos : typeclass_instances.

Section preservation.
  Context `{Naturals B} `{SemiRing A1} `{!NatPowSpec A1 B pw1} `{SemiRing A2} `{!NatPowSpec A2 B pw2}
    {f : A1 A2} `{!SemiRing_Morphism f}.

  Add Ring B2 : (rings.stdlib_semiring_theory B).

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

Section exp_preservation.
  Context `{SemiRing A} `{Naturals B1} `{Naturals B2} `{!NatPowSpec A B1 pw1} `{!NatPowSpec A B2 pw2}
    {f : B1 B2} `{!SemiRing_Morphism f}.

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

Section nat_pow_default.
  Context `{SemiRing A}.

  Global Instance nat_pow_peano: Pow A nat :=
    fix nat_pow_rec (x: A) (n : nat) : A := match n with
    | 0 => 1
    | S n => x * nat_pow_rec x n
    end.

  Instance: Proper ((=) ==> (=) ==> (=)) nat_pow_peano.

  Global Instance: NatPowSpec A nat nat_pow_peano.

  Context `{Naturals B}.

  Global Instance default_nat_pow: Pow A B | 10 := λ x n, nat_pow_peano x (naturals_to_semiring B nat n).
  Global Instance: NatPowSpec A B default_nat_pow.
End nat_pow_default.

Typeclasses Opaque default_nat_pow.