Zulip Chat Archive

Stream: mathlib4

Topic: How to make InferInstance ignore my new instance

Bolton Bailey (Jul 17 2023 at 18:59):

I was told to add the instance
noncomputable instance [Monoid α] [Fintype α] : Fintype αˣ := Fintype.ofFinite αˣ
to Data.Fintype.Units for #5738. But now I am getting errors in other files: In Algebra.Group.ConjFinite I get

IR check failed at 'instDecidableRelIsConj._rarg', error: unknown declaration 'instFintypeUnits_1'

At

instance [DecidableEq α] [Fintype α] : DecidableRel (IsConj : α → α → Prop) := fun a b =>
  inferInstanceAs (Decidable (∃ c : αˣ, c.1 * a = b * c.1))

How do I fix this?

Matthew Ballard (Jul 17 2023 at 19:12):

It is picking up on your new instance and, since it is non-computable, it cannot generate code for it. One fix is to mark it noncomputable also. That seems strange for a Decidable instance. Another is to use attribute [-instance] to remove from the tree beforehand.

In general, a noncomputable instance that creates data (Fintype) seems like something you want to be careful with

Notification Bot (Jul 17 2023 at 19:20):

This topic was moved here from #lean4 > How to make InferInstance ignore my new instance by Floris van Doorn.

Eric Wieser (Jul 17 2023 at 19:21):

That sounds like a bad instance to me

Floris van Doorn (Jul 17 2023 at 19:21):

I think you should make your new instance computable. Presumably you can make it computable if you add DecidableEq \a?

Matthew Ballard (Jul 17 2023 at 19:23):

There is something like instance [Fintype B] (f : A -> B) (h : Injective f) : Fintype A right?

Floris van Doorn (Jul 17 2023 at 19:24):

yes: docs#Fintype.ofInjective

Matthew Ballard (Jul 17 2023 at 19:24):

That would better to use for the new instance

Floris van Doorn (Jul 17 2023 at 19:24):

but it's also noncomputable

Matthew Ballard (Jul 17 2023 at 19:25):

Oh!

Eric Wieser (Jul 17 2023 at 19:27):

I'm surprised this instance doesn't already exist

Matthew Ballard (Jul 17 2023 at 19:32):

There seems to be a few ways to make this computable.

Eric Wieser (Jul 17 2023 at 19:33):

all of them are just the O(N²) enumerate and filter, right?

Matthew Ballard (Jul 17 2023 at 19:34):

That was one. The other had that implicitly in there where you give an equivalence between Units and a subtype

Eric Wieser (Jul 17 2023 at 19:36):

I think that's the one you want

Eric Wieser (Jul 17 2023 at 19:36):

Via the equivalence

Eric Wieser (Jul 17 2023 at 19:38):

docs#Units.embedProduct is most of the way there

Kyle Miller (Jul 17 2023 at 19:38):

Here's the general rule (modulo exceptions due to some development halting due to the port):

  • All global Fintype instances should be computable
  • If you can't make a computable Fintype instance, then make a global Finite instance
  • When you need a Fintype instance for a classical proof, use Fintype.ofFinite locally

Since we're in the world of Lean 4, you should be able to do local attribute [instance] Fintype.ofFinite without anything bad happening (except for sometimes needing to use convert in proofs). We couldn't do this in Lean 3 due to this introducing cycles.

Eric Wieser (Jul 17 2023 at 19:39):

@Kyle Miller, does your fintype derive handler work on units?

Kyle Miller (Jul 17 2023 at 19:42):

It might work, though you might need to do it semi-manually with the fintype term elaborator with an additional DecidableEq argument

Kyle Miller (Jul 17 2023 at 19:45):

Yeah, semi-manually is needed:

instance [Fintype α] [DecidableEq α] [Monoid α] : Fintype αˣ :=
  derive_fintype% _

Kyle Miller (Jul 17 2023 at 19:50):

You might need this extra import: import Mathlib.Tactic.DeriveFintype

Matthew Ballard (Jul 17 2023 at 19:58):

Is there no instance [Fintype A] : DecidableEq A?

Eric Wieser (Jul 17 2023 at 20:00):

No, that's not computably true

Eric Wieser (Jul 17 2023 at 20:01):

This has been discussed before, and usually amounts to "what some people call constructively finite, mathlib calls Fintype + DecidableEq"

Matthew Ballard (Jul 17 2023 at 20:01):

Ah ok

Bolton Bailey (Jul 19 2023 at 00:00):

Yeah instance [Monoid α] [Fintype α] [DecidableEq α] : Fintype αˣ := Fintype.ofEquiv _ (unitsEquivProdSubtype α).symm already exists. I guess there is a typeclass called Finite, is this just exactly equivalent to Fintype + DecidableEq? Maybe that's the instance which is needed/the way the lemma I need should be written?

Eric Wieser (Jul 19 2023 at 00:10):

No, docs#Finite is something quite different

Eric Wieser (Jul 19 2023 at 00:11):

Fintype is "you can ask me to compute the list of entries but you can't compare against them", Finite is "I'm not going to compute anything", DecidableEq is "If you have a list you can compare against it".

Bolton Bailey (Jul 19 2023 at 00:15):

I see we have docs#Fintype.ofFinite (apparently noncomputable) and docs#Finite.of_fintype (apparently computable)

Eric Wieser (Jul 19 2023 at 00:16):

It is very deliberate that the first one is not an instance (and not just to avoid loops)

Eric Wieser (Jul 19 2023 at 00:17):

Yeah instance [Monoid α] [Fintype α] [DecidableEq α] : Fintype αˣ := Fintype.ofEquiv _ (unitsEquivProdSubtype α).symm already exists.

Where?

Bolton Bailey (Jul 19 2023 at 00:18):

Uh, immediately above my PR, I think

Eric Wieser (Jul 19 2023 at 00:18):

docs#instFintypeUnits

Bolton Bailey (Jul 19 2023 at 00:19):

Yep, that's it

Eric Wieser (Jul 19 2023 at 00:21):

It looks like @Oliver Nash gave some slightly misleading advice and then we tricked ourselves into running in circles over nothing :sweat_smile:

Eric Wieser (Jul 19 2023 at 00:21):

The instances in the PR look fine

Bolton Bailey (Jul 19 2023 at 00:22):

Well, it seems his main advice was "use Nat.card" which maybe would avoid this entirely.

Eric Wieser (Jul 19 2023 at 00:31):

We should have lemmas about both

Last updated: Dec 20 2023 at 11:08 UTC