Decidability of `is_unit` on finite rings

Stream: Is there code for X?

[Michael Stoll]

The following works:

import data.zmod.basic

example : ∀ (a : zmod 8), a.val % 2 = 1 → a ^ 2 = 1 := dec_trivial

but this does not:

import data.zmod.basic

example : ∀ (a : zmod 8), is_unit a → a ^ 2 = 1 := dec_trivial

==>

failed to synthesize type class instance for
⊢ decidable (∀ (a : zmod 8), is_unit a → a ^ 2 = 1)

Shouldn't there be a decidability instance catching basically any predicate on a finite structure like zmod 8?

[Eric Wieser]

Does it work for fin 8?

[Michael Stoll]

Eric Wieser said:

Does it work for fin 8?

No, it gives the same error.

[Michael Stoll]

The following does work:

import data.zmod.basic

example (a : zmod 8) (ha : is_unit a) : a ^ 2 = 1 :=
begin
  have h₁ : ∀ (x : (zmod 8)ˣ), (x : zmod 8).val % 2 = 1 := dec_trivial,
  have h₂ : ∀ (a : zmod 8), a.val % 2 = 1 → a ^ 2 = 1 := dec_trivial,
  exact h₂ a (h₁ ha.unit),
end

I'm a bit confused now...

[Reid Barton]

one way

import data.zmod.basic

example : ∀ (a : zmod 8), is_unit a → a ^ 2 = 1 :=
by { unfold is_unit, exact dec_trivial }

[Reid Barton]

Probably a better way would be to write an instance for decidable (is_unit x) on a finite type, but where to put it?

[Michael Stoll]

What I actually need is

import number_theory.legendre_symbol.zmod_char

open zmod

example (a : zmod 8) (ha : ¬ is_unit a) : χ₈ a = 0 := sorry

for which your suggestion to use unfold is_unit does not seem to work.

[Michael Stoll]

It does with dec_trivial!, though.

[Michael Stoll]

example (a : zmod 8) (ha : ¬ is_unit a) : χ₈ a = 0 :=
begin
  unfold is_unit at ha,
  dec_trivial!,
end

[Reid Barton]

Off-topic fun fact: did you know that zmod_char is a substring of category_theory.limits.multiequalizer.category_theory.limits.multicospan_index.snd_pi_map.category_theory.limits.has_equalizer?

[Michael Stoll]

The search window is always good for surprises...

[Michael Stoll]

Reid Barton said:

Probably a better way would be to write an instance for decidable (is_unit x) on a finite type, but where to put it?

In algebra.group.units near the definition of is_unit?

[Adam Topaz]

(deleted)

[Michael Stoll]

I'm trying to write this decidability instance for is_unit. But I'm running into the problem that I cannot get [fintype Mˣ] from [monoid M] [fintype M] automatically. Is this a gap in mathlib?

[Reid Barton]

You will also need decidable_eq M

[Adam Topaz]

It works with that

import data.fintype.basic
import algebra.group.units

variables (M : Type*) [fintype M] [decidable_eq M] [monoid M]
example : fintype Mˣ := infer_instance

[Michael Stoll]

OK, so

import algebra.group.units
import data.fintype.basic

instance {M : Type*} [monoid M] [fintype M] [decidable_eq M] (x : M) : decidable (is_unit x) :=
begin
  unfold is_unit,
  apply fintype.decidable_exists_fintype,
end

In which file should this go? algebra.group.units does not know about fintypes.
But data.fintype.basic knows about units, so perhaps this would be a good location.

[Michael Stoll]

Perhaps near docs#fintype.card_units ?

[Eric Wieser]

.

[Eric Wieser]

It might be worth changing that to

instance {M : Type*} [monoid M] : Π [decidable (∃ u : Mˣ, ↑u = m)], decidable (is_unit x) :=
id

Which both applies more generally, and can go in an earlier file.

[Violeta Hernández]

Reid Barton said:

Off-topic fun fact: did you know that zmod_char is a substring of category_theory.limits.multiequalizer.category_theory.limits.multicospan_index.snd_pi_map.category_theory.limits.has_equalizer?

So is zero_le_three :P

[Violeta Hernández]

Someone really needs to rename those instances

[Kevin Buzzard]

I think the long names are funny but it's not clear to me that they need to be renamed. Bytes are cheap and the names are descriptive.

[Yaël Dillies]

I don't think of putting category_theory three times in the name as very descriptive, Kevin.

[Yaël Dillies]

The problem is that autogenerated names apply the namespace to every atom rather than just once at the end. I guess this is a conservative behavior to avoid mixing up different namespaces, but empirically most declarations use stuff from a single namespace, and people think of namespaces as, well... spaces, not as a step you keep jumping on and off from.

[Kevin Buzzard]

I see, you're right in that it can be trimmed a bit ;-)

[Eric Rodriguez]

Kevin Buzzard said:

I think the long names are funny but it's not clear to me that they need to be renamed. Bytes are cheap and the names are descriptive.

At some point we're also going to run into names >100 chars long, making them unusable because of the liner. I think the cosine rule is close already

[Alex J. Best]

We can also teach the linter to ignore lines with <= 2 spaces in or something like that, it already ignores lines containing a http.

[Reid Barton]

Names of instances don't really matter, it's just funny when they pop up in the documentation search for totally unrelated things.

[Michael Stoll]

Eric Wieser said:

It might be worth changing that to

instance {M : Type*} [monoid M] : Π [decidable (∃ u : Mˣ, ↑u = m)], decidable (is_unit x) :=
id

Which both applies more generally, and can go in an earlier file.

I have now added this in algebra.group.units: #14873. @Eric Wieser

[Michael Stoll]

#14873 is now green. Would it make sense to label this as easy?

[Violeta Hernández]

Reid Barton said:

Names of instances don't really matter, it's just funny when they pop up in the documentation search for totally unrelated things.

They do matter at times, particularly when you want to use said instances to define other instances

[Michael Stoll]

@Eric Wieser Can #14873 be merged now, or is there more to be done?

[Michael Stoll]

@Eric Wieser Can you push this onto the merge queue?

[Eric Wieser]

I'll let @Yury G. Kudryashov make the call; it looks fine to me