select

Stream: new members

[vxctyxeha]

hi everyone my problem is find all element of oder 4 in s4,the key point is that forall，and I already know how to list all the elements of S4.Is the code below correct?

import Mathlib
open Equiv Equiv.Perm Finset

theorem S4_ele:
    ({ c[0,1,2,3], c[0,1,3,2], c[0,2,1,3], c[0,2,3,1], c[0,3,2,1], c[0,3,1,2] } : Finset (Perm (Fin 4))) =
    ((univ : Finset (Perm (Fin 4))).filter (fun σ => orderOf σ = 4)) := by

[Aaron Liu]

I believe it is provable, and it seems correct.

[vxctyxeha]

Can the code below prove all the elements of s4?

import Mathlib

open Equiv
open Perm
theorem if_element_is_in_explicit_list_then_it_is_in_S4 (x : Perm (Fin 4)) :
  x ∈ ({

    (1 : Perm (Fin 4)),


    c[(0 : Fin 4), 1], c[(0 : Fin 4), 2], c[(0 : Fin 4), 3],
    c[(1 : Fin 4), 2], c[(1 : Fin 4), 3],
    c[(2 : Fin 4), 3],


    c[(0 : Fin 4), 1, 2], c[(0 : Fin 4), 2, 1],
    c[(0 : Fin 4), 1, 3], c[(0 : Fin 4), 3, 1],
    c[(0 : Fin 4), 2, 3], c[(0 : Fin 4), 3, 2],
    c[(1 : Fin 4), 2, 3], c[(1 : Fin 4), 3, 2],

    -- 4-轮换 (6个)
    c[(0 : Fin 4), 1, 2, 3], c[(0 : Fin 4), 1, 3, 2],
    c[(0 : Fin 4), 2, 1, 3], c[(0 : Fin 4), 2, 3, 1],
    c[(0 : Fin 4), 3, 1, 2], c[(0 : Fin 4), 3, 2, 1],

    (c[(0 : Fin 4), 1] * c[(2 : Fin 4), 3]),
    (c[(0 : Fin 4), 2] * c[(1 : Fin 4), 3]),
    (c[(0 : Fin 4), 3] * c[(1 : Fin 4), 2])
  } : Finset (Perm (Fin 4))) → x ∈ (Finset.univ : Finset (Perm (Fin 4))) := by

  intro h_mem_explicit_list

  exact Finset.mem_univ x

[vxctyxeha]

@Aaron Liu

[Kenny Lau]

@vxctyxeha not sure if it proves anything, since everything is in the univ set by definition

[Kenny Lau]

@vxctyxeha this proves it in about 5 seconds

import Mathlib
open Equiv Equiv.Perm Finset

set_option profiler true
theorem S4_ele:
    ({ c[0,1,2,3], c[0,1,3,2], c[0,2,1,3], c[0,2,3,1], c[0,3,2,1], c[0,3,1,2] } : Finset (Perm (Fin 4))) =
    ((univ : Finset (Perm (Fin 4))).filter (fun σ => orderOf σ = 4)) := by
  ext x; constructor
  · revert x; simp [orderOf_eq_iff]; refine ⟨?_, ?_, ?_, ?_, ?_, ?_⟩ <;> decide
  · simp [orderOf_eq_iff]; fin_cases x <;> decide