theory.rings

Require
  varieties.monoids theory.groups strong_setoids.
Require Import
  Ring abstract_algebra.

Definition is_ne_0 `(x : R) `{Equiv R} `{RingZero R} `{p : PropHolds (x 0)} : x 0 := p.
Definition is_nonneg `(x : R) `{Equiv R} `{Le R} `{RingZero R} `{p : PropHolds (0 x)} : 0 x := p.
Definition is_pos `(x : R) `{Equiv R} `{Lt R} `{RingZero R} `{p : PropHolds (0 < x)} : 0 < x := p.

Lemma stdlib_semiring_theory R `{SemiRing R} : Ring_theory.semi_ring_theory 0 1 (+) (.*.) (=).

Section cancellation.
  Context `{e : Equiv A} (op : A A A) `{!RingZero A}.

  Lemma left_cancellation_ne_0 `{ z, PropHolds (z 0) LeftCancellation op z} z : z 0 LeftCancellation op z.

  Lemma right_cancellation_ne_0 `{ z, PropHolds (z 0) RightCancellation op z} z : z 0 RightCancellation op z.

  Lemma right_cancel_from_left `{!Setoid A} `{!Commutative op} `{!LeftCancellation op z} :
    RightCancellation op z.
End cancellation.

Section strong_cancellation.
  Context `{StrongSetoid A} (op : A A A).

  Lemma strong_right_cancel_from_left `{!Commutative op} `{!StrongLeftCancellation op z} :
    StrongRightCancellation op z.

  Global Instance strong_left_cancellation_cancel `{!StrongLeftCancellation op z} : LeftCancellation op z | 20.

  Global Instance strong_right_cancellation_cancel `{!StrongRightCancellation op z} : RightCancellation op z | 20.
End strong_cancellation.

Section semiring_props.
  Context `{SemiRing R}.
  Add Ring SR: (stdlib_semiring_theory R).

  Instance mult_ne_0 `{NoZeroDivisors R} x y : PropHolds (x 0) PropHolds (y 0) PropHolds (x * y 0).

  Global Instance plus_0_r: RightIdentity (+) 0 := right_identity.
  Global Instance plus_0_l: LeftIdentity (+) 0 := left_identity.
  Global Instance mult_1_l: LeftIdentity (.*.) 1 := left_identity.
  Global Instance mult_1_r: RightIdentity (.*.) 1 := right_identity.

  Global Instance mult_0_l: LeftAbsorb (.*.) 0 := left_absorb.

  Global Instance mult_0_r: RightAbsorb (.*.) 0.

  Lemma plus_mult_distr_r x y z: (x + y) * z = x * z + y * z.
  Lemma plus_mult_distr_l x y z: x * (y + z) = x * y + x * z.

  Global Instance: r : R, @Monoid_Morphism R R _ _ (0:R) (0:R) (+) (+) (r *.).
End semiring_props.

Hint Extern 3 (PropHolds (_ * _ 0)) => eapply @mult_ne_0 : typeclass_instances.

Section semiringmor_props.
  Context `{SemiRing_Morphism A B f}.

  Lemma preserves_0: f 0 = 0.
  Lemma preserves_1: f 1 = 1.
  Lemma preserves_mult: x y, f (x * y) = f x * f y.
  Lemma preserves_plus: x y, f (x + y) = f x + f y.

  Instance: SemiRing B := semiringmor_b.

  Lemma preserves_2: f 2 = 2.

  Lemma preserves_3: f 3 = 3.

  Lemma preserves_4: f 4 = 4.

  Context `{!Injective f}.
  Instance injective_ne_0 x : PropHolds (x 0) PropHolds (f x 0).

  Lemma injective_ne_1 x : x 1 f x 1.
End semiringmor_props.

Hint Extern 12 (PropHolds (_ _ 0)) => eapply @injective_ne_0 : typeclass_instances.

Lemma stdlib_ring_theory R `{Ring R} :
  Ring_theory.ring_theory 0 1 (+) (.*.) (λ x y, x - y) (-) (=).

