FinMatrix.Matrix.MatrixDet
Require Import Extraction.
Require Export ListExt NatExt Matrix Permutation.
Require ZArith Reals.
Generalizable Variable A Aadd Azero Aopp Amul Aone Ainv.
Section mdet.
Context `{HARing : ARing}.
Add Ring ring_inst : (make_ring_theory HARing).
Notation "0" := Azero : A_scope.
Notation "1" := Aone : A_scope.
Infix "+" := Aadd : A_scope.
Notation "- a" := (Aopp a) : A_scope.
Notation Asub a b := (a + -b).
Infix "-" := Asub : A_scope.
Infix "*" := Amul : A_scope.
Notation vadd := (@vadd _ Aadd).
Infix "+" := vadd : vec_scope.
Notation vcmul := (@vcmul _ Amul).
Infix "c*" := vcmul : vec_scope.
Notation smat n := (smat A n).
Notation mmul := (@mmul _ Aadd 0 Amul).
Infix "*" := mmul : mat_scope.
Notation mat1 := (@mat1 _ 0 1).
Notation seqsum := (@seqsum _ Aadd 0).
Notation seqprod := (@seqprod _ Amul 1).
Notation ronum := (@ronum nat Nat.ltb).
Context `{HARing : ARing}.
Add Ring ring_inst : (make_ring_theory HARing).
Notation "0" := Azero : A_scope.
Notation "1" := Aone : A_scope.
Infix "+" := Aadd : A_scope.
Notation "- a" := (Aopp a) : A_scope.
Notation Asub a b := (a + -b).
Infix "-" := Asub : A_scope.
Infix "*" := Amul : A_scope.
Notation vadd := (@vadd _ Aadd).
Infix "+" := vadd : vec_scope.
Notation vcmul := (@vcmul _ Amul).
Infix "c*" := vcmul : vec_scope.
Notation smat n := (smat A n).
Notation mmul := (@mmul _ Aadd 0 Amul).
Infix "*" := mmul : mat_scope.
Notation mat1 := (@mat1 _ 0 1).
Notation seqsum := (@seqsum _ Aadd 0).
Notation seqprod := (@seqprod _ Amul 1).
Notation ronum := (@ronum nat Nat.ltb).
n阶行列式的完全展开式 (行下标固定，列下标来自于全排列）
Definition mdet_old {n} : smat n -> A :=
match n with
| O => fun _ => 1
| S n' =>
fun (M : smat (S n')) =>
let colIds := perm (seq 0 n) in
let item (l:list nat) : A :=
(let x := seqprod n (fun i => M.[#i].[#(nth i l O)]) in
if odd (ronum l) then - x else x) in
fold_left Aadd (map item colIds) 0
end.
新的实现：元素索引为 nat 类型，避免了提供 i < n 的证明，无需处理 n = 0
Definition mdet {n} (M : smat n) : A :=
let colIds : dlist nat := perm (seq 0 n) in
let item (l : list nat) : A :=
(let x := seqprod n (fun i => (m2f 0 M) i (nth i l O)) in
if odd (ronum l) then - x else x) in
fold_left Aadd (map item colIds) 0.
Notation "| M |" := (mdet M) : mat_scope.
let colIds : dlist nat := perm (seq 0 n) in
let item (l : list nat) : A :=
(let x := seqprod n (fun i => (m2f 0 M) i (nth i l O)) in
if odd (ronum l) then - x else x) in
fold_left Aadd (map item colIds) 0.
Notation "| M |" := (mdet M) : mat_scope.
n阶行列式的完全展开式 (列下标固定，行下标来自于全排列）
Definition mdet' {n} (M : smat n) : A :=
let rowIds : dlist nat := perm (seq 0 n) in
let item (l : list nat) : A :=
(let x := seqprod n (fun j => (m2f 0 M) (nth j l O) j) in
if odd (ronum l) then - x else x) in
fold_left Aadd (map item rowIds) 0.
Lemma mdet'_eq_mdet : forall {n} (M : smat n), mdet' M = mdet M.
Proof.
Admitted.
let rowIds : dlist nat := perm (seq 0 n) in
let item (l : list nat) : A :=
(let x := seqprod n (fun j => (m2f 0 M) (nth j l O) j) in
if odd (ronum l) then - x else x) in
fold_left Aadd (map item rowIds) 0.
Lemma mdet'_eq_mdet : forall {n} (M : smat n), mdet' M = mdet M.
Proof.
Admitted.
Property 1: |M\T| = |M|
Lemma mdet_mtrans : forall {n} (M : smat n), |M\T| = |M|.
Proof.
intros. rewrite <- mdet'_eq_mdet at 1.
unfold mdet, mdet'. f_equal.
apply map_ext_in; intros.
destruct (odd (ronum a)).
- f_equal. apply seqsum_eq; intros.
erewrite !nth_m2f, mnth_mtrans; auto.
- apply seqprod_eq; intros. erewrite !nth_m2f, mnth_mtrans; auto.
Unshelve. all: auto.
apply perm_index_lt; auto.
apply perm_index_lt; auto.
Qed.
Lemma mdet_mmul : forall {n} (M N : smat n), |M * N| = (|M| * |N|)%A.
Proof.
Admitted.
Lemma mdet_mat1 : forall {n}, |@mat1 n| = 1.
Proof.
induction n; simpl.
- unfold mdet. simpl. ring.
- unfold mdet in *. simpl.
Admitted.
Proof.
intros. rewrite <- mdet'_eq_mdet at 1.
unfold mdet, mdet'. f_equal.
apply map_ext_in; intros.
destruct (odd (ronum a)).
- f_equal. apply seqsum_eq; intros.
erewrite !nth_m2f, mnth_mtrans; auto.
- apply seqprod_eq; intros. erewrite !nth_m2f, mnth_mtrans; auto.
Unshelve. all: auto.
apply perm_index_lt; auto.
apply perm_index_lt; auto.
Qed.
Lemma mdet_mmul : forall {n} (M N : smat n), |M * N| = (|M| * |N|)%A.
Proof.
Admitted.
Lemma mdet_mat1 : forall {n}, |@mat1 n| = 1.
Proof.
induction n; simpl.
- unfold mdet. simpl. ring.
- unfold mdet in *. simpl.
Admitted.
g (f a1 + ... + f an + b) = gf a1 + ... + gf an + g b
Lemma fold_left_map :
forall {A B} (l : list A) (fadd : B -> B -> B) (b : B) (f : A -> B) (g : B -> B)
(homo: forall b1 b2, g (fadd b1 b2) = fadd (g b1) (g b2)),
g (fold_left fadd (map f l) b) =
fold_left fadd (map (fun x => g (f x)) l) (g b).
Proof.
clear. intros A B l.
induction l; intros; simpl; auto.
rewrite IHl; auto. f_equal. auto.
Qed.
forall {A B} (l : list A) (fadd : B -> B -> B) (b : B) (f : A -> B) (g : B -> B)
(homo: forall b1 b2, g (fadd b1 b2) = fadd (g b1) (g b2)),
g (fold_left fadd (map f l) b) =
fold_left fadd (map (fun x => g (f x)) l) (g b).
Proof.
clear. intros A B l.
induction l; intros; simpl; auto.
rewrite IHl; auto. f_equal. auto.
Qed.
h (f a1 + ... + f an + b1) (g a1 + ... + g an + b2) =
hfg a1 + ... + hfg an + h b1 b2
Lemma fold_left_map_map :
forall {A B} (l : list A) (fadd : B -> B -> B) (b1 b2 : B) (f g : A -> B)
(h : B -> B -> B)
(homo: forall b1 b2 b3 b4, h (fadd b1 b3) (fadd b2 b4) = fadd (h b1 b2) (h b3 b4)),
h (fold_left fadd (map f l) b1) (fold_left fadd (map g l) b2) =
fold_left fadd (map (fun x => h (f x) (g x)) l) (h b1 b2).
Proof.
clear. intros A B l.
induction l; intros; simpl; auto.
rewrite IHl; auto. f_equal. auto.
Qed.
forall {A B} (l : list A) (fadd : B -> B -> B) (b1 b2 : B) (f g : A -> B)
(h : B -> B -> B)
(homo: forall b1 b2 b3 b4, h (fadd b1 b3) (fadd b2 b4) = fadd (h b1 b2) (h b3 b4)),
h (fold_left fadd (map f l) b1) (fold_left fadd (map g l) b2) =
fold_left fadd (map (fun x => h (f x) (g x)) l) (h b1 b2).
Proof.
clear. intros A B l.
induction l; intros; simpl; auto.
rewrite IHl; auto. f_equal. auto.
Qed.
Property 2 : | M with x*row(M,i) | = x * |M|
Lemma mdet_row_scale : forall {n} (M1 M2 : smat n) (i : 'I_n) (x : A),
(forall j, j <> i -> M1.[j] = M2.[j]) ->
(M1.[i] = x c* M2.[i])%V -> |M1| = (x * |M2|)%A.
Proof.
intros. unfold mdet.
rewrite fold_left_map.
2:{ intros; ring. }
f_equal; try ring. apply map_ext_in; intros.
assert (seqprod n (fun i0 : nat => m2f 0 M1 i0 (nth i0 a O)) =
(x * seqprod n (fun i0 : nat => m2f 0 M2 i0 (nth i0 a O)))%A).
- rewrite seqprod_cmul_l with (j:=i); [|fin].
apply seqprod_eq; intros.
assert (i0 < n) as Hi by lia.
assert (nth i0 a O < n) as Hj. apply perm_index_lt; auto.
bdestruct (i0 =? i).
+ rewrite !nth_m2f with (Hi:=Hi)(Hj:=Hj).
replace (nat2fin i0 Hi) with i. rewrite H0; auto. subst; fin.
+ rewrite !nth_m2f with (Hi:=Hi)(Hj:=Hj). rewrite H; auto.
intro; destruct H3; subst; fin.
- destruct (odd (ronum a)) eqn:E; auto.
rewrite H2. ring.
Qed.
(forall j, j <> i -> M1.[j] = M2.[j]) ->
(M1.[i] = x c* M2.[i])%V -> |M1| = (x * |M2|)%A.
Proof.
intros. unfold mdet.
rewrite fold_left_map.
2:{ intros; ring. }
f_equal; try ring. apply map_ext_in; intros.
assert (seqprod n (fun i0 : nat => m2f 0 M1 i0 (nth i0 a O)) =
(x * seqprod n (fun i0 : nat => m2f 0 M2 i0 (nth i0 a O)))%A).
- rewrite seqprod_cmul_l with (j:=i); [|fin].
apply seqprod_eq; intros.
assert (i0 < n) as Hi by lia.
assert (nth i0 a O < n) as Hj. apply perm_index_lt; auto.
bdestruct (i0 =? i).
+ rewrite !nth_m2f with (Hi:=Hi)(Hj:=Hj).
replace (nat2fin i0 Hi) with i. rewrite H0; auto. subst; fin.
+ rewrite !nth_m2f with (Hi:=Hi)(Hj:=Hj). rewrite H; auto.
intro; destruct H3; subst; fin.
- destruct (odd (ronum a)) eqn:E; auto.
rewrite H2. ring.
Qed.
Property 3: 若某一行是两组数的和，则行列式等于两个行列式的和，
它们的这一行分别是这两组数
Lemma mdet_row_add : forall {n} (M1 M2 M : smat n) (i : 'I_n),
(forall j, j <> i -> M1.[j] = M.[j] /\ M2.[j] = M.[j]) ->
(M1.[i] + M2.[i])%V = M.[i] -> |M| = (|M1| + |M2|)%A.
Proof.
intros. unfold mdet.
rewrite fold_left_map_map.
2:{ intros; ring. }
f_equal; try ring. apply map_ext_in; intros.
assert (seqprod n (fun i0 : nat => m2f 0 M i0 (nth i0 a O)) =
(seqprod n (fun i0 : nat => m2f 0 M1 i0 (nth i0 a O)) +
seqprod n (fun i0 : nat => m2f 0 M2 i0 (nth i0 a O)))%A).
- pose proof (fin2nat_lt i) as Hi.
replace n with (i + S (n - S i))%nat at 1 2 3 by lia.
rewrite !seqprod_plusIdx_three.
replace (m2f 0 M i (nth i a O))
with ((m2f 0 M1 i (nth i a O)) + (m2f 0 M2 i (nth i a O)))%A.
2:{
assert (nth i a O < n) as Hj. apply perm_index_lt; auto.
rewrite !nth_m2f with (Hi:=Hi) (Hj:=Hj). fin.
rewrite <- H0. rewrite vnth_vadd. auto. }
ring_simplify. f_equal.
+
move2h (m2f 0 M1 i (nth i a O)). f_equal. f_equal.
* apply seqprod_eq; intros.
assert (i0 < n) as Hi0. pose proof (fin2nat_lt i). lia.
assert (nth i0 a O < n) as Hj0. apply perm_index_lt; auto.
rewrite !nth_m2f with (Hi:=Hi0) (Hj:=Hj0).
assert (nat2fin i0 Hi0 <> i).
{ intro. subst. fin. }
destruct (H _ H3). rewrite H4. auto.
* apply seqprod_eq; intros.
assert (S (i + i0) < n) as Hi0. pose proof (fin2nat_lt i). lia.
assert (nth (S (i + i0)) a O < n) as Hj0. apply perm_index_lt; auto.
rewrite !nth_m2f with (Hi:=Hi0) (Hj:=Hj0).
assert (nat2fin (S (i + i0)) Hi0 <> i).
{ intro. destruct i. simpl in *. apply fin_eq_iff in H3. lia. }
destruct (H _ H3). rewrite H4. auto.
+
move2h (m2f 0 M2 i (nth i a O)). f_equal. f_equal.
* apply seqprod_eq; intros.
assert (i0 < n) as Hi0. pose proof (fin2nat_lt i). lia.
assert (nth i0 a O < n) as Hj0. apply perm_index_lt; auto.
rewrite !nth_m2f with (Hi:=Hi0) (Hj:=Hj0).
assert (nat2fin i0 Hi0 <> i).
{ intro. subst. fin. }
destruct (H _ H3). rewrite H5. auto.
* apply seqprod_eq; intros.
assert (S (i + i0) < n) as Hi0. pose proof (fin2nat_lt i). lia.
assert (nth (S (i + i0)) a O < n) as Hj0. apply perm_index_lt; auto.
rewrite !nth_m2f with (Hi:=Hi0) (Hj:=Hj0).
assert (nat2fin (S (i + i0)) Hi0 <> i).
{ intro. destruct i. simpl in *. apply fin_eq_iff in H3. lia. }
destruct (H _ H3). rewrite H5. auto.
- destruct (odd (ronum a)) eqn:E; auto.
rewrite H2. ring.
Qed.
Lemma mdet_row_swap_lt : forall {n} (M1 M2 : smat n) (i k : 'I_n),
i < k ->
(forall j, j <> i -> j <> k -> M1.[j] = M2.[j]) ->
M1.[i] = M2.[k] -> M1.[k] = M2.[i] ->
(|M1| = - |M2|)%A.
Proof.
intros. unfold mdet.
rewrite fold_left_map. 2: intros; ring.
f_equal; try ring. apply map_ext_in; intros.
assert (seqprod n (fun i0 : nat => m2f 0 M1 i0 (nth i0 a O)) =
- seqprod n (fun i0 : nat => m2f 0 M2 i0 (nth i0 a O))).
- pose proof (fin2nat_lt i) as Hi.
pose proof (fin2nat_lt k) as Hk.
replace n with (i + S ((k - S i) + S (n - S k)))%nat at 1 2; fin.
repeat (rewrite ?seqprod_plusIdx; rewrite ?seqprodS_head).
replace (i + O)%nat with (fin2nat i); fin.
replace (i + S (k - S i + O))%nat with (fin2nat k); fin.
move2h (m2f 0 M1 k (nth k a O)).
move2h (m2f 0 M1 i (nth i a O)).
move2h (m2f 0 M2 k (nth k a O)).
move2h (m2f 0 M2 i (nth i a O)).
ring_simplify.
assert (nth i a O < n) as Hi'. apply perm_index_lt; auto.
assert (nth k a O < n) as Hk'. apply perm_index_lt; auto.
rewrite !nth_m2f with (Hi:=Hi)(Hj:=Hi').
rewrite !nth_m2f with (Hi:=Hk)(Hj:=Hk').
fin. rewrite H1,H2.
remember (seqprod i (fun i0 : nat => m2f 0 M1 i0 (nth i0 a O))) as x1.
remember (seqprod i (fun i0 : nat => m2f 0 M2 i0 (nth i0 a O))) as y1.
remember (seqprod (k - S i)
(fun i0 : nat => m2f 0 M1 (i + S i0) (nth (i + S i0) a O))) as x2.
remember (seqprod (k - S i)
(fun i0 : nat => m2f 0 M2 (i + S i0) (nth (i + S i0) a O))) as y2.
remember (seqprod (n - S k)
(fun i0 : nat => m2f 0 M1 (i + S (k - S i + S i0))
(nth (i + S (k - S i + S i0)) a O)))%A as x3.
remember (seqprod (n - S k)
(fun i0 : nat => m2f 0 M2 (i + S (k - S i + S i0))
(nth (i + S (k - S i + S i0)) a O)))%A as y3.
assert (x1 = y1).
{ rewrite Heqx1, Heqy1. apply seqprod_eq; intros.
assert (i0 < n) by lia. assert (nth i0 a O < n). apply perm_index_lt; auto.
erewrite !nth_m2f with (Hi:=H5)(Hj:=H6).
destruct i,k. fin. rewrite H0; auto.
{ intro. apply fin_eq_iff in H7. lia. }
{ intro. apply fin_eq_iff in H7. lia. } }
assert (x2 = y2).
{ rewrite Heqx2, Heqy2. apply seqprod_eq; intros.
assert (i + S i0 < n) by lia.
assert (nth (i + S i0) a O < n). apply perm_index_lt; auto.
erewrite !nth_m2f with (Hi:=H6)(Hj:=H7).
destruct i,k. fin. rewrite H0; auto.
{ intro. apply fin_eq_iff in H8. fin. }
{ intro. apply fin_eq_iff in H8. fin. } }
assert (x3 = y3).
{ rewrite Heqx3, Heqy3. apply seqprod_eq; intros.
assert (i + S (k - S i + S i0) < n) by lia.
assert (nth (i + S (k - S i + S i0)) a O < n). apply perm_index_lt; auto.
erewrite !nth_m2f with (Hi:=H7)(Hj:=H8).
destruct i,k. fin. rewrite H0; auto.
{ intro. apply fin_eq_iff in H9. fin. }
{ intro. apply fin_eq_iff in H9. fin. } }
clear Heqx1 Heqy1 Heqx2 Heqy2 Heqx3 Heqy3. subst.
admit.
- rewrite H4. destruct (odd (ronum a)); auto.
Admitted.
Lemma mdet_row_swap : forall {n} (M1 M2 : smat n) (i k : 'I_n),
i <> k ->
(forall j, j <> i -> j <> k -> M1.[j] = M2.[j]) ->
M1.[i] = M2.[k] -> M1.[k] = M2.[i] ->
(|M1| = - |M2|)%A.
Proof.
intros. destruct (i ??< k).
- apply mdet_row_swap_lt with (i:=i)(k:=k); auto.
- apply mdet_row_swap_lt with (i:=k)(k:=i); auto.
assert (fin2nat i <> fin2nat k). fin2nat; auto. lia.
Qed.
Lemma mdet_row_mrowSwap : forall {n} (M : smat n) (i k : 'I_n),
i <> k -> (|mrowSwap i k M| = - |M|)%A.
Proof.
intros. unfold mrowSwap.
apply mdet_row_swap with (i:=i) (k:=k); auto; intros; fin.
Qed.
Section Field.
Context `{HField : Field A Aadd Azero Aopp Amul Aone}.
Context {AeqDec : Dec (@eq A)}.
(forall j, j <> i -> M1.[j] = M.[j] /\ M2.[j] = M.[j]) ->
(M1.[i] + M2.[i])%V = M.[i] -> |M| = (|M1| + |M2|)%A.
Proof.
intros. unfold mdet.
rewrite fold_left_map_map.
2:{ intros; ring. }
f_equal; try ring. apply map_ext_in; intros.
assert (seqprod n (fun i0 : nat => m2f 0 M i0 (nth i0 a O)) =
(seqprod n (fun i0 : nat => m2f 0 M1 i0 (nth i0 a O)) +
seqprod n (fun i0 : nat => m2f 0 M2 i0 (nth i0 a O)))%A).
- pose proof (fin2nat_lt i) as Hi.
replace n with (i + S (n - S i))%nat at 1 2 3 by lia.
rewrite !seqprod_plusIdx_three.
replace (m2f 0 M i (nth i a O))
with ((m2f 0 M1 i (nth i a O)) + (m2f 0 M2 i (nth i a O)))%A.
2:{
assert (nth i a O < n) as Hj. apply perm_index_lt; auto.
rewrite !nth_m2f with (Hi:=Hi) (Hj:=Hj). fin.
rewrite <- H0. rewrite vnth_vadd. auto. }
ring_simplify. f_equal.
+
move2h (m2f 0 M1 i (nth i a O)). f_equal. f_equal.
* apply seqprod_eq; intros.
assert (i0 < n) as Hi0. pose proof (fin2nat_lt i). lia.
assert (nth i0 a O < n) as Hj0. apply perm_index_lt; auto.
rewrite !nth_m2f with (Hi:=Hi0) (Hj:=Hj0).
assert (nat2fin i0 Hi0 <> i).
{ intro. subst. fin. }
destruct (H _ H3). rewrite H4. auto.
* apply seqprod_eq; intros.
assert (S (i + i0) < n) as Hi0. pose proof (fin2nat_lt i). lia.
assert (nth (S (i + i0)) a O < n) as Hj0. apply perm_index_lt; auto.
rewrite !nth_m2f with (Hi:=Hi0) (Hj:=Hj0).
assert (nat2fin (S (i + i0)) Hi0 <> i).
{ intro. destruct i. simpl in *. apply fin_eq_iff in H3. lia. }
destruct (H _ H3). rewrite H4. auto.
+
move2h (m2f 0 M2 i (nth i a O)). f_equal. f_equal.
* apply seqprod_eq; intros.
assert (i0 < n) as Hi0. pose proof (fin2nat_lt i). lia.
assert (nth i0 a O < n) as Hj0. apply perm_index_lt; auto.
rewrite !nth_m2f with (Hi:=Hi0) (Hj:=Hj0).
assert (nat2fin i0 Hi0 <> i).
{ intro. subst. fin. }
destruct (H _ H3). rewrite H5. auto.
* apply seqprod_eq; intros.
assert (S (i + i0) < n) as Hi0. pose proof (fin2nat_lt i). lia.
assert (nth (S (i + i0)) a O < n) as Hj0. apply perm_index_lt; auto.
rewrite !nth_m2f with (Hi:=Hi0) (Hj:=Hj0).
assert (nat2fin (S (i + i0)) Hi0 <> i).
{ intro. destruct i. simpl in *. apply fin_eq_iff in H3. lia. }
destruct (H _ H3). rewrite H5. auto.
- destruct (odd (ronum a)) eqn:E; auto.
rewrite H2. ring.
Qed.
Lemma mdet_row_swap_lt : forall {n} (M1 M2 : smat n) (i k : 'I_n),
i < k ->
(forall j, j <> i -> j <> k -> M1.[j] = M2.[j]) ->
M1.[i] = M2.[k] -> M1.[k] = M2.[i] ->
(|M1| = - |M2|)%A.
Proof.
intros. unfold mdet.
rewrite fold_left_map. 2: intros; ring.
f_equal; try ring. apply map_ext_in; intros.
assert (seqprod n (fun i0 : nat => m2f 0 M1 i0 (nth i0 a O)) =
- seqprod n (fun i0 : nat => m2f 0 M2 i0 (nth i0 a O))).
- pose proof (fin2nat_lt i) as Hi.
pose proof (fin2nat_lt k) as Hk.
replace n with (i + S ((k - S i) + S (n - S k)))%nat at 1 2; fin.
repeat (rewrite ?seqprod_plusIdx; rewrite ?seqprodS_head).
replace (i + O)%nat with (fin2nat i); fin.
replace (i + S (k - S i + O))%nat with (fin2nat k); fin.
move2h (m2f 0 M1 k (nth k a O)).
move2h (m2f 0 M1 i (nth i a O)).
move2h (m2f 0 M2 k (nth k a O)).
move2h (m2f 0 M2 i (nth i a O)).
ring_simplify.
assert (nth i a O < n) as Hi'. apply perm_index_lt; auto.
assert (nth k a O < n) as Hk'. apply perm_index_lt; auto.
rewrite !nth_m2f with (Hi:=Hi)(Hj:=Hi').
rewrite !nth_m2f with (Hi:=Hk)(Hj:=Hk').
fin. rewrite H1,H2.
remember (seqprod i (fun i0 : nat => m2f 0 M1 i0 (nth i0 a O))) as x1.
remember (seqprod i (fun i0 : nat => m2f 0 M2 i0 (nth i0 a O))) as y1.
remember (seqprod (k - S i)
(fun i0 : nat => m2f 0 M1 (i + S i0) (nth (i + S i0) a O))) as x2.
remember (seqprod (k - S i)
(fun i0 : nat => m2f 0 M2 (i + S i0) (nth (i + S i0) a O))) as y2.
remember (seqprod (n - S k)
(fun i0 : nat => m2f 0 M1 (i + S (k - S i + S i0))
(nth (i + S (k - S i + S i0)) a O)))%A as x3.
remember (seqprod (n - S k)
(fun i0 : nat => m2f 0 M2 (i + S (k - S i + S i0))
(nth (i + S (k - S i + S i0)) a O)))%A as y3.
assert (x1 = y1).
{ rewrite Heqx1, Heqy1. apply seqprod_eq; intros.
assert (i0 < n) by lia. assert (nth i0 a O < n). apply perm_index_lt; auto.
erewrite !nth_m2f with (Hi:=H5)(Hj:=H6).
destruct i,k. fin. rewrite H0; auto.
{ intro. apply fin_eq_iff in H7. lia. }
{ intro. apply fin_eq_iff in H7. lia. } }
assert (x2 = y2).
{ rewrite Heqx2, Heqy2. apply seqprod_eq; intros.
assert (i + S i0 < n) by lia.
assert (nth (i + S i0) a O < n). apply perm_index_lt; auto.
erewrite !nth_m2f with (Hi:=H6)(Hj:=H7).
destruct i,k. fin. rewrite H0; auto.
{ intro. apply fin_eq_iff in H8. fin. }
{ intro. apply fin_eq_iff in H8. fin. } }
assert (x3 = y3).
{ rewrite Heqx3, Heqy3. apply seqprod_eq; intros.
assert (i + S (k - S i + S i0) < n) by lia.
assert (nth (i + S (k - S i + S i0)) a O < n). apply perm_index_lt; auto.
erewrite !nth_m2f with (Hi:=H7)(Hj:=H8).
destruct i,k. fin. rewrite H0; auto.
{ intro. apply fin_eq_iff in H9. fin. }
{ intro. apply fin_eq_iff in H9. fin. } }
clear Heqx1 Heqy1 Heqx2 Heqy2 Heqx3 Heqy3. subst.
admit.
- rewrite H4. destruct (odd (ronum a)); auto.
Admitted.
Lemma mdet_row_swap : forall {n} (M1 M2 : smat n) (i k : 'I_n),
i <> k ->
(forall j, j <> i -> j <> k -> M1.[j] = M2.[j]) ->
M1.[i] = M2.[k] -> M1.[k] = M2.[i] ->
(|M1| = - |M2|)%A.
Proof.
intros. destruct (i ??< k).
- apply mdet_row_swap_lt with (i:=i)(k:=k); auto.
- apply mdet_row_swap_lt with (i:=k)(k:=i); auto.
assert (fin2nat i <> fin2nat k). fin2nat; auto. lia.
Qed.
Lemma mdet_row_mrowSwap : forall {n} (M : smat n) (i k : 'I_n),
i <> k -> (|mrowSwap i k M| = - |M|)%A.
Proof.
intros. unfold mrowSwap.
apply mdet_row_swap with (i:=i) (k:=k); auto; intros; fin.
Qed.
Section Field.
Context `{HField : Field A Aadd Azero Aopp Amul Aone}.
Context {AeqDec : Dec (@eq A)}.
WE ASSUME the field is not F2, i.e. {0,1},
because we mainly use a numerical field.
SO, WE ASSUME THIS AXIOM HERE.
Axiom two_neq0 : (1 + 1)%A <> 0.
Lemma mdet_row_same_eq0 : forall {n} (M : smat n) (i j : 'I_n),
i <> j -> M.[i] = M.[j] -> |M| = 0.
Proof.
intros.
assert (|M| = -|M|). apply (mdet_row_swap M M i j); auto.
apply group_sub_eq0_iff_eq in H1.
rewrite group_opp_opp in H1.
replace (|M|) with (1 * |M|)%A in H1 by ring.
rewrite <- distrRight in H1.
rewrite field_mul_eq0_iff in H1. destruct H1; auto.
apply two_neq0 in H1. easy.
Qed.
Corollary mdet_row_vset_eq0 : forall {n} (M : smat n) (i j : 'I_n),
i <> j -> |vset M i (M j)| = 0.
Proof.
intros. apply (mdet_row_same_eq0 _ i j); auto.
rewrite vnth_vset_eq, vnth_vset_neq; auto.
Qed.
Lemma mdet_row_cmul : forall {n} (M : smat n) (i j : 'I_n) (x : A),
i <> j -> M.[i] = (x c* M.[j])%A -> |M| = 0.
Proof.
intros. rewrite (mdet_row_scale M (vset M i M.[j]) i x).
- pose proof (mdet_row_vset_eq0 M i j H). rewrite H1. ring.
- intros k Hk. bdestruct (i =? k); fin.
rewrite vnth_vset_neq; auto.
- rewrite vnth_vset_eq; auto.
Qed.
Corollary mdet_row_vset_cmul_eq0 : forall {n} (M : smat n) (i j : 'I_n) x,
i <> j -> |vset M i (x c* M j)| = 0.
Proof.
intros.
pose proof (mdet_row_cmul (vset M i (x c* M j)) i j x H).
rewrite vnth_vset_eq, vnth_vset_neq in H0; auto.
Qed.
Lemma mdet_row_addRow : forall {n} (M1 M2 : smat n) (i j : 'I_n) (x : A),
i <> j ->
(forall k, k <> i -> M1.[k] = M2.[k]) ->
M1.[i] = (M2.[i] + x c*M2.[j])%V -> |M1| = |M2|.
Proof.
intros.
pose proof (mdet_row_add M2 (vset M2 i (x c* M2.[j])) M1 i).
rewrite H2; auto.
- rewrite (mdet_row_vset_cmul_eq0); auto. ring.
- intros k Hk. rewrite H0; auto. split; auto.
rewrite vnth_vset_neq; auto.
- rewrite vnth_vset_eq. auto.
Qed.
End Field.
Section Field.
Context `{HField : Field A Aadd 0 Aopp Amul 1}.
Add Field field_inst : (make_field_theory HField).
Lemma mdet_row_same_eq0 : forall {n} (M : smat n) (i j : 'I_n),
i <> j -> M.[i] = M.[j] -> |M| = 0.
Proof.
intros.
assert (|M| = -|M|). apply (mdet_row_swap M M i j); auto.
apply group_sub_eq0_iff_eq in H1.
rewrite group_opp_opp in H1.
replace (|M|) with (1 * |M|)%A in H1 by ring.
rewrite <- distrRight in H1.
rewrite field_mul_eq0_iff in H1. destruct H1; auto.
apply two_neq0 in H1. easy.
Qed.
Corollary mdet_row_vset_eq0 : forall {n} (M : smat n) (i j : 'I_n),
i <> j -> |vset M i (M j)| = 0.
Proof.
intros. apply (mdet_row_same_eq0 _ i j); auto.
rewrite vnth_vset_eq, vnth_vset_neq; auto.
Qed.
Lemma mdet_row_cmul : forall {n} (M : smat n) (i j : 'I_n) (x : A),
i <> j -> M.[i] = (x c* M.[j])%A -> |M| = 0.
Proof.
intros. rewrite (mdet_row_scale M (vset M i M.[j]) i x).
- pose proof (mdet_row_vset_eq0 M i j H). rewrite H1. ring.
- intros k Hk. bdestruct (i =? k); fin.
rewrite vnth_vset_neq; auto.
- rewrite vnth_vset_eq; auto.
Qed.
Corollary mdet_row_vset_cmul_eq0 : forall {n} (M : smat n) (i j : 'I_n) x,
i <> j -> |vset M i (x c* M j)| = 0.
Proof.
intros.
pose proof (mdet_row_cmul (vset M i (x c* M j)) i j x H).
rewrite vnth_vset_eq, vnth_vset_neq in H0; auto.
Qed.
Lemma mdet_row_addRow : forall {n} (M1 M2 : smat n) (i j : 'I_n) (x : A),
i <> j ->
(forall k, k <> i -> M1.[k] = M2.[k]) ->
M1.[i] = (M2.[i] + x c*M2.[j])%V -> |M1| = |M2|.
Proof.
intros.
pose proof (mdet_row_add M2 (vset M2 i (x c* M2.[j])) M1 i).
rewrite H2; auto.
- rewrite (mdet_row_vset_cmul_eq0); auto. ring.
- intros k Hk. rewrite H0; auto. split; auto.
rewrite vnth_vset_neq; auto.
- rewrite vnth_vset_eq. auto.
Qed.
End Field.
Section Field.
Context `{HField : Field A Aadd 0 Aopp Amul 1}.
Add Field field_inst : (make_field_theory HField).
M * N = mat1 -> |M| <> 0
Lemma mmul_eq1_imply_mdet_neq0_l : forall {n} (M N : smat n),
M * N = mat1 -> |M| <> 0.
Proof.
intros. assert(|M * N|=|@mat1 n|). rewrite H; auto.
rewrite mdet_mmul in H0. intro. rewrite H1 in H0. rewrite mdet_mat1 in H0.
ring_simplify in H0. apply field_1_neq_0; auto.
Qed.
M * N = mat1 -> |M| <> 0.
Proof.
intros. assert(|M * N|=|@mat1 n|). rewrite H; auto.
rewrite mdet_mmul in H0. intro. rewrite H1 in H0. rewrite mdet_mat1 in H0.
ring_simplify in H0. apply field_1_neq_0; auto.
Qed.
M * N = mat1 -> |N| <> 0
Lemma mmul_eq1_imply_mdet_neq0_r : forall {n} (M N : smat n),
M * N = mat1 -> |N| <> 0.
Proof.
intros. assert(|M * N|=|@mat1 n|). rewrite H; auto.
rewrite mdet_mmul in H0. intro. rewrite H1 in H0. rewrite mdet_mat1 in H0.
ring_simplify in H0. apply field_1_neq_0; auto.
Qed.
End Field.
End mdet.
M * N = mat1 -> |N| <> 0.
Proof.
intros. assert(|M * N|=|@mat1 n|). rewrite H; auto.
rewrite mdet_mmul in H0. intro. rewrite H1 in H0. rewrite mdet_mat1 in H0.
ring_simplify in H0. apply field_1_neq_0; auto.
Qed.
End Field.
End mdet.
Section mdet_concrete.
Context `{HARing : ARing}.
Add Ring ring_inst : (make_ring_theory HARing).
Notation "0" := Azero : A_scope.
Notation "1" := Aone : A_scope.
Infix "+" := Aadd : A_scope.
Notation "- a" := (Aopp a) : A_scope.
Notation Asub a b := (a + -b).
Infix "-" := Asub : A_scope.
Infix "*" := Amul : A_scope.
Notation mdet := (@mdet _ Aadd 0 Aopp Amul 1).
Context `{HARing : ARing}.
Add Ring ring_inst : (make_ring_theory HARing).
Notation "0" := Azero : A_scope.
Notation "1" := Aone : A_scope.
Infix "+" := Aadd : A_scope.
Notation "- a" := (Aopp a) : A_scope.
Notation Asub a b := (a + -b).
Infix "-" := Asub : A_scope.
Infix "*" := Amul : A_scope.
Notation mdet := (@mdet _ Aadd 0 Aopp Amul 1).
Determinant of a matrix of dimension-1
mdet1 M = |M|
|M| <> 0 <-> mdet_exp <> 0
Lemma mdet1_neq0_iff : forall (M : smat A 1),
mdet M <> 0 <-> M.11 <> 0.
Proof. intros. rewrite <- mdet1_eq_mdet; easy. Qed.
mdet M <> 0 <-> M.11 <> 0.
Proof. intros. rewrite <- mdet1_eq_mdet; easy. Qed.
Determinant of a matrix of dimension-2
mdet2 M = |M|
Lemma mdet2_eq_mdet : forall M, mdet2 M = mdet M.
Proof. intros. unfold mdet2. cbn; rewrite <- !(nth_m2f_nat2finS 0); auto; ring. Qed.
Proof. intros. unfold mdet2. cbn; rewrite <- !(nth_m2f_nat2finS 0); auto; ring. Qed.
|M| <> 0 <-> mdet_exp <> 0
Lemma mdet2_neq0_iff : forall (M : smat A 2),
mdet M <> 0 <-> (M.11*M.22 - M.12*M.21)%A <> 0.
Proof. intros. rewrite <- mdet2_eq_mdet; easy. Qed.
mdet M <> 0 <-> (M.11*M.22 - M.12*M.21)%A <> 0.
Proof. intros. rewrite <- mdet2_eq_mdet; easy. Qed.
Determinant of a matrix of dimension-3
Definition mdet3 (M : smat A 3) :=
(M.11 * M.22 * M.33 - M.11 * M.23 * M.32 -
M.12 * M.21 * M.33 + M.12 * M.23 * M.31 +
M.13 * M.21 * M.32 - M.13 * M.22 * M.31)%A.
(M.11 * M.22 * M.33 - M.11 * M.23 * M.32 -
M.12 * M.21 * M.33 + M.12 * M.23 * M.31 +
M.13 * M.21 * M.32 - M.13 * M.22 * M.31)%A.
mdet3 M = mdet M
Lemma mdet3_eq_mdet : forall M, mdet3 M = mdet M.
Proof. intros. unfold mdet3. cbn; rewrite <- !(nth_m2f_nat2finS 0); auto; ring. Qed.
Proof. intros. unfold mdet3. cbn; rewrite <- !(nth_m2f_nat2finS 0); auto; ring. Qed.
|M| <> 0 <-> mdet_exp <> 0
Lemma mdet3_neq0_iff : forall (M : smat A 3),
mdet M <> 0 <->
(M.11 * M.22 * M.33 - M.11 * M.23 * M.32 -
M.12 * M.21 * M.33 + M.12 * M.23 * M.31 +
M.13 * M.21 * M.32 - M.13 * M.22 * M.31)%A <> 0.
Proof. intros. rewrite <- mdet3_eq_mdet; easy. Qed.
mdet M <> 0 <->
(M.11 * M.22 * M.33 - M.11 * M.23 * M.32 -
M.12 * M.21 * M.33 + M.12 * M.23 * M.31 +
M.13 * M.21 * M.32 - M.13 * M.22 * M.31)%A <> 0.
Proof. intros. rewrite <- mdet3_eq_mdet; easy. Qed.
Determinant of a matrix of dimension-4
Definition mdet4 (M : smat A 4) :=
(M.11*M.22*M.33*M.44 - M.11*M.22*M.34*M.43 -
M.11*M.23*M.32*M.44 + M.11*M.23*M.34*M.42 +
M.11*M.24*M.32*M.43 - M.11*M.24*M.33*M.42 -
M.12*M.21*M.33*M.44 + M.12*M.21*M.34*M.43 +
M.12*M.23*M.31*M.44 - M.12*M.23*M.34*M.41 -
M.12*M.24*M.31*M.43 + M.12*M.24*M.33*M.41 +
M.13*M.21*M.32*M.44 - M.13*M.21*M.34*M.42 -
M.13*M.22*M.31*M.44 + M.13*M.22*M.34*M.41 +
M.13*M.24*M.31*M.42 - M.13*M.24*M.32*M.41 -
M.14*M.21*M.32*M.43 + M.14*M.21*M.33*M.42 +
M.14*M.22*M.31*M.43 - M.14*M.22*M.33*M.41 -
M.14*M.23*M.31*M.42 + M.14*M.23*M.32*M.41)%A.
(M.11*M.22*M.33*M.44 - M.11*M.22*M.34*M.43 -
M.11*M.23*M.32*M.44 + M.11*M.23*M.34*M.42 +
M.11*M.24*M.32*M.43 - M.11*M.24*M.33*M.42 -
M.12*M.21*M.33*M.44 + M.12*M.21*M.34*M.43 +
M.12*M.23*M.31*M.44 - M.12*M.23*M.34*M.41 -
M.12*M.24*M.31*M.43 + M.12*M.24*M.33*M.41 +
M.13*M.21*M.32*M.44 - M.13*M.21*M.34*M.42 -
M.13*M.22*M.31*M.44 + M.13*M.22*M.34*M.41 +
M.13*M.24*M.31*M.42 - M.13*M.24*M.32*M.41 -
M.14*M.21*M.32*M.43 + M.14*M.21*M.33*M.42 +
M.14*M.22*M.31*M.43 - M.14*M.22*M.33*M.41 -
M.14*M.23*M.31*M.42 + M.14*M.23*M.32*M.41)%A.
mdet4 M = mdet M
Lemma mdet4_eq_mdet : forall M, mdet4 M = mdet M.
Proof. intros. unfold mdet4. cbn; rewrite <- !(nth_m2f_nat2finS 0); auto; ring. Qed.
Proof. intros. unfold mdet4. cbn; rewrite <- !(nth_m2f_nat2finS 0); auto; ring. Qed.
|M| <> 0 <-> mdet_exp <> 0
Lemma mdet4_neq0_iff : forall (M : smat A 4),
mdet M <> 0 <->
(M.11*M.22*M.33*M.44 - M.11*M.22*M.34*M.43 -
M.11*M.23*M.32*M.44 + M.11*M.23*M.34*M.42 +
M.11*M.24*M.32*M.43 - M.11*M.24*M.33*M.42 -
M.12*M.21*M.33*M.44 + M.12*M.21*M.34*M.43 +
M.12*M.23*M.31*M.44 - M.12*M.23*M.34*M.41 -
M.12*M.24*M.31*M.43 + M.12*M.24*M.33*M.41 +
M.13*M.21*M.32*M.44 - M.13*M.21*M.34*M.42 -
M.13*M.22*M.31*M.44 + M.13*M.22*M.34*M.41 +
M.13*M.24*M.31*M.42 - M.13*M.24*M.32*M.41 -
M.14*M.21*M.32*M.43 + M.14*M.21*M.33*M.42 +
M.14*M.22*M.31*M.43 - M.14*M.22*M.33*M.41 -
M.14*M.23*M.31*M.42 + M.14*M.23*M.32*M.41)%A <> 0.
Proof. intros. rewrite <- mdet4_eq_mdet. easy. Qed.
End mdet_concrete.
mdet M <> 0 <->
(M.11*M.22*M.33*M.44 - M.11*M.22*M.34*M.43 -
M.11*M.23*M.32*M.44 + M.11*M.23*M.34*M.42 +
M.11*M.24*M.32*M.43 - M.11*M.24*M.33*M.42 -
M.12*M.21*M.33*M.44 + M.12*M.21*M.34*M.43 +
M.12*M.23*M.31*M.44 - M.12*M.23*M.34*M.41 -
M.12*M.24*M.31*M.43 + M.12*M.24*M.33*M.41 +
M.13*M.21*M.32*M.44 - M.13*M.21*M.34*M.42 -
M.13*M.22*M.31*M.44 + M.13*M.22*M.34*M.41 +
M.13*M.24*M.31*M.42 - M.13*M.24*M.32*M.41 -
M.14*M.21*M.32*M.43 + M.14*M.21*M.33*M.42 +
M.14*M.22*M.31*M.43 - M.14*M.22*M.33*M.41 -
M.14*M.23*M.31*M.42 + M.14*M.23*M.32*M.41)%A <> 0.
Proof. intros. rewrite <- mdet4_eq_mdet. easy. Qed.
End mdet_concrete.
Section testZ.
Import ZArith.
Open Scope Z_scope.
Let mdet {n} (M : @smat Z n) : Z := @mdet _ Z.add 0 Z.opp Z.mul 1 n M.
Let ex_1_5 : mat Z 5 5 :=
l2m 0 [[0;0;0;1;0];[0;0;2;0;0];[0;3;8;0;0];[4;9;0;7;0];[6;0;0;0;5]].
Goal mdet ex_1_5 = 120. cbv. auto. Qed.
Let ex_2_1 : mat Z 3 3 := l2m 0 [[1;4;2];[3;5;1];[2;1;6]].
Goal mdet ex_2_1 = -49. cbv. auto. Qed.
End testZ.
Import ZArith.
Open Scope Z_scope.
Let mdet {n} (M : @smat Z n) : Z := @mdet _ Z.add 0 Z.opp Z.mul 1 n M.
Let ex_1_5 : mat Z 5 5 :=
l2m 0 [[0;0;0;1;0];[0;0;2;0;0];[0;3;8;0;0];[4;9;0;7;0];[6;0;0;0;5]].
Goal mdet ex_1_5 = 120. cbv. auto. Qed.
Let ex_2_1 : mat Z 3 3 := l2m 0 [[1;4;2];[3;5;1];[2;1;6]].
Goal mdet ex_2_1 = -49. cbv. auto. Qed.
End testZ.
Section testR.
Import Reals.
Open Scope R_scope.
Notation "0" := R0.
Notation "1" := R1.
Let mdet {n} (M : @smat R n) : R := @mdet _ Rplus 0 Ropp Rmult 1 n M.
Variable a11 a12 a13 a21 a22 a23 a31 a32 a33 : R.
Let ex_2_3 : mat R 3 3 := l2m 0 [[a11;a12;a13];[0;a22;a23];[0;0;a33]].
Goal mdet ex_2_3 = a11 * a22 * a33. cbv. lra. Qed.
Example eg_2_2_2_3 : forall a1 a2 a3 a4 a5 b1 b2 b3 b4 b5 c1 c2 d1 d2 e1 e2 : R,
mdet (@l2m _ 0 5 5
[[a1;a2;a3;a4;a5];
[b1;b2;b3;b4;b5];
[ 0; 0; 0;c1;c2];
[ 0; 0; 0;d1;d2];
[ 0; 0; 0;e1;e2]]) = 0.
Proof. intros. cbv. lra. Qed.
Example eg_2_2_2_4 : forall x:R,
mdet (@l2m _ 0 4 4
[[7*x;x;1;2*x];
[1;x;5;-1];
[4;3;x;1];
[2;-1;1;x]]) = 7*x^4 - 5*x^3 - 99*x^2 + 38*x + 11.
Proof. intros. cbv. lra. Qed.
End testR.
Import Reals.
Open Scope R_scope.
Notation "0" := R0.
Notation "1" := R1.
Let mdet {n} (M : @smat R n) : R := @mdet _ Rplus 0 Ropp Rmult 1 n M.
Variable a11 a12 a13 a21 a22 a23 a31 a32 a33 : R.
Let ex_2_3 : mat R 3 3 := l2m 0 [[a11;a12;a13];[0;a22;a23];[0;0;a33]].
Goal mdet ex_2_3 = a11 * a22 * a33. cbv. lra. Qed.
Example eg_2_2_2_3 : forall a1 a2 a3 a4 a5 b1 b2 b3 b4 b5 c1 c2 d1 d2 e1 e2 : R,
mdet (@l2m _ 0 5 5
[[a1;a2;a3;a4;a5];
[b1;b2;b3;b4;b5];
[ 0; 0; 0;c1;c2];
[ 0; 0; 0;d1;d2];
[ 0; 0; 0;e1;e2]]) = 0.
Proof. intros. cbv. lra. Qed.
Example eg_2_2_2_4 : forall x:R,
mdet (@l2m _ 0 4 4
[[7*x;x;1;2*x];
[1;x;5;-1];
[4;3;x;1];
[2;-1;1;x]]) = 7*x^4 - 5*x^3 - 99*x^2 + 38*x + 11.
Proof. intros. cbv. lra. Qed.
End testR.
Section mdetEx.
Context `{HARing : ARing}.
Add Ring ring_inst : (make_ring_theory HARing).
Notation "0" := Azero : A_scope.
Notation "1" := Aone : A_scope.
Infix "+" := Aadd : A_scope.
Infix "*" := Amul : A_scope.
Notation "- a" := (Aopp a) : A_scope.
Notation vsum := (@vsum _ Aadd 0).
Notation vdot := (@vdot _ Aadd 0 Amul).
Notation smat n := (smat A n).
Notation mat0 := (@mat0 _ 0).
Notation madd := (@madd _ Aadd).
Infix "+" := madd : mat_scope.
Notation mdet := (@mdet _ Aadd 0 Aopp Amul 1).
Notation "| M |" := (mdet M) : mat_scope.
Context `{HARing : ARing}.
Add Ring ring_inst : (make_ring_theory HARing).
Notation "0" := Azero : A_scope.
Notation "1" := Aone : A_scope.
Infix "+" := Aadd : A_scope.
Infix "*" := Amul : A_scope.
Notation "- a" := (Aopp a) : A_scope.
Notation vsum := (@vsum _ Aadd 0).
Notation vdot := (@vdot _ Aadd 0 Amul).
Notation smat n := (smat A n).
Notation mat0 := (@mat0 _ 0).
Notation madd := (@madd _ Aadd).
Infix "+" := madd : mat_scope.
Notation mdet := (@mdet _ Aadd 0 Aopp Amul 1).
Notation "| M |" := (mdet M) : mat_scope.
Definition msubmatNat (M : nat -> nat -> A) (i j : nat) : nat -> nat -> A :=
fun i0 j0 =>
M (if i0 ??< i then i0 else S i0) (if j0 ??< j then j0 else S j0).
sub-matrix of M by remove i-th row and j-th column
Definition msubmat' {n} (M : smat (S n)) (i j : 'I_(S n)) : smat n :=
fun i0 j0 =>
let i1 := if i0 ??< i then fSuccRange i0 else fSuccRangeS i0 in
let j1 := if j0 ??< j then fSuccRange j0 else fSuccRangeS j0 in
M.[i1].[j1].
Definition msubmat {n} (M : smat (S n)) (i j : 'I_(S n)) : smat n :=
fun i0 j0 =>
let i1 := if i0 ??< i then #i0 else #(S i0) in
let j1 := if j0 ??< j then #j0 else #(S j0) in
M.[i1].[j1].
msubmat (msetr M a j) i j = msubmat M i j
Lemma msubmat_msetr : forall {n} (M : smat (S n)) (a : vec (S n)) (i j : 'I_(S n)),
msubmat (msetr M a i) i j = msubmat M i j.
Proof. intros. apply meq_iff_mnth; intros. unfold msubmat. unfold msetr. fin. Qed.
msubmat (msetr M a i) i j = msubmat M i j.
Proof. intros. apply meq_iff_mnth; intros. unfold msubmat. unfold msetr. fin. Qed.
msubmat (msetc M a j) i j = msubmat M i j
Lemma msubmat_msetc : forall {n} (M : smat (S n)) (a : vec (S n)) (i j : 'I_(S n)),
msubmat (msetc M a j) i j = msubmat M i j.
Proof. intros. apply meq_iff_mnth; intros. unfold msubmat. unfold msetc. fin. Qed.
Lemma msubmat_eq_msubmatNat : forall {n} (M : smat (S n)) (i j : 'I_(S n)),
msubmat M i j = @f2m _ n n (msubmatNat (m2f 0 M) i j).
Proof.
intros. unfold msubmat, msubmatNat. apply meq_iff_mnth; intros.
rewrite mnth_f2m.
destruct i0,j0,i,j; simpl.
assert ((if i0 ??< i then i0 else S i0) < S n) as Hi.
{ destruct (_??<_). lia. lia. }
assert ((if i1 ??< i2 then i1 else S i1) < S n) as Hj.
{ destruct (i1 ??< i2). lia. lia. }
rewrite nth_m2f with (Hi:=Hi)(Hj:=Hj). f_equal.
- assert (i0 < S n) by lia. rewrite nat2finS_eq with (E:=H).
assert (S i0 < S n) by lia. rewrite nat2finS_eq with (E:=H0). fin.
- assert (i1 < S n) by lia. rewrite nat2finS_eq with (E:=H).
assert (S i1 < S n) by lia. rewrite nat2finS_eq with (E:=H0). fin.
Qed.
msubmat (msetc M a j) i j = msubmat M i j.
Proof. intros. apply meq_iff_mnth; intros. unfold msubmat. unfold msetc. fin. Qed.
Lemma msubmat_eq_msubmatNat : forall {n} (M : smat (S n)) (i j : 'I_(S n)),
msubmat M i j = @f2m _ n n (msubmatNat (m2f 0 M) i j).
Proof.
intros. unfold msubmat, msubmatNat. apply meq_iff_mnth; intros.
rewrite mnth_f2m.
destruct i0,j0,i,j; simpl.
assert ((if i0 ??< i then i0 else S i0) < S n) as Hi.
{ destruct (_??<_). lia. lia. }
assert ((if i1 ??< i2 then i1 else S i1) < S n) as Hj.
{ destruct (i1 ??< i2). lia. lia. }
rewrite nth_m2f with (Hi:=Hi)(Hj:=Hj). f_equal.
- assert (i0 < S n) by lia. rewrite nat2finS_eq with (E:=H).
assert (S i0 < S n) by lia. rewrite nat2finS_eq with (E:=H0). fin.
- assert (i1 < S n) by lia. rewrite nat2finS_eq with (E:=H).
assert (S i1 < S n) by lia. rewrite nat2finS_eq with (E:=H0). fin.
Qed.
minor(M\T,i,j) = minor(M,j,i)
Lemma mminor_mtrans : forall {n} (M : smat (S n)) (i j : 'I_(S n)),
mminor (M\T) i j = mminor M j i.
Proof. intros. unfold mminor. rewrite <- mdet_mtrans. auto. Qed.
mminor (M\T) i j = mminor M j i.
Proof. intros. unfold mminor. rewrite <- mdet_mtrans. auto. Qed.
mminor (msetr M a i) i j = mminor M i j
Lemma mminor_msetr : forall {n} (M : smat (S n)) (a : vec (S n)) (i j : 'I_(S n)),
mminor (msetr M a i) i j = mminor M i j.
Proof. intros. unfold mminor. rewrite msubmat_msetr. auto. Qed.
mminor (msetr M a i) i j = mminor M i j.
Proof. intros. unfold mminor. rewrite msubmat_msetr. auto. Qed.
mminor (msetc M a j) i j = mminor M i j
Lemma mminor_msetc : forall {n} (M : smat (S n)) (a : vec (S n)) (i j : 'I_(S n)),
mminor (msetc M a j) i j = mminor M i j.
Proof. intros. unfold mminor. rewrite msubmat_msetc. auto. Qed.
Definition mminorNat {n:nat} (M : nat -> nat -> A) (i j : nat) : A :=
mdet (@f2m _ n n (msubmatNat M i j)).
Lemma mminor_eq_mminorNat : forall {n} (M : smat (S n)) (i j : 'I_(S n)),
mminor M i j = @mminorNat n (m2f 0 M) i j.
Proof.
intros. unfold mminor, mminorNat. rewrite msubmat_eq_msubmatNat. auto.
Qed.
mminor (msetc M a j) i j = mminor M i j.
Proof. intros. unfold mminor. rewrite msubmat_msetc. auto. Qed.
Definition mminorNat {n:nat} (M : nat -> nat -> A) (i j : nat) : A :=
mdet (@f2m _ n n (msubmatNat M i j)).
Lemma mminor_eq_mminorNat : forall {n} (M : smat (S n)) (i j : 'I_(S n)),
mminor M i j = @mminorNat n (m2f 0 M) i j.
Proof.
intros. unfold mminor, mminorNat. rewrite msubmat_eq_msubmatNat. auto.
Qed.
Definition mcofactor {n} (M : smat (S n)) (i j : 'I_(S n)) : A :=
let x := mminor M i j in
if Nat.even (i + j) then x else - x.
let x := mminor M i j in
if Nat.even (i + j) then x else - x.
A(M\T,i,j) = A(M,j,i)
Lemma mcofactor_mtrans : forall {n} (M : smat (S n)) (i j : 'I_(S n)),
mcofactor (M\T) i j = mcofactor M j i.
Proof.
intros. unfold mcofactor. rewrite mminor_mtrans. rewrite Nat.add_comm. auto.
Qed.
mcofactor (M\T) i j = mcofactor M j i.
Proof.
intros. unfold mcofactor. rewrite mminor_mtrans. rewrite Nat.add_comm. auto.
Qed.
mcofactor (msetr M a i) i j = mcofactor M i j
Lemma mcofactor_msetr : forall {n} (M : smat (S n)) (a : vec (S n)) (i j : 'I_(S n)),
mcofactor (msetr M a i) i j = mcofactor M i j.
Proof. intros. unfold mcofactor. rewrite mminor_msetr. auto. Qed.
mcofactor (msetr M a i) i j = mcofactor M i j.
Proof. intros. unfold mcofactor. rewrite mminor_msetr. auto. Qed.
mcofactor (msetc M a j) i j = mcofactor M i j
Lemma mcofactor_msetc : forall {n} (M : smat (S n)) (a : vec (S n)) (i j : 'I_(S n)),
mcofactor (msetc M a j) i j = mcofactor M i j.
Proof. intros. unfold mcofactor. rewrite mminor_msetc. auto. Qed.
mcofactor (msetc M a j) i j = mcofactor M i j.
Proof. intros. unfold mcofactor. rewrite mminor_msetc. auto. Qed.
Cofactor expansion of the determinant (Laplace expansion)
Definition mdetExRow {n} : smat n -> 'I_n -> A :=
match n with
| O => fun _ _ => 1
| S n' => fun M i => vsum (fun j => M.[i].[j] * mcofactor M i j)
end.
match n with
| O => fun _ _ => 1
| S n' => fun M i => vsum (fun j => M.[i].[j] * mcofactor M i j)
end.
Cofactor expansion of `M` along the j-th column
Definition mdetExCol {n} : smat n -> 'I_n -> A :=
match n with
| O => fun _ _ => 1
| S n' => fun M j => vsum (fun i => M.[i].[j] * mcofactor M i j)
end.
match n with
| O => fun _ _ => 1
| S n' => fun M j => vsum (fun i => M.[i].[j] * mcofactor M i j)
end.
row_expansion (M\T, i) = col_expansion (M, i)
Lemma mdetExRow_mtrans : forall {n} (M : smat n) (i : 'I_n),
mdetExRow (M \T) i = mdetExCol M i.
Proof.
intros. unfold mdetExRow, mdetExCol. destruct n; auto.
apply vsum_eq; intros. rewrite mcofactor_mtrans, mnth_mtrans. auto.
Qed.
mdetExRow (M \T) i = mdetExCol M i.
Proof.
intros. unfold mdetExRow, mdetExCol. destruct n; auto.
apply vsum_eq; intros. rewrite mcofactor_mtrans, mnth_mtrans. auto.
Qed.
col_expansion (M\T, i) = row_expansion (M, i)
Lemma mdetExCol_mtrans : forall {n} (M : smat n) (i : 'I_n),
mdetExCol (M \T) i = mdetExRow M i.
Proof. intros. rewrite <- mdetExRow_mtrans. auto. Qed.
mdetExCol (M \T) i = mdetExRow M i.
Proof. intros. rewrite <- mdetExRow_mtrans. auto. Qed.
Cofactor expansion by row is equivalent to full expansion
Theorem mdetExRow_eq_mdet : forall {n} (M : smat n) (i : 'I_n), mdetExRow M i = mdet M.
Proof.
intros. destruct n. cbv; ring.
unfold mdetExRow, mdet in *.
Admitted.
Proof.
intros. destruct n. cbv; ring.
unfold mdetExRow, mdet in *.
Admitted.
Cofactor expansion by column is equivalent to full expansion
Theorem mdetExCol_eq_mdet : forall {n} (M : smat n) (j : 'I_n), mdetExCol M j = mdet M.
Proof.
intros.
pose proof(mdetExRow_eq_mdet (M\T) j).
rewrite mdet_mtrans in H. rewrite <- H.
rewrite mdetExRow_mtrans. auto.
Qed.
Proof.
intros.
pose proof(mdetExRow_eq_mdet (M\T) j).
rewrite mdet_mtrans in H. rewrite <- H.
rewrite mdetExRow_mtrans. auto.
Qed.
Cofactor expansion by row is equivalent to cofactor expansion by column
Theorem mdetExRow_eq_mdetExCol : forall {n} (M : smat n) (i : 'I_n),
mdetExRow M i = mdetExCol M i.
Proof. intros. rewrite mdetExRow_eq_mdet, mdetExCol_eq_mdet. auto. Qed.
Section Field.
Context `{HField: Field A Aadd Azero Aopp Amul Aone}.
Context {AeqDec: Dec (@eq A)}.
mdetExRow M i = mdetExCol M i.
Proof. intros. rewrite mdetExRow_eq_mdet, mdetExCol_eq_mdet. auto. Qed.
Section Field.
Context `{HField: Field A Aadd Azero Aopp Amul Aone}.
Context {AeqDec: Dec (@eq A)}.
< i-th row, cofactor of k-th row > = 0 (if i <> k)
Theorem vdot_mcofactor_row_diff_eq0 : forall {n} (M : smat (S n)) (i k : 'I_(S n)),
i <> k -> vdot (M.[i]) (fun j => mcofactor M k j) = 0.
Proof.
intros.
pose (msetr M (M.[i]) k) as B.
pose proof (mdetExRow_eq_mdet B k).
assert (mdetExRow B k = vdot M.[i] (fun j => mcofactor M k j)).
- unfold mdetExRow. unfold vdot.
apply vsum_eq; intros.
rewrite vnth_vmap2. unfold B.
rewrite mnth_msetr_same; auto. f_equal.
unfold mcofactor.
destruct (Nat.even (k + i0)) eqn:H1.
+ unfold mminor. f_equal. apply meq_iff_mnth; intros.
unfold msubmat. unfold msetr. fin.
+ f_equal. unfold mminor. f_equal. apply meq_iff_mnth; intros.
unfold msubmat. unfold msetr. fin.
- rewrite <- H1. unfold B.
rewrite mdetExRow_eq_mdet.
apply (mdet_row_same_eq0 _ i k); auto.
apply veq_iff_vnth; intros.
rewrite mnth_msetr_diff; auto.
rewrite mnth_msetr_same; auto.
Qed.
i <> k -> vdot (M.[i]) (fun j => mcofactor M k j) = 0.
Proof.
intros.
pose (msetr M (M.[i]) k) as B.
pose proof (mdetExRow_eq_mdet B k).
assert (mdetExRow B k = vdot M.[i] (fun j => mcofactor M k j)).
- unfold mdetExRow. unfold vdot.
apply vsum_eq; intros.
rewrite vnth_vmap2. unfold B.
rewrite mnth_msetr_same; auto. f_equal.
unfold mcofactor.
destruct (Nat.even (k + i0)) eqn:H1.
+ unfold mminor. f_equal. apply meq_iff_mnth; intros.
unfold msubmat. unfold msetr. fin.
+ f_equal. unfold mminor. f_equal. apply meq_iff_mnth; intros.
unfold msubmat. unfold msetr. fin.
- rewrite <- H1. unfold B.
rewrite mdetExRow_eq_mdet.
apply (mdet_row_same_eq0 _ i k); auto.
apply veq_iff_vnth; intros.
rewrite mnth_msetr_diff; auto.
rewrite mnth_msetr_same; auto.
Qed.
< j-th column, cofactor of l-column row > = 0 (if j <> l)
Theorem vdot_mcofactor_col_diff_eq0 : forall {n} (M : smat (S n)) (j l : 'I_(S n)),
j <> l -> vdot (M&[j]) (fun i => mcofactor M i l) = 0.
Proof.
intros. pose proof (vdot_mcofactor_row_diff_eq0 (M\T) j l H).
rewrite <- H0 at 2. f_equal. apply veq_iff_vnth; intros.
rewrite mcofactor_mtrans. auto.
Qed.
End Field.
j <> l -> vdot (M&[j]) (fun i => mcofactor M i l) = 0.
Proof.
intros. pose proof (vdot_mcofactor_row_diff_eq0 (M\T) j l H).
rewrite <- H0 at 2. f_equal. apply veq_iff_vnth; intros.
rewrite mcofactor_mtrans. auto.
Qed.
End Field.
< i-th row, cofactor of i-th row > = |M|
Lemma vdot_mcofactor_row_same_eq_det : forall {n} (M : smat (S n)) (i : 'I_(S n)),
vdot (M.[i]) (fun j => mcofactor M i j) = |M|.
Proof. intros. rewrite <- mdetExRow_eq_mdet with (i:=i). auto. Qed.
vdot (M.[i]) (fun j => mcofactor M i j) = |M|.
Proof. intros. rewrite <- mdetExRow_eq_mdet with (i:=i). auto. Qed.
< j-th column, cofactor of j-th column > = |M|
Lemma vdot_mcofactor_col_same_eq_det : forall {n} (M : smat (S n)) (j : 'I_(S n)),
vdot (M&[j]) (fun i => mcofactor M i j) = |M|.
Proof. intros. rewrite <- mdetExCol_eq_mdet with (j:=j). auto. Qed.
Section example1.
Let n := 7.
Variable a b : A.
Let M1 : smat (S n) := mdiagMk 0 (vrepeat a).
Let M2 : smat (S n) := mclsr (mdiagMk 0 (vrepeat b)) #1.
Let M := M1 + M2.
Fixpoint ApowNat (a : A) (n : nat) : A :=
match n with
| O => Aone
| S n' => a * ApowNat a n'
end.
Example mdet_example1 :
|M| = (ApowNat a (S n) + (if odd (S (S n)) then -b*b else b*b))%A.
Proof.
rewrite <- (mdetExCol_eq_mdet) with (j:=#0).
unfold M,M1,M2.
simpl.
Abort.
End example1.
Section example2.
End example2.
vdot (M&[j]) (fun i => mcofactor M i j) = |M|.
Proof. intros. rewrite <- mdetExCol_eq_mdet with (j:=j). auto. Qed.
Section example1.
Let n := 7.
Variable a b : A.
Let M1 : smat (S n) := mdiagMk 0 (vrepeat a).
Let M2 : smat (S n) := mclsr (mdiagMk 0 (vrepeat b)) #1.
Let M := M1 + M2.
Fixpoint ApowNat (a : A) (n : nat) : A :=
match n with
| O => Aone
| S n' => a * ApowNat a n'
end.
Example mdet_example1 :
|M| = (ApowNat a (S n) + (if odd (S (S n)) then -b*b else b*b))%A.
Proof.
rewrite <- (mdetExCol_eq_mdet) with (j:=#0).
unfold M,M1,M2.
simpl.
Abort.
End example1.
Section example2.
End example2.
Cofactor expansion of `M` along the 0-th row
Fixpoint mdetEx {n} : smat n -> A :=
match n with
| O => fun M => 1
| S n' =>
fun M =>
vsum (fun j =>
let a := if Nat.even j
then (M.[#0].[j])
else (-(M.[#0].[j]))%A in
let d := mdetEx (msubmat M #0 j) in
a * d)
end.
match n with
| O => fun M => 1
| S n' =>
fun M =>
vsum (fun j =>
let a := if Nat.even j
then (M.[#0].[j])
else (-(M.[#0].[j]))%A in
let d := mdetEx (msubmat M #0 j) in
a * d)
end.
mdetEx is equal to mdetExRow along 0-th row
Lemma mdetEx_eq_mdetExRow_0 : forall {n} (M : smat (S n)),
mdetEx M = mdetExRow M #0.
Proof.
induction n; intros.
- cbv. rewrite <- (nth_m2f 0). ring.
- unfold mdetEx, mdetExRow; fold (@mdetEx n).
apply vsum_eq; intros.
specialize (IHn (msubmat M #0 i)) as H.
unfold mdetEx, mdetExRow in H; fold (@mdetEx n) in H. rewrite H; clear H.
destruct (Nat.even i) eqn:H1.
+ f_equal.
unfold mcofactor; simpl. rewrite H1. unfold mminor at 3.
rewrite <- (mdetExRow_eq_mdet _ #0).
unfold mdetExRow. apply vsum_eq; intros. auto.
+ unfold mcofactor; simpl. rewrite H1. ring_simplify. f_equal.
unfold mminor at 3.
rewrite <- (mdetExRow_eq_mdet _ #0).
unfold mdetExRow. apply vsum_eq; intros. auto.
Qed.
mdetEx M = mdetExRow M #0.
Proof.
induction n; intros.
- cbv. rewrite <- (nth_m2f 0). ring.
- unfold mdetEx, mdetExRow; fold (@mdetEx n).
apply vsum_eq; intros.
specialize (IHn (msubmat M #0 i)) as H.
unfold mdetEx, mdetExRow in H; fold (@mdetEx n) in H. rewrite H; clear H.
destruct (Nat.even i) eqn:H1.
+ f_equal.
unfold mcofactor; simpl. rewrite H1. unfold mminor at 3.
rewrite <- (mdetExRow_eq_mdet _ #0).
unfold mdetExRow. apply vsum_eq; intros. auto.
+ unfold mcofactor; simpl. rewrite H1. ring_simplify. f_equal.
unfold mminor at 3.
rewrite <- (mdetExRow_eq_mdet _ #0).
unfold mdetExRow. apply vsum_eq; intros. auto.
Qed.
mdetEx is equal to mdet
Theorem mdetEx_eq_mdet : forall {n} (M : smat n), mdetEx M = mdet M.
Proof.
intros. destruct n.
- cbv. ring.
- rewrite mdetEx_eq_mdetExRow_0. rewrite mdetExRow_eq_mdet. auto.
Qed.
Ltac mdetEx_eq_mdet :=
match goal with
| |- mdetEx ?M = mdet ?M =>
let HeqM := fresh "HeqM" in
remember (mdet M) eqn: HeqM; cbv; rewrite <- !(nth_m2f 0);
rewrite HeqM; unfold mdet; simpl;
try ring
end.
Example mdetEx_eq_mdet_1 : forall (M : smat 1), mdetEx M = mdet M.
Proof. intros. mdetEx_eq_mdet. Qed.
Example mdetEx_eq_mdet_2 : forall (M : smat 2), mdetEx M = mdet M.
Proof. intros. mdetEx_eq_mdet. Qed.
Example mdetEx_eq_mdet_3 : forall (M : smat 3), mdetEx M = mdet M.
Proof. intros. mdetEx_eq_mdet. Qed.
Example mdetEx_eq_mdet_4 : forall (M : smat 4), mdetEx M = mdet M.
Proof.
intros.
mdetEx_eq_mdet.
Qed.
Proof.
intros. destruct n.
- cbv. ring.
- rewrite mdetEx_eq_mdetExRow_0. rewrite mdetExRow_eq_mdet. auto.
Qed.
Ltac mdetEx_eq_mdet :=
match goal with
| |- mdetEx ?M = mdet ?M =>
let HeqM := fresh "HeqM" in
remember (mdet M) eqn: HeqM; cbv; rewrite <- !(nth_m2f 0);
rewrite HeqM; unfold mdet; simpl;
try ring
end.
Example mdetEx_eq_mdet_1 : forall (M : smat 1), mdetEx M = mdet M.
Proof. intros. mdetEx_eq_mdet. Qed.
Example mdetEx_eq_mdet_2 : forall (M : smat 2), mdetEx M = mdet M.
Proof. intros. mdetEx_eq_mdet. Qed.
Example mdetEx_eq_mdet_3 : forall (M : smat 3), mdetEx M = mdet M.
Proof. intros. mdetEx_eq_mdet. Qed.
Example mdetEx_eq_mdet_4 : forall (M : smat 4), mdetEx M = mdet M.
Proof.
intros.
mdetEx_eq_mdet.
Qed.
cofactor of matrix (Expansion version) 代数余子式(行列式为展开形式的版本)
Definition mcofactorEx {n} (M : smat (S n)) (i j : 'I_(S n)) : A :=
let x := mdetEx (msubmat M i j) in
if Nat.even (i + j) then x else - x.
let x := mdetEx (msubmat M i j) in
if Nat.even (i + j) then x else - x.
mcofactorEx is equal to mcofactor
Lemma mcofactorEx_eq_mcofactor : forall {n} (M : smat (S n)) (i j : 'I_(S n)),
mcofactorEx M i j = mcofactor M i j.
Proof.
intros. unfold mcofactorEx, mcofactor. unfold mminor.
rewrite <- mdetEx_eq_mdet. auto.
Qed.
End mdetEx.
mcofactorEx M i j = mcofactor M i j.
Proof.
intros. unfold mcofactorEx, mcofactor. unfold mminor.
rewrite <- mdetEx_eq_mdet. auto.
Qed.
End mdetEx.
Section madj.
Context `{HField : Field} {HAeqDec : Dec (@eq A)}.
Add Field field_thy_inst : (make_field_theory HField).
Open Scope A_scope.
Open Scope mat_scope.
Notation "0" := Azero : A_scope.
Notation "1" := Aone : A_scope.
Infix "+" := Aadd : A_scope.
Notation "- a" := (Aopp a) : A_scope.
Notation "a - b" := ((a + -b)%A) : A_scope.
Infix "*" := Amul : A_scope.
Notation "/ a" := (Ainv a) : A_scope.
Notation "a / b" := ((a * /b)%A) : A_scope.
Notation vsum := (@vsum _ Aadd 0).
Notation smat n := (smat A n).
Notation mat1 := (@mat1 _ 0 1).
Notation mcmul := (@mcmul _ Amul).
Infix "c*" := mcmul : mat_scope.
Notation mmul := (@mmul _ Aadd 0 Amul).
Infix "*" := mmul : mat_scope.
Notation mmulv := (@mmulv _ Aadd 0 Amul).
Infix "*v" := mmulv : mat_scope.
Notation mdet := (@mdet _ Aadd 0 Aopp Amul 1).
Notation "| M |" := (mdet M) : mat_scope.
Notation mdetEx := (@mdetEx _ Aadd 0 Aopp Amul 1).
Notation mcofactor := (@mcofactor _ Aadd 0 Aopp Amul 1).
Notation mcofactorEx := (@mcofactorEx _ Aadd 0 Aopp Amul 1).
Context `{HField : Field} {HAeqDec : Dec (@eq A)}.
Add Field field_thy_inst : (make_field_theory HField).
Open Scope A_scope.
Open Scope mat_scope.
Notation "0" := Azero : A_scope.
Notation "1" := Aone : A_scope.
Infix "+" := Aadd : A_scope.
Notation "- a" := (Aopp a) : A_scope.
Notation "a - b" := ((a + -b)%A) : A_scope.
Infix "*" := Amul : A_scope.
Notation "/ a" := (Ainv a) : A_scope.
Notation "a / b" := ((a * /b)%A) : A_scope.
Notation vsum := (@vsum _ Aadd 0).
Notation smat n := (smat A n).
Notation mat1 := (@mat1 _ 0 1).
Notation mcmul := (@mcmul _ Amul).
Infix "c*" := mcmul : mat_scope.
Notation mmul := (@mmul _ Aadd 0 Amul).
Infix "*" := mmul : mat_scope.
Notation mmulv := (@mmulv _ Aadd 0 Amul).
Infix "*v" := mmulv : mat_scope.
Notation mdet := (@mdet _ Aadd 0 Aopp Amul 1).
Notation "| M |" := (mdet M) : mat_scope.
Notation mdetEx := (@mdetEx _ Aadd 0 Aopp Amul 1).
Notation mcofactor := (@mcofactor _ Aadd 0 Aopp Amul 1).
Notation mcofactorEx := (@mcofactorEx _ Aadd 0 Aopp Amul 1).
Definition madj {n} : smat n -> smat n :=
match n with
| O => fun M => M
| S n' => fun M i j => mcofactorEx M j i
end.
Notation "M \A" := (madj M) : mat_scope.
match n with
| O => fun M => M
| S n' => fun M i j => mcofactorEx M j i
end.
Notation "M \A" := (madj M) : mat_scope.
M * (M\A) = |M| * I
Lemma mmul_madj_r : forall {n} (M : smat n), M * M\A = |M| c* mat1.
Proof.
intros. apply meq_iff_mnth; intros.
unfold madj. destruct n. fin.
rewrite mnth_mmul. unfold mcol.
replace (fun i0 => mcofactorEx M j i0) with (fun i0 => mcofactor M j i0).
2:{ extensionality i0. rewrite mcofactorEx_eq_mcofactor. auto. }
destruct (i ??= j) as [E|E].
- fin2nat. subst.
rewrite vdot_mcofactor_row_same_eq_det.
rewrite mnth_mcmul. rewrite mnth_mat1_same; auto. ring.
- fin2nat.
rewrite (vdot_mcofactor_row_diff_eq0 M i j); auto.
rewrite mnth_mcmul. rewrite mnth_mat1_diff; auto. ring.
Qed.
Proof.
intros. apply meq_iff_mnth; intros.
unfold madj. destruct n. fin.
rewrite mnth_mmul. unfold mcol.
replace (fun i0 => mcofactorEx M j i0) with (fun i0 => mcofactor M j i0).
2:{ extensionality i0. rewrite mcofactorEx_eq_mcofactor. auto. }
destruct (i ??= j) as [E|E].
- fin2nat. subst.
rewrite vdot_mcofactor_row_same_eq_det.
rewrite mnth_mcmul. rewrite mnth_mat1_same; auto. ring.
- fin2nat.
rewrite (vdot_mcofactor_row_diff_eq0 M i j); auto.
rewrite mnth_mcmul. rewrite mnth_mat1_diff; auto. ring.
Qed.
(M\A) * M = |M| * I
Lemma mmul_madj_l : forall {n} (M : smat n), M\A * M = |M| c* mat1.
Proof.
intros. apply meq_iff_mnth; intros.
unfold madj. destruct n. fin.
rewrite mnth_mmul. rewrite vdot_comm.
replace (fun j0 => mcofactorEx M j0 i) with (fun j0 => mcofactor M j0 i).
2:{ extensionality j0. rewrite mcofactorEx_eq_mcofactor. auto. }
destruct (i ??= j) as [E|E].
- fin2nat. subst.
rewrite vdot_mcofactor_col_same_eq_det.
rewrite mnth_mcmul. rewrite mnth_mat1_same; auto. ring.
- fin2nat.
rewrite (vdot_mcofactor_col_diff_eq0 M j i); auto.
rewrite mnth_mcmul. rewrite mnth_mat1_diff; auto. ring.
Qed.
Proof.
intros. apply meq_iff_mnth; intros.
unfold madj. destruct n. fin.
rewrite mnth_mmul. rewrite vdot_comm.
replace (fun j0 => mcofactorEx M j0 i) with (fun j0 => mcofactor M j0 i).
2:{ extensionality j0. rewrite mcofactorEx_eq_mcofactor. auto. }
destruct (i ??= j) as [E|E].
- fin2nat. subst.
rewrite vdot_mcofactor_col_same_eq_det.
rewrite mnth_mcmul. rewrite mnth_mat1_same; auto. ring.
- fin2nat.
rewrite (vdot_mcofactor_col_diff_eq0 M j i); auto.
rewrite mnth_mcmul. rewrite mnth_mat1_diff; auto. ring.
Qed.
(/|M| .* M\A) * M = mat1
Lemma mmul_det_cmul_adj_l : forall {n} (M : smat n),
|M| <> 0 -> (/|M| c* M\A) * M = mat1.
Proof.
intros. rewrite mmul_mcmul_l. rewrite mmul_madj_l. rewrite mcmul_assoc.
rewrite field_mulInvL; auto. apply mcmul_1_l.
Qed.
|M| <> 0 -> (/|M| c* M\A) * M = mat1.
Proof.
intros. rewrite mmul_mcmul_l. rewrite mmul_madj_l. rewrite mcmul_assoc.
rewrite field_mulInvL; auto. apply mcmul_1_l.
Qed.
M * (/|M| .* M\A) = mat1
Lemma mmul_det_cmul_adj_r : forall {n} (M : smat n),
|M| <> 0 -> M * (/|M| c* M\A) = mat1.
Proof.
intros. rewrite mmul_mcmul_r. rewrite mmul_madj_r. rewrite mcmul_assoc.
rewrite field_mulInvL; auto. apply mcmul_1_l.
Qed.
|M| <> 0 -> M * (/|M| c* M\A) = mat1.
Proof.
intros. rewrite mmul_mcmul_r. rewrite mmul_madj_r. rewrite mcmul_assoc.
rewrite field_mulInvL; auto. apply mcmul_1_l.
Qed.
|M| <> 0 -> (exists N : smat n, N * M = mat1)
Lemma mdet_neq0_imply_mmul_eq1_l : forall {n} (M : smat n),
|M| <> 0 -> (exists N : smat n, N * M = mat1).
Proof. intros. exists (/|M| c* M\A). apply mmul_det_cmul_adj_l. auto. Qed.
|M| <> 0 -> (exists N : smat n, N * M = mat1).
Proof. intros. exists (/|M| c* M\A). apply mmul_det_cmul_adj_l. auto. Qed.
|M| <> 0 -> (exists N : smat n, M * N = mat1)
Lemma mdet_neq0_imply_mmul_eq1_r : forall {n} (M : smat n),
|M| <> 0 -> (exists N : smat n, M * N = mat1).
Proof. intros. exists (/|M| c* M\A). apply mmul_det_cmul_adj_r. auto. Qed.
|M| <> 0 -> (exists N : smat n, M * N = mat1).
Proof. intros. exists (/|M| c* M\A). apply mmul_det_cmul_adj_r. auto. Qed.
|M| <> 0 -> (exists N : smat n, N * M = mat1 /\ M * N = mat1)
Lemma mdet_neq0_imply_mmul_eq1 : forall {n} (M : smat n),
|M| <> 0 -> (exists N : smat n, N * M = mat1 /\ M * N = mat1).
Proof.
intros. exists (/|M| c* M\A). split.
apply mmul_det_cmul_adj_l. auto.
apply mmul_det_cmul_adj_r. auto.
Qed.
|M| <> 0 -> (exists N : smat n, N * M = mat1 /\ M * N = mat1).
Proof.
intros. exists (/|M| c* M\A). split.
apply mmul_det_cmul_adj_l. auto.
apply mmul_det_cmul_adj_r. auto.
Qed.
Cramer rule
Definition cramerRule {n} (B : smat n) (c : @vec A n) : @vec A n :=
fun i => mdetEx (msetc B c i) / (mdetEx B).
fun i => mdetEx (msetc B c i) / (mdetEx B).
B *v (cramerRule B c) = c, (The dimension is `S n`)
Lemma cramerRule_eq_S : forall {n} (B : smat (S n)) (c : @vec A (S n)),
|B| <> 0 -> B *v (cramerRule B c) = c.
Proof.
intros. unfold cramerRule. rewrite !mdetEx_eq_mdet.
remember (msetc B c) as C. apply veq_iff_vnth; intros.
rewrite vnth_mmulv. unfold vdot. unfold vmap2.
rewrite vsum_eq with (b:=fun j => (/|B| * (B.[i].[j] * |C j|))%A).
2:{ intros. rewrite !mdetEx_eq_mdet. field. auto. }
rewrite <- vsum_cmul_l.
rewrite vsum_eq
with (b:=fun j => (vsum (fun k => B.[i].[j] * (c.[k] * mcofactor B k j)))%A).
2:{ intros j. rewrite <- vsum_cmul_l. f_equal.
rewrite <- (mdetExCol_eq_mdet _ j). unfold mdetExCol.
apply vsum_eq; intros k. rewrite HeqC.
rewrite mnth_msetc_same; auto. f_equal.
rewrite mcofactor_msetc. auto. }
rewrite vsum_eq
with (b:=fun j=> vsum (fun k=> (B.[i].[j] * c.[k] * mcofactor B k j)%A)).
2:{ intros j. apply vsum_eq; intros k. ring. }
rewrite vsum_vsum.
rewrite vsum_eq
with (b:=fun k=> (c.[k] * vsum (fun j=> B.[i].[j] * mcofactor B k j))%A).
2:{ intros j. rewrite vsum_cmul_l. apply vsum_eq; intros k. ring. }
rewrite vsum_unique with (i:=i) (x:=(|B| * c.[i])%A).
- field; auto.
- pose proof (vdot_mcofactor_row_same_eq_det B i).
unfold vdot in H0. unfold vmap2 in H0. rewrite H0. ring.
- intros.
pose proof (vdot_mcofactor_row_diff_eq0 B i j H0).
unfold vdot in H1. unfold vmap2 in H1. rewrite H1. ring.
Qed.
|B| <> 0 -> B *v (cramerRule B c) = c.
Proof.
intros. unfold cramerRule. rewrite !mdetEx_eq_mdet.
remember (msetc B c) as C. apply veq_iff_vnth; intros.
rewrite vnth_mmulv. unfold vdot. unfold vmap2.
rewrite vsum_eq with (b:=fun j => (/|B| * (B.[i].[j] * |C j|))%A).
2:{ intros. rewrite !mdetEx_eq_mdet. field. auto. }
rewrite <- vsum_cmul_l.
rewrite vsum_eq
with (b:=fun j => (vsum (fun k => B.[i].[j] * (c.[k] * mcofactor B k j)))%A).
2:{ intros j. rewrite <- vsum_cmul_l. f_equal.
rewrite <- (mdetExCol_eq_mdet _ j). unfold mdetExCol.
apply vsum_eq; intros k. rewrite HeqC.
rewrite mnth_msetc_same; auto. f_equal.
rewrite mcofactor_msetc. auto. }
rewrite vsum_eq
with (b:=fun j=> vsum (fun k=> (B.[i].[j] * c.[k] * mcofactor B k j)%A)).
2:{ intros j. apply vsum_eq; intros k. ring. }
rewrite vsum_vsum.
rewrite vsum_eq
with (b:=fun k=> (c.[k] * vsum (fun j=> B.[i].[j] * mcofactor B k j))%A).
2:{ intros j. rewrite vsum_cmul_l. apply vsum_eq; intros k. ring. }
rewrite vsum_unique with (i:=i) (x:=(|B| * c.[i])%A).
- field; auto.
- pose proof (vdot_mcofactor_row_same_eq_det B i).
unfold vdot in H0. unfold vmap2 in H0. rewrite H0. ring.
- intros.
pose proof (vdot_mcofactor_row_diff_eq0 B i j H0).
unfold vdot in H1. unfold vmap2 in H1. rewrite H1. ring.
Qed.
B *v (cramerRule B c) = c
Theorem cramerRule_spec : forall {n} (B : smat n) (c : @vec A n),
|B| <> 0 -> B *v (cramerRule B c) = c.
Proof.
intros. destruct n.
- cbv. apply v0eq.
- apply cramerRule_eq_S. auto.
Qed.
|B| <> 0 -> B *v (cramerRule B c) = c.
Proof.
intros. destruct n.
- cbv. apply v0eq.
- apply cramerRule_eq_S. auto.
Qed.
Cramer rule over list
Definition cramerRuleList (n : nat) (lB : dlist A) (lc : list A) : list A :=
let B : smat n := l2m 0 lB in
let c : vec n := l2v 0 lc in
let x := cramerRule B c in
v2l x.
let B : smat n := l2m 0 lB in
let c : vec n := l2v 0 lc in
let x := cramerRule B c in
v2l x.
{cramerRuleList lB lc} = cramerRule {lB} {lc}
Theorem cramerRuleList_spec : forall n (lB : dlist A) (lc : list A),
let B : smat n := l2m 0 lB in
let c : vec n := l2v 0 lc in
l2v 0 (cramerRuleList n lB lc) = cramerRule B c.
Proof. intros. unfold cramerRuleList. rewrite l2v_v2l. auto. Qed.
End madj.
Section test.
Import QcExt.
Notation cramerRule := (@cramerRule _ Qcplus 0 Qcopp Qcmult 1 Qcinv).
Notation cramerRuleList := (@cramerRuleList _ Qcplus 0 Qcopp Qcmult 1 Qcinv).
Notation mdetEx := (@mdetEx _ Qcplus 0 Qcopp Qcmult 1).
Let lB1 := Q2Qc_dlist [[1;2];[3;4]]%Q.
Let lc1 := Q2Qc_list [5;6]%Q.
Let B1 : smat Qc 2 := l2m 0 lB1.
Let c1 : @vec Qc 2 := l2v 0 lc1.
Let lB2 := Q2Qc_dlist
[[1;2;3;4;5];
[2;4;3;5;1];
[3;1;5;2;4];
[4;5;2;3;1];
[5;4;1;2;3]]%Q.
Let lc2 := Q2Qc_list [1;2;3;5;4]%Q.
End test.
let B : smat n := l2m 0 lB in
let c : vec n := l2v 0 lc in
l2v 0 (cramerRuleList n lB lc) = cramerRule B c.
Proof. intros. unfold cramerRuleList. rewrite l2v_v2l. auto. Qed.
End madj.
Section test.
Import QcExt.
Notation cramerRule := (@cramerRule _ Qcplus 0 Qcopp Qcmult 1 Qcinv).
Notation cramerRuleList := (@cramerRuleList _ Qcplus 0 Qcopp Qcmult 1 Qcinv).
Notation mdetEx := (@mdetEx _ Qcplus 0 Qcopp Qcmult 1).
Let lB1 := Q2Qc_dlist [[1;2];[3;4]]%Q.
Let lc1 := Q2Qc_list [5;6]%Q.
Let B1 : smat Qc 2 := l2m 0 lB1.
Let c1 : @vec Qc 2 := l2v 0 lc1.
Let lB2 := Q2Qc_dlist
[[1;2;3;4;5];
[2;4;3;5;1];
[3;1;5;2;4];
[4;5;2;3;1];
[5;4;1;2;3]]%Q.
Let lc2 := Q2Qc_list [1;2;3;5;4]%Q.
End test.