Use typeclasses of coerced type?

Stream: new members

[Fernando Chu]

Is there any way to use the typeclasses of a coerced type without manually specifying the coercion? E.g.

import Mathlib

structure WrappedList where
  wrap : List ℕ

attribute [coe] WrappedList.wrap

instance : Coe WrappedList (List ℕ) where
  coe l := WrappedList.wrap l

def Foo : WrappedList := ⟨[1,2]⟩

#check 1 ∈ (Foo : List ℕ) --works
#check 1 ∈ Foo -- failed to synthesize Membership ?m.18521 WrappedList

[Fernando Chu]

Seems not. Is there at least an easy way for Foo to inherit all of List ℕ's typeclasses?

[Kenny Lau]

abbrev is the easy way (but it's not applicable here and i hate abbrev)

[Yaël Dillies]

Please don't use abbrev anymore. It now has (or always had?) confusing reduction behavior, and one should instead use @[reducible] def

[Fernando Chu]

Yaël Dillies said:

Please don't use abbrev anymore. It now has (or always had?) confusing reduction behavior, and one should instead use @[reducible] def

Oh that's interesting, could you please point to one such example?

[Yaël Dillies]

Very unminimised, but @Edison Xie's repo https://github.com/Whysoserioushah/BrauerGroup_new got much faster once we replaced abbrev with @[reducible] def. I believe @Bhavik Mehta was the one teaching this to us.

[Kenny Lau]

please just pretend abbrev doesn't exist, i really hate abbrev

[Kyle Miller]

Yaël Dillies said:

Please don't use abbrev anymore. It now has (or always had?) confusing reduction behavior, and one should instead use @[reducible] def

abbrev is short for @[reducible, inline] def, so when it comes to reduction, it should be exactly the same as @[reducible] def.

Maybe you ran into some code generation slowness from @[inline]?

[Kyle Miller]

That link is certainly unminimized. What kind of declaration did you switch from abbrev? A type synonym? Or some other term?

[Yaël Dillies]

What I understood from Bhavik was that abbrev A := B meant "reduce A to B" AND "reduce B to A". I suggest we wait for him to confirm/infirm my understanding of what he said

[Kyle Miller]

That's definitely is not the case. An abbrev is like any other def, except for the additional attributes.

[Kyle Miller]

I guess there's one other difference: abbrev also marks the definition to be an abbrev in the kernel. I thought that meant the definition is preferred to be unfolded in kernel defeqs, but I'm not completely sure. (Edit: yes, some details below.)

[Yaël Dillies]

Maybe "reduce" in my understanding above should be "kernel-reduce"

[Yaël Dillies]

Kyle Miller said:

That link is certainly unminimized. What kind of declaration did you switch from abbrev? A type synonym? Or some other term?

It was a term. Edison will know more

[Kyle Miller]

(docs#Lean.Elab.Command.mkDefViewOfAbbrev is where an abbrev gains @[inline, reducible], and Lean.Elab.addNonRecAux is where the definition is added to the environment with ReducibilityHints.abbrev instead of ReducibilityHints.regular.)

[Kyle Miller]

I think we shouldn't tell people that abbrev is somehow deprecated. We use it frequently for type synonyms in core Lean.

[Yaël Dillies]

I am certainly not trying to say it is deprecated. And I do not exactly know what's wrong with it, but for sure something is wrong

[Kyle Miller]

Ok, then please don't say things like this:
Yaël Dillies said:

Please don't use abbrev anymore. [...] one should instead use @[reducible] def

That seems like a clear deprecation to me.

Are you able to point out which definition was changed to @[reducible] in that repo?

(I just checked the kernel code: abbrev only affects tie-breaking when you have f x1 ... xn =?= g y1 ... yn and something needs to be unfolded. Normally, regular definitions use the heuristic that the more-or-less newer definition gets unfolded. Using abbrev causes the definition to be "newer" than even definitions that haven't been defined yet. There are definitely cases where this is the wrong heuristic, but that doesn't mean that abbrev itself is incorrect. It's worth getting some examples to see what's going on.)

[Kyle Miller]

@Fernando Chu Sorry, this is getting off-topic.

Answering your question, there's not an easy way to inherit all typeclasses in a wrapper like that.

The problem you were running into with the Membership instance is that in 1 ∈ Foo, the existence of the coercion and the existence of a List membership instance isn't enough to trigger inserting the coercion.

I assume in your application WrappedList has other fields too, not just wrap?

[Fernando Chu]

Kyle Miller said:

I assume in your application WrappedList has other fields too, not just wrap?

Indeed. The abbrev thing is still quite interesting to me though; since I'm doing stuff with syntax, I do have been also struggling with getting the right reduction behaviour.

[Kenny Lau]

Kyle Miller said:

Ok, then please don't say things like this:

but can I say that I hate abbrev?

[Kyle Miller]

Maybe there are other techniques, but copying instances seems like it takes a lot of boilerplate:

import Mathlib

structure WrappedList where
  wrap : List ℕ

instance : Coe WrappedList (List ℕ) where
  coe := WrappedList.wrap

instance : Membership ℕ WrappedList where
  mem l n := n ∈ l.wrap

@[simp] theorem WrappedList.mem_coe {n : ℕ} {l : WrappedList} : n ∈ (l : List ℕ) ↔ n ∈ l := Iff.rfl

You need that last lemma to normalize which membership instance is actually being used when you're proving things.

[Fernando Chu]

Kyle Miller said:

The problem you were running into with the Membership instance is that in 1 ∈ Foo, the existence of the coercion and the existence of a List membership instance isn't enough to trigger inserting the coercion.

The reference says

Coercion insertion is attempted in the following situations where an error would otherwise occur:
- The expected type for a term is not equal to the type found for the term.

Is this not totally accurate? At least my interpretation is that it should trigger in your described case

[Kyle Miller]

There's no expected type here, that's the problem.

[Fernando Chu]

Ah! I see, thanks that clears things up.

[Kenny Lau]

you also want attribute [coe] WrappedList.wrap

[Yaël Dillies]

Kyle Miller said:

Ok, then please don't say things like this:
Yaël Dillies said:

Please don't use abbrev anymore. [...] one should instead use @[reducible] def

That seems like a clear deprecation to me.

Apologies, I took the abbrev news from Bhavik/Edison a bit too uncritically, and I thought that the worst thing that could happen was that you would look up the source code to disprove me

[Edison Xie]

Yaël Dillies said:

Very unminimised, but Edison Xie's repo https://github.com/Whysoserioushah/BrauerGroup_new got much faster once we replaced abbrev with @[reducible] def. I believe Bhavik Mehta was the one teaching this to us.

I’m already an expert in making things slow and thanks to you and Bhavik I’m on my way to become an expert to make things fast! :))

