proposition: Lemma improve_pivot_recP : forall m n (P : 'M_(1 + m)) (M : 'M_(1 + m,1 + n)) Q (k : Acc (@sdvdr [the dvdRingType of R]) (M 0 0)), M 0 0 != 0 -> P \in unitmx -> Q \in unitmx -> improve_pivot_rec_spec P M Q (improve_pivot_rec P Q k).
proof: Proof. move=> m n P M Q k. rewrite -/(ecast a (Acc (fun x y : R => x %<| y) a) (erefl (M 0 0)) k). move: (erefl _) => eq_M00; move: eq_M00 k. move: {1 3 5}(fun_of_matrix M 0 0) => a eq_a k. elim/Acc_rect_dep: k M P Q eq_a => a' Acc_a' IHa' M P Q eq_a' nzM00 unitL unitR /=. move: (eq_a') Acc_a' IHa'. rewrite eq_a' => {}eq_a' Acc_a' IHa'; rewrite {eq_a'}[eq_a']eq_axiomK /=. case: find1P=> [i Hi|Hi]. set P0 := Bezout_step _ _ P _; set M0 := Bezout_step _ _ M _. have /(_ erefl) [|||P' A' Q' HA' ? ? Hdiv HP' HQ'] // := IHa' (M0 0 0) (sdvd_Bezout_step Hi) M0 P0 Q. + by rewrite -eqdr0 (congr_eqd (Bezout_step_mx00 M) (eqdd _)) eqdr0 gcdr_eq0 (negbTE nzM00). + by rewrite /P0 Bezout_stepE !unitmxEE. + constructor=> //. rewrite -HA' /P0 /M0 !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 M' := map_mx _ _. have Hblock : (matrix.block_mx 1 0 M' 1%:M) *m M = matrix.block_mx (M 0 0)%:M (matrix.ursubmx M) (matrix.const_mx (M 0 0)) (M' *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 M' 1%:M \in unitmx by rewrite unitmxE (det_lblock 1 M') !det1 mul1r unitr1. have HblockP : (matrix.block_mx 1 0 M' 1%:M) *m P = matrix.col_mx (matrix.usubmx P) (M' *m matrix.usubmx P + matrix.dsubmx P) by rewrite -{1}[P]vsubmxK mul_block_col !mul1mx mul0mx addr0. case: find2P=> [[i j]|Hij] /=. set B := matrix.block_mx _ _ _ _; set C := matrix.xrow _ _ B => Hij. have HMA: M 0 0 = C^T 0 0. rewrite /C /B -{4}(lshift0 n 0) !mxE tpermL. by case: splitP=> [i' _|i' Hi']; rewrite ?ord1 row_mxEl mxE ?eqxx. rewrite HMA in nzM00. set P0 := xrow _ _ _; set Q0 := (Bezout_step _ _ Q^T _)^T. set M0 := (Bezout_step _ _ C^T _)^T; set dvd_prf := sdvd_Bezout_step2 _. have /(_ erefl) [|||P' A' Q' HA' ? ? Hdiv HP' HQ'] // := IHa' (M0 0 0) dvd_prf M0 P0 Q0. + rewrite /M0 -[C]trmxK [C^T^T^T]trmxK ![C^T^T _ _]mxE. by rewrite mxE -eqdr0 (congr_eqd (Bezout_step_mx00 _) (eqdd _)) eqdr0 gcdr_eq0 (negbTE nzM00). + by rewrite /P0 xrowE -HblockP !unitmxEE unit_block. + by rewrite /Q0 !Bezout_stepE !unitmxEE. + constructor=> //. + rewrite -HA' /P0 /M0 /Q0 -[C]trmxK [C^T^T^T]trmxK ![C^T^T _ _]mxE. rewrite ![(C^T) 0 _]mxE /C /B -Hblock -HblockP !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 /M0 -[C]trmxK [C^T^T^T]trmxK ![C^T^T _ _]mxE in Hdiv. rewrite (dvdr_trans Hdiv) // mxE (eqd_dvd (Bezout_step_mx00 _) (eqdd _)) HMA. exact: dvdr_gcdl. constructor=> //; first by rewrite -HblockP -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. 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 -HblockP unitmx_mul unitmxE (det_lblock 1 M') !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