proposition: Lemma ctrband_correct cm cp : size cm = ctrmsize cp -> config_prog cp -> [/\ proper_cpmask cp (ctrband cm cp) & fband (insertE (mask cm (ctrenum cp))) =i fband (cpmask (ctrband cm cp) cp)].
proof: Proof. move=> Ecm cp_ok; elim: cp cp_ok cm Ecm => // s cp IHcp cp_ok. move: cp_ok (config_prog_cubic cp_ok) IHcp => /=. case: s => // [n||] cp_ok cpQ; move: (cpmap_plain cpQ) (cpmap_proper cpQ); rewrite [cpmap _]/=; set G := cpmap cp => plainG ntG IHcp cm Ecm. - case: (ctrband cm cp) {IHcp Ecm cp_ok}(IHcp cp_ok _ Ecm) => mr mk. case=> /andP[Emr Emc] IHcp; split; first by rewrite /= size_rot Emr. rewrite /cpmask /= -/G cpring_ecpR /= => x. rewrite IHcp /= !fband_cat /=; congr (_ || _). by rewrite mask_rot ?fband_rot // (eqP Emr) -size_ring_cpmap. - rewrite /G; case Dcp: cp cm cp_ok Ecm => [|s cp'] // [|b1 cm] //. by rewrite /cpmask /= cpring_ecpY cpring0. rewrite -Dcp -/G [size _]/= => cp_ok [Ecm]. case: (ctrband cm cp) {IHcp}(IHcp cp_ok _ Ecm) => mr mk [/andP[/eqP Emr Emk]]. have: 1 < size mr by rewrite Emr -size_ring_cpmap -size_proper_cpring. case: mr Emr => [|a0 [|a1 mr]] // Emr _ IHcp. split=> [|u]; first by rewrite /= -Emr /= eqxx. rewrite -map_cons /cpmask [cpmap _]/= [cpker _]/= -/G. rewrite cpring_ecpY /behead (head_proper_cpring ntG). rewrite -!map_mask insertE_icpY map_cons !mask_cons cat0s insertE_cat. rewrite insertE_seqb -!catA !unfold_in !has_cat !has_seqb -map_mask. have [[x uFx] | XFu] := fband_icpY u; last first. have DuF := etrans (esym (same_cface XFu _)) (cface_ecpY _). by rewrite !DuF !andbF !(eq_has DuF) !has_map !has_pred0. rewrite !(same_cface uFx) !(eq_has (same_cface uFx)) !cface_icpY. rewrite !has_map !(eq_has (cface_icpY G x)) !has_cat !has_seqb. rewrite [has _ _]IHcp [in rhs in _ = rhs]cface1r cface_icpY. rewrite /cpmask {1}(head_proper_cpring ntG) unfold_in has_cat !has_mask_cons. by rewrite orbCA cface1r nodeK !andb_orl -!orbA; do !bool_congr. case: cm Ecm => [|b1 [|b0 [|b2 cm]]] //; rewrite [size _]/= => [] [Ecm]. case: (ctrband cm cp) {IHcp}(IHcp cp_ok _ Ecm) => mr mk [/andP[/eqP Emr Emk]]. have longG: long_cpring G by apply: cfmap_long. have: 2 < size mr by rewrite Emr -size_ring_cpmap -size_long_cpring. case: mr Emr => [|a0 [|a1 [|a2 mr]]] // Emr _ IHcp; rewrite /= in Emr. split=> [|u]; first by rewrite /= -Emr /= eqxx. rewrite /cpmask [cpmap _]/= [cpker _]/= -/G (head_long_cpring longG). rewrite cpring_ecpH // !mask_cons !insertE_cat -!map_mask !insertE_seqb. rewrite insertE_icpH !unfold_in !has_cat !has_seqb. have fnX: face (node (ecpH G)) = icpH G (node G). by rewrite /= /long_cpring /= nodeK (negPf ntG) /= nodeK (negPf ntG). have <-: face (icpH G (edge (node G))) = edge (face (ecpH G)). rewrite /= nodeK (negPf ntG) /= [_ == _](inj_eq edgeI) eq_sym (negPf ntG). by rewrite eqxx. rewrite (cface1r (node _)) fnX -(cface1r (ecpH G)) -cface1r. case uFX: (cface u (ecpH G)). have DuF := etrans (same_cface uFX _) (cface_ecpH ntG _). by rewrite !andbT !DuF !andbF !(eq_has DuF) !has_map !has_pred0. have [[x uFx]|] := fband_icpH u; last by rewrite cfaceC uFX. have DuF := etrans (same_cface uFx _) (cface_icpH _ _ _). rewrite !DuF !andbF !has_map !(eq_has DuF) [has _ _]IHcp unfold_in. rewrite /cpmask (head_long_cpring longG) has_cat !has_mask_cons. by rewrite cface1r nodeK -cface1r /= !andb_orl -!orbA; do !bool_congr. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring cfmap ctree) fourcolor(cfcolor)