proposition: Lemma contract_ctreeP cf : if contract_ctree cf is Some ct then let r := cfring cf in [/\ valid_contract r (cfcontract cf) & forall et, cc_ring_trace (cfcontract cf) (rev r) et -> ctree_mem ct (etrace (behead et))] else True.
proof: Proof. case: cf => sym ccr cp; rewrite /contract_ctree /cfcontract /cfcontract_mask /=. rewrite /cfring revK /cfmap {sym}/= -size_ring_cpmap. set G := cpmap cp; set r := cpring G. set cm := ctrmask cp ccr; set mr0 := nseq (size r) false. have Emr0: size mr0 = cprsize cp by rewrite -size_ring_cpmap /mr0 size_nseq. have Ecm: size cm = ctrmsize cp by apply: size_ctrmask. move: (sparse_cfctr Emr0 Ecm) (cfctr_correct Emr0 Ecm). case: (cfctr mr0 cm cp) (cfctr_config_prog mr0 cm cp) => //= [cpc] cp_ok. have plainG := cpmap_plain (config_prog_cubic cp_ok). set cc := mask cm (ctrenum cp); rewrite -/G -/r in cc *. rewrite {1}mask_false cat0s => cc_sparse cc_col. case: ifP => // cm_valid; split=> [|_ [k col_k ->]]; last first. have{cc_col} := cc_col k; rewrite mask_false map_nseq mask_true //. case=> {k col_k}// k col_k <-. apply/ctree_mem_cpcolor; split; first exact: even_etrace. set et := trace _; rewrite /etrace; set h := etrace_perm _. exists (h \o k); first by apply: coloring_inj col_k; apply: permc_inj. rewrite sumt_permt map_comp trace_permt -/et -map_cons; congr (map h _). have tr_et: sumt et = Color0 by apply: sumt_trace. by rewrite -[sumt _]add0c -{}tr_et /et head_cpring /= [ctrace _]headI addcK. have size_cc: size cc = count id cm by rewrite size_mask // size_ctrenum. rewrite /valid_ctrm -{}size_cc -(mem_iota 1 3) !inE in cm_valid. split=> [|||cc4]; first 2 [by case/andP: cc_sparse]. - have:= uniq_ctrenum cp_ok; rewrite -/G -/r insertE_cat cat_uniq disjoint_has. rewrite andbA andbAC => /andP[_]; apply: contra => /hasP[x] /=. rewrite mem_rev mem_insertE // => r_x /has_mask KEx. by apply/hasP; exists x; rewrite /= mem_insertE //; apply/hasP; exists x. - by rewrite /= !orbA orbC -!orbA; case: ifP cm_valid. move: cm_valid; rewrite {}cc4 /=; apply: contraL => /pred0P no_triad. elim: {-2}(_ cp) (leqnn (cpksize cp)) => //= i IHi lt_i_cp. move: (cfmask1 cp i) (cpmask1 lt_i_cp cp_ok) (proper_cpmask1 cp i) => cmx. set x := nth _ _ i => Dcpx cmx_valid. move: (cpadj_proper cmx_valid) (cpmask_adj cp_ok cmx_valid). case: (cpadj cmx cp) => mrt mkt. case: {-4}(ctrband cm cp) (ctrband_correct Ecm cp_ok) => mrc mkc. rewrite -/cc /= -/G -/r => [] [/andP[Emrc Emkc] DccF] /andP[Emrt Emkt] DmtF. case: andP => [{IHi}[mtc_max mtc_min]|_]; last by apply: IHi; last apply: ltnW. rewrite -size_ring_cpmap -/G -/r in Emrc Emrt. pose mt := mrt ++ mkt; pose mc := mrc ++ mkc; pose q := r ++ cpker cp. have Emtq: size mt == size q. by rewrite !size_cat (eqP Emrt) (eqP Emkt) (size_cpker cp_ok) eqxx. have Emcq: size mc == size q. by rewrite !size_cat (eqP Emrc) (eqP Emkc) (size_cpker cp_ok) eqxx. have Uq: simple q by apply: cpmap_simple. rewrite -!mask_cat -/mt -/mc -/q ?(eqP Emrt) ?(eqP Emrc) // {}Dcpx in DccF DmtF. rewrite -mask_cat -/mt -/mc ?(eqP Emrt) ?(eqP Emrc) // in mtc_max mtc_min. case/andP: {no_triad}(no_triad x); split=> /=. move: Uq; rewrite simple_cat => /and3P[_ Urk _]; apply: contra Urk. case/hasP=> y; rewrite mem_rev => r_y xFx. apply/hasP; exists x; first by rewrite mem_nth ?size_cpker. by apply/hasP; exists y. apply/andP; split=> [{mtc_max} | {mtc_min}]; last first. apply: contraL mtc_max => /subsetP ccAx. have{ccAx DccF DmtF}: {subset fband (mask mc q) <= fband (mask mt q)}. move=> y; rewrite -DccF DmtF /= orbF adjC //. by case/hasP=> z /ccAx xAz /adjFr->. move: mc mt Emcq Emtq Uq; rewrite simple_recI. elim: q => [|y q IHq] [|b1 m1] // [|b2 m2] //= Em1 Em2 /andP[qF'y Uq]. have {}qF'y m: (y \in fband (mask m q)) = false. by apply: contraNF qF'y; apply: has_mask. case: b1 b2 => [] [] //= q12F; try apply: (IHq m1 m2) => //. - move=> z q1Fz; have:= q12F z; rewrite !unfold_in /=. case zFy: (cface z y); last exact. by rewrite (closed_connect (fbandF _) zFy) qF'y in q1Fz. - by rewrite -(qF'y m2) q12F // fband_cons connect0. move=> z q1Fz; case/orP: (q12F z q1Fz) => // zFy. by rewrite (closed_connect (fbandF _) zFy) qF'y in q1Fz. pose n_Ax_cc := fcard face (predI (adj x) (fband (insertE cc))). apply: leq_trans mtc_min _; apply: (@leq_trans n_Ax_cc); last first. rewrite -size_filter -(size_map (froot face \o edge)). apply: leq_trans (card_size _); apply: subset_leq_card. apply/subsetP=> y /and3P[/eqP Dy /adjP[z xFz zRy] cc_y]. apply/mapP; exists z; last by rewrite /= (rootP cfaceC zRy). rewrite mem_filter -fconnect_orbit xFz andbT. by rewrite /fband (eq_has (same_cface zRy)). pose nF_qtc := fcard face (fband (filter (fband (mask mt q)) (mask mc q))). apply: eq_leq; transitivity nF_qtc; last first. apply: eq_n_comp_r => y; rewrite unfold_in has_filter inE [fband _ _]DccF. rewrite (eq_filter DmtF) -filter_predI -has_filter adjC //. apply/hasP/andP=> [[z qc_z /andP[yFz zAx]] | [yAx /hasP[z qc_z zFy]]]. by rewrite /= orbF -(adjF yFz) in zAx; split; last by apply/hasP; exists z. by exists z => //=; rewrite zFy -(adjF zFy) yAx. rewrite {n_Ax_cc DccF DmtF}/nF_qtc simple_fcard_fband; last first. by rewrite /simple filter_mask !map_mask !mask_uniq. move: mc mt Emcq Emtq Uq; rewrite simple_recI. elim: q => [|y q IHq] [|b1 m1] // [|b2 m2] //= Em1 Em2 /andP[qF'y Uq]. set q1 := mask m1 q; set q2 := mask m2 q. have {}qF'y m: (y \in fband (mask m q)) = false. by apply: contraNF qF'y; apply: has_mask. have Eq21: filter (fband (y :: q2)) q1 = filter (fband q2) q1. apply: eq_in_filter => z q1z; apply: orb_idl; rewrite cfaceC => yFz. by case/hasP: (qF'y m1); exists z. by case: b1 b2 => [] []; rewrite /= IHq ?Eq21 ?connect0 ?[fband _ y]qF'y. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring cfmap ctree) fourcolor(cfcolor)