From c7f7ae57f333da67eadbd89b7efaabe628450b41 Mon Sep 17 00:00:00 2001 From: YAMAMOTO Mitsuharu Date: Tue, 26 Mar 2024 14:45:06 +0900 Subject: [PATCH 1/4] Add solve_Qint_span to intdiv.v. --- CHANGELOG_UNRELEASED.md | 3 ++ mathcomp/algebra/intdiv.v | 79 +++++++++++++++++++++++++++++++-------- 2 files changed, 67 insertions(+), 15 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 5209d76013..211486eb87 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -20,6 +20,9 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/). - in `path.v` + lemma `count_sort` +- in `intdiv.v` + + lemma `solve_Qint_span` + ### Changed - in `bigop.v` diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v index feb87cf697..c734cb88a0 100644 --- a/mathcomp/algebra/intdiv.v +++ b/mathcomp/algebra/intdiv.v @@ -1030,8 +1030,13 @@ Qed. Definition inIntSpan (V : zmodType) m (s : m.-tuple V) v := exists a : int ^ m, v = \sum_(i < m) s`_i *~ a i. -Lemma dec_Qint_span (vT : vectType rat) m (s : m.-tuple vT) v : - decidable (inIntSpan s v). +Lemma solve_Qint_span (vT : vectType rat) m (s : m.-tuple vT) v : + {b : int ^ m & + {p : seq (int ^ m) & + forall a : int ^ m, + v = \sum_(i < m) s`_i *~ a i <-> + exists c : seq int, a = b + \sum_(i < size p) p`_i *~ c`_i}} + + (~ inIntSpan s v). Proof. have s_s (i : 'I_m): s`_i \in <>%VS by rewrite memv_span ?memt_nth. have s_Zs a: \sum_(i < m) s`_i *~ a i \in <>%VS. @@ -1051,7 +1056,8 @@ have [K kerK]: {K : 'M_(k, m) | map_mx intr K == kermx S}%MS. by rewrite intr_eq0; apply/prodf_neq0 => i _; apply: denq_neq0. have [L _ [G uG [D _ defK]]] := int_Smith_normal_form K. pose Gud := castmx (Dm, Em) G; pose G'lr := castmx (Em, Dm) (invmx G). -have{K L D defK kerK} kerGu: map_mx intr (usubmx Gud) *m S = 0. +have{K L D defK kerK} [kerGu kerS_sub_Gu]: map_mx intr (usubmx Gud) *m S = 0 /\ + (kermx S <= map_mx intr (usubmx Gud))%MS. pose Kl : 'M[rat]_k:= map_mx intr (lsubmx (castmx (Ek, Dm) (K *m invmx G))). have{} defK: map_mx intr K = row_mx Kl 0 *m map_mx intr Gud. rewrite -[K](mulmxKV uG) -{2}[G](castmxK Dm Em) -/Gud. @@ -1061,6 +1067,9 @@ have{K L D defK kerK} kerGu: map_mx intr (usubmx Gud) *m S = 0. congr (row_mx _ _ *m _); apply/matrixP=> i j; rewrite !mxE defK mulmxK //=. rewrite castmxE mxE big1 //= => j1 _; rewrite mxE /= eqn_leq andbC. by rewrite leqNgt (leq_trans (valP j1)) ?mulr0 ?leq_addr. + split; last first. + rewrite -(eqmxP kerK); apply/submxP; exists Kl. + by rewrite defK -{1}[Gud]vsubmxK map_col_mx mul_row_col mul0mx addr0. have /row_full_inj: row_full Kl; last apply. rewrite /row_full eqn_leq rank_leq_row /= -{1}[k](mxrank_ker S). rewrite -(eqmxP kerK) defK map_castmx mxrankMfree; last first. @@ -1070,7 +1079,7 @@ have{K L D defK kerK} kerGu: map_mx intr (usubmx Gud) *m S = 0. rewrite mulmx0 mulmxA (sub_kermxP _) // -(eqmxP kerK) defK. by rewrite -{2}[Gud]vsubmxK map_col_mx mul_row_col mul0mx addr0. pose T := map_mx intr (dsubmx Gud) *m S. -have{kerGu} defS: map_mx intr (rsubmx G'lr) *m T = S. +have defS: map_mx intr (rsubmx G'lr) *m T = S. have: G'lr *m Gud = 1%:M by rewrite /G'lr /Gud; case: _ / (Dm); apply: mulVmx. rewrite -{1}[G'lr]hsubmxK -[Gud]vsubmxK mulmxA mul_row_col -map_mxM. move/(canRL (addKr _))->; rewrite -mulNmx raddfD /= map_mx1 map_mxM /=. @@ -1084,17 +1093,49 @@ have uS: row_full S. by apply: eq_bigr => i _; rewrite !mxE (tnth_nth 0) !linearZ. have eqST: (S :=: T)%MS by apply/eqmxP; rewrite -{1}defS !submxMl. case Zv: (map_mx denq (vv *m pinvmx T) == const_mx 1). - pose a := map_mx numq (vv *m pinvmx T) *m dsubmx Gud. - left; exists [ffun j => a 0 j]. - transitivity (\sum_j (map_mx intr a *m S) 0 j *: (vbasis <>)`_j). - rewrite {1}(coord_vbasis s_v); apply: eq_bigr => j _; congr (_ *: _). - have ->: map_mx intr a = vv *m pinvmx T *m map_mx intr (dsubmx Gud). - rewrite map_mxM /=; congr (_ *m _); apply/rowP=> i; rewrite 2!mxE numqE. - by have /eqP/rowP/(_ i)/[!mxE]-> := Zv; rewrite mulr1. - by rewrite -(mulmxA _ _ S) mulmxKpV ?mxE // -eqST submx_full. - rewrite (coord_vbasis (s_Zs _)); apply: eq_bigr => j _; congr (_ *: _). - rewrite linear_sum mxE; apply: eq_bigr => i _. - by rewrite -scaler_int linearZ [a]lock !mxE ffunE. + pose b := map_mx numq (vv *m pinvmx T) *m dsubmx Gud. + left; exists [ffun j => b 0 j], [seq [ffun j => (usubmx Gud) i j] | i : 'I_k]. + rewrite size_image card_ord => a; rewrite -[a](addNKr [ffun j => b 0 j]). + move: (_ + a) => h; under eq_bigr => i _ do rewrite !ffunE mulrzDr_tmp. + rewrite big_split /=. + have <-: v = \sum_(i < m) s`_i *~ b 0 i. + transitivity (\sum_j (map_mx intr b *m S) 0 j *: (vbasis <>)`_j). + rewrite {1}(coord_vbasis s_v); apply: eq_bigr => j _; congr (_ *: _). + have ->: map_mx intr b = vv *m pinvmx T *m map_mx intr (dsubmx Gud). + rewrite map_mxM /=; congr (_ *m _); apply/rowP=> i; rewrite 2!mxE numqE. + by have /eqP/rowP/(_ i)/[!mxE]-> := Zv; rewrite mulr1. + by rewrite -(mulmxA _ _ S) mulmxKpV ?mxE // -eqST submx_full. + rewrite (coord_vbasis (s_Zs _)); apply: eq_bigr => j _; congr (_ *: _). + rewrite linear_sum mxE; apply: eq_bigr => i _. + by rewrite -scaler_int linearZ [b]lock !mxE. + split. + rewrite -[LHS]addr0 => /addrI hP; pose c := \row_i h i *m lsubmx G'lr. + exists [seq c 0 i | i : 'I_k]; congr (_ + _). + have/sub_kermxP: map_mx intr (\row_i h i) *m S = 0. + transitivity (\row_j coord (vbasis <>) j (\sum_(i < m) s`_i *~ h i)). + apply/rowP=> j; rewrite !mxE linear_sum; apply: eq_bigr => i _. + by rewrite !mxE -scaler_int linearZ. + by apply/rowP=> j; rewrite !mxE -hP linear0. + case/submx_trans/(_ kerS_sub_Gu)/submxP=> c' /[dup]. + move/(congr1 (mulmx^~ (map_mx intr (lsubmx G'lr)))). + rewrite -mulmxA -!map_mxM [in RHS]mulmx_lsub mul_usub_mx -/c /=. + have ->: Gud *m G'lr = 1%:M + by rewrite /G'lr /Gud; case: _ / (Dm); apply: mulmxV. + rewrite scalar_mx_block -/(ulsubmx _) block_mxKul map_scalar_mx mulmx1. + move=> {c'}<-; rewrite -map_mxM /= => defh; apply/ffunP=> j. + move/rowP/(_ j): defh; rewrite sum_ffunE !mxE; move/intr_inj->. + apply: eq_bigr => i _; rewrite ffunMzE mulrzz mulrC. + rewrite (nth_map i) ?size_enum_ord // nth_ord_enum ffunE. + by rewrite (nth_map i) ?size_enum_ord // nth_ord_enum. + case=> c {h}/addrI->; rewrite -[LHS]addr0; congr (_ + _). + pose h := \row_(j < k) c`_j *m usubmx Gud. + transitivity (\sum_j (map_mx intr h *m S) 0 j *: (vbasis <>)`_j). + by rewrite map_mxM -mulmxA kerGu mulmx0 big1 // => j _; rewrite mxE scale0r. + rewrite (coord_vbasis (s_Zs _)); apply: eq_bigr => i _; congr (_ *: _). + rewrite linear_sum mxE; apply: eq_bigr => j _. + rewrite -scaler_int linearZ !mxE sum_ffunE; congr (_%:~R * _). + apply: {i} eq_bigr => i _; rewrite mxE ffunMzE mulrzz mulrC. + by rewrite (nth_map i) ?size_enum_ord // ffunE nth_ord_enum. right=> [[a Dv]]; case/eqP: Zv; apply/rowP. have ->: vv = map_mx intr (\row_i a i) *m S. apply/rowP=> j; rewrite !mxE Dv linear_sum. @@ -1104,3 +1145,11 @@ rewrite -defS -2!mulmxA; have ->: T *m pinvmx T = 1%:M. by apply: (row_free_inj uT); rewrite mul1mx mulmxKpV. by move=> i; rewrite mulmx1 -map_mxM 2!mxE denq_int mxE. Qed. + +Lemma dec_Qint_span (vT : vectType rat) m (s : m.-tuple vT) v : + decidable (inIntSpan s v). +Proof. +have [[b [p aP]]|] := solve_Qint_span s v; last by right. +left; exists b; apply/(aP b); exists [::]; rewrite big1 ?addr0 // => i _. +by rewrite nth_nil mulr0z. +Qed. From 7b124c96229fc896daa5403ddcac007b4cdcf77b Mon Sep 17 00:00:00 2001 From: Quentin Vermande Date: Thu, 28 Mar 2024 10:47:05 +0100 Subject: [PATCH 2/4] change matrices' size, edit spacing, reorganise proof flow --- mathcomp/algebra/intdiv.v | 162 ++++++++++++++++++-------------------- 1 file changed, 77 insertions(+), 85 deletions(-) diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v index c734cb88a0..771f0c4242 100644 --- a/mathcomp/algebra/intdiv.v +++ b/mathcomp/algebra/intdiv.v @@ -1043,107 +1043,99 @@ have s_Zs a: \sum_(i < m) s`_i *~ a i \in <>%VS. by rewrite memv_suml // => i _; rewrite -scaler_int memvZ. case s_v: (v \in <>%VS); last by right=> [[a Dv]]; rewrite Dv s_Zs in s_v. pose S := \matrix_(i < m, j < _) coord (vbasis <>) j s`_i. -pose r := \rank S; pose k := (m - r)%N; pose Em := erefl m; pose Ek := erefl k. -have Dm: (m = k + r)%N by rewrite subnK ?rank_leq_row. +remember (\rank S) as r eqn:rE; remember (m - r)%N as k eqn:kE. +have Dm: (m = k + r)%N by rewrite kE rE subnK ?rank_leq_row. +subst m; pose m := (k + r)%N. have [K kerK]: {K : 'M_(k, m) | map_mx intr K == kermx S}%MS. + move: (mxrank_ker S); rewrite -rE -kE => krk. pose B := row_base (kermx S); pose d := \prod_ij denq (B ij.1 ij.2). - exists (castmx (mxrank_ker S, Em) (map_mx numq (intr d *: B))). - rewrite /k; case: _ / (mxrank_ker S); set B1 := map_mx _ _. - have ->: B1 = (intr d *: B). - apply/matrixP=> i j; rewrite 3!mxE mulrC [d](bigD1 (i, j)) // rmorphM mulrA. + exists (castmx (krk, erefl m) (map_mx numq (intr d *: B))). + rewrite map_castmx !eqmx_cast -map_mx_comp map_mx_id_in => [|i j]; last first. + rewrite mxE mulrC [d](bigD1 (i, j)) //= rmorphM mulrA. by rewrite -numqE -rmorphM numq_int. suffices nz_d: d%:Q != 0 by rewrite !eqmx_scale // !eq_row_base andbb. by rewrite intr_eq0; apply/prodf_neq0 => i _; apply: denq_neq0. have [L _ [G uG [D _ defK]]] := int_Smith_normal_form K. -pose Gud := castmx (Dm, Em) G; pose G'lr := castmx (Em, Dm) (invmx G). -have{K L D defK kerK} [kerGu kerS_sub_Gu]: map_mx intr (usubmx Gud) *m S = 0 /\ - (kermx S <= map_mx intr (usubmx Gud))%MS. - pose Kl : 'M[rat]_k:= map_mx intr (lsubmx (castmx (Ek, Dm) (K *m invmx G))). - have{} defK: map_mx intr K = row_mx Kl 0 *m map_mx intr Gud. - rewrite -[K](mulmxKV uG) -{2}[G](castmxK Dm Em) -/Gud. - rewrite -[K *m _](castmxK Ek Dm) map_mxM map_castmx. - rewrite -(hsubmxK (castmx _ _)) map_row_mx -/Kl map_castmx /Em. - set Kr := map_mx _ _; case: _ / (esym Dm) (map_mx _ _) => /= GudQ. - congr (row_mx _ _ *m _); apply/matrixP=> i j; rewrite !mxE defK mulmxK //=. - rewrite castmxE mxE big1 //= => j1 _; rewrite mxE /= eqn_leq andbC. +have {K L D defK kerK} [kerGu kerS_sub_Gu]: map_mx intr (usubmx G) *m S = 0 /\ + (kermx S <= map_mx intr (usubmx G))%MS. + pose Kl : 'M[rat]_k := map_mx intr (lsubmx (K *m invmx G)). + have {}defK: map_mx intr K = Kl *m map_mx intr (usubmx G). + rewrite /Kl -map_mxM; congr map_mx. + rewrite -[LHS](mulmxKV uG) -{2}[G]vsubmxK -{1}[K *m _]hsubmxK. + rewrite mul_row_col -[RHS]addr0; congr (_ + _). + rewrite defK mulmxK //= -[RHS](mul0mx _ (dsubmx G)); congr (_ *m _). + apply/matrixP => i j; rewrite !mxE big1 //= => j1 _. + rewrite mxE /= eqn_leq andbC. by rewrite leqNgt (leq_trans (valP j1)) ?mulr0 ?leq_addr. - split; last first. - rewrite -(eqmxP kerK); apply/submxP; exists Kl. - by rewrite defK -{1}[Gud]vsubmxK map_col_mx mul_row_col mul0mx addr0. - have /row_full_inj: row_full Kl; last apply. - rewrite /row_full eqn_leq rank_leq_row /= -{1}[k](mxrank_ker S). - rewrite -(eqmxP kerK) defK map_castmx mxrankMfree; last first. - case: _ / (Dm); apply/row_freeP; exists (map_mx intr (invmx G)). - by rewrite -map_mxM mulmxV ?map_mx1. - by rewrite -mxrank_tr tr_row_mx trmx0 -addsmxE addsmx0 mxrank_tr. - rewrite mulmx0 mulmxA (sub_kermxP _) // -(eqmxP kerK) defK. - by rewrite -{2}[Gud]vsubmxK map_col_mx mul_row_col mul0mx addr0. -pose T := map_mx intr (dsubmx Gud) *m S. -have defS: map_mx intr (rsubmx G'lr) *m T = S. - have: G'lr *m Gud = 1%:M by rewrite /G'lr /Gud; case: _ / (Dm); apply: mulVmx. - rewrite -{1}[G'lr]hsubmxK -[Gud]vsubmxK mulmxA mul_row_col -map_mxM. - move/(canRL (addKr _))->; rewrite -mulNmx raddfD /= map_mx1 map_mxM /=. + split; last by rewrite -(eqmxP kerK); apply/submxP; exists Kl. + suff /row_full_inj: row_full Kl. + by apply; rewrite mulmx0 mulmxA (sub_kermxP _) // -(eqmxP kerK) defK. + rewrite /row_full eqn_leq rank_leq_row /= {1}kE {2}rE -(mxrank_ker S). + by rewrite -(eqmxP kerK) defK mxrankM_maxl. +pose T := map_mx intr (dsubmx G) *m S. +have defS: map_mx intr (rsubmx (invmx G)) *m T = S. + rewrite mulmxA -map_mxM /=; move: (mulVmx uG). + rewrite -{2}[G]vsubmxK -{1}[invmx G]hsubmxK mul_row_col. + move/(canRL (addKr _)) ->; rewrite -mulNmx raddfD /= map_mx1 map_mxM /=. by rewrite mulmxDl -mulmxA kerGu mulmx0 add0r mul1mx. pose vv := \row_j coord (vbasis <>) j v. have uS: row_full S. apply/row_fullP; exists (\matrix_(i, j) coord s j (vbasis <>)`_i). - apply/matrixP=> j1 j2; rewrite !mxE. + apply/matrixP => j1 j2; rewrite !mxE. rewrite -(coord_free _ _ (basis_free (vbasisP _))). rewrite -!tnth_nth (coord_span (vbasis_mem (mem_tnth j1 _))) linear_sum. by apply: eq_bigr => i _; rewrite !mxE (tnth_nth 0) !linearZ. have eqST: (S :=: T)%MS by apply/eqmxP; rewrite -{1}defS !submxMl. -case Zv: (map_mx denq (vv *m pinvmx T) == const_mx 1). - pose b := map_mx numq (vv *m pinvmx T) *m dsubmx Gud. - left; exists [ffun j => b 0 j], [seq [ffun j => (usubmx Gud) i j] | i : 'I_k]. - rewrite size_image card_ord => a; rewrite -[a](addNKr [ffun j => b 0 j]). - move: (_ + a) => h; under eq_bigr => i _ do rewrite !ffunE mulrzDr_tmp. - rewrite big_split /=. - have <-: v = \sum_(i < m) s`_i *~ b 0 i. - transitivity (\sum_j (map_mx intr b *m S) 0 j *: (vbasis <>)`_j). - rewrite {1}(coord_vbasis s_v); apply: eq_bigr => j _; congr (_ *: _). - have ->: map_mx intr b = vv *m pinvmx T *m map_mx intr (dsubmx Gud). - rewrite map_mxM /=; congr (_ *m _); apply/rowP=> i; rewrite 2!mxE numqE. - by have /eqP/rowP/(_ i)/[!mxE]-> := Zv; rewrite mulr1. +case Zv: (map_mx denq (vv *m pinvmx T) == const_mx 1); last first. + right=> [[a Dv]]; case/eqP: Zv; apply/rowP. + have ->: vv = map_mx intr (\row_i a i) *m S. + apply/rowP => j; rewrite !mxE Dv linear_sum. + by apply: eq_bigr => i _; rewrite -scaler_int linearZ !mxE. + rewrite -defS -2!mulmxA; have ->: T *m pinvmx T = 1%:M. + have uT: row_free T by rewrite /row_free -eqST -rE. + by apply: (row_free_inj uT); rewrite mul1mx mulmxKpV. + by move=> i; rewrite mulmx1 -map_mxM 2!mxE denq_int mxE. +pose b := map_mx numq (vv *m pinvmx T) *m dsubmx G. +left; exists [ffun j => b 0 j], [seq [ffun j => (usubmx G) i j] | i : 'I_k]. +rewrite size_image card_ord => a; rewrite -[a](addNKr [ffun j => b 0 j]). +move: (_ + a) => h; under eq_bigr => i _ do rewrite !ffunE mulrzDr_tmp. +rewrite big_split /=. +have <-: v = \sum_(i < m) s`_i *~ b 0 i. + transitivity (\sum_j (map_mx intr b *m S) 0 j *: (vbasis <>)`_j). + rewrite {1}(coord_vbasis s_v); apply: eq_bigr => j _; congr (_ *: _). + suff ->: map_mx intr b = vv *m pinvmx T *m map_mx intr (dsubmx G). by rewrite -(mulmxA _ _ S) mulmxKpV ?mxE // -eqST submx_full. - rewrite (coord_vbasis (s_Zs _)); apply: eq_bigr => j _; congr (_ *: _). - rewrite linear_sum mxE; apply: eq_bigr => i _. - by rewrite -scaler_int linearZ [b]lock !mxE. - split. - rewrite -[LHS]addr0 => /addrI hP; pose c := \row_i h i *m lsubmx G'lr. - exists [seq c 0 i | i : 'I_k]; congr (_ + _). - have/sub_kermxP: map_mx intr (\row_i h i) *m S = 0. - transitivity (\row_j coord (vbasis <>) j (\sum_(i < m) s`_i *~ h i)). - apply/rowP=> j; rewrite !mxE linear_sum; apply: eq_bigr => i _. - by rewrite !mxE -scaler_int linearZ. - by apply/rowP=> j; rewrite !mxE -hP linear0. - case/submx_trans/(_ kerS_sub_Gu)/submxP=> c' /[dup]. - move/(congr1 (mulmx^~ (map_mx intr (lsubmx G'lr)))). - rewrite -mulmxA -!map_mxM [in RHS]mulmx_lsub mul_usub_mx -/c /=. - have ->: Gud *m G'lr = 1%:M - by rewrite /G'lr /Gud; case: _ / (Dm); apply: mulmxV. - rewrite scalar_mx_block -/(ulsubmx _) block_mxKul map_scalar_mx mulmx1. - move=> {c'}<-; rewrite -map_mxM /= => defh; apply/ffunP=> j. - move/rowP/(_ j): defh; rewrite sum_ffunE !mxE; move/intr_inj->. - apply: eq_bigr => i _; rewrite ffunMzE mulrzz mulrC. - rewrite (nth_map i) ?size_enum_ord // nth_ord_enum ffunE. - by rewrite (nth_map i) ?size_enum_ord // nth_ord_enum. - case=> c {h}/addrI->; rewrite -[LHS]addr0; congr (_ + _). - pose h := \row_(j < k) c`_j *m usubmx Gud. - transitivity (\sum_j (map_mx intr h *m S) 0 j *: (vbasis <>)`_j). - by rewrite map_mxM -mulmxA kerGu mulmx0 big1 // => j _; rewrite mxE scale0r. - rewrite (coord_vbasis (s_Zs _)); apply: eq_bigr => i _; congr (_ *: _). - rewrite linear_sum mxE; apply: eq_bigr => j _. - rewrite -scaler_int linearZ !mxE sum_ffunE; congr (_%:~R * _). - apply: {i} eq_bigr => i _; rewrite mxE ffunMzE mulrzz mulrC. - by rewrite (nth_map i) ?size_enum_ord // ffunE nth_ord_enum. -right=> [[a Dv]]; case/eqP: Zv; apply/rowP. -have ->: vv = map_mx intr (\row_i a i) *m S. - apply/rowP=> j; rewrite !mxE Dv linear_sum. - by apply: eq_bigr => i _; rewrite -scaler_int linearZ !mxE. -rewrite -defS -2!mulmxA; have ->: T *m pinvmx T = 1%:M. - have uT: row_free T by rewrite /row_free -eqST. - by apply: (row_free_inj uT); rewrite mul1mx mulmxKpV. -by move=> i; rewrite mulmx1 -map_mxM 2!mxE denq_int mxE. + rewrite map_mxM /=; congr (_ *m _); apply/rowP => i; rewrite 2!mxE numqE. + by have /eqP/rowP/(_ i)/[!mxE] -> := Zv; rewrite mulr1. + rewrite (coord_vbasis (s_Zs _)); apply: eq_bigr => j _; congr (_ *: _). + rewrite linear_sum mxE; apply: eq_bigr => i _. + by rewrite -scaler_int linearZ [b]lock !mxE. +split. + rewrite -[LHS]addr0 => /addrI hP; pose c := \row_i h i *m lsubmx (invmx G). + exists [seq c 0 i | i : 'I_k]; congr (_ + _). + have/sub_kermxP: map_mx intr (\row_i h i) *m S = 0. + transitivity (\row_j coord (vbasis <>) j (\sum_(i < m) s`_i *~ h i)). + apply/rowP => j; rewrite !mxE linear_sum; apply: eq_bigr => i _. + by rewrite !mxE -scaler_int linearZ. + by apply/rowP => j; rewrite !mxE -hP linear0. + case/submx_trans/(_ kerS_sub_Gu)/submxP => c' /[dup]. + move/(congr1 (mulmx^~ (map_mx intr (lsubmx (invmx G))))). + rewrite -mulmxA -!map_mxM [in RHS]mulmx_lsub mul_usub_mx -/c mulmxV //=. + rewrite scalar_mx_block -/(ulsubmx _) block_mxKul map_scalar_mx mulmx1. + move=> <- {c'}; rewrite -map_mxM /= => defh; apply/ffunP => j. + move/rowP/(_ j): defh; rewrite sum_ffunE !mxE => /intr_inj ->. + apply: eq_bigr => i _; rewrite ffunMzE mulrzz mulrC. + rewrite (nth_map i) ?size_enum_ord // nth_ord_enum ffunE. + by rewrite (nth_map i) ?size_enum_ord // nth_ord_enum. +case=> c /addrI -> {h}; rewrite -[LHS]addr0; congr (_ + _). +pose h := \row_(j < k) c`_j *m usubmx G. +transitivity (\sum_j (map_mx intr h *m S) 0 j *: (vbasis <>)`_j). + by rewrite map_mxM -mulmxA kerGu mulmx0 big1 // => j _; rewrite mxE scale0r. +rewrite (coord_vbasis (s_Zs _)); apply: eq_bigr => i _; congr (_ *: _). +rewrite linear_sum mxE; apply: eq_bigr => j _. +rewrite -scaler_int linearZ !mxE sum_ffunE; congr (_%:~R * _). +apply: {i} eq_bigr => i _; rewrite mxE ffunMzE mulrzz mulrC. +by rewrite (nth_map i) ?size_enum_ord // ffunE nth_ord_enum. Qed. Lemma dec_Qint_span (vT : vectType rat) m (s : m.-tuple vT) v : From 5a64ea4f5cd52d1818c5782d6c4bb188866c3410 Mon Sep 17 00:00:00 2001 From: Yves Bertot Date: Fri, 29 Mar 2024 14:50:07 +0100 Subject: [PATCH 3/4] removes a usage of the subst tactic, relying on idiomatic ssreflect --- mathcomp/algebra/intdiv.v | 25 +++++++++++++------------ 1 file changed, 13 insertions(+), 12 deletions(-) diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v index 771f0c4242..627caba251 100644 --- a/mathcomp/algebra/intdiv.v +++ b/mathcomp/algebra/intdiv.v @@ -1042,12 +1042,13 @@ have s_s (i : 'I_m): s`_i \in <>%VS by rewrite memv_span ?memt_nth. have s_Zs a: \sum_(i < m) s`_i *~ a i \in <>%VS. by rewrite memv_suml // => i _; rewrite -scaler_int memvZ. case s_v: (v \in <>%VS); last by right=> [[a Dv]]; rewrite Dv s_Zs in s_v. -pose S := \matrix_(i < m, j < _) coord (vbasis <>) j s`_i. -remember (\rank S) as r eqn:rE; remember (m - r)%N as k eqn:kE. -have Dm: (m = k + r)%N by rewrite kE rE subnK ?rank_leq_row. -subst m; pose m := (k + r)%N. +move SE : (\matrix_(i < m, j < _) coord (vbasis <>) j s`_i) => S. +move rE : (\rank S) => r; move kE : (m - r)%N => k. +have Dm: (m = k + r)%N by rewrite -kE -rE subnK ?rank_leq_row. +move: s s_s s_Zs s_v S SE rE kE; rewrite Dm=> s s_s s_Zs s_v S SE rE kE. +move=> {Dm m}; pose m := (k + r)%N. have [K kerK]: {K : 'M_(k, m) | map_mx intr K == kermx S}%MS. - move: (mxrank_ker S); rewrite -rE -kE => krk. + move: (mxrank_ker S); rewrite rE kE => krk. pose B := row_base (kermx S); pose d := \prod_ij denq (B ij.1 ij.2). exists (castmx (krk, erefl m) (map_mx numq (intr d *: B))). rewrite map_castmx !eqmx_cast -map_mx_comp map_mx_id_in => [|i j]; last first. @@ -1070,7 +1071,7 @@ have {K L D defK kerK} [kerGu kerS_sub_Gu]: map_mx intr (usubmx G) *m S = 0 /\ split; last by rewrite -(eqmxP kerK); apply/submxP; exists Kl. suff /row_full_inj: row_full Kl. by apply; rewrite mulmx0 mulmxA (sub_kermxP _) // -(eqmxP kerK) defK. - rewrite /row_full eqn_leq rank_leq_row /= {1}kE {2}rE -(mxrank_ker S). + rewrite /row_full eqn_leq rank_leq_row /= -{1}kE -{2}rE -(mxrank_ker S). by rewrite -(eqmxP kerK) defK mxrankM_maxl. pose T := map_mx intr (dsubmx G) *m S. have defS: map_mx intr (rsubmx (invmx G)) *m T = S. @@ -1084,15 +1085,15 @@ have uS: row_full S. apply/matrixP => j1 j2; rewrite !mxE. rewrite -(coord_free _ _ (basis_free (vbasisP _))). rewrite -!tnth_nth (coord_span (vbasis_mem (mem_tnth j1 _))) linear_sum. - by apply: eq_bigr => i _; rewrite !mxE (tnth_nth 0) !linearZ. + by apply: eq_bigr=> /= i _; rewrite -SE !mxE (tnth_nth 0) !linearZ. have eqST: (S :=: T)%MS by apply/eqmxP; rewrite -{1}defS !submxMl. case Zv: (map_mx denq (vv *m pinvmx T) == const_mx 1); last first. right=> [[a Dv]]; case/eqP: Zv; apply/rowP. have ->: vv = map_mx intr (\row_i a i) *m S. apply/rowP => j; rewrite !mxE Dv linear_sum. - by apply: eq_bigr => i _; rewrite -scaler_int linearZ !mxE. + by apply: eq_bigr => i _; rewrite -SE -scaler_int linearZ !mxE. rewrite -defS -2!mulmxA; have ->: T *m pinvmx T = 1%:M. - have uT: row_free T by rewrite /row_free -eqST -rE. + have uT: row_free T by rewrite /row_free -eqST rE. by apply: (row_free_inj uT); rewrite mul1mx mulmxKpV. by move=> i; rewrite mulmx1 -map_mxM 2!mxE denq_int mxE. pose b := map_mx numq (vv *m pinvmx T) *m dsubmx G. @@ -1109,14 +1110,14 @@ have <-: v = \sum_(i < m) s`_i *~ b 0 i. by have /eqP/rowP/(_ i)/[!mxE] -> := Zv; rewrite mulr1. rewrite (coord_vbasis (s_Zs _)); apply: eq_bigr => j _; congr (_ *: _). rewrite linear_sum mxE; apply: eq_bigr => i _. - by rewrite -scaler_int linearZ [b]lock !mxE. + by rewrite -SE -scaler_int linearZ [b]lock !mxE. split. rewrite -[LHS]addr0 => /addrI hP; pose c := \row_i h i *m lsubmx (invmx G). exists [seq c 0 i | i : 'I_k]; congr (_ + _). have/sub_kermxP: map_mx intr (\row_i h i) *m S = 0. transitivity (\row_j coord (vbasis <>) j (\sum_(i < m) s`_i *~ h i)). apply/rowP => j; rewrite !mxE linear_sum; apply: eq_bigr => i _. - by rewrite !mxE -scaler_int linearZ. + by rewrite -SE !mxE -scaler_int linearZ. by apply/rowP => j; rewrite !mxE -hP linear0. case/submx_trans/(_ kerS_sub_Gu)/submxP => c' /[dup]. move/(congr1 (mulmx^~ (map_mx intr (lsubmx (invmx G))))). @@ -1132,7 +1133,7 @@ pose h := \row_(j < k) c`_j *m usubmx G. transitivity (\sum_j (map_mx intr h *m S) 0 j *: (vbasis <>)`_j). by rewrite map_mxM -mulmxA kerGu mulmx0 big1 // => j _; rewrite mxE scale0r. rewrite (coord_vbasis (s_Zs _)); apply: eq_bigr => i _; congr (_ *: _). -rewrite linear_sum mxE; apply: eq_bigr => j _. +rewrite linear_sum -SE mxE; apply: eq_bigr => j _. rewrite -scaler_int linearZ !mxE sum_ffunE; congr (_%:~R * _). apply: {i} eq_bigr => i _; rewrite mxE ffunMzE mulrzz mulrC. by rewrite (nth_map i) ?size_enum_ord // ffunE nth_ord_enum. From a9b068b86a3d16d16325828a8f4b11cf0ea401bd Mon Sep 17 00:00:00 2001 From: Yves Bertot Date: Fri, 29 Mar 2024 15:07:25 +0100 Subject: [PATCH 4/4] space twiddling --- mathcomp/algebra/intdiv.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v index 627caba251..b4be88a6ad 100644 --- a/mathcomp/algebra/intdiv.v +++ b/mathcomp/algebra/intdiv.v @@ -1085,7 +1085,7 @@ have uS: row_full S. apply/matrixP => j1 j2; rewrite !mxE. rewrite -(coord_free _ _ (basis_free (vbasisP _))). rewrite -!tnth_nth (coord_span (vbasis_mem (mem_tnth j1 _))) linear_sum. - by apply: eq_bigr=> /= i _; rewrite -SE !mxE (tnth_nth 0) !linearZ. + by apply: eq_bigr => /= i _; rewrite -SE !mxE (tnth_nth 0) !linearZ. have eqST: (S :=: T)%MS by apply/eqmxP; rewrite -{1}defS !submxMl. case Zv: (map_mx denq (vv *m pinvmx T) == const_mx 1); last first. right=> [[a Dv]]; case/eqP: Zv; apply/rowP.