proposition: Lemma kind_filter {A : eqType} k i (s : {set ord_of_kind m n' (negk k)}) (F : id' -> A) : let a := id_of_kind k i in let inj := id_of_kind (negk k) in [seq F c | c in finset (tanner_rel H a) :\: inj @: s] = [seq F (inj x) | x in finset (tanner_rel H a \o inj) :\: s].
proof: Proof. move=> a inj. rewrite /image_mem /enum_mem /id' /id /=. have ->: Finite.enum [finType of 'I_m + 'I_n] = sum_enum [finType of 'I_m] [finType of 'I_n]. by rewrite unlock /=. rewrite /sum_enum filter_cat map_cat !filter_map -!map_comp. transitivity [seq ([eta F] \o [eta inj]) i | i <- Finite.enum (ord_of_kind m n' (negk k)) & [preim [eta inj] of [set x | tanner_rel H a x] :\: [set inj x | x in s]] i]. have Hp: [preim (id_of_kind k) of [set x | tanner_rel H (id_of_kind k i) x] :\: inj @: s] =i pred0. move=> x; destruct k; by rewrite /= !inE tanner_relE andbF. destruct k; by rewrite (eq_filter Hp) filter_pred0 // cats0. congr (map _ _). apply eq_filter => x /=; rewrite !inE. case/boolP : (x \in s) => /= Hx; first by rewrite imset_f. case /boolP: (inj x \in _) => // /imsetP [y Hy] /id_of_kind_inj xy. by rewrite xy Hy in Hx. Qed.
imports: Wf_nat Init.Wf Recdef Reals mathcomp(all_ssreflect perm zmodp matrix ssralg) mathcomp(Rstruct) ssrR Reals_ext ssr_ext ssralg_ext bigop_ext f2 fdist channel pproba linearcode subgraph_partition tanner tanner_partition summary ldpc checksum ldpc_algo