[Bhavik Mehta]

What I think I said to Yaël and Edison is that abbrev often does things which I think are undesirable, and so I personally don't use it.
The case which is somewhat related to reduction (but I don't think is just because of reduction) happened with determinants in sphere packing, see example 1 and example 2, where in both cases abbrev doesn't work but changing Matrix.det to a reducible inline def did work (if I remember correctly).
The other case, which is what I think the A -> B and B -> A bit is referring to, was in #26494, where inference was working "backwards" (in my eyes) to get a TopologicalSpace instance using Scott in a case where Scott was never mentioned. Note this is now fixed in mathlib4 master, so you'll need to look at an earlier version to reproduce

[Bhavik Mehta]

On the second one, to quote from DMs with Sebastian Ullrich:

Bhavik Mehta: I observed recently that we sometimes end up with an instance getting applied on X if that instance exists for F X, where F X is an abbrev type synonym for X, and leads to what I think is confusing/unintended behaviour in mathlib, eg #26494. Is this expected behaviour of abbrev? More specifically, given abbrev Scott (X : Type*) := X, and instance : TopologicalSpace (Scott X) := ..., is it expected that TopologicalSpace X is synthesised by the scott version?

Sebastian Ullrich: Yes, that's expected. It is how the normalized indexing for instance lookup works/must work.

In the space of a week, Yaël and I found three independent projects which were unintentionally using this instance, and therefore had false sorries!

[Aaron Liu]

Well Scott should never have been an abbrev

[Bhavik Mehta]

Sure, that's why the fix here was to remove Scott rather than change the behaviour of abbrev wrt typeclass search. (We have WithScott which correctly handles it instead) But the behaviour was still surprising to me

[Yaël Dillies]

Wait, that rings a bell! #mathlib4 > Bug in instance synthesis? @ 💬

[Bhavik Mehta]

I think that's different still actually, since that's about why def is also not good for type synonyms, whereas this is about why abbrev is not good for type synonyms

[Kyle Miller]

Bhavik Mehta said:

this is about why abbrev is not good for type synonyms

I'm not understanding why it's not good for type synonyms? This Scott example shows that typeclass instance sees directly through the abbreviation, so it's a perfect synonym, and it shouldn't have been a synonym. It's like type in Haskell.

The other thread is that def is actually not enough like Haskell's newtype.

[Bhavik Mehta]

Kyle Miller said:

Bhavik Mehta said:

this is about why abbrev is not good for type synonyms

I'm not understanding why it's not good for type synonyms? This Scott example shows that typeclass instance sees directly through the abbreviation, so it's a perfect synonym, and it shouldn't have been a synonym. It's like type in Haskell.

"not good" was too strong, you're right. All I mean is that it's surprising to me that Scott got introduced in a situation where it wasn't mentioned at all, and that this (in combination with the bad synonym in mathlib) ended up being a footgun for beginners

[Kyle Miller]

Bhavik Mehta said:

see example 1 and example 2,

Can you help me interpret these? What needs to be @[reducible] def instead of an abbrev?

[Bhavik Mehta]

Matrix.det needed to be a reducible def rather than an abbrev

[Kyle Miller]

Why is Matrix.det reducible at all?

[Bhavik Mehta]

After seeing these examples, I agree it shouldn't be :)

[Kyle Miller]

I'm surprised though that

abbrev det (M : Matrix n n R) : R :=
  detRowAlternating M

could cause any troubles. The detRowAlternating function isn't reducible, so it seems like it's a straightforward sort of abbreviation.

[Bhavik Mehta]

I spent quite a bit of time discussing very similar things with Sebastian a couple of weeks ago :) eg

