fixes #69 (#119)

_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

ecc_classic/alternant.v

@@ -3,7 +3,7 @@
 From mathcomp Require Import all_ssreflect ssralg finalg poly polydiv.
 From mathcomp Require Import cyclic perm matrix mxpoly vector mxalgebra zmodp.
 From mathcomp Require Import finfield falgebra fieldext.
-Require Import ssr_ext ssralg_ext vandermonde linearcode.
+Require Import ssr_ext ssralg_ext linearcode.
 Require Import dft poly_decoding grs bch.
 
 (******************************************************************************)

ecc_classic/bch.v

@@ -3,7 +3,7 @@
 From mathcomp Require Import all_ssreflect ssralg poly polydiv finalg zmodp.
 From mathcomp Require Import matrix mxalgebra mxpoly vector fieldext finfield.
 Require Import ssralg_ext hamming linearcode decoding cyclic_code poly_decoding.
-Require Import vandermonde dft euclid grs f2.
+Require Import dft euclid grs f2.
 
 (******************************************************************************)
 (*                        Binary BCH codes                                    *)
@@ -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

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).

ecc_classic/mceliece.v

@@ -35,9 +35,9 @@ Variable CSM : 'M['F_2]_(n - k, k).
 Local Notation "'H" := (Syslcode.PCM Hdimlen CSM).
 Local Notation "'G" := (Syslcode.GEN Hdimlen CSM).
 Let encode := Syslcode.encode Hdimlen CSM.
-Let discard := @Syslcode.discard [finFieldType of 'F_2] _ _ Hdimlen.
+Let discard := @Syslcode.discard 'F_2 _ _ Hdimlen.
 
-Variable repair : repairT [finType of 'F_2] [finType of 'F_2] n.
+Variable repair : repairT 'F_2 'F_2 n.
 Variable repair_img : oimg repair \subset kernel 'H.
 Variable encode_discard : cancel_on (kernel 'H) encode discard.
 

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.

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,32 +220,32 @@ 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
   end.
 
 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,22 +327,22 @@ 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
   end.
 
 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,