instance and show_term

Stream: new members

[Alex Zhang]

show_term suggests Try this: exact (f F).ker.fintype, but this is incorrect when changing it to this. What should be the correct term inferred?

import field_theory.finite.basic

variables (F : Type*) [field F] [fintype F] [decidable_eq F] {p : ℕ} [char_p F p]
open finset fintype monoid_hom

def f : (units F) →* (units F) :=
⟨λ a, a * a, by simp, (λ x y, by simp [units.ext_iff]; ring)⟩

noncomputable
instance : fintype ((f F).ker) := by show_term {apply_instance}

[Kevin Buzzard]

It works fine for me.

[Kevin Buzzard]

What error are you getting?

[Alex Zhang]

It works for me too now!

[Alex Zhang]

How can I construct the last instance, do I need more assumptions?

import field_theory.finite.basic

variables (F : Type*) [field F] [fintype F] [decidable_eq F] {p : ℕ} [char_p F p]
open finset fintype monoid_hom

def f : (units F) →* (units F) :=
⟨λ a, a * a, by simp, (λ x y, by simp [units.ext_iff]; ring)⟩

instance in_ker_dec (x : units F):
decidable (x ∈ (f F).ker) := (f F).decidable_mem_ker x

instance in_ker_carrier_dec (x : units F):
decidable (x ∈ (f F).ker.carrier) := sorry

[Adam Topaz]

import field_theory.finite.basic

variables (F : Type*) [field F] [fintype F] [decidable_eq F] {p : ℕ} [char_p F p]
open finset fintype monoid_hom

def f : (units F) →* (units F) :=
⟨λ a, a * a, by simp, (λ x y, by simp [units.ext_iff]; ring)⟩

instance in_ker_dec (x : units F):
decidable (x ∈ (f F).ker) := (f F).decidable_mem_ker x

instance in_ker_carrier_dec (x : units F):
decidable (x ∈ (f F).ker.carrier) :=
begin
  change decidable ((f F) x = 1),
  apply_instance,
end

[Adam Topaz]

But this breaks the API, so we should try to find a better way

[Adam Topaz]

e.g.

import field_theory.finite.basic

variables (F : Type*) [field F] [fintype F] [decidable_eq F] {p : ℕ} [char_p F p]
open finset fintype monoid_hom

def f : (units F) →* (units F) :=
⟨λ a, a * a, by simp, (λ x y, by simp [units.ext_iff]; ring)⟩

instance in_ker_dec (x : units F):
decidable (x ∈ (f F).ker) := (f F).decidable_mem_ker x

instance in_ker_carrier_dec (x : units F):
decidable (x ∈ (f F).ker.carrier) := in_ker_dec _ _

[Adam Topaz]

I'm not sure why you need both in_ker_dec and in_ker_carrier_dec. In practice you will never write x ∈ (f F).ker.carrier, but rather you should always use x ∈ (f F).ker

[Alex Zhang]

as I need to prove something about card, the story is complicated..
Thanks for your solution!

[Alex Zhang]

Could you explain why the first one breaks API?

[Adam Topaz]

well, because to use change I had to know the definitions. It's usually better to use the API we have, and if something is missing from the API, to add it.

[Alex Zhang]

or just

instance in_ker_carrier_dec (x : units F):
decidable (x ∈ (f F).ker.carrier) :=
(f F).decidable_mem_ker x

[Yakov Pechersky]

docs#monoid_hom.decidable_mem_ker

[Yakov Pechersky]

You shouldn't need to add specialized instances in your file because this is already an instance on decidable_eq F

[Yakov Pechersky]

That's all you should need to declare. Or just open_locale classical, since you said you don't care about computation.

[Adam Topaz]

I guess we're missing a decidable_eq (units F) given [decidable_eq F]

[Yakov Pechersky]

import tactic
import data.fintype.card
import data.finset.basic
import field_theory.finite.basic
import group_theory.quotient_group

example {G : Type*} [monoid G] [decidable_eq G] : decidable_eq (units G) :=
by apply_instance

works for me, so we're not missing it

[Adam Topaz]

Right, so this works

import field_theory.finite.basic

variables (F : Type*) [field F] [fintype F] [decidable_eq F] {p : ℕ} [char_p F p]
open finset fintype monoid_hom

def f : (units F) →* (units F) :=
⟨λ a, a * a, by simp, (λ x y, by simp [units.ext_iff]; ring)⟩

example (x : units F) : decidable (x ∈ (f F).ker) := by apply_instance

[Yakov Pechersky]

What's likely going on it that Alex is trying to make a lemma relating cardinality of that subgroup (when coerced to a Sort). And those lemmas can't be stated unless the membership of the kernel is decidable. He likely was trying to figure out a way to state instance ... to get the lemma statements to be correct. And the correct approach is avoiding defining any new or specialized instances, but rather just stating that [decidable_eq F].

[Yakov Pechersky]

Which is a stronger claim than [decidable (x ∈ (f F).ker)] but is more idiomatic.