proposition: Lemma singleton_bound : min_dist <= n - \dim C + 1.
proof: Proof. set k := \dim C. have dimCn : k.-1 < n. have /dimvS := subvf C. rewrite dimvf /Vector.dim /= mul1n. by apply: leq_trans; rewrite prednK // not_trivial_dim. set f := linfun (sbound_f_linear (ltnW dimCn)). have H1 : \dim (f @: C) <= k.-1. suff : \dim (f @: C) <= \dim (fullv : {vspace 'rV[F]_k.-1}). by rewrite dimvf /= /Vector.dim /= mul1n. by apply/dimvS/subvf. have H2 : (\dim (f @: C) + \dim (C :&: lker f) = \dim (fullv : {vspace 'rV[F]_k}))%N. by rewrite dimvf /= /Vector.dim /= mul1n -[RHS](limg_ker_dim f C) addnC. have H3 : 1 <= \dim (C :&: lker f). rewrite lt0n; apply/eqP => abs; move: H2. rewrite abs addn0 dimvf /Vector.dim /= mul1n -/k. apply/eqP. move: H1; rewrite leqNgt; apply: contra => /eqP ->. by rewrite prednK // not_trivial_dim. have [cw [Hcw1 [Hcw2 Hcw3]]] : exists cw, cw \in C /\ cw != 0 /\ f cw = 0. have : \dim (C :&: lker f) != O by rewrite lt0n in H3. rewrite dimv_eq0. rewrite -vpick0 => Htmp. exists (vpick (C :&: lker f)). split. move: (memv_pick (C :&: lker f)). by rewrite memv_cap => /andP[]. split => //. apply/eqP; rewrite -memv_ker. move: (memv_pick (C :&: lker f)). by rewrite memv_cap => /andP[]. have Kcw : wH cw <= n - k + 1. rewrite wH_sum (bigID (fun x : 'I_n => x < k.-1)) /=. rewrite (eq_bigr (fun=> O)) ?big_const ?iter_addn ?mul0n ?add0n; last first. move=> i Hi /=. apply/eqP. rewrite eqb0 negbK. move: Hcw3. rewrite lfunE /= /sbound_f'. move/rowP => /= /(_ (Ordinal Hi)). rewrite !mxE /=. set x := widen_ord _ _. suff -> : x = i by move/eqP. exact: val_inj. have X : forall i : 'I_n, ~~ (i < k.-1) -> (cw ord0 i != 0) <= 1. move=> i Hi. by case: (_ != _). apply: (leq_trans (@leq_sum _ _ _ _ (fun=> 1%N) X)). set lhs := (X in X <= _). rewrite (_ : lhs = (\sum_(k.-1 <= i < n) 1%N))%N; last first. rewrite /lhs. rewrite -(big_mkord (fun i => ~~ (i < k.-1)) (fun=> 1%N)). rewrite {1}/index_iota subn0. rewrite {1}(_ : n = k.-1 + (n - k.-1))%N; last by rewrite subnKC // ltnW. rewrite iotaD big_cat /=. rewrite sum1_count. rewrite (@eq_in_count _ _ xpred0); last first. move=> i. by rewrite mem_iota add0n leq0n /= => ->. rewrite count_pred0 add0n add0n. rewrite sum1_count. rewrite (@eq_in_count _ _ xpredT); last first. move=> i. rewrite mem_iota -ltnNge => /andP[K1 K2]. by rewrite ltnS. rewrite sum1_count. by rewrite /index_iota. rewrite sum_nat_const_nat muln1 -subn1 subnBA ?not_trivial_dim //. rewrite addn1 subSn; last first. clear f H1 H2 H3 Hcw3. move: dimCn. by rewrite prednK // not_trivial_dim. by rewrite addn1. exact/(leq_trans _ Kcw)/min_dist_is_min. Qed.
imports: mathcomp(all_ssreflect ssralg poly polydiv fingroup perm) mathcomp(finalg zmodp matrix mxalgebra mxpoly vector) ssr_ext ssralg_ext poly_ext f2 hamming decoding channel_code