proposition: Lemma tree_ok h (s : seq id') k (i : ord_of_kind m n' k) : let t1 := build_tree_rec H rW h s k i in let t2 := sumprod_up t1 in let dn := down_msg s (id_of_kind k i) in let t := sumprod_down t2 dn in (#|id'| - #|s| <= h)%nat -> uniq_path (tanner_rel H) (id_of_kind k i) s -> t = build_computed_tree h s i.
proof: Proof. elim: h => [|h IH] in s k i *. move=> t1 t2 dn t Ht1. have His: id_of_kind k i \in s by apply seq_full. by rewrite /uniq_path /= His andbF. move=> t1 t2 dn t Hh Hun. have Hh': (#|id'| - #|id_of_kind k i :: s| <= h)%nat. move/andP/proj2: Hun => Hun. by apply card_uniq_seq_decr. rewrite /t /dn /=. have Hspec' x: uniq_path (tanner_rel H) (id_of_kind (negk k) x) (id_of_kind k i :: s) -> msg_spec' (id_of_kind (negk k) x) (id_of_kind k i) = up (sumprod_up (build_tree_rec H rW h [:: id_of_kind k i & s] (negk k) x)). move=> Hx. rewrite msg_spec_alpha_beta; last first. by move/andP/proj1: Hx => /= /andP/proj1. rewrite -(up_sumprod_down (down_msg [:: id_of_kind k i] (id_of_kind (negk k) x))). rewrite IH //=. by destruct h; rewrite /= alpha_beta_tag_of_id; f_equal; rewrite /image_mem /enum_mem; f_equal; apply eq_filter=> y /=; rewrite !inE orbF. destruct s; simpl. congr {|children := _ ; up := _ |}. rewrite apply_seqs_but1 -!map_comp; last by apply unique_children. apply eq_in_map => [j] /= Hj. move: (Hj). rewrite select_children_spec => /andP [Hpj Hunj]. rewrite -IH //; last first. apply cons_uniq_path => //. by rewrite sym_tanner_rel. rewrite /down_msg. congr sumprod_down. congr Some. rewrite msg_spec_alpha_beta // alpha_beta_tag_of_id. congr alpha_beta. rewrite filter_map -map_comp. rewrite -imset_set1 kind_filter. rewrite -enum_select_children. rewrite /image_mem /enum_mem. rewrite -filter_predI. symmetry. apply eq_in_map_seqs. apply eq_filter => x. rewrite /= !inE /=. rewrite !node_id_sumprod_up !node_id_build. rewrite (inj_eq (@id_of_kind_inj _ _ _)). rewrite select_children_spec. by rewrite in_cons (eq_sym (id_of_kind _ x)) id_of_kind_neq in_nil andbT. move=> x /= Hx. rewrite mem_filter !inE in Hx. apply Hspec'. apply: cons_uniq_path => //. by move/andP/proj1/andP/proj2: Hx; rewrite sym_tanner_rel. by rewrite mem_seq1 eq_sym id_of_kind_neq. congr alpha_beta. rewrite -!map_comp /=. rewrite -/set0 -(imset0 (id_of_kind (negk k))) kind_filter. rewrite -enum_select_children. rewrite /image_mem /enum_mem. symmetry. apply eq_in_map_seqs. apply eq_filter => x. rewrite /= !inE /=. rewrite select_children_spec. by rewrite in_cons (eq_sym (id_of_kind _ x)) id_of_kind_neq in_nil andbT. move=> x /= Hx. rewrite mem_filter !inE in Hx. apply Hspec'. apply: cons_uniq_path => //. by move/andP/proj1/andP/proj2: Hx; rewrite sym_tanner_rel. by rewrite mem_seq1 eq_sym id_of_kind_neq. have [o Hs]: exists o, s = id_of_kind (negk k) o. move: Hun => /= /andP/proj1 /= /andP/proj1. destruct s as [o|o], k. by rewrite tanner_relE. move=> ?; by exists o. move=> ?; by exists o. by rewrite tanner_relE. congr {| children := _; up := _; down := _ |}. rewrite apply_seqs_but1 -!map_comp; last by apply unique_children. apply eq_in_map => [j] /= Hj. move: (Hj). rewrite select_children_spec => /andP [Hpj Hunj]. rewrite -IH //; last first. apply cons_uniq_path => //. by rewrite sym_tanner_rel. rewrite /down_msg. congr sumprod_down. congr Some. symmetry. rewrite msg_spec_alpha_beta // alpha_beta_tag_of_id. rewrite -imset_set1 kind_filter. rewrite filter_map -map_comp Hs. set ups := map (_ \o _ \o _) _. have ->: ups = [seq msg_spec' (id_of_kind (negk k) x) (id_of_kind k i) | x in [set x | (tanner_rel H (id_of_kind k i) \o id_of_kind (negk k)) x] :\ j :\ o]. apply eq_in_map_seqs. rewrite -Hs (select_children_def (j:=o) Hun) Hs //. rewrite /enum_mem. rewrite -filter_predI. apply eq_filter => x. rewrite /= !inE /=. rewrite !node_id_sumprod_up !node_id_build. rewrite (inj_eq (@id_of_kind_inj _ _ _)). by rewrite !andbA (andbC (x !=j)). move=> x /=. rewrite mem_filter !inE !node_id_sumprod_up !node_id_build. rewrite select_children_spec -Hs => /andP/proj2/andP [Hx1 Hx2]. rewrite Hspec' //=. apply cons_uniq_path => //. by rewrite sym_tanner_rel. rewrite /image_mem /enum_mem. rewrite -(map_cons (fun x => msg_spec' (id_of_kind (negk k) x) (id_of_kind k i))). apply eq_alpha_beta => //. apply uniq_perm. by rewrite filter_uniq // -enumT enum_uniq. rewrite /= filter_uniq //. by rewrite mem_filter !inE eqxx. by rewrite -enumT enum_uniq. move=> x /=. rewrite in_cons mem_filter /= mem_enum !inE -enumT mem_enum /=. case Hxo: (x == o). rewrite (eqP Hxo). move: Hunj. rewrite !in_cons Hs. rewrite (inj_eq (@id_of_kind_inj _ _ _)) (eq_sym j). move/norP/proj2/norP/proj1 => -> /=. move/andP/proj1: Hun. by rewrite /= Hs => /andP/proj1 ->. by destruct k; rewrite /= !inE andbT. congr alpha_beta. rewrite -!map_comp. symmetry. rewrite Hs in Hun Hspec' *. rewrite set1F -imset_set1 kind_filter. rewrite (select_children_def (j:=o) Hun) //. rewrite /image_mem. apply eq_in_map. move=> x /=. rewrite mem_filter !inE /= sym_tanner_rel => /andP [] /andP [Hx1 Hx2] _. rewrite -/msg_spec' Hspec' //. apply: cons_uniq_path => //. rewrite !in_cons !negb_or. rewrite (ext_uniq_path tanner_acyclic Hun) //. rewrite (eq_sym (id_of_kind _ x)) id_of_kind_neq //=. by rewrite (inj_eq (@id_of_kind_inj _ _ _)) Hx1. apply msg_spec_alpha_beta. rewrite sym_tanner_rel. by move/andP/proj1: Hun => /= /andP/proj1. 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