proposition: Lemma enc_discard_is_id : cancel_on (Hamming.code m) (enc channel_code) discard.
proof: Proof. move=> y Hy. rewrite /discard /= ffunE. rewrite /syndrome in Hy. have {}Hy : SysHamming.PCM m' *m row_perm systematic y^T = 0. rewrite /SysHamming.PCM. rewrite mul_col_perm. rewrite 2!row_permE. rewrite !(mulmxA (perm_mx systematic^-1)). rewrite -perm_mxM. rewrite mulVg. rewrite perm_mx1. rewrite mul1mx. apply/trmx_inj/eqP. by rewrite trmx0 -mem_kernel_syndrome0. rewrite /discard /GEN. rewrite /mx_discard /SysHamming.GEN'. rewrite SysHamming.PCM_A_1 in Hy. rewrite tr_col_perm. rewrite mul_row_perm. rewrite invgK. rewrite trmx_cast /=. rewrite tr_row_mx. rewrite trmx0 trmx1. rewrite [in X in _ *m _ *m X = _ ]col_permE. rewrite invgK. set tmp := castmx _ (col_mx _ _). rewrite -mulmxA. rewrite (mulmxA tmp). rewrite {}/tmp. rewrite (_ : castmx _ _ *m castmx _ _ = castmx (subnK (Hamming.dim_len m'), subnK (Hamming.dim_len m')) ((col_mx 1%:M 0) *m (row_mx 1%:M (- SysHamming.CSM m')^T))); last first. apply/matrixP => a b. rewrite !mxE. rewrite castmxE. rewrite !mxE. apply eq_bigr => /= i _. congr (_ * _); by rewrite castmxE /= cast_ord_id. rewrite mul_col_row. rewrite 2!mul1mx 2!mul0mx. rewrite block_mxEv row_mx0. apply trmx_inj. rewrite trmx_mul. rewrite tr_col_perm. rewrite trmx_mul. rewrite trmx_cast. rewrite tr_col_mx. rewrite trmx0 tr_row_mx. rewrite trmx1 trmxK /=. rewrite tr_perm_mx. rewrite -mulmxA. have [Y1 [Y2 HY]] : exists (Y1 : 'cV_ _) Y2, (row_perm systematic y^T) = castmx (subnK (Hamming.dim_len m'), erefl 1%nat) (col_mx Y1 Y2). exists (\matrix_(j < 1, i < n - m) (y j (systematic (widen_ord (leq_subr m n) i))))^T. have dim_len_new i (Hi : i < m) : n - m + i < n. by rewrite -ltn_subRL subnBA ?Hamming.dim_len // addnC addnK. exists (\matrix_(j < 1, i < m) (y j (systematic (Ordinal (dim_len_new _ (ltn_ord i))))))^T. apply/colP => a /=. rewrite !mxE castmxE /=. rewrite !mxE. case: splitP. move=> j aj. rewrite !mxE /=. congr (y _ (systematic _)); by apply val_inj. move=> k ak. rewrite mxE /= mxE /=. congr (y _ (systematic _)); by apply val_inj. rewrite HY in Hy. rewrite (castmx_cols_mulmx subnK) in Hy. rewrite mul_row_col in Hy. rewrite mul1mx in Hy. rewrite HY. transitivity (perm_mx systematic^-1 *m (castmx (subnK (Hamming.dim_len m'), erefl (n - m)%nat) (col_mx 1%:M (- SysHamming.CSM m')) *m Y1)). congr (_ *m _). rewrite (castmx_cols_mulmx2 subnK). rewrite mul_row_col. rewrite mul0mx addr0. by rewrite (mulmx_castmx_cols_comm2 subnK). transitivity (perm_mx systematic^-1 *m (castmx (subnK (Hamming.dim_len m'), erefl 1%nat) (col_mx Y1 ((- SysHamming.CSM m') *m Y1)))). congr (_ *m _). transitivity (castmx (subnK (Hamming.dim_len m'), erefl 1%nat) (col_mx 1%:M (- SysHamming.CSM m') *m Y1)). by rewrite (mulmx_castmx_cols_comm2 subnK). congr castmx. by rewrite mul_col_mx mul1mx. have {}HY : y^T = row_perm (systematic^-1) (castmx (subnK (Hamming.dim_len m'), erefl 1%nat) (col_mx Y1 Y2)). rewrite -HY. rewrite 2!row_permE. rewrite mulmxA. rewrite -perm_mxM. rewrite mulVg. rewrite perm_mx1. by rewrite mul1mx. rewrite HY row_permE; congr (_ *m castmx _ (col_mx _ _)). apply/eqP; by rewrite eq_sym -subr_eq0 mulNmx opprK addrC Hy. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) mathcomp(Rstruct) realType_ext ssr_ext ssralg_ext f2 linearcode natbin ssrR hamming bigop_ext fdist proba channel channel_code decoding binary_symmetric_channel