This file is part of CoqEAL, the Coq Effective Algebra Library.
(c) Copyright INRIA and University of Gothenburg.
Require Import ssreflect ssrfun ssrbool eqtype ssrnat div seq.
Require Import ssralg fintype perm.
Require Import matrix bigop zmodp mxalgebra.
Require Import seqmatrix cssralg ssrcomplements.
Import GRing.Theory.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensives.
Section FieldRank.
Variable K :
fieldType.
Local Open Scope ring_scope.
Fixpoint elim_step {
p n:
nat} {
struct p} : '
M[
K]
_(
p, 1 +
n) -> ('
M[
K]
_(
p,
n) *
bool) :=
match p return '
M[
K]
_(
p, 1 +
n) -> ('
M[
K]
_(
p,
n) *
bool)
with
|
p'.+1 =>
fun (
l : '
M_(1 +
p', 1 +
n)) =>
let a :=
l 0 0
in
if a == 0
then
let (
R,
b) :=
elim_step (
dsubmx l)
in
(
col_mx (
ursubmx l)
R,
b)
else
let v :=
a^-1 *:
dlsubmx l in
let R :=
drsubmx l -
v *
m ursubmx l in
let v0 : '
rV[
K]
_n := 0
in
(
castmx (
addn1 _,
erefl _) (
col_mx R v0),
true)
|
_ =>
fun l => (0,
false)
end.
Lemma directmx0M m n (
M : '
M[
K]
_(1 +
m,
n)) (
v : '
rV_(1 +
n)) :
v 0 0 != 0 ->
mxdirect (
row_mx 0
M +
v).
Proof.
move=> Hv0; apply/mxdirect_addsP; apply/eqP/rowV0P=> v0; rewrite sub_capmx.
case/andP=> Hrow /sub_rVP [k Hv0k]; move:Hrow; rewrite Hv0k -[M]vsubmxK.
rewrite -col_mx0 -block_mxEh block_mxEv -!addsmxE.
case/sub_addsmxP=> [[a b] /=] /matrixP/(_ 0 0); rewrite !mxE !big1=> [|i _|i _].
+ move/eqP; rewrite addr0 (mulf_eq0 k (v 0 0)) (negbTE Hv0) orbF.
by move/eqP=> ->; rewrite scale0r.
+ by rewrite mxE; case:splitP=> // j; rewrite ord1 mxE mulr0.
by rewrite mxE; case:splitP=> // j; rewrite ord1 mxE mulr0.
Qed.
Lemma adds_rowmx0M m1 m2 m3 n (
v : '
rV[
K]
_(1 +
n)) (
N : '
M_(
m1,
_))
(
P : '
M_(
m2,
_)) (
Q : '
M_(
m3,
_)) :
v 0 0 = 0 -> (
N :=:
row_mx 0
P +
Q)%
MS ->
(
col_mx v N :=:
row_mx 0 (
col_mx (
rsubmx v)
P) +
Q)%
MS.
Proof.
move=> HM00 H; rewrite -col_mx0 -block_mxEh block_mxEv.
apply/eqmxP; rewrite -!addsmxE; apply/eqmxP.
have ->: row_mx 0 (rsubmx v) = v.
by rewrite -{2}[v]hsubmxK [lsubmx v]mx11_scalar !mxE !lshift0 HM00 raddf0.
have: (v + (row_mx 0 P + Q) :=: col_mx v (row_mx 0 P) + Q)%MS.
by rewrite addsmxA; apply:adds_eqmx=> //; exact: addsmxE.
by apply:eqmx_trans; exact:adds_eqmx.
Qed.
Lemma elim_stepP :
forall m n (
M: '
M[
K]
_(
m, 1 +
n)),
let (
R,
b) :=
elim_step M in exists (
v : '
rV_(1 +
n)),
[/\
v 0 0 != 0, (
M :=:
row_mx 0
R +
v *+
b)%
MS &
mxdirect (
row_mx 0
R +
v *+
b)].
Proof.
elim=> [n M | m IHm n] /=.
exists (const_mx 1); split; first by rewrite mxE oner_eq0.
by rewrite flatmx0 row_mx0 mulr0n; apply/eqmx_sym/addsmx0.
by rewrite flatmx0 mxdirectE /= addsmx0 !mxrank0.
change m.+1 with (1 + m)%N=> M.
have [HM00|HM00] := altP (M 0 0 =P 0).
move:(IHm _ (@dsubmx _ 1 m _ M)).
case:(elim_step _)=> [R b] [v [Hv0]].
case:b=> [[HS Hd] | [HS Hd]].
exists v; split=> //.
by rewrite -{1}[M]vsubmxK; apply:adds_rowmx0M=> //; rewrite mxE lshift0.
exact:directmx0M.
exists (const_mx 1); split; first by rewrite mxE oner_eq0.
by rewrite -{1}[M]vsubmxK; apply:adds_rowmx0M=> //; rewrite mxE lshift0.
by apply/mxdirect_addsP; exact:capmx0.
exists (usubmx M); split; first by rewrite mxE lshift0 HM00.
pose D : 'M[K]_(1 + m) := block_mx 1%:M 0 (-1 / M 0 0 *: (dlsubmx M)) 1%:M.
have hD : row_full D.
by rewrite row_full_unit unitmxE !det_lblock !det1 !mul1r unitr1.
apply:eqmx_sym; apply/eqmxP.
rewrite -!(eqmxMfull M hD) -{6 7}[M]submxK mulmx_block block_mxEv addsmxC.
rewrite -!addsmxE; apply/eqmxP; apply:adds_eqmx.
by rewrite !mul0mx !addr0 !mul1mx -[usubmx M]hsubmxK.
rewrite {1}/GRing.zero /=; apply/eqmxP; rewrite [ulsubmx M]mx11_scalar !mxE.
rewrite !lshift0 mul_mx_scalar scalerA mulrC (mulfVK HM00) scaleN1r mul1mx.
rewrite addNr addrC mul1mx -(castmx_const (addn1 _, erefl _)) -castmx_row.
rewrite -scalerA scaleN1r mulNmx -col_mx_const -block_mxEh block_mxEv.
by rewrite !eqmx_cast row_mx_const -!addsmxE !raddf0 !addsmx0; exact/eqmxP.
by apply:directmx0M; rewrite mxE lshift0 HM00.
Qed.
Lemma rank_row0mx (
n m:
nat) (
M: '
M[
K]
_(
n,
m)) :
\
rank (
row_mx (0: '
cV[
K]
_n)
M) = \
rank M.
Proof.
by rewrite -mxrank_tr tr_row_mx trmx0 -addsmxE adds0mx mxrank_tr. Qed.
Lemma elim_step_rank m n (
M: '
M[
K]
_(
m, 1 +
n)) :
let (
R,
b) :=
elim_step M in \
rank M = (\
rank R +
b)%
N.
Proof.
move:(elim_stepP M); case:(elim_step _)=> R b [v [Hv0 ->]].
rewrite mxdirectE /= rank_rV rank_row0mx; move/eqP.
case:b; last by rewrite eqxx.
have -> //: v != 0.
by apply/eqP=> /matrixP/(_ 0 0)/eqP; rewrite mxE (negbTE Hv0).
Qed.
Fixpoint rank_elim (
m n :
nat) {
struct n} : '
M[
K]
_(
m,
n) ->
nat :=
match n return '
M[
K]
_(
m,
n) ->
nat with
|
q.+1 =>
fun M =>
let (
R,
b) :=
elim_step M in (
rank_elim R +
b)%
N
|
_ =>
fun _ => 0%
N
end.
Lemma rank_elimP :
forall n m (
M : '
M[
K]
_(
m,
n)),
rank_elim M = \
rank M.
Proof.
elim=> [m M|n IHn m M] /=; first by rewrite thinmx0 mxrank0.
by move:(elim_step_rank M); case:(elim_step M)=> R b ->; rewrite IHn.
Qed.
Variable CK :
cunitRingType K.
Fixpoint elim_step_seqmx p n {
struct p} :
seqmatrix CK -> (
seqmatrix CK *
bool) :=
match p return seqmatrix CK -> (
seqmatrix CK *
bool)
with
|
p'.+1 =>
fun l =>
let a :=
l 0%
N 0%
N in
if a ==
zero CK then
let (
R,
b) :=
elim_step_seqmx p'
n (
dsubseqmx 1
l)
in
(
col_seqmx (
ursubseqmx 1 1
l)
R,
b)
else
let v :=
scaleseqmx (
cinv a) (
dlsubseqmx 1 1
l)
in
let R :=
subseqmx (
drsubseqmx 1 1
l) (
mulseqmx 1
n v (
ursubseqmx 1 1
l))
in
let v0 :=
const_seqmx 1 (
size (
rowseqmx l 0)).-1 (
zero CK)
in
(
col_seqmx R v0,
true)
|
_ =>
fun l => ([::] ,
false)
end.
Lemma elim_step_seqmxE :
forall m n (
M : '
M_(
m, 1 +
n)),
let (
R,
b) := (
elim_step M)
in
elim_step_seqmx m (1 +
n) (
seqmx_of_mx CK M) = (
seqmx_of_mx CK R,
b).
Proof.
elim=> [n M /=|m IHm n M /=]; first by rewrite seqmx0n.
rewrite -(inj_eq (@inj_trans K CK) (M 0 0) 0) zeroE -seqmxE; case: ifP=> _.
move:(IHm _ (@dsubmx _ 1 _ _ M)); case:(elim_step (dsubmx _))=> R b.
by rewrite dsubseqmxE=> ->; rewrite ursubseqmxE col_seqmxE.
rewrite cast_seqmx -col_seqmxE subseqmxE -drsubseqmxE -mulseqmxE -scaleseqmxE.
rewrite -dlsubseqmxE -ursubseqmxE -const_seqmxE size_row_seqmx //.
by rewrite cinvE zeroE -seqmxE.
Qed.
Fixpoint rank_elim_seqmx (
m n:
nat) {
struct n} :
seqmatrix CK ->
nat :=
match n return seqmatrix CK ->
nat with
|
q.+1 =>
fun M =>
let:(
R,
b) :=
elim_step_seqmx m n M in
(
rank_elim_seqmx m q R +
b)%
N
|
_ =>
fun _ => 0%
N
end.
Lemma rank_elim_seqmxE :
forall m n (
M : '
M_(
m,
n)),
rank_elim_seqmx m n (
seqmx_of_mx CK M) =
rank_elim M.
Proof.
move=> m; elim=> // n IHn M; rewrite /rank_elim_seqmx /rank_elim.
by move:(elim_step_seqmxE M); case: (elim_step _)=> R b ->; rewrite -/rank_elim_seqmx IHn.
Qed.
End FieldRank.