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.
Complements on the ring algebraic structure.
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.
Let K : Ring.
Let x y : K.
This module may be used through the import of Algebra.Ring.Ring,
Algebra.Algebra, or Algebra.Algebra_wDep, where it is exported.
Brief description
Description
Additional definitions
- 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
- classic, the weak form of excluded middle;
- classic_dec, an alias for excluded_middle_informative, the strong form of excluded middle;
- ex_EX, an alias for constructive_indefinite_description.
Usage
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 Hx ⇒ proj1_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. move⇒ x /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.
move⇒ x 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 i ⇒ x × 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 i ⇒ u 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; rewrite → Rinv_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.