From 60357114988f3f5bc578e8e07ae9ee29098cb35e Mon Sep 17 00:00:00 2001 From: thery Date: Fri, 27 Oct 2023 11:24:15 +0200 Subject: [PATCH] remane gaussInteger -> gaussInt --- gauss_int.v | 52 +++++++++++++++++++++++++++++----------------------- 1 file changed, 29 insertions(+), 23 deletions(-) diff --git a/gauss_int.v b/gauss_int.v index 23f1163..5bfb603 100644 --- a/gauss_int.v +++ b/gauss_int.v @@ -164,39 +164,44 @@ End PreliminaryLemmas. - Exercice 3.10. ENS Lyon *) -Section GaussIntegers. +Section gaussInts. (** First we define a predicate for the algebraic numbers which are gauss integers. *) -Definition gaussInteger_subdef := - [pred x : algC | ('Re x \is a Num.int) && ('Im x \is a Num.int)]. +Definition gaussInt_subdef : pred algC := + [pred x | ('Re x \is a Num.int) && ('Im x \is a Num.int)]. -Definition gaussInteger := [qualify a x | gaussInteger_subdef x]. +Definition gaussInt := [qualify a x | gaussInt_subdef x]. + +Lemma gaussIntE x : + x \is a gaussInt = (('Re x \is a Num.int) && ('Im x \is a Num.int)). +Proof. by []. Qed. (** ** Question 1: Prove that integers are gauss integers *) -Lemma Cint_GI (x : algC) : x \is a Num.int -> x \is a gaussInteger. +Lemma Cint_GI (x : algC) : x \is a Num.int -> x \is a gaussInt. Proof. -move=> x_int; rewrite qualifE /= (Creal_ReP _ _) ?(Creal_ImP _ _) ?Rreal_int //. +move=> x_int. +rewrite !gaussIntE (Creal_ReP _ _) ?(Creal_ImP _ _) ?Rreal_int //. by rewrite x_int rpred0. Qed. (** ** Question 2: Prove that gauss integers form a subfield *) -Lemma GI_subring : subring_closed gaussInteger. +Lemma GI_subring : subring_closed gaussInt. Proof. split => [|x y /andP[??] /andP[??]|x y /andP[??] /andP[??]]. - by rewrite Cint_GI. -- by rewrite qualifE /= !raddfB /= ?rpredB. -by rewrite qualifE /= algReM algImM rpredB ?rpredD // rpredM. +- by rewrite gaussIntE !raddfB /= ?rpredB. +by rewrite gaussIntE algReM algImM rpredB ?rpredD // rpredM. Qed. HB.instance Definition _ := - GRing.isSubringClosed.Build algC gaussInteger_subdef GI_subring. + GRing.isSubringClosed.Build algC gaussInt_subdef GI_subring. (** @@ -206,7 +211,7 @@ algebraic numbers. We soon prove that this is in fact a sub type. *) Record GI := GIof { algGI : algC; - algGIP : algGI \is a gaussInteger }. + algGIP : algGI \is a gaussInt }. (** We make the defining property of GI a Hint *) Hint Resolve algGIP : core. (** @@ -235,7 +240,7 @@ Definition ImGI x := GIof (Cint_GI (GIIm x)). (** We provide a ring structure to the type GI, using the subring -canonical property for the predicate gaussInteger +canonical property for the predicate gaussInt *) @@ -262,7 +267,7 @@ HB.instance Definition _ := [SubRing_isSubComRing of GI by <:]. *) Definition invGI (x : GI) := insubd x (val x)^-1. -Definition unitGI (x : GI) := (x != 0) && ((val x)^-1 \is a gaussInteger). +Definition unitGI (x : GI) := (x != 0) && ((val x)^-1 \is a gaussInt). (** ** Question 3: prove a few facts in order to find a comUnitRingMixin @@ -299,16 +304,16 @@ HB.instance Definition _ := ** Question 4: Show that gauss integers are stable by conjugation. *) -Lemma conjGIE x : (x^* \is a gaussInteger) = (x \is a gaussInteger). +Lemma conjGIE x : (x^* \is a gaussInt) = (x \is a gaussInt). Proof. -by rewrite ![_ \is a gaussInteger]qualifE /= Re_conj Im_conj rpredN. +by rewrite gaussIntE Re_conj Im_conj rpredN. Qed. (** We use this fact to build the conjugation of a gauss Integers *) -Fact conjGI_subproof (x : GI) : (val x)^* \is a gaussInteger. +Fact conjGI_subproof (x : GI) : (val x)^* \is a gaussInt. Proof. by rewrite conjGIE. Qed. Canonical conjGI x := GIof (conjGI_subproof x). @@ -428,6 +433,7 @@ rewrite /normGI gaussNormE normC2_Re_Im truncD ?natr_exp_even //; last first. by rewrite qualifE /= natr_ge0 // natr_exp_even. by rewrite -!truncX ?natr_norm_int // !intr_normK. Qed. + Lemma truncC_Cint (x : algC) : x \is a Num.int -> x = (-1) ^+ (x < 0)%R * (Num.trunc `|x|)%:R. Proof. @@ -527,8 +533,8 @@ Qed. HB.instance Definition _ := GRing.ComUnitRing_isIntegral.Build GI GI_idomainAxiom. -Fact divGI_subproof (x y : int) : x%:~R + 'i * y%:~R \is a gaussInteger. -Proof. by rewrite qualifE /= Re_rect ?Im_rect ?Rreal_int ?intr_int. Qed. +Fact divGI_subproof (x y : int) : x%:~R + 'i * y%:~R \is a gaussInt. +Proof. by rewrite gaussIntE Re_rect ?Im_rect ?Rreal_int ?intr_int. Qed. Definition divGI (x y : GI) : GI := let zr := Num.floor ('Re (val x) * 'Re (val y) + 'Im (val x) * 'Im (val y)) in @@ -765,8 +771,8 @@ case/dvdGIP=> q ->; apply/dvdGIP; exists (conjGI q). by rewrite rmorphM. Qed. -Fact iGI_proof : 'i \is a gaussInteger. -Proof. by rewrite qualifE /= Re_i Im_i int_num0 int_num1. Qed. +Fact iGI_proof : 'i \is a gaussInt. +Proof. by rewrite gaussIntE Re_i Im_i int_num0 int_num1. Qed. Definition iGI := GIof iGI_proof. @@ -780,14 +786,14 @@ apply/dvdGIP. have := algGIP x; rewrite qualifE => / andP[]. have := Ex; rewrite normGIE oddD !oddX /= negb_add. set m := 'Re _; set n := 'Im _ => /eqP Omn Cm Cn. -suff FF : (n + m)/2%:R + 'i * ((n - m)/2%:R) \is a gaussInteger. +suff FF : (n + m)/2%:R + 'i * ((n - m)/2%:R) \is a gaussInt. exists (GIof FF); apply/val_eqP => /=. rewrite -{2}['i]mulr1 mulC_rect !mulr1 mul1r -mulrBl -mulrDl. rewrite opprB [_ + (m - n)]addrC addrA subrK. rewrite -addrA [_ + (_ - _)]addrC subrK. have F u : (u * 2%:R = u + u) by rewrite mulrDr mulr1. by rewrite -!F !mulfK 1?[algGI x]algCrect ?(eqC_nat _ 0). -rewrite qualifE /= Re_rect ?Im_rect; last 4 first. +rewrite gaussIntE Re_rect ?Im_rect; last 4 first. - by rewrite !(rpredM, rpredV) 1? rpredD ?Rreal_int. - by rewrite !(rpredM, rpredV) 1? rpredB ?rpredD ?Rreal_int. - by rewrite !(rpredM, rpredV) 1? rpredD ?Rreal_int. @@ -1847,7 +1853,7 @@ by rewrite eqGI_sym mulGI_gcdl. Qed. -End GaussIntegers. +End gaussInts. Declare Scope GI_scope. Delimit Scope GI_scope with GI.