From c8e1a4a3d103eee8b89c4e7b8281d9abcf400056 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 30 May 2024 11:40:59 +0900 Subject: [PATCH] fixes #69 --- _CoqProject | 1 - ecc_classic/bch.v | 2 +- ecc_classic/grs.v | 7 +- ecc_classic/reed_solomon.v | 6 +- ecc_modern/ldpc_algo.v | 39 ++- ecc_modern/ldpc_algo_proof.v | 75 +++--- lib/vandermonde.v | 454 ----------------------------------- 7 files changed, 62 insertions(+), 522 deletions(-) delete mode 100644 lib/vandermonde.v diff --git a/_CoqProject b/_CoqProject index 04c24f75..6673bf51 100644 --- a/_CoqProject +++ b/_CoqProject @@ -21,7 +21,6 @@ lib/hamming.v lib/poly_ext.v lib/euclid.v lib/dft.v -lib/vandermonde.v lib/classical_sets_ext.v probability/fdist.v probability/proba.v diff --git a/ecc_classic/bch.v b/ecc_classic/bch.v index f0fcb430..ec7c8daf 100644 --- a/ecc_classic/bch.v +++ b/ecc_classic/bch.v @@ -561,7 +561,7 @@ Definition BCH_err y : {poly 'F_2} := let s := vstop.[0]^-1 *: vstop in \poly_(i < n) (if s.[a^- i] == 0 then 1 else 0). -Definition BCH_repair : repairT [finType of 'F_2] [finType of 'F_2] n := +Definition BCH_repair : repairT 'F_2 'F_2 n := [ffun y => if \BCHsynp_(rVexp a n, y, t) == 0 then Some y else diff --git a/ecc_classic/grs.v b/ecc_classic/grs.v index 7a2e42e0..76508876 100644 --- a/ecc_classic/grs.v +++ b/ecc_classic/grs.v @@ -2,8 +2,7 @@ (* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later *) From mathcomp Require Import all_ssreflect ssralg finalg poly polydiv cyclic. From mathcomp Require Import perm matrix mxpoly vector mxalgebra zmodp. -Require Import ssr_ext ssralg_ext vandermonde linearcode. -Require Import dft poly_decoding. +Require Import ssr_ext ssralg_ext linearcode dft poly_decoding. (******************************************************************************) (* Generalized Reed-Solomon Codes *) @@ -120,7 +119,7 @@ Definition GRS_PCM_sq (a b : 'rV[F]_n) r := Lemma GRS_PCM_sq_vander (a b : 'rV[F]_n) (rn : r <= n) : GRS_PCM_sq a b r = - vandermonde.Vandermonde r (\row_(i < r) a``_(inord i)) *m + Vandermonde r (\row_(i < r) a``_(inord i)) *m diag_mx (\row_(i < r) b``_(inord i)). Proof. apply/matrixP => i j. @@ -150,7 +149,7 @@ apply mxrank_unit. rewrite unitmxE unitfE GRS_PCM_sq_vander // det_mulmx mulf_neq0 //; last first. by rewrite det_diag prodf_seq_neq0; apply/allP => /= i _; rewrite mxE b0. case: r rn => [|r' rn]; first by rewrite det_mx00 oner_neq0. -rewrite vandermonde.det_Vandermonde prodf_seq_neq0; apply/allP => /= i _. +rewrite det_Vandermonde prodf_seq_neq0; apply/allP => /= i _. rewrite prodf_seq_neq0; apply/allP => /= j _; apply/implyP. rewrite ltnNge => ij; rewrite !mxE subr_eq0; apply: contra ij => /eqP ij. move: (@a_inj (inord i) (inord j)); rewrite !ffunE ij => /(_ erefl). diff --git a/ecc_classic/reed_solomon.v b/ecc_classic/reed_solomon.v index 6ef1dfd3..7807fd0d 100644 --- a/ecc_classic/reed_solomon.v +++ b/ecc_classic/reed_solomon.v @@ -702,7 +702,7 @@ Variables (d : nat) (n' : nat). Let n := n'.+1. Hypothesis dn : RS.redundancy_ub d n. -Definition encoder : encT F [finType of 'rV[F]_(n - d.+1).+1] n := +Definition encoder : encT F 'rV[F]_(n - d.+1).+1 n := let g := \gen_(a, d) in [ffun m => let mxd := rVpoly m * 'X^d in poly_rV (mxd - mxd %% g)]. @@ -720,7 +720,7 @@ Definition RS_discard' (x : 'rV[F]_n) : 'rV[F]_(n - d.+1).+1 := Definition RS_discard (x : 'rV[F]_n) : 'rV[F]_(n - d.+1).+1 := poly_rV ((rVpoly x) %/ 'X^d). -Definition decoder : decT F [finType of 'rV[F]_(n - d.+1).+1] n := +Definition decoder : decT F 'rV[F]_(n - d.+1).+1 n := [ffun y => omap RS_discard (RS_repair a _ d y)]. Definition RS_code := mkCode encoder decoder. @@ -778,7 +778,7 @@ Hypothesis a_not_uroot_on : not_uroot_on a n. (* NB: corresponds to lemma 10.59? *) Lemma RS_enc_img : - (enc RS_code) @: [finType of 'rV[F]_(n - d.+1).+1] \subset RS.code a n d. + (enc RS_code) @: 'rV[F]_(n - d.+1).+1 \subset RS.code a n d. Proof. apply/subsetP => /= c /imsetP[/= m _] ->{c}. rewrite /encoder ffunE. diff --git a/ecc_modern/ldpc_algo.v b/ecc_modern/ldpc_algo.v index dfdf1463..6b452592 100644 --- a/ecc_modern/ldpc_algo.v +++ b/ecc_modern/ldpc_algo.v @@ -203,7 +203,7 @@ Extract Constant Rmult => "( *.)". Extract Constant Rplus => "(+.)". Extract Constant Rinv => "fun x -> 1. /. x". Extract Constant Ropp => "(~-.)". -Extraction "extraction/sumprod.ml" sumprod estimation. +(*Extraction "extraction/sumprod.ml" sumprod estimation.*) Section ToGraph. @@ -220,20 +220,20 @@ Fixpoint labels {id} {k U D} (n : tn_tree id k U D) : seq id := End ToGraph. +Definition sumbool_ord m n : finType := ('I_m + 'I_n)%type. + Section BuildTree. Variables m n' : nat. Let n := n'.+1. Variable H : 'M['F_2]_(m, n). -Definition id := [finType of ('I_m + 'I_n)]. - Import GRing.Theory. Local Open Scope ring_scope. Variable rW : 'I_n -> R2. -Definition kind_of_id (i : id) := +Definition kind_of_id (i : sumbool_ord m n) := match i with | inl _ => kf | inr _ => kv @@ -241,11 +241,11 @@ Definition kind_of_id (i : id) := Definition ord_of_kind k : finType := match k with - | kv => [finType of 'I_n] - | kf => [finType of 'I_m] + | kv => 'I_n + | kf => 'I_m end. -Definition id_of_kind k : ord_of_kind k -> id := +Definition id_of_kind k : ord_of_kind k -> sumbool_ord m n := match k with | kv => inr | kf => inl @@ -257,13 +257,13 @@ Definition tag_of_kind k : ord_of_kind k -> tag k := | kf => fun i => Func end. -Definition tag_of_id (a : id) : tag (kind_of_id a) := +Definition tag_of_id (a : sumbool_ord m n) : tag (kind_of_id a) := match a with | inl _ => Func | inr i => Var (rW i) end. -Definition select_children (s : seq id) k := +Definition select_children (s : seq (sumbool_ord m n)) k := match k return ord_of_kind k -> seq (ord_of_kind (negk k)) with | kv => fun i => let s := id_of_kind i :: s in @@ -273,8 +273,8 @@ Definition select_children (s : seq id) k := [seq j <- ord_enum n | (H i j == 1) && (inr j \notin s)] end. -Fixpoint build_tree_rec (h : nat) (s : seq id) k (i : ord_of_kind k) -: tn_tree id k unit unit := +Fixpoint build_tree_rec (h : nat) (s : seq (sumbool_ord m n)) + k (i : ord_of_kind k) : tn_tree (sumbool_ord m n) k unit unit := let chrn := match h with 0 => [::] | h'.+1 => @@ -284,9 +284,10 @@ Fixpoint build_tree_rec (h : nat) (s : seq id) k (i : ord_of_kind k) in Node (id_of_kind i) (tag_of_kind i) chrn tt tt. -Definition build_tree := build_tree_rec #|id| [::]. +Definition build_tree := build_tree_rec #|sumbool_ord m n| [::]. -Fixpoint msg (i1 i2 : id) (i : option id) {k} (t : tn_tree id k R2 R2) := +Fixpoint msg (i1 i2 : sumbool_ord m n) (i : option (sumbool_ord m n)) {k} + (t : tn_tree (sumbool_ord m n) k R2 R2) := if Some i1 == i then if i2 == node_id t then [:: down t] else [::] else if Some i2 == i then @@ -306,8 +307,6 @@ Variables m n' : nat. Let n := n'.+1. Variable H : 'M['F_2]_(m, n). -Let id' := id m n'. - Import GRing.Theory. Local Open Scope ring_scope. @@ -328,14 +327,14 @@ Let p01 f n0 : R2 := (f (d `[n0 := 0]), f (d `[n0 := 1])). Let alpha' := ldpc.alpha H W y. Let beta' := ldpc.beta H W y. -Definition msg_spec (i j : id') : R2 := +Definition msg_spec (i j : sumbool_ord m n) : R2 := match i, j with | inl m0, inr n0 => p01 (alpha' m0 n0) n0 | inr n0, inl m0 => p01 (beta' n0 m0) n0 | _, _ => (R0,R0) end. -Definition prec_node (s : seq id') := +Definition prec_node (s : seq (sumbool_ord m n)) := match s with | [::] => None | [:: a & r] => Some a @@ -343,7 +342,7 @@ Definition prec_node (s : seq id') := Coercion choice.seq_of_opt : option >-> seq. -Fixpoint build_computed_tree h s k i : tn_tree id' k R2 R2 := +Fixpoint build_computed_tree h s k i : tn_tree (sumbool_ord m n) k R2 R2 := let chrn := match h with | 0 => [::] @@ -366,7 +365,7 @@ Fixpoint build_computed_tree h s k i : tn_tree id' k R2 R2 := end. Definition computed_tree_spec := - computed_tree = build_computed_tree #|id'| [::] (k:=kv) ord0. + computed_tree = build_computed_tree #|sumbool_ord m n| [::] (k:=kv) ord0. Definition sumprod_spec := forall a b, tanner_rel H a b -> @@ -380,7 +379,7 @@ Definition estimation_spec := uniq (unzip1 estimations) /\ forall n0, (inr n0, (esti_spec n0 0, esti_spec n0 1)) \in estimations. Definition get_esti (n0 : 'I_n) := - pmap (fun (p : id' * R2) => + pmap (fun (p : sumbool_ord m n * R2) => let (i, e) := p in if i == inr n0 then Some e else None). Definition get_esti_spec := forall n0 : 'I_n, diff --git a/ecc_modern/ldpc_algo_proof.v b/ecc_modern/ldpc_algo_proof.v index d2e5bd87..b480871a 100644 --- a/ecc_modern/ldpc_algo_proof.v +++ b/ecc_modern/ldpc_algo_proof.v @@ -137,8 +137,6 @@ Variables (m n : nat) (H : 'M['F_2]_(m, n.+1)). Hypothesis tanner_acyclic : acyclic' (tanner_rel H). Hypothesis tanner_connected : forall a b, connect (tanner_rel H) a b. -Let id' := id m n. (* NB: 'I_m + 'I_n *) - Import GRing.Theory. Local Open Scope ring_scope. @@ -322,14 +320,14 @@ by move /andP/proj2/card_uniqP: Hun => <-. Qed. Lemma build_tree_rec_ok h k i s : - (#|id'| - #|s| <= h)%N -> + (#|sumbool_ord m n.+1| - #|s| <= h)%N -> uniq_path (tanner_rel H) (id_of_kind k i) s -> let l := labels (build_tree_rec H rW h s k i) in forall a b, a \in l -> b \in l -> tanner_rel H a b -> graph (build_tree_rec H rW h s k i) a b. Proof. elim: h k i s => [|h IHh] k i s Hh Hi. - have His: id_of_kind k i \in s by apply seq_full. + have His : id_of_kind k i \in s by exact: seq_full. by rewrite /uniq_path /= His andbF in Hi. move=> l. have Hab b: b \in l -> tanner_rel H (id_of_kind k i) b -> @@ -374,10 +372,10 @@ case Hiab: (ia == ib). rewrite has_map /=. apply /hasP. exists ia. - rewrite select_children_spec; by apply /andP. + by rewrite select_children_spec; exact/andP. rewrite -(eqP Hiab) in Hsb. - apply IHh => //. - by apply card_uniq_seq_decr. + apply: IHh => //. + exact: card_uniq_seq_decr. by apply cons_uniq_path => //; rewrite sym_tanner_rel. set sa := id_of_kind (negk k) ia in Hia Hias. set sb := id_of_kind (negk k) ib in Hib Hibs. @@ -396,10 +394,10 @@ rewrite !lastE Hal. case Hsasb: (sa == sb). move /eqP: Hsasb. rewrite /sa /sb=> eq. - destruct k; inversion eq; by rewrite H1 eqxx in Hiab. + by destruct k; inversion eq; rewrite H1 eqxx in Hiab. move=> Hcy. -move /andP: Hp1 => [Hp1 Hun1]. -move /andP: Hp2 => [Hp2 Hun2]. +move: Hp1 => /andP[Hp1 Hun1]. +move: Hp2 => /andP[Hp2 Hun2]. apply Hcy; clear Hcy Hsasb. rewrite -cat_cons -rev_rcons -{1}Hbl -lastI. rewrite mem_cat mem_rev negb_or. @@ -424,7 +422,8 @@ rewrite -cat1s catA cat_path in Hp1. by case/andP: Hp1. Qed. -Definition tanner_split (s : seq id') : rel id' := +Definition tanner_split (s : seq (sumbool_ord m n.+1)) : + rel (sumbool_ord m n.+1) := fun a b => if (a \in s) || (b \in s) then false else tanner_rel H a b. Lemma tanner_split_tanner s : subrel (tanner_split s) (tanner_rel H). @@ -442,8 +441,8 @@ case Hb: (b \in s); first by rewrite /= orbT orbT. by case: ifP. Qed. -Lemma tanner_rel_split (s : seq id') (x : id') p : - ~~has (mem s) (x::p) -> path (tanner_rel H) x p -> path (tanner_split s) x p. +Lemma tanner_rel_split (s : seq (sumbool_ord m n.+1)) (x : sumbool_ord m n.+1) p : + ~~ has (mem s) (x :: p) -> path (tanner_rel H) x p -> path (tanner_split s) x p. Proof. move: x s. elim: p => //= y p IHp x s Hs /andP[Hx Hp]. @@ -453,7 +452,8 @@ rewrite IHp //. by case/norP: Hs. Qed. -Lemma tanner_split_uncons (s : seq id') (c x : id') p : +Lemma tanner_split_uncons (s : seq (sumbool_ord m n.+1)) + (c x : sumbool_ord m n.+1) p : c \notin (x :: p) -> path (tanner_split s) x p -> path (tanner_split (c :: s)) x p. Proof. @@ -467,7 +467,7 @@ by move /norP/proj2: Hc. Qed. Lemma build_tree_rec_full h k i s : - (#|id'| - #|s| <= h)%N -> + (#|sumbool_ord m n.+1| - #|s| <= h)%N -> uniq_path (tanner_rel H) (id_of_kind k i) s -> mem (labels (build_tree_rec H rW h s k i)) =i connect (tanner_split s) (id_of_kind k i). @@ -483,7 +483,7 @@ case Hai: (a == id_of_kind k i); simpl. apply /connectP. by exists [::]. move/andP: Hc => [] /= Hc Hun. -have Hh': (#|id'| - #|id_of_kind k i :: s| <= h)%N. +have Hh': (#|sumbool_ord m n.+1| - #|id_of_kind k i :: s| <= h)%N. by apply card_uniq_seq_decr. have Hchild o: o \in select_children H s k i -> uniq_path (tanner_rel H) (id_of_kind (negk k) o) (id_of_kind k i :: s). @@ -509,8 +509,8 @@ case Hcb: (connect _ _ a). apply (sub_path (@tanner_split_tanner _)) in Hp. destruct k, s0. by rewrite tanner_relE in Hp. - by exists o. - by exists o. + by eexists; reflexivity. + by eexists; reflexivity. by rewrite tanner_relE in Hp. subst s0. have Ho: o \in select_children H s k i. @@ -558,7 +558,7 @@ by apply Hchild. Qed. Lemma build_tree_full k i a : - a \in labels (build_tree_rec H rW #|id'| [::] k i). + a \in labels (build_tree_rec H rW #|sumbool_ord m n.+1| [::] k i). Proof. rewrite build_tree_rec_full //. rewrite inE. @@ -568,11 +568,10 @@ rewrite build_tree_rec_full //. by rewrite card_sum !card_ord card0 subn0. Qed. -Theorem build_tree_ok : forall k i, - tanner_rel H =2 graph (build_tree H rW (k:=k) i). +Theorem build_tree_ok k i : + tanner_rel H =2 graph (build_tree H rW (k:=k) i). Proof. -rewrite /build_tree. -move=> k i a b. +rewrite /build_tree => a b. case Htan: (tanner_rel H a b). symmetry. apply build_tree_rec_ok with (s:=[::]). @@ -591,7 +590,7 @@ End BuildTreeOk. Section BuildTreeTest. Let m := 2. Let n := 3. -Let id' := id m n.-1. +Let id' := sumbool_ord m n. Import GRing.Theory. Local Open Scope ring_scope. @@ -762,7 +761,7 @@ Let rW n0 := (W 0 (vb ``_ n0), W 1 (vb ``_ n0)). Close Scope ring_scope. -Let id' := id m n'. +Let id' := sumbool_ord m n. Let tn_tree' k := tn_tree id' k R2 R2. @@ -1289,9 +1288,8 @@ Lemma kind_filter {A : eqType} k i (s : {set ord_of_kind m n' (negk k)}) Proof. move=> a inj. rewrite /image_mem /enum_mem /id' /id /=. -have ->: Finite.enum [finType of 'I_m + 'I_n] - = sum_enum [finType of 'I_m] [finType of 'I_n]. - by rewrite unlock /=. +have -> : Finite.enum ('I_m + 'I_n)%type = sum_enum 'I_m 'I_n. + by rewrite unlock. rewrite /sum_enum filter_cat map_cat !filter_map -!map_comp. transitivity [seq ([eta F] \o [eta inj]) i | i <- Finite.enum (ord_of_kind m n' (negk k)) @@ -1303,7 +1301,7 @@ transitivity congr (map _ _). apply eq_filter => x /=; rewrite !inE. case/boolP : (x \in s) => /= Hx; first by rewrite imset_f. -case /boolP: (inj x \in _) => // /imsetP [y Hy] /id_of_kind_inj xy. +case/boolP : (inj x \in _) => // /imsetP [y Hy] /id_of_kind_inj xy. by rewrite xy Hy in Hx. Qed. @@ -1824,9 +1822,8 @@ case Hid: (node_id t == inr n0). congr beta. rewrite /image_mem /enum_mem. apply eq_in_map_seqs => //. - have ->: Finite.enum [finType of 'I_m] = ord_enum m. - by rewrite unlock. - apply eq_filter => x; by rewrite /= !inE /= -VnextE -FnextE. + have -> : Finite.enum 'I_m = ord_enum m by rewrite unlock. + by apply eq_filter => x; rewrite /= !inE /= -VnextE -FnextE. (* inner node *) destruct s; [ | ]; last first. by rewrite tanner_relE in Hun. @@ -1840,7 +1837,7 @@ case Hid: (node_id t == inr n0). rewrite -msg_spec_alpha_beta; last first. rewrite sym_tanner_rel. by move/andP/proj1: Hun => /= /andP/proj1. - rewrite -(big_seq1 beta_op o (fun j => msg_spec' (inl j) (inr i))). + rewrite -(big_seq1 beta_op _ (fun j => msg_spec' (inl j) (inr i))). rewrite -big_cat. apply/perm_big/uniq_perm. - rewrite /= filter_uniq. @@ -1849,8 +1846,8 @@ case Hid: (node_id t == inr n0). - by rewrite enum_uniq. move=> j /=. rewrite in_cons mem_filter /= mem_enum !inE /= -VnextE. - case Hjo: (j == o). - rewrite (eqP Hjo). + case Hjs: (j == s). + rewrite (eqP Hjs). by move/andP/proj1/andP/proj1 : Hun => /=; rewrite -VnextE -FnextE. case Hji: (i \in 'V j) => /=. by rewrite -enumT mem_enum FnextE Hji. @@ -1977,12 +1974,12 @@ rewrite /= in IH. destruct tag0. eapply subseq_trans; [| apply subseq_cons]. rewrite map_flatten -map_comp. - apply (subseq_flatten (f':=labels)) => x Hx. - by apply IH. + apply: (subseq_flatten (f':=labels)) => x Hx. + exact: IH. rewrite /= eqxx. rewrite map_flatten -map_comp. -apply (subseq_flatten (f':=labels)) => x Hx. -by apply IH. +apply: (subseq_flatten (f':=labels)) => x Hx. +exact: IH. Qed. Lemma get_esti_subseq n0 l : diff --git a/lib/vandermonde.v b/lib/vandermonde.v deleted file mode 100644 index aded7f3a..00000000 --- a/lib/vandermonde.v +++ /dev/null @@ -1,454 +0,0 @@ -(* infotheo: information theory and error-correcting codes in Coq *) -(* Copyright (C) 2020 infotheo authors, license: LGPL-2.1-or-later *) -From mathcomp Require Import all_ssreflect ssralg perm zmodp. -From mathcomp Require Import matrix. -Require Import ssralg_ext. - -(******************************************************************************) -(* Vandermonde Matrices *) -(******************************************************************************) - -(* OUTLINE: -- Section vandermonde_matrix. -- Section vandermonde_k_matrix. -- Section vandermonde_determinant. - -*) - -Set Implicit Arguments. -Unset Strict Implicit. -Unset Printing Implicit Defensive. - -Import GRing.Theory. -Local Open Scope ring_scope. -Local Open Scope vec_ext_scope. - -Section vandermonde_matrix. - -Variables (R : ringType) (n : nat) (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. - -Section vandermonde_k_matrix. - -Variable (R : comRingType). - -Let lc n (a : R) (r0 r1 : 'rV[R]_n) := r0 - a *: r1. - -Let 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. - -(* 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 *) -Let 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)). - -Let 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. -Proof. -elim: k => [n0 i ni|k IH]. - move=> M. - case: ifPn => [/eqP ->|n0']. - rewrite /vander_k /= (_ : inord 0 = 0) //. - apply/val_inj => /=; by rewrite inordK. - by rewrite subn0 ni andbT ltnNge ni. -rewrite ltnS => kn i ni M. -case: ifPn => [|i0]. - move/eqP => ?; subst i. - rewrite /vander_k -{2}(add1n k) iotaD rev_cat foldl_cat addn1. - rewrite -subSn // subSS -/(vander_k a _ k) subSS /= /mat_lc. - case: ifP => [|nk0]. - move/eqP => /(congr1 (fun x => nat_of_ord x)) /=. - rewrite inordK; last by rewrite ltnS leq_subr. - move/eqP. - rewrite subn_eq0 => nk. - have ? : n = k by apply/eqP; rewrite eqn_leq kn nk. - by rewrite IH // ltnW. - rewrite rowK eq_sym (_ : inord 0 = 0) //; last first. - apply/val_inj => /=; by rewrite inordK. - rewrite nk0 -(_ : inord 0 = 0) //; last first. - apply/val_inj => /=. - by rewrite inordK. - rewrite IH //; last by rewrite ltnW. - rewrite eqxx (_ : inord 0 = 0) //. - apply/val_inj => /=. - by rewrite inordK. -rewrite {1}/vander_k -{2}(add1n k) iotaD rev_cat foldl_cat. -rewrite addn1 -subSn // subSS -/(vander_k a _ k) subSS /= /mat_lc. -case: ifP => [|nk0]. - move/eqP/(congr1 (fun x => nat_of_ord x)) => /=. - rewrite inordK //; last by rewrite ltnS leq_subr. - move/eqP. - rewrite subn_eq0 => nk. - have ? : n = k by apply/eqP; rewrite eqn_leq kn nk. - subst k. - by rewrite subnn leq0n /= ni IH // (negbTE i0) subSn // subnn lt0n i0 ni. -rewrite rowK. -case: ifPn => [|nik]. - move/eqP => /(congr1 (fun x => nat_of_ord x)) /=. - rewrite inordK; last by rewrite ltnS. - rewrite inordK; last by rewrite ltnS leq_subr. - move/eqP => ink. - rewrite -(eqP ink) leqnn /= ni IH //; last by rewrite ltnW. - rewrite (negbTE i0) {1}(eqP ink). - case: ifPn. - case/andP. - by rewrite leq_subLR subnKC // ltnn. - rewrite ni andbT -ltnNge => ok. - rewrite {1}IH; last first. - by apply: (leq_trans (@leq_pred _) ni). - by rewrite ltnW. - case: ifPn => [Hi1|Hi1]. - rewrite (eqP Hi1) (_ : inord 0 = 0) //. - apply/val_inj => /=. - by rewrite inordK. - case: ifP => //. - case/andP. - rewrite {1}(eqP ink) -subnS subSn // subnS => abs. - exfalso. - move: abs. - by rewrite ltnNge => /negP; rewrite leq_pred. -rewrite ni andbT. -case: ifPn => nki. - rewrite /lc IH //; last by rewrite ltnW. - rewrite (negbTE i0) ni andbT. - case: ifPn => [nki' //|]. - rewrite -ltnNge subSn // ltnS => abs. - have abs' : (i = n - k)%N by apply/eqP; rewrite eqn_leq nki abs. - exfalso. - move/eqP : nik; apply. - apply/val_inj => /=. - by rewrite inordK // inordK // ltnS leq_subr. -rewrite IH //; last by rewrite ltnW. -rewrite (negbTE i0) ni andbT. -case: ifP => // abs. -exfalso. -rewrite -ltnNge in nki. -rewrite subSn // in abs. -by move: (ltn_trans nki abs); rewrite ltnn. -Qed. - -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. - -Lemma vander_lastE n (a : 'rV[R]_n.+1) : vander_last a = vander_k a (vander a) n. -Proof. -apply/row_matrixP => i. -rewrite {2}(_ : i = inord i); last first. - apply/val_inj => /=. - by rewrite inordK. -rewrite vander_k_rec //; last by rewrite -ltnS. -case: ifPn => i0. - rewrite /vander_last. - apply/rowP => j. - rewrite !mxE. - case: ifP => //. - move/eqP => abs; exfalso. - apply abs. - apply/val_inj => /=. - by move/eqP : i0. -rewrite subSn // subnn lt0n i0 /= -ltnS ltn_ord /= /lc /vander_last; apply/rowP => j. -rewrite !mxE. -case: ifP => [|i0']. - move/eqP/(congr1 (fun x => nat_of_ord x)) => /= abs; exfalso. - move/eqP : i0; by apply. -case: ifP => [|j0]. - move=> /eqP ->. - rewrite -exprS inordK // inordK; last first. - by rewrite (leq_trans _ (ltn_ord i)) // ltnS leq_pred. - rewrite prednK; last first. - by rewrite lt0n. - by rewrite (_ : 0 = ord0) // subrr. -rewrite inordK // inordK // (ltn_trans _ (ltn_ord i)) // -subn1. -by rewrite -{2}(subn0 i) ltn_sub2l // lt0n. -Qed. - -Let 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. -Proof. -apply/row_matrixP => i. -rewrite (_ : i = inord i); last first. - apply/val_inj => /=. - by rewrite inordK. -rewrite vander_k_rec //; last by rewrite -ltnS. -case: ifPn => i0. - by rewrite (eqP i0) vander_k_rec // leq_pred. -rewrite subnn leq0n -ltnS ltn_ord /=. -rewrite vander_k_rec ?leq_pred //; last by rewrite -ltnS ltn_ord. -rewrite (negbTE i0) -(ltnS i) ltn_ord andbT. -by rewrite /= subSn // subnn lt0n i0. -Qed. - -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). -Proof. -move=> kn. -destruct k as [|k] => //=. -rewrite /lc /= (@determinant_multilinear _ _ _ - (\matrix_i (if i == inord (n.+1 - k.+1) then row (inord i) (vander_k a M k) else row (inord i) (vander_k a M k.+1))) - (\matrix_i (if i == inord (n.+1 - k.+1) then row (inord i.-1) (vander_k a M k) else row (inord i) (vander_k a M k.+1))) - (inord (n.+1 - k.+1)) 1 (- a``_ord0)); last 3 first. - rewrite scale1r !rowK eqxx vander_k_rec //; last first. - by rewrite subSS leq_subr. - by rewrite ltnW. - rewrite subSS. - rewrite leq_subr andbT subn_eq0. - case: ifPn => [nk|]. - by move: (leq_ltn_trans nk kn); rewrite ltnn. - rewrite -ltnNge => kn'. - rewrite leqnn /lc inordK; last by rewrite ltnS leq_subr. - rewrite vander_k_rec //; last 2 first. - rewrite ltnW //; by apply: (ltn_trans kn'). - by rewrite leq_subr. - rewrite subn_eq0 leqNgt kn' /= leq_subr andbT leq_subLR addnBA; last first. - by rewrite ltnW. - rewrite addnC. - rewrite -addnBA // subnn addn0 ltnn vander_k_rec //; last 2 first. - by rewrite ltnW // ltnS ltnW. - by rewrite -subnS leq_subr. - rewrite -subnS subn_eq0. - rewrite ltnS in kn, kn'. - case: ifPn. - rewrite -subn_eq0 => /eqP ->. - rewrite (_ : inord 0 = 0) // ?scaleNr //. - apply/val_inj => //=. - by rewrite inordK. - rewrite -ltnNge => k1n. - case: ifPn => //. - case/andP. - rewrite subnS subSn; last by rewrite ltnW. - by rewrite ltnNge leq_pred. - by rewrite scaleNr. - apply/matrixP => i j; by rewrite !mxE eq_sym (negbTE (neq_lift _ _)) mxE inord_val. - apply/matrixP => i j; by rewrite !mxE eq_sym (negbTE (neq_lift _ _)) mxE inord_val. -rewrite mul1r (_ : \matrix_i _ = vander_k a M k); last first. - apply/matrixP => i j; rewrite !mxE. - case: ifPn => [/eqP Hi|Hi]. - rewrite !mxE (_ : inord i = i) //. - apply/val_inj => /=. - by rewrite inordK. - rewrite vander_k_rec //; last first. - by rewrite -ltnS. - by rewrite ltnW. - case: ifPn => i0. - transitivity ((row (inord i) (vander_k a M k)) 0 j); last first. - rewrite mxE (_ : inord i = i) //. - apply/val_inj => /=. - by rewrite inordK. - rewrite vander_k_rec //; last 2 first. - by rewrite (leq_trans _ kn) // -addn2 leq_addr. - by rewrite -ltnS. - by rewrite i0. - rewrite -(ltnS i) ltn_ord andbT. - case: ifPn => nki. - rewrite /lc. - transitivity ((row (inord i) (vander_k a M k)) 0 j); last first. - rewrite mxE (_ : inord i = i) //. - apply/val_inj => /=. - by rewrite inordK. - rewrite vander_k_rec //; last 2 first. - by rewrite ltnW // ltnW. - by rewrite -ltnS. - rewrite (negbTE i0) -(ltnS i) ltn_ord andbT. - have {nki} : n.+1 - k.+1 < i. - rewrite ltn_neqAle nki andbT. - apply: contra Hi => /eqP ->. - apply/eqP/val_inj => /=. - by rewrite inordK //. - rewrite subnS -ltnS prednK; last by rewrite lt0n subn_eq0 -ltnNge ltnW. - by rewrite ltnS => ->. - transitivity ((row (inord i) (vander_k a M k)) 0 j); last first. - rewrite mxE (_ : inord i = i) //. - apply/val_inj => /=. - by rewrite inordK. - rewrite vander_k_rec //; last 2 first. - by rewrite ltnW // ltnW. - by rewrite -ltnS. - rewrite (negbTE i0) -(ltnS i) ltn_ord andbT. - have /negbTE -> // : ~~ (n.+1 - k <= i). - apply: contra nki. - apply: leq_trans. - rewrite leq_subLR addnC. - destruct n as [|n] => //. - rewrite subSn; last by rewrite -ltnS ltnW. - by rewrite addSn addnS subnK // -ltnS ltnW. -rewrite (_ : \det (\matrix_i _) = 0) ?mulr0 ?addr0 //. -have H : inord (n.+1 - k.+1) != inord (n.+1 - k.+2) :> 'I_n.+1. - apply/eqP => /(congr1 (fun x => nat_of_ord x)) /=. - rewrite 2!subSS. - rewrite inordK // ?ltnS ?leq_subr //. - rewrite inordK // ?ltnS ?leq_subr //. - destruct n as [|n] => //. - rewrite !subSS. - move/(congr1 (fun x => x + k)%N). - rewrite subnK; last by rewrite ltnW. - rewrite addnC addnBA // addnC. - rewrite addnK -{2}(addn0 n). - rewrite -addn1 => /eqP. - by rewrite eqn_add2l. -apply (@determinant_alternate _ _ _ (inord (n.+1 - k.+1)) (inord (n.+1 - k.+2))) => //. -move=> i. -rewrite !mxE eqxx eq_sym (negbTE H) 2!subSS. -rewrite inordK; last by rewrite ltnS leq_subr. -rewrite inordK; last by rewrite ltnS leq_subr. -rewrite -subnS [in LHS]vander_k_rec // ?leq_subr //; last by rewrite ltnW // ltnW. -rewrite subn_eq0. -case: ifPn => // nk2. - rewrite (_ : n - k.+1 = 0)%N //; last by apply/eqP; rewrite subn_eq0. - by rewrite vander_k_rec // ltnW // ltnW. -rewrite andbT (_ : _ <= _ = false); last first. - rewrite -(leq_add2r k.+1) subnK //. - rewrite addnC addnBA; last by rewrite ltnW // ltnW. - rewrite addnC -addnBA; last by rewrite -addn1 leq_addr. - rewrite subSn // subnn // addn1. - apply/negbTE. - by rewrite -leqNgt. -rewrite [in RHS]vander_k_rec // ?leq_subr //; last by rewrite ltnW. -rewrite subn_eq0 (negbTE nk2) andbT (_ : _ <= _ = false) //. -rewrite -(leq_add2r k.+1) subnK //; last by rewrite ltnW. -by rewrite subnK ?ltnn. -Qed. - -Let 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). -Proof. -rewrite leq_eqVlt => /orP[/eqP ->|]; - by [rewrite vander_k_max | apply det_vander_k_rec]. -Qed. - -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). -Proof. -elim: k => // k IH. -rewrite ltnS => kn. -by rewrite det_vander_k // IH // ltnW. -Qed. - -End vandermonde_k_matrix. - -Section vandermonde_determinant. - -Variable (R : comRingType). - -Let 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)). -Proof. -elim: k => [_|k IH]; first by rewrite big_ord0 mul1r. -rewrite ltnS => kn. -rewrite IH; last by rewrite ltnW. -rewrite big_ord_recr /= -mulrA; congr (_ * _). -rewrite (@determinant_multilinear _ _ _ (\matrix_(j, i) (f i j * (if k < j then g j else 1))) (\matrix_(j, i) (f i j * (if k <= j then g j else 1))) (inord k) (g (inord k)) 0); last 3 first. - rewrite scale0r addr0. - apply/rowP => j. - rewrite !mxE mulrCA; congr (_ * _). - by rewrite inordK // leqnn ltnn mulr1. - apply/matrixP => i j; rewrite !mxE. - case: ifPn => [H1|]. - case: ifP => // /negbT; by rewrite leq_eqVlt H1 orbT. - case: ifPn => //; rewrite -ltnNge ltnS => H1 H2. - rewrite mulr1. - have /eqP abs : k = lift (inord k) i by apply/eqP; rewrite eqn_leq H1 H2. - exfalso. - move/eqP : abs; apply/eqP. - apply: contra (@neq_lift _ (inord k) i) => /eqP {1}->. - apply/eqP/val_inj; by rewrite inord_val. - apply/matrixP => i j; by rewrite !mxE. -rewrite mul0r addr0 -det_tr. -rewrite (_ : _^T = \matrix_(i, j) (f i j * (if k < j then g j else 1))) //. -by apply/matrixP => i j; rewrite !mxE. -Qed. - -Let 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)). -Proof. -destruct n as [|n]; first by rewrite big_ord0 mul1r !det_mx00. -rewrite -det_tr (_ : _^T = (\matrix_(j, i) (f i j * g j))); last first. - by apply/matrixP => i j; rewrite !mxE. -rewrite (@det_mlinear_rec _ _ _ n.+1) //; congr (_ * _). - apply eq_bigr => i _; by rewrite inord_val. -rewrite -det_tr; congr (\det _). -apply/matrixP => i j; by rewrite !mxE ltnNge -ltnS ltn_ord /= mulr1. -Qed. - -Let 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). -Proof. -transitivity (\det (vander_last a)); first by rewrite vander_lastE /= det_vander_k_vander. -rewrite /vander_last (expand_det_col _ ord0) /= (bigD1 ord0) //=. -rewrite [X in _ + X = _](_ : _ = 0) ?addr0; last first. - rewrite (eq_bigr (fun=> 0)); first by rewrite big_const iter_addr0. - move=> i i0; by rewrite !mxE (negbTE i0) /= mul0r. -rewrite mxE /= mul1r /cofactor expr0 mul1r. -transitivity (\det (\matrix_(i < n, j < n) ((\row_(i < n) a``_(inord i.+1))``_j ^+ i.+1 - a``_0 * (\row_(i < n) a``_(inord i.+1))``_j ^+ i))). - congr (\det _). - apply/matrixP => i j; rewrite !mxE. - do 2 rewrite eq_sym (negbTE (neq_lift _ _)). - rewrite !lift0 /=; congr (a ``_ _ ^+ _ - _ * a ``_ _ ^+ _); - by apply/val_inj; rewrite -lift0 inord_val. -transitivity (\det (\matrix_(i < n, j < n) ((\row_(i < n) a``_(inord i.+1))``_j ^+ i * ((\row_(i < n) a``_(inord i.+1))``_j - a``_0)))). - congr (\det _). - apply/matrixP => i j; by rewrite !mxE exprS -mulrBl mulrC. -transitivity ((\prod_(j < n) (a``_(inord j.+1) - a``_0)) * \det (\matrix_(i < n, j < n) ((\row_(i < n) a``_(inord i.+1))``_j ^+ i))). - rewrite det_mlinear; congr (_ * _). - by apply/eq_bigr => j _; rewrite mxE. -rewrite mulrC; congr (_ * _). -rewrite (big_addn 0 n.+1 1) subn1 /= big_mkord; apply/eq_bigr => i _; by rewrite addn1. -Qed. - -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)). -Proof. -elim: n a => [a|n IH a]. - rewrite (mx11_scalar (vander a)) det_scalar1 mxE expr0 big_ord_recr /=. - rewrite big_ord0 mul1r (eq_bigl (xpred0)) ?big_pred0 // => i; by rewrite ord1. -rewrite det_vander_rec IH. -rewrite (eq_bigr (fun i : 'I_n.+1 => \prod_(1 <= j < n.+2 | i < j.-1) - (a``_(inord j) - a``_(inord i.+1)))); last first. - move=> i _; rewrite (big_addn O n.+2 1) subn1 /= big_mkord. - apply/eq_big; first by move=> ?; rewrite addn1. - move=> *; by rewrite 2!mxE addn1. -rewrite [in RHS]big_ord_recl [in RHS]mulrC; congr (_ * _); last first. - rewrite [in RHS]big_mkcond /= [in RHS]big_ord_recl ltnn mul1r big_add1. - rewrite big_mkord; apply/eq_bigr => i _; congr (a ``_ _ - _). - by apply/val_inj => /=; rewrite inordK // ltnS. -apply eq_bigr => i _. -rewrite [in RHS]big_mkcond /= [in RHS]big_ord_recl ltn0 mul1r big_add1. -rewrite big_mkord [in LHS]big_mkcond /=; apply eq_bigr => j _; rewrite /bump. -rewrite 2!leq0n 2!add1n ltnS; case: ifPn => // ij. -by congr (a ``_ _ - a ``_ _); apply val_inj => /=; rewrite inordK // ltnS. -Qed. - -End vandermonde_determinant. - -Notation Vandermonde r a := (vander_gen a r). - -Lemma det_Vandermonde (R: comRingType) (n:nat) (a: 'rV[R]_n) : - \det (Vandermonde n a) = \prod_(i < n) \prod_(j < n | i < j) (a 0 j - a 0 i). -Proof. - case: n a => [a|n a]; first by rewrite det_mx00 big1 // => -[] []. - exact: det_vander. -Qed.