proposition: Lemma dec_Qint_span (vT : vectType rat) m (s : m.-tuple vT) v : decidable (inIntSpan s v).
proof: Proof. have s_s (i : 'I_m): s`_i \in <<s>>%VS by rewrite memv_span ?memt_nth. have s_Zs a: \sum_(i < m) s`_i *~ a i \in <<s>>%VS. by rewrite memv_suml // => i _; rewrite -scaler_int memvZ. case s_v: (v \in <<s>>%VS); last by right=> [[a Dv]]; rewrite Dv s_Zs in s_v. pose S := \matrix_(i < m, j < _) coord (vbasis <<s>>) 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. have [K kerK]: {K : 'M_(k, m) | map_mx intr K == kermx S}%MS. 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. 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: map_mx intr (usubmx Gud) *m S = 0. 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. by rewrite leqNgt (leq_trans (valP j1)) ?mulr0 ?leq_addr. 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{kerGu} 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 /=. by rewrite mulmxDl -mulmxA kerGu mulmx0 add0r mul1mx. pose vv := \row_j coord (vbasis <<s>>) j v. have uS: row_full S. apply/row_fullP; exists (\matrix_(i, j) coord s j (vbasis <<s>>)`_i). 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 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 <<s>>)`_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. 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. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime order) mathcomp(ssralg poly ssrnum ssrint archimedean rat matrix) mathcomp(polydiv perm zmodp mxalgebra vector)