proposition: Lemma BCH_min_dist1 t x (x0 : x != 0) (t0 : 0 < t) (C : BCH.code a t) : x \in C -> t < wH x.
proof: Proof. move/(proj1 (Rcode.P C _)). rewrite mem_kernel_syndrome0 BCH.PCM_altP // => /eqP H. rewrite leqNgt; apply/negP => abs. have /eqP : #| wH_supp x | = (wH x).-1.+1. by rewrite card_wH_supp prednK // lt0n wH_eq0. rewrite cardE => supp_wH. have Hinj : injective [ffun i : 'I_(wH x).-1.+1 => tnth (Tuple supp_wH) i]. move=> /= i j. rewrite !ffunE /tnth /= => /eqP. rewrite (set_nth_default (tnth_default (Tuple supp_wH) j)) //; last first. rewrite -cardE card_wH_supp; move: i; by rewrite prednK // lt0n wH_eq0. rewrite nth_uniq ?enum_uniq //. by move/eqP/val_inj. rewrite -cardE card_wH_supp; move: i; by rewrite prednK // lt0n wH_eq0. rewrite -cardE card_wH_supp; move: j; by rewrite prednK // lt0n wH_eq0. set f := finfun (tnth (Tuple supp_wH)). move=> [:tmp]. have @f' : 'I_n -> 'I_(wH x).-1.+1. move=> i. set tmp' := fun i => if x ``_ i != 0 then index i (enum (wH_supp x)) else O. refine (@Ordinal _ (tmp' i) _). move: i. abstract: tmp. move=> i. case: ifP => // H'. by rewrite -(eqP supp_wH) index_mem mem_enum -mem_wH_supp. have f'K : forall j, x ``_ j != 0 -> f (f' j) = j. move=> i xj. by rewrite ffunE /tnth /= xj nth_index // mem_enum -mem_wH_supp. have Hf : \sum_(i < (wH x).-1.+1) (GF2_of_F2 x``_(f i)) *: col (f i) (BCH.PCM_alt a t) = 0 :> 'cV__. move/(congr1 trmx) : H; rewrite trmx0 => H. rewrite -[RHS]H. apply/colP => i. rewrite ![in RHS]mxE ![in LHS]summxE [in RHS](bigID (fun j => x ``_ j == 0)). rewrite /= [X in _ = X + _](_ : _ = 0) ?add0r; last first. rewrite (eq_bigr (fun x=> 0)); last first. by move=> j /eqP xj0; rewrite !mxE xj0 rmorph0 mulr0. by rewrite big_const iter_addr0. have ? : (wH x).-1.+1 <= n by rewrite -ltnS prednK ?lt0n ?wH_eq0 // ltnS max_wH. rewrite [in RHS](reindex_onto (fun x => f x) f' f'K) /= [in RHS]big_mkcond /=. apply/eq_bigr => j _. case: ifPn => [_|]; first by rewrite!mxE mulrC. rewrite negb_and negbK. case/orP => [/eqP ->|abs']; first by rewrite rmorph0 scale0r mxE. case/boolP : (x ``_ (f j) == 0) => [/eqP ->|abs'']. by rewrite rmorph0 scale0r mxE. exfalso. move/eqP: abs'; apply. rewrite /f'; apply/val_inj => /=. rewrite abs'' /f ffunE /tnth /= index_uniq //. by rewrite -cardE card_wH_supp -[in X in _ < X](@prednK (wH x)) // lt0n wH_eq0. by rewrite enum_uniq. set r' := (wH x).-1. have Hr' : r'.+1 < t.*2. by rewrite /r' prednK // ?lt0n ?wH_eq0 // (leq_trans abs) // -addnn -{1}(add0n t) ltn_add2r. have {}Hf : \sum_(i < r'.+1) GF2_of_F2 x ``_ (f i) *: \col_(j < r'.+1) (BCH.PCM_alt a t (widen_ord (ltnW Hr') j) (f i)) = 0. apply/colP => j. rewrite mxE summxE. move/colP : Hf => /(_ (widen_ord (ltnW Hr') j)). rewrite !mxE summxE => Hf. rewrite -[RHS]Hf. apply eq_bigr => /= i _; by rewrite !mxE. have /negP := det_B_neq0 Hr' Hinj. rewrite -det_tr; apply. apply/det0P; exists (\row_i GF2_of_F2 x ``_ (f i)). suff -> : \row_i GF2_of_F2 x ``_ (f i) = const_mx 1. apply/eqP => /rowP/(_ 0). rewrite !mxE; apply/eqP; exact: oner_neq0. move=> n0; apply/rowP => k. rewrite !mxE /f ffunE /tnth /=. have -> : forall i, i \in (enum (wH_supp x)) -> x ``_ i = 1. by move=> /= i; rewrite mem_enum inE -f2.F2_eq1 => /eqP. by rewrite rmorph1. apply/(nthP (tnth_default (Tuple supp_wH) k)); exists k => //. rewrite -cardE card_wH_supp. move: (ltn_ord k); by rewrite {2}prednK // lt0n wH_eq0. apply/rowP => i; rewrite !mxE. move/colP : Hf => /(_ i). rewrite !mxE => Hf; rewrite -[RHS]Hf. rewrite summxE; apply eq_bigr=> k _; by rewrite !mxE. 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