proposition: Lemma iso_Lovasz_repl (G : sgraph) (m : G -> nat) (z : G) (i : 'I_(m z)) : @replicate (Lovasz m) ⟨ z, i ⟩ ≃ Lovasz (m[upd z := (m z).+1]).
proof: Proof. set F := replicate _; set m' := update _ _ _; set F' := Lovasz _. have mzS: (m z).+1 = m' z by rewrite /m' updateE. have mxP : m z < m' z by rewrite /m' updateE. have xNzP x : x != z -> m x = m' x by move=> ?; rewrite /m' updateE. have xzP x (j : 'I_(m x)) : x == z -> j < m' z. { by move => xz; rewrite /m' updateE -(eqP xz) ltnW // ltnS ltn_ord. } pose f (x' : F) : F' := if x' isn't Some ⟨ x , j ⟩ then ⟨ z , Ordinal mxP ⟩ else match @boolP (x == z) with | AltTrue xEz => ⟨ z , Ordinal (xzP x j xEz) ⟩ | AltFalse xDz => ⟨ x , cast_ord (xNzP _ xDz) j ⟩ end. pose g (x' : F') : F := let: ⟨ x , j ⟩ := x' in match @boolP (x == z) with | AltTrue xEz => if insub (j : nat) : option 'I_(m z) is Some j' then Some ⟨z, j'⟩ else None | AltFalse xDz => Some ⟨ x , cast_ord (esym (xNzP _ xDz)) j ⟩ end. have can_g : cancel g f. { move=> [x j]; rewrite /g/f/=; case : {-}_ / boolP => [/eqP xEz|xDz]; apply/eqP. - subst x. case: insubP => [j' Hj' vj'|]. + by rewrite altT tagged_eq -ord_eq -vj'. + rewrite -leqNgt tagged_eq -ord_eq /= eqn_leq => -> /=. by rewrite -ltnS mzS ltn_ord. - by rewrite altF tagged_eq -ord_eq /=. } have can_f : cancel f g. { move=> [[x j]|]; last by rewrite /= altT // insubF ?ltnn. rewrite /g/f/=; case : {-}_ / boolP => [xEz|xDz]; apply/eqP. - rewrite altT //= insubT -?(eqP xEz) ?ltn_ord // => lt_j_mx. by rewrite Some_eqE tagged_eq -ord_eq. - by rewrite altF Some_eqE tagged_eq -ord_eq. } apply : Diso' can_f can_g _. move => [[x j]|] [[y o]|]; rewrite /f; last by rewrite !sgP. - case: {-}_ / boolP => [xEz|xDz]; case: {-}_ / boolP => [yEz|yDz]. + move: j o. have [? ?] : x = z /\ y = z by split; apply/eqP. subst x y => j o. by rewrite /edge_rel/= [RHS]/edge_rel/= /LovaszRel/= eqxx !tagged_eq -!ord_eq. + move: j. have ? : x = z by apply/eqP. subst x => j. by rewrite /edge_rel/= [RHS]/edge_rel/= /LovaszRel/= eq_sym (negbTE yDz). + move: o. have ? : y = z by apply/eqP. subst y => o. by rewrite /edge_rel/= [RHS]/edge_rel/= /LovaszRel/= (negbTE xDz). + rewrite /edge_rel/= [RHS]/edge_rel/= /LovaszRel/=. have [xEy|//] := eqVneq x y. move: o; subst y => o. by rewrite !tagged_eq -!ord_eq. - case: {-}_ / boolP => [xEz|xDz]. + rewrite /edge_rel/=/LovaszRel/= eqxx tagged_eq -ord_eq /=. move: j; have ? : x = z by apply/eqP. subst x => j. rewrite !inE /edge_rel/=/LovaszRel/= eqxx !tagged_eq. by rewrite -[j == i]eq_sym orbN eqn_leq negb_and -!ltnNge ltn_ord orbT. + rewrite /edge_rel/=/LovaszRel/= (negbTE xDz) !inE tagged_eqF //=. by rewrite /edge_rel/=/LovaszRel/= eq_sym (negbTE xDz) sgP. - case: {-}_ / boolP => [yEz|yDz]. + rewrite /edge_rel/=/LovaszRel/= eqxx tagged_eq -ord_eq /=. move: o; have ? : y = z by apply/eqP. subst y => o. rewrite !inE /edge_rel/=/LovaszRel/= eqxx !tagged_eq. by rewrite -[o == i]eq_sym orbN eqn_leq negb_and -!ltnNge ltn_ord. + rewrite /edge_rel/=/LovaszRel/= eq_sym (negbTE yDz) !inE tagged_eqF //=. by rewrite /edge_rel/=/LovaszRel/= eq_sym (negbTE yDz). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph sgraph) GraphTheory(dom partition coloring) mathcomp(ssrint)