proposition: Lemma RS_enc_injective : injective (enc RS_code).
proof: Proof. move=> x1 x2 /=. rewrite /encoder 2!ffunE => x1x2. suff H : rVpoly x1 * 'X^d.+1 = rVpoly x2 * 'X^d.+1. rewrite -(rVpolyK x1) -(rVpolyK x2). have : (rVpoly x1 * 'X^d.+1) %/ 'X^d.+1 = (rVpoly x2 * 'X^d.+1) %/ 'X^d.+1 by rewrite H. rewrite mulpK; last by rewrite -size_poly_gt0 size_polyXn. rewrite mulpK; last by rewrite -size_poly_gt0 size_polyXn. by move=> ->. apply/eqP. rewrite -subr_eq0 -mulrBl. suff : ((rVpoly x1 - rVpoly x2) == 0) && ((rVpoly x2 * 'X^d) %% \gen_(a, d) - (rVpoly x1 * 'X^d) %% \gen_(a, d) == 0). case/andP => /eqP ->; by rewrite mul0r. have H1 : size ((rVpoly x2 * 'X^d) %% \gen_(a, d)) < d.+1. by rewrite -[in X in _ < X](size_rs_gen a d) ltn_modp gen_neq0. have H2 : size ((rVpoly x1 * 'X^d) %% \gen_(a, d)) < d.+1. by rewrite -[in X in _ < X](size_rs_gen a d) ltn_modp gen_neq0. rewrite -(@rreg_div0 _ _ _ 'X^d). - rewrite mulrBl -(opprB (_ %% _)). rewrite (_ : forall a b c d, a - b - (c - d) = (a - c) + (d - b)); last first. move=> *. rewrite -2!addrA; congr (_ + _). rewrite addrA addrC opprD; congr (_ - _). by rewrite opprK. rewrite addr_eq0 opprB -subr_eq0. move/eqP : x1x2. rewrite -[in X in X -> _]subr_eq0 -linearB /= => /poly_rV_0_inv; apply. rewrite (leq_trans (size_add _ _)) // size_opp geq_max. have H : forall x : 'rV[F]_(n - d.+1).+1, size (rVpoly x * 'X^d) <= n. move=> x. apply (leq_trans (size_mul_leq _ _)). rewrite size_polyXn addnS /=. rewrite (@leq_trans ((n - d.+1).+1 + d)) //. by rewrite leq_add2r size_poly. move: dn; rewrite /RS.redundancy_ub => ?. by rewrite subnS prednK // ?subn_gt0 // subnK // ltnW. apply/andP; split; rewrite (leq_trans (size_add _ _)) // geq_max size_opp H /=. by rewrite (leq_trans _ dn) // ltnW. by rewrite (leq_trans _ dn) // ltnW. - rewrite lead_coefXn; exact: GRing.rreg1. - rewrite size_polyXn ltnS (leq_trans (size_add _ _)) //. rewrite geq_max size_opp /=; apply/andP; split; by rewrite -ltnS. Qed.
imports: mathcomp(all_ssreflect ssralg finalg poly polydiv cyclic) mathcomp(perm matrix mxpoly vector mxalgebra zmodp) ssr_ext ssralg_ext poly_ext channel_code decoding linearcode hamming dft poly_decoding euclid grs cyclic_code