proposition: Lemma kap_smithP (M : 'M[R]_2) : smith_spec M (kap_smith M).
proof: Proof. rewrite /kap_smith; set A := hermite _ : 'M_(1+1). set a00 := (_ 0 0); set a01 := (_ 0 1); set a11 := (_ 1 1). case: egcdr3P=> /= d xd yd zd a b c heq; rewrite eqd_sym=> hgcd ha hb hc. have [d0|dn0] := boolP (d == 0). constructor; rewrite ?unitmx1 ?unit_Bezout_mx // mulmx1 -Bezout_stepE. have -> : Bezout_step (M 0 0) (M 1 0) M 0 = A by []. rewrite diag_mx_seq_nil -(@block_mx0 _ 1 _ 1). have -> : A = mx2 a00 a01 0 a11. rewrite -[A]submxK. congr block_mx; apply/rowP=> i; rewrite !mxE ord1 ?lshift0 ?mulr1n ?rshift1 //; have -> // : lift 0 0 = 1 by move=> n; apply/ord_inj. by rewrite hermite10. by rewrite /mx2; f_equal; rewrite ?ha ?hb ?hc ?(eqP d0) ?mulr0 -scalemx1 scale0r. have /kapP : gcdr a (gcdr b c) %= 1. rewrite -(eqd_mul2r _ _ dn0) mul1r (eqd_trans _ hgcd) //. rewrite (eqd_trans (mulr_gcdl _ _ _)) //. by rewrite -ha eqd_gcd ?(eqd_trans (mulr_gcdl _ _ _)) // -hb -hc. move: (kapWP a b c); case: kap => p q H1 H3; move: (H1 H3). case: kapW=> x1 y1 => {H1 H3} H; move: (H). rewrite mulrCA [x1 * a]mulrC mulrDr [y1 * _]mulrCA addrA -mulrDr. set x := a * x1 + y1 * b; rewrite mulrCA [y1 * c]mulrC; set y := c * y1=> Hxy. constructor. * set M1 := mx2 _ _ _ _; set M2 := mx2 _ _ _ _. rewrite -!mulmxA [_ *m (_ *m M2)]mulmxA -Bezout_stepE. have -> : Bezout_step (M 0 0) (M 1 0) M 0 = d *: mx2 a b 0 c. rewrite scale_block_mx -!mul_scalar_mx -!scalar_mxM mulr0 mulrC -ha mulrC. rewrite -hb -mulrC -hc -[Bezout_step _ _ _ _](@submxK _ 1). have h1 : lift 0 0 = 1 by move=> n; apply/ord_inj. f_equal; apply/rowP=> i; rewrite !mxE ord1 ?(lshift0,rshift1,h1) mulr1n //. by rewrite hermite10. rewrite -scalemxAl -!scalemxAr -diag_mx_seq_scale; congr (_ *: _). rewrite /M1 /M2 /mx2 !(@mulmx_block _ 1) -[0%:M]scalemx1 scale0r !mul0mx. rewrite !add0r -?(scalar_mxM,raddfD) /= mulrC [_ * y1]mulrC. rewrite !diag_mx_seq_cons diag_mx_seq_nil. f_equal. - by rewrite mulrC Hxy. - rewrite [a * _ + _]addrC [a * _]mulrDr addrA mulrCA [a * _]mulrCA. rewrite [b * a]mulrC mulNr addNr add0r ![_ * (- p * _)]mulrCA mulNr. by rewrite [c * _]mulrC [q * (_ * _)]mulrCA addrN -[0%:M]scalemx1 scale0r. - by rewrite -/x -/y mulNr mulrC addNr -[0%:M]scalemx1 scale0r. - apply/matrixP=> i j; rewrite !ord1 {i j} [RHS]mxE split1. case: unliftP=> //= _; rewrite [RHS]mxE split1; case: unliftP => //= _. rewrite !mxE !mulr1n !mulrDr !mulNr !mulrN opprK [_ + y * _]addrC addrA. rewrite [p * b]mulrC [a * (b * p)]mulrCA [p * a]mulrC addrN sub0r. rewrite ![_ * (a * _)]mulrCA -!mulNr -mulrDr mulrCA mulrAC -mulrA -mulrDr. by rewrite [x * p]mulrC addrC -mulrA Hxy mulr1. * by apply: sorted_cons => //=; rewrite mulr1 dvdr_mulr. * rewrite !unitmx_mul unit_Bezout_mx !unitmxE detmx2 /x /y mulNr opprK. by rewrite [_ * q]mulrC Hxy unitr1. by rewrite unitmxE detmx2 mulNr mulrN -opprD -mulN1r unitrMl ?unitrN1 // H unitr1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path) mathcomp(ssralg fintype matrix mxalgebra bigop zmodp perm choice) dvdring mxstructure minor stronglydiscrete coherent edr