## ビルド
`.zshrc` に以下のような追記をする：
```diff
+# ==== Coq ====
+export OCAMLFIND_CONF="$OPAM_SWITCH_PREFIX/lib/findlib.conf"
+
```
いろいろライブラリを入れる：
- 参考： [Mathematical Components: Installation](https://math-comp.github.io/installation.html)
```console
gfnmac@gfnMBP infotheo % opam install coq-mathcomp-algebra
[ERROR] No package named coq-mathcomp-algebra found.
gfnmac@gfnMBP infotheo % opam repo add coq-released https://coq.inria.fr/opam/released
[coq-released] Initialised
[NOTE] Repository coq-released has been added to the selections of switch 4.12.0 only.
Run `opam repository add coq-released --all-switches|--set-default' to use it in all existing switches,
or in newly created switches, respectively.
gfnmac@gfnMBP infotheo % opam repo add coq-released https://coq.inria.fr/opam/released --all-switches
[coq-released] no changes from https://coq.inria.fr/opam/released
gfnmac@gfnMBP infotheo % opam install coq-mathcomp-algebra
The following actions will be performed:
∗ install conf-gmp 4 [required by zarith]
∗ install conf-findutils 1 [required by coq]
∗ install zarith 1.12 [required by coq]
∗ install coq 8.15.2 [required by coq-mathcomp-ssreflect]
∗ install coq-mathcomp-ssreflect 1.15.0 [required by coq-mathcomp-fingroup]
∗ install coq-mathcomp-fingroup 1.15.0 [required by coq-mathcomp-algebra]
∗ install coq-mathcomp-algebra 1.15.0
===== ∗ 7 =====
Do you want to continue? [Y/n] Y
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><> 🐫
∗ installed conf-findutils.1
⬇ retrieved coq-mathcomp-fingroup.1.15.0 (https://github.com/math-comp/math-comp/archive/mathcomp-1.15.0.tar.gz)
⬇ retrieved coq-mathcomp-algebra.1.15.0 (https://github.com/math-comp/math-comp/archive/mathcomp-1.15.0.tar.gz)
⬇ retrieved coq-mathcomp-ssreflect.1.15.0 (cached)
⬇ retrieved zarith.1.12 (cached)
∗ installed conf-gmp.4
∗ installed zarith.1.12
⬇ retrieved coq.8.15.2 (https://opam.ocaml.org/cache)
∗ installed coq.8.15.2
∗ installed coq-mathcomp-ssreflect.1.15.0
∗ installed coq-mathcomp-fingroup.1.15.0
∗ installed coq-mathcomp-algebra.1.15.0
Done.
```
```console
gfnmac@gfnMBP infotheo % opam install coq-mathcomp-analysis
The following actions will be performed:
∗ install coq-mathcomp-finmap 1.5.2 [required by coq-mathcomp-analysis]
↗ upgrade menhirSdk 20210419 to 20220210 [required by menhir]
∗ install coq-mathcomp-bigenough 1.0.1 [required by coq-mathcomp-analysis]
↗ upgrade menhirLib 20210419 to 20220210 [required by menhir]
↗ upgrade menhir 20210419 to 20220210 [required by elpi]
∗ install elpi 1.15.2 [required by coq-elpi]
↻ recompile satysfi 0.0.7* [uses menhir]
∗ install coq-elpi 1.14.0 [required by coq-hierarchy-builder]
∗ install coq-hierarchy-builder 1.3.0 [required by coq-mathcomp-analysis]
∗ install coq-mathcomp-analysis 0.5.4
===== ∗ 6 ↻ 1 ↗ 3 =====
Do you want to continue? [Y/n] Y
<><> Processing actions <><><><><><><><><><><><><><><><><><><><><><><><><><> 🐫
⬇ retrieved coq-hierarchy-builder.1.3.0 (https://github.com/math-comp/hierarchy-builder/archive/v1.3.0.tar.gz)
⬇ retrieved coq-elpi.1.14.0 (https://github.com/LPCIC/coq-elpi/archive/v1.14.0.tar.gz)
⬇ retrieved coq-mathcomp-analysis.0.5.4 (https://github.com/math-comp/analysis/archive/0.5.4.tar.gz)
⬇ retrieved coq-mathcomp-finmap.1.5.2 (https://github.com/math-comp/finmap/archive/1.5.2.tar.gz)
⬇ retrieved menhir.20220210 (cached)
⬇ retrieved coq-mathcomp-bigenough.1.0.1 (https://github.com/math-comp/bigenough/archive/1.0.1.tar.gz)
⬇ retrieved menhirLib.20220210 (cached)
⬇ retrieved menhirSdk.20220210 (cached)
⊘ removed satysfi.0.0.7
⊘ removed menhir.20210419
⊘ removed menhirLib.20210419
⊘ removed menhirSdk.20210419
∗ installed coq-mathcomp-bigenough.1.0.1
∗ installed menhirLib.20220210
∗ installed menhirSdk.20220210
⬇ retrieved elpi.1.15.2 (https://opam.ocaml.org/cache)
∗ installed coq-mathcomp-finmap.1.5.2
∗ installed menhir.20220210
∗ installed elpi.1.15.2
∗ installed satysfi.0.0.7
∗ installed coq-elpi.1.14.0
∗ installed coq-hierarchy-builder.1.3.0
∗ installed coq-mathcomp-analysis.0.5.4
Done.
gfnmac@gfnMBP infotheo % eval `opam config env`
```
入った様子を見る：
```console
gfnmac@gfnMBP infotheo % opam list | grep coq
coq 8.15.2 Formal proof management system
coq-elpi 1.14.0 Elpi extension language for Coq
coq-hierarchy-builder 1.3.0 High level commands to declare and evolve a hierarchy based on packed classes
coq-mathcomp-algebra 1.15.0 Mathematical Components Library on Algebra
coq-mathcomp-analysis 0.5.4 An analysis library for mathematical components
coq-mathcomp-bigenough 1.0.1 A small library to do epsilon - N reasoning
coq-mathcomp-character 1.15.0 Mathematical Components Library on character theory
coq-mathcomp-field 1.15.0 Mathematical Components Library on Fields
coq-mathcomp-fingroup 1.15.0 Mathematical Components Library on finite groups
coq-mathcomp-finmap 1.5.2 Finite sets, finite maps, finitely supported functions
coq-mathcomp-solvable 1.15.0 Mathematical Components Library on finite groups (II)
coq-mathcomp-ssreflect 1.15.0 Small Scale Reflection
```
ちなみにソースとしてはこのあたりにあるようだ：
```console
gfnmac@gfnMBP infotheo % ls /Users/gfnmac/.opam/4.12.0/lib/coq/user-contrib/mathcomp/fingroup
action.glob all_fingroup.vo fingroup.v morphism.glob perm.vo quotient.v
action.v automorphism.glob fingroup.vo morphism.v presentation.glob quotient.vo
action.vo automorphism.v gproduct.glob morphism.vo presentation.v
all_fingroup.glob automorphism.vo gproduct.v perm.glob presentation.vo
all_fingroup.v fingroup.glob gproduct.vo perm.v quotient.glob
gfnmac@gfnMBP infotheo % ls /Users/gfnmac/.opam/4.12.0/lib/coq/user-contrib/mathcomp/ssreflect
all_ssreflect.glob div.glob finset.glob path.glob ssrbool.glob ssrnat.glob
all_ssreflect.v div.v finset.v path.v ssrbool.v ssrnat.v
all_ssreflect.vo div.vo finset.vo path.vo ssrbool.vo ssrnat.vo
bigop.glob eqtype.glob fintype.glob prime.glob ssreflect.glob ssrnotations.glob
bigop.v eqtype.v fintype.v prime.v ssreflect.v ssrnotations.v
bigop.vo eqtype.vo fintype.vo prime.vo ssreflect.vo ssrnotations.vo
binomial.glob finfun.glob generic_quotient.glob seq.glob ssrfun.glob tuple.glob
binomial.v finfun.v generic_quotient.v seq.v ssrfun.v tuple.v
binomial.vo finfun.vo generic_quotient.vo seq.vo ssrfun.vo tuple.vo
choice.glob fingraph.glob order.glob ssrAC.glob ssrmatching.glob
choice.v fingraph.v order.v ssrAC.v ssrmatching.v
choice.vo fingraph.vo order.vo ssrAC.vo ssrmatching.vo
```
再度ビルドしてみる（最初 `coq-mathcomp-analysis` を入れ忘れていたりなどしてビルドできなかった）：
```console
gfnmac@gfnMBP infotheo % make
/Library/Developer/CommandLineTools/usr/bin/make -f Makefile.coq all
W: This Makefile was generated by Coq 8.16.0
W: while the current Coq version is 8.15.2
COQC lib/ssrR.v
While loading initial state:
Warning: Native compiler is disabled, -native-compiler ondemand option
ignored. [native-compiler-disabled,native-compiler]
COQC lib/Reals_ext.v
While loading initial state:
Warning: Native compiler is disabled, -native-compiler ondemand option
ignored. [native-compiler-disabled,native-compiler]
COQC lib/logb.v
While loading initial state:
Warning: Native compiler is disabled, -native-compiler ondemand option
ignored. [native-compiler-disabled,native-compiler]
COQC lib/Ranalysis_ext.v
While loading initial state:
Warning: Native compiler is disabled, -native-compiler ondemand option
ignored. [native-compiler-disabled,native-compiler]
COQC lib/ssr_ext.v
While loading initial state:
Warning: Native compiler is disabled, -native-compiler ondemand option
ignored. [native-compiler-disabled,native-compiler]
File "./lib/ssr_ext.v", line 904, characters 13-22:
Warning: Notation enum_ordS is deprecated since mathcomp 1.15.0.
Use enum_ordSl instead. [deprecated-syntactic-definition,deprecated]
File "./lib/ssr_ext.v", line 904, characters 13-22:
Warning: Notation enum_ordS is deprecated since mathcomp 1.15.0.
Use enum_ordSl instead. [deprecated-syntactic-definition,deprecated]
File "./lib/ssr_ext.v", line 904, characters 13-22:
Warning: Notation enum_ordS is deprecated since mathcomp 1.15.0.
Use enum_ordSl instead. [deprecated-syntactic-definition,deprecated]
File "./lib/ssr_ext.v", line 908, characters 8-17:
Warning: Notation enum_ordS is deprecated since mathcomp 1.15.0.
Use enum_ordSl instead. [deprecated-syntactic-definition,deprecated]
File "./lib/ssr_ext.v", line 908, characters 8-17:
Warning: Notation enum_ordS is deprecated since mathcomp 1.15.0.
Use enum_ordSl instead. [deprecated-syntactic-definition,deprecated]
File "./lib/ssr_ext.v", line 908, characters 8-17:
Warning: Notation enum_ordS is deprecated since mathcomp 1.15.0.
Use enum_ordSl instead. [deprecated-syntactic-definition,deprecated]
COQC lib/f2.v
While loading initial state:
Warning: Native compiler is disabled, -native-compiler ondemand option
ignored. [native-compiler-disabled,native-compiler]
COQC lib/ssralg_ext.v
While loading initial state:
Warning: Native compiler is disabled, -native-compiler ondemand option
ignored. [native-compiler-disabled,native-compiler]
File "./lib/ssralg_ext.v", line 503, characters 37-51:
Error:
In environment
F : fieldType
The term "mem [char F]" has type "mem_pred nat"
while it is expected to have type
"mem_pred (GRing.Zmodule.sort (GRing.Ring.zmodType ?t))".
make[2]: *** [lib/ssralg_ext.vo] Error 1
make[1]: *** [all] Error 2
make: *** [all] Error 2
```
失敗した．`ssralg_ext.v` に型エラーがあるらしい？ 503行目の `2 \in [char F]` がダメとのこと：
```coq
Lemma sum_char2 (F : fieldType) (_ : 2 \in [char F]) k (f : 'I_k -> F) :
(\sum_(i < k) (f i)) ^+ 2 = \sum_(i < k) (f i) ^+ 2.
Proof.
elim/big_ind2 : _ => [|x1 x2 y1 y2 <- <-|//] /=; first by rewrite expr0n.
by rewrite sqrrD mulr2n addrr_char2 // addr0.
Qed.
```
## アドホックに対処
今井さんによると `ssralg_ext` への依存は以下の変更を `vandermonde.v` に施せば解消可能とのこと：
```diff
Local Open Scope ring_scope.
+
+Declare Scope vec_ext_scope.
+Notation "x '``_' i" := (x ord0 i) (at level 9) : vec_ext_scope.
+Open Scope vec_ext_scope.
+
+Lemma iter_addr0 (R : ringType) : forall n x, iter n (+%R (0 : R)) x = x.
+Proof. elim=> //= n IH x. by rewrite IH add0r. Qed.
+
Local Open Scope vec_ext_scope.
```
実際，最後まで `C-c C-<enter>` で通った．めでたし．
## 読む
### `iter_addr0`
移植したこれを見てみる：
```coq
Lemma iter_addr0 (R : ringType) : forall n x, iter n (+%R (0 : R)) x = x.
Proof. elim=> //= n IH x. by rewrite IH add0r. Qed.
```
`iter` の型を `Check iter.` で見てみる：
```coq
iter
: forall T : Type, nat -> (T -> T) -> T -> T
```
どうやら何度も繰り返し適用する函数らしい．
`+%R` は `ssralg` を見てみる：
```coq
Reserved Notation "+%R" (at level 0).
Notation "+%R" := (@add _) : fun_scope.
```
あまりわからないが，おそらく単に環の加法．
つまり，`iter_addr0` は “`x` に何度 `0`（環に於ける加法の単位元）を足しても `x`” という補題らしい．
証明も見てみる．いきなり `elim=> //=` という知らないtacticが使われている．`move=> //`（萩原・Affeldt本 p.48）が単純計算を備えた `move=>` の変種であることや，`rewrite /=`（同 p.82）が定義を辿る程度の計算を行なうtacticであることを思うとこの類いではありそう．
最初の状態はこれ：
```coq
1 goal (ID 2504)
R : ringType
============================
forall (n : nat) (x : R), iter n (+%R (0 : R)) x = x
```
`elim=> //= n IH x.` を読むとゴールは以下のようになる：
```coq
1 goal (ID 2551)
R : ringType
n : nat
IH : forall x : R, iter n (+%R 0) x = x
x : R
============================
0 + iter n (+%R 0) x = x
```
`//` に変えると以下のようになる：
```coq
1 goal (ID 2547)
R : ringType
n : nat
IH : forall x : R, iter n (+%R 0) x = x
x : R
============================
iter n.+1 (+%R 0) x = x
```
どうやら `iter` の定義に基づいた展開がされていないようだ．
一方で `/=` に変えると次のようなエラーになる：
```coq
Error: No assumption in (n = n)
```
どうやら `//=` は `//` にして次に `rewrite /=` がくるのと等価らしい？ 以下が通った：
```coq
Lemma iter_addr0 (R : ringType) : forall n x, iter n (+%R (0 : R)) x = x.
Proof. elim=> // n IH x. rewrite /=. by rewrite IH add0r. Qed.
```
調べたところ，Garrigue先生の文書に解説があった：
- [述語論理とSSReflectのタクティック](https://www.math.nagoya-u.ac.jp/~garrigue/lecture/2020_AW/ssrcoq2.pdf)
> - `/=` は焦点と結論を単純化する．
> - `//` は全てのゴールに対して `done` で解決を失敗せずに試みる．
> - `//=` はその両方を行う.
文書中に説明があるが，「焦点」とはゴールのトップの前件のこと（ゴールが `A -> B` の形でない場合は無し扱い）．「結論」とはゴールの後件のこと（これは恒にある）．`done` はそういうtacticで，自明な解決を試みるもの（解決しなければ失敗する）．
とりあえず読み進める．
### `Section vandermonde_matrix`
#### `Definition vander_gen`，`Definition vander`
```coq
Section vandermonde_matrix.
Variables (n : nat) (R : ringType) (a : 'rV[R]_n).
Definition vander_gen (r : nat) := \matrix_(i < r, j < n) (a``_j) ^+ i.
Definition vander := vander_gen n.
End vandermonde_matrix.
```
`'rV[R]_n` は長さ `n` の行ベクトル (row vector)．`[R]` は要素の環に相当するものだろう．`\matrix` 云々はそのまま行列をつくるための記法．
* 参考： [mathcomp.algebra.matrix](https://math-comp.github.io/htmldoc/mathcomp.algebra.matrix.html)
> ```coq
> Notation "\matrix_ ( i < m , j < n ) E" :=
> (@matrix_of_fun _ m n matrix_key (fun i j ⇒ E)) (only parsing) : ring_scope.
> ```
というわけで `vander_gen r` は `r` 行 `n` 列のVandermonde行列のようだ．`(i, j)` 要素が `(a``_j) ^+ i` であり，これはつまりベクトル `a` の `j` 番目の要素の `i` 乗．
`vander` は `vander_gen n` であり，つまり正方行列版．
### `Section vandermonde_k_matrix`
```coq
Section vandermonde_k_matrix.
…
End vandermonde_k_matrix.
```
結構長い．46行目から360行目まであり，`vandermonde.v` が456行なので，半分以上をこのsectionが占めている．
#### `Variable R`
```coq
Variable (R : comRingType).
```
可換環 `R` が固定されている．
- 参考： [Library mathcomp.algebra.ssralg](http://www.math.nagoya-u.ac.jp/~garrigue/lecture/2017_AW/mathcomp-1.6/htmldoc/mathcomp.algebra.ssralg.html)
#### `Definition lc`，`Definition mat_lc`
```coq
Definition lc n (a : R) (r0 r1 : 'rV[R]_n) := r0 - a *: r1.
Definition mat_lc n cst (M : 'M[R]_n.+1) (k : 'I_n.+1) :=
if k == 0 then
M
else
\matrix_(i < n.+1)
if i == k then
lc cst (row i M) (row (inord i.-1) M)
else
row i M.
```
`lc n a r0 r1` は簡単で，`r0` から `r1` を `a` 倍（スカラー倍）したものを引いた行ベクトル．つまり**掃き出し操作**．
`M : 'M[R]_n.+1` は $(n + 1)$ 行 $(n + 1)$ 列の正方行列．`'I_n.+1` は集合 $\{0, 1, \ldots, n\}$．
`\matrix_(i < n.+1) 〈rv_i〉` は要するに第 `i` 行が行ベクトル `〈rv_i〉` で与えられる行列らしい：
> ```
> \matrix(i < m) RowExpr(i) ==
> the m x n matrix with row i given by RowExpr(i) : 'rV_n.
> ```
`inord` は単に `I_n.+1` の元への入射らしい（おそらくここでは減算をしていて非自明なために必要になっている）：
> ```
> inord k == the i : 'I_n.+1 with value k (n is inferred from the
> context).
> ```
* 参考： [mathcomp.ssreflect.fintype](https://math-comp.github.io/htmldoc/mathcomp.ssreflect.fintype.html)
つまり `mat_lc n cst M k` は行列 `M` の第 `k` 行から第 `k - 1` 行の `cst` 倍を引いたもの（ただし行の番号は0-originで，`k = 0` の場合は単に `M`）．
#### `Definition vander_k`
```coq
(* k = 0 -> modifies nothing *)
(* k = 1 -> modifies row n *)
(* k = 2 -> modifies row n-1, n *)
(* k = 3 -> modifies row n-2, n-1, n *)
(* k = n.+1 -> modifies row 0, 1, ..., n *)
(* do not use with k > n.+1 *)
Definition vander_k n (a : 'rV[R]_n.+1) (M : 'M_n.+1) (k : nat) :=
foldl (fun acc x => mat_lc (a``_ord0) acc (inord x)) M (rev (iota (n.+1 - k) k)).
```
`iota m n` は区間 `[m, m + 1, …, m + n - 1]`．
* 参考： [mathcomp.ssreflect.seq](https://math-comp.github.io/htmldoc/mathcomp.ssreflect.seq.html)
ここでは以下：
```
(rev (iota (n.+1 - k) k)) = rev [n + 1 - k, …, n + 1 - 1] = [n, …, n - k + 1]
```
`ord0` は単に添字集合 `I_n.+1` の `0` に相当する元．
* 参考： [mathcomp.ssreflect.fintype](https://math-comp.github.io/htmldoc/mathcomp.ssreflect.fintype.html)
`a` は行ベクトルで与えられているが先頭の要素しか使わないらしい．これを `a0` と書くことにすると，上記の処理は大体以下のような具合：
```
let acc = M in
let acc = mat_lc a0 acc n in
let acc = mat_lc a0 acc (n - 1) in
…
let acc = mat_lc a0 acc (n - k + 1) in
acc
```
つまり第 `n` 行から第 `n - 1` 行の `a0` 倍を引き，第 `n - 1` 行から第 `n - 2` 行の `a0` 倍を引き，… と繰り返したもの．コメントにある通り，下 `k` 行分が変わる．
#### `Lemma vander_k_rec`
```
Lemma vander_k_rec n (a : 'rV[R]_n.+1) k :
k <= n.+1 ->
forall i, i <= n ->
forall M,
row (inord i) (vander_k a M k) =
if i == O then
row 0 M
else if n.+1 - k <= i <= n then
lc (a``_ord0) (row (inord i) M) (row (inord i.-1) M)
else
row (inord i) M.
```
数式風に書き起こすと以下のような具合（行列 $A$ に対して $A_i$ は $A$ の $i$ 番目の行ベクトル）：
$$
\begin{multline}
k ≤ n + 1 ⇒ ∀i ∈ ℕ. i ≤ n ⇒ ∀M ∈ R^{(n + 1) × (n + 1)}.
\\
(\mathrm{vanderk}(a, M, k))_i =
\begin{cases}
M_0 & (\text{if}\ i = 0)
\\
M_i & (\text{if}\ 1 ≤ i ≤ n - k)
\\
\mathrm{lc}(a_0, M_i, M_{i - 1}) & (\text{if}\ n - k + 1 ≤ i ≤ n)
\end{cases}
\end{multline}
$$
言っていること自体はそんなに複雑ではなく，ほぼ `vander_k` の性質の直観そのものである．
証明は80行ほどある．
- 今井さん： 「ひととおり主張を見たあと，トップダウンに `elim` と `case` で場合分けの骨組みを把握し，手で証明してみましょう．そうすると単純な証明なのに無駄に長い証明をしている場所がわかりやすくなるかも」
#### `Definition vander_last`
```coq
Definition vander_last n (a : 'rV[R]_n.+1) :=
\matrix_(i < n.+1, j < n.+1)
if i == 0 then
1
else if j == 0 then
0
else
(a``_j) ^+ i - a``_0 * (a``_j) ^+ i.-1.
```
0行目が全部1，0列目の0番目以外が全部0，他の $(i, j)$ 要素は $a_j^i - a_0 \cdot a_j^{i - 1}$ であるような行列らしい．
$$
\mathrm{vanderlast}(a) :=
\begin{pmatrix}
1 & 1 & 1 & \cdots & 1
\\
0 & a_1^1 - a_0 a_1^0 & a_2^1 - a_0 a_2^0 & \cdots & a_n^1 - a_0 a_n^0
\\
0 & a_1^2 - a_0 a_1^1 & a_2^2 - a_0 a_2^1 & \cdots & a_n^2 - a_0 a_n^1
\\
\vdots & \vdots & \vdots & \ddots & \vdots
\\
0 & a_1^n - a_0 a_1^{n - 1} & a_2^n - a_0 a_2^{n - 1} & \cdots & a_n^n - a_0 a_n^{n - 1}
\end{pmatrix}
$$
#### `Lemma vander_lastE`
```coq
Lemma vander_lastE n (a : 'rV[R]_n.+1) :
vander_last a = vander_k a (vander a) n.
```
通常の多項式のVandermonde行列 `vander a` に対し，第 `n` 行から第 `n - 1` 行の `a0` 倍を引き，第 `n - 1` 行から第 `n - 2` 行の `a0` 倍を引き，… 第1行から第0行の `a0` 倍を引いて得られるのが上記の `vander_last a` であると言っている．たしかに要素ごとにみるとそうなっていそうだ．
* 今井さんコメント： 定義に `E` を後置した名前の補題は，だいたいその定義の最も嬉しい性質に関する補題であるという慣習がある
#### `Lemma vander_k_max`
```coq
Lemma vander_k_max n (a : 'rV[R]_n.+1) (M : 'M[R]_n.+1) :
vander_k a M n.+1 = vander_k a M n.
```
これは単に `vander_k` の第3引数が `n + 1` であっても `n` の場合に等しいということを言っているだけ．
#### `Lemma det_vander_k_rec`，`Lemma det_vander_k`，`Lemma det_vander_k_vander`
```coq
Lemma det_vander_k_rec n (a : 'rV[R]_n.+1) (k : nat) (M : 'M[R]_n.+1) :
k < n.+1 -> \det (vander_k a M k) = \det (vander_k a M k.-1).
```
行列式が `vander_k` の操作で保存するということを言っている．掃き出し操作の前後で行列式は不変なので線型代数的には当たり前だが，証明は125行ある．
```coq
Lemma det_vander_k n (a : 'rV[R]_n.+1) (k : nat) (M : 'M[R]_n.+1) :
k <= n.+1 -> \det (vander_k a M k) = \det (vander_k a M k.-1).
```
これは上の不等号が強くなっただけ．証明も2行だけ．
```coq
Lemma det_vander_k_vander n (a : 'rV[R]_n.+1) (k : nat) :
k <= n.+1 -> \det (vander_k a (vander a) k) = \det (vander a).
```
やはりこれも `M` に `vander a` をあてはめて系として出てくる．証明は3行．
### `Section vandermonde_determinant`
#### `Variable R`
```coq
Variable (R : comRingType).
```
やはり可換環 `R` が固定されている．
#### `Lemma det_mlinear_rec`
`mlinear` は多分多重線型性のこと．
```coq
Lemma det_mlinear_rec n (f : 'I_n.+1 -> 'I_n.+1 -> R) (g : 'I_n.+1 -> R) k :
k <= n.+1 ->
\det (\matrix_(j, i) (f i j * g j)) =
(\prod_(l < k) g (inord l)) * \det (\matrix_(j, i) (f i j * if j >= k then g j else 1)).
```
ややこしいが `j` が行のインデックスで `i` が列のインデックス．
`f i j` と `g j` を単に $f_{ij}$ や $g_j$ などと書くことにすると，
$$
\det
\begin{pmatrix}
f_{00} g_0 & f_{10} g_0 & \cdots & f_{n0} g_0
\\
f_{01} g_1 & f_{11} g_1 & \cdots & f_{n1} g_1
\\
\vdots & \vdots & \ddots & \vdots
\\
f_{0n} g_n & f_{1n} g_n & \cdots & f_{nn} g_n
\end{pmatrix} =
\left(\prod_{l < k} g_l\right) \cdot
\det
\begin{pmatrix}
f_{00} & f_{10} & \cdots & f_{n0}
\\
f_{01} & f_{11} & \cdots & f_{n1}
\\
\vdots & \vdots & \ddots & \vdots
\\
f_{0(k - 1)} & f_{1(k - 1)} & \cdots & f_{n(k - 1)}
\\\hline
f_{0k} g_{k} & f_{1k} g_{k} & \cdots & f_{nk} g_{k}
\\
\vdots & \vdots & \ddots & \vdots
\\
f_{0n} g_{n} & f_{1n} g_{n} & \cdots & f_{nn} g_{n}
\end{pmatrix}
$$
という主張．これは $\det$ の線型性から簡単に言える．証明は23行ほど．
#### `Lemma det_mlinear`
```coq
Lemma det_mlinear n (f : 'I_n -> 'I_n -> R) (g : 'I_n -> R) :
\det (\matrix_(i, j) (f i j * g j)) = \prod_(i < n) g i * \det (\matrix_(i, j) (f i j)).
```
`det_mlinear_rec` を `k = n + 1` に限定した系．
#### `Lemma det_vander_rec`
```coq
Lemma det_vander_rec n (a : 'rV[R]_n.+1) :
\det (vander a) =
\det (vander (\row_(i < n) a``_(inord i.+1))) * \prod_(1 <= j < n.+1) (a``_(inord j) - a``_0).
```
`vander a` は以下のような行列だった：
$$
\mathrm{vander}(a) =
\begin{pmatrix}
a_0^0 & a_1^0 & \cdots & a_n^0
\\
a_0^1 & a_1^1 & \cdots & a_n^1
\\
\vdots & \vdots & \ddots & \vdots
\\
a_0^{n - 1} & a_1^{n - 1} & \cdots & a_n^{n - 1}
\\
a_0^n & a_1^n & \cdots & a_n^n
\end{pmatrix}
$$
`vander (\row_(i < n) a``_(inord i.+1))` はこうである（行数と列数が1ずつ小さい）：
$$
\begin{pmatrix}
a_1^0 & a_2^0 & \cdots & a_n^0
\\
a_1^1 & a_2^1 & \cdots & a_n^1
\\
\vdots & \vdots & \ddots & \vdots
\\
a_1^{n - 1} & a_2^{n - 1} & \cdots & a_n^{n - 1}
\end{pmatrix}
$$
（特に使わない性質だが，これは `vander a` の左1列と下1行を削った行列である．）
まず，`Lemma det_vander_k_vander` より
```coq
\det (vander a) = \det (vander_k a (vander a) n)
```
が成り立つ．さらに `Lemma vander_lastE` より
```coq
\det (vander_k a (vander a) n) = \det (vander_last a)
```
が成り立つ．したがって
```coq
\det (vander_last a) =
\det (vander (\row_(i < n) a``_(inord i.+1))) * \prod_(1 <= j < n.+1) (a``_(inord j) - a``_0)
```
が言えれば十分．ところで `\det (vander_last a)` は $\det$ の性質から簡単な形にできる（$\det$ の定義を考えると，$0$ の要素を選ぶような置換は考えなくてよいため）：
$$
\begin{align*}
\det \mathrm{vanderlast}(a) &=
\det
\left(\begin{array}{c|cccc}
1 & 1 & 1 & \cdots & 1
\\\hline
0 & a_1^1 - a_0 a_1^0 & a_2^1 - a_0 a_2^0 & \cdots & a_n^1 - a_0 a_n^0
\\
0 & a_1^2 - a_0 a_1^1 & a_2^2 - a_0 a_2^1 & \cdots & a_n^2 - a_0 a_n^1
\\
\vdots & \vdots & \vdots & \ddots & \vdots
\\
0 & a_1^n - a_0 a_1^{n - 1} & a_2^n - a_0 a_2^{n - 1} & \cdots & a_n^n - a_0 a_n^{n - 1}
\end{array}\right)
\\&=
\det
\begin{pmatrix}
a_1^1 - a_0 a_1^0 & a_2^1 - a_0 a_2^0 & \cdots & a_n^1 - a_0 a_n^0
\\
a_1^2 - a_0 a_1^1 & a_2^2 - a_0 a_2^1 & \cdots & a_n^2 - a_0 a_n^1
\\
\vdots & \vdots & \ddots & \vdots
\\
a_1^n - a_0 a_1^{n - 1} & a_2^n - a_0 a_2^{n - 1} & \cdots & a_n^n - a_0 a_n^{n - 1}
\end{pmatrix}
\\&=
\det
\begin{pmatrix}
a_1^0 (a_1 - a_0) & a_2^0 (a_2 - a_0) & \cdots & a_n^0 (a_n - a_0)
\\
a_1^1 (a_1 - a_0) & a_2^1 (a_2 - a_0) & \cdots & a_n^1 (a_n - a_0)
\\
\vdots & \vdots & \ddots & \vdots
\\
a_1^{n - 1} (a_1 - a_0) & a_2^{n - 1} (a_2 - a_0) & \cdots & a_n^{n - 1} (a_n - a_0)
\end{pmatrix}
\\&=
(a_1 - a_0) \cdots (a_n - a_0) \cdot
\det
\begin{pmatrix}
a_1^0 & a_2^0 & \cdots & a_n^0
\\
a_1^1 & a_2^1 & \cdots & a_n^1
\\
\vdots & \vdots & \ddots & \vdots
\\
a_1^{n - 1} & a_2^{n - 1} & \cdots & a_n^{n - 1}
\end{pmatrix}
\end{align*}
$$
というわけで右辺が出てきて示せた．
#### `Lemma det_vander`
```coq
Lemma det_vander n (a : 'rV[R]_n.+1) :
\det (vander a) = \prod_(i < n.+1) (\prod_(j < n.+1 | i < j) (a``_j - a``_i)).
```
これが最終目標の補題で，Vandermonde行列の行列式の一般形を示している．
上記の `Lemma det_vander_rec` を繰り返し適用することで以下のように示せる：
$$
\begin{align*}
\det
\begin{pmatrix}
a_0^0 & a_1^0 & \cdots & a_n^0
\\
a_0^1 & a_1^1 & \cdots & a_n^1
\\
\vdots & \vdots & \ddots & \vdots
\\
a_0^{n - 1} & a_1^{n - 1} & \cdots & a_n^{n - 1}
\\
a_0^n & a_1^n & \cdots & a_n^n
\end{pmatrix}
&=
\left(\prod_{i = 1}^{n} (a_i - a_0)\right) \cdot
\det
\begin{pmatrix}
a_1^0 & a_2^0 & \cdots & a_n^0
\\
a_1^1 & a_2^1 & \cdots & a_n^1
\\
\vdots & \vdots & \ddots & \vdots
\\
a_1^{n - 1} & a_2^{n - 1} & \cdots & a_n^{n - 1}
\end{pmatrix}
\\&=
\left(\prod_{i = 1}^{n} (a_i - a_0)\right) \cdot
\left(\prod_{i = 2}^{n} (a_i - a_1)\right) \cdot
\det
\begin{pmatrix}
a_2^0 & a_3^0 & \cdots & a_n^0
\\
a_2^1 & a_3^1 & \cdots & a_n^1
\\
\vdots & \vdots & \ddots & \vdots
\\
a_2^{n - 2} & a_3^{n - 2} & \cdots & a_n^{n - 2}
\end{pmatrix}
\\&=
\left(\prod_{i = 1}^{n} (a_i - a_0)\right) \cdot
\left(\prod_{i = 2}^{n} (a_i - a_1)\right) \cdot
\cdots \cdot
\left(\prod_{i = n}^{n} (a_i - a_{n - 1})\right) \cdot
\det (a_n^0)
\\&=
\prod_{j = 0}^{n} \prod_{i = 0}^{j - 1} (a_j - a_i)
\end{align*}
$$
## どう改善できそうか
### `det_vander_k_rec`
まずは `det_vander_k_rec` が簡単にできそう．これは単に掃き出し1回で行列式が保存することの系であるため．
以下の補題が有効活用できそう：
```coq
foldl_cat
: forall (T R : Type) (f : R -> T -> R) (z : R) (s1 s2 : seq T),
foldl f z (s1 ++ s2) = foldl f (foldl f z s1) s2
```
簡単に手で変形してみる：
```
f := fun acc x => mat_lc (a``_ord0) acc (inord x)
case k >= 1
vander_k a M k.-1
==
foldl f M (rev (iota (n.+1 - (k.-1)) (k.-1)))
==
foldl f M (rev (iota (n + 2 - k) (k - 1)))
==
foldl f M (rev [n + 2 - k, … n + 2 - 2])
==
foldl f M [n, …, n - k + 2]
vander_k a M k
==
foldl f M (rev (iota (n.+1 - k) k))
==
let x :: xs = rev (iota (n.+1 - k) k) in
foldl f (f M x) xs
==
let x :: xs = [n, …, n - k + 1] in
foldl f (f M x) xs
==
foldl f (f M n) [n - 1, …, n - k + 1]
==
foldl f (f M n) ([n - 1, …, n - k + 2] ++ [n - k + 1])
==
foldl f (foldl f (f M n) [n - 1, …, n - k + 2]) [n - k + 1] (by foldl_cat)
==
foldl f (foldl f M [n, n - 1, …, n - k + 2]) [n - k + 1] (by def. of foldl)
==
foldl f (vander_k a M k.-1) [n - k + 1]
==
foldl (f (vander_k a M k.-1) (n - k + 1)) [] (by def. of foldl)
==
f (vander_k a M k.-1) (n - k + 1) (by def. of foldl)
===
mat_lc (a``_ord0) (vander_k a M k.-1) (inord (n - k + 1)) (by def. of f)
```
これをCoqで書き起こせば `vander_k a M k` は `vander_k a M k.-1` から掃き出しを1回行なって得られることが言える．
あとは `mat_lc` が行列式を保存するという一般の線型代数の議論をすればよい．
まずは（型や前件は適切に与えるとして）以下を補題にするとよさそう：
```coq
Lemma vander_k_recurrence_relation : ...
vander_k a M k = mat_lc (a``_ord0) (vander_k a M k.-1) (inord (n.+1 - k)).
```
続いて以下が言えればよさそう：
```coq
Lemma mat_lc_preserves_det : ...
\det (mat_lc cst M n) = \det M.
```
Sign in with Wallet
Connect another wallet