proposition: Lemma sparse_cfctr mr mc cp : size mr = cprsize cp -> size mc = ctrmsize cp -> let G := cpmap cp in let cc := map edge (mask mr (cpring G)) ++ insertE (mask mc (ctrenum cp)) in cfctr mr mc cp ==> sparse ((G : G) :: cc).
proof: Proof. lazy zeta; elim: cp => [|s cp IHcp] // in mr mc *. case Dcpc: (cfctr _ _) (cfctr_config_prog mr mc (s :: cp)) => // [cpc]. case: s Dcpc => // [n||] Dcpc; rewrite !implyTb => cp_ok Emr Emc; have cpQ := config_prog_cubic cp_ok; rewrite /= in Dcpc cpQ Emr Emc; move: IHcp {cpQ} (cpmap_plain cpQ) (cpmap_cubic cpQ) (cpmap_proper cpQ); rewrite [cpmap (_ :: _)]/=; set G := cpmap cp => IHcp plainG cubicG ntG. - rewrite cpring_ecpR /= -(rotrK n mr). rewrite -(size_rotr n mr) in Emr; move: Dcpc (IHcp _ _ Emr Emc). case: (cfctr _ mc cp) => //= _ _ {cpc}; apply: etrans; apply: eq_simple. move=> y; congr (_ || _). by rewrite !(cfaceC y); apply/esym/(@same_cnode G)/fconnect_iter. apply: eq_has_r => x {y}; rewrite !mem_cat; congr (_ || _). by rewrite !map_mask map_rot mem_mask_rot // size_map size_ring_cpmap. rewrite /= !size_cat !size_map; congr (_ + _).+1; rewrite /rot mask_cat. rewrite -rot_size_cat size_rot -mask_cat ?cat_take_drop //. by rewrite !size_take Emr -size_ring_cpmap. by rewrite !size_drop Emr -size_ring_cpmap. - rewrite /G. case Dcp: cp mc mr Emc Emr Dcpc => [|s cp'] [|b3 mc] // [|b1 [|b2 mr]] //. case: mr {cp Dcp G IHcp cp_ok plainG cubicG ntG} => [|b3 [|b4 mr]] // _ _. rewrite sparse_cons -(eq_has (mem_cpring (ecpY _))) cpring_ecpY cpring0 /=. by case: b1 b2 b3 => [] [] []. rewrite -Dcp -/G; have plainGX: plain (ecpY G) := plain_ecpY G plainG. case: ifP => // b123; rewrite [size _]/= [size _ = _]/= => [] [Emc] [Emr]. case: (cfctr _ _) {IHcp}(IHcp (b3 :: mr) mc Emr Emc) => // {}cpc IHcp _. have <-: map (icpY G) (node G :: ctrenum cp) = ctrenum (CpY :: cp). by rewrite /G Dcp. move: IHcp; set p := _ ++ _; rewrite sparse_cons -(eq_has (mem_cpring G)). case/andP=> {cpc}rG'p IHp. have{rG'p IHp}: sparse ((ecpY G : ecpY G) :: map (icpY G) (node G :: p)). rewrite map_cons !sparse_cons; apply/and3P; split. - rewrite -(eq_has (mem_cpring (ecpY G))) cpring_ecpY -map_cons. apply: contra rG'p => /hasP[_ /mapP[y py ->] r_y]; apply/hasP. rewrite !inE (mem_map (@icpY_inj _ G)) !orFb in r_y. exists y; last exact: mem_behead; case/predU1P: py => // y_nG. by have:= cpring_uniq G; rewrite head_cpring /= -y_nG r_y. - apply: contra rG'p => /hasP[_ /mapP[y py ->]]; rewrite cnodeC => yNnG. apply/hasP; exists y => //; apply: wlog_neg => r'y. by rewrite mem_cpring cnode1 cnodeC -(@cnode_injcp [:: CpY]). elim: p rG'p IHp => //= x p IHp /norP[r'x r'p]. rewrite !sparse_cons => /andP[pN'x /IHp->] {r'p}//; rewrite andbT has_map. by rewrite (eq_has (@cnode_injcp [:: CpY] _ _ _ r'x)). rewrite -cat1s sparse_catC cats1 -(cat1s (pointer _)) sparse_catC cats1. rewrite -map_mask /p head_cpring cpring_ecpY !mask_cons map_cons !map_cat. rewrite insertE_cat -insertE_icpY !map_mask -!map_comp rcons_cons !rcons_cat. move: (rcons _ _) => rk; rewrite insertE_icpY insertE_seqb map_cat !map_nseq. move: {p}(mask mr _) (nseq b3 _) => rr r3; set x3 := icpY G (node G). rewrite sparse_catCA -!(catA _ _ rk) -catA sparse_catCA. rewrite [cat r3]lock 2!catA -lock sparse_catCA; move: {rr rk}(r3 ++ _) => rk. case: b1 b2 b3 b123 => [] [] [] // _; rewrite !sparse_cons => /andP[// /contra->//]; apply: sub_has => u. - by rewrite 2!cnode1. by rewrite cnode1. case: mc mr Emc Emr Dcpc => [|b3 [|b4 [|b5 mc]]] [|b1 [|b2 mr]] // [Emc] Emr. rewrite /= in Emc Emr; case: ifP => // b314_325; case: ifP => // _. have{IHcp}:= IHcp [:: b4, b5 & mr] mc Emr Emc; set p := _ ++ _. case: (cfctr _ _ _) => // []{}cpc IHcp _; rewrite {cpc}implyTb in IHcp. have plainGX := plain_ecpH G plainG. have <-: face (ecpH G) :: map (icpH G) [:: node G, G : G & ctrenum cp] = ctrenum (CpH :: cp) by []. move: IHcp; rewrite sparse_cons -(eq_has (mem_cpring G)) => /andP[r'p IHp]. have nX: node (ecpH G) = icpN _ (icpN _ (edge (ecpU G))). by rewrite /= /long_cpring /= nodeK (negPf ntG). have n1G: node (icpH G G) = icpN _ (ecpY G) by rewrite /= (negPf ntG) /= !eqxx. have in_rH x: (icpH G x \in cpring (ecpH G)) = (x \in drop 2 (cpring G)). by rewrite cpring_ecpH // nX !inE (mem_map (@icpH_inj _ G)). have{IHp r'p}: sparse (pointer (ecpH G) :: map (icpH G) [:: node G, G : G & p]). rewrite !map_cons !sparse_cons; apply/and4P; split. - rewrite -!map_cons -(eq_has (mem_cpring (ecpH G))) has_map (eq_has in_rH). apply: contra r'p => /hasP[x]; rewrite !inE orbA => /orP[Gx | p_x] r_x. have:= cpring_uniq G; rewrite head_proper_cpring // (cat_uniq [:: _; _]). by case/and3P=> _ /hasP[]; exists x; rewrite ?inE. by apply/hasP; exists x; last apply: mem_drop r_x. - rewrite -map_cons has_map; apply/hasPn=> y; rewrite !inE => p_y. set n0nG := icpH G _; pose n1nG : ecpH G := icpN _ (icpN _ (ecpU G)). pose n2nG : ecpH G := icpN _ (edge (ecpY G)). have cycNnG : fcycle node [:: n0nG; n1nG; n2nG] by rewrite /= !eqxx. rewrite (fconnect_cycle cycNnG) ?mem_head // !inE !orbF. case/predU1P: p_y => [-> | p_y]. by have:= cpring_uniq G; rewrite head_proper_cpring. apply: contraNneq r'p => /icpH_inj y_nG; apply/hasP; exists y => //. by rewrite head_cpring -y_nG mem_head. - rewrite has_map; apply/hasPn=> y p_y; rewrite inE. have r'y := hasPn r'p _ p_y. by rewrite cnodeC (@cnode_injcp [:: CpH]) // cnodeC -mem_cpring. elim: p r'p IHp => [|x p IHp] //= /norP[r'x r'p]. rewrite !sparse_cons has_map => /andP[/contra->]; first exact: IHp. by apply: etrans; apply: eq_has => y; rewrite inE (@cnode_injcp [:: CpH]). rewrite {}/p head_proper_cpring // cpring_ecpH //. rewrite -cat1s sparse_catC cats1 -(cat1s (ecpH G : ecpH G)) sparse_catC cats1. rewrite 4!map_cons !mask_cons !insertE_cat map_cat -insertE_icpH map_mask. rewrite !rcons_cons !rcons_cat -map_comp !map_cat; move: (rcons _ _) => rk. rewrite !map_mask -map_comp !map_nseq /comp; move: (mask mr _) => rr IHcp. rewrite 4!(catA (insertE _), =^~ insertE_cat) sparse_catCA. rewrite (catA _ _ rr) -2!catA sparse_catCA !insertE_cat !insertE_seqb !catA. rewrite -3!catA sparse_catCA; do[rewrite -!catA; move: (_ ++ _) => r] in IHcp *. rewrite (catA (nseq b2 _)) (catA (nseq b5 _)) sparse_catCA -!catA. pose xG b := nseq b (icpH G G); pose yG b := nseq b (icpH G (node G)). transitivity (sparse (xG b2 ++ xG b3 ++ xG b5 ++ yG b1 ++ yG b3 ++ yG b4 ++ r)). congr uniq; rewrite !map_cat !map_nseq. do !congr cat; congr nseq; apply/(rootP (@cnodeC (ecpH G))). - by rewrite 2!cnode1r n1G. - by rewrite cnode1r n1G. - by rewrite nX 2!cnode1 /= eqxx. by rewrite cnode1 /= eqxx. move: IHcp; rewrite (sparse_catCA [::_] [::_]) {}/xG {}/yG. move: (ecpY G) (icpH G G) (icpH G (node G)) r => G' x y r. case: b3 b1 b2 b4 b5 b314_325 => [] [] [] [] [] // _. - by case/andP. - by rewrite sparse_catCA => /andP[]. - by case/andP. - by rewrite sparse_catCA => /andP[]. by case/and3P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring cfmap ctree) fourcolor(cfcolor)