proposition: Theorem ctree_mem_cpcolor cp et : reflect (even_trace et /\ ring_trace (cpring (cpmap cp)) (sumt et :: et)) (ctree_mem (cpcolor cp) et).
proof: Proof. rewrite ctree_mem_cons_rot -[in _ /\ _](revK cp); set G := cpmap _. have [/= _] := cpcolor0_correct et (rev cp); rewrite /cp_tr0 -/G => etP. apply: {etP}(iffP etP) => [[k [col_k tr_k] _] | [et_even [k col_k tr_k]]]. set rc := rot 1 _ in tr_k. have [rc_ok et_ok]: proper_trace (ptrace rc) /\ proper_trace et. move: (memc0_trace_cpring G col_k) (proper_trace_cpring G col_k) tr_k. rewrite -urtrace_trace -/rc; case: rc => // y rc. rewrite /urtrace /ptrace /= /ttail /eptrace inE => /norP[_]. case: ifP => // _ rc'0 rc_ok /esym/(congr1 (has (pred1 Color0))). by rewrite has_pred1 memc0_permt memc0_ttail rc_ok (negPf rc'0). have [[h2 Eh2] [h1]] := (etail_perm rc_ok, etail_perm et_ok). rewrite /etail /etrace_perm /even_trace {}tr_k even_etail permt_id -{}Eh2. pose h1' := inv_eperm h1; pose h12 := h1' \o h2. move=> eq_h12; split=> //; exists (h12 \o k). by apply: coloring_inj col_k; apply: inj_comp; apply: permc_inj. rewrite 2!map_comp !trace_permt; apply: canRL (mapK (inv_permc h1)) _. rewrite /= -sumt_permt -/(permt h1) {}eq_h12 sumt_permt -map_cons. congr (map _ _); apply: (can_inj (@rotK 1 _)). by rewrite rot1_cons -trace_rot -/rc; case: rc rc_ok. set ic0 := @injcp _ _; pose e0 := k (ic0 true) +c k (ic0 false). have et_ok: proper_trace et. by have:= proper_trace_cpring G col_k; rewrite -tr_k. have e0ok: proper_trace [:: e0]. rewrite /proper_trace /= addc_eq0. have [] // := andP ((gcol_adj col_k) false [:: true] _). by move=> b; rewrite unfold_in /adj orbit_id /= /rlink !fconnect_id eq_sym. have [h0 [he0 _]] := etail_perm e0ok. exists (fun w => Color2 +c h0 (k (ic0 false)) +c h0 (k w)) => [|x]. apply: gcol_perm; split; rewrite // /cp_tr0 -/G /eptrace. move: tr_k; rewrite -urtrace_trace /urtrace; case: (rot 1 _) => //= x p [_]. by move <-; rewrite /etail /etrace_perm et_even permt_id. rewrite [Color2]lock /= -lock; case: x; last by rewrite addcK. by rewrite -addcA -permc_addc (addcC (k _)) he0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype path fingraph) fourcolor(hypermap geometry color coloring cfmap ctree)