theory.dec_fields

Require Import
  Field Ring
  abstract_algebra theory.fields theory.strong_setoids.
Require Export
  theory.rings.

Section contents.
Context `{DecField F} `{ x y: F, Decision (x = y)}.

Add Ring F : (stdlib_ring_theory F).

Global Instance: ZeroProduct F.

Global Instance: IntegralDomain F.

Lemma dec_mult_inv_1: / 1 = 1.

Lemma dec_mult_inv_distr (x y: F): / (x * y) = / x * / y.

Lemma dec_mult_inv_zero x : / x = 0 x = 0.

Lemma dec_mult_inv_ne_0_iff x : / x 0 x 0.

Instance dec_mult_inv_ne_0 x : PropHolds (x 0) PropHolds (/x 0).

Lemma equal_by_one_quotient (x y : F) : x / y = 1 x = y.

Global Instance dec_mult_inv_inj: Injective (/).

Lemma dec_mult_inv_involutive x : / / x = x.

Lemma equal_dec_quotients (a b c d : F) : b 0 d 0 (a * d = c * b a / b = c / d).

Lemma dec_quotients (a c b d : F) : b 0 d 0 a / b + c / d = (a * d + c * b) / (b * d).

Lemma dec_mult_inv_swap_l x y: x / y = / (/ x * y).

Lemma dec_mult_inv_swap_r x y: / x * y = / (x / y).

Lemma dec_mult_inv_opp x : -(/ x) = / (-x).
End contents.

Hint Extern 7 (PropHolds (/ _ 0)) => eapply @dec_mult_inv_ne_0 : typeclass_instances.

Section is_field.
  Context `{DecField F} `{Apart F} `{!TrivialApart F} `{ x y: F, Decision (x = y)}.

  Global Program Instance mult_inv_dec_field: MultInv F := λ x, /`x.

  Instance: StrongSetoid F := dec_strong_setoid.

  Global Instance: Field F.

  Lemma dec_mult_inv_correct (x : F) Px : / x = // xPx.
End is_field.

Definition stdlib_field_theory F `{DecField F} :
  Field_theory.field_theory 0 1 (+) (.*.) (λ x y, x - y) (-) (λ x y, x / y) (/) (=).

Section from_stdlib_field_theory.
  Context `(ftheory : @field_theory F zero one pl mu mi op div rinv e)
    (rinv_0 : e (rinv zero) zero)
    `{!@Setoid F e}
    `{!Proper (e ==> e ==> e) pl}
    `{!Proper (e ==> e ==> e) mu}
    `{!Proper (e ==> e) rinv}
    `{!Proper (e ==> e) op}.

  Add Field F2 : ftheory.

  Definition from_stdlib_field_theory: @DecField F e pl mu zero one op rinv.
End from_stdlib_field_theory.

Section morphisms.
  Context `{DecField F} `{ x y: F, Decision (x = y)}.

  Global Instance dec_field_to_domain_inj `{IntegralDomain R}
    `{!SemiRing_Morphism (f : F R)} : Injective f.

  Lemma preserves_dec_mult_inv `{DecField F2} `{ x y: F2, Decision (x = y)}
    `{!SemiRing_Morphism (f : F F2)} x : f (/ x) = / f x.

  Lemma dec_mult_inv_to_mult_inv `{Field F2} `{!StrongSemiRing_Morphism (f : F F2)} x Pfx :
    f (/ x) = // (f x)↾Pfx.
End morphisms.