Div

Theorems about division in ring-like structures.

Division can be either:

multiplication by the inverse (ab⁻¹) or
partial division (with the property ab/b=a).

See module RingLike.Core explaining that.

Some of the theorems below require one or several properties:

rngl_has_inv T = true : that inversion (x⁻¹) exists,
rngl_mul_is_comm T = true : that the multiplication is commutative,
rngl_characteristic T = 0 : that the characteristics is 0,
rngl_characteristic T ≠ 1 : that the characteristics ≠ 1,
rngl_has_opp_or_psub T = true : that opposite or partial subtraction exists,
rngl_has_inv_or_pdiv T = true : that inversion or partial division exists.

See the module RingLike.Core for the general description of the ring-like library.

In general, it is not necessary to import the present module. The normal usage is to do:

    Require Import RingLike.Core.

which imports the present module and some other ones.

From Stdlib Require Import Utf8 Arith.
Require Import Structures.
Require Import Add.
Require Import Mul.

Section a.

Context {T : Type}.
Context {ro : ring_like_op T}.
Context {rp : ring_like_prop T}.

Theorem rngl_mul_inv_diag_l :
  rngl_has_inv T = true →
  ∀ a : T, a ≠ 0%L → (a⁻¹ × a = 1)%L.

Theorem rngl_mul_inv_diag_r :
  rngl_has_inv T = true →
  ∀ a : T, a ≠ 0%L → (a × a⁻¹ = 1)%L.

Theorem rngl_mul_inv_r :
  rngl_has_inv T = true →
  ∀ a b, (a × b⁻¹)%L = (a / b)%L.

Theorem rngl_div_diag :
  rngl_has_inv_or_pdiv T = true →
  ∀ a : T, a ≠ 0%L → (a / a = 1)%L.

Theorem rngl_mul_div :
  rngl_has_inv_or_pdiv T = true →
  ∀ a b : T, b ≠ 0%L → (a × b / b)%L = a.
Theorem rngl_mul_cancel_l :
  rngl_has_inv_or_pdiv_and_comm T = true →
  ∀ a b c, a ≠ 0%L
  → (a × b = a × c)%L
  → b = c.
Theorem rngl_mul_cancel_r :
  rngl_has_inv_or_pdiv T = true →
  ∀ a b c, c ≠ 0%L
  → (a × c = b × c)%L
  → a = b.

Theorem rngl_div_mul_mul_div :
  rngl_mul_is_comm T = true →
  rngl_has_inv T = true →
  ∀ a b c, (a / b × c = a × c / b)%L.

Theorem rngl_mul_div_r :
  rngl_mul_is_comm T = true →
  rngl_has_inv_or_pdiv T = true →
  ∀ a b : T, a ≠ 0%L → (a × b / a)%L = b.

Theorem rngl_div_0_l :
  rngl_has_opp_or_psub T = true →
  rngl_has_inv_or_pdiv T = true →
  ∀ a, a ≠ 0%L → (0 / a)%L = 0%L.

Theorem rngl_div_mul :
  rngl_has_inv T = true →
  ∀ a b, b ≠ 0%L → (a / b × b)%L = a.

Theorem rngl_div_div_swap :
  rngl_mul_is_comm T = true →
  rngl_has_inv T = true →
  ∀ a b c,
  (a / b / c = a / c / b)%L.

Theorem rngl_div_div_mul_mul :
  rngl_mul_is_comm T = true →
  rngl_has_inv T = true →
  ∀ a b c d,
  b ≠ 0%L
  → d ≠ 0%L
  → (a / b = c / d)%L ↔ (a × d = b × c)%L.
Theorem rngl_eq_mul_0_l :
  rngl_has_opp_or_psub T = true →
  rngl_has_inv_or_pdiv T = true →
  ∀ a b, (a × b = 0)%L → b ≠ 0%L → a = 0%L.

Theorem rngl_eq_mul_0_r :
  rngl_has_opp_or_psub T = true →
  rngl_has_inv_or_pdiv_and_comm T = true →
  ∀ a b, (a × b = 0)%L → a ≠ 0%L → b = 0%L.
Theorem rngl_neq_mul_0 :
  rngl_has_opp_or_psub T = true →
  rngl_has_inv_or_pdiv T = true →
  ∀ a b, (a ≠ 0 → b ≠ 0 → a × b ≠ 0)%L.

Theorem rngl_div_add_distr_r:
  rngl_has_inv T = true →
  ∀ a b c, ((a + b ) / c)%L = (a / c + b / c)%L.

