Library mathcomp.solvable.burnside_app
+ +
+(* (c) Copyright 2006-2016 Microsoft Corporation and Inria.
+ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+
++ Distributed under the terms of CeCILL-B. *)
+Require Import mathcomp.ssreflect.ssreflect.
+ +
+
+ Application of the Burside formula to count the number of distinct
+ colorings of the vertices of a square and a cube.
+
+
+
+
+Set Implicit Arguments.
+ +
+Import GroupScope.
+ +
+Lemma burnside_formula : ∀ (gT : finGroupType) s (G : {group gT}),
+ uniq s → s =i G →
+ ∀ (sT : finType) (to : {action gT &-> sT}),
+ (#|orbit to G @: setT| × size s)%N = \sum_(p <- s) #|'Fix_to[p]|.
+ +
+ +
+Section colouring.
+ +
+Variable n : nat.
+Definition colors := 'I_n.
+Canonical colors_eqType := Eval hnf in [eqType of colors].
+Canonical colors_choiceType := Eval hnf in [choiceType of colors].
+Canonical colors_countType := Eval hnf in [countType of colors].
+Canonical colors_finType := Eval hnf in [finType of colors].
+ +
+Section square_colouring.
+ +
+Definition square := 'I_4.
+Canonical square_eqType := Eval hnf in [eqType of square].
+Canonical square_choiceType := Eval hnf in [choiceType of square].
+Canonical square_countType := Eval hnf in [countType of square].
+Canonical square_finType := Eval hnf in [finType of square].
+Canonical square_subType := Eval hnf in [subType of square].
+Canonical square_subCountType :=
+ Eval hnf in [subCountType of square].
+Canonical square_subFinType := Eval hnf in [subFinType of square].
+ +
+Definition mksquare i : square := Sub (i %% _) (ltn_mod i 4).
+Definition c0 := mksquare 0.
+Definition c1 := mksquare 1.
+Definition c2 := mksquare 2.
+Definition c3 := mksquare 3.
+ +
+
+
++Set Implicit Arguments.
+ +
+Import GroupScope.
+ +
+Lemma burnside_formula : ∀ (gT : finGroupType) s (G : {group gT}),
+ uniq s → s =i G →
+ ∀ (sT : finType) (to : {action gT &-> sT}),
+ (#|orbit to G @: setT| × size s)%N = \sum_(p <- s) #|'Fix_to[p]|.
+ +
+ +
+Section colouring.
+ +
+Variable n : nat.
+Definition colors := 'I_n.
+Canonical colors_eqType := Eval hnf in [eqType of colors].
+Canonical colors_choiceType := Eval hnf in [choiceType of colors].
+Canonical colors_countType := Eval hnf in [countType of colors].
+Canonical colors_finType := Eval hnf in [finType of colors].
+ +
+Section square_colouring.
+ +
+Definition square := 'I_4.
+Canonical square_eqType := Eval hnf in [eqType of square].
+Canonical square_choiceType := Eval hnf in [choiceType of square].
+Canonical square_countType := Eval hnf in [countType of square].
+Canonical square_finType := Eval hnf in [finType of square].
+Canonical square_subType := Eval hnf in [subType of square].
+Canonical square_subCountType :=
+ Eval hnf in [subCountType of square].
+Canonical square_subFinType := Eval hnf in [subFinType of square].
+ +
+Definition mksquare i : square := Sub (i %% _) (ltn_mod i 4).
+Definition c0 := mksquare 0.
+Definition c1 := mksquare 1.
+Definition c2 := mksquare 2.
+Definition c3 := mksquare 3.
+ +
+
+rotations
+
+
+Definition R1 (sc : square) : square := tnth [tuple c1; c2; c3; c0] sc.
+ +
+Definition R2 (sc : square) : square := tnth [tuple c2; c3; c0; c1] sc.
+ +
+Definition R3 (sc : square) : square := tnth [tuple c3; c0; c1; c2] sc.
+ +
+Ltac get_inv elt l :=
+ match l with
+ | (_, (elt, ?x)) ⇒ x
+ | (elt, ?x) ⇒ x
+ | (?x, _) ⇒ get_inv elt x
+ end.
+ +
+Definition rot_inv := ((R1, R3), (R2, R2), (R3, R1)).
+ +
+Ltac inj_tac :=
+ move: (erefl rot_inv); unfold rot_inv;
+ match goal with |- ?X = _ → injective ?Y ⇒
+ move⇒ _; let x := get_inv Y X in
+ apply: (can_inj (g:=x)); move⇒ [val H1]
+ end.
+ +
+Lemma R1_inj : injective R1.
+ +
+Lemma R2_inj : injective R2.
+ +
+Lemma R3_inj : injective R3.
+ +
+Definition r1 := (perm R1_inj).
+Definition r2 := (perm R2_inj).
+Definition r3 := (perm R3_inj).
+Definition id1 := (1 : {perm square}).
+ +
+Definition is_rot (r : {perm _}) := (r × r1 == r1 × r).
+Definition rot := [set r | is_rot r].
+ +
+Lemma group_set_rot : group_set rot.
+ +
+Canonical rot_group := Group group_set_rot.
+ +
+Definition rotations := [set id1; r1; r2; r3].
+ +
+Lemma rot_eq_c0 : ∀ r s : {perm square},
+ is_rot r → is_rot s → r c0 = s c0 → r = s.
+ +
+Lemma rot_r1 : ∀ r, is_rot r → r = r1 ^+ (r c0).
+ +
+Lemma rotations_is_rot : ∀ r, r \in rotations → is_rot r.
+ +
+Lemma rot_is_rot : rot = rotations.
+ +
+
+
++ +
+Definition R2 (sc : square) : square := tnth [tuple c2; c3; c0; c1] sc.
+ +
+Definition R3 (sc : square) : square := tnth [tuple c3; c0; c1; c2] sc.
+ +
+Ltac get_inv elt l :=
+ match l with
+ | (_, (elt, ?x)) ⇒ x
+ | (elt, ?x) ⇒ x
+ | (?x, _) ⇒ get_inv elt x
+ end.
+ +
+Definition rot_inv := ((R1, R3), (R2, R2), (R3, R1)).
+ +
+Ltac inj_tac :=
+ move: (erefl rot_inv); unfold rot_inv;
+ match goal with |- ?X = _ → injective ?Y ⇒
+ move⇒ _; let x := get_inv Y X in
+ apply: (can_inj (g:=x)); move⇒ [val H1]
+ end.
+ +
+Lemma R1_inj : injective R1.
+ +
+Lemma R2_inj : injective R2.
+ +
+Lemma R3_inj : injective R3.
+ +
+Definition r1 := (perm R1_inj).
+Definition r2 := (perm R2_inj).
+Definition r3 := (perm R3_inj).
+Definition id1 := (1 : {perm square}).
+ +
+Definition is_rot (r : {perm _}) := (r × r1 == r1 × r).
+Definition rot := [set r | is_rot r].
+ +
+Lemma group_set_rot : group_set rot.
+ +
+Canonical rot_group := Group group_set_rot.
+ +
+Definition rotations := [set id1; r1; r2; r3].
+ +
+Lemma rot_eq_c0 : ∀ r s : {perm square},
+ is_rot r → is_rot s → r c0 = s c0 → r = s.
+ +
+Lemma rot_r1 : ∀ r, is_rot r → r = r1 ^+ (r c0).
+ +
+Lemma rotations_is_rot : ∀ r, r \in rotations → is_rot r.
+ +
+Lemma rot_is_rot : rot = rotations.
+ +
+
+symmetries
+
+
+Definition Sh (sc : square) : square := tnth [tuple c1; c0; c3; c2] sc.
+ +
+Lemma Sh_inj : injective Sh.
+ +
+Definition sh := (perm Sh_inj).
+ +
+Lemma sh_inv : sh^-1 = sh.
+ +
+Definition Sv (sc : square) : square := tnth [tuple c3; c2; c1; c0] sc.
+ +
+Lemma Sv_inj : injective Sv.
+ +
+Definition sv := (perm Sv_inj).
+ +
+Lemma sv_inv : sv^-1 = sv.
+ +
+Definition Sd1 (sc : square) : square := tnth [tuple c0; c3; c2; c1] sc.
+ +
+Lemma Sd1_inj : injective Sd1.
+ +
+Definition sd1 := (perm Sd1_inj).
+ +
+Lemma sd1_inv : sd1^-1 = sd1.
+ +
+Definition Sd2 (sc : square) : square := tnth [tuple c2; c1; c0; c3] sc.
+ +
+Lemma Sd2_inj : injective Sd2.
+ +
+Definition sd2 := (perm Sd2_inj).
+ +
+Lemma sd2_inv : sd2^-1 = sd2.
+ +
+Lemma ord_enum4 : enum 'I_4 = [:: c0; c1; c2; c3].
+ +
+Lemma diff_id_sh : 1 != sh.
+ +
+Definition isometries2 := [set 1; sh].
+ +
+Lemma card_iso2 : #|isometries2| = 2.
+ +
+Lemma group_set_iso2 : group_set isometries2.
+Canonical iso2_group := Group group_set_iso2.
+ +
+Definition isometries :=
+ [set p | [|| p == 1, p == r1, p == r2, p == r3,
+ p == sh, p == sv, p == sd1 | p == sd2 ]].
+ +
+Definition opp (sc : square) := tnth [tuple c2; c3; c0; c1] sc.
+ +
+Definition is_iso (p : {perm square}) := ∀ ci, p (opp ci) = opp (p ci).
+ +
+Lemma isometries_iso : ∀ p, p \in isometries → is_iso p.
+ +
+Ltac non_inj p a1 a2 heq1 heq2 :=
+let h1:= fresh "h1" in
+(absurd (p a1 = p a2); first (by red ⇒ - h1; move: (perm_inj h1));
+by rewrite heq1 heq2; apply/eqP).
+ +
+Ltac is_isoPtac p f e0 e1 e2 e3 :=
+ suff ->: p = f by [rewrite inE eqxx ?orbT];
+ let e := fresh "e" in apply/permP;
+ do 5?[case] ⇒ // ?; [move: e0 | move: e1 | move: e2 | move: e3] ⇒ e;
+ apply: etrans (congr1 p _) (etrans e _); apply/eqP; rewrite // permE.
+ +
+Lemma is_isoP : ∀ p, reflect (is_iso p) (p \in isometries).
+ +
+Lemma group_set_iso : group_set isometries.
+ +
+Canonical iso_group := Group group_set_iso.
+ +
+Lemma card_rot : #|rot| = 4.
+ +
+Lemma group_set_rotations : group_set rotations.
+ +
+Canonical rotations_group := Group group_set_rotations.
+ +
+Notation col_squares := {ffun square → colors}.
+ +
+Definition act_f (sc : col_squares) (p : {perm square}) : col_squares :=
+ [ffun z ⇒ sc (p^-1 z)].
+ +
+Lemma act_f_1 : ∀ k, act_f k 1 = k.
+ +
+Lemma act_f_morph : ∀ k x y, act_f k (x × y) = act_f (act_f k x) y.
+ +
+Definition to := TotalAction act_f_1 act_f_morph.
+ +
+Definition square_coloring_number2 := #|orbit to isometries2 @: setT|.
+Definition square_coloring_number4 := #|orbit to rotations @: setT|.
+Definition square_coloring_number8 := #|orbit to isometries @: setT|.
+ +
+Lemma Fid : 'Fix_to(1) = setT.
+ +
+Lemma card_Fid : #|'Fix_to(1)| = (n ^ 4)%N.
+ +
+Definition coin0 (sc : col_squares) : colors := sc c0.
+Definition coin1 (sc : col_squares) : colors := sc c1.
+Definition coin2 (sc : col_squares) : colors := sc c2.
+Definition coin3 (sc : col_squares) : colors := sc c3.
+ +
+Lemma eqperm_map : ∀ p1 p2 : col_squares,
+ (p1 == p2) = all (fun s ⇒ p1 s == p2 s) [:: c0; c1; c2; c3].
+ +
+Lemma F_Sh :
+ 'Fix_to[sh] = [set x | (coin0 x == coin1 x) && (coin2 x == coin3 x)].
+ +
+Lemma F_Sv :
+ 'Fix_to[sv] = [set x | (coin0 x == coin3 x) && (coin2 x == coin1 x)].
+ +
+Ltac inv_tac :=
+ apply: esym (etrans _ (mul1g _)); apply: canRL (mulgK _) _;
+ let a := fresh "a" in apply/permP ⇒ a;
+ apply/eqP; rewrite permM !permE; case: a; do 4?case.
+ +
+Lemma r1_inv : r1^-1 = r3.
+ +
+Lemma r2_inv : r2^-1 = r2.
+ +
+Lemma r3_inv : r3^-1 = r1.
+ +
+Lemma F_r2 :
+ 'Fix_to[r2] = [set x | (coin0 x == coin2 x) && (coin1 x == coin3 x)].
+ +
+Lemma F_r1 : 'Fix_to[r1] =
+ [set x | (coin0 x == coin1 x)&&(coin1 x == coin2 x)&&(coin2 x == coin3 x)].
+ +
+Lemma F_r3 : 'Fix_to[r3] =
+ [set x | (coin0 x == coin1 x)&&(coin1 x == coin2 x)&&(coin2 x == coin3 x)].
+ +
+Lemma card_n2 : ∀ x y z t : square, uniq [:: x; y; z; t] →
+ #|[set p : col_squares | (p x == p y) && (p z == p t)]| = (n ^ 2)%N.
+ +
+Lemma card_n :
+ #|[set x | (coin0 x == coin1 x)&&(coin1 x == coin2 x)&& (coin2 x == coin3 x)]|
+ = n.
+ +
+Lemma burnside_app2 : (square_coloring_number2 × 2 = n ^ 4 + n ^ 2)%N.
+ +
+Lemma burnside_app_rot :
+ (square_coloring_number4 × 4 = n ^ 4 + n ^ 2 + 2 × n)%N.
+ +
+Lemma F_Sd1 : 'Fix_to[sd1] = [set x | coin1 x == coin3 x].
+ +
+Lemma card_n3 : ∀ x y : square, x != y →
+ #|[set k : col_squares | k x == k y]| = (n ^ 3)%N.
+ +
+Lemma F_Sd2 : 'Fix_to[sd2] = [set x | coin0 x == coin2 x].
+ +
+Lemma burnside_app_iso :
+ (square_coloring_number8 × 8 = n ^ 4 + 2 × n ^ 3 + 3 × n ^ 2 + 2 × n)%N.
+ +
+End square_colouring.
+ +
+Section cube_colouring.
+ +
+Definition cube := 'I_6.
+Canonical cube_eqType := Eval hnf in [eqType of cube].
+Canonical cube_choiceType := Eval hnf in [choiceType of cube].
+Canonical cube_countType := Eval hnf in [countType of cube].
+Canonical cube_finType := Eval hnf in [finType of cube].
+Canonical cube_subType := Eval hnf in [subType of cube].
+Canonical cube_subCountType := Eval hnf in [subCountType of cube].
+Canonical cube_subFinType := Eval hnf in [subFinType of cube].
+ +
+Definition mkFcube i : cube := Sub (i %% 6) (ltn_mod i 6).
+Definition F0 := mkFcube 0.
+Definition F1 := mkFcube 1.
+Definition F2 := mkFcube 2.
+Definition F3 := mkFcube 3.
+Definition F4 := mkFcube 4.
+Definition F5 := mkFcube 5.
+ +
+
+
++ +
+Lemma Sh_inj : injective Sh.
+ +
+Definition sh := (perm Sh_inj).
+ +
+Lemma sh_inv : sh^-1 = sh.
+ +
+Definition Sv (sc : square) : square := tnth [tuple c3; c2; c1; c0] sc.
+ +
+Lemma Sv_inj : injective Sv.
+ +
+Definition sv := (perm Sv_inj).
+ +
+Lemma sv_inv : sv^-1 = sv.
+ +
+Definition Sd1 (sc : square) : square := tnth [tuple c0; c3; c2; c1] sc.
+ +
+Lemma Sd1_inj : injective Sd1.
+ +
+Definition sd1 := (perm Sd1_inj).
+ +
+Lemma sd1_inv : sd1^-1 = sd1.
+ +
+Definition Sd2 (sc : square) : square := tnth [tuple c2; c1; c0; c3] sc.
+ +
+Lemma Sd2_inj : injective Sd2.
+ +
+Definition sd2 := (perm Sd2_inj).
+ +
+Lemma sd2_inv : sd2^-1 = sd2.
+ +
+Lemma ord_enum4 : enum 'I_4 = [:: c0; c1; c2; c3].
+ +
+Lemma diff_id_sh : 1 != sh.
+ +
+Definition isometries2 := [set 1; sh].
+ +
+Lemma card_iso2 : #|isometries2| = 2.
+ +
+Lemma group_set_iso2 : group_set isometries2.
+Canonical iso2_group := Group group_set_iso2.
+ +
+Definition isometries :=
+ [set p | [|| p == 1, p == r1, p == r2, p == r3,
+ p == sh, p == sv, p == sd1 | p == sd2 ]].
+ +
+Definition opp (sc : square) := tnth [tuple c2; c3; c0; c1] sc.
+ +
+Definition is_iso (p : {perm square}) := ∀ ci, p (opp ci) = opp (p ci).
+ +
+Lemma isometries_iso : ∀ p, p \in isometries → is_iso p.
+ +
+Ltac non_inj p a1 a2 heq1 heq2 :=
+let h1:= fresh "h1" in
+(absurd (p a1 = p a2); first (by red ⇒ - h1; move: (perm_inj h1));
+by rewrite heq1 heq2; apply/eqP).
+ +
+Ltac is_isoPtac p f e0 e1 e2 e3 :=
+ suff ->: p = f by [rewrite inE eqxx ?orbT];
+ let e := fresh "e" in apply/permP;
+ do 5?[case] ⇒ // ?; [move: e0 | move: e1 | move: e2 | move: e3] ⇒ e;
+ apply: etrans (congr1 p _) (etrans e _); apply/eqP; rewrite // permE.
+ +
+Lemma is_isoP : ∀ p, reflect (is_iso p) (p \in isometries).
+ +
+Lemma group_set_iso : group_set isometries.
+ +
+Canonical iso_group := Group group_set_iso.
+ +
+Lemma card_rot : #|rot| = 4.
+ +
+Lemma group_set_rotations : group_set rotations.
+ +
+Canonical rotations_group := Group group_set_rotations.
+ +
+Notation col_squares := {ffun square → colors}.
+ +
+Definition act_f (sc : col_squares) (p : {perm square}) : col_squares :=
+ [ffun z ⇒ sc (p^-1 z)].
+ +
+Lemma act_f_1 : ∀ k, act_f k 1 = k.
+ +
+Lemma act_f_morph : ∀ k x y, act_f k (x × y) = act_f (act_f k x) y.
+ +
+Definition to := TotalAction act_f_1 act_f_morph.
+ +
+Definition square_coloring_number2 := #|orbit to isometries2 @: setT|.
+Definition square_coloring_number4 := #|orbit to rotations @: setT|.
+Definition square_coloring_number8 := #|orbit to isometries @: setT|.
+ +
+Lemma Fid : 'Fix_to(1) = setT.
+ +
+Lemma card_Fid : #|'Fix_to(1)| = (n ^ 4)%N.
+ +
+Definition coin0 (sc : col_squares) : colors := sc c0.
+Definition coin1 (sc : col_squares) : colors := sc c1.
+Definition coin2 (sc : col_squares) : colors := sc c2.
+Definition coin3 (sc : col_squares) : colors := sc c3.
+ +
+Lemma eqperm_map : ∀ p1 p2 : col_squares,
+ (p1 == p2) = all (fun s ⇒ p1 s == p2 s) [:: c0; c1; c2; c3].
+ +
+Lemma F_Sh :
+ 'Fix_to[sh] = [set x | (coin0 x == coin1 x) && (coin2 x == coin3 x)].
+ +
+Lemma F_Sv :
+ 'Fix_to[sv] = [set x | (coin0 x == coin3 x) && (coin2 x == coin1 x)].
+ +
+Ltac inv_tac :=
+ apply: esym (etrans _ (mul1g _)); apply: canRL (mulgK _) _;
+ let a := fresh "a" in apply/permP ⇒ a;
+ apply/eqP; rewrite permM !permE; case: a; do 4?case.
+ +
+Lemma r1_inv : r1^-1 = r3.
+ +
+Lemma r2_inv : r2^-1 = r2.
+ +
+Lemma r3_inv : r3^-1 = r1.
+ +
+Lemma F_r2 :
+ 'Fix_to[r2] = [set x | (coin0 x == coin2 x) && (coin1 x == coin3 x)].
+ +
+Lemma F_r1 : 'Fix_to[r1] =
+ [set x | (coin0 x == coin1 x)&&(coin1 x == coin2 x)&&(coin2 x == coin3 x)].
+ +
+Lemma F_r3 : 'Fix_to[r3] =
+ [set x | (coin0 x == coin1 x)&&(coin1 x == coin2 x)&&(coin2 x == coin3 x)].
+ +
+Lemma card_n2 : ∀ x y z t : square, uniq [:: x; y; z; t] →
+ #|[set p : col_squares | (p x == p y) && (p z == p t)]| = (n ^ 2)%N.
+ +
+Lemma card_n :
+ #|[set x | (coin0 x == coin1 x)&&(coin1 x == coin2 x)&& (coin2 x == coin3 x)]|
+ = n.
+ +
+Lemma burnside_app2 : (square_coloring_number2 × 2 = n ^ 4 + n ^ 2)%N.
+ +
+Lemma burnside_app_rot :
+ (square_coloring_number4 × 4 = n ^ 4 + n ^ 2 + 2 × n)%N.
+ +
+Lemma F_Sd1 : 'Fix_to[sd1] = [set x | coin1 x == coin3 x].
+ +
+Lemma card_n3 : ∀ x y : square, x != y →
+ #|[set k : col_squares | k x == k y]| = (n ^ 3)%N.
+ +
+Lemma F_Sd2 : 'Fix_to[sd2] = [set x | coin0 x == coin2 x].
+ +
+Lemma burnside_app_iso :
+ (square_coloring_number8 × 8 = n ^ 4 + 2 × n ^ 3 + 3 × n ^ 2 + 2 × n)%N.
+ +
+End square_colouring.
+ +
+Section cube_colouring.
+ +
+Definition cube := 'I_6.
+Canonical cube_eqType := Eval hnf in [eqType of cube].
+Canonical cube_choiceType := Eval hnf in [choiceType of cube].
+Canonical cube_countType := Eval hnf in [countType of cube].
+Canonical cube_finType := Eval hnf in [finType of cube].
+Canonical cube_subType := Eval hnf in [subType of cube].
+Canonical cube_subCountType := Eval hnf in [subCountType of cube].
+Canonical cube_subFinType := Eval hnf in [subFinType of cube].
+ +
+Definition mkFcube i : cube := Sub (i %% 6) (ltn_mod i 6).
+Definition F0 := mkFcube 0.
+Definition F1 := mkFcube 1.
+Definition F2 := mkFcube 2.
+Definition F3 := mkFcube 3.
+Definition F4 := mkFcube 4.
+Definition F5 := mkFcube 5.
+ +
+
+ axial symetries
+
+
+Definition S05 := [:: F0; F4; F3; F2; F1; F5].
+Definition S05f (sc : cube) : cube := tnth [tuple of S05] sc.
+ +
+Definition S14 := [:: F5; F1; F3; F2; F4; F0].
+Definition S14f (sc : cube) : cube := tnth [tuple of S14] sc.
+ +
+Definition S23 := [:: F5; F4; F2; F3; F1; F0].
+Definition S23f (sc : cube) : cube := tnth [tuple of S23] sc.
+ +
+
+
++Definition S05f (sc : cube) : cube := tnth [tuple of S05] sc.
+ +
+Definition S14 := [:: F5; F1; F3; F2; F4; F0].
+Definition S14f (sc : cube) : cube := tnth [tuple of S14] sc.
+ +
+Definition S23 := [:: F5; F4; F2; F3; F1; F0].
+Definition S23f (sc : cube) : cube := tnth [tuple of S23] sc.
+ +
+
+ rotations 90
+
+
+Definition R05 := [:: F0; F2; F4; F1; F3; F5].
+Definition R05f (sc : cube) : cube := tnth [tuple of R05] sc.
+Definition R50 := [:: F0; F3; F1; F4; F2; F5].
+Definition R50f (sc : cube) : cube := tnth [tuple of R50] sc.
+Definition R14 := [:: F3; F1; F0; F5; F4; F2].
+Definition R14f (sc : cube) : cube := tnth [tuple of R14] sc.
+Definition R41 := [:: F2; F1; F5; F0; F4; F3].
+Definition R41f (sc : cube) : cube := tnth [tuple of R41] sc.
+Definition R23 := [:: F1; F5; F2; F3; F0; F4].
+Definition R23f (sc : cube) : cube := tnth [tuple of R23] sc.
+Definition R32 := [:: F4; F0; F2; F3; F5; F1].
+Definition R32f (sc : cube) : cube := tnth [tuple of R32] sc.
+
+
++Definition R05f (sc : cube) : cube := tnth [tuple of R05] sc.
+Definition R50 := [:: F0; F3; F1; F4; F2; F5].
+Definition R50f (sc : cube) : cube := tnth [tuple of R50] sc.
+Definition R14 := [:: F3; F1; F0; F5; F4; F2].
+Definition R14f (sc : cube) : cube := tnth [tuple of R14] sc.
+Definition R41 := [:: F2; F1; F5; F0; F4; F3].
+Definition R41f (sc : cube) : cube := tnth [tuple of R41] sc.
+Definition R23 := [:: F1; F5; F2; F3; F0; F4].
+Definition R23f (sc : cube) : cube := tnth [tuple of R23] sc.
+Definition R32 := [:: F4; F0; F2; F3; F5; F1].
+Definition R32f (sc : cube) : cube := tnth [tuple of R32] sc.
+
+ rotations 120
+
+
+Definition R024 := [:: F2; F5; F4; F1; F0; F3].
+Definition R024f (sc : cube) : cube := tnth [tuple of R024] sc.
+Definition R042 := [:: F4; F3; F0; F5; F2; F1].
+Definition R042f (sc : cube) : cube := tnth [tuple of R042] sc.
+Definition R012 := [:: F1; F2; F0; F5; F3; F4].
+Definition R012f (sc : cube) : cube := tnth [tuple of R012] sc.
+Definition R021 := [:: F2; F0; F1; F4; F5; F3].
+Definition R021f (sc : cube) : cube := tnth [tuple of R021] sc.
+Definition R031 := [:: F3; F0; F4; F1; F5; F2].
+Definition R031f (sc : cube) : cube := tnth [tuple of R031] sc.
+Definition R013 := [:: F1; F3; F5; F0; F2; F4].
+Definition R013f (sc : cube) : cube := tnth [tuple of R013] sc.
+Definition R043 := [:: F4; F2; F5; F0; F3; F1].
+Definition R043f (sc : cube) : cube := tnth [tuple of R043] sc.
+Definition R034 := [:: F3; F5; F1; F4; F0; F2].
+Definition R034f (sc : cube) : cube := tnth [tuple of R034] sc.
+
+
++Definition R024f (sc : cube) : cube := tnth [tuple of R024] sc.
+Definition R042 := [:: F4; F3; F0; F5; F2; F1].
+Definition R042f (sc : cube) : cube := tnth [tuple of R042] sc.
+Definition R012 := [:: F1; F2; F0; F5; F3; F4].
+Definition R012f (sc : cube) : cube := tnth [tuple of R012] sc.
+Definition R021 := [:: F2; F0; F1; F4; F5; F3].
+Definition R021f (sc : cube) : cube := tnth [tuple of R021] sc.
+Definition R031 := [:: F3; F0; F4; F1; F5; F2].
+Definition R031f (sc : cube) : cube := tnth [tuple of R031] sc.
+Definition R013 := [:: F1; F3; F5; F0; F2; F4].
+Definition R013f (sc : cube) : cube := tnth [tuple of R013] sc.
+Definition R043 := [:: F4; F2; F5; F0; F3; F1].
+Definition R043f (sc : cube) : cube := tnth [tuple of R043] sc.
+Definition R034 := [:: F3; F5; F1; F4; F0; F2].
+Definition R034f (sc : cube) : cube := tnth [tuple of R034] sc.
+
+ last symmetries
+
+
+Definition S1 := [:: F5; F2; F1; F4; F3; F0].
+Definition S1f (sc : cube) : cube := tnth [tuple of S1] sc.
+Definition S2 := [:: F5; F3; F4; F1; F2; F0].
+Definition S2f (sc : cube) : cube := tnth [tuple of S2] sc.
+Definition S3 := [:: F1; F0; F3; F2; F5; F4].
+Definition S3f (sc : cube) : cube := tnth [tuple of S3] sc.
+Definition S4 := [:: F4; F5; F3; F2; F0; F1].
+Definition S4f (sc : cube) : cube := tnth [tuple of S4] sc.
+Definition S5 := [:: F2; F4; F0; F5; F1; F3].
+Definition S5f (sc : cube) : cube := tnth [tuple of S5] sc.
+Definition S6 := [::F3; F4; F5; F0; F1; F2].
+Definition S6f (sc : cube) : cube := tnth [tuple of S6] sc.
+ +
+Lemma S1_inv : involutive S1f.
+ +
+Lemma S2_inv : involutive S2f.
+ +
+Lemma S3_inv : involutive S3f.
+ +
+Lemma S4_inv : involutive S4f.
+ +
+Lemma S5_inv : involutive S5f.
+ +
+Lemma S6_inv : involutive S6f.
+ +
+Lemma S05_inj : injective S05f.
+ +
+Lemma S14_inj : injective S14f.
+ +
+Lemma S23_inv : involutive S23f.
+ +
+Lemma R05_inj : injective R05f.
+ +
+Lemma R14_inj : injective R14f.
+ +
+Lemma R23_inj : injective R23f.
+ +
+Lemma R50_inj : injective R50f.
+ +
+Lemma R41_inj : injective R41f.
+ +
+Lemma R32_inj : injective R32f.
+ +
+Lemma R024_inj : injective R024f.
+ +
+Lemma R042_inj : injective R042f.
+ +
+Lemma R012_inj : injective R012f.
+ +
+Lemma R021_inj : injective R021f.
+ +
+Lemma R031_inj : injective R031f.
+ +
+Lemma R013_inj : injective R013f.
+ +
+Lemma R043_inj : injective R043f.
+ +
+Lemma R034_inj : injective R034f.
+ +
+Definition id3 := 1 : {perm cube}.
+ +
+Definition s05 := (perm S05_inj).
+ +
+Definition s14 : {perm cube}.
+ +
+Definition s23 := (perm (inv_inj S23_inv)).
+Definition r05 := (perm R05_inj).
+Definition r14 := (perm R14_inj).
+Definition r23 := (perm R23_inj).
+Definition r50 := (perm R50_inj).
+Definition r41 := (perm R41_inj).
+Definition r32 := (perm R32_inj).
+Definition r024 := (perm R024_inj).
+Definition r042 := (perm R042_inj).
+Definition r012 := (perm R012_inj).
+Definition r021 := (perm R021_inj).
+Definition r031 := (perm R031_inj).
+Definition r013 := (perm R013_inj).
+Definition r043 := (perm R043_inj).
+Definition r034 := (perm R034_inj).
+ +
+Definition s1 := (perm (inv_inj S1_inv)).
+Definition s2 := (perm (inv_inj S2_inv)).
+Definition s3 := (perm (inv_inj S3_inv)).
+Definition s4 := (perm (inv_inj S4_inv)).
+Definition s5 := (perm (inv_inj S5_inv)).
+Definition s6 := (perm (inv_inj S6_inv)).
+ +
+Definition dir_iso3 := [set p |
+[|| id3 == p, s05 == p, s14 == p, s23 == p, r05 == p, r14 == p, r23 == p,
+ r50 == p, r41 == p, r32 == p, r024 == p, r042 == p, r012 == p, r021 == p,
+ r031 == p, r013 == p, r043 == p, r034 == p,
+ s1 == p, s2 == p, s3 == p, s4 == p, s5 == p | s6 == p]].
+ +
+Definition dir_iso3l := [:: id3; s05; s14; s23; r05; r14; r23; r50; r41;
+ r32; r024; r042; r012; r021; r031; r013; r043; r034;
+ s1; s2; s3; s4; s5; s6].
+ +
+Definition S0 := [:: F5; F4; F3; F2; F1; F0].
+Definition S0f (sc : cube) : cube := tnth [tuple of S0] sc.
+ +
+Lemma S0_inv : involutive S0f.
+ +
+Definition s0 := (perm (inv_inj S0_inv)).
+ +
+Definition is_iso3 (p : {perm cube}) := ∀ fi, p (s0 fi) = s0 (p fi).
+ +
+Lemma dir_iso_iso3 : ∀ p, p \in dir_iso3 → is_iso3 p.
+ +
+Lemma iso3_ndir : ∀ p, p \in dir_iso3 → is_iso3 (s0 × p).
+ +
+Definition sop (p : {perm cube}) : seq cube := val (val (val p)).
+ +
+Lemma sop_inj : injective sop.
+ +
+Definition prod_tuple (t1 t2 : seq cube) :=
+ map (fun n : 'I_6 ⇒ nth F0 t2 n) t1.
+ +
+Lemma sop_spec : ∀ x (n0 : 'I_6), nth F0 (sop x) n0 = x n0.
+ +
+Lemma prod_t_correct : ∀ (x y : {perm cube}) (i : cube),
+ (x × y) i = nth F0 (prod_tuple (sop x) (sop y)) i.
+ +
+Lemma sop_morph : {morph sop : x y / x × y >-> prod_tuple x y}.
+ +
+Definition ecubes : seq cube := [:: F0; F1; F2; F3; F4; F5].
+ +
+Lemma ecubes_def : ecubes = enum (@predT cube).
+ +
+Definition seq_iso_L := [::
+ [:: F0; F1; F2; F3; F4; F5];
+ S05; S14; S23; R05; R14; R23; R50; R41; R32;
+ R024; R042; R012; R021; R031; R013; R043; R034;
+ S1; S2; S3; S4; S5; S6].
+ +
+Lemma seqs1 : ∀ f injf, sop (@perm _ f injf) = map f ecubes.
+ +
+Lemma Lcorrect : seq_iso_L == map sop [:: id3; s05; s14; s23; r05; r14; r23;
+ r50; r41; r32; r024; r042; r012; r021; r031; r013; r043; r034;
+ s1; s2; s3; s4; s5; s6].
+ +
+Lemma iso0_1 : dir_iso3 =i dir_iso3l.
+ +
+Lemma L_iso : ∀ p, (p \in dir_iso3) = (sop p \in seq_iso_L).
+ +
+Lemma stable : ∀ x y,
+ x \in dir_iso3 → y \in dir_iso3 → x × y \in dir_iso3.
+ +
+Lemma iso_eq_F0_F1 : ∀ r s : {perm cube}, r \in dir_iso3 →
+ s \in dir_iso3 → r F0 = s F0 → r F1 = s F1 → r = s.
+ +
+Lemma ndir_s0p : ∀ p, p \in dir_iso3 → s0 × p \notin dir_iso3.
+ +
+Definition indir_iso3l := map (mulg s0) dir_iso3l.
+ +
+Definition iso3l := dir_iso3l ++ indir_iso3l.
+ +
+Definition seq_iso3_L := map sop iso3l.
+ +
+Lemma eqperm : ∀ p1 p2 : {perm cube},
+ (p1 == p2) = all (fun s ⇒ p1 s == p2 s) ecubes.
+ +
+Lemma iso_eq_F0_F1_F2 : ∀ r s : {perm cube}, is_iso3 r →
+ is_iso3 s → r F0 = s F0 → r F1 = s F1 → r F2 = s F2 → r = s.
+ +
+Ltac iso_tac :=
+ let a := fresh "a" in apply/permP ⇒ a;
+ apply/eqP; rewrite !permM !permE; case: a; do 6?case.
+ +
+Ltac inv_tac :=
+ apply: esym (etrans _ (mul1g _)); apply: canRL (mulgK _) _; iso_tac.
+ +
+Lemma dir_s0p : ∀ p, (s0 × p) \in dir_iso3 → p \notin dir_iso3.
+ +
+Definition is_iso3b p := (p × s0 == s0 × p).
+Definition iso3 := [set p | is_iso3b p].
+ +
+Lemma is_iso3P : ∀ p, reflect (is_iso3 p) (p \in iso3).
+ +
+Lemma group_set_iso3 : group_set iso3.
+ +
+Canonical iso_group3 := Group group_set_iso3.
+ +
+Lemma group_set_diso3 : group_set dir_iso3.
+Canonical diso_group3 := Group group_set_diso3.
+ +
+Lemma gen_diso3 : dir_iso3 = <<[set r05; r14]>>.
+ +
+Notation col_cubes := {ffun cube → colors}.
+ +
+Definition act_g (sc : col_cubes) (p : {perm cube}) : col_cubes :=
+ [ffun z ⇒ sc (p^-1 z)].
+ +
+Lemma act_g_1 : ∀ k, act_g k 1 = k.
+ +
+Lemma act_g_morph : ∀ k x y, act_g k (x × y) = act_g (act_g k x) y.
+ +
+Definition to_g := TotalAction act_g_1 act_g_morph.
+ +
+Definition cube_coloring_number24 := #|orbit to_g diso_group3 @: setT|.
+ +
+Lemma Fid3 : 'Fix_to_g[1] = setT.
+ +
+Lemma card_Fid3 : #|'Fix_to_g[1]| = (n ^ 6)%N.
+ +
+Definition col0 (sc : col_cubes) : colors := sc F0.
+Definition col1 (sc : col_cubes) : colors := sc F1.
+Definition col2 (sc : col_cubes) : colors := sc F2.
+Definition col3 (sc : col_cubes) : colors := sc F3.
+Definition col4 (sc : col_cubes) : colors := sc F4.
+Definition col5 (sc : col_cubes) : colors := sc F5.
+ +
+Lemma eqperm_map2 : ∀ p1 p2 : col_cubes,
+ (p1 == p2) = all (fun s ⇒ p1 s == p2 s) [:: F0; F1; F2; F3; F4; F5].
+ +
+Notation infE := (sameP afix1P eqP).
+ +
+Lemma F_s05 :
+ 'Fix_to_g[s05] = [set x | (col1 x == col4 x) && (col2 x == col3 x)].
+ +
+Lemma F_s14 :
+ 'Fix_to_g[s14]= [set x | (col0 x == col5 x) && (col2 x == col3 x)].
+ +
+Lemma r05_inv : r05^-1 = r50.
+ +
+Lemma r50_inv : r50^-1 = r05.
+ +
+Lemma r14_inv : r14^-1 = r41.
+ +
+Lemma r41_inv : r41^-1 = r14.
+ +
+Lemma s23_inv : s23^-1 = s23.
+ +
+Lemma F_s23 :
+ 'Fix_to_g[s23] = [set x | (col0 x == col5 x) && (col1 x == col4 x)].
+ +
+Lemma F_r05 : 'Fix_to_g[r05]=
+ [set x | (col1 x == col2 x) && (col2 x == col3 x)
+ && (col3 x == col4 x)].
+ +
+Lemma F_r50 : 'Fix_to_g[r50]=
+ [set x | (col1 x == col2 x) && (col2 x == col3 x)
+ && (col3 x == col4 x)].
+ +
+Lemma F_r23 : 'Fix_to_g[r23] =
+ [set x | (col0 x == col1 x) && (col1 x == col4 x)
+ && (col4 x == col5 x)].
+ +
+Lemma F_r32 : 'Fix_to_g[r32] =
+ [set x | (col0 x == col1 x) && (col1 x == col4 x)
+ && (col4 x == col5 x)].
+ +
+Lemma F_r14 : 'Fix_to_g[r14] =
+ [set x | (col0 x == col2 x) && (col2 x == col3 x) && (col3 x == col5 x)].
+ +
+Lemma F_r41 : 'Fix_to_g[r41] =
+ [set x | (col0 x == col2 x) && (col2 x == col3 x) && (col3 x == col5 x)].
+ +
+Lemma F_r024 : 'Fix_to_g[r024] =
+ [set x | (col0 x == col4 x) && (col4 x == col2 x) && (col1 x == col3 x)
+ && (col3 x == col5 x) ].
+ +
+Lemma F_r042 : 'Fix_to_g[r042] =
+ [set x | (col0 x == col4 x) && (col4 x == col2 x) && (col1 x == col3 x)
+ && (col3 x == col5 x)].
+ +
+Lemma F_r012 : 'Fix_to_g[r012] =
+ [set x | (col0 x == col2 x) && (col2 x == col1 x) && (col3 x == col4 x)
+ && (col4 x == col5 x)].
+ +
+Lemma F_r021 : 'Fix_to_g[r021] =
+ [set x | (col0 x == col2 x) && (col2 x == col1 x) && (col3 x == col4 x)
+ && (col4 x == col5 x)].
+ +
+Lemma F_r031 : 'Fix_to_g[r031] =
+ [set x | (col0 x == col3 x) && (col3 x == col1 x) && (col2 x == col4 x)
+ && (col4 x == col5 x)].
+ +
+Lemma F_r013 : 'Fix_to_g[r013] =
+ [set x | (col0 x == col3 x) && (col3 x == col1 x) && (col2 x == col4 x)
+ && (col4 x == col5 x)].
+ +
+Lemma F_r043 : 'Fix_to_g[r043] =
+ [set x | (col0 x == col4 x) && (col4 x == col3 x) && (col1 x == col2 x)
+ && (col2 x == col5 x)].
+ +
+Lemma F_r034 : 'Fix_to_g[r034] =
+ [set x | (col0 x == col4 x) && (col4 x == col3 x) && (col1 x == col2 x)
+ && (col2 x == col5 x)].
+ +
+Lemma F_s1 : 'Fix_to_g[s1] =
+ [set x | (col0 x == col5 x) && (col1 x == col2 x) && (col3 x == col4 x)].
+ +
+Lemma F_s2 : 'Fix_to_g[s2] =
+ [set x | (col0 x == col5 x) && (col1 x == col3 x) && (col2 x == col4 x)].
+ +
+Lemma F_s3 : 'Fix_to_g[s3] =
+ [set x | (col0 x == col1 x) && (col2 x == col3 x) && (col4 x == col5 x)].
+ +
+Lemma F_s4 : 'Fix_to_g[s4] =
+ [set x | (col0 x == col4 x) && (col1 x == col5 x) && (col2 x == col3 x)].
+ +
+Lemma F_s5 : 'Fix_to_g[s5] =
+ [set x | (col0 x == col2 x) && (col1 x == col4 x) && (col3 x == col5 x)].
+ +
+Lemma F_s6 : 'Fix_to_g[s6] =
+ [set x | (col0 x == col3 x) && (col1 x == col4 x) && (col2 x == col5 x)].
+ +
+Lemma uniq4_uniq6 : ∀ x y z t : cube,
+ uniq [:: x; y; z; t] → ∃ u, ∃ v, uniq [:: x; y; z; t; u; v].
+ +
+Lemma card_n4 : ∀ x y z t : cube, uniq [:: x; y; z; t] →
+ #|[set p : col_cubes | (p x == p y) && (p z == p t)]| = (n ^ 4)%N.
+ +
+Lemma card_n3_3 : ∀ x y z t: cube, uniq [:: x; y; z; t] →
+ #|[set p : col_cubes | (p x == p y) && (p y == p z)&& (p z == p t)]|
+ = (n ^ 3)%N.
+ +
+Lemma card_n2_3 : ∀ x y z t u v: cube, uniq [:: x; y; z; t; u; v] →
+ #|[set p : col_cubes | (p x == p y) && (p y == p z)&& (p t == p u )
+ && (p u== p v)]| = (n ^ 2)%N.
+ +
+Lemma card_n3s : ∀ x y z t u v: cube, uniq [:: x; y; z; t; u; v] →
+ #|[set p : col_cubes | (p x == p y) && (p z == p t)&& (p u == p v )]|
+ = (n ^ 3)%N.
+ +
+Lemma burnside_app_iso3 :
+ (cube_coloring_number24 × 24 =
+ n ^ 6 + 6 × n ^ 3 + 3 × n ^ 4 + 8 × (n ^ 2) + 6 × n ^ 3)%N.
+ +
+End cube_colouring.
+ +
+End colouring.
+ +
+Corollary burnside_app_iso_3_3col: cube_coloring_number24 3 = 57.
+ +
+Corollary burnside_app_iso_2_4col: square_coloring_number8 4 = 55.
+ +
+
++Definition S1f (sc : cube) : cube := tnth [tuple of S1] sc.
+Definition S2 := [:: F5; F3; F4; F1; F2; F0].
+Definition S2f (sc : cube) : cube := tnth [tuple of S2] sc.
+Definition S3 := [:: F1; F0; F3; F2; F5; F4].
+Definition S3f (sc : cube) : cube := tnth [tuple of S3] sc.
+Definition S4 := [:: F4; F5; F3; F2; F0; F1].
+Definition S4f (sc : cube) : cube := tnth [tuple of S4] sc.
+Definition S5 := [:: F2; F4; F0; F5; F1; F3].
+Definition S5f (sc : cube) : cube := tnth [tuple of S5] sc.
+Definition S6 := [::F3; F4; F5; F0; F1; F2].
+Definition S6f (sc : cube) : cube := tnth [tuple of S6] sc.
+ +
+Lemma S1_inv : involutive S1f.
+ +
+Lemma S2_inv : involutive S2f.
+ +
+Lemma S3_inv : involutive S3f.
+ +
+Lemma S4_inv : involutive S4f.
+ +
+Lemma S5_inv : involutive S5f.
+ +
+Lemma S6_inv : involutive S6f.
+ +
+Lemma S05_inj : injective S05f.
+ +
+Lemma S14_inj : injective S14f.
+ +
+Lemma S23_inv : involutive S23f.
+ +
+Lemma R05_inj : injective R05f.
+ +
+Lemma R14_inj : injective R14f.
+ +
+Lemma R23_inj : injective R23f.
+ +
+Lemma R50_inj : injective R50f.
+ +
+Lemma R41_inj : injective R41f.
+ +
+Lemma R32_inj : injective R32f.
+ +
+Lemma R024_inj : injective R024f.
+ +
+Lemma R042_inj : injective R042f.
+ +
+Lemma R012_inj : injective R012f.
+ +
+Lemma R021_inj : injective R021f.
+ +
+Lemma R031_inj : injective R031f.
+ +
+Lemma R013_inj : injective R013f.
+ +
+Lemma R043_inj : injective R043f.
+ +
+Lemma R034_inj : injective R034f.
+ +
+Definition id3 := 1 : {perm cube}.
+ +
+Definition s05 := (perm S05_inj).
+ +
+Definition s14 : {perm cube}.
+ +
+Definition s23 := (perm (inv_inj S23_inv)).
+Definition r05 := (perm R05_inj).
+Definition r14 := (perm R14_inj).
+Definition r23 := (perm R23_inj).
+Definition r50 := (perm R50_inj).
+Definition r41 := (perm R41_inj).
+Definition r32 := (perm R32_inj).
+Definition r024 := (perm R024_inj).
+Definition r042 := (perm R042_inj).
+Definition r012 := (perm R012_inj).
+Definition r021 := (perm R021_inj).
+Definition r031 := (perm R031_inj).
+Definition r013 := (perm R013_inj).
+Definition r043 := (perm R043_inj).
+Definition r034 := (perm R034_inj).
+ +
+Definition s1 := (perm (inv_inj S1_inv)).
+Definition s2 := (perm (inv_inj S2_inv)).
+Definition s3 := (perm (inv_inj S3_inv)).
+Definition s4 := (perm (inv_inj S4_inv)).
+Definition s5 := (perm (inv_inj S5_inv)).
+Definition s6 := (perm (inv_inj S6_inv)).
+ +
+Definition dir_iso3 := [set p |
+[|| id3 == p, s05 == p, s14 == p, s23 == p, r05 == p, r14 == p, r23 == p,
+ r50 == p, r41 == p, r32 == p, r024 == p, r042 == p, r012 == p, r021 == p,
+ r031 == p, r013 == p, r043 == p, r034 == p,
+ s1 == p, s2 == p, s3 == p, s4 == p, s5 == p | s6 == p]].
+ +
+Definition dir_iso3l := [:: id3; s05; s14; s23; r05; r14; r23; r50; r41;
+ r32; r024; r042; r012; r021; r031; r013; r043; r034;
+ s1; s2; s3; s4; s5; s6].
+ +
+Definition S0 := [:: F5; F4; F3; F2; F1; F0].
+Definition S0f (sc : cube) : cube := tnth [tuple of S0] sc.
+ +
+Lemma S0_inv : involutive S0f.
+ +
+Definition s0 := (perm (inv_inj S0_inv)).
+ +
+Definition is_iso3 (p : {perm cube}) := ∀ fi, p (s0 fi) = s0 (p fi).
+ +
+Lemma dir_iso_iso3 : ∀ p, p \in dir_iso3 → is_iso3 p.
+ +
+Lemma iso3_ndir : ∀ p, p \in dir_iso3 → is_iso3 (s0 × p).
+ +
+Definition sop (p : {perm cube}) : seq cube := val (val (val p)).
+ +
+Lemma sop_inj : injective sop.
+ +
+Definition prod_tuple (t1 t2 : seq cube) :=
+ map (fun n : 'I_6 ⇒ nth F0 t2 n) t1.
+ +
+Lemma sop_spec : ∀ x (n0 : 'I_6), nth F0 (sop x) n0 = x n0.
+ +
+Lemma prod_t_correct : ∀ (x y : {perm cube}) (i : cube),
+ (x × y) i = nth F0 (prod_tuple (sop x) (sop y)) i.
+ +
+Lemma sop_morph : {morph sop : x y / x × y >-> prod_tuple x y}.
+ +
+Definition ecubes : seq cube := [:: F0; F1; F2; F3; F4; F5].
+ +
+Lemma ecubes_def : ecubes = enum (@predT cube).
+ +
+Definition seq_iso_L := [::
+ [:: F0; F1; F2; F3; F4; F5];
+ S05; S14; S23; R05; R14; R23; R50; R41; R32;
+ R024; R042; R012; R021; R031; R013; R043; R034;
+ S1; S2; S3; S4; S5; S6].
+ +
+Lemma seqs1 : ∀ f injf, sop (@perm _ f injf) = map f ecubes.
+ +
+Lemma Lcorrect : seq_iso_L == map sop [:: id3; s05; s14; s23; r05; r14; r23;
+ r50; r41; r32; r024; r042; r012; r021; r031; r013; r043; r034;
+ s1; s2; s3; s4; s5; s6].
+ +
+Lemma iso0_1 : dir_iso3 =i dir_iso3l.
+ +
+Lemma L_iso : ∀ p, (p \in dir_iso3) = (sop p \in seq_iso_L).
+ +
+Lemma stable : ∀ x y,
+ x \in dir_iso3 → y \in dir_iso3 → x × y \in dir_iso3.
+ +
+Lemma iso_eq_F0_F1 : ∀ r s : {perm cube}, r \in dir_iso3 →
+ s \in dir_iso3 → r F0 = s F0 → r F1 = s F1 → r = s.
+ +
+Lemma ndir_s0p : ∀ p, p \in dir_iso3 → s0 × p \notin dir_iso3.
+ +
+Definition indir_iso3l := map (mulg s0) dir_iso3l.
+ +
+Definition iso3l := dir_iso3l ++ indir_iso3l.
+ +
+Definition seq_iso3_L := map sop iso3l.
+ +
+Lemma eqperm : ∀ p1 p2 : {perm cube},
+ (p1 == p2) = all (fun s ⇒ p1 s == p2 s) ecubes.
+ +
+Lemma iso_eq_F0_F1_F2 : ∀ r s : {perm cube}, is_iso3 r →
+ is_iso3 s → r F0 = s F0 → r F1 = s F1 → r F2 = s F2 → r = s.
+ +
+Ltac iso_tac :=
+ let a := fresh "a" in apply/permP ⇒ a;
+ apply/eqP; rewrite !permM !permE; case: a; do 6?case.
+ +
+Ltac inv_tac :=
+ apply: esym (etrans _ (mul1g _)); apply: canRL (mulgK _) _; iso_tac.
+ +
+Lemma dir_s0p : ∀ p, (s0 × p) \in dir_iso3 → p \notin dir_iso3.
+ +
+Definition is_iso3b p := (p × s0 == s0 × p).
+Definition iso3 := [set p | is_iso3b p].
+ +
+Lemma is_iso3P : ∀ p, reflect (is_iso3 p) (p \in iso3).
+ +
+Lemma group_set_iso3 : group_set iso3.
+ +
+Canonical iso_group3 := Group group_set_iso3.
+ +
+Lemma group_set_diso3 : group_set dir_iso3.
+Canonical diso_group3 := Group group_set_diso3.
+ +
+Lemma gen_diso3 : dir_iso3 = <<[set r05; r14]>>.
+ +
+Notation col_cubes := {ffun cube → colors}.
+ +
+Definition act_g (sc : col_cubes) (p : {perm cube}) : col_cubes :=
+ [ffun z ⇒ sc (p^-1 z)].
+ +
+Lemma act_g_1 : ∀ k, act_g k 1 = k.
+ +
+Lemma act_g_morph : ∀ k x y, act_g k (x × y) = act_g (act_g k x) y.
+ +
+Definition to_g := TotalAction act_g_1 act_g_morph.
+ +
+Definition cube_coloring_number24 := #|orbit to_g diso_group3 @: setT|.
+ +
+Lemma Fid3 : 'Fix_to_g[1] = setT.
+ +
+Lemma card_Fid3 : #|'Fix_to_g[1]| = (n ^ 6)%N.
+ +
+Definition col0 (sc : col_cubes) : colors := sc F0.
+Definition col1 (sc : col_cubes) : colors := sc F1.
+Definition col2 (sc : col_cubes) : colors := sc F2.
+Definition col3 (sc : col_cubes) : colors := sc F3.
+Definition col4 (sc : col_cubes) : colors := sc F4.
+Definition col5 (sc : col_cubes) : colors := sc F5.
+ +
+Lemma eqperm_map2 : ∀ p1 p2 : col_cubes,
+ (p1 == p2) = all (fun s ⇒ p1 s == p2 s) [:: F0; F1; F2; F3; F4; F5].
+ +
+Notation infE := (sameP afix1P eqP).
+ +
+Lemma F_s05 :
+ 'Fix_to_g[s05] = [set x | (col1 x == col4 x) && (col2 x == col3 x)].
+ +
+Lemma F_s14 :
+ 'Fix_to_g[s14]= [set x | (col0 x == col5 x) && (col2 x == col3 x)].
+ +
+Lemma r05_inv : r05^-1 = r50.
+ +
+Lemma r50_inv : r50^-1 = r05.
+ +
+Lemma r14_inv : r14^-1 = r41.
+ +
+Lemma r41_inv : r41^-1 = r14.
+ +
+Lemma s23_inv : s23^-1 = s23.
+ +
+Lemma F_s23 :
+ 'Fix_to_g[s23] = [set x | (col0 x == col5 x) && (col1 x == col4 x)].
+ +
+Lemma F_r05 : 'Fix_to_g[r05]=
+ [set x | (col1 x == col2 x) && (col2 x == col3 x)
+ && (col3 x == col4 x)].
+ +
+Lemma F_r50 : 'Fix_to_g[r50]=
+ [set x | (col1 x == col2 x) && (col2 x == col3 x)
+ && (col3 x == col4 x)].
+ +
+Lemma F_r23 : 'Fix_to_g[r23] =
+ [set x | (col0 x == col1 x) && (col1 x == col4 x)
+ && (col4 x == col5 x)].
+ +
+Lemma F_r32 : 'Fix_to_g[r32] =
+ [set x | (col0 x == col1 x) && (col1 x == col4 x)
+ && (col4 x == col5 x)].
+ +
+Lemma F_r14 : 'Fix_to_g[r14] =
+ [set x | (col0 x == col2 x) && (col2 x == col3 x) && (col3 x == col5 x)].
+ +
+Lemma F_r41 : 'Fix_to_g[r41] =
+ [set x | (col0 x == col2 x) && (col2 x == col3 x) && (col3 x == col5 x)].
+ +
+Lemma F_r024 : 'Fix_to_g[r024] =
+ [set x | (col0 x == col4 x) && (col4 x == col2 x) && (col1 x == col3 x)
+ && (col3 x == col5 x) ].
+ +
+Lemma F_r042 : 'Fix_to_g[r042] =
+ [set x | (col0 x == col4 x) && (col4 x == col2 x) && (col1 x == col3 x)
+ && (col3 x == col5 x)].
+ +
+Lemma F_r012 : 'Fix_to_g[r012] =
+ [set x | (col0 x == col2 x) && (col2 x == col1 x) && (col3 x == col4 x)
+ && (col4 x == col5 x)].
+ +
+Lemma F_r021 : 'Fix_to_g[r021] =
+ [set x | (col0 x == col2 x) && (col2 x == col1 x) && (col3 x == col4 x)
+ && (col4 x == col5 x)].
+ +
+Lemma F_r031 : 'Fix_to_g[r031] =
+ [set x | (col0 x == col3 x) && (col3 x == col1 x) && (col2 x == col4 x)
+ && (col4 x == col5 x)].
+ +
+Lemma F_r013 : 'Fix_to_g[r013] =
+ [set x | (col0 x == col3 x) && (col3 x == col1 x) && (col2 x == col4 x)
+ && (col4 x == col5 x)].
+ +
+Lemma F_r043 : 'Fix_to_g[r043] =
+ [set x | (col0 x == col4 x) && (col4 x == col3 x) && (col1 x == col2 x)
+ && (col2 x == col5 x)].
+ +
+Lemma F_r034 : 'Fix_to_g[r034] =
+ [set x | (col0 x == col4 x) && (col4 x == col3 x) && (col1 x == col2 x)
+ && (col2 x == col5 x)].
+ +
+Lemma F_s1 : 'Fix_to_g[s1] =
+ [set x | (col0 x == col5 x) && (col1 x == col2 x) && (col3 x == col4 x)].
+ +
+Lemma F_s2 : 'Fix_to_g[s2] =
+ [set x | (col0 x == col5 x) && (col1 x == col3 x) && (col2 x == col4 x)].
+ +
+Lemma F_s3 : 'Fix_to_g[s3] =
+ [set x | (col0 x == col1 x) && (col2 x == col3 x) && (col4 x == col5 x)].
+ +
+Lemma F_s4 : 'Fix_to_g[s4] =
+ [set x | (col0 x == col4 x) && (col1 x == col5 x) && (col2 x == col3 x)].
+ +
+Lemma F_s5 : 'Fix_to_g[s5] =
+ [set x | (col0 x == col2 x) && (col1 x == col4 x) && (col3 x == col5 x)].
+ +
+Lemma F_s6 : 'Fix_to_g[s6] =
+ [set x | (col0 x == col3 x) && (col1 x == col4 x) && (col2 x == col5 x)].
+ +
+Lemma uniq4_uniq6 : ∀ x y z t : cube,
+ uniq [:: x; y; z; t] → ∃ u, ∃ v, uniq [:: x; y; z; t; u; v].
+ +
+Lemma card_n4 : ∀ x y z t : cube, uniq [:: x; y; z; t] →
+ #|[set p : col_cubes | (p x == p y) && (p z == p t)]| = (n ^ 4)%N.
+ +
+Lemma card_n3_3 : ∀ x y z t: cube, uniq [:: x; y; z; t] →
+ #|[set p : col_cubes | (p x == p y) && (p y == p z)&& (p z == p t)]|
+ = (n ^ 3)%N.
+ +
+Lemma card_n2_3 : ∀ x y z t u v: cube, uniq [:: x; y; z; t; u; v] →
+ #|[set p : col_cubes | (p x == p y) && (p y == p z)&& (p t == p u )
+ && (p u== p v)]| = (n ^ 2)%N.
+ +
+Lemma card_n3s : ∀ x y z t u v: cube, uniq [:: x; y; z; t; u; v] →
+ #|[set p : col_cubes | (p x == p y) && (p z == p t)&& (p u == p v )]|
+ = (n ^ 3)%N.
+ +
+Lemma burnside_app_iso3 :
+ (cube_coloring_number24 × 24 =
+ n ^ 6 + 6 × n ^ 3 + 3 × n ^ 4 + 8 × (n ^ 2) + 6 × n ^ 3)%N.
+ +
+End cube_colouring.
+ +
+End colouring.
+ +
+Corollary burnside_app_iso_3_3col: cube_coloring_number24 3 = 57.
+ +
+Corollary burnside_app_iso_2_4col: square_coloring_number8 4 = 55.
+ +
+