Sebastian Ullrich:

Here is a question that may have very subjective answers: after looking at the output of

set_option pp.all true
#print Matrix.det

would you say that Mathlib is correct in making det an abbrev? :)

[Bhavik Mehta]

In the second example, I also tried

set_option allowUnsafeReducibility true
attribute [local semireducible] Matrix.det in

before the theorem which gives a kernel error, but Sebastian told me

Ah, this behavior is actually specific to abbrev, not [reducible]
It creates a ReducibilityHints.abbrev definition which cannot be adjusted after the fact
And this kind of hint is the only one shared by the elaborator and the kernel, which explains why both are affected

[Bhavik Mehta]

(cc @Sebastian Ullrich. I'm quoting directly to avoid accidentally spreading misinformation, but perhaps you can explain better than I can)

[Bhavik Mehta]

Oh and the conclusion of the discussion:

Bhavik Mehta: Is it your opinion that Matrix.det should be a def (or reducible def)? I expect mathlib will be okay with that if there isn't much fallout in mathlib as a consequence, but if lots of other things need to be changed then it might be trickier

Sebastian Ullrich: Reducible def sounds like a good compromise to me, that should not break any code

[Kyle Miller]

(The ReducibilityHints.abbrev is definitely a property of abbrevs, and it's inside the definition's environment declaration itself. It's used inside defeq to decide, when you have two function applications, and no progress can be made without unfolding, which of the functions to unfold first.)

[Bhavik Mehta]

My interpretation is that that's what Yaël's

It now has (or always had?) confusing reduction behavior, and one should instead use @[reducible] def

was intending to say, but got mangled into something unhelpful because it was third- or fourth-hand information

[Sebastian Ullrich]

Since I haven't seen it being mentioned explicitly yet: please note that there is no difference between abbrev and @[reducible] def in the "backwards instance" case

[Robin Arnez]

Bhavik Mehta schrieb:

see example 1 and example 2

I'm not sure if you can blame this on abbrev, really:

import Mathlib.Data.Real.Basic
import Mathlib.LinearAlgebra.Matrix.Determinant.Basic

variable {R : Type*}

def E8Matrix (R : Type*) [Field R] : Matrix (Fin 8) (Fin 8) R := 1

theorem E8Matrix_det_eq_one (R : Type*) [Field R] [NeZero (2 : R)] : Matrix.detRowAlternating (E8Matrix R) = 1 := by
  sorry

lemma test : Matrix.detRowAlternating (E8Matrix ℝ) = 1 := E8Matrix_det_eq_one ℝ

has the same problem

[Aaron Liu]

I think abbrev is really intuitive. It's what you do when you have some long term and you want to introduce an abbreviation for it. So the abbrev will inherit all the typeclass instances on the original type, and simp will see through it, and if you put an instance on an abbrev then it will apply to the original type too.

[Aaron Liu]

Like notation but it also gives you a constant

[Bhavik Mehta]

Aaron Liu said:

simp will see through it

I would argue that "simp will see through it" implies the first of these should succeed, but it doesn't

abbrev bar (a b : Nat) : Prop := Nat.gcd a b = 1

theorem test_bar : ∀ a b : Nat, bar a b → ¬ a = 0 → bar a b := by
  simp +contextual -- fails

theorem test_no_bar : ∀ a b : Nat, Nat.gcd a b = 1 → ¬ a = 0 → Nat.gcd a b = 1 := by
  simp +contextual -- works

[Bhavik Mehta]

Robin Arnez said:

I'm not sure if you can blame this on abbrev, really:

import Mathlib.Data.Real.Basic
import Mathlib.LinearAlgebra.Matrix.Determinant.Basic

variable {R : Type*}

def E8Matrix (R : Type*) [Field R] : Matrix (Fin 8) (Fin 8) R := 1

theorem E8Matrix_det_eq_one (R : Type*) [Field R] [NeZero (2 : R)] : Matrix.detRowAlternating (E8Matrix R) = 1 := by
  sorry

lemma test : Matrix.detRowAlternating (E8Matrix ℝ) = 1 := E8Matrix_det_eq_one ℝ

has the same problem

That's perhaps fair, although the fix for example 2 was to make a local version of Matrix.det which wasn't an abbrev, and then it goes through completely fine. Since making the single change of avoiding abbrev fixes it, I think it's not unreasonable to say abbrev was at fault

[Fernando Chu]

Was just about to mention that, see also this. Abbrev is not really an abbreviation, at least not in the usual math or programming way

[Fernando Chu]

As a summary, is my following interpretation of abbrev correct?

abbrev is an abbreviation (i.e. writing the definition again in its place) except that:

• It creates a ReducibilityHints.abbrev definition which cannot be adjusted after the fact. This is used to decide, when you have two function applications, and no progress can be made without unfolding, which of the functions to unfold first. (I'm not sure if this breaks abbrev being an abbreviation)
• Tactics may not always work as explained in the issue

[Kyle Miller]

It's possible that lean4#5606 could be reopened...

We don't want simp to unfold every reducible definition, since the abbreviations are helpful to understand goal states. However, simp could tentatively unfold definitions, see whether or not the result simplifies any further, and if no progress is made, revert to the original term.

[Kyle Miller]

Bhavik Mehta said:

I think it's not unreasonable to say abbrev was at fault

Lean's a very complex system though, and while abbrev might be an ingredient (a proximal cause) it might not be what's at fault...

[Bhavik Mehta]

That's fair, if you have suggestions for other fixes here then I'd be very happy to hear them; I spent quite a lot of time on this and this is the only way I could find to make example 2 work

[Kyle Miller]

I think that it's reasonable having this abbrev -> @[reducible] def trick in the toolbox of workarounds, and it's worth telling people about it, so long as it's clear that we're not really sure what it's working around precisely yet.

[Bhavik Mehta]

Isn't it precisely working around ReducibilityHints.abbrev as you mentioned?

[Kyle Miller]

No, I wouldn't say that. There seems to be something weird about these terms that triggers more unfolding than necessary.

Analogue: let's say you find out that setting the priority of some instance to 100 fixes a problem. Would it make sense to say that priority 1000 is at fault? No, it's how the priorities interact with everything else in the whole collection of instances.

[Kyle Miller]

@Robin Arnez's example suggests something is amiss, right? Why is the definition Matrix.detRowAlternating being unfolded at all?

It seems significant that it's ℝ rather than a general field. Maybe there's an instance diamond? (Or a diamond in some weaker sense that causes defeq to decide the arguments aren't similar enough, triggering unfolding?)

[Bhavik Mehta]

I agree it's significant; the particular specialisation of R to \R is what seems to break it. My interpretation of this was that now the lhs is a closed term, and so reduction can fire at all, but that's just a guess

[Bhavik Mehta]

Note, as I mentioned before, that attribute [-instance] Real.commRing in fixes Robin's example, but not example 2

[Kyle Miller]

There's also some chance that the fact that Matrix.detRowAlternating is a funlike is breaking some of the elaborator's isdefeq heurstics. That could explain why having a semireducible Matrix.det would make it go through.

The heuristic is "for f a1 ... an =?= f b1 ... bn, see if ai =?= bi for each i. When there are higher-order things going on (like in DFunLike.coe) the logic is more complicated, and it could be hitting some bug or other limitation.

[Kyle Miller]

It looks like attribute [-instance] Real.commRing causes the expressions in Robin's example to be structurally equal, so defeq doesn't have to do any work. In particular, Matrix.detRowAlternating (E8Matrix ℝ) =?= Matrix.detRowAlternating (E8Matrix ℝ)

[Kyle Miller]

This seems to be the most promising explanation at the moment. When it's an abbrev, then DFunLike.coe Matrix.detRowAlternating is exposed to defeq checks, and that's apparently very sensitive to some relevant arguments being only defeq.

I don't know these defeq internals well enough though. It could also be that since DFunLike.coe is a class projection that the elaborator likes to reduce these.

[Bhavik Mehta]

That doesn't explain the second example though right, since there it's a kernel problem rather than an elaborator problem?

[Kyle Miller]

You're right, the second example succeeds with set_option debug.skipKernelTC true.

[Kyle Miller]

The heuristics between the kernel and elaborator might be a bit different though. It could be a similar phenomenon, but it's unclear.

[Kyle Miller]

In the kernel, lazy_delta_reduction_step prefers unfolding projections (and skips the are-the-arguments-defeq heuristic), so it could still be that DFunLike.coe explains it to some degree.

[Jireh Loreaux]

I'll note something that @Frédéric Dupuis and I observed related to this "backwards instance" problem:
Bhavik Mehta said:

The other case, which is what I think the A -> B and B -> A bit is referring to, was in #26494, where inference was working "backwards" (in my eyes) to get a TopologicalSpace instance using Scott in a case where Scott was never mentioned.

We needed to create a type synyonym for docs#Matrix which is docs#CStarMatrix. This is just Matrix with a new norm. The norm is defined by action on vectors with entries in a C⋆-algebra. Originally, we had tried using abbrev, but we also experienced a situation in the middle of a proof where a term of type Matrix picked up the instance from CStarMatrix. So, we had to resort to a def synonym at default transparency (although now lean4#9077 even makes that choice suspect, which is very frightening).

The issue with using default transparency, of course, is that every algebraic Matrix operation we need must be ported to the new type (and there are a hell of a lot). If we use one-field structures, this would be even more painful I suspect.

[Kyle Miller]

I was hoping that pulling the toFun definition out like this would be a fix:

def alternatization.f (m : MultilinearMap R (fun _ : ι ↦ M) N') : M [⋀^ι]→ₗ[R] N' :=
  { ∑ σ : Perm ι, Equiv.Perm.sign σ • m.domDomCongr σ with
    toFun := ⇑(∑ σ : Perm ι, Equiv.Perm.sign σ • m.domDomCongr σ)
    map_eq_zero_of_eq' := fun v i j hvij hij =>
      alternization_map_eq_zero_of_eq_aux m v i j hij hvij }

/-- Produce an `AlternatingMap` out of a `MultilinearMap`, by summing over all argument
permutations. -/
def alternatization : MultilinearMap R (fun _ : ι => M) N' →+ M [⋀^ι]→ₗ[R] N' where
  toFun := alternatization.f
  map_add' a b := by
    ext
    simp only [mk_coe, AlternatingMap.coe_mk, sum_apply, smul_apply, domDomCongr_apply, add_apply,
      smul_add, Finset.sum_add_distrib, AlternatingMap.add_apply, alternatization.f]
  map_zero' := by
    ext
    simp only [mk_coe, AlternatingMap.coe_mk, sum_apply, smul_apply, domDomCongr_apply,
      zero_apply, smul_zero, Finset.sum_const_zero, AlternatingMap.zero_apply, alternatization.f]

but it seems that the default ProjReductionKind.yesWithDelta somehow causes this to still unfold alternatization.f unnecessarily (or at least, changing this option prevents the unfolding from happing in some way!)

Setting this to ProjReductionKind.no or .yes prevents it from being unfolded. The following even works without any changes to alternatization:

import Mathlib.Data.Real.Basic
import Mathlib.LinearAlgebra.Matrix.Determinant.Basic

variable {R : Type*}

def E8Matrix (R : Type*) [Field R] : Matrix (Fin 8) (Fin 8) R := 1

elab "foo " t:term : term <= expectedType? => do
  Lean.Meta.withConfig (fun c => { c with proj := .yes }) do
    Lean.Elab.Term.elabTerm t expectedType?

theorem E8Matrix_det_eq_one (R : Type*) [Field R] [NeZero (2 : R)] : Matrix.detRowAlternating (E8Matrix R) = 1 := by
  sorry
set_option debug.skipKernelTC true

lemma test : Matrix.detRowAlternating (E8Matrix ℝ) = 1 :=
  foo (id (E8Matrix_det_eq_one ℝ))

(the id is to make sure that the defeq is definitely done within the scope of foo)

[Bhavik Mehta]

Jireh Loreaux said:

The issue with using default transparency, of course, is that every algebraic Matrix operation we need must be ported to the new type (and there are a hell of a lot). If we use one-field structures, this would be even more painful I suspect.

I wonder if we should try to introduce some automation to make the one-field structure instance copying easier, generalizing the existing deriving machinery

[Bhavik Mehta]

Kyle Miller said:

You're right, the second example succeeds with set_option debug.skipKernelTC true.

It may be the case that the first and second examples have different root causes. The second is closer to the actual case that showed up, and the first was my first attempt at minimising, except I think I over-minimised; since the instance change solves the first and not the second. They're both solved by changing Matrix.det to a def, but as you say this might not be the true cause

[Jireh Loreaux]

Bhavik Mehta said:

I wonder if we should try to introduce some automation to make the one-field structure instance copying easier, generalizing the existing deriving machinery

I think that's a good idea in general, but it would have to be quite sophisticated to copy over all the relevant bits of Matrix.