proposition: Lemma SmithP : forall (m n : nat) (M : 'M_(m,n)), smith_spec M (Smith M).
proof: Proof. elim=> [n M|m IHn]. constructor=> //; try by exact: unitmx1. rewrite [M]flatmx0 mulmx1 mul1mx; apply/matrixP => i j. by rewrite !mxE nth_nil mul0rn. case=> [M|n M /=]. constructor=> //; try by exact: unitmx1. rewrite [M]thinmx0 mulmx1 mul1mx; apply/matrixP => i j. by rewrite !mxE nth_nil mul0rn. case: find_pivotP =>[[i j] HMij | H]. case: improve_pivotP; rewrite ?mxE ?tpermR ?leqnn //. rewrite -[m.+1]/(1 + m)%N -[n.+1]/(1 + n)%N => L B Q0 HB Hdiv HAi0 HA00. set A' := map_mx _ _; set v' := map_mx _ _. case: IHn=> L' d Q' Hd Hsorted HL' HQ' HL HQ; constructor. * rewrite xcolE xrowE -!mulmxA (mulmxA M) -xcolE (mulmxA (tperm_mx _ _)). rewrite -xrowE (mulmxA L) (mulmxA _ Q0) HB mulmx_block !mulmxA mulmx_block. rewrite -{1}(submxK B) !mulmx_block. do 2! rewrite !mul0mx !mulmx0 !mulmx1 !mul1mx !addr0 ?add0r. have Hu: matrix.const_mx 1 *m matrix.ulsubmx B = matrix.dlsubmx B. rewrite [matrix.ulsubmx B]mx11_scalar mul_mx_scalar; apply/matrixP=> k l. by rewrite ord1 !mxE mulr1 !lshift0 !HAi0. have Hv': (matrix.ulsubmx B *m v') = matrix.ursubmx B. apply/matrixP=> k l. rewrite (ord1 k) !mxE big_ord_recl big_ord0 !mxE !lshift0 addr0. case: odivrP=>[x ->|H]; first by rewrite mulrC. by case/dvdrP:(Hdiv 0 (rshift 1 l))=> q /eqP; rewrite (negbTE (H q)). rewrite diag_mx_seq_cons; congr matrix.block_mx. + by apply/matrixP=> k l; rewrite !ord1 !mxE !lshift0 eqxx. + by rewrite mulNmx mulmxN mulmxA Hv' addNr. + by rewrite mulmxN mulNmx -mulmxA Hu addNr. + rewrite mulmxN !mulNmx -mulmxA Hu addNr mul0mx add0r addrC -mulmxA -mulmxBr. transitivity (B 0 0 *: (L' *m A' *m Q')). rewrite -[_ *m A' *m _]mulmxA scalemxAr scalemxAl. have Hdiv' : forall i j, B 0 0 %| (matrix.drsubmx B - matrix.const_mx 1 *m matrix.ursubmx B) i j. by move=> k l; rewrite !mxE big_ord1 !mxE mul1r dvdr_sub ?Hdiv. have -> : B 0 0 *: A' = matrix.drsubmx B - matrix.const_mx 1 *m matrix.ursubmx B. apply/matrixP => k l; rewrite 2!mxE. case: odivrP => [x ->|H]; first by rewrite mulrC. by case/dvdrP:(Hdiv' k l)=> q /eqP; rewrite (negbTE (H q)). by rewrite mulmxA. rewrite Hd; apply/matrixP=> k l; rewrite !mxE. case: eqP => /=; last by rewrite mulr0. case: (ltnP k (size d)) => /= Hk. by rewrite (nth_map 0 _ _ Hk) mulrC. by rewrite !nth_default ?size_map ?Hk // mulr0. * have {}HA00: B 0 0 != 0. by apply/eqP=> H; move:HA00; rewrite H dvd0r (negbTE HMij). rewrite /= path_min_sorted; last by apply/allP => a /mapP [b _ ->]; exact:dvdr_mull. case: d Hsorted {Hd} => //= a d; elim: d a=> //= a1 d IHd a0 /andP[a01 /IHd]. by rewrite dvdr_mul2r ?a01. * rewrite xcolE !unitmx_mul unitmx_perm HL !unitmxE. by rewrite !det_lblock !det1 mul1r mulr1 unitr1 -unitmxE !andbT. * rewrite xrowE !unitmx_mul unitmx_perm HQ !unitmxE. by rewrite 2!det_ublock 2!det1 2!mul1r unitr1 -unitmxE. constructor =>[|||]; rewrite ?mxE ?unitmx1 //. rewrite mul1mx mulmx1; apply/matrixP=> i j; rewrite !mxE (eqP (negbFE (H (i,j)))). by case: (i == j :> nat); rewrite ?nth_nseq ?if_same nth_nil. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg ssrint ssrnum fintype choice) mathcomp(matrix mxalgebra bigop zmodp perm) dvdring mxstructure stronglydiscrete coherent edr