Section ring_props.
  Context `{Ring R}.

  Add Ring R: (stdlib_ring_theory R).

  Instance: LeftAbsorb (.*.) 0.

  Global Instance Ring_Semi: SemiRing R.

  Lemma opp_involutive x: - -x = x.
  Lemma plus_opp_r x: x + -x = 0.
  Lemma plus_opp_l x: -x + x = 0.
  Lemma opp_swap_r x y: x + - y = - (y - x).
  Lemma opp_swap_l x y: -x + y = - (x - y).
  Lemma opp_distr x y: - (x + y) = - x + - y.
  Lemma opp_mult a: -a = -1 * a.
  Lemma opp_mult_distr_l a b: -(a * b) = -a * b.
  Lemma opp_mult_distr_r a b: -(a * b) = a * -b.
  Lemma opp_mult_opp a b: -a * -b = a * b.
  Lemma opp_0: -0 = 0.

  Lemma equal_by_zero_sum x y : x + - y = 0 x = y.

  Lemma flip_opp_zero x : -x = 0 x = 0.

  Lemma flip_opp_ne_0 x : -x 0 x 0.

  Lemma opp_zero_prod_l x y : -x * y = 0 x * y = 0.

  Lemma opp_zero_prod_r x y : x * -y = 0 x * y = 0.

  Lemma units_dont_divide_zero (x: R) `{!RingMultInverse x} `{!RingUnit x}: ¬ ZeroDivisor x.

  Context `{!NoZeroDivisors R} `{ x y, Stable (x = y)}.

  Global Instance ring_mult_left_cancel: z, PropHolds (z 0) LeftCancellation (.*.) z.

  Global Instance: z, PropHolds (z 0) RightCancellation (.*.) z.
End ring_props.

Section integral_domain_props.
  Context `{IntegralDomain R}.

  Instance intdom_nontrivial_apart `{Apart R} `{!TrivialApart R} :
    PropHolds (1 0).
End integral_domain_props.

Hint Extern 6 (PropHolds (1 0)) => eapply @intdom_nontrivial_apart : typeclass_instances.

Section ringmor_props.
  Context `{Ring A} `{Ring B} {f : A B} `{!SemiRing_Morphism f}.

  Lemma preserves_opp x : f (- x) = - f x.

  Lemma preserves_minus x y : f (x - y) = f x - f y.

  Lemma injective_preserves_0 : ( x, f x = 0 x = 0) Injective f.
End ringmor_props.

Section from_another_ring.
  Context `{Ring A} `{Setoid B}
   `{plus : RingPlus B} `{RingZero B} `{mult : RingMult B} `{RingOne B} `{opp : GroupInv B}
    (f : B A) `{!Injective f}
    (plus_correct : x y, f (x + y) = f x + f y) (zero_correct : f 0 = 0)
    (mult_correct : x y, f (x * y) = f x * f y) (one_correct : f 1 = 1) (opp_correct : x, f (-x) = -f x).

  Instance: Setoid_Morphism f := injective_mor f.
  Add Ring A : (stdlib_ring_theory A).

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

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

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

  Lemma projected_ring: Ring B.
End from_another_ring.

Section from_stdlib_semiring_theory.
  Context
    `(H: @semi_ring_theory R zero one pl mu e)
    `{!@Setoid R e}
    `{!Proper (e ==> e ==> e) pl}
    `{!Proper (e ==> e ==> e) mu}.

  Add Ring R2: H.

  Definition from_stdlib_semiring_theory: @SemiRing R e pl mu zero one.
End from_stdlib_semiring_theory.

Section from_stdlib_ring_theory.
  Context
    `(H: @ring_theory R zero one pl mu mi op e)
    `{!@Setoid R e}
    `{!Proper (e ==> e ==> e) pl}
    `{!Proper (e ==> e ==> e) mu}
    `{!Proper (e ==> e) op}.

  Add Ring R3: H.

  Definition from_stdlib_ring_theory: @Ring R e pl mu zero one op.
End from_stdlib_ring_theory.

Section morphism_composition.
  Context (A B C: Type)
    `{!RingMult A} `{!RingPlus A} `{!RingOne A} `{!RingZero A} `{!Equiv A}
    `{!RingMult B} `{!RingPlus B} `{!RingOne B} `{!RingZero B} `{!Equiv B}
    `{!RingMult C} `{!RingPlus C} `{!RingOne C} `{!RingZero C} `{!Equiv C}
    (f: A B) (g: B C).

  Global Instance id_semiring_morphism `{!SemiRing A}: SemiRing_Morphism id := {}.

  Global Instance compose_semiring_morphisms `{!SemiRing_Morphism f} `{!SemiRing_Morphism g} :
    SemiRing_Morphism (g f).
End morphism_composition.

Instance semiring_morphism_proper {A B eA eB pA mA zA oA pB mB zB oB} :
  Proper ((=) ==> (=)) (@SemiRing_Morphism A B eA eB pA mA zA oA pB mB zB oB).