proposition: Theorem message_ok (a b : id') h (s : seq id') k (i : ord_of_kind m n' k) : let t := build_computed_tree h s i in (#|id'| - #|s| <= h)%nat -> uniq_path (tanner_rel H) (id_of_kind k i) s -> tanner_rel H a b -> a \in prec_node s ++ labels t -> b \in prec_node s ++ labels t -> msg a b (prec_node s) t = [:: msg_spec' a b].
proof: Proof. elim: h => [|h IH] in a b s k i *. move=> t Ht. have His: id_of_kind k i \in s by apply seq_full. by rewrite /uniq_path /= His andbF. move=> t Hh Hun Hgr Ha Hb. have Hh': (#|id'| - #|id_of_kind k i :: s| <= h)%nat. move/andP/proj2: Hun => Hun. by apply card_uniq_seq_decr. rewrite /t /=. case Has: (Some a == prec_node s). destruct s; first by []. rewrite /= (inj_eq (@Some_inj _)) in Has. case Hb0: (b == id_of_kind k i). rewrite msg_spec_alpha_beta //. by rewrite (eqP Has) (eqP Hb0). move: Hb0. rewrite !(eqP Has) /t in Hun Hb Hgr *. rewrite -tree_ok // labels_sumprod_down labels_sumprod_up in Hb. rewrite (cycle_in_subtree Hun Hgr Hb). by rewrite eqxx. case Hbs: (Some b == prec_node s). destruct s; first by []. simpl in Hbs. move/eqP: Hbs => [] Hbs; subst b. case Ha0: (a == _). rewrite msg_spec_alpha_beta // alpha_beta_tag_of_id. move/eqP: Ha0 => Ha0 /=; subst a. by rewrite set1F. move: Ha0. rewrite /t -tree_ok // labels_sumprod_down labels_sumprod_up in Ha. rewrite (cycle_in_subtree Hun _ Ha). by rewrite eqxx. by rewrite sym_tanner_rel. have Hgr': graph t a b. rewrite /t -tree_ok // -graph_sumprod_down -graph_sumprod_up labels_sumprod_down labels_sumprod_up in Ha Hb *. apply build_tree_rec_ok => //. move: Ha. rewrite mem_cat => /orP [] //. destruct s; first by []. rewrite in_cons => /orP [] // Hab. by rewrite (eqP Hab) eqxx in Has. move: Hb. rewrite mem_cat => /orP [] //. destruct s; first by []. rewrite in_cons => /orP [] // Hab. by rewrite (eqP Hab) eqxx in Hbs. have Hun': uniq (labels t). rewrite /t -tree_ok // labels_sumprod_down labels_sumprod_up. by apply uniq_labels_build_tree_rec. have Hsz : size (msg a b (prec_node s) t) = graph t a b. destruct s. by apply msg_sz. rewrite msg_none_eq. by apply msg_sz. by apply /contraFN: Has => /eqP ->. by apply /contraFN: Hbs => /eqP ->. rewrite {}Hgr' /= {}Has {}Hbs in Hsz. set fl := flatten _ in Hsz *. have Hfl: fl = fl by []. rewrite {1}/fl in Hfl. destruct fl; first by []. destruct fl; last by []. move: {Hsz} (eq_refl r). rewrite -mem_seq1 -Hfl. move/flattenP => [l Hl Hrl]. move/mapP: Hl => [c Hc Hmsgc]. subst l. set fl := flatten _ in Hfl *. suff : msg_spec' a b \in fl. rewrite Hfl mem_seq1. by move/eqP => ->. apply/flatten_mapP. exists c; first by []. set e := id_of_kind k i in Hun Hh' Hrl *. move/mapP: Hc => [j Hj] /= Hc. rewrite -/e in Hc *. rewrite select_children_spec in Hj. change (Some e) with (prec_node [:: e & s]). pose inj := @id_of_kind m n' (negk k). destruct (@msg_nonnil a b (Some e) _ c) as [Hac Hbc]. move: Hrl. by destruct (msg _ _ _ _). have Hunj: uniq_path (tanner_rel H) (inj j) (e :: s). apply: cons_uniq_path => //. move/andP/proj1: Hj. by rewrite sym_tanner_rel. by move/andP/proj2: Hj. rewrite Hc -tree_ok // ?labels_sumprod_down ?labels_sumprod_up in Hac Hbc. rewrite Hc (IH a b [:: e & s] _ j) //. by rewrite mem_seq1. rewrite -tree_ok //. by rewrite labels_sumprod_down labels_sumprod_up. rewrite -tree_ok //. by rewrite labels_sumprod_down labels_sumprod_up. 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