Fintype (alternatingGroup α)

Stream: mathlib4

[Jeremy Tan]

How do I synthesise the instance fta given these imports?

import Mathlib.Algebra.Group.ConjFinite
import Mathlib.GroupTheory.Perm.Fin
import Mathlib.GroupTheory.Subgroup.Simple
import Mathlib.Tactic.IntervalCases

open Equiv Equiv.Perm Subgroup Fintype

variable (α : Type _) [Fintype α] [DecidableEq α]

def alternatingGroup : Subgroup (Perm α) :=
  sign.ker deriving Fintype -- deriving Fintype doesn't work

instance fta : Fintype (alternatingGroup α) :=
  fintypePerm (α := α) -- ???

[Eric Wieser]

deriving doesn't make sense there, since that's not a type in the first place

[Eric Wieser]

The second instance should be docs4#Subtype.fintype

[Eric Wieser]

The missing instance you probably need to add yourself is DecidablePred (∈ alternatingGroup α)

[Eric Wieser]

I would guess lean 3 just unfolded for you

[Jeremy Tan]

Eric Wieser said:

The missing instance you probably need to add yourself is DecidablePred (∈ alternatingGroup α)

I'm not sure how that can be proved from the given variables

[Jeremy Tan]

It may in fact be false

[Jeremy Tan]

…wait, this seems to work

instance : DecidablePred fun x => x ∈ alternatingGroup α := MonoidHom.decidableMemKer sign

[Eric Wieser]

That's a pretty good indication that it's not false :)

[Eric Wieser]

fun x => x ∈ alternatingGroup α can be written slightly more concisely as (\. ∈ alternatingGroup α)

[Jeremy Tan]

!4#3371 is as far as I could get on the relevant file

[Jeremy Tan]

@Eric Wieser would like to see if you can solve the 4 remaining errors

[Jeremy Tan]

The last error is particularly laughable; none of decide, ring, linarith and aesop can close what simplifies to (-1) ^ 5 != 1!

[Johan Commelin]

What about norm_num?

[Johan Commelin]

What is the type of these numbers?

[Jeremy Tan]

mathlib3 closes the proof of (-1) ^ (Multiset.sum {4} + ↑Multiset.card {4}) ≠ 1 using decide @Johan Commelin

norm_num also doesn't work, but leaves the goal as ¬(-1) ^ 5 = 1 where the -1 is of type ℤˣ, the 5 is of type \N and the RHS 1 is of type (fun x => ℤˣ) g

[Johan Commelin]

Does ext; simp make some progress?

[Johan Commelin]

ext should turn this into a goal about ℤ as opposed to ℤˣ.

[Eric Wieser]

Are we missing docs#units.decidable_eq? docs4#instUnitsDecidableEq ?

[Eric Wieser]

Hmm, docs4#Units.instDecidableEqUnits exists (though I hate that it's no longer easy to guess instance names)

[Jeremy Tan]

ext doesn't work, it gives another error:

applyExtLemma only applies to equations, not
  (-1) ^ 5 = 1 → False

[Eric Wieser]

Right, ext doesn't work on ne

[Eric Wieser]

does rw [ne.def] allow decide to work?

[Eric Wieser]

Does decide give any diagnostics when it fails?

[Jeremy Tan]

the original decide gives the error message

expected type must not contain free or meta variables
  (-1) ^ (Multiset.sum {4} + ↑Multiset.card {4}) ≠ 1

[Yakov Pechersky]

Jeremy Tan said:

ext doesn't work, it gives another error:

applyExtLemma only applies to equations, not
  (-1) ^ 5 = 1 → False

One can always use an explicit ext lemma like Subtype.ext_iff or Units.ext_iff

[Eric Wieser]

The decide works if you put a dsimp only before it. This looks like a bug in decide.

[Eric Wieser]

ext only works on = not ≠

[Matthew Ballard]

simp only [Set.singleton_subset_iff, SetLike.mem_coe, ne_eq, mk_eq_one_iff] also works

[Yakov Pechersky]

Right. I meant my message as an interpretation of Johan's message

[Yakov Pechersky]

simp [Something.ext_iff]

[Jeremy Tan]

Right, I pushed the dsimp only fix

[Eric Wieser]

Matthew Ballard said:

simp only [Set.singleton_subset_iff, SetLike.mem_coe, ne_eq, mk_eq_one_iff] also works

So does simp only because that uses decide under the hood, so here simp only is essentially the same as dsimp only; decide

[Jeremy Tan]

I tested simp only on Lean 4 Web, it doesn't work

[Eric Wieser]

It worked for me in your PR branch

[Eric Wieser]

Though there's an error higher up the same proof that might be causing trouble

[Jeremy Tan]

I actually don't know how to fill in the underscores here, which is the last remaining non-timeout error in the alternating group file
have h := SetLike.mem_coe.1 (@subset_normalClosure _ _ >_< _ (Set.mem_singleton _))

[Jeremy Tan]

It needs a Group but I don't know which Group is the right one

[Eric Wieser]

Looking at the type of h in Lean 3 might help

[Jeremy Tan]

h's type is h : ?m_3 ∈ normal_closure {?m_3}, which I feel is totally unrelated to the existing term

[Notification Bot]

A message was moved here from #mathlib4 > lake exe cache get by Jeremy Tan.