port completed

ecc_classic/alternant.v

@@ -54,7 +54,7 @@ Section injection_into_extension_field.
 
 Variables (F0 : finFieldType) (F1 : fieldExtType F0).
 
-Definition ext_inj : {rmorphism F0 -> F1} := @GRing.in_alg_rmorphism F0 F1.
+Definition ext_inj : {rmorphism F0 -> F1} := @GRing.in_alg F1.
 
 Definition ext_inj_tmp : {rmorphism F0 -> (FinFieldExtType F1)} := ext_inj.
 

ecc_classic/bch.v

@@ -158,7 +158,7 @@ Section BCH_def.
 Variables (n : nat) (m : nat).
 
 Definition code (a : 'rV_n) t :=
-  Rcode.t (@GF2_of_F2_rmorphism m) (kernel (PCM a t)).
+  Rcode.t (@GF2_of_F2 m) (kernel (PCM a t)).
 
 End BCH_def.
 

ecc_classic/grs.v

@@ -72,7 +72,7 @@ Qed.
 
 Definition syndromep r y := \poly_(l < r) (syndrome_coord l y).
 
-Lemma syndomepE r y :
+Lemma syndromepE r y :
   syndromep r y = \sum_(i in supp y)
      (y ``_ i * b ``_ i)%:P * (\sum_(l < r) (a ``_ i ^+ l)%:P * 'X^l).
 Proof.
@@ -221,11 +221,14 @@ case/boolP : (r == O) => r0.
   rewrite -scalerAl mulrC mul_polyC; congr (_ *: (_ *: _)).
   apply eq_bigl => k; by rewrite in_setD1 andbC.
 rewrite /GRS_mod big_distrl /= /Omega /erreval -big_split /=.
-rewrite GRS.syndomepE big_distrr /=.
+rewrite GRS.syndromepE big_distrr /=.
 apply eq_bigr => i iy.
 rewrite -3!scalerAl -scalerA -scalerDr.
 rewrite polyCM -!mulrA mulrCA !mulrA mul_polyC -!scalerAl; congr (_ *: _).
-rewrite /Sigma /errloc (bigD1 i) //= mulrC -!mulrA mulrBl mul1r.
+rewrite /Sigma /errloc.
+rewrite (bigD1 i) //=.
+rewrite (mulrC (1 - a ``_ i *: 'X)).
+rewrite -!mulrA mulrBl mul1r.
 set x := (X in _ * X = _).
 rewrite (_ : x = (b ``_ i)%:P * (1 - (a ``_ i ^+ r)%:P * 'X^r)); last first.
   rewrite /x mulrCA -mulrBr big_distrr /= -sumrB.
@@ -241,7 +244,7 @@ rewrite (_ : x = (b ``_ i)%:P * (1 - (a ``_ i ^+ r)%:P * 'X^r)); last first.
     rewrite -!scalerAl mulrCA -exprS !scalerAl; congr (_ * _).
     by rewrite -mul_polyC -polyCM -exprS.
   by rewrite -mulrCA -scalerAl -exprS 2!mul_polyC scalerA -exprSr.
-rewrite mulrA mulrBr mulr1 mulrC -mul_polyC; congr (_ * _ + _).
+rewrite [in LHS]mulrA mulrBr mulr1 mulrC -mul_polyC; congr (_ * _ + _).
  apply/eq_bigl => j; by rewrite in_setD1 andbC.
 rewrite -mulNr !mulrA; congr (_ * _).
 by rewrite -mulNr -mulrA mulrC -!mulrA.

ecc_classic/reed_solomon.v

@@ -167,7 +167,7 @@ rewrite {}/tmp (exchange_big_dep xpredT) //=; apply eq_bigr => j _; rewrite !mxE
 have @i' :  'I_d.
   by apply (@Ordinal _ i); rewrite (leq_trans (ltn_ord i)).
 rewrite (bigD1 i') //= coefXn insubT //= => Hj.
-rewrite eqxx mulr1 (_ : Ordinal Hj = j); last by apply val_inj.
+rewrite eqxx mulr1 (_ : Sub _ _ = j); last by apply val_inj.
 rewrite mxE inordK; last by rewrite ltnS (leq_trans (ltn_ord i)).
 rewrite mulrC; apply/eqP.
 rewrite addrC -subr_eq subrr; apply/eqP/esym.
@@ -444,10 +444,10 @@ Proof.
 move=> an c0 Hc.
 have a_neq0 := primitive_uroot_neq0 an.
 rewrite -(wH_phase_shift a_neq0 _ d).
-apply: (@BCH_argument_lemma _ _ (@GRing.idfun_rmorphism F) _ RS_Hchar _ an
+apply: (@BCH_argument_lemma _ _ idfun _ RS_Hchar _ an
   (phase_shift a c d.+1) _ dn).
   by rewrite -wH_eq0 wH_phase_shift // wH_eq0.
-rewrite (_ : \row_i0 (GRing.idfun_rmorphism F) ((phase_shift a c d.+1) ``_ i0) =
+rewrite (_ : \row_i0 idfun ((phase_shift a c d.+1) ``_ i0) =
   phase_shift a c d.+1); last by apply/rowP => i; rewrite !mxE.
 apply (dft_shifting a_neq0 (prim_expr_order an) dn) => i /andP[ir1 ir2].
 have {Hc} : c \in RS.codebook a n' d by rewrite -(RS.lcode0_codebook a dn) inE.
@@ -467,7 +467,7 @@ move/poly_rV_0_inv; apply; by rewrite size_rs_gen.
 Qed.
 
 Lemma PCM_lin1_mx :
-  RS.PCM a n d = (lin1_mx (linfun (lin_syndrome (RS.PCM a n d))))^T.
+  RS.PCM a n d = (lin1_mx (linfun (syndrome (RS.PCM a n d))))^T.
 Proof.
 apply/matrixP => i j.
 rewrite !(mxE,lfunE) (bigD1 j) //= !mxE !eqxx mulr1 (eq_bigr (fun=> 0)).
@@ -892,7 +892,7 @@ by rewrite -RS.lcode0_codebook // ?inE.
 Qed.
 
 Definition RS_as_lcode (an1 : a ^+ n = 1) (Hchar : ([char F]^').-nat n) :
-  Lcode.t _ _ _ [finType of 'rV_(n - d.+1).+1] :=
+  Lcode.t _ _ _ 'rV_(n - d.+1).+1 :=
     @Lcode.mk _ _ _ _ _
       (Encoder.mk RS_enc_injective RS_enc_img)
       (Decoder.mk (RS_repair_img an1 Hchar) RS_discard)