instances don't apply to instance-defeq types

Stream: lean4

[Junyan Xu]

Update: see #lean4 > instances don't apply to instance-defeq types @ 💬 for mathlib-free code sample that shows the actual problem.

---

Original message:

Why does the second example fail, given that HasQuotient.Quotient is an abbrev?

import Mathlib.Algebra.Quotient

variable (A : Type*)
instance : HasQuotient Unit A := ⟨fun _ ↦ A⟩

example (a : A) : (Unit ⧸ a) = A := rfl -- succeeds
example (a : A) : (Unit ⧸ a) = A := by with_reducible rfl
/- tactic 'rfl' failed, the left-hand side
  Unit ⧸ a
is not definitionally equal to the right-hand side
  A -/

On the other hand,

instance : Zero Unit := ⟨()⟩
example : (Zero.zero : Unit) = () := by with_reducible rfl -- succeeds

works.

[Markus Himmel]

I think the second example only works because in Unit all equalities are definitional.

instance : Zero Bool := ⟨false⟩
example : (Zero.zero : Bool) = false := by with_reducible rfl -- fails

[Junyan Xu]

Hmm, that's unexpected. Looks like structure (inductive type with a single constructor) eta is doing too much? Even this works:

example : () = Classical.arbitrary Unit := by with_reducible rfl

[Junyan Xu]

It still doesn't work even if I add attributes [reducible, inline] to the projection:

class Foo (α : Type) : Type where
  foo : α

instance : Foo Bool := ⟨false⟩
example : (Foo.foo : Bool) = false := rfl -- succeeds
example : (Foo.foo : Bool) = false := by with_reducible rfl -- fails

attribute [reducible, inline] Foo.foo
example : (Foo.foo : Bool) = false := by with_reducible rfl -- fails

[Matthew Ballard]

Why aren't you using with_reducible_and_instances?

[Junyan Xu]

Indeed that works, thanks! I might have seen it before but had forgotten it exists.

[Junyan Xu]

Now to the actual problem: why does the last #synth fail?

import Mathlib.GroupTheory.QuotientGroup.Defs
import Mathlib.Algebra.Module.Submodule.Defs

variable {R M : Type*} [Ring R] [AddCommGroup M] [Module R M] (p : Submodule R M)

instance : HasQuotient M (Submodule R M) := ⟨fun p ↦ M ⧸ p.toAddSubgroup⟩

example : (M ⧸ p) = (M ⧸ p.toAddSubgroup) := by with_reducible_and_instances rfl
--succeeds

#synth AddCommGroup (M ⧸ p.toAddSubgroup) -- QuotientAddGroup.Quotient.addCommGroup p.toAddSubgroup
#synth AddCommGroup (M ⧸ p) -- fails

[Edward van de Meent]

answer: you're missing import Mathlib.LinearAlgebra.Quotient.Defs

[Junyan Xu]

I'm trying to make the two reducibly defeq in #21384, but the instances don't transfer.

[Edward van de Meent]

presumably, that's because toAddSubgroup is not instance-reducable?

[Edward van de Meent]

(actually i should read the code example)

[Matthew Ballard]

I am guessing you have a key problem

[Matthew Ballard]

I am not really reading the example either ;)

[Junyan Xu]

Actually this minimized mathlib-free example also show the same issue:

class HasQuotient (A B : Type) : Type 1 where
  q : B → Type

open HasQuotient (q)

variable (A B : Type)

instance [HasQuotient A B] : HasQuotient A (B × B) := ⟨fun b ↦ q A b.1⟩

variable [HasQuotient A Unit]

instance (b : Unit) : Add (q A b) := ⟨fun _ ↦ id⟩

variable (b : Unit × Unit)

example : (q A b) = (q A b.1) := by with_reducible_and_instances rfl

#synth Add (q A b.1) -- succeeds
#synth Add (q A b) -- fails
instance : Add (q A b) := inferInstanceAs (Add (q A b.1)) -- succeeds

[Edward van de Meent]

HasQuotient.Quotient not reducible?

[Matthew Ballard]

Take a look at the output of #discr_tree_key

[Junyan Xu]

Edward van de Meent said:

HasQuotient.Quotient not reducible?

It's an abbrev, I said in first message.

[Junyan Xu]

Matthew Ballard said:

Take a look at the output of #discr_tree_key

Where I do I put it?

[Matthew Ballard]

Plug in the name of the decl. (Sorry limited atm)

