proposition: Lemma build_tree_rec_full h k i s : #|id'| - #|s| <= h -> uniq_path (tanner_rel H) (id_of_kind k i) s -> mem (labels (build_tree_rec H rW h s k i)) =i connect (tanner_split s) (id_of_kind k i).
proof: Proof. elim: h k i s => [|h IHh] k i s Hh Hc. have His: id_of_kind k i \in s by apply seq_full. by rewrite /uniq_path /= His andbF in Hc. move=> a /=. rewrite in_cons. case Hai: (a == id_of_kind k i); simpl. symmetry. rewrite inE (eqP Hai). apply /connectP. by exists [::]. move/andP: Hc => [] /= Hc Hun. have Hh': #|id'| - #|id_of_kind k i :: s| <= h. by apply card_uniq_seq_decr. have Hchild o: o \in select_children H s k i -> uniq_path (tanner_rel H) (id_of_kind (negk k) o) (id_of_kind k i :: s). rewrite /uniq_path /= Hc Hun. rewrite select_children_spec. move /andP=> [Hio Hos]. by rewrite sym_tanner_rel Hio Hos. rewrite inE. case Hcb: (connect _ _ a). rewrite -map_comp. apply /flatten_mapP. move /connectP: Hcb => [p Hcb Ha]. have Hsp:= shortenP Hcb. set a' := last (id_of_kind k i) p in Hsp. have : a = a' by rewrite Ha. destruct Hsp as [p3 Hp Hun' Hsp]. clear p Hcb Ha Hsp. move => Ha. rename p3 into p. destruct p. by rewrite Ha /= eqxx in Hai. have [o Ho]: exists o, s0 = id_of_kind (negk k) o. apply (sub_path (@tanner_split_tanner _)) in Hp. destruct k, s0. by rewrite tanner_relE in Hp. by exists o. by exists o. by rewrite tanner_relE in Hp. subst s0. have Ho: o \in select_children H s k i. rewrite select_children_spec. apply /andP; split. apply (@tanner_split_tanner s). by move /andP/proj1: Hp. rewrite in_cons. move: (Hun'). rewrite /= in_cons. move /andP/proj1/norP/proj1/negbTE => Hoi. rewrite eq_sym Hoi. move /andP/proj1: Hp. rewrite /tanner_split. case: (id_of_kind (negk k) o \in s); last by []. by rewrite orbT. exists o; first by []. rewrite IHh //. rewrite inE. apply /connectP. exists p => //. apply tanner_split_uncons. by move /andP/proj1: Hun'. by move /andP/proj2: Hp. exact: Hchild. rewrite -map_comp. apply /flatten_mapP => Hl. move: Hl => [l Hl Hal]. rewrite IHh // in Hal. rewrite inE in Hal. move /connectP: Hcb. apply. move /connectP: Hal => [p Hp Hlp]. exists (id_of_kind (negk k) l :: p); last by []. simpl. apply /andP; split. rewrite select_children_spec in Hl. rewrite /tanner_split. move /andP/proj1/negbTE: Hun => ->. rewrite in_cons in Hl. move /andP/proj2/norP/proj2/negbTE: (Hl) => -> /=. by move /andP/proj1: Hl. by apply (sub_path (@tanner_split_cons (id_of_kind k i) _)). by apply Hchild. 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