proposition: Lemma improve_pivot_recP : forall k m n (P : 'M_(1 + m)) (M : 'M_(1 + m,1 + n)) Q, (enorm (M 0%R 0%R) <= k)%N -> M 0 0 != 0 -> P \in unitmx -> Q \in unitmx -> improve_pivot_rec_spec P M Q (improve_pivot_rec k P M Q).
proof: Proof. elim=> [m n L M R0|k IHk m n L M R0 Hk nzM00 unitL unitR /=]. by rewrite leqn0 => /eqP /enorm_eq0 ->; rewrite eqxx. case: find1P=> [i Hi|Hi]. have [||||L' A' R' HA' ? ? Hdiv HL' HR'] // := IHk; do ?constructor => //. + by rewrite -ltnS (leq_trans (ltn_enorm nzM00 (sdvd_Bezout_step Hi)) Hk). + by rewrite -eqdr0 (congr_eqd (Bezout_step_mx00 M) (eqdd _)) eqdr0 gcdr_eq0 (negbTE nzM00). + by rewrite Bezout_stepE !unitmxEE. + rewrite -HA' !Bezout_stepE invrM ?unit_Bezout_mx // !mulmxA. by congr (_ *m _ *m _); rewrite -mulmxA mulVmx ?unit_Bezout_mx // mulmx1. + rewrite (eqd_dvd (eqdd _) (Bezout_step_mx00 _)) in Hdiv. exact: (dvdr_trans Hdiv (dvdr_gcdl _ _)). set P := map_mx _ _. have Hblock : (matrix.block_mx 1 0 P 1%:M) *m M = matrix.block_mx (M 0 0)%:M (matrix.ursubmx M) (matrix.const_mx (M 0 0)) (P *m matrix.ursubmx M + matrix.drsubmx M). rewrite -{1}[M]submxK mulmx_block !mul0mx !mul1mx !addr0 [matrix.ulsubmx M]mx11_scalar 2!mxE !lshift0. congr matrix.block_mx; rewrite mul_mx_scalar. apply/matrixP=> p q; rewrite ord1 !mxE lshift0 mulrBr mulr1 !rshift1. case: odivrP=> [d ->|]; first by rewrite mulrC subrK. by case/dvdrP:(negbFE (Hi p))=> x -> /(_ x); rewrite eqxx. have unit_block : matrix.block_mx 1 0 P 1%:M \in unitmx by rewrite unitmxE (det_lblock 1 P) !det1 mul1r unitr1. have HblockL : (matrix.block_mx 1 0 P 1%:M) *m L = matrix.col_mx (matrix.usubmx L) (P *m matrix.usubmx L + matrix.dsubmx L) by rewrite -{1}[L]vsubmxK mul_block_col !mul1mx mul0mx addr0. case: find2P=> [[i j]|Hij] /=. set B := matrix.block_mx _ _ _ _; set A := matrix.xrow _ _ B => Hij. have HMA: M 0 0 = A^T 0 0. rewrite /A /B -{4}(lshift0 n 0) !mxE tpermL. by case: splitP=> [i' _|i' Hi']; rewrite ?ord1 row_mxEl mxE ?eqxx. rewrite HMA in nzM00 Hk Hij; rewrite -[A]trmxK [A^T^T^T]trmxK ![A^T^T _ _]mxE. case: IHk => [||||L' A' R' HA' ? ? Hdiv HL' HR']; do ?constructor=> //. + rewrite -ltnS mxE (leq_trans _ Hk) ?(ltn_enorm nzM00) ?sdvd_Bezout_step //. by rewrite {2}/A [_ (lift _ _) _]mxE [matrix.xrow _ _ _ _ _]mxE tpermL. + by rewrite mxE -eqdr0 (congr_eqd (Bezout_step_mx00 _) (eqdd _)) eqdr0 gcdr_eq0 (negbTE nzM00). + by rewrite xrowE -HblockL !unitmxEE unit_block. + by rewrite !Bezout_stepE !unitmxEE. + rewrite -HA' ![(A^T) 0 _]mxE /A /B -Hblock -HblockL !xrowE. rewrite !Bezout_stepE !trmx_mul !trmxK !invrM //. - rewrite !mulmxA -[_ / _ *m _]mulmxA mulVmx ?unitmx_perm // mulmx1. rewrite -[_ / _ *m _]mulmxA mulVmx // mulmx1 -[_ *m _^T *m _]mulmxA. by rewrite mulmxV ?unitmx_tr ?unit_Bezout_mx // mulmx1. - by rewrite unitmx_tr unit_Bezout_mx. - by rewrite unitmx_perm. by rewrite !unitmxEE unit_block. rewrite (dvdr_trans Hdiv) // mxE (eqd_dvd (Bezout_step_mx00 _) (eqdd _)) HMA. exact: dvdr_gcdl. constructor=> //; first by rewrite -HblockL -Hblock invrM // mulmxA mulmxKV. + rewrite -[m.+1]/(1 + m)%N -[n.+1]/(1 + n)%N => i j. rewrite -{3}(lshift0 m 0) -{3}(lshift0 n 0) block_mxEul mxE eqxx !mxE. case: splitP=> i' Hi'; rewrite mxE; case: splitP=> j' Hj'; rewrite ?mxE ?ord1 //=. by move: (negbFE (Hij (lshift m 0,j'))); rewrite -rshift1 block_mxEur !mxE. by move: (negbFE (Hij (lift 0 i',j'))); rewrite -!rshift1 block_mxEdr !mxE. + rewrite -[m.+1]/(1 + m)%N => i. rewrite -{5}(lshift0 m 0) -{3 6}(lshift0 n 0) (block_mxEul (M 0 0)%:M _) !mxE eqxx /=. by case: splitP=> i' _; rewrite row_mxEl !mxE // ord1. + rewrite -{3}(lshift0 m 0) -{3}(lshift0 n 0). by rewrite (block_mxEul (M 0 0)%:M (matrix.ursubmx M)) mxE dvdrr. by rewrite -HblockL unitmx_mul unitmxE (det_lblock 1 P) !det1 mulr1 unitr1. 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