[Junyan Xu]

#discr_tree_key HasQuotient.Quotient says <other>. Same for HasQuotient.quotient' and my handrolled HasQuotient.q. There aren't other named decls in my code sample.

[Junyan Xu]

#discr_tree_key Zero (or Add) says <other> too. #discr_tree_key Add.add (or Zero.zero) says _.

[Matthew Ballard]

#discr_tree_key instAddQuotientUnit #discr_tree_key instAddQuotientProdUnit

[Matthew Ballard]

Or whatever the instances are now named

[Junyan Xu]

In the mathlib-y code sample (now replaced by mathlib-free code), #discr_tree_key instAddQuotientUnit says Add (@HasQuotient.quotient' _ PUnit.{u} _ _)

[Junyan Xu]

#discr_tree_key instAddQuotientProdUnit says Add (@HasQuotient.quotient' _ (Prod PUnit.{u} PUnit.{u}) _ _)

[Matthew Ballard]

What is your anonymous named now?

[Junyan Xu]

See below

#discr_tree_key instAddQUnit
#discr_tree_key instAddQProdUnit

says

Add (q _ PUnit _ _)
Add (q _ (Prod PUnit PUnit) _ _)

[Notification Bot]

12 messages were moved from this topic to #lean4 > instances don't apply to instance-defeq types by Johan Commelin.

[Junyan Xu]

@Johan Commelin
Can you please move everything here to #lean4 > instances don't apply to instance-defeq types @ 💬 ? (hopefully messages will still be ordered by time)

[Johan Commelin]

You mean the entire thread? Maybe just edit your first message in the new thread with a pointer back to this one.

[Notification Bot]

29 messages were moved here from #mathlib4 > Quotients are not reducibly defeq to their definitions by Johan Commelin.

[Jovan Gerbscheid]

You can use set_option trace.Meta.synthInstance true to see for yourself what is going on during type class search.

During typeclass search, Lean first chooses the available instances from the discrimination tree. In this step it only unfolds reducible constants (and not instance projections such as q or ⧸. In the next step it does unification in the with_reducible_and_instances setting. So in your example, the discrimination tree doesn't find the instance that you want it to find.

[Junyan Xu]

Do you think anything should be done about this? Is it likely to be causing any performance issue in Mathlib? It's certainly annoying that instances don't transfer even when one type is defined (reducibly defeq'ly) in terms of another type.
cc @Matthew Ballard

[Jovan Gerbscheid]

I think it is working exactly as intended. HasQuotient.quotient' is not a reducible constant, so it doesn't get unfolded :)

[Junyan Xu]

That's a good hint! I made HasQuotient.q reducible and now the instance automatically applies, but somehow I still need with_reducible_and_instances rfl and with_reducible rfl doesn't suffice. I'll test the effect on mathlib of adding this attribute to HasQuotient.quotient' and SetLike.coe. (If I set the attribute outside of the file HasQuotient/SetLike is defined, I get some warning and it's not sure what should be done.)

class HasQuotient (A B : Type) : Type 1 where
  q : B → Type

attribute [reducible] HasQuotient.q

open HasQuotient (q)

variable (A B : Type)

instance [HasQuotient A B] : HasQuotient A (B × B) := ⟨fun b ↦ q A b.1⟩

variable [HasQuotient A Unit]

instance (b : Unit) : Add (q A b) := ⟨fun _ ↦ id⟩

variable (b : Unit × Unit)

example : q A b = q A b.1 := by with_reducible_and_instances rfl -- succeeds
example : q A b = q A b.1 := by with_reducible rfl -- fails

#synth Add (q A b.1) -- succeeds
#synth Add (q A b) -- now succeeds

[Jovan Gerbscheid]

Note that for the failing with_reducible rfl to succeed, you have to write

@[reducible]
instance [HasQuotient A B] : HasQuotient A (B × B) := ⟨fun b ↦ q A b.1⟩

It surprises me that only the with_reducible rfl needs this. It seems that the unification and the discrimination tree indexing use a different configuration for how aggressively to unfold projections.

[Junyan Xu]

Thanks! I'm hitting build errors in my experiments #21495 and #21496, where some rw that worked need to be replaced by erw. It's possible that reducibility of HasQuotient.quotient' made the statements pick up some instances not reducibly defeq to the old ones, which adding @[reducible] might be a solution ...?

[Jovan Gerbscheid]

It seems expected to me that something might break from such changes. Why is it that you want to change this?