From ffda7780264fc48805d1fef1514413111c3b29cd Mon Sep 17 00:00:00 2001 From: Yves Bertot Date: Wed, 28 Jul 2021 13:38:03 +0200 Subject: [PATCH 1/4] modulus of the inverse, easy consequence of normcM modified: theories/complex.v --- theories/complex.v | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/theories/complex.v b/theories/complex.v index 58bdd5a..4b43e09 100644 --- a/theories/complex.v +++ b/theories/complex.v @@ -286,6 +286,18 @@ Qed. Lemma normCM x y : normC (x * y) = normC x * normC y. Proof. by rewrite -rmorphM normcM. Qed. +Lemma normcV x : normc (x ^-1) = (normc x)^-1. +Proof. +have [/eqP -> | xn0] := boolP(x == 0); last first. + have normxn0 : normc x != 0 by apply/eqP=> /eq0_normc /eqP; apply/negP. + apply: (mulfI normxn0); rewrite mulfV // -normcM mulfV //. + by rewrite /normc /= expr0n /= addr0 expr1n sqrtr1. +by rewrite /= mul0r oppr0 expr0n addr0 sqrtr0 invr0. +Qed. + +Lemma normCV x : normC(x ^-1) = (normC x) ^-1. +Proof. by rewrite -fmorphV normcV. Qed. + Lemma subc_ge0 x y : lec 0 (y - x) = lec x y. Proof. by move: x y => [a b] [c d] /=; simpc; rewrite subr_ge0 subr_eq0. Qed. From f85049542715d9be49d76a711f06c5f768027450 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 5 Jul 2022 00:49:44 +0900 Subject: [PATCH 2/4] normc0, normc1 --- theories/complex.v | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) diff --git a/theories/complex.v b/theories/complex.v index 4b43e09..49d7f4b 100644 --- a/theories/complex.v +++ b/theories/complex.v @@ -252,6 +252,12 @@ Definition normc (x : R[i]) : R := Notation normC x := (normc x)%:C. +Lemma normc0 : normc 0%C = 0. +Proof. by rewrite /normc /= expr0n/= addr0 sqrtr0. Qed. + +Lemma normc1 : normc 1%C = 1. +Proof. by rewrite /normc /= expr0n/= expr1n addr0 sqrtr1. Qed. + Lemma ltc0_add : forall x y, ltc 0 x -> ltc 0 y -> ltc 0 (x + y). Proof. move=> [a b] [c d] /= /andP [/eqP-> ha] /andP [/eqP-> hc]. @@ -286,16 +292,14 @@ Qed. Lemma normCM x y : normC (x * y) = normC x * normC y. Proof. by rewrite -rmorphM normcM. Qed. -Lemma normcV x : normc (x ^-1) = (normc x)^-1. +Lemma normcV x : normc x^-1 = (normc x)^-1. Proof. -have [/eqP -> | xn0] := boolP(x == 0); last first. - have normxn0 : normc x != 0 by apply/eqP=> /eq0_normc /eqP; apply/negP. - apply: (mulfI normxn0); rewrite mulfV // -normcM mulfV //. - by rewrite /normc /= expr0n /= addr0 expr1n sqrtr1. -by rewrite /= mul0r oppr0 expr0n addr0 sqrtr0 invr0. +have [->|x0] := eqVneq x 0; first by rewrite ?(invr0,normc0). +have nx0 : normc x != 0 by apply: contra x0 => /eqP/eq0_normc ->. +by apply: (mulfI nx0); rewrite -normcM !divrr ?unitfE// normc1. Qed. -Lemma normCV x : normC(x ^-1) = (normC x) ^-1. +Lemma normCV x : normC x^-1 = (normC x)^-1. Proof. by rewrite -fmorphV normcV. Qed. Lemma subc_ge0 x y : lec 0 (y - x) = lec x y. From a8fa900e864da750e3e279c79035165942f7c1f2 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 5 Jul 2022 00:59:58 +0900 Subject: [PATCH 3/4] normCV is already available as normfV --- theories/complex.v | 3 --- 1 file changed, 3 deletions(-) diff --git a/theories/complex.v b/theories/complex.v index 49d7f4b..93bdc68 100644 --- a/theories/complex.v +++ b/theories/complex.v @@ -299,9 +299,6 @@ have nx0 : normc x != 0 by apply: contra x0 => /eqP/eq0_normc ->. by apply: (mulfI nx0); rewrite -normcM !divrr ?unitfE// normc1. Qed. -Lemma normCV x : normC x^-1 = (normC x)^-1. -Proof. by rewrite -fmorphV normcV. Qed. - Lemma subc_ge0 x y : lec 0 (y - x) = lec x y. Proof. by move: x y => [a b] [c d] /=; simpc; rewrite subr_ge0 subr_eq0. Qed. From 4e9346fbf59fb9e1fce294472458f90fa05b516e Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 5 Jul 2022 17:03:47 +0900 Subject: [PATCH 4/4] put normc in a module --- theories/complex.v | 109 +++++++++++++++++++++++++-------------------- 1 file changed, 60 insertions(+), 49 deletions(-) diff --git a/theories/complex.v b/theories/complex.v index 93bdc68..51c0a3f 100644 --- a/theories/complex.v +++ b/theories/complex.v @@ -219,9 +219,52 @@ Canonical real_complex_additive := End ComplexField_realFieldType. -Section ComplexField. +Module Normc. +Section Normc. +Variable R : rcfType. +Implicit Types x : R[i]. + +(* TODO: when Pythagorean Fields are added, weaken to Pythagorean Field *) +Definition normc x := + let: a +i* b := x in sqrtr (a ^+ 2 + b ^+ 2). + +Lemma normc0 : normc 0%C = 0 :> R. +Proof. by rewrite /normc /= expr0n/= addr0 sqrtr0. Qed. + +Lemma normc1 : normc 1%C = 1 :> R. +Proof. by rewrite /normc /= expr0n/= expr1n addr0 sqrtr1. Qed. + +Lemma eq0_normc x : normc x = 0 -> x = 0. +Proof. +case: x => a b /= /eqP; rewrite sqrtr_eq0 le_eqVlt => /orP[|]; last first. + by rewrite ltNge addr_ge0 ?sqr_ge0. +by rewrite paddr_eq0 ?sqr_ge0 ?expf_eq0 //= => /andP[/eqP -> /eqP ->]. +Qed. +Lemma normcM x y : normc (x * y) = normc x * normc y. +Proof. +move: x y => [a b] [c d] /=; rewrite -sqrtrM ?addr_ge0 ?sqr_ge0 //. +rewrite sqrrB sqrrD mulrDl !mulrDr -!exprMn. +rewrite mulrAC [b * d]mulrC !mulrA. +suff -> : forall (u v w z t : R), (u - v + w) + (z + v + t) = u + w + (z + t). + by rewrite addrAC !addrA. +by move=> u v w z t; rewrite [_ - _ + _]addrAC [z + v]addrC !addrA addrNK. +Qed. + +Lemma normcV x : normc x^-1 = (normc x)^-1. +Proof. +have [->|x0] := eqVneq x 0; first by rewrite ?(invr0,normc0). +have nx0 : normc x != 0 by apply: contra x0 => /eqP/eq0_normc ->. +by apply: (mulfI nx0); rewrite -normcM !divrr ?unitfE// normc1. +Qed. + +End Normc. +End Normc. + +Section ComplexField. Variable R : rcfType. +Implicit Types x y : R[i]. + Local Notation C := R[i]. Local Notation C0 := ((0 : R)%:C). Local Notation C1 := ((1 : R)%:C). @@ -238,69 +281,43 @@ Proof. by move=> a [b c] [d e]. Qed. Canonical Im_additive := Additive Im_is_scalar. Canonical Im_linear := Linear Im_is_scalar. -Definition lec (x y : R[i]) := +Definition lec x y := let: a +i* b := x in let: c +i* d := y in (d == b) && (a <= c). -Definition ltc (x y : R[i]) := +Definition ltc x y := let: a +i* b := x in let: c +i* d := y in (d == b) && (a < c). -(* TODO: when Pythagorean Fields are added, weaken to Pythagorean Field *) -Definition normc (x : R[i]) : R := - let: a +i* b := x in sqrtr (a ^+ 2 + b ^+ 2). - -Notation normC x := (normc x)%:C. - -Lemma normc0 : normc 0%C = 0. -Proof. by rewrite /normc /= expr0n/= addr0 sqrtr0. Qed. - -Lemma normc1 : normc 1%C = 1. -Proof. by rewrite /normc /= expr0n/= expr1n addr0 sqrtr1. Qed. - -Lemma ltc0_add : forall x y, ltc 0 x -> ltc 0 y -> ltc 0 (x + y). +Lemma ltc0_add x y : ltc 0 x -> ltc 0 y -> ltc 0 (x + y). Proof. -move=> [a b] [c d] /= /andP [/eqP-> ha] /andP [/eqP-> hc]. +move: x y => [a b] [c d] /= /andP [/eqP-> ha] /andP [/eqP-> hc]. by rewrite addr0 eqxx addr_gt0. Qed. -Lemma eq0_normc x : normc x = 0 -> x = 0. -Proof. -case: x => a b /= /eqP; rewrite sqrtr_eq0 le_eqVlt => /orP [|]; last first. - by rewrite ltNge addr_ge0 ?sqr_ge0. -by rewrite paddr_eq0 ?sqr_ge0 ?expf_eq0 //= => /andP[/eqP -> /eqP ->]. -Qed. - -Lemma eq0_normC x : normC x = 0 -> x = 0. Proof. by case=> /eq0_normc. Qed. - Lemma ge0_lec_total x y : lec 0 x -> lec 0 y -> lec x y || lec y x. Proof. move: x y => [a b] [c d] /= /andP[/eqP -> a_ge0] /andP[/eqP -> c_ge0]. by rewrite eqxx le_total. Qed. -Lemma normcM x y : normc (x * y) = normc x * normc y. +Lemma subc_ge0 x y : lec 0 (y - x) = lec x y. +Proof. by move: x y => [a b] [c d] /=; simpc; rewrite subr_ge0 subr_eq0. Qed. + +Lemma ltc_def x y : ltc x y = (y != x) && lec x y. Proof. -move: x y => [a b] [c d] /=; rewrite -sqrtrM ?addr_ge0 ?sqr_ge0 //. -rewrite sqrrB sqrrD mulrDl !mulrDr -!exprMn. -rewrite mulrAC [b * d]mulrC !mulrA. -suff -> : forall (u v w z t : R), (u - v + w) + (z + v + t) = u + w + (z + t). - by rewrite addrAC !addrA. -by move=> u v w z t; rewrite [_ - _ + _]addrAC [z + v]addrC !addrA addrNK. +move: x y => [a b] [c d] /=; simpc; rewrite eq_complex /=. +by have [] := altP eqP; rewrite ?(andbF, andbT) //= lt_def. Qed. -Lemma normCM x y : normC (x * y) = normC x * normC y. -Proof. by rewrite -rmorphM normcM. Qed. +Import Normc. -Lemma normcV x : normc x^-1 = (normc x)^-1. -Proof. -have [->|x0] := eqVneq x 0; first by rewrite ?(invr0,normc0). -have nx0 : normc x != 0 by apply: contra x0 => /eqP/eq0_normc ->. -by apply: (mulfI nx0); rewrite -normcM !divrr ?unitfE// normc1. -Qed. +Notation normC x := (normc x)%:C. -Lemma subc_ge0 x y : lec 0 (y - x) = lec x y. -Proof. by move: x y => [a b] [c d] /=; simpc; rewrite subr_ge0 subr_eq0. Qed. +Lemma eq0_normC x : normC x = 0 -> x = 0. Proof. by case=> /eq0_normc. Qed. + +Lemma normCM x y : normC (x * y) = normC x * normC y. +Proof. by rewrite -rmorphM normcM. Qed. Lemma lec_def x y : lec x y = (normC (y - x) == y - x). Proof. @@ -309,12 +326,6 @@ have [<- /=|_] := altP eqP; last by rewrite andbF. by rewrite [0 ^+ _]mul0r addr0 andbT sqrtr_sqr ger0_def. Qed. -Lemma ltc_def x y : ltc x y = (y != x) && lec x y. -Proof. -move: x y => [a b] [c d] /=; simpc; rewrite eq_complex /=. -by have [] := altP eqP; rewrite ?(andbF, andbT) //= lt_def. -Qed. - Lemma lec_normD x y : lec (normC (x + y)) (normC x + normC y). Proof. move: x y => [a b] [c d] /=; simpc; rewrite addr0 eqxx /=.