Theorem rngl_div_sub_distr_r:
  rngl_has_opp T = true →
  rngl_has_inv T = true →
  ∀ a b c, ((a - b ) / c)%L = (a / c - b / c)%L.

Theorem rngl_inv_1 :
  rngl_has_inv T = true →
  rngl_has_opp_or_psub T = true ∨ rngl_characteristic T ≠ 1 →
  (1⁻¹ = 1)%L.

Theorem rngl_div_1_l :
  rngl_has_inv T = true →
  ∀ a, (1 / a = a⁻¹)%L.

Theorem rngl_div_1_r :
  rngl_has_inv_or_pdiv T = true →
  rngl_has_opp_or_psub T = true ∨ rngl_characteristic T ≠ 1 →
  ∀ a, (a / 1 = a)%L.

Theorem rngl_mul_div_assoc :
  rngl_has_inv T = true →
  ∀ a b c, (a × (b / c ) = a × b / c)%L.

Theorem rngl_div_compat_l :
  rngl_has_inv T = true →
  ∀ a b c, c ≠ 0%L → (a = b)%L → (a / c = b / c)%L.

Theorem rngl_inv_if_then_else_distr : ∀ (c : bool) a b,
  ((if c then a else b )⁻¹ = if c then a⁻¹ else b⁻¹)%L.

Theorem rngl_mul_move_1_r :
  rngl_has_inv T = true →
  ∀ a b : T, b ≠ 0%L → (a × b)%L = 1%L ↔ a = (b⁻¹)%L.
Theorem rngl_mul_move_l :
  rngl_mul_is_comm T = true →
  rngl_has_inv_or_pdiv T = true →
  ∀ a b c, a ≠ 0%L → (a × b)%L = c → b = (c / a)%L.

Theorem rngl_mul_move_r :
  rngl_has_inv_or_pdiv T = true →
  ∀ a b c, b ≠ 0%L → (a × b)%L = c → a = (c / b)%L.

Theorem rngl_inv_neq_0 :
  rngl_has_opp_or_psub T = true →
  rngl_has_inv T = true →
  ∀ a, a ≠ 0%L → (a⁻¹ ≠ 0)%L.

Theorem rngl_inv_involutive :
  rngl_has_opp_or_psub T = true →
  rngl_has_inv T = true →
  ∀ x, x ≠ 0%L → (x⁻¹⁻¹)%L = x.

Theorem rngl_inv_inj :
  rngl_has_opp_or_psub T = true →
  rngl_has_inv T = true →
  ∀ a b, a ≠ 0%L → b ≠ 0%L →(a⁻¹ = b⁻¹)%L → a = b.

Theorem rngl_inv_mul_distr :
  rngl_has_opp_or_psub T = true →
  rngl_has_inv T = true →
  ∀ a b, a ≠ 0%L → b ≠ 0%L →((a × b )⁻¹ = b⁻¹ × a⁻¹)%L.

Theorem rngl_div_div :
  rngl_has_opp_or_psub T = true →
  rngl_has_inv T = true →
  ∀ a b c, (b ≠ 0 → c ≠ 0 → a / b / c = a / (c × b ))%L.

Theorem rngl_div_div_r :
  rngl_has_opp_or_psub T = true →
  rngl_has_inv T = true →
  ∀ a b c,
  b ≠ 0%L
  → c ≠ 0%L
  → (a / (b / c ) = a × c / b)%L.

Theorem rngl_opp_inv :
  rngl_has_opp T = true →
  rngl_has_inv T = true →
  ∀ a, a ≠ 0%L → (- a⁻¹ = (- a )⁻¹)%L.
Theorem rngl_div_mul_div :
  rngl_has_inv T = true →
  ∀ x y z, y ≠ 0%L → ((x / y ) × (y / z ))%L = (x / z)%L.

Theorem eq_rngl_div_1 :
  rngl_has_inv_or_pdiv T = true →
   ∀ a b, b ≠ 0%L → a = b → (a / b = 1)%L.

Theorem eq_rngl_add_same_0 :
  rngl_has_opp_or_psub T = true →
  rngl_has_inv_or_pdiv T = true →
  rngl_characteristic T = 0 →
  ∀ a,
  (a + a = 0)%L
  → a = 0%L.

Theorem rngl_pow_neq_0 :
  rngl_has_opp_or_psub T = true →
  rngl_has_inv_or_pdiv T = true →
  ∀ a n, (a ≠ 0 → a ^ n ≠ 0)%L.

Theorem rngl_squ_inv :
  rngl_has_opp_or_psub T = true →
  rngl_has_inv T = true →
  ∀ a, (a ≠ 0 → (a⁻¹ )² = (a ² )⁻¹)%L.

