proposition: Lemma build_tree_rec_ok h k i s : #|id'| - #|s| <= h -> uniq_path (tanner_rel H) (id_of_kind k i) s -> let l := labels (build_tree_rec H rW h s k i) in forall a b, a \in l -> b \in l -> tanner_rel H a b -> graph (build_tree_rec H rW h s k i) a b.
proof: Proof. elim: h k i s => [|h IHh] k i s Hh Hi. have His: id_of_kind k i \in s by apply seq_full. by rewrite /uniq_path /= His andbF in Hi. move=> l. have Hab b: b \in l -> tanner_rel H (id_of_kind k i) b -> b \in [seq node_id i | i <- [seq build_tree_rec H rW h (id_of_kind k i :: s) (negk k) j | j <- select_children H s k i]]. move=> Hb HH. rewrite -map_comp. apply /mapP. have [x Hx]: exists x, b = id_of_kind (negk k) x. move: HH; clear; rewrite tanner_relE. case: k b i => -[] b i // _; by exists b. exists x; last by destruct h. rewrite select_children_spec. rewrite -Hx HH /=. case Hbs: (b \in s). have [p [Hp [Ha Hl]]] := labels_build_tree_rec Hb Hi. rewrite in_cons Hx eq_sym id_of_kind_neq /=. move /andP/proj2: Hp. by rewrite cons_uniq mem_cat Hbs orbT. by rewrite /= in_cons Hbs Hx eq_sym id_of_kind_neq. move=> a b Ha Hb HH /=. case: ifP => Heq. rewrite -(eqP Heq) in HH; by apply Hab. case: ifP => Heq'. rewrite sym_tanner_rel -(eqP Heq') in HH; by apply Hab. clear Hab. simpl in l. rewrite /l in_cons eq_sym Heq /= in Ha. rewrite {}/l in_cons eq_sym Heq' /= in Hb. move /flattenP: Ha => [sa Ha Hsa]. move /flattenP: Hb => [sb Hb Hsb]. rewrite -!map_comp in Ha Hb. move /mapP: Ha => [ia Hia Ha]. move /mapP: Hb => [ib Hib Hb]. subst sa sb. rewrite !select_children_spec in Hia Hib. move /andP: Hia => [Hia Hias]. move /andP: Hib => [Hib Hibs]. move /andP: (Hi) => [Hpi Hun]. case Hiab: (ia == ib). rewrite has_map /=. apply /hasP. exists ia. rewrite select_children_spec; by apply /andP. rewrite -(eqP Hiab) in Hsb. apply IHh => //. by apply card_uniq_seq_decr. by apply cons_uniq_path => //; rewrite sym_tanner_rel. set sa := id_of_kind (negk k) ia in Hia Hias. set sb := id_of_kind (negk k) ib in Hib Hibs. set si := id_of_kind k i in Hia Hib Hsa Hsb Hias Hibs. have Hiap: uniq_path (tanner_rel H) sa (si :: s). by rewrite /uniq_path /= sym_tanner_rel Hia Hpi Hias. have Hibp: uniq_path (tanner_rel H) sb (si :: s). by rewrite /uniq_path /= sym_tanner_rel Hib Hpi Hibs. have [p1 [Hp1 [Hal Hpl1]]]:= labels_build_tree_rec Hsa Hiap. have [p2 [Hp2 [Hbl Hpl2]]]:= labels_build_tree_rec Hsb Hibp. suff: false by []. rewrite -/sb -/sa -/si in Hp1 Hp2 Hi Hpi Hun Hal Hbl. clear -Hp1 Hp2 Hi Hpi Hun Hal Hbl Hiab HH tanner_acyclic. move: (@tanner_acyclic si sb (rev (belast b p2) ++ a :: p1)). rewrite !lastE Hal. case Hsasb: (sa == sb). move /eqP: Hsasb. rewrite /sa /sb=> eq. destruct k; inversion eq; by rewrite H1 eqxx in Hiab. move=> Hcy. move /andP: Hp1 => [Hp1 Hun1]. move /andP: Hp2 => [Hp2 Hun2]. apply Hcy; clear Hcy Hsasb. rewrite -cat_cons -rev_rcons -{1}Hbl -lastI. rewrite mem_cat mem_rev negb_or. have Hsi c p: uniq ((si :: c :: p) ++ s) = uniq (c :: p ++ si :: s). apply perm_uniq. rewrite -cat1s -(cat1s c) perm_sym -cat1s -(cat1s si). rewrite !catA perm_cat2r. by rewrite perm_catC catA. rewrite -!Hsi !cat_uniq in Hun1 Hun2. case/andP/proj1/andP: Hun2 => -> _. by case/andP/proj1/andP: Hun1. rewrite {Hun1 Hun2} /cycle. rewrite -cats1 -cat_cons -rev_rcons -catA cat_path -{1 2}Hbl -lastI. have {1}->: si = last b (rcons p2 si) by rewrite last_rcons. rewrite -{1}(belast_rcons b p2 si) rev_path rev_cons !lastE. apply /andP; split. rewrite -(eq_path (sym_tanner_rel _)) -cats1. rewrite -cat1s catA cat_path in Hp2. by case/andP: Hp2. rewrite /= sym_tanner_rel HH. rewrite -cat1s catA cat_path in Hp1. by case/andP: Hp1. 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