How many elements of order two does S_4 have

Stream: Is there code for X?

[Ruben Van de Velde]

Working through a textbook from my younger days, I came across this exercise... I wonder if lean could be made to brute-force it

import group_theory.perm.cycle.concrete

example : nat.card { x : equiv.perm (fin 4) // order_of x = 2 } = 9 :=
begin
  sorry
end

[Floris van Doorn]

This gives you the answer, at least when using #eval:

import group_theory.perm.cycle.concrete

open function

variables {α : Type*} [fintype α] [decidable_eq α] [group α]

lemma exists_order (x : α) : x ∈ periodic_pts ((* x)) :=
sorry

def computable_order (x : α) : ℕ :=
nat.find (exists_order x)

#eval fintype.card { x : equiv.perm (fin 4) // computable_order x = 2 } -- 9

Note that #eval happily computes even though I've sorry'd one lemma. There is still some work to be done to turn this into what you asked...

[Yury G. Kudryashov]

AFAIR, Lean 4 has a way to associate a "computationally better implementation" with a function. Can it work with extra decidability assumptions? Or should we have definitions like decidable.order_of and a special simp set that consists of lemmas like order_of x = decidable.order_of x?

[Yury G. Kudryashov]

Then a tactic can simplify using these formulas & eval. However, it doesn't work for order_of hidden deep inside of another noncomputable definition.

[Yaël Dillies]

From what I understand of Kyle's arguments, the Lean 4 system means we will drop decidability entirely. This means all constructions will be noncomputable according to the Lean 3 definition of computing.

[Kyle Miller]

@Yury G. Kudryashov As I understand it, while in Lean 4 you can associate a computationally better implementation, you cannot have it depend on additional decidability assumptions. It has to be a replacement with the exact same type.

What Yael is referring to is that I've been wanting to see a computable class that you can use to associate computations to specific terms given specific additional typeclasses (and, for example, associating a computation to a normally noncomputable term). Then we can be more free to prefer noncomputable definitions in mathlib. In principle, the compiler could use instances of this class when compiling, though I haven't heard of anyone looking into this possibility yet.

I'm not sure there is anything Lean 3 vs Lean 4 about this, other than perhaps Lean 4 noncomputability detection is more reliable.

[Yury G. Kudryashov]

Can the computationally better implementation be unsafe? If yes, then it can try to generate the missing decidability arguments (though I'm not sure if it has access to the environment). OTOH, with this approach we don't have a proof of the fact that the computationally better implementation returns the same result.