Theorem rngl_squ_div :
  rngl_mul_is_comm T = true →
  rngl_has_opp_or_psub T = true →
  rngl_has_inv T = true →
  ∀ a b, b ≠ 0%L → (a / b )²%L = (a ² / b ²)%L.

Theorem rngl_div_opp_l :
  rngl_has_opp T = true →
  rngl_has_inv T = true →
  ∀ a b, (- a / b = - (a / b ))%L.

Theorem rngl_div_opp_r :
  rngl_has_opp T = true →
  rngl_has_inv T = true →
  ∀ a b, b ≠ 0%L → (a / - b = - (a / b ))%L.

Theorem rngl_div_opp_opp :
  rngl_has_opp T = true →
  rngl_has_inv T = true →
  ∀ a b, (b ≠ 0 → - a / - b = a / b)%L.

Theorem rngl_inv_pow :
  rngl_has_opp_or_psub T = true →
  rngl_has_inv T = true →
  ∀ x n, x ≠ 0%L → ((x ^ n )⁻¹ = x⁻¹ ^ n)%L.

End a.

For the Rocq tactic "ring"

The Rocq tactics "ring" and "ring_simplify" help to directly simplify some kinds of expressions in the "ring" world. It can be applied to ring-like structures, providing the following code is added:

  From Stdlib Require Import Ring.
  Section a.
  Context {T : Type}.
  Context {ro : ring_like_op T}.
  Context {rp : ring_like_prop T}.
  Context {Hic : rngl_mul_is_comm T = true}.
  Context {Hop : rngl_has_opp T = true}.
  Add Ring rngl_ring : (rngl_ring_theory Hic Hop).

A typical example (you must stay in this section):

  Example a2_b2 : ∀ a b, ((a + b) * (a - b) = a * a - b * b)%L.
  Proof.
  intros.
  ring_simplify. (* just to see what happens *)
  easy.
  Qed.

From Stdlib Require Import Ring_theory.
From Stdlib Require Import Field_theory.

Section a.

Context {T : Type}.
Context {ro : ring_like_op T}.
Context {rp : ring_like_prop T}.
Context (Hic : rngl_mul_is_comm T = true).
Context (Hop : rngl_has_opp T = true).

Definition rngl_ring_theory
    : ring_theory 0%L 1%L rngl_add rngl_mul rngl_sub rngl_opp eq :=
  {| Radd_0_l := rngl_add_0_l;
     Radd_comm := rngl_add_comm;
     Radd_assoc := rngl_add_assoc;
     Rmul_1_l := rngl_mul_1_l;
     Rmul_comm := rngl_mul_comm Hic;
     Rmul_assoc := rngl_mul_assoc;
     Rdistr_l := rngl_mul_add_distr_r;
     Rsub_def x y := eq_sym (rngl_add_opp_r Hop x y);
     Ropp_def := rngl_add_opp_diag_r Hop |}.

Context (Hiv : rngl_has_inv T = true).
Context (Hc1 : rngl_characteristic T ≠ 1).

Definition rngl_field_theory :
  field_theory 0%L 1%L rngl_add rngl_mul rngl_sub rngl_opp
    rngl_div rngl_inv eq :=
  {| F_R := rngl_ring_theory;
     F_1_neq_0 := rngl_1_neq_0 Hc1;
     Fdiv_def := rngl_div_eq_inv_r Hiv;
     Finv_l := rngl_mul_inv_diag_l Hiv |}.

Commutative field

Define the typical properties of what a commutative field in mathematics is.

Record charac_0_field :=
  { cf_mul_is_comm : rngl_mul_is_comm T = true;
    cf_has_opp : rngl_has_opp T = true;
    cf_has_inv : rngl_has_inv T = true;
    cf_has_eq_dec : rngl_has_eq_dec T = true;
    cf_characteristic : rngl_characteristic T = 0 }.

End a.

Arguments rngl_div_add_distr_r {T ro rp} Hiv (a b c)%_L.
Arguments rngl_div_diag {T ro rp} Hiq a%_L.
Arguments rngl_div_mul {T ro rp} Hiv (a b)%_L.
Arguments rngl_div_opp_opp {T ro rp} Hop Hiv (a b)%_L.
Arguments rngl_div_1_l {T ro rp} Hiv a%_L.
Arguments rngl_mul_cancel_r {T ro rp} Hi1 (a b c)%_L.
Arguments rngl_mul_div {T ro rp} Hiv (a b)%_L.
Arguments rngl_mul_inv_r {T ro} Hiv (a b)%_L.

Arguments charac_0_field T%_type {ro rp}.

This page has been generated by coqdoc