Library Algebra.Ring.Ring_compl

This file is part of the Coq Numerical Analysis library
Copyright (C) Boldo, Clément, Martin, Mayero, Mouhcine
This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details.

Brief description

Complements on the ring algebraic structure.

Description

The Ring algebraic structure is defined in the Coquelicot library, including the canonical structure prod_Ring for the cartesian product of rings.
Results needing a commutative Ring are only stated for the ring of real numbers R_Ring.

Additional definitions

Let K : Ring. Let x y : K.
  • is_inverse x y states that y is the left and right inverse of x;
  • invertible x states that x has a left and right inverse;
  • inv x is the inverse of x if it is invertible, and 0 otherwise;
  • div is the multiplication by the inverse.
  • notation / x is for inv x;
  • notation x / y is for div x y.
  • is_comm K states that mult is commutative, ie K is a commutative ring;
  • is_integral K states that multiplication of nonzero elements is nonzero;
  • has_inv K states that all nonzero elements are invertible; ie have an inverse;
  • is_field K states that K is not reduced to zero and that all nonzero elements have an inverse, ie that K is a field;
  • is_comm_field K states that K is a commutative field.

Used logic axioms

Usage

This module may be used through the import of Algebra.Ring.Ring, Algebra.Algebra, or Algebra.Algebra_wDep, where it is exported.

From Requisite Require Import stdlib_wR ssr_wMC.

From Coquelicot Require Import Hierarchy.
Close Scope R_scope.

From Subsets Require Import Subsets_wDep.
From Algebra Require Import Hierarchy_compl Monoid Group.

Local Open Scope Monoid_scope.
Local Open Scope Group_scope.
Local Open Scope Ring_scope.

Section Ring_Def1.

Context {K : Ring}.

Definition is_inverse (x y : K) : Prop := y × x = 1 x × y = 1.

Lemma is_inverse_comm : x y, is_inverse x y is_inverse y x.
Proof. move=>> [H1 H2]; easy. Qed.

Lemma is_inverse_compat_l :
   x1 x2 y, x1 = x2 is_inverse x1 y is_inverse x2 y.
Proof. intros; subst; easy. Qed.

Lemma is_inverse_compat_r :
   y1 y2 x, y1 = y2 is_inverse x y1 is_inverse x y2.
Proof. intros; subst; easy. Qed.

Lemma is_inverse_uniq :
   x y1 y2, is_inverse x y1 is_inverse x y2 y1 = y2.
Proof.
intros x y1 y2 [Hy1 _] [_ Hy2].
rewrite -(mult_one_r y1) -Hy2 mult_assoc Hy1 mult_one_l; easy.
Qed.

Inductive invertible (x : K) : Prop :=
  | Invertible : y, is_inverse x y invertible x.

Lemma invertible_ext :
   {x} (y : K), x = y invertible x invertible y.
Proof. intros; subst; easy. Qed.

Lemma invertible_ex : {x}, ( y, is_inverse x y) invertible x.
Proof. intros x [y Hy]; apply (Invertible _ _ Hy). Qed.

Lemma invertible_EX : {x}, invertible x { y | is_inverse x y }.
Proof. move=>> Hx; apply ex_EX; destruct Hx as [y Hy]; y; easy. Defined.

Lemma invertible_dec : x, { invertible x } + { ¬ invertible x }.
Proof. intros; apply classic_dec. Qed.

Definition inv (x : K) : K :=
  match invertible_dec x with
  | left Hxproj1_sig (invertible_EX Hx)
  | right _ ⇒ 0
  end.

Definition div (x y : K) : K := x × inv y.

Lemma inv_correct : {x y}, is_inverse x y inv x = y.
Proof.
intros x y H; apply (is_inverse_uniq x); try easy.
unfold inv; destruct (invertible_dec _) as [H' | H'].
apply (proj2_sig (invertible_EX _)).
contradict H'; apply (Invertible _ _ H).
Qed.

Lemma inv_correct_rev :
   {x y}, invertible x y = inv x is_inverse x y.
Proof.
move=>> [y' Hy'] Hy; rewrite Hy; apply (is_inverse_compat_r y'); try easy.
apply eq_sym, inv_correct; easy.
Qed.

Lemma div_eq : x y : K, div x y = x × inv y.
Proof. easy. Qed.

End Ring_Def1.

Notation "/ x" := (inv x) : Ring_scope.
Notation "x / y" := (div x y) : Ring_scope.

Section Ring_Def2.

Variable K : Ring.

Definition is_comm : Prop := (x y : K), x × y = y × x.


Definition is_integral : Prop :=
   (x y : K), x 0 y 0 x × y 0.

Definition has_inv : Prop := (x : K), x 0 invertible x.

Definition is_field : Prop := nonzero_struct K has_inv.

Definition is_comm_field : Prop := is_comm is_field.

End Ring_Def2.

Section Ring_Facts1.

Context {K : Ring}.

Lemma inhabited_r : inhabited K.
Proof. apply inhabited_g. Qed.

Lemma inhabited_fct_r : {T : Type}, inhabited (T K).
Proof. intros; apply inhabited_fct_g. Qed.

Lemma one_is_zero : (1 : K) = 0 zero_struct K.
Proof. intros H x; rewrite -(mult_one_l x) H mult_zero_l; easy. Qed.

Lemma one_not_zero : nonzero_struct K (1 : K) 0.
Proof.
intros [x Hx]; generalize Hx; rewrite -contra_equiv.
intros; apply one_is_zero; easy.
Qed.

Lemma one_is_zero_equiv : (1 : K) = 0 zero_struct K.
Proof. split; [apply one_is_zero | easy]. Qed.

Lemma one_not_zero_equiv : (1 : K) 0 nonzero_struct K.
Proof. split; [intros; 1; easy | apply one_not_zero]. Qed.

Lemma minus_one_not_zero : nonzero_struct K - (1 : K) 0.
Proof.
intros; rewrite -opp_zero; apply opp_neq_compat, one_not_zero; easy.
Qed.

Lemma mult_compat_l : x x1 x2 : K, x1 = x2 x × x1 = x × x2.
Proof. move=>> H; rewrite H; easy. Qed.

Lemma mult_compat_r : x x1 x2 : K, x1 = x2 x1 × x = x2 × x.
Proof. move=>> H; rewrite H; easy. Qed.

Lemma mult_zero_rev_l :
   x1 x2 : K, x1 × x2 = 0 ¬ invertible x1 x2 = 0.
Proof.
intros x1 x2 H.
destruct (classic (invertible x1)) as [[y1 [H1 _]] | H1]; [right | now left].
rewrite -(mult_one_l x2) -H1 -mult_assoc H mult_zero_r; easy.
Qed.

Lemma mult_zero_rev_r :
   x1 x2 : K, x1 × x2 = 0 x1 = 0 ¬ invertible x2.
Proof.
intros x1 x2 H.
destruct (classic (invertible x2)) as [[y2 [_ H2]] | H2]; [left | now right].
rewrite -(mult_one_r x1) -H2 mult_assoc H mult_zero_l; easy.
Qed.

Lemma mult_not_zero_l :
   x1 x2 : K, invertible x1 x2 0 x1 × x2 0.
Proof. move=>> H1 H2 H; destruct (mult_zero_rev_l _ _ H); easy. Qed.

Lemma mult_not_zero_r :
   x1 x2 : K, x1 0 invertible x2 x1 × x2 0.
Proof. move=>> H1 H2 H; destruct (mult_zero_rev_r _ _ H); easy. Qed.

Lemma mult_reg_l :
   x x1 x2 : K, invertible x x × x1 = x × x2 x1 = x2.
Proof.
move=>> [y [Hy _]] /(mult_compat_l y) Hx.
rewrite 2!mult_assoc Hy 2!mult_one_l in Hx; easy.
Qed.

Lemma mult_reg_r :
   x x1 x2 : K, invertible x x1 × x = x2 × x x1 = x2.
Proof.
move=>> [y [_ Hy]] /(mult_compat_r y) Hx.
rewrite -2!mult_assoc Hy 2!mult_one_r in Hx; easy.
Qed.

Lemma mult_minus_distr_l : x y1 y2 : K, x × (y1 - y2) = x × y1 - x × y2.
Proof. intros; rewrite !minus_eq opp_mult_r; apply mult_distr_l. Qed.

Lemma mult_minus_distr_r : x1 x2 y : K, (x1 - x2) × y = x1 × y - x2 × y.
Proof. intros; rewrite !minus_eq opp_mult_l; apply mult_distr_r. Qed.

Lemma is_inverse_sym : x y : K, is_inverse x y is_inverse y x.
Proof. move=>> [H1 H2]; easy. Qed.

Lemma is_inverse_sym_equiv : x y : K, is_inverse x y is_inverse y x.
Proof. intros; split; apply is_inverse_sym. Qed.

Lemma is_inverse_zero_struct : x y : K, zero_struct K is_inverse x y.
Proof.
intros x y HK; split; rewrite (HK x) (HK y) (HK 1); apply mult_zero_l.
Qed.

Lemma invertible_zero_struct : x : K, zero_struct K invertible x.
Proof. movex /is_inverse_zero_struct Hx; apply (Invertible x 0); easy. Qed.

Lemma invertible_zero : invertible (0 : K) zero_struct K.
Proof.
intros [z [_ H]]; rewrite mult_zero_l in H; apply one_is_zero; easy.
Qed.

Lemma is_inverse_zero : x : K, is_inverse 0 x zero_struct K.
Proof. move=>> Hx; apply invertible_zero; apply (Invertible _ _ Hx). Qed.

Lemma invertible_one : invertible (1 : K).
Proof. apply (Invertible _ 1); split; apply mult_one_l. Qed.

Lemma invertible_eq_one : {a : K}, a = 1 invertible a.
Proof. intros; subst; apply invertible_one. Qed.

Lemma noninvertible_zero : nonzero_struct K ¬ invertible (0 : K).
Proof. intros [x0 Hx0]; contradict Hx0; apply invertible_zero; easy. Qed.

Lemma is_inverse_nonzero_l :
   x y : K, nonzero_struct K is_inverse x y x 0.
Proof.
move=>> HK; apply contra_not_r_equiv.
intros; subst; move⇒ [_ H]; contradict H.
rewrite mult_zero_l; apply not_eq_sym, one_not_zero; easy.
Qed.

Lemma is_inverse_nonzero_r :
   x y : K, nonzero_struct K is_inverse x y y 0.
Proof. move=>> HK /is_inverse_sym; apply is_inverse_nonzero_l; easy. Qed.

Lemma is_inverse_invertible_l : x y : K, is_inverse x y invertible x.
Proof. intros x y H; apply (Invertible x y H). Qed.

Lemma is_inverse_invertible_r : x y : K, is_inverse x y invertible y.
Proof. move=>> /is_inverse_sym; apply is_inverse_invertible_l. Qed.

Lemma inv_0 : / (0 : K) = 0.
Proof.
unfold inv; destruct (invertible_dec _); try easy.
apply invertible_zero; easy.
Qed.

Lemma mult_invertible_compat :
   x y : K, invertible x invertible y invertible (x × y).
Proof.
move=>> [x1 [Hxa Hxb]] [y1 [Hya Hyb]]; apply (Invertible _ (y1 × x1)); split.
rewrite -mult_assoc (mult_assoc x1) Hxa mult_one_l; easy.
rewrite -mult_assoc (mult_assoc _ y1) Hyb mult_one_l; easy.
Qed.

Lemma mult_invertible_reg_l :
   x y : K, invertible y invertible (x × y) invertible x.
Proof.
intros x y Hy [z [Hza Hzb]]; apply (Invertible _ (y × z)); split.
generalize Hy; intros [y1 Hy1].
apply (mult_reg_l y1); try now apply (is_inverse_invertible_r y).
apply (mult_reg_r y); try easy.
destruct Hy1 as [Hy1 _].
rewrite 2!mult_assoc Hy1 mult_one_l mult_one_r -mult_assoc Hy1; easy.
rewrite mult_assoc; easy.
Qed.

Lemma mult_invertible_reg_r :
   x y : K, invertible x invertible (x × y) invertible y.
Proof.
intros x y Hx [z [Hza Hzb]]; apply (Invertible _ (z × x)); split.
rewrite -mult_assoc; easy.
generalize Hx; intros [x1 Hx1].
apply (mult_reg_l x); try easy.
apply (mult_reg_r x1); try now apply (is_inverse_invertible_r x).
destruct Hx1 as [_ Hx1].
rewrite mult_assoc -mult_assoc -(mult_assoc z) Hx1 !mult_one_r Hx1; easy.
Qed.

Lemma mult_invertible_equiv_l :
   x y : K, invertible y invertible (x × y) invertible x.
Proof.
intros; split.
apply mult_invertible_reg_l; easy.
intros; apply mult_invertible_compat; easy.
Qed.

Lemma mult_invertible_equiv_r :
   x y : K, invertible x invertible (x × y) invertible y.
Proof.
intros; split.
apply mult_invertible_reg_r; easy.
intros; apply mult_invertible_compat; easy.
Qed.

Lemma mult_inv_l : {x : K}, invertible x / x × x = 1.
Proof. intros x [y Hy]; rewrite (inv_correct Hy); apply Hy. Qed.

Lemma mult_inv_r : {x : K}, invertible x x × / x = 1.
Proof. intros x [y Hy]; rewrite (inv_correct Hy); apply Hy. Qed.

Lemma is_inverse_inv_r : {x : K}, invertible x is_inverse x (/ x).
Proof. intros x Hx; apply (inv_correct_rev Hx); easy. Qed.

Lemma is_inverse_inv_l : {x : K}, invertible x is_inverse (/ x) x.
Proof. intros; apply is_inverse_sym, is_inverse_inv_r; easy. Qed.

Lemma inv_invertible : {x : K}, invertible x invertible (/ x).
Proof. intros x Hx; apply (Invertible _ x), (is_inverse_inv_l Hx). Qed.

Lemma inv_invol : {x : K}, invertible x / (/ x) = x.
Proof. intros; apply inv_correct, is_inverse_inv_l; easy. Qed.

Lemma div_eq_one : {x : K}, invertible x x / x = 1.
Proof. move=>>; apply mult_inv_r. Qed.

Lemma div_one_compat : {x y : K}, invertible y x = y x / y = 1.
Proof. move=>> Hy ->; apply div_eq_one; easy. Qed.

Lemma div_one_reg : {x y : K}, invertible y x / y = 1 x = y.
Proof.
movex y Hy /(mult_compat_r y); rewrite -mult_assoc (mult_inv_l Hy).
rewrite mult_one_l mult_one_r; easy.
Qed.

Lemma div_one_equiv : {x y : K}, invertible y x / y = 1 x = y.
Proof. intros; split; [apply div_one_reg | apply div_one_compat]; easy. Qed.

Lemma mult_sum_distr_l :
   {n} x (u : 'K^n), x × sum u = sum (fun ix × u i).
Proof.
intros n; induction n as [| n Hn]; intros.
rewrite !sum_nil; apply mult_zero_r.
rewrite !sum_ind_l mult_distr_l Hn; easy.
Qed.

Lemma mult_sum_distr_r :
   {n} x (u : 'K^n), sum u × x = sum (fun iu i × x).
Proof.
intros n; induction n as [| n Hn]; intros.
rewrite !sum_nil; apply mult_zero_l.
rewrite !sum_ind_l mult_distr_r Hn; easy.
Qed.

Lemma sum_nil_noninvertible :
   (u : 'K^0), nonzero_struct K ¬ invertible (sum u).
Proof. move=>>; rewrite sum_nil; apply noninvertible_zero. Qed.

Lemma invertible_sum_nonnil :
   {n} (u : 'K^n),
    nonzero_struct K invertible (sum u) n 0%nat.
Proof.
move=>> HK; apply contra_not_r_equiv; intros; subst.
apply sum_nil_noninvertible; easy.
Qed.

Lemma sum_singleF_invertible :
   {a : K}, invertible a invertible (sum (singleF a)).
Proof. move=>>; rewrite sum_singleF; easy. Qed.

Lemma invertible_sum_equiv :
   {n} (u : 'K^n),
    invertible (sum u) invertible (sum (filter_n0F u)).
Proof. intros; rewrite sum_filter_n0F; easy. Qed.

Lemma sum_insertF_baryc :
   {n} (u : 'K^n) i0, sum (insertF u (1 - sum u) i0) = 1.
Proof. intros; rewrite sum_insertF plus_minus_l; easy. Qed.

Lemma invertible_sum_squeezeF :
   {n} (u : 'K^n.+1) {i0 i1},
    i1 i0 invertible (sum u) invertible (sum (squeezeF u i0 i1)).
Proof. intros; rewrite sum_squeezeF; easy. Qed.

Lemma is_integral_contra :
  is_integral K (x y : K), x × y = 0 x = 0 y = 0.
Proof.
split; intros HK x y.
rewrite contra_equiv not_or_equiv; intros; apply HK; easy.
intros H1 H2; contradict H1; destruct (HK _ _ H1); easy.
Qed.

End Ring_Facts1.

Section Ring_Facts2.

Context {T : Type}.
Context {K : Ring}.

Lemma fct_inv_eq : {f : T K} t, invertible f (/ f) t = / f t.
Proof.
intros; apply eq_sym, inv_correct; split;
    rewrite -fct_mult_eq; [rewrite mult_inv_l | rewrite mult_inv_r]; easy.
Qed.

Lemma fct_div_eq :
   (f : T K) {g} t, invertible g (f / g) t = f t / g t.
Proof. intros; unfold div; rewrite -fct_inv_eq; easy. Qed.

End Ring_Facts2.

Section Ring_R_Facts.

Lemma one_eq_R : 1 = 1%R.
Proof. easy. Qed.

Lemma nonzero_struct_R : nonzero_struct R_AbelianGroup.
Proof. 1; unfold one, zero; simpl; easy. Qed.

Lemma one_not_zero_R : (1 : R_Ring) 0.
Proof. apply one_not_zero, nonzero_struct_R. Qed.

Lemma minus_one_not_zero_R : - (1 : R_Ring) 0.
Proof. apply minus_one_not_zero, nonzero_struct_R. Qed.

Lemma is_inverse_Rinv : a, a 0 is_inverse a (/ a)%R.
Proof.
intros; unfold is_inverse, mult; simpl; rewriteRinv_l, Rinv_r; easy.
Qed.

Lemma inv_eq_R : a, / a = (/ a)%R.
Proof.
intros; destruct (Req_dec a 0) as [Ha | Ha].
rewrite Ha inv_0 Rinv_0; easy.
apply inv_correct, is_inverse_Rinv; easy.
Qed.

Lemma div_eq_R : a b, a / b = (a / b)%R.
Proof. intros; unfold div, Rdiv; rewrite inv_eq_R; easy. Qed.

Lemma invertible_equiv_R : a : R, invertible a a 0.
Proof.
intros; split; intros Ha.
contradict Ha; rewrite Ha; apply (noninvertible_zero nonzero_struct_R).
apply (Invertible _ (/ a)); rewrite inv_eq_R; apply is_inverse_Rinv; easy.
Qed.

Lemma non_invertible_equiv_R : a : R, ¬ invertible a a = 0.
Proof. intros; rewrite -iff_not_r_equiv; apply invertible_equiv_R. Qed.

Lemma invertible_2 : invertible 2%R.
Proof. apply invertible_equiv_R; easy. Qed.

Lemma mult_comm_R : is_comm R_Ring.
Proof. intro; unfold mult; simpl; apply Rmult_comm. Qed.

Lemma mult_pos_R : a : R, (0 a × a)%R.
Proof. unfold mult; simpl; apply Rle_0_sqr. Qed.

Lemma mult_inv_l_R : a : R, a 0 (/ a)%R × a = 1.
Proof.
intros; rewrite -inv_eq_R; apply mult_inv_l; apply invertible_equiv_R; easy.
Qed.

Lemma mult_inv_r_R : a : R, a 0 a × (/ a)%R = 1.
Proof.
intros; rewrite -inv_eq_R; apply mult_inv_r; apply invertible_equiv_R; easy.
Qed.

Lemma is_inverse_nonzero_l_R : a b : R, is_inverse a b a 0.
Proof. move=>>; apply (is_inverse_nonzero_l _ _ nonzero_struct_R). Qed.

Lemma is_inverse_nonzero_r_R : a b : R, is_inverse a b b 0.
Proof. move=>>; apply (is_inverse_nonzero_r _ _ nonzero_struct_R). Qed.

Lemma is_inverse_equiv_R : a : R, is_inverse a (/ a)%R a 0.
Proof.
intros; split; try apply is_inverse_nonzero_l_R.
split; [apply mult_inv_l_R | apply mult_inv_r_R]; easy.
Qed.

Lemma is_integral_contra_R :
   (x y : R_Ring), x × y = 0 x = 0 y = 0.
Proof. apply Rmult_integral. Qed.

Lemma is_integral_R : is_integral R_Ring.
Proof. apply is_integral_contra, is_integral_contra_R. Qed.

Lemma has_inv_R : has_inv R_Ring.
Proof. move=>> /is_inverse_equiv_R H; apply (Invertible _ _ H). Qed.

Lemma is_comm_field_R : is_comm_field R_Ring.
Proof.
repeat split. apply mult_comm_R. apply nonzero_struct_R. apply has_inv_R.
Qed.

End Ring_R_Facts.