Library dvdring
This file is part of CoqEAL, the Coq Effective Algebra Library.
(c) Copyright INRIA and University of Gothenburg.
Require Import ssreflect ssrfun ssrbool eqtype ssrnat div seq path.
Require Import ssralg fintype perm tuple choice.
Require Import matrix bigop zmodp mxalgebra poly generic_quotient.
Import GRing.Theory.
Set Implicit Arguments.
Local Open Scope ring_scope.
Require Import ssralg fintype perm tuple choice.
Require Import matrix bigop zmodp mxalgebra poly generic_quotient.
Import GRing.Theory.
Set Implicit Arguments.
Local Open Scope ring_scope.
tools for Acc induction
Scheme acc_dep := Induction for Acc Sort Type.
Lemma lt_wf2 : well_founded (fun x y => x < y).
Section GUARD.
Variable A: Type.
Variable P : A -> A -> Prop.
Fixpoint guarded (n:nat) (Wf : well_founded P) : well_founded P :=
match n with
| O => Wf
| S n => fun x =>
(@Acc_intro _ _ x (fun y _ => guarded n (guarded n Wf) y))
end.
End GUARD.
Explicit divisibility ring
Module DvdRing.
CoInductive div_spec (R : ringType) (a b :R) : option R -> Type :=
| DivDvd x of a = x * b : div_spec a b (Some x)
| DivNDvd of (forall x, a != x * b) : div_spec a b None.
Record mixin_of (R : ringType) : Type := Mixin {
div : R -> R -> option R;
_ : forall a b, div_spec a b (div a b)
}.
Section ClassDef.
Record class_of (R : Type) : Type := Class {
base : GRing.IntegralDomain.class_of R;
mixin : mixin_of (GRing.IntegralDomain.Pack base R)
}.
Local Coercion base : class_of >-> GRing.IntegralDomain.class_of.
Structure type : Type := Pack {sort : Type; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
Variable (T : Type) (cT : type).
Definition class := let: Pack _ c _ := cT return class_of cT in c.
Definition clone c of phant_id class c := @Pack T c T.
Definition pack b0 (m0 : mixin_of (@GRing.IntegralDomain.Pack T b0 T)) :=
fun bT b & phant_id (GRing.IntegralDomain.class bT) b =>
fun m & phant_id m m0 => Pack (@Class T b m) T.
Definition eqType := Equality.Pack class cT.
Definition choiceType := Choice.Pack class cT.
Definition zmodType := GRing.Zmodule.Pack class cT.
Definition ringType := GRing.Ring.Pack class cT.
Definition comRingType := GRing.ComRing.Pack class cT.
Definition unitRingType := GRing.UnitRing.Pack class cT.
Definition comUnitRingType := GRing.ComUnitRing.Pack class cT.
Definition idomainType := GRing.IntegralDomain.Pack class cT.
End ClassDef.
Module Exports.
Coercion base : class_of >-> GRing.IntegralDomain.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Canonical Structure eqType.
Coercion choiceType : type >-> Choice.type.
Canonical Structure choiceType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical Structure zmodType.
Coercion ringType : type >-> GRing.Ring.type.
Canonical Structure ringType.
Coercion comRingType : type >-> GRing.ComRing.type.
Canonical Structure comRingType.
Coercion unitRingType : type >-> GRing.UnitRing.type.
Canonical Structure unitRingType.
Coercion comUnitRingType : type >-> GRing.ComUnitRing.type.
Canonical Structure comUnitRingType.
Coercion idomainType : type >-> GRing.IntegralDomain.type.
Canonical Structure idomainType.
Notation dvdRingType := type.
Notation DvdRingType T m := (@pack T _ m _ _ id _ id).
Notation DvdRingMixin := Mixin.
Notation "[ 'dvdRingType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
(at level 0, format "[ 'dvdRingType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'dvdRingType' 'of' T ]" := (@clone T _ _ id)
(at level 0, format "[ 'dvdRingType' 'of' T ]") : form_scope.
End Exports.
End DvdRing.
Export DvdRing.Exports.
Definition odivr R := DvdRing.div (DvdRing.class R).
Definition dvdr R a b := @odivr R b a : bool.
Definition eqd (R : dvdRingType) (a b : R) := (dvdr a b) && (dvdr b a).
Definition sdvdr (R : dvdRingType) (x y : R) := (dvdr x y) && ~~(dvdr y x).
Module Notations.
Notation "%=R" := (@eqd _) : ring_scope.
Notation "a %= b" := (@eqd _ a b) (at level 70, no associativity): ring_scope.
Notation "%|%R" := (@dvdr _) : ring_scope.
Notation "a %| b" := (dvdr a b) : ring_scope.
Notation "%/?%R" := (@odivr _) : ring_scope.
Notation "a %/? b" := (odivr a b)
(at level 70, no associativity): ring_scope.
Notation "%<|R" := (@sdvdr _).
Notation "x %<| y" := (sdvdr x y) (at level 70, no associativity).
End Notations.
Export Notations.
Section DvdRingTheory.
Variable R : dvdRingType.
Implicit Types a b c : R.
CoInductive div_spec (R : ringType) (a b :R) : option R -> Type :=
| DivDvd x of a = x * b : div_spec a b (Some x)
| DivNDvd of (forall x, a != x * b) : div_spec a b None.
Record mixin_of (R : ringType) : Type := Mixin {
div : R -> R -> option R;
_ : forall a b, div_spec a b (div a b)
}.
Section ClassDef.
Record class_of (R : Type) : Type := Class {
base : GRing.IntegralDomain.class_of R;
mixin : mixin_of (GRing.IntegralDomain.Pack base R)
}.
Local Coercion base : class_of >-> GRing.IntegralDomain.class_of.
Structure type : Type := Pack {sort : Type; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
Variable (T : Type) (cT : type).
Definition class := let: Pack _ c _ := cT return class_of cT in c.
Definition clone c of phant_id class c := @Pack T c T.
Definition pack b0 (m0 : mixin_of (@GRing.IntegralDomain.Pack T b0 T)) :=
fun bT b & phant_id (GRing.IntegralDomain.class bT) b =>
fun m & phant_id m m0 => Pack (@Class T b m) T.
Definition eqType := Equality.Pack class cT.
Definition choiceType := Choice.Pack class cT.
Definition zmodType := GRing.Zmodule.Pack class cT.
Definition ringType := GRing.Ring.Pack class cT.
Definition comRingType := GRing.ComRing.Pack class cT.
Definition unitRingType := GRing.UnitRing.Pack class cT.
Definition comUnitRingType := GRing.ComUnitRing.Pack class cT.
Definition idomainType := GRing.IntegralDomain.Pack class cT.
End ClassDef.
Module Exports.
Coercion base : class_of >-> GRing.IntegralDomain.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Canonical Structure eqType.
Coercion choiceType : type >-> Choice.type.
Canonical Structure choiceType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical Structure zmodType.
Coercion ringType : type >-> GRing.Ring.type.
Canonical Structure ringType.
Coercion comRingType : type >-> GRing.ComRing.type.
Canonical Structure comRingType.
Coercion unitRingType : type >-> GRing.UnitRing.type.
Canonical Structure unitRingType.
Coercion comUnitRingType : type >-> GRing.ComUnitRing.type.
Canonical Structure comUnitRingType.
Coercion idomainType : type >-> GRing.IntegralDomain.type.
Canonical Structure idomainType.
Notation dvdRingType := type.
Notation DvdRingType T m := (@pack T _ m _ _ id _ id).
Notation DvdRingMixin := Mixin.
Notation "[ 'dvdRingType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
(at level 0, format "[ 'dvdRingType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'dvdRingType' 'of' T ]" := (@clone T _ _ id)
(at level 0, format "[ 'dvdRingType' 'of' T ]") : form_scope.
End Exports.
End DvdRing.
Export DvdRing.Exports.
Definition odivr R := DvdRing.div (DvdRing.class R).
Definition dvdr R a b := @odivr R b a : bool.
Definition eqd (R : dvdRingType) (a b : R) := (dvdr a b) && (dvdr b a).
Definition sdvdr (R : dvdRingType) (x y : R) := (dvdr x y) && ~~(dvdr y x).
Module Notations.
Notation "%=R" := (@eqd _) : ring_scope.
Notation "a %= b" := (@eqd _ a b) (at level 70, no associativity): ring_scope.
Notation "%|%R" := (@dvdr _) : ring_scope.
Notation "a %| b" := (dvdr a b) : ring_scope.
Notation "%/?%R" := (@odivr _) : ring_scope.
Notation "a %/? b" := (odivr a b)
(at level 70, no associativity): ring_scope.
Notation "%<|R" := (@sdvdr _).
Notation "x %<| y" := (sdvdr x y) (at level 70, no associativity).
End Notations.
Export Notations.
Section DvdRingTheory.
Variable R : dvdRingType.
Implicit Types a b c : R.
Properties of odivr
Lemma odivrP : forall a b, DvdRing.div_spec a b (a %/? b).
Lemma odiv0r : forall a, a != 0 -> 0 %/? a = Some 0.
Lemma odivr0 : forall a, a != 0 -> a %/? 0 = None.
Lemma odivr1 : forall a, a %/? 1 = Some a.
Lemma odivrr : forall a, a != 0 -> a %/? a = Some 1.
Lemma odivr_mulrK : forall a b, a != 0 -> b * a %/? a = Some b.
Lemma odivr_mulKr : forall a b, a != 0 -> a * b %/? a = Some b.
Lemma odivr_mul2l : forall a b c, a != 0 -> b != 0 ->
a * b %/? (a * c) = (b %/? c).
Lemma odivr_mul2r : forall a b c, a != 0 -> b != 0 ->
b * a %/? (c * a) = (b %/? c).
Lemma odivr_some : forall a b c, a %/? b = Some c -> a = b * c.
Properties of dvdr
Lemma dvdrP : forall a b, reflect (exists x, b = x * a) (a %| b).
Lemma eqdP (m n : R) : reflect (exists2 c12 : R,
(c12 \is a GRing.unit) & c12 * m = n)
(m %= n).
Lemma dvdrr : forall a, a %| a.
Hint Resolve dvdrr.
Lemma dvdr_trans : transitive (@dvdr R).
Lemma dvdr0 : forall a, a %| 0.
Lemma dvd0r : forall a, (0 %| a) = (a == 0) :> bool.
Lemma dvdr_add : forall a b c, a %| b -> a %| c -> a %| b + c.
Lemma dvdrN : forall a b, (a %| (-b)) = (a %| b).
Lemma dvdNr : forall a b, ((-a) %| b) = (a %| b).
Lemma dvdrNN : forall a b, ((-a) %| (-b)) = (a %| b).
Lemma dvdr_sub : forall a b c, a %| b -> a %| c -> a %| b - c.
Lemma dvdr_addl : forall a b c, (b %| a) -> (b %| c + a) = (b %| c).
Lemma dvdr_addr : forall a b c, (b %| a) -> (b %| a + c) = (b %| c).
Lemma dvdr_add_eq : forall a b c, (a %| b + c) -> (a %| b) = (a %| c).
Lemma dvdr_mull : forall c a b, a %| b -> a %| c * b.
Lemma dvdr_mulr : forall b a c, a %| c -> a %| c * b.
Lemma dvdr_mul : forall c d a b, a %| c -> b %| d -> a * b %| c * d.
Lemma dvdr_mul2r : forall c a b, c != 0 -> (a * c %| b * c) = (a %| b) :> bool.
Lemma dvdr_mul2l : forall c a b, c != 0 -> (c * a %| c * b) = (a %| b) :> bool.
Lemma dvd1r : forall a, 1 %| a.
Hint Resolve dvd1r.
Properties of eqd
Lemma eqd_def : forall a b, a %= b = (a %| b) && (b %| a).
Lemma eqdd : forall a, a %= a.
Hint Resolve eqdd.
Lemma eqd_sym : symmetric (@eqd R).
Hint Resolve eqd_sym.
Lemma eqd_trans : transitive (@eqd R).
Lemma congr_eqd : forall b d a c, a %= b -> c %= d -> (a %= c) = (b %= d).
Lemma eqdr0 : forall a, (a %= 0) = (a == 0).
Lemma eqd0r : forall a, (0 %= a) = (a == 0).
Lemma eq_eqd : forall a b, a = b -> a %= b.
Lemma eqd_mul : forall c d a b, a %= c -> b %= d -> a * b %= c * d.
Lemma eqd_mul2l : forall c a b, c != 0 -> (c * a %= c * b) = (a %= b).
Lemma eqd_mul2r : forall c a b, c != 0 -> (a * c %= b * c) = (a %= b).
Lemma eqd_dvd : forall c d a b, a %= c -> b %= d -> (a %| b) = (c %| d).
Lemma eqd_dvdr (q p d : R) : p %= q -> (d %| p) = (d %| q).
Lemma eqd_dvdl (q p d : R) : p %= q -> (p %| d) = (q %| d).
Lemma eqd_ltrans : left_transitive (@eqd R).
Lemma eqd_rtrans : right_transitive (@eqd R).
Lemma eqd_mulr (q p r : R) : p %= q -> p * r %= q * r.
Lemma eqd_mull (q p r : R) : p %= q -> r * p %= r * q.
Lemma dvdr1 : forall a, (a %| 1) = (a %= 1).
Lemma unitd1 : forall a, (a \in GRing.unit) = (a %= 1).
Lemma eqd1 : forall a, a \in GRing.unit -> a %= 1.
Lemma dvdUr : forall a b, a %= 1 -> a %| b.
Lemma dvdrU : forall b a, b %= 1 -> a %| b = (a %= 1).
Lemma dvdr_mulr_l: forall b a, b != 0 -> (a * b %| b) = (a %= 1).
Lemma dvdr_mull_l : forall b a, b != 0 -> (b * a %| b) = (a %= 1).
Properties of sdvdr
Lemma sdvdr_def : forall a b, a %<| b = (a %| b) && ~~(b %| a).
Lemma sdvdrW : forall a b, a %<| b -> a %| b.
Lemma sdvdrNW : forall a b, a %<| b -> ~~(b %| a).
Lemma sdvdr0 : forall a, a %<| 0 = (a != 0).
Lemma sdvd0r : forall a, 0 %<| a = false.
bigop
Lemma big_dvdr (I : finType) (d : R) (F : I -> R) (P : pred I) :
(forall i, d %| F i) -> d %| \sum_(i : I | P i) (F i).
Lemma eqd_big_mul n (P : pred 'I_n) (F1 F2 : 'I_n -> R) :
(forall i, P i -> F1 i %= F2 i) ->
\prod_(i | P i) F1 i %= \prod_(i | P i) F2 i.
Lemma eqd_big_mul1 n (P : pred 'I_n) (F : 'I_n -> R) :
\prod_(i < n | P i) F i %= 1 -> (forall i, P i -> F i %= 1).
End DvdRingTheory.
Hint Resolve dvdrr.
Hint Resolve dvd1r.
Hint Resolve eqdd.
Module GcdRing.
Record mixin_of (R : dvdRingType) : Type := Mixin {
gcd : R -> R -> R;
_ : forall a b g, g %| gcd a b = (g %| a) && (g %| b)
}.
Section ClassDef.
Record class_of (R : Type) : Type := Class {
base : DvdRing.class_of R;
mixin : mixin_of (DvdRing.Pack base R)
}.
Local Coercion base : class_of >-> DvdRing.class_of.
Structure type : Type := Pack {sort : Type; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
Variable (T : Type) (cT : type).
Definition class := let: Pack _ c _ := cT return class_of cT in c.
Definition clone c of phant_id class c := @Pack T c T.
Definition pack b0 (m0 : mixin_of (@DvdRing.Pack T b0 T)) :=
fun bT b & phant_id (DvdRing.class bT) b =>
fun m & phant_id m m0 => Pack (@Class T b m) T.
Definition eqType := Equality.Pack class cT.
Definition choiceType := Choice.Pack class cT.
Definition zmodType := GRing.Zmodule.Pack class cT.
Definition ringType := GRing.Ring.Pack class cT.
Definition comRingType := GRing.ComRing.Pack class cT.
Definition unitRingType := GRing.UnitRing.Pack class cT.
Definition comUnitRingType := GRing.ComUnitRing.Pack class cT.
Definition idomainType := GRing.IntegralDomain.Pack class cT.
Definition dvdRingType := DvdRing.Pack class cT.
End ClassDef.
Module Exports.
Coercion base : class_of >-> DvdRing.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Canonical Structure eqType.
Coercion choiceType : type >-> Choice.type.
Canonical Structure choiceType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical Structure zmodType.
Coercion ringType : type >-> GRing.Ring.type.
Canonical Structure ringType.
Coercion comRingType : type >-> GRing.ComRing.type.
Canonical Structure comRingType.
Coercion unitRingType : type >-> GRing.UnitRing.type.
Canonical Structure unitRingType.
Coercion comUnitRingType : type >-> GRing.ComUnitRing.type.
Canonical Structure comUnitRingType.
Coercion idomainType : type >-> GRing.IntegralDomain.type.
Canonical Structure idomainType.
Coercion dvdRingType : type >-> DvdRing.type.
Canonical Structure dvdRingType.
Notation gcdRingType := type.
Notation GcdRingType T m := (@pack T _ m _ _ id _ id).
Notation GcdRingMixin := Mixin.
Notation "[ 'gcdRingType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
(at level 0, format "[ 'gcdRingType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'gcdRingType' 'of' T ]" := (@clone T _ _ id)
(at level 0, format "[ 'gcdRingType' 'of' T ]") : form_scope.
End Exports.
End GcdRing.
Export GcdRing.Exports.
Definition gcdr R := GcdRing.gcd (GcdRing.class R).
Definition lcmr R a b := nosimpl
(if (a == 0) || (b == 0) then 0 else odflt 0 ((a * b) %/? (@gcdr R a b))).
Definition gcdsr R := foldr (@gcdr R) 0.
Definition lcmsr R := foldr (@lcmr R) 1.
Section GCDRingTheory.
Variable R : gcdRingType.
Implicit Types a b : R.
Lemma dvdr_gcd : forall g a b, g %| gcdr a b = (g %| a) && (g %| b) :> bool.
Lemma dvdr_gcdl : forall a b, gcdr a b %| a.
Lemma dvdr_gcdr : forall a b, gcdr a b %| b.
Lemma gcdr_eq0 : forall a b, (gcdr a b == 0) = (a == 0) && (b == 0).
Hint Resolve dvdr_gcdr.
Hint Resolve dvdr_gcdl.
Lemma gcdr_def : forall x a b, x %| a -> x %| b ->
(forall x', x' %| a -> x' %| b -> (x' %| x)) -> gcdr a b %= x.
Lemma gcdrC : forall a b, gcdr a b %= gcdr b a.
Hint Resolve gcdrC.
Lemma eqd_gcd : forall c d a b, a %= c -> b %= d -> gcdr a b %= gcdr c d.
Lemma gcd0r : forall a, gcdr 0 a %= a.
Lemma gcdr0 : forall a, gcdr a 0 %= a.
Lemma gcd1r : forall a, gcdr 1 a %= 1.
Lemma gcdr1 : forall a, gcdr a 1 %= 1.
Lemma gcdrA : forall a b c, gcdr a (gcdr b c) %= gcdr (gcdr a b) c.
Lemma gcdrCA : forall a b c, gcdr a (gcdr b c) %= gcdr b (gcdr a c).
Lemma gcdrAC : forall a b c, gcdr (gcdr a b) c %= gcdr (gcdr a c) b.
Lemma gcdr_mul2r : forall a b c, gcdr (a * c) (b * c) %= gcdr a b * c.
Lemma gcdr_mul2l : forall a b c, gcdr (c * a) (c * b) %= c * gcdr a b.
Lemma mulr_gcdr : forall a b c, a * gcdr b c %= gcdr (a * b) (a * c).
Lemma mulr_gcdl : forall a b c, gcdr a b * c %= gcdr (a * c) (b * c).
Lemma gcdr_addr_r : forall c a b, a %| b -> gcdr a (c + b) %= gcdr a c.
Lemma gcdr_addl_r : forall c a b, a %| b -> gcdr a (b + c) %= gcdr a c.
Lemma gcdr_addr_l : forall a b c, b %| c -> gcdr (a + c) b %= gcdr a b.
Lemma gcdr_addl_l : forall a b c, b %| c -> gcdr (c + a) b %= gcdr a b.
Lemma gcdr_addl_mul : forall a b m, gcdr a (a * m + b) %= gcdr a b.
Lemma dvdr_gcd_mul : forall a b, gcdr a b %| a * b.
Lemma mulr_lcm_gcd : forall a b, lcmr a b * gcdr a b = a * b.
Lemma lcmr0 : forall a, lcmr a 0 = 0.
Lemma lcm0r : forall a, lcmr 0 a = 0.
Lemma dvdr_lcm : forall a b c, (lcmr a b %| c) = (a %| c) && (b %| c) :> bool.
Lemma dvdr_lcml : forall a b, a %| lcmr a b.
Hint Resolve dvdr_lcml.
Lemma dvdr_lcmr : forall a b, b %| lcmr a b.
Hint Resolve dvdr_lcmr.
Lemma dvdr_gcdr_lcmr : forall a b, gcdr a b %| lcmr a b.
Lemma lcm1r : forall a, lcmr 1 a %= a.
Lemma lcmr1 : forall a, lcmr a 1 %= a.
Lemma lcmrC : forall a b, lcmr a b %= lcmr b a.
Lemma lcmrA : forall a b c, lcmr a (lcmr b c) %= lcmr (lcmr a b) c.
Lemma eqd_lcmr : forall a b c, a %= b -> lcmr a c %= lcmr b c.
Lemma eqd_lcml : forall a b c, a %= b -> lcmr c a %= lcmr c b.
Lemma lcmrCA : forall a b c, lcmr a (lcmr b c) %= lcmr b (lcmr a c).
Lemma lcmrAC : forall a b c, lcmr (lcmr a b) c %= lcmr (lcmr a c) b.
Lemma mulr_lcmr : forall a b c, a * lcmr b c %= lcmr (a * b) (a * c).
Lemma mulr_lcml : forall a b c, lcmr a b * c %= lcmr (a * c) (b * c).
Lemma lcmr_mul2r : forall a b c, lcmr (a * c) (b * c) %= lcmr a b * c.
Lemma lcmr_mul2l : forall a b c, lcmr (c * a) (c * b) %= c * lcmr a b.
Lemma lcmr_mull : forall a b, lcmr a (a * b) %= a * b.
Lemma lcmr_mulr : forall a b, lcmr b (a * b) %= a * b.
Lemma dvdr_lcm_idr : forall a b, a %| b -> lcmr a b %= b.
Lemma dvdr_lcm_idl : forall a b, b %| a -> lcmr a b %= a.
Lemma gcdsr0 : (@gcdsr R) [::] = 0.
Lemma gcdsr_cons : forall a s, gcdsr (a :: s) = gcdr a (gcdsr s).
Lemma dvdr_gcds : forall (l : seq R) (g : R), g %| gcdsr l = all (%|%R g) l.
Lemma dvdr_mem_gcds : forall (l : seq R) (x : R), x \in l -> gcdsr l %| x.
Lemma lcmsr0 : (@lcmsr R) [::] = 1.
Lemma lcmsr_cons : forall a s, lcmsr (a :: s) = lcmr a (lcmsr s).
Lemma dvdr_lcms : forall (l : seq R) (m : R), lcmsr l %| m = all (%|%R^~ m) l.
Lemma dvdr_mem_lcms : forall (l : seq R) (x : R), x \in l -> x %| lcmsr l.
(forall i, d %| F i) -> d %| \sum_(i : I | P i) (F i).
Lemma eqd_big_mul n (P : pred 'I_n) (F1 F2 : 'I_n -> R) :
(forall i, P i -> F1 i %= F2 i) ->
\prod_(i | P i) F1 i %= \prod_(i | P i) F2 i.
Lemma eqd_big_mul1 n (P : pred 'I_n) (F : 'I_n -> R) :
\prod_(i < n | P i) F i %= 1 -> (forall i, P i -> F i %= 1).
End DvdRingTheory.
Hint Resolve dvdrr.
Hint Resolve dvd1r.
Hint Resolve eqdd.
Module GcdRing.
Record mixin_of (R : dvdRingType) : Type := Mixin {
gcd : R -> R -> R;
_ : forall a b g, g %| gcd a b = (g %| a) && (g %| b)
}.
Section ClassDef.
Record class_of (R : Type) : Type := Class {
base : DvdRing.class_of R;
mixin : mixin_of (DvdRing.Pack base R)
}.
Local Coercion base : class_of >-> DvdRing.class_of.
Structure type : Type := Pack {sort : Type; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
Variable (T : Type) (cT : type).
Definition class := let: Pack _ c _ := cT return class_of cT in c.
Definition clone c of phant_id class c := @Pack T c T.
Definition pack b0 (m0 : mixin_of (@DvdRing.Pack T b0 T)) :=
fun bT b & phant_id (DvdRing.class bT) b =>
fun m & phant_id m m0 => Pack (@Class T b m) T.
Definition eqType := Equality.Pack class cT.
Definition choiceType := Choice.Pack class cT.
Definition zmodType := GRing.Zmodule.Pack class cT.
Definition ringType := GRing.Ring.Pack class cT.
Definition comRingType := GRing.ComRing.Pack class cT.
Definition unitRingType := GRing.UnitRing.Pack class cT.
Definition comUnitRingType := GRing.ComUnitRing.Pack class cT.
Definition idomainType := GRing.IntegralDomain.Pack class cT.
Definition dvdRingType := DvdRing.Pack class cT.
End ClassDef.
Module Exports.
Coercion base : class_of >-> DvdRing.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Canonical Structure eqType.
Coercion choiceType : type >-> Choice.type.
Canonical Structure choiceType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical Structure zmodType.
Coercion ringType : type >-> GRing.Ring.type.
Canonical Structure ringType.
Coercion comRingType : type >-> GRing.ComRing.type.
Canonical Structure comRingType.
Coercion unitRingType : type >-> GRing.UnitRing.type.
Canonical Structure unitRingType.
Coercion comUnitRingType : type >-> GRing.ComUnitRing.type.
Canonical Structure comUnitRingType.
Coercion idomainType : type >-> GRing.IntegralDomain.type.
Canonical Structure idomainType.
Coercion dvdRingType : type >-> DvdRing.type.
Canonical Structure dvdRingType.
Notation gcdRingType := type.
Notation GcdRingType T m := (@pack T _ m _ _ id _ id).
Notation GcdRingMixin := Mixin.
Notation "[ 'gcdRingType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
(at level 0, format "[ 'gcdRingType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'gcdRingType' 'of' T ]" := (@clone T _ _ id)
(at level 0, format "[ 'gcdRingType' 'of' T ]") : form_scope.
End Exports.
End GcdRing.
Export GcdRing.Exports.
Definition gcdr R := GcdRing.gcd (GcdRing.class R).
Definition lcmr R a b := nosimpl
(if (a == 0) || (b == 0) then 0 else odflt 0 ((a * b) %/? (@gcdr R a b))).
Definition gcdsr R := foldr (@gcdr R) 0.
Definition lcmsr R := foldr (@lcmr R) 1.
Section GCDRingTheory.
Variable R : gcdRingType.
Implicit Types a b : R.
Lemma dvdr_gcd : forall g a b, g %| gcdr a b = (g %| a) && (g %| b) :> bool.
Lemma dvdr_gcdl : forall a b, gcdr a b %| a.
Lemma dvdr_gcdr : forall a b, gcdr a b %| b.
Lemma gcdr_eq0 : forall a b, (gcdr a b == 0) = (a == 0) && (b == 0).
Hint Resolve dvdr_gcdr.
Hint Resolve dvdr_gcdl.
Lemma gcdr_def : forall x a b, x %| a -> x %| b ->
(forall x', x' %| a -> x' %| b -> (x' %| x)) -> gcdr a b %= x.
Lemma gcdrC : forall a b, gcdr a b %= gcdr b a.
Hint Resolve gcdrC.
Lemma eqd_gcd : forall c d a b, a %= c -> b %= d -> gcdr a b %= gcdr c d.
Lemma gcd0r : forall a, gcdr 0 a %= a.
Lemma gcdr0 : forall a, gcdr a 0 %= a.
Lemma gcd1r : forall a, gcdr 1 a %= 1.
Lemma gcdr1 : forall a, gcdr a 1 %= 1.
Lemma gcdrA : forall a b c, gcdr a (gcdr b c) %= gcdr (gcdr a b) c.
Lemma gcdrCA : forall a b c, gcdr a (gcdr b c) %= gcdr b (gcdr a c).
Lemma gcdrAC : forall a b c, gcdr (gcdr a b) c %= gcdr (gcdr a c) b.
Lemma gcdr_mul2r : forall a b c, gcdr (a * c) (b * c) %= gcdr a b * c.
Lemma gcdr_mul2l : forall a b c, gcdr (c * a) (c * b) %= c * gcdr a b.
Lemma mulr_gcdr : forall a b c, a * gcdr b c %= gcdr (a * b) (a * c).
Lemma mulr_gcdl : forall a b c, gcdr a b * c %= gcdr (a * c) (b * c).
Lemma gcdr_addr_r : forall c a b, a %| b -> gcdr a (c + b) %= gcdr a c.
Lemma gcdr_addl_r : forall c a b, a %| b -> gcdr a (b + c) %= gcdr a c.
Lemma gcdr_addr_l : forall a b c, b %| c -> gcdr (a + c) b %= gcdr a b.
Lemma gcdr_addl_l : forall a b c, b %| c -> gcdr (c + a) b %= gcdr a b.
Lemma gcdr_addl_mul : forall a b m, gcdr a (a * m + b) %= gcdr a b.
Lemma dvdr_gcd_mul : forall a b, gcdr a b %| a * b.
Lemma mulr_lcm_gcd : forall a b, lcmr a b * gcdr a b = a * b.
Lemma lcmr0 : forall a, lcmr a 0 = 0.
Lemma lcm0r : forall a, lcmr 0 a = 0.
Lemma dvdr_lcm : forall a b c, (lcmr a b %| c) = (a %| c) && (b %| c) :> bool.
Lemma dvdr_lcml : forall a b, a %| lcmr a b.
Hint Resolve dvdr_lcml.
Lemma dvdr_lcmr : forall a b, b %| lcmr a b.
Hint Resolve dvdr_lcmr.
Lemma dvdr_gcdr_lcmr : forall a b, gcdr a b %| lcmr a b.
Lemma lcm1r : forall a, lcmr 1 a %= a.
Lemma lcmr1 : forall a, lcmr a 1 %= a.
Lemma lcmrC : forall a b, lcmr a b %= lcmr b a.
Lemma lcmrA : forall a b c, lcmr a (lcmr b c) %= lcmr (lcmr a b) c.
Lemma eqd_lcmr : forall a b c, a %= b -> lcmr a c %= lcmr b c.
Lemma eqd_lcml : forall a b c, a %= b -> lcmr c a %= lcmr c b.
Lemma lcmrCA : forall a b c, lcmr a (lcmr b c) %= lcmr b (lcmr a c).
Lemma lcmrAC : forall a b c, lcmr (lcmr a b) c %= lcmr (lcmr a c) b.
Lemma mulr_lcmr : forall a b c, a * lcmr b c %= lcmr (a * b) (a * c).
Lemma mulr_lcml : forall a b c, lcmr a b * c %= lcmr (a * c) (b * c).
Lemma lcmr_mul2r : forall a b c, lcmr (a * c) (b * c) %= lcmr a b * c.
Lemma lcmr_mul2l : forall a b c, lcmr (c * a) (c * b) %= c * lcmr a b.
Lemma lcmr_mull : forall a b, lcmr a (a * b) %= a * b.
Lemma lcmr_mulr : forall a b, lcmr b (a * b) %= a * b.
Lemma dvdr_lcm_idr : forall a b, a %| b -> lcmr a b %= b.
Lemma dvdr_lcm_idl : forall a b, b %| a -> lcmr a b %= a.
Lemma gcdsr0 : (@gcdsr R) [::] = 0.
Lemma gcdsr_cons : forall a s, gcdsr (a :: s) = gcdr a (gcdsr s).
Lemma dvdr_gcds : forall (l : seq R) (g : R), g %| gcdsr l = all (%|%R g) l.
Lemma dvdr_mem_gcds : forall (l : seq R) (x : R), x \in l -> gcdsr l %| x.
Lemma lcmsr0 : (@lcmsr R) [::] = 1.
Lemma lcmsr_cons : forall a s, lcmsr (a :: s) = lcmr a (lcmsr s).
Lemma dvdr_lcms : forall (l : seq R) (m : R), lcmsr l %| m = all (%|%R^~ m) l.
Lemma dvdr_mem_lcms : forall (l : seq R) (x : R), x \in l -> x %| lcmsr l.
Coprimality
Definition coprimer a b := gcdr a b %= 1.
Lemma coprimer_sym : forall a b, coprimer a b = coprimer b a.
Lemma euclid_inv : forall a b c, coprimer a b ->
(a * b %| c) = (a %| c) && (b %| c).
Lemma euclid : forall b a c, coprimer a b -> (a %| c * b) = (a %| c) :> bool.
Lemma euclid_gcdr : forall a b c, coprimer a b -> gcdr a (c * b) %= gcdr a c.
Lemma euclid_gcdl : forall a b c, coprimer a b -> gcdr a (b * c) %= gcdr a c.
Lemma coprimer_mulr :
forall a b c, coprimer a (b * c) = coprimer a b && coprimer a c.
Lemma coprimer_mull :
forall a b c, coprimer (b * c) a = coprimer b a && coprimer c a.
Lemma coprimer_sym : forall a b, coprimer a b = coprimer b a.
Lemma euclid_inv : forall a b c, coprimer a b ->
(a * b %| c) = (a %| c) && (b %| c).
Lemma euclid : forall b a c, coprimer a b -> (a %| c * b) = (a %| c) :> bool.
Lemma euclid_gcdr : forall a b c, coprimer a b -> gcdr a (c * b) %= gcdr a c.
Lemma euclid_gcdl : forall a b c, coprimer a b -> gcdr a (b * c) %= gcdr a c.
Lemma coprimer_mulr :
forall a b c, coprimer a (b * c) = coprimer a b && coprimer a c.
Lemma coprimer_mull :
forall a b c, coprimer (b * c) a = coprimer b a && coprimer c a.
Irreducible and prime elements
Definition primer a :=
((a == 0 = false)
* (a %= 1 = false)
* (forall b c, a %| (b * c) = (a %| b) || (a %| c) :> bool)%R)%type.
Definition irredr a := ((a == 0 = false)
* (a %= 1 = false)
* (forall b c, a %= b * c
-> (b %= 1) || (c %= 1))%R)%type.
Lemma irredrP : forall a, irredr a ->
forall b c, a %= b * c -> b %= 1 \/ c %= 1.
Lemma irredr_dvd : forall a b, irredr a -> a %| b = ~~(coprimer a b) :> bool.
Lemma irredr_coprimer : forall a b, irredr a -> coprimer a b = ~~(a %| b).
Lemma irredr_primer : forall a, irredr a <-> primer a.
bigop
Lemma big_dvdr_gcdr (I : finType) (F : I -> R) :
forall i, \big[(@gcdr R)/0]_i F i %| F i.
Lemma big_gcdrP (I : finType) (F : I -> R) d :
(forall i, d %| F i) -> d %| \big[(@gcdr R)/0]_(i : I) F i.
Lemma big_gcdr_def (I : finType) (F : I -> R) d :
(exists k, F k %| d) -> \big[(@gcdr R)/0]_(i : I) F i %| d.
End GCDRingTheory.
Module BezoutRing.
CoInductive bezout_spec (R : gcdRingType) (a b : R) : R * R -> Type:=
BezoutSpec x y of gcdr a b %= x * a + y * b : bezout_spec a b (x, y).
Record mixin_of (R : gcdRingType) : Type := Mixin {
bezout : R -> R -> (R * R);
_ : forall a b, bezout_spec a b (bezout a b)
}.
Section ClassDef.
Record class_of (R : Type) : Type := Class {
base : GcdRing.class_of R;
mixin : mixin_of (GcdRing.Pack base R)
}.
Local Coercion base : class_of >-> GcdRing.class_of.
Structure type : Type := Pack {sort : Type; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
Variable (T : Type) (cT : type).
Definition class := let: Pack _ c _ := cT return class_of cT in c.
Definition clone c of phant_id class c := @Pack T c T.
Definition pack b0 (m0 : mixin_of (@GcdRing.Pack T b0 T)) :=
fun bT b & phant_id (GcdRing.class bT) b =>
fun m & phant_id m m0 => Pack (@Class T b m) T.
Definition eqType := Equality.Pack class cT.
Definition choiceType := Choice.Pack class cT.
Definition zmodType := GRing.Zmodule.Pack class cT.
Definition ringType := GRing.Ring.Pack class cT.
Definition comRingType := GRing.ComRing.Pack class cT.
Definition unitRingType := GRing.UnitRing.Pack class cT.
Definition comUnitRingType := GRing.ComUnitRing.Pack class cT.
Definition idomainType := GRing.IntegralDomain.Pack class cT.
Definition dvdRingType := DvdRing.Pack class cT.
Definition gcdRingType := GcdRing.Pack class cT.
End ClassDef.
Module Exports.
Coercion base : class_of >-> GcdRing.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Canonical Structure eqType.
Coercion choiceType : type >-> Choice.type.
Canonical Structure choiceType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical Structure zmodType.
Coercion ringType : type >-> GRing.Ring.type.
Canonical Structure ringType.
Coercion comRingType : type >-> GRing.ComRing.type.
Canonical Structure comRingType.
Coercion unitRingType : type >-> GRing.UnitRing.type.
Canonical Structure unitRingType.
Coercion comUnitRingType : type >-> GRing.ComUnitRing.type.
Canonical Structure comUnitRingType.
Coercion idomainType : type >-> GRing.IntegralDomain.type.
Canonical Structure idomainType.
Coercion dvdRingType : type >-> DvdRing.type.
Canonical Structure dvdRingType.
Coercion gcdRingType : type >-> GcdRing.type.
Canonical Structure gcdRingType.
Notation bezoutRingType := type.
Notation BezoutRingType T m := (@pack T _ m _ _ id _ id).
Notation BezoutRingMixin := Mixin.
Notation "[ 'bezoutRingType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
(at level 0, format "[ 'bezoutRingType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'bezoutRingType' 'of' T ]" := (@clone T _ _ id)
(at level 0, format "[ 'bezoutRingType' 'of' T ]") : form_scope.
End Exports.
End BezoutRing.
Export BezoutRing.Exports.
Definition bezout R := BezoutRing.bezout (BezoutRing.class R).
Section BezoutRingTheory.
Variable R : bezoutRingType.
Implicit Types a b : R.
Lemma bezoutP : forall a b, BezoutRing.bezout_spec a b (bezout a b).
Definition egcdr a b :=
let: (u, v) := bezout a b in
let g := u * a + v * b in
let a1 := odflt 0 (a %/? g) in
let b1 := odflt 0 (b %/? g) in
if g == 0 then (0,1,0,1,0) else (g, u, v, a1, b1).
CoInductive egcdr_spec a b : R * R * R * R * R -> Type :=
EgcdrSpec g u v a1 b1 of u * a1 + v * b1 = 1
& g %= gcdr a b
& a = a1 * g & b = b1 * g : egcdr_spec a b (g, u, v, a1, b1).
Lemma egcdrP : forall a b, egcdr_spec a b (egcdr a b).
forall i, \big[(@gcdr R)/0]_i F i %| F i.
Lemma big_gcdrP (I : finType) (F : I -> R) d :
(forall i, d %| F i) -> d %| \big[(@gcdr R)/0]_(i : I) F i.
Lemma big_gcdr_def (I : finType) (F : I -> R) d :
(exists k, F k %| d) -> \big[(@gcdr R)/0]_(i : I) F i %| d.
End GCDRingTheory.
Module BezoutRing.
CoInductive bezout_spec (R : gcdRingType) (a b : R) : R * R -> Type:=
BezoutSpec x y of gcdr a b %= x * a + y * b : bezout_spec a b (x, y).
Record mixin_of (R : gcdRingType) : Type := Mixin {
bezout : R -> R -> (R * R);
_ : forall a b, bezout_spec a b (bezout a b)
}.
Section ClassDef.
Record class_of (R : Type) : Type := Class {
base : GcdRing.class_of R;
mixin : mixin_of (GcdRing.Pack base R)
}.
Local Coercion base : class_of >-> GcdRing.class_of.
Structure type : Type := Pack {sort : Type; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
Variable (T : Type) (cT : type).
Definition class := let: Pack _ c _ := cT return class_of cT in c.
Definition clone c of phant_id class c := @Pack T c T.
Definition pack b0 (m0 : mixin_of (@GcdRing.Pack T b0 T)) :=
fun bT b & phant_id (GcdRing.class bT) b =>
fun m & phant_id m m0 => Pack (@Class T b m) T.
Definition eqType := Equality.Pack class cT.
Definition choiceType := Choice.Pack class cT.
Definition zmodType := GRing.Zmodule.Pack class cT.
Definition ringType := GRing.Ring.Pack class cT.
Definition comRingType := GRing.ComRing.Pack class cT.
Definition unitRingType := GRing.UnitRing.Pack class cT.
Definition comUnitRingType := GRing.ComUnitRing.Pack class cT.
Definition idomainType := GRing.IntegralDomain.Pack class cT.
Definition dvdRingType := DvdRing.Pack class cT.
Definition gcdRingType := GcdRing.Pack class cT.
End ClassDef.
Module Exports.
Coercion base : class_of >-> GcdRing.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Canonical Structure eqType.
Coercion choiceType : type >-> Choice.type.
Canonical Structure choiceType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical Structure zmodType.
Coercion ringType : type >-> GRing.Ring.type.
Canonical Structure ringType.
Coercion comRingType : type >-> GRing.ComRing.type.
Canonical Structure comRingType.
Coercion unitRingType : type >-> GRing.UnitRing.type.
Canonical Structure unitRingType.
Coercion comUnitRingType : type >-> GRing.ComUnitRing.type.
Canonical Structure comUnitRingType.
Coercion idomainType : type >-> GRing.IntegralDomain.type.
Canonical Structure idomainType.
Coercion dvdRingType : type >-> DvdRing.type.
Canonical Structure dvdRingType.
Coercion gcdRingType : type >-> GcdRing.type.
Canonical Structure gcdRingType.
Notation bezoutRingType := type.
Notation BezoutRingType T m := (@pack T _ m _ _ id _ id).
Notation BezoutRingMixin := Mixin.
Notation "[ 'bezoutRingType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
(at level 0, format "[ 'bezoutRingType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'bezoutRingType' 'of' T ]" := (@clone T _ _ id)
(at level 0, format "[ 'bezoutRingType' 'of' T ]") : form_scope.
End Exports.
End BezoutRing.
Export BezoutRing.Exports.
Definition bezout R := BezoutRing.bezout (BezoutRing.class R).
Section BezoutRingTheory.
Variable R : bezoutRingType.
Implicit Types a b : R.
Lemma bezoutP : forall a b, BezoutRing.bezout_spec a b (bezout a b).
Definition egcdr a b :=
let: (u, v) := bezout a b in
let g := u * a + v * b in
let a1 := odflt 0 (a %/? g) in
let b1 := odflt 0 (b %/? g) in
if g == 0 then (0,1,0,1,0) else (g, u, v, a1, b1).
CoInductive egcdr_spec a b : R * R * R * R * R -> Type :=
EgcdrSpec g u v a1 b1 of u * a1 + v * b1 = 1
& g %= gcdr a b
& a = a1 * g & b = b1 * g : egcdr_spec a b (g, u, v, a1, b1).
Lemma egcdrP : forall a b, egcdr_spec a b (egcdr a b).
Proof that any finitely generated ideal is principal
This could use gcdsr if it would be expressed using bigops...
Fixpoint principal_gen n : 'rV[R]_n -> R := match n with
| 0 => fun _ => 0
| S p => fun (I : 'rV[R]_(1 + p)) =>
let x := I 0 0 in
let y := principal_gen (rsubmx I) in
let: (g,_,_,_,_) := egcdr x y in g
end.
Lemma principal_gen_dvd : forall n (I : 'rV[R]_n) i, principal_gen I %| I 0 i.
Definition principal n (I : 'rV[R]_n) : 'M[R]_1 := (principal_gen I)%:M.
| 0 => fun _ => 0
| S p => fun (I : 'rV[R]_(1 + p)) =>
let x := I 0 0 in
let y := principal_gen (rsubmx I) in
let: (g,_,_,_,_) := egcdr x y in g
end.
Lemma principal_gen_dvd : forall n (I : 'rV[R]_n) i, principal_gen I %| I 0 i.
Definition principal n (I : 'rV[R]_n) : 'M[R]_1 := (principal_gen I)%:M.
(x) \subset (x1...xn) iff
exists (v1...vn) such that (x1...xn)(v1...vn)^T = (x)
Fixpoint principal_w1 n : 'rV[R]_n -> 'cV[R]_n := match n with
| 0 => fun _ => 0
| S p => fun (I : 'rV[R]_(1 + p)) =>
let g := principal_gen (rsubmx I) in
let us := principal_w1 (rsubmx I) in
let: (g',u,v,a1,b1) := egcdr (I 0 0) g in
col_mx u%:M (v *: us)
end.
Lemma principal_w1_correct : forall n (I : 'rV[R]_n),
I *m principal_w1 I = principal I.
| 0 => fun _ => 0
| S p => fun (I : 'rV[R]_(1 + p)) =>
let g := principal_gen (rsubmx I) in
let us := principal_w1 (rsubmx I) in
let: (g',u,v,a1,b1) := egcdr (I 0 0) g in
col_mx u%:M (v *: us)
end.
Lemma principal_w1_correct : forall n (I : 'rV[R]_n),
I *m principal_w1 I = principal I.
(x1...xn) \subset (x) iff
exists (w1...wn) such that (x)(w1...wn) = (x1...xn)
Definition principal_w2 n (I : 'rV[R]_n) : 'rV[R]_n :=
let g := principal_gen I in
map_mx (fun x => odflt 0 (x %/? g)) I.
Lemma principal_w2_correct : forall n (I : 'rV[R]_n),
principal I *m principal_w2 I = I.
End BezoutRingTheory.
Module PrincipalRing.
Record mixin_of (R : dvdRingType) : Type := Mixin {
_ : well_founded (@sdvdr R)
}.
Section ClassDef.
Record class_of (R : Type) : Type := Class {
base : BezoutRing.class_of R;
mixin : mixin_of (DvdRing.Pack base R)
}.
Local Coercion base : class_of >-> BezoutRing.class_of.
Structure type : Type := Pack {sort : Type; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
Variable (T : Type) (cT : type).
Definition class := let: Pack _ c _ := cT return class_of cT in c.
Definition clone c of phant_id class c := @Pack T c T.
Definition pack b0 (m0 : mixin_of (@DvdRing.Pack T b0 T)) :=
fun bT b & phant_id (BezoutRing.class bT) b =>
fun m & phant_id m m0 => Pack (@Class T b m) T.
Definition eqType := Equality.Pack class cT.
Definition choiceType := Choice.Pack class cT.
Definition zmodType := GRing.Zmodule.Pack class cT.
Definition ringType := GRing.Ring.Pack class cT.
Definition comRingType := GRing.ComRing.Pack class cT.
Definition unitRingType := GRing.UnitRing.Pack class cT.
Definition comUnitRingType := GRing.ComUnitRing.Pack class cT.
Definition idomainType := GRing.IntegralDomain.Pack class cT.
Definition dvdRingType := DvdRing.Pack class cT.
Definition gcdRingType := GcdRing.Pack class cT.
Definition bezoutRingType := BezoutRing.Pack class cT.
End ClassDef.
Module Exports.
Coercion base : class_of >-> BezoutRing.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Canonical Structure eqType.
Coercion choiceType : type >-> Choice.type.
Canonical Structure choiceType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical Structure zmodType.
Coercion ringType : type >-> GRing.Ring.type.
Canonical Structure ringType.
Coercion comRingType : type >-> GRing.ComRing.type.
Canonical Structure comRingType.
Coercion unitRingType : type >-> GRing.UnitRing.type.
Canonical Structure unitRingType.
Coercion comUnitRingType : type >-> GRing.ComUnitRing.type.
Canonical Structure comUnitRingType.
Coercion idomainType : type >-> GRing.IntegralDomain.type.
Canonical Structure idomainType.
Coercion dvdRingType : type >-> DvdRing.type.
Canonical Structure dvdRingType.
Coercion gcdRingType : type >-> GcdRing.type.
Canonical Structure gcdRingType.
Coercion bezoutRingType : type >-> BezoutRing.type.
Canonical Structure bezoutRingType.
Notation priRingType := type.
Notation PriRingType T m := (@pack T _ m _ _ id _ id).
Notation PriRingMixin := Mixin.
Notation "[ 'priRingType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
(at level 0, format "[ 'priRingType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'priRingType' 'of' T ]" := (@clone T _ _ id)
(at level 0, format "[ 'priRingType' 'of' T ]") : form_scope.
End Exports.
End PrincipalRing.
Export PrincipalRing.Exports.
Section PrincipalRingTheory.
Variable R : priRingType.
Implicit Types a b : R.
Lemma sdvdr_wf : well_founded (@sdvdr R).
Definition sdvdr_rect := (well_founded_induction_type (sdvdr_wf)).
Definition sdvdr_rec := (well_founded_induction (sdvdr_wf)).
Definition sdvdr_ind := (well_founded_ind (sdvdr_wf)).
End PrincipalRingTheory.
Module EuclideanRing.
CoInductive edivr_spec (R : ringType)
(g : R -> nat) (a b : R) : R * R -> Type :=
EdivrSpec q r of a = q * b + r & (b != 0) ==> (g r < g b)
: edivr_spec g a b (q, r).
Record mixin_of (R : ringType) : Type := Mixin {
enorm : R -> nat;
ediv : R -> R -> (R * R);
_ : forall a b, a != 0 -> enorm b <= enorm (a * b);
_ : forall a b, edivr_spec enorm a b (ediv a b)
}.
Module Mixins.
Section Mixins.
Variable R : Type.
Implicit Type a b : R.
Hypothesis cR : GRing.IntegralDomain.class_of R.
Canonical Structure R_eqType := EqType R cR.
Canonical Structure R_choiceType := ChoiceType R (Choice.mixin cR).
Canonical Structure R_zmod := @GRing.Zmodule.Pack R cR R.
Canonical Structure R_ring := @GRing.Ring.Pack R cR R.
Canonical Structure R_com := @GRing.ComRing.Pack R cR R.
Canonical Structure R_unit := @GRing.UnitRing.Pack R cR R.
Canonical Structure R_comunit := [comUnitRingType of R].
Canonical Structure R_idom := @GRing.IntegralDomain.Pack R cR R.
Hypothesis mR : mixin_of [ringType of R].
Local Notation norm := (enorm mR).
Local Notation ediv := (ediv mR).
Definition div a b := if b == 0 then 0 else (ediv a b).1.
Local Notation "a %/ b" := (div a b) : ring_scope.
Local Notation "a %% b" := (ediv a b).2 : ring_scope.
Lemma norm_mul : forall a b, a != 0 -> norm b <= norm (a * b).
Lemma edivP : forall a b, edivr_spec norm a b (ediv a b).
Lemma norm0_lt : forall a, a != 0 -> norm 0 < norm a.
Definition odiv a b := let (q, r) := ediv a b in
if r == 0 then Some (if b == 0 then 0 else q) else None.
Lemma odivP : forall a b, DvdRing.div_spec a b (odiv a b).
Lemma odiv_def : forall a b, odiv a b =
if a %% b == 0 then Some (a %/ b) else None.
Definition EuclidDvd := DvdRingMixin odivP.
Hypothesis dvdM : DvdRing.mixin_of [ringType of R].
Canonical Structure euclidDvdRing := DvdRingType R dvdM.
Lemma leq_norm : forall a b, b != 0 -> a %| b -> norm a <= norm b.
Lemma ltn_norm : forall a b, b != 0 -> a %<| b -> norm a < norm b.
Lemma sdvdr_wf : well_founded (@sdvdr [dvdRingType of R]).
Definition EuclidPrincipal := PriRingMixin sdvdr_wf.
Lemma mod_eq0 : forall a b, (a %% b == 0) = (b %| a).
Lemma norm_eq0 : forall a, norm a = 0%N -> a = 0.
Lemma mod_spec: forall a b, b != 0 -> norm (a %% b) < (norm b).
Lemma modr0 : forall a, a %% 0 = a.
Lemma mod0r : forall a, 0 %% a = 0.
Lemma dvd_mod : forall a b g, (g %| a) && (g %| b) = (g %| b) && (g %| a %% b).
let g := principal_gen I in
map_mx (fun x => odflt 0 (x %/? g)) I.
Lemma principal_w2_correct : forall n (I : 'rV[R]_n),
principal I *m principal_w2 I = I.
End BezoutRingTheory.
Module PrincipalRing.
Record mixin_of (R : dvdRingType) : Type := Mixin {
_ : well_founded (@sdvdr R)
}.
Section ClassDef.
Record class_of (R : Type) : Type := Class {
base : BezoutRing.class_of R;
mixin : mixin_of (DvdRing.Pack base R)
}.
Local Coercion base : class_of >-> BezoutRing.class_of.
Structure type : Type := Pack {sort : Type; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
Variable (T : Type) (cT : type).
Definition class := let: Pack _ c _ := cT return class_of cT in c.
Definition clone c of phant_id class c := @Pack T c T.
Definition pack b0 (m0 : mixin_of (@DvdRing.Pack T b0 T)) :=
fun bT b & phant_id (BezoutRing.class bT) b =>
fun m & phant_id m m0 => Pack (@Class T b m) T.
Definition eqType := Equality.Pack class cT.
Definition choiceType := Choice.Pack class cT.
Definition zmodType := GRing.Zmodule.Pack class cT.
Definition ringType := GRing.Ring.Pack class cT.
Definition comRingType := GRing.ComRing.Pack class cT.
Definition unitRingType := GRing.UnitRing.Pack class cT.
Definition comUnitRingType := GRing.ComUnitRing.Pack class cT.
Definition idomainType := GRing.IntegralDomain.Pack class cT.
Definition dvdRingType := DvdRing.Pack class cT.
Definition gcdRingType := GcdRing.Pack class cT.
Definition bezoutRingType := BezoutRing.Pack class cT.
End ClassDef.
Module Exports.
Coercion base : class_of >-> BezoutRing.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Canonical Structure eqType.
Coercion choiceType : type >-> Choice.type.
Canonical Structure choiceType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical Structure zmodType.
Coercion ringType : type >-> GRing.Ring.type.
Canonical Structure ringType.
Coercion comRingType : type >-> GRing.ComRing.type.
Canonical Structure comRingType.
Coercion unitRingType : type >-> GRing.UnitRing.type.
Canonical Structure unitRingType.
Coercion comUnitRingType : type >-> GRing.ComUnitRing.type.
Canonical Structure comUnitRingType.
Coercion idomainType : type >-> GRing.IntegralDomain.type.
Canonical Structure idomainType.
Coercion dvdRingType : type >-> DvdRing.type.
Canonical Structure dvdRingType.
Coercion gcdRingType : type >-> GcdRing.type.
Canonical Structure gcdRingType.
Coercion bezoutRingType : type >-> BezoutRing.type.
Canonical Structure bezoutRingType.
Notation priRingType := type.
Notation PriRingType T m := (@pack T _ m _ _ id _ id).
Notation PriRingMixin := Mixin.
Notation "[ 'priRingType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
(at level 0, format "[ 'priRingType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'priRingType' 'of' T ]" := (@clone T _ _ id)
(at level 0, format "[ 'priRingType' 'of' T ]") : form_scope.
End Exports.
End PrincipalRing.
Export PrincipalRing.Exports.
Section PrincipalRingTheory.
Variable R : priRingType.
Implicit Types a b : R.
Lemma sdvdr_wf : well_founded (@sdvdr R).
Definition sdvdr_rect := (well_founded_induction_type (sdvdr_wf)).
Definition sdvdr_rec := (well_founded_induction (sdvdr_wf)).
Definition sdvdr_ind := (well_founded_ind (sdvdr_wf)).
End PrincipalRingTheory.
Module EuclideanRing.
CoInductive edivr_spec (R : ringType)
(g : R -> nat) (a b : R) : R * R -> Type :=
EdivrSpec q r of a = q * b + r & (b != 0) ==> (g r < g b)
: edivr_spec g a b (q, r).
Record mixin_of (R : ringType) : Type := Mixin {
enorm : R -> nat;
ediv : R -> R -> (R * R);
_ : forall a b, a != 0 -> enorm b <= enorm (a * b);
_ : forall a b, edivr_spec enorm a b (ediv a b)
}.
Module Mixins.
Section Mixins.
Variable R : Type.
Implicit Type a b : R.
Hypothesis cR : GRing.IntegralDomain.class_of R.
Canonical Structure R_eqType := EqType R cR.
Canonical Structure R_choiceType := ChoiceType R (Choice.mixin cR).
Canonical Structure R_zmod := @GRing.Zmodule.Pack R cR R.
Canonical Structure R_ring := @GRing.Ring.Pack R cR R.
Canonical Structure R_com := @GRing.ComRing.Pack R cR R.
Canonical Structure R_unit := @GRing.UnitRing.Pack R cR R.
Canonical Structure R_comunit := [comUnitRingType of R].
Canonical Structure R_idom := @GRing.IntegralDomain.Pack R cR R.
Hypothesis mR : mixin_of [ringType of R].
Local Notation norm := (enorm mR).
Local Notation ediv := (ediv mR).
Definition div a b := if b == 0 then 0 else (ediv a b).1.
Local Notation "a %/ b" := (div a b) : ring_scope.
Local Notation "a %% b" := (ediv a b).2 : ring_scope.
Lemma norm_mul : forall a b, a != 0 -> norm b <= norm (a * b).
Lemma edivP : forall a b, edivr_spec norm a b (ediv a b).
Lemma norm0_lt : forall a, a != 0 -> norm 0 < norm a.
Definition odiv a b := let (q, r) := ediv a b in
if r == 0 then Some (if b == 0 then 0 else q) else None.
Lemma odivP : forall a b, DvdRing.div_spec a b (odiv a b).
Lemma odiv_def : forall a b, odiv a b =
if a %% b == 0 then Some (a %/ b) else None.
Definition EuclidDvd := DvdRingMixin odivP.
Hypothesis dvdM : DvdRing.mixin_of [ringType of R].
Canonical Structure euclidDvdRing := DvdRingType R dvdM.
Lemma leq_norm : forall a b, b != 0 -> a %| b -> norm a <= norm b.
Lemma ltn_norm : forall a b, b != 0 -> a %<| b -> norm a < norm b.
Lemma sdvdr_wf : well_founded (@sdvdr [dvdRingType of R]).
Definition EuclidPrincipal := PriRingMixin sdvdr_wf.
Lemma mod_eq0 : forall a b, (a %% b == 0) = (b %| a).
Lemma norm_eq0 : forall a, norm a = 0%N -> a = 0.
Lemma mod_spec: forall a b, b != 0 -> norm (a %% b) < (norm b).
Lemma modr0 : forall a, a %% 0 = a.
Lemma mod0r : forall a, 0 %% a = 0.
Lemma dvd_mod : forall a b g, (g %| a) && (g %| b) = (g %| b) && (g %| a %% b).
Acc experiment:
Lemma tool : forall (a b: R), (b != 0) ==> (norm (a %% b) < norm b).
Definition acc_gcd (n:nat) (hn: Acc (fun x y => x < y) n) :
forall (a b:R), n = norm b -> R.
Defined.
Lemma acc_gcdP : forall (n:nat) (hn: Acc (fun x y => x < y) n)
(a b: R) (hb: n = norm b) (g :R),
g %| (acc_gcd hn a hb) = (g %| a) && (g %| b).
Definition GCD (a b:R) : R :=
acc_gcd (guarded 100 lt_wf2 (norm b)) a (refl_equal (norm b)).
Lemma GCDP : forall (a b g:R),
g %| GCD a b = (g %| a) && (g %| b).
Definition gcd a b :=
let: (a1, b1) := if norm a < norm b then (b, a) else (a, b) in
if a1 == 0 then b1 else
let fix loop (n : nat) (aa bb : R) {struct n} :=
let rr := aa %% bb in
if rr == 0 then bb else
if n is n1.+1 then loop n1 bb rr else rr in
loop (norm a1) a1 b1.
Lemma gcdP : forall a b g, g %| gcd a b = (g %| a) && (g %| b).
Definition EuclidGCD := GcdRingMixin GCDP.
Definition EuclidGcd := GcdRingMixin gcdP.
Hypothesis gcdM : GcdRing.mixin_of [dvdRingType of R].
Canonical Structure R_gcdRing := GcdRingType R gcdM.
Fixpoint egcd_rec (a b : R) n {struct n} : R * R :=
if n is n'.+1 then
if b == 0 then (1, 0) else
let: (u, v) := egcd_rec b (a %% b) n' in
(v, (u - v * (a %/ b)))
else (1, 0).
Definition egcd p q := egcd_rec p q (norm q).
Lemma gcdrE : forall a b, gcdr a b %= gcdr b (a %% b).
Lemma egcd_recP : forall n a b, norm b <= n
-> let e := (egcd_rec a b n) in gcdr a b %= e.1 * a + e.2 * b.
Lemma egcdP : forall a b, BezoutRing.bezout_spec a b (egcd a b).
Definition EuclidBezout := BezoutRingMixin egcdP.
End Mixins.
End Mixins.
Definition EuclidDvdMixin R cR (m0 : mixin_of cR) :=
fun bT b & phant_id (GRing.IntegralDomain.class bT) b =>
fun m & phant_id m0 m => @Mixins.EuclidDvd R b m.
Definition EuclidGcdMixin R cR (m0 : mixin_of cR) :=
fun biT bi & phant_id (GRing.IntegralDomain.class biT) bi =>
fun bdT bd & phant_id (DvdRing.class bdT : DvdRing.mixin_of _) bd =>
fun m & phant_id m0 m => @Mixins.EuclidGcd R bi m bd.
Definition EuclidGCDMixin R cR (m0 : mixin_of cR) :=
fun biT bi & phant_id (GRing.IntegralDomain.class biT) bi =>
fun bdT bd & phant_id (DvdRing.class bdT : DvdRing.mixin_of _) bd =>
fun m & phant_id m0 m => @Mixins.EuclidGCD R bi m bd.
Definition EuclidBezoutMixin R cR (m0 : mixin_of cR) :=
fun biT bi & phant_id (GRing.IntegralDomain.class biT) bi =>
fun bdT bd & phant_id (DvdRing.class bdT : DvdRing.mixin_of _) bd =>
fun bgT bg & phant_id (GcdRing.class bgT : GcdRing.mixin_of _) bg =>
fun m & phant_id m0 m => @Mixins.EuclidBezout R bi m bd bg.
Definition EuclidPriMixin R cR (m0 : mixin_of cR) :=
fun biT bi & phant_id (GRing.IntegralDomain.class biT) bi =>
fun bdT bd & phant_id (DvdRing.class bdT : DvdRing.mixin_of _) bd =>
fun m & phant_id m0 m => @Mixins.EuclidPrincipal R bi m bd.
Section ClassDef.
Record class_of (R : Type) : Type := Class {
base : PrincipalRing.class_of R;
mixin : mixin_of (GRing.Ring.Pack base R)
}.
Local Coercion base : class_of >-> PrincipalRing.class_of.
Structure type : Type := Pack {sort : Type; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
Variable (T : Type) (cT : type).
Definition class := let: Pack _ c _ := cT return class_of cT in c.
Definition clone c of phant_id class c := @Pack T c T.
Definition pack b0 (m0 : mixin_of (@GRing.Ring.Pack T b0 T)) :=
fun bT b & phant_id (PrincipalRing.class bT) b =>
fun m & phant_id m m0 => Pack (@Class T b m) T.
Definition eqType := Equality.Pack class cT.
Definition choiceType := Choice.Pack class cT.
Definition zmodType := GRing.Zmodule.Pack class cT.
Definition ringType := GRing.Ring.Pack class cT.
Definition comRingType := GRing.ComRing.Pack class cT.
Definition unitRingType := GRing.UnitRing.Pack class cT.
Definition comUnitRingType := GRing.ComUnitRing.Pack class cT.
Definition idomainType := GRing.IntegralDomain.Pack class cT.
Definition dvdRingType := DvdRing.Pack class cT.
Definition gcdRingType := GcdRing.Pack class cT.
Definition bezoutRingType := BezoutRing.Pack class cT.
Definition priRingType := PrincipalRing.Pack class cT.
End ClassDef.
Module Exports.
Coercion base : class_of >-> PrincipalRing.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Canonical Structure eqType.
Coercion choiceType : type >-> Choice.type.
Canonical Structure choiceType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical Structure zmodType.
Coercion ringType : type >-> GRing.Ring.type.
Canonical Structure ringType.
Coercion comRingType : type >-> GRing.ComRing.type.
Canonical Structure comRingType.
Coercion unitRingType : type >-> GRing.UnitRing.type.
Canonical Structure unitRingType.
Coercion comUnitRingType : type >-> GRing.ComUnitRing.type.
Canonical Structure comUnitRingType.
Coercion idomainType : type >-> GRing.IntegralDomain.type.
Canonical Structure idomainType.
Coercion dvdRingType : type >-> DvdRing.type.
Canonical Structure dvdRingType.
Coercion gcdRingType : type >-> GcdRing.type.
Canonical Structure gcdRingType.
Coercion bezoutRingType : type >-> BezoutRing.type.
Canonical Structure bezoutRingType.
Coercion priRingType : type >-> PrincipalRing.type.
Canonical Structure priRingType.
Notation euclidRingType := type.
Notation EuclidRingType T m := (@pack T _ m _ _ id _ id).
Notation EuclidRingMixin := Mixin.
Notation "[ 'euclidRingType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
(at level 0, format "[ 'euclidRingType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'euclidRingType' 'of' T ]" := (@clone T _ _ id)
(at level 0, format "[ 'euclidRingType' 'of' T ]") : form_scope.
Notation EuclidDvdMixin T m := (@EuclidDvdMixin T _ m _ _ id _ id).
Notation EuclidGcdMixin T m := (@EuclidGcdMixin T _ m _ _ id _ _ id _ id).
Notation EuclidGCDMixin T m := (@EuclidGCDMixin T _ m _ _ id _ _ id _ id).
Notation EuclidBezoutMixin T m :=
(@EuclidBezoutMixin T _ m _ _ id _ _ id _ _ id _ id).
Notation EuclidPriMixin T m := (@EuclidPriMixin T _ m _ _ id _ _ id _ id).
End Exports.
End EuclideanRing.
Export EuclideanRing.Exports.
Definition edivr (R : euclidRingType) :=
EuclideanRing.ediv (EuclideanRing.class R).
Definition enorm (R : euclidRingType) :=
EuclideanRing.enorm (EuclideanRing.class R).
Definition GCD (R : euclidRingType) :=
EuclideanRing.Mixins.GCD (EuclideanRing.class R).
Definition ACC_GCD (R : euclidRingType) :=
@EuclideanRing.Mixins.acc_gcd _ (EuclideanRing.class R).
Definition divr (R : euclidRingType) (m d : R) := (edivr m d).1.
Notation "m %/ d" := (divr m d) : ring_scope.
Definition modr (R : euclidRingType) (m d : R) := (edivr m d).2.
Notation "m %% d" := (modr m d) : ring_scope.
Notation "m = n %[mod d ]" := (m %% d = n %% d) : ring_scope.
Notation "m == n %[mod d ]" := (m %% d == n %% d) : ring_scope.
Notation "m <> n %[mod d ]" := (m %% d <> n %% d) : ring_scope.
Notation "m != n %[mod d ]" := (m %% d != n %% d) : ring_scope.
Section EuclideanRingTheory.
Variable R : euclidRingType.
Implicit Types a b : R.
Lemma enorm_mul : forall a b, a != 0 -> enorm b <= enorm (a * b).
Lemma edivrP : forall a b, EuclideanRing.edivr_spec (@enorm _) a b (edivr a b).
Lemma enorm0_lt : forall a, a != 0 -> enorm (0 : R) < enorm a.
Lemma leq_enorm : forall a b, b != 0 -> a %| b -> enorm a <= enorm b.
Lemma ltn_enorm : forall a b, b != 0 -> a %<| b -> enorm a < enorm b.
Lemma modr_eq0 : forall a b, (a %% b == 0) = (b %| a).
Lemma enorm_eq0 : forall a, enorm a = 0%N -> a = 0.
Lemma modr_spec: forall a b, b != 0 -> enorm (a %% b) < (enorm b).
Lemma modr0 : forall a, a %% 0 = a.
Lemma mod0r : forall a, 0 %% a = 0.
Lemma dvdr_mod : forall a b g, (g %| a) && (g %| b) = (g %| b) && (g %| a %% b).
Lemma divr_mulKr a b : b != 0 -> (b * a) %/ b = a.
Lemma divr_mulKl a b : b != 0 -> (a * b) %/ b = a.
End EuclideanRingTheory.
Definition acc_gcd (n:nat) (hn: Acc (fun x y => x < y) n) :
forall (a b:R), n = norm b -> R.
Defined.
Lemma acc_gcdP : forall (n:nat) (hn: Acc (fun x y => x < y) n)
(a b: R) (hb: n = norm b) (g :R),
g %| (acc_gcd hn a hb) = (g %| a) && (g %| b).
Definition GCD (a b:R) : R :=
acc_gcd (guarded 100 lt_wf2 (norm b)) a (refl_equal (norm b)).
Lemma GCDP : forall (a b g:R),
g %| GCD a b = (g %| a) && (g %| b).
Definition gcd a b :=
let: (a1, b1) := if norm a < norm b then (b, a) else (a, b) in
if a1 == 0 then b1 else
let fix loop (n : nat) (aa bb : R) {struct n} :=
let rr := aa %% bb in
if rr == 0 then bb else
if n is n1.+1 then loop n1 bb rr else rr in
loop (norm a1) a1 b1.
Lemma gcdP : forall a b g, g %| gcd a b = (g %| a) && (g %| b).
Definition EuclidGCD := GcdRingMixin GCDP.
Definition EuclidGcd := GcdRingMixin gcdP.
Hypothesis gcdM : GcdRing.mixin_of [dvdRingType of R].
Canonical Structure R_gcdRing := GcdRingType R gcdM.
Fixpoint egcd_rec (a b : R) n {struct n} : R * R :=
if n is n'.+1 then
if b == 0 then (1, 0) else
let: (u, v) := egcd_rec b (a %% b) n' in
(v, (u - v * (a %/ b)))
else (1, 0).
Definition egcd p q := egcd_rec p q (norm q).
Lemma gcdrE : forall a b, gcdr a b %= gcdr b (a %% b).
Lemma egcd_recP : forall n a b, norm b <= n
-> let e := (egcd_rec a b n) in gcdr a b %= e.1 * a + e.2 * b.
Lemma egcdP : forall a b, BezoutRing.bezout_spec a b (egcd a b).
Definition EuclidBezout := BezoutRingMixin egcdP.
End Mixins.
End Mixins.
Definition EuclidDvdMixin R cR (m0 : mixin_of cR) :=
fun bT b & phant_id (GRing.IntegralDomain.class bT) b =>
fun m & phant_id m0 m => @Mixins.EuclidDvd R b m.
Definition EuclidGcdMixin R cR (m0 : mixin_of cR) :=
fun biT bi & phant_id (GRing.IntegralDomain.class biT) bi =>
fun bdT bd & phant_id (DvdRing.class bdT : DvdRing.mixin_of _) bd =>
fun m & phant_id m0 m => @Mixins.EuclidGcd R bi m bd.
Definition EuclidGCDMixin R cR (m0 : mixin_of cR) :=
fun biT bi & phant_id (GRing.IntegralDomain.class biT) bi =>
fun bdT bd & phant_id (DvdRing.class bdT : DvdRing.mixin_of _) bd =>
fun m & phant_id m0 m => @Mixins.EuclidGCD R bi m bd.
Definition EuclidBezoutMixin R cR (m0 : mixin_of cR) :=
fun biT bi & phant_id (GRing.IntegralDomain.class biT) bi =>
fun bdT bd & phant_id (DvdRing.class bdT : DvdRing.mixin_of _) bd =>
fun bgT bg & phant_id (GcdRing.class bgT : GcdRing.mixin_of _) bg =>
fun m & phant_id m0 m => @Mixins.EuclidBezout R bi m bd bg.
Definition EuclidPriMixin R cR (m0 : mixin_of cR) :=
fun biT bi & phant_id (GRing.IntegralDomain.class biT) bi =>
fun bdT bd & phant_id (DvdRing.class bdT : DvdRing.mixin_of _) bd =>
fun m & phant_id m0 m => @Mixins.EuclidPrincipal R bi m bd.
Section ClassDef.
Record class_of (R : Type) : Type := Class {
base : PrincipalRing.class_of R;
mixin : mixin_of (GRing.Ring.Pack base R)
}.
Local Coercion base : class_of >-> PrincipalRing.class_of.
Structure type : Type := Pack {sort : Type; _ : class_of sort; _ : Type}.
Local Coercion sort : type >-> Sortclass.
Variable (T : Type) (cT : type).
Definition class := let: Pack _ c _ := cT return class_of cT in c.
Definition clone c of phant_id class c := @Pack T c T.
Definition pack b0 (m0 : mixin_of (@GRing.Ring.Pack T b0 T)) :=
fun bT b & phant_id (PrincipalRing.class bT) b =>
fun m & phant_id m m0 => Pack (@Class T b m) T.
Definition eqType := Equality.Pack class cT.
Definition choiceType := Choice.Pack class cT.
Definition zmodType := GRing.Zmodule.Pack class cT.
Definition ringType := GRing.Ring.Pack class cT.
Definition comRingType := GRing.ComRing.Pack class cT.
Definition unitRingType := GRing.UnitRing.Pack class cT.
Definition comUnitRingType := GRing.ComUnitRing.Pack class cT.
Definition idomainType := GRing.IntegralDomain.Pack class cT.
Definition dvdRingType := DvdRing.Pack class cT.
Definition gcdRingType := GcdRing.Pack class cT.
Definition bezoutRingType := BezoutRing.Pack class cT.
Definition priRingType := PrincipalRing.Pack class cT.
End ClassDef.
Module Exports.
Coercion base : class_of >-> PrincipalRing.class_of.
Coercion mixin : class_of >-> mixin_of.
Coercion sort : type >-> Sortclass.
Coercion eqType : type >-> Equality.type.
Canonical Structure eqType.
Coercion choiceType : type >-> Choice.type.
Canonical Structure choiceType.
Coercion zmodType : type >-> GRing.Zmodule.type.
Canonical Structure zmodType.
Coercion ringType : type >-> GRing.Ring.type.
Canonical Structure ringType.
Coercion comRingType : type >-> GRing.ComRing.type.
Canonical Structure comRingType.
Coercion unitRingType : type >-> GRing.UnitRing.type.
Canonical Structure unitRingType.
Coercion comUnitRingType : type >-> GRing.ComUnitRing.type.
Canonical Structure comUnitRingType.
Coercion idomainType : type >-> GRing.IntegralDomain.type.
Canonical Structure idomainType.
Coercion dvdRingType : type >-> DvdRing.type.
Canonical Structure dvdRingType.
Coercion gcdRingType : type >-> GcdRing.type.
Canonical Structure gcdRingType.
Coercion bezoutRingType : type >-> BezoutRing.type.
Canonical Structure bezoutRingType.
Coercion priRingType : type >-> PrincipalRing.type.
Canonical Structure priRingType.
Notation euclidRingType := type.
Notation EuclidRingType T m := (@pack T _ m _ _ id _ id).
Notation EuclidRingMixin := Mixin.
Notation "[ 'euclidRingType' 'of' T 'for' cT ]" := (@clone T cT _ idfun)
(at level 0, format "[ 'euclidRingType' 'of' T 'for' cT ]") : form_scope.
Notation "[ 'euclidRingType' 'of' T ]" := (@clone T _ _ id)
(at level 0, format "[ 'euclidRingType' 'of' T ]") : form_scope.
Notation EuclidDvdMixin T m := (@EuclidDvdMixin T _ m _ _ id _ id).
Notation EuclidGcdMixin T m := (@EuclidGcdMixin T _ m _ _ id _ _ id _ id).
Notation EuclidGCDMixin T m := (@EuclidGCDMixin T _ m _ _ id _ _ id _ id).
Notation EuclidBezoutMixin T m :=
(@EuclidBezoutMixin T _ m _ _ id _ _ id _ _ id _ id).
Notation EuclidPriMixin T m := (@EuclidPriMixin T _ m _ _ id _ _ id _ id).
End Exports.
End EuclideanRing.
Export EuclideanRing.Exports.
Definition edivr (R : euclidRingType) :=
EuclideanRing.ediv (EuclideanRing.class R).
Definition enorm (R : euclidRingType) :=
EuclideanRing.enorm (EuclideanRing.class R).
Definition GCD (R : euclidRingType) :=
EuclideanRing.Mixins.GCD (EuclideanRing.class R).
Definition ACC_GCD (R : euclidRingType) :=
@EuclideanRing.Mixins.acc_gcd _ (EuclideanRing.class R).
Definition divr (R : euclidRingType) (m d : R) := (edivr m d).1.
Notation "m %/ d" := (divr m d) : ring_scope.
Definition modr (R : euclidRingType) (m d : R) := (edivr m d).2.
Notation "m %% d" := (modr m d) : ring_scope.
Notation "m = n %[mod d ]" := (m %% d = n %% d) : ring_scope.
Notation "m == n %[mod d ]" := (m %% d == n %% d) : ring_scope.
Notation "m <> n %[mod d ]" := (m %% d <> n %% d) : ring_scope.
Notation "m != n %[mod d ]" := (m %% d != n %% d) : ring_scope.
Section EuclideanRingTheory.
Variable R : euclidRingType.
Implicit Types a b : R.
Lemma enorm_mul : forall a b, a != 0 -> enorm b <= enorm (a * b).
Lemma edivrP : forall a b, EuclideanRing.edivr_spec (@enorm _) a b (edivr a b).
Lemma enorm0_lt : forall a, a != 0 -> enorm (0 : R) < enorm a.
Lemma leq_enorm : forall a b, b != 0 -> a %| b -> enorm a <= enorm b.
Lemma ltn_enorm : forall a b, b != 0 -> a %<| b -> enorm a < enorm b.
Lemma modr_eq0 : forall a b, (a %% b == 0) = (b %| a).
Lemma enorm_eq0 : forall a, enorm a = 0%N -> a = 0.
Lemma modr_spec: forall a b, b != 0 -> enorm (a %% b) < (enorm b).
Lemma modr0 : forall a, a %% 0 = a.
Lemma mod0r : forall a, 0 %% a = 0.
Lemma dvdr_mod : forall a b g, (g %| a) && (g %| b) = (g %| b) && (g %| a %% b).
Lemma divr_mulKr a b : b != 0 -> (b * a) %/ b = a.
Lemma divr_mulKl a b : b != 0 -> (a * b) %/ b = a.
End EuclideanRingTheory.
This page has been generated by coqdoc