proposition: Lemma BCH_repair_is_correct (C : BCH.code (rVexp a n) t) : not_uroot_on a n -> t.-BDD (C, BCH_repair).
proof: Proof. move=> a_not_uroot c e. set y := c + e. set r0 : {poly F} := 'X^t.*2. set r1 := \BCHsynp_(rVexp a n, y, t). set vj := Euclid.v r0 r1 (stop t r0 r1). move=> Hc et. set r : {poly F} := \BCHomega_(rVexp a n, twisted a (F2_to_GF2 m e)). have H1 := distinct_non_zero_rVexp a_neq0 a_not_uroot. rewrite /BCH_repair. have syn_c : \BCHsynp_(rVexp a n, c, t) = 0. move/(proj1 (Rcode.P C _)) : Hc. by rewrite mem_kernel_syndrome0 BCH_syndrome_synp // => /eqP ->. have syn_y_e : \BCHsynp_(rVexp a n, y, t) = \BCHsynp_(rVexp a n, e, t). rewrite {1}/BCH.syndromep /F2_to_GF2 map_mxD syndromepD. by rewrite -!/(BCH.syndromep _ _ _) syn_c add0r. rewrite ffunE. case: ifPn => syn_y. suff e0 : e = 0 by rewrite /y e0 addr0. apply/eqP/negPn/negP => e0. move: et. apply/negP. rewrite -ltnNge (@BCH_min_dist1 _ _ _ H1 _ _ e0 _ C) //. rewrite (_ : e = y - c); last by rewrite /y addrAC subrr add0r. apply Lcode0.aclosed => //; last by rewrite Lcode0.oclosed. apply: (proj2 (Rcode.P C _)). by rewrite mem_kernel_syndrome0 BCH_syndrome_synp. have size_r1 : size r1 <= size ('X^t.*2 : {poly F}). by rewrite /r1 /BCH.syndromep size_polyXn (leq_trans (size_syndromep _ _ _)). have eqn : \sigma_(rVexp a n, F2_to_GF2 m e) * r1 = r + - - BCH_mod (F2_to_GF2 m e) * 'X^t.*2. by rewrite opprK -(BCH_key_equation e) /r1 syn_y_e. have size_sigma : size \sigma_(rVexp a n, F2_to_GF2 m e) <= t.+1. by rewrite (leq_trans (size_errloc _ _)) // ltnS supp_F2_to_GF2 -wH_card_supp. have size_r : size r <= t. move: et. rewrite /r wH_card_supp -(@supp_F2_to_GF2 _ m _) -(supp_twisted a_neq0) => et'. by rewrite (leq_trans (size_erreval (rVexp a n) (Errvec et') _)). have deg : (t.+1 + t)%N = size ('X^t.*2 : {poly F}). by rewrite size_polyXn addSn addnn. have cop : coprimep \sigma_(rVexp a n, F2_to_GF2 m e) r. have tmp : (forall i, ((const_mx 1) : 'rV[F]_n) ``_ i != 0 :> F). by move=> ?; rewrite mxE ?oner_neq0. rewrite /r errloc_twisted; by apply: (coprime_errloc_erreval H1 tmp). case: (solve_key_equation_coprimep size_r1 (errloc_neq0 _ _) syn_y eqn size_sigma size_r deg cop) => [l [l0 [Hvj _]]]. by rewrite -(@BCH_err_is_correct _ l e) // -addrA F2_addmx addr0 syn_c eqxx. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv finalg zmodp) mathcomp(matrix mxalgebra mxpoly vector fieldext finfield) ssralg_ext hamming linearcode decoding cyclic_code poly_decoding vandermonde dft euclid grs f2