Using `abbrev` for a class

Stream: lean4

[Wrenna Robson]

Suppose I have a class that is a special case of another class: the example I am thinking of is OrderHomClass. In this case, this is defined using abbrev. Suppose I want to make this definition non-reducible. I don't think I can use def (because I want it to be recognised as a class), but I'm not sure how to therefore define it, as using class doesn't seem to work.

I can make this work:

/-- `OrderHomClass F α b` asserts that `F` is a type of `≤`-preserving morphisms. -/
class OrderHomClass (F : Type*) (α β : outParam Type*) [LE α] [LE β] [FunLike F α β] extends
  RelHomClass F ((· ≤ ·) : α → α → Prop) ((· ≤ ·) : β → β → Prop)

But then things that define a RelHomClass don't seem to define this (I'm not sure precisely what extends does.)

What is the best way to do this?

[Jovan Gerbscheid]

You seem to already get how it works. There are two options:

• use abbrev. This has the convenience that all existing instances also apply to your new class
• use class, possibly with an extends clause. This defines an entirely new class, so you will have to add all instances about it manually. In this may come with performance benefits.

[Wrenna Robson]

Related question: OrderEmbedding is defined using abbrev. I could define it using def instead here, or I could do something similar to the above and use structure with a possible extends on RelEmbedding.

We are minded to stop it being reducible, in part because we don't want all the instances of RelEmbedding to apply, or rather we want to be able to apply them if we choose but don't want them to automatically apply. My initial thought was to use def for this. Initial trials suggest this might work but it does give some undesired behaviour - in particular, I was having some issues with simps-generated lemmas not actually simplifying when they seem like they ought to, and in general it doesn't seem to be possible to define custom simps projections for the new structure. So perhaps this isn't actually recommended?

[Jovan Gerbscheid]

If the simps lemmas involve projections from OrderEmbedding applied to a term of type RelEmbedding, then that is some defeq abuse that simp doesn't support.

And I think using structure + extends is a reasonable option (and it will probably be easier for to_dual to deal with)

[Jovan Gerbscheid]

Which instances are the ones that you would like to not apply automatically?

[Wrenna Robson]

No, I was thinking of projections from OrderEmbedding applied to a term of type OrderEmbedding.

[Wrenna Robson]

Jovan Gerbscheid said:

Which instances are the ones that you would like to not apply automatically?

It is honestly hard to be sure about this because the current situation (where OrderHom is defined inconsistently to OrderEmbedding and OrderIso) is such a mess.

[Wrenna Robson]

It's possible we do want them. But I think (@Bhavik Mehta is who I have been discussing this with) we are in general frustrated at the weird lack of API for Order* in places because you can "just use Rel*", even though sometimes that ends up a bit hacky.

[Jovan Gerbscheid]

Wrenna Robson said:

OrderHom is defined inconsistently to OrderEmbedding and OrderIso

Oh, that doesn't look good. Is there consensus on which kind is the preferred form?

[Wrenna Robson]

We thought that using a def for Rel* was going to be right. I am no longer certain of this!

[Wrenna Robson]

Essentially there's a number of tasks here - the file that defines them needs tidying and untangling a bit (I have a PR for this ready and up), then the re-definitions, probably doing "fix OrderEmbedding and OrderIso" and "fix OrderHom" separately. There's also some smaller tasks that reflect other issues.

[Wrenna Robson]

(OrderHom is also dependent on Preorder when the others aren't - I believe there is now consensus that this, at least, should be changed, i.e. we don't use the Monotone predicate but instead something equivalent that doesn't require Preorder.)

[Jovan Gerbscheid]

Oh, why does Monotone even require Preorder?

[Wrenna Robson]

Ultimately everyone agrees that they should be consistent - I would say we are getting to the point of consensus on what they should be but not quite there.

[Wrenna Robson]

Jovan Gerbscheid said:

Oh, why does Monotone even require Preorder?

That is a different argument :)

[Wrenna Robson]

I feel similarly to you but it was changed to be dependent for reasons that made sense at the time at the very least.

[Wrenna Robson]

This patch is the one where I was working on changing OrderEmbedding and OrderIso to def. If you look at the file with sorries in it, some places that previously were solved with simp are no longer solved by it.

https://github.com/leanprover-community/mathlib4/pull/28968/commits/d2e6c811bc8499294e4853d7a5cd19fab3fa249c

You can rewrite them manually using the lemma generated by simps, but simp itself doesn't work, even if you explictly give it that lemma. Which is Weird Behaviour.

[Wrenna Robson]

And I think ultimately comes down to this thing of simps getting confused about the fact it's a def defined from a structure.

[Jovan Gerbscheid]

It is indeed as I suggested above, that the lemma is ill-typed in the reducible transparency, and therefore we can't rely on simp to apply it. The LHS is:

@DFunLike.coe ((fun x1 x2 ↦ x1 ≤ x2) ≃r fun x1 x2 ↦ x1 ≤ x2) (α₁ ⊕ β₁) (fun x ↦ α₂ ⊕ β₂) RelIso.instFunLike
  (ea.sumCongr eb) a✝ : α₂ ⊕ β₂

This implicit argument implies that ea.sumCongr eb has type (fun x1 x2 ↦ x1 ≤ x2) ≃r fun x1 x2 ↦ x1 ≤ x2. Which only holds in default transparency.

[Wrenna Robson]

Yeah - what I don't get is why it's done it reducible as you say? Like this does work if it's abbrev but it doesn't work if it's def.

[Wrenna Robson]

But indeed this does feel like a transparency issue and I will freely admit I don't fully understand them. It feels to me that using def, risking the existence of simps lemmas that do not apply in practice, is not good.

[Jovan Gerbscheid]

Arguably this is a bug in simps. It should not have (fun x1 x2 ↦ x1 ≤ x2) ≃r fun x1 x2 ↦ x1 ≤ x2 there, but instead α₁ ⊕ β₁ ≃o α₂ ⊕ β₂.

[Wrenna Robson]

Yes, that sounds right.

[Wrenna Robson]

It's why I raised this in this stream rather than the mathlib one - while this is in mathlib it felt more like a discussion about how to define things "right" in Lean itself.

[Jovan Gerbscheid]

Here's the MWE of what's going on:

import Mathlib

variable (α : Type)

def B := Equiv α α

@[simps]
def b : B α where
  toFun := id
  invFun := id

set_option pp.explicit true
#check b_apply
/-
b_apply (α : Type) (a : α) :
  @Eq α
    (@DFunLike.coe (Equiv α α) α (fun x => α) (@EquivLike.toFunLike (Equiv α α) α α (@Equiv.instEquivLike α α)) (b α) a)
    (@id α a)
-/

Actually, I don't think we can blame simps here. Because in the definition of b we are constructing a B α, using the Equiv.mk constructor.

[Wrenna Robson]

Right, ultimately what we want on some level is a way to go "B is a new structure, but it is a copy of Equiv α α and I want an easy way of copying over instances on the latter to the former".

[Wrenna Robson]

Because then there would be a "B.mk" (which currently there is not).

[Jovan Gerbscheid]

Doesn't structure + extends do exactly that?

[Wrenna Robson]

Well, it isn't clear how to copy the instances. How would you implement FunLike B α α if you had structure B extends Equiv α α.

[Jovan Gerbscheid]

Ah, that's true

[Wrenna Robson]

Obviously if you use abbrev you have the instances and there's no issue with simps but you kinda have the undesirable behaviour that the "innards" of B are exposed - in the context above, we kinda want Order* to maybe be semi-reducible at worst.