theory.shiftl

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

Section shiftl.
Context `{SemiRing A} `{!LeftCancellation (.*.) (2:A)} `{SemiRing B} `{!Biinduction B} `{!ShiftLSpec A B sl}.

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

Global Instance: Proper ((=) ==> (=) ==> (=)) (≪) | 1.

Lemma shiftl_nat_pow_alt `{Naturals B2} `{!NatPowSpec A B2 pw}
  `{!SemiRing_Morphism (f : B2 B)} x n : x f n = x * 2 ^ n.

Lemma shiftl_nat_pow `{!NaturalsToSemiRing B} `{!Naturals B} `{!NatPowSpec A B np} x n :
  x n = x * 2 ^ n.

Lemma shiftl_1 x : x (1:B) = 2 * x.

Lemma shiftl_2 x : x (2:B) = 4 * x.

Global Instance shiftl_base_0: LeftAbsorb (≪) 0.

Lemma shiftl_exp_plus x n m : x (n + m) = x n m.

Lemma shiftl_order x n m: x n m = x m n.

Lemma shiftl_reverse (x : A) (n m : B) : n + m = 0 x n m = x.

Lemma shiftl_mult_l x y n : x * (y n) = (x * y) n.

Lemma shiftl_mult_r x y n : (x n) * y = (x * y) n.

Lemma shiftl_base_plus x y n : (x + y) n = x n + y n.

Lemma shiftl_base_nat_pow `{Naturals B2} `{!NatPowSpec A B2 pw} `{!SemiRing_Morphism (f : B2 B)} x n m :
  (x n) ^ m = (x ^ m) (n * f m).

Lemma shiftl_opp `{GroupInv A} `{!Ring A} x n : (-x) n = -(x n).

Instance: n, Setoid_Morphism (≪ n).

Global Instance shiftl_inj: n, Injective (≪ n).

Instance shiftl_ne_0 x n :
  PropHolds (x 0) PropHolds (x n 0).

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

Let shiftl_strict_order_embedding (x y : A) (n : B) : x < y x n < y n.

Global Instance: n, StrictOrderEmbedding (≪ n).

Global Instance: n, OrderEmbedding (≪ n).

Global Instance shiftl_strong_inj: n, StrongInjective (≪ n).

Lemma shiftl_le_flip_r `{GroupInv B} `{!Ring B} (x y : A) (n : B) :
  x y (-n) x n y.

Lemma shiftl_le_flip_l `{GroupInv B} `{!Ring B} (x y : A) (n : B) :
  x (-n) y x y n.

Instance shiftl_nonneg (x : A) (n : B) : PropHolds (0 x) PropHolds (0 x n).

Instance shiftl_pos (x : A) (n : B) : PropHolds (0 < x) PropHolds (0 < x n).
End shiftl.

Hint Extern 18 (PropHolds (_ _ 0)) => eapply @shiftl_ne_0 : typeclass_instances.
Hint Extern 18 (PropHolds (0 _ _)) => eapply @shiftl_nonneg : typeclass_instances.
Hint Extern 18 (PropHolds (0 < _ _)) => eapply @shiftl_pos : typeclass_instances.

Section preservation.
  Context `{SemiRing B} `{!Biinduction B}
    `{SemiRing A1} `{!ShiftLSpec A1 B sl1} `{SemiRing A2} `{!LeftCancellation (.*.) (2:A2)} `{!ShiftLSpec A2 B sl2}
    `{!SemiRing_Morphism (f : A1 A2)}.

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

Section exp_preservation.
  Context `{SemiRing B1} `{!Biinduction B1} `{SemiRing B2} `{!Biinduction B2}
   `{SemiRing A} `{!LeftCancellation (.*.) (2:A)} `{!ShiftLSpec A B1 sl1} `{!ShiftLSpec A B2 sl2}
   `{!SemiRing_Morphism (f : B1 B2)}.

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

Section shiftl_dec_field.
  Context `{SemiRing R} `{Integers Z} `{!ShiftLSpec R Z sl}
     `{DecField F} `{ x y : F, Decision (x = y)} `{!PropHolds ((2:F) 0)} `{!IntPowSpec F Z ipw}
     `{!SemiRing_Morphism (f : R F)}.

  Add Ring F: (rings.stdlib_ring_theory F).
  Add Ring Z: (rings.stdlib_ring_theory Z).


  Lemma shiftl_to_int_pow x n : f (x n) = f x * 2 ^ n.

  Lemma shiftl_base_1_to_int_pow n : f (1 n) = 2 ^ n.

  Lemma shiftl_opp_1_to_half x : f (x -1) = f x / 2.

  Lemma shiftl_opp_1_to_fourth x : f (x -2) = f x / 4.
End shiftl_dec_field.

Section more_shiftl_dec_field.
  Context `{DecField A} `{Integers B} `{ x y : A, Decision (x = y)}
    `{!PropHolds ((2:A) 0)} `{!ShiftLSpec A B sl} `{!IntPowSpec A B ipw}.

  Lemma shiftl_int_pow x n : x n = x * 2 ^ n.

  Lemma shiftl_base_1_int_pow n : 1 n = 2 ^ n.

  Lemma shiftl_opp_1_half x : x (-1) = x / 2.

  Lemma shiftl_opp_1_fourth x : x (-2) = x / 4.
End more_shiftl_dec_field.

Section shiftl_field.
  Context `{Ring R} `{Integers Z} `{!ShiftLSpec R Z sl}
    `{Field F} `{!PropHolds ((2:F) 0)} `{Naturals N} `{!NatPowSpec F N npw}
    `{!SemiRing_Morphism (g : N Z)} `{!SemiRing_Morphism (f : R F)}.

  Add Ring F2: (rings.stdlib_ring_theory F).
  Add Ring Z2: (rings.stdlib_ring_theory Z).

  Lemma shiftl_opp_nat_pow x n : f (x (-g n)) * 2 ^ n = f x.

  Lemma shiftl_opp_to_mult_inv_nat_pow x n P2n : f (x (-g n)) = f x // (2 ^ n)↾P2n.
End shiftl_field.

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

  Global Instance default_shiftl: ShiftL A B | 10 := λ x n, x * 2 ^ n.

  Global Instance: ShiftLSpec A B default_shiftl.
End default_shiftl_naturals.

Typeclasses Opaque default_shiftl.

Section default_shiftl_integers.
  Context `{DecField A} `{!PropHolds ((2:A) 0)} `{Integers B} `{!IntPowSpec A B ipw}.

  Global Instance default_shiftl_int: ShiftL A B | 9 := λ x n, x * 2 ^ n.

  Global Instance: ShiftLSpec A B default_shiftl_int.
End default_shiftl_integers.

Typeclasses Opaque default_shiftl_int.