From c24c8d7853411b1c29cddc0e9ecfa7003e38957f Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 4 Jul 2025 12:31:24 +0900 Subject: [PATCH 1/4] rm forms.v --- CHANGELOG_UNRELEASED.md | 2 + _CoqProject | 2 - theories/Make | 1 - theories/all_analysis.v | 1 - theories/derive.v | 3 +- theories/forms.v | 564 ---------------------------------------- 6 files changed, 4 insertions(+), 569 deletions(-) delete mode 100644 theories/forms.v diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 67bb43c3b6..2e06d9019b 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -14,6 +14,8 @@ ### Removed +- file `forms.v` (superseded by MathComp's `sesquilinear.v`) + ### Infrastructure ### Misc diff --git a/_CoqProject b/_CoqProject index 4bd2a3f29c..9aeb2ba098 100644 --- a/_CoqProject +++ b/_CoqProject @@ -30,7 +30,6 @@ reals/constructive_ereal.v reals/reals.v reals/real_interval.v reals/signed.v -reals/interval_inference.v reals/prodnormedzmodule.v reals/all_reals.v experimental_reals/xfinmap.v @@ -93,7 +92,6 @@ theories/esum.v theories/measurable_realfun.v theories/lebesgue_measure.v theories/lebesgue_stieltjes_measure.v -theories/forms.v theories/derive.v theories/measure.v theories/numfun.v diff --git a/theories/Make b/theories/Make index c9088359b5..d80af9e6f2 100644 --- a/theories/Make +++ b/theories/Make @@ -57,7 +57,6 @@ trigo.v esum.v measurable_realfun.v lebesgue_measure.v -forms.v derive.v measure.v numfun.v diff --git a/theories/all_analysis.v b/theories/all_analysis.v index b567c76901..9043f05ae0 100644 --- a/theories/all_analysis.v +++ b/theories/all_analysis.v @@ -11,7 +11,6 @@ From mathcomp Require Export exp. From mathcomp Require Export trigo. From mathcomp Require Export esum. From mathcomp Require Export lebesgue_measure. -From mathcomp Require Export forms. From mathcomp Require Export derive. From mathcomp Require Export measure. From mathcomp Require Export numfun. diff --git a/theories/derive.v b/theories/derive.v index 9494425809..5362d57f99 100644 --- a/theories/derive.v +++ b/theories/derive.v @@ -1,9 +1,10 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum matrix interval poly. +From mathcomp Require Import sesquilinear. From mathcomp Require Import mathcomp_extra unstable boolp classical_sets. From mathcomp Require Import functions reals interval_inference topology. -From mathcomp Require Import prodnormedzmodule tvs normedtype landau forms. +From mathcomp Require Import prodnormedzmodule tvs normedtype landau. (**md**************************************************************************) (* # Differentiation *) diff --git a/theories/forms.v b/theories/forms.v deleted file mode 100644 index 524f0f36c2..0000000000 --- a/theories/forms.v +++ /dev/null @@ -1,564 +0,0 @@ -From HB Require Import structures. -From mathcomp Require Import all_ssreflect ssralg fingroup zmodp poly ssrnum. -From mathcomp Require Import matrix mxalgebra vector falgebra ssrnum fieldext. -From mathcomp Require Import vector mathcomp_extra. - -(**md**************************************************************************) -(* # Bilinear forms *) -(* (undocumented) *) -(******************************************************************************) - -Set Implicit Arguments. -Unset Strict Implicit. -Unset Printing Implicit Defensive. - -Local Open Scope ring_scope. -Import GRing.Theory Num.Theory. - -Reserved Notation "'[ u , v ]" (format "'[hv' ''[' u , '/ ' v ] ']'"). -Reserved Notation "'[ u , v ]_ M" (format "'[hv' ''[' u , '/ ' v ]_ M ']'"). -Reserved Notation "'[ u ]_ M" (format "''[' u ]_ M"). -Reserved Notation "'[ u ]" (format "''[' u ]"). -Reserved Notation "u '``_' i" - (at level 3, i at level 2, left associativity, format "u '``_' i"). -Reserved Notation "A ^_|_" (at level 8, format "A ^_|_"). -Reserved Notation "A _|_ B" (at level 69, format "A _|_ B"). -Reserved Notation "eps_theta .-sesqui" (format "eps_theta .-sesqui"). - -Notation "u '``_' i" := (u (0 : 'I_1) i) : ring_scope. -Notation "''e_' i" := (delta_mx 0 i) - (at level 8, i at level 2, format "''e_' i") : ring_scope. - -Local Notation "M ^ phi" := (map_mx phi M). -Local Notation "M ^t phi" := (map_mx phi (M ^T)) (phi at level 30, at level 30). - -Lemma eq_map_mx_id (R : ringType) m n (M : 'M[R]_(m,n)) (f : R -> R) : - f =1 id -> M ^ f = M. -Proof. by move=> /eq_map_mx->; rewrite map_mx_id. Qed. - -HB.mixin Record isBilinear (R : ringType) (U U' : lmodType R) (V : zmodType) - (s : R -> V -> V) (s' : R -> V -> V) (f : U -> U' -> V) := { - additivel_subproof : forall u', additive (f^~ u'); - additiver_subproof : forall u, additive (f u); - linearl_subproof : forall u', scalable_for s (f^~ u'); - linearr_subproof : forall u, scalable_for s' (f u); -}. - -HB.structure Definition Bilinear (R : ringType) (U U' : lmodType R) (V : zmodType) - (s : R -> V -> V) (s' : R -> V -> V) := - {f of isBilinear R U U' V s s' f}. - -Definition bilinear_for (R : ringType) (U U' : lmodType R) (V : zmodType) - (s : GRing.Scale.law R V) (s' : GRing.Scale.law R V) (f : U -> U' -> V) := - ((forall u', GRing.linear_for (s : R -> V -> V) (f^~ u')) - * (forall u, GRing.linear_for s' (f u)))%type. - -HB.factory Record bilinear_isBilinear (R : ringType) (U U' : lmodType R) (V : zmodType) - (s : GRing.Scale.law R V) (s' : GRing.Scale.law R V) (f : U -> U' -> V) := { - bilinear_subproof : bilinear_for s s' f; -}. - -HB.builders Context R U U' V s s' f of bilinear_isBilinear R U U' V s s' f. -HB.instance Definition _ := isBilinear.Build R U U' V s s' f - (fun u' => additive_linear (bilinear_subproof.1 u')) - (fun u => additive_linear (bilinear_subproof.2 u)) - (fun u' => scalable_linear (bilinear_subproof.1 u')) - (fun u => scalable_linear (bilinear_subproof.2 u)). -HB.end. - -Module BilinearExports. -Notation bilinear f := (bilinear_for *:%R *:%R f). -Notation biscalar f := (bilinear_for *%R *%R f). -Module Bilinear. -Definition map (R : ringType) (U U' : lmodType R) (V : zmodType) - (s : R -> V -> V) (s' : R -> V -> V) - (phUU'V : phant (U -> U' -> V)) := Bilinear.type U U' s s'. -End Bilinear. -Notation "{ 'bilinear' fUV | s & s' }" := (Bilinear.map s s' (Phant fUV)) - (at level 0, format "{ 'bilinear' fUV | s & s' }") : ring_scope. -Notation "{ 'bilinear' fUV | s }" := (Bilinear.map s.1 s.2 (Phant fUV)) - (at level 0, format "{ 'bilinear' fUV | s }") : ring_scope. -Notation "{ 'bilinear' fUV }" := {bilinear fUV | *:%R & *:%R} - (at level 0, format "{ 'bilinear' fUV }") : ring_scope. -Notation "{ 'biscalar' U }" := {bilinear U -> U -> _ | *%R & *%R} - (at level 0, format "{ 'biscalar' U }") : ring_scope. -Notation "[ 'bilinear' 'of' f 'as' g ]" := (Bilinear.clone _ _ _ _ _ _ f g) - (at level 0, format "[ 'bilinear' 'of' f 'as' g ]") : form_scope. -Notation "[ 'bilinear' 'of' f ]" := (Bilinear.clone _ _ _ _ _ _ f _) - (at level 0, format "[ 'bilinear' 'of' f ]") : form_scope. -End BilinearExports. -Export BilinearExports. - -Section applyr. - -Variables (R : ringType) (U U' : lmodType R) (V : zmodType) (s s' : R -> V -> V). - -(* Fact applyr_key : unit. Proof. exact. Qed. *) -Definition applyr_head t (f : U -> U' -> V) u v := let: tt := t in f v u. - -End applyr. - -Notation applyr := (applyr_head tt). - -Section BilinearTheory. - -Variable R : ringType. - -Section GenericProperties. - -Variables (U U' : lmodType R) (V : zmodType) (s : R -> V -> V) (s' : R -> V -> V). -Variable f : {bilinear U -> U' -> V | s & s'}. - -Section GenericPropertiesr. - -Variable z : U. - -#[local, non_forgetful_inheritance] -HB.instance Definition _ := - GRing.isAdditive.Build _ _ (f z) (@additiver_subproof _ _ _ _ _ _ f z). -#[local, non_forgetful_inheritance] -HB.instance Definition _ := - GRing.isScalable.Build _ _ _ _ (f z) (@linearr_subproof _ _ _ _ _ _ f z). - -Lemma linear0r : f z 0 = 0. Proof. by rewrite raddf0. Qed. -Lemma linearNr : {morph f z : x / - x}. Proof. exact: raddfN. Qed. -Lemma linearDr : {morph f z : x y / x + y}. Proof. exact: raddfD. Qed. -Lemma linearBr : {morph f z : x y / x - y}. Proof. exact: raddfB. Qed. -Lemma linearMnr n : {morph f z : x / x *+ n}. Proof. exact: raddfMn. Qed. -Lemma linearMNnr n : {morph f z : x / x *- n}. Proof. exact: raddfMNn. Qed. -Lemma linear_sumr I r (P : pred I) E : - f z (\sum_(i <- r | P i) E i) = \sum_(i <- r | P i) f z (E i). -Proof. exact: raddf_sum. Qed. - -Lemma linearZr_LR : scalable_for s' (f z). Proof. exact: linearZ_LR. Qed. -Lemma linearPr a : {morph f z : u v / a *: u + v >-> s' a u + v}. -Proof. exact: linearP. Qed. - -End GenericPropertiesr. - -Lemma applyrE x : applyr f x =1 f^~ x. Proof. by []. Qed. - -Section GenericPropertiesl. - -Variable z : U'. - -#[local, non_forgetful_inheritance] -HB.instance Definition _ := - GRing.isAdditive.Build _ _ (applyr f z) (@additivel_subproof _ _ _ _ _ _ f z). -#[local, non_forgetful_inheritance] -HB.instance Definition _ := - GRing.isScalable.Build _ _ _ _ (applyr f z) (@linearl_subproof _ _ _ _ _ _ f z). - -Lemma linear0l : f 0 z = 0. Proof. by rewrite -applyrE raddf0. Qed. -Lemma linearNl : {morph f^~ z : x / - x}. -Proof. by move=> ?; rewrite -applyrE raddfN. Qed. -Lemma linearDl : {morph f^~ z : x y / x + y}. -Proof. by move=> ??; rewrite -applyrE raddfD. Qed. -Lemma linearBl : {morph f^~ z : x y / x - y}. -Proof. by move=> ??; rewrite -applyrE raddfB. Qed. -Lemma linearMnl n : {morph f^~ z : x / x *+ n}. -Proof. by move=> ?; rewrite -applyrE raddfMn. Qed. -Lemma linearMNnl n : {morph f^~ z : x / x *- n}. -Proof. by move=> ?; rewrite -applyrE raddfMNn. Qed. -Lemma linear_suml I r (P : pred I) E : - f (\sum_(i <- r | P i) E i) z = \sum_(i <- r | P i) f (E i) z. -Proof. by rewrite -applyrE raddf_sum. Qed. - -Lemma linearZl_LR : scalable_for s (f^~ z). -Proof. by move=> ??; rewrite -applyrE linearZ_LR. Qed. -Lemma linearPl a : {morph f^~ z : u v / a *: u + v >-> s a u + v}. -Proof. by move=> ??; rewrite -applyrE linearP. Qed. - -End GenericPropertiesl. - -End GenericProperties. - -Section BidirectionalLinearZ. - -Variables (U : lmodType R) (V : zmodType) (s : R -> V -> V). -Variables (S : ringType) (h : GRing.Scale.law S V). - -(* Lemma linearZr z c a (h_c := GRing.Scale.op h_law c) (f : GRing.Linear.map_for U s a h_c) u : *) -(* f z (a *: u) = h_c (GRing.Linear.wrap (f z) u). *) -(* Proof. by rewrite linearZ_LR; case: f => f /= ->. Qed. *) - -End BidirectionalLinearZ. - -End BilinearTheory. - -Lemma mulmx_is_bilinear (R : comRingType) m n p : - bilinear_for - (GRing.Scale.Law.clone _ _ *:%R _) (GRing.Scale.Law.clone _ _ *:%R _) - (@mulmx R m n p). -Proof. -split=> [u'|u] a x y /=. -- by rewrite mulmxDl scalemxAl. -- by rewrite mulmxDr scalemxAr. -Qed. - -HB.instance Definition _ (R : comRingType) m n p := - bilinear_isBilinear.Build R - 'M[R]_(m, n) 'M[R]_(n, p) 'M[R]_(m, p) _ _ (@mulmx R m n p) - (mulmx_is_bilinear R m n p). - -(* Section classfun. *) -(* Import mathcomp.character.classfun. *) - -(* Canonical rev_cfdot (gT : finGroupType) (B : {set gT}) := *) -(* @RevOp _ _ _ (@cfdotr_head gT B tt) *) -(* (@cfdot gT B) (fun _ _ => erefl). *) - -(* Section Cfdot. *) -(* Variables (gT : finGroupType) (G : {group gT}). *) -(* Lemma cfdot_is_linear xi : linear_for (@conjC _ \; *%R) (cfdot xi : 'CF(G) -> algC^o). *) -(* Proof. *) -(* move=> /= a phi psi; rewrite cfdotC -cfdotrE linearD linearZ /=. *) -(* by rewrite !['[_, xi]]cfdotC rmorphD rmorphM !conjCK. *) -(* Qed. *) -(* Canonical cfdot_additive xi := Additive (cfdot_is_linear xi). *) -(* Canonical cfdot_linear xi := Linear (cfdot_is_linear xi). *) -(* End Cfdot. *) - -(* Canonical cfdot_bilinear (gT : finGroupType) (B : {group gT}) := *) -(* [bilinear of @cfdot gT B]. *) -(* End classfun. *) - -Section BilinearForms. - -Variables (R : fieldType) (theta : {rmorphism R -> R}). -Variables (n : nat) (M : 'M[R]_n). -Implicit Types (a b : R) (u v : 'rV[R]_n) (N P Q : 'M[R]_n). - -Definition form u v := (u *m M *m (v ^t theta)) 0 0. - -Local Notation "''[' u , v ]" := (form u%R v%R) : ring_scope. -Local Notation "''[' u ]" := '[u, u] : ring_scope. - -Lemma form0l u : '[0, u] = 0. -Proof. by rewrite /form !mul0mx mxE. Qed. - -Lemma form0r u : '[u, 0] = 0. -Proof. by rewrite /form trmx0 map_mx0 mulmx0 mxE. Qed. - -Lemma formDl u v w : '[u + v, w] = '[u, w] + '[v, w]. -Proof. by rewrite /form !mulmxDl mxE. Qed. - -Lemma formDr u v w : '[u, v + w] = '[u, v] + '[u, w]. -Proof. by rewrite /form linearD !map_mxD !mulmxDr mxE. Qed. - -Lemma formZr a u v : '[u, a *: v] = theta a * '[u, v]. -Proof. by rewrite /form !(linearZ, map_mxZ) /= mxE. Qed. - -Lemma formZl a u v : '[a *: u, v] = a * '[u, v]. -Proof. -by do !rewrite /form -[_ *: _ *m _]/(mulmxr _ _) linearZ /=; rewrite mxE. -Qed. - -Lemma formNl u v : '[- u, v] = - '[u, v]. -Proof. by rewrite -scaleN1r formZl mulN1r. Qed. - -Lemma formNr u v : '[u, - v] = - '[u, v]. -Proof. by rewrite -scaleN1r formZr rmorphN1 mulN1r. Qed. - -Lemma formee i j : '['e_i, 'e_j] = M i j. -Proof. -rewrite /form -rowE -map_trmx map_delta_mx -[M in LHS]trmxK. -by rewrite -tr_col -trmx_mul -rowE !mxE. -Qed. - -Lemma form0_eq0 : M = 0 -> forall u v, '[u, v] = 0. -Proof. by rewrite/form=> -> u v; rewrite mulmx0 mul0mx mxE. Qed. - -End BilinearForms. - -Section Sesquilinear. - -Variable R : fieldType. -Variable n : nat. -Implicit Types (a b : R) (u v : 'rV[R]_n) (N P Q : 'M[R]_n). - -Section Def. -Variable eps_theta : (bool * {rmorphism R -> R}). - -Definition sesqui := - [qualify M : 'M_n | M == ((-1) ^+ eps_theta.1) *: M ^t eps_theta.2]. -Fact sesqui_key : pred_key sesqui. Proof. by []. Qed. -Canonical sesqui_keyed := KeyedQualifier sesqui_key. -End Def. - -Local Notation "eps_theta .-sesqui" := (sesqui eps_theta). - -Variables (eps : bool) (theta : {rmorphism R -> R}). -Variables (M : 'M[R]_n). -Local Notation "''[' u , v ]" := (form theta M u%R v%R) : ring_scope. -Local Notation "''[' u ]" := '[u, u] : ring_scope. - -Lemma sesquiE : (M \is (eps,theta).-sesqui) = (M == (-1) ^+ eps *: M ^t theta). -Proof. by rewrite qualifE. Qed. - -Lemma sesquiP : reflect (M = (-1) ^+ eps *: M ^t theta) - (M \is (eps,theta).-sesqui). -Proof. by rewrite sesquiE; apply/eqP. Qed. - -Hypothesis (thetaK : involutive theta). -Hypothesis (M_sesqui : M \is (eps, theta).-sesqui). - -Lemma trmx_sesqui : M^T = (-1) ^+ eps *: M ^ theta. -Proof. -rewrite [in LHS](sesquiP _) // -mul_scalar_mx trmx_mul. -by rewrite tr_scalar_mx mul_mx_scalar map_trmx trmxK. -Qed. - -Lemma maptrmx_sesqui : M^t theta = (-1) ^+ eps *: M. -Proof. -by rewrite trmx_sesqui map_mxZ rmorph_sign -map_mx_comp eq_map_mx_id. -Qed. - -Lemma formC u v : '[u, v] = (-1) ^+ eps * theta '[v, u]. -Proof. -rewrite /form [M in LHS](sesquiP _) // -mulmxA !mxE rmorph_sum mulr_sumr. -apply: eq_bigr => /= i _; rewrite !(mxE, mulr_sumr, mulr_suml, rmorph_sum). -apply: eq_bigr => /= j _; rewrite !mxE !rmorphM mulrCA -!mulrA. -by congr (_ * _); rewrite mulrA mulrC /= thetaK. -Qed. - -Lemma form_eq0C u v : ('[u, v] == 0) = ('[v, u] == 0). -Proof. by rewrite formC mulf_eq0 signr_eq0 /= fmorph_eq0. Qed. - -Definition ortho m (B : 'M_(m,n)) := (kermx (M *m (B ^t theta))). -Local Notation "B ^_|_" := (ortho B) : ring_scope. -Local Notation "A _|_ B" := (A%MS <= B^_|_)%MS : ring_scope. - -Lemma normalE u v : (u _|_ v) = ('[u, v] == 0). -Proof. -by rewrite (sameP sub_kermxP eqP) mulmxA [_ *m _^t _]mx11_scalar fmorph_eq0. -Qed. - -Lemma form_eq0P {u v} : reflect ('[u, v] = 0) (u _|_ v). -Proof. by rewrite normalE; apply/eqP. Qed. - -Lemma normalP p q (A : 'M_(p, n)) (B :'M_(q, n)) : - reflect (forall (u v : 'rV_n), (u <= A)%MS -> (v <= B)%MS -> u _|_ v) - (A _|_ B). -Proof. -apply: (iffP idP) => AnB. - move=> u v uA vB; rewrite (submx_trans uA) // (submx_trans AnB) //. - apply/sub_kermxP; have /submxP [w ->] := vB. - rewrite trmx_mul map_mxM !mulmxA -[kermx _ *m _ *m _]mulmxA. - by rewrite [kermx _ *m _](sub_kermxP _) // mul0mx. -apply/rV_subP => u /AnB /(_ _) /sub_kermxP uMv; apply/sub_kermxP. -suff: forall m (v : 'rV[R]_m), - (forall i, v *m 'e_i ^t theta = 0 :> 'M_1) -> v = 0. - apply => i; rewrite !mulmxA -!mulmxA -map_mxM -trmx_mul uMv //. - by apply/submxP; exists 'e_i. -move=> /= m v Hv; apply: (can_inj (@trmxK _ _ _)). -rewrite trmx0; apply/row_matrixP=> i; rewrite row0 rowE. -apply: (can_inj (@trmxK _ _ _)); rewrite trmx0 trmx_mul trmxK. -by rewrite -(map_delta_mx theta) map_trmx Hv. -Qed. - -Lemma normalC p q (A : 'M_(p, n)) (B :'M_(q, n)) : (A _|_ B) = (B _|_ A). -Proof. -gen have nC : p q A B / A _|_ B -> B _|_ A; last by apply/idP/idP; apply/nC. -move=> AnB; apply/normalP => u v ? ?; rewrite normalE. -rewrite formC mulf_eq0 ?fmorph_eq0 ?signr_eq0 /=. -by rewrite -normalE (normalP _ _ AnB). -Qed. - -Lemma normal_ortho_mx p (A : 'M_(p, n)) : ((A^_|_) _|_ A). -Proof. by []. Qed. - -Lemma normal_mx_ortho p (A : 'M_(p, n)) : (A _|_ (A^_|_)). -Proof. by rewrite normalC. Qed. - -Lemma rank_normal u : (\rank (u ^_|_) >= n.-1)%N. -Proof. -rewrite mxrank_ker -subn1 leq_sub2l //. -by rewrite (leq_trans (mxrankM_maxr _ _)) // rank_leq_col. -Qed. - -Definition rad := 1%:M^_|_. - -Lemma rad_ker : rad = kermx M. -Proof. by rewrite /rad /ortho trmx1 map_mx1 mulmx1. Qed. - -(* Pythagore *) -Theorem formDd u v : u _|_ v -> '[u + v] = '[u] + '[v]. -Proof. -move=> uNv; rewrite formDl !formDr ['[v, u]]formC. -by rewrite ['[u, v]](form_eq0P _) // rmorph0 mulr0 addr0 add0r. -Qed. - -Lemma formZ a u : '[a *: u]= (a * theta a) * '[u]. -Proof. by rewrite formZl formZr mulrA. Qed. - -Lemma formN u : '[- u] = '[u]. -Proof. by rewrite formNr formNl opprK. Qed. - -Lemma form_sign m u : '[(-1) ^+ m *: u] = '[u]. -Proof. by rewrite -signr_odd scaler_sign; case: odd; rewrite ?formN. Qed. - -Lemma formD u v : let d := '[u, v] in - '[u + v] = '[u] + '[v] + (d + (-1) ^+ eps * theta d). -Proof. by rewrite formDl !formDr ['[v, _]]formC [_ + '[v]]addrC addrACA. Qed. - -Lemma formB u v : let d := '[u, v] in - '[u - v] = '[u] + '[v] - (d + (-1) ^+ eps * theta d). -Proof. by rewrite formD formN !formNr rmorphN mulrN -opprD. Qed. - -Lemma formBd u v : u _|_ v -> '[u - v] = '[u] + '[v]. -Proof. -by move=> uTv; rewrite formDd ?formN // normalE formNr oppr_eq0 -normalE. -Qed. - -(* Lemma formJ u v : '[u ^ theta, v ^ theta] = (-1) ^+ eps * theta '[u, v]. *) -(* Proof. *) -(* rewrite {1}/form -map_trmx -map_mx_comp (@eq_map_mx _ _ _ _ _ id) ?map_mx_id //. *) -(* set x := (_ *m _); have -> : x 0 0 = theta ((x^t theta) 0 0) by rewrite !mxE. *) -(* rewrite !trmx_mul trmxK map_trmx mulmxA !map_mxM. *) -(* rewrite maptrmx_sesqui -!scalemxAr -scalemxAl mxE rmorphM rmorph_sign. *) - -(* Lemma formJ u : '[u ^ theta] = (-1) ^+ eps * '[u]. *) -(* Proof. *) -(* rewrite {1}/form -map_trmx -map_mx_comp (@eq_map_mx _ _ _ _ _ id) ?map_mx_id //. *) -(* set x := (_ *m _); have -> : x 0 0 = theta ((x^t theta) 0 0) by rewrite !mxE. *) -(* rewrite !trmx_mul trmxK map_trmx mulmxA !map_mxM. *) -(* rewrite maptrmx_sesqui -!scalemxAr -scalemxAl mxE rmorphM rmorph_sign. *) -(* rewrite !map_mxM. *) -(* rewrite -map_mx_comp eq_map_mx_id //. *) -(* !linearZr_LR /=. linearZ. *) -(* linearZl. *) -(* rewrite trmx_sesqui. *) - - -(* rewrite mapmx. *) -(* rewrite map *) -(* apply/matrixP. *) - -(* rewrite formC. *) -(* Proof. by rewrite cfdot_conjC geC0_conj // cfnorm_ge0. Qed. *) - -(* Lemma cfCauchySchwarz u v : *) -(* `|'[u, v]| ^+ 2 <= '[u] * '[v] ?= iff ~~ free (u :: v). *) -(* Proof. *) -(* rewrite free_cons span_seq1 seq1_free -negb_or negbK orbC. *) -(* have [-> | nz_v] /= := altP (v =P 0). *) -(* by apply/lerifP; rewrite !cfdot0r normCK mul0r mulr0. *) -(* without loss ou: u / '[u, v] = 0. *) -(* move=> IHo; pose a := '[u, v] / '[v]; pose u1 := u - a *: v. *) -(* have ou: '[u1, v] = 0. *) -(* by rewrite cfdotBl cfdotZl divfK ?cfnorm_eq0 ?subrr. *) -(* rewrite (canRL (subrK _) (erefl u1)) rpredDr ?rpredZ ?memv_line //. *) -(* rewrite cfdotDl ou add0r cfdotZl normrM (ger0_norm (cfnorm_ge0 _)). *) -(* rewrite exprMn mulrA -cfnormZ cfnormDd; last by rewrite cfdotZr ou mulr0. *) -(* by have:= IHo _ ou; rewrite mulrDl -lerif_subLR subrr ou normCK mul0r. *) -(* rewrite ou normCK mul0r; split; first by rewrite mulr_ge0 ?cfnorm_ge0. *) -(* rewrite eq_sym mulf_eq0 orbC cfnorm_eq0 (negPf nz_v) /=. *) -(* apply/idP/idP=> [|/vlineP[a {2}->]]; last by rewrite cfdotZr ou mulr0. *) -(* by rewrite cfnorm_eq0 => /eqP->; apply: rpred0. *) -(* Qed. *) - -End Sesquilinear. - -Notation "eps_theta .-sesqui" := (sesqui _ eps_theta) : ring_scope. - -Notation symmetric_form := (false, idfun).-sesqui. -Notation skew := (true, idfun).-sesqui. -Notation hermitian := (false, @Num.conj_op _).-sesqui. - -(* Section ClassificationForm. *) - -(* Variables (F : fieldType) (L : fieldExtType) (theat : 'Aut()) *) - -(* Notation "''[' u , v ]_ M" := (form M%R u%R v%R) : ring_scope. *) -(* Notation "''[' u ]_ M" := (form M%R u%R u%R) : ring_scope. *) - -(* Hypothesis (thetaK : involutive theta). *) - -(* Lemma sesqui_test M : (forall u v, '[v, u]_M = 0 -> '[u, v]_M = 0) -> *) -(* {eps | eps^+2 = 1 & M \is (eps,theta).-sesqui}. *) -(* Proof. *) -(* pose *) - - -(* [/\ forall u, '[u] = 0, theta =1 id & eps = -1] *) -(* \/ ((exists u, '[u] != 0) /\ (eps = 1)). *) -(* Proof. *) -(* move=> M_neq0 form_eq0. *) -(* have [] := boolP [forall i : 'I_n, '['e_i] == 0]; last first. *) -(* rewrite negb_forall => /existsP [i ei_neq0]. *) -(* right; split; first by exists ('e_i). *) -(* apply/eqP; *) - -(* contraT *) - - -(* suff [f_eq0|] : (forall u, '[u] = 0) \/ (exists u, '[u] != 0). *) -(* left; split=> //. *) - -(* have [] := boolP [forall i : 'I_n, '['e_i] == 0]. *) - -(* suff /eqP : eps ^+ 2 = 1. *) -(* rewrite -subr_eq0 subr_sqr_1 mulf_eq0. *) -(* move => /orP[]; rewrite addr_eq0 ?opprK=> /eqP eps_eq. *) -(* right; split=> //. *) - -(* have [] := boolP [forall i : 'I_n, '['e_i] == 0]. *) - -(* have := sesquiC u u. *) - - -(* rewrite !linearZ /= -[eps *: _ *m _]/(mulmxr _ _) linearZ /= mxE; congr (_ * _). *) -(* have : u = map_mx theta (map_mx theta u). *) -(* apply/rowP=> i; rewrite !mxE. *) -(* rewrite -[in LHS]mulmxA -map_mxM. *) -(* rewrite *) -(* !mxE rmorph_sum; apply: eq_bigr => /= i _; rewrite !mxE. *) -(* rewrite !rmorphM thetaK rmorph_sum. *) - -(* Hypothesis (M_sesqui : M \is (eps, theta).-sesqui). *) - -(* rewrite -[a *: u *m _]/(mulmxr _ _). *) -(* rewrite linearZ. *) - -(* Variables (R : fieldType) (n : nat). *) - -(* Local Notation "A _|_ B" := (A%MS <= kermx B%MS^T)%MS. *) - -(* Lemma normal_sym k m (A : 'M[R]_(k,n)) (B : 'M[R]_(m,n)) : *) -(* A _|_ B = B _|_ A. *) -(* Proof. *) -(* rewrite !(sameP sub_kermxP eqP) -{1}[A]trmxK -trmx_mul. *) -(* by rewrite -{1}trmx0 (inj_eq (@trmx_inj _ _ _)). *) -(* Qed. *) - -(* Lemma normalNm k m (A : 'M[R]_(k,n)) (B : 'M[R]_(m,n)) : (- A) _|_ B = A _|_ B. *) -(* Proof. by rewrite eqmx_opp. Qed. *) - -(* Lemma normalmN k m (A : 'M[R]_(k,n)) (B : 'M[R]_(m,n)) : A _|_ (- B) = A _|_ B. *) -(* Proof. by rewrite ![A _|_ _]normal_sym normalNm. Qed. *) - -(* Lemma normalDm k m p (A : 'M[R]_(k,n)) (B : 'M[R]_(m,n)) (C : 'M[R]_(p,n)) : *) -(* (A + B _|_ C) = (A _|_ C) && (B _|_ C). *) -(* Proof. by rewrite addsmxE !(sameP sub_kermxP eqP) mul_col_mx col_mx_eq0. Qed. *) - -(* Lemma normalmD k m p (A : 'M[R]_(k,n)) (B : 'M[R]_(m,n)) (C : 'M[R]_(p,n)) : *) -(* (A _|_ B + C) = (A _|_ B) && (A _|_ C). *) -(* Proof. by rewrite ![A _|_ _]normal_sym normalDm. Qed. *) - -(* Definition dot (u v : 'rV[R]_n) : R := (u *m v^T) 0 0. *) - -(* Notation "''[' u , v ]" := (dot u v) : ring_scope. *) -(* Notation "''[' u ]" := '[u, u]%MS : ring_scope. *) - -(* Lemma dotmulE (u v : 'rV[R]_n) : '[u, v] = \sum_k u``_k * v``_k. *) -(* Proof. by rewrite [LHS]mxE; apply: eq_bigr=> i; rewrite mxE. Qed. *) - -(* Lemma normalvv (u v : 'rV[R]_n) : (u _|_ v) = ('[u, v] == 0). *) -(* Proof. by rewrite (sameP sub_kermxP eqP) [_ *m _^T]mx11_scalar fmorph_eq0. Qed. *) - -(* End Normal. *) - -(* Local Notation "''[' u , v ]" := (form u v) : ring_scope. *) -(* Local Notation "''[' u ]" := '[u%R, u%R] : ring_scope. *) -(* Local Notation "A _|_ B" := (A%MS <= kermx B%MS^T)%MS. *) From d589405c1c01f119fd8404eeb068946c1bb9e7af Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 7 Jul 2025 08:38:34 +0900 Subject: [PATCH 2/4] drop MC 2.2 --- coq-mathcomp-classical.opam | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/coq-mathcomp-classical.opam b/coq-mathcomp-classical.opam index 3f74755023..c8d1f862a5 100644 --- a/coq-mathcomp-classical.opam +++ b/coq-mathcomp-classical.opam @@ -17,7 +17,7 @@ install: [make "-C" "classical" "install"] depends: [ ("coq" {>= "8.20" & < "8.21~"} | "coq-core" { (>= "9.0" & < "9.1~") | (= "dev") }) - "coq-mathcomp-ssreflect" { (>= "2.2.0" & < "2.5~") | (= "dev") } + "coq-mathcomp-ssreflect" { (>= "2.3.0" & < "2.5~") | (= "dev") } "coq-mathcomp-fingroup" "coq-mathcomp-algebra" "coq-mathcomp-finmap" { (>= "2.1.0") } From 15deff341c0a01235c359a9d1a9a79fbeef09376 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 7 Jul 2025 18:55:41 +0900 Subject: [PATCH 3/4] drop MC 2.2 on nix --- .nix/config.nix | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.nix/config.nix b/.nix/config.nix index c4a5558666..1c2452fe09 100644 --- a/.nix/config.nix +++ b/.nix/config.nix @@ -51,7 +51,7 @@ in bundles."8.20".coqPackages = common-bundle // { coq.override.version = "8.20"; - mathcomp.override.version = "2.2.0"; + mathcomp.override.version = "2.3.0"; }; bundles."9.0".coqPackages = common-bundle // { From fa15ee67393d15386502290eb718e211ae2a4b31 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 7 Jul 2025 20:45:19 +0900 Subject: [PATCH 4/4] fix --- _CoqProject | 1 + 1 file changed, 1 insertion(+) diff --git a/_CoqProject b/_CoqProject index 9aeb2ba098..7feb87c50a 100644 --- a/_CoqProject +++ b/_CoqProject @@ -30,6 +30,7 @@ reals/constructive_ereal.v reals/reals.v reals/real_interval.v reals/signed.v +reals/interval_inference.v reals/prodnormedzmodule.v reals/all_reals.v experimental_reals/xfinmap.v