calculation

Stream: new members

[vxctyxeha]

I tried to make it computable, but when I use native_decide, it slows down as the data increases. Are there any acceleration methods?

import Mathlib
open Equiv Classical Nat

-- Add compiler options for faster computation
set_option maxHeartbeats 400000
set_option maxRecDepth 10000


/-- The number of elements of order 30 in the symmetric group S_10 is 120960. -/
theorem order_30_elements_S10 : Finset.card {σ : Perm (Fin 10) | orderOf σ = 30} = 120960 := by
  -- We first show that the set of permutations of order 30 is equal to the set of permutations σ such that σ^30 = 1 and for all k < 30, σ^k ≠ 1.
  have eq : ({σ : Perm (Fin 10) | orderOf σ = 30} : Finset (Perm (Fin 10)))
      = ({σ : Perm (Fin 10) | σ ^ 30 = 1 ∧ ∀ k < 30, k ≠ 0 → σ ^ k ≠ 1} : Finset (Perm (Fin 10))) := by
    ext g
    simp only [Finset.mem_filter, Finset.mem_univ, true_and, ne_eq]
    constructor
    · intro hg
      constructor
      · rw [← hg]
        exact pow_orderOf_eq_one g
      · intro k hk hk_ne_zero
        refine pow_ne_one_of_lt_orderOf hk_ne_zero ?_
        rw [hg]
        exact hk
    · intro hg
      refine (orderOf_eq_iff ?_).mpr ?_
      exact Nat.zero_lt_succ 29
      constructor
      · exact hg.1
      intro m hm_pos hm_lt_30
      -- hm_pos is 0 < m, hm_lt_30 is m < 30
      have hm_ne_zero : m ≠ 0 := Nat.pos_iff_ne_zero.mp hm_lt_30
      exact hg.2 m hm_pos hm_ne_zero
  rw [eq]
  -- Use decide with optimizations for faster computation
  native_decide

[Aaron Liu]

Do you have an easier proof? Checking everything is computationally expensive.

[vxctyxeha]

Then I can only discuss it in categories.

[vxctyxeha]

By the way, native_decide can only be applied to small data, so smaller proofs can be transformed into computable ones.

[Aaron Liu]

vxctyxeha said:

Then I can only discuss it in categories.

explain?

[vxctyxeha]

Aaron Liu said:

vxctyxeha said:

Then I can only discuss it in categories.

The order of a product of disjoint cycles of lengths i,j is equal to the lcm(i,j).

explain?