equiv_like extending fun_like

Stream: maths

[Jireh Loreaux]

@Anne Baanen Why doesn't equiv_like extend fun_like? I mean, I know why it can't with the current definition (because the the coe_injective is different). But it seems that this is not required because the second argument of equiv_like.coe_injective can be derived from everything else, so it is redundant in the implicaiton. See below. Changing this would allow all the equiv_type classes to be just extensions of equiv_like as well as the corresponding fun_like instances for whatever morphisms we care about.

I was led to this from the consideration about alg_equiv_class that I mentioned before in this thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/redefining.20alg_equiv_class. Namely, I really wanted to simplify the typeclass assumptions to has_{mul,add,smul} on both the source and the target. If we had a smul_equiv_class, I could do that, but we don't, we only have a smul_hom_class. (Maybe we should have a smul_equiv_class, but that's beside the point.) So, I tried smul_hom_class and that led to an error because I can't extend both smul_hom_class and ring_equiv_class since equiv_like and fun_like have different coe_injective fields.

import data.fun_like.equiv
import tactic

variables {E α β : Type*} [equiv_like E α β]
example (e₁ e₂ : E) (h : (equiv_like.coe e₁ : α → β)  = (equiv_like.coe e₂)) : (equiv_like.inv e₁ : β → α) = equiv_like.inv e₂ :=
begin
  funext,
  have h₁ := @equiv_like.left_inv E α β _ e₂,
  have h₂ := @equiv_like.right_inv E α β _ e₁,
  specialize h₂ x,
  nth_rewrite 0 h at h₂,
  nth_rewrite 1 ←h₂,
  rw h₁ _,
end

[Anne Baanen]

I recall my reasoning was that docs#equiv_like.coe_injective' is much easier to prove in practice: by { intros f g h₁ h₂; cases f; cases g; congr'}. Not allowing diamond inheritance is annoying indeed, so if you know a nice way to keep proofs of coe_injective easy then I'm not going to object to changing this.

[Anne Baanen]

Note however that docs#ring_equiv_class is not just docs#ring_hom_class with an extra inverse: bijective maps automatically preserve zero and one, so we don't include map_zero and map_one fields. So I don't know how many cases the diamond inheritance actually helps with. (Similarly for alg_equiv_class.)

[Eric Wieser]

Why do we case whether equiv_like extends fun_like when we already have docs#equiv_like.fun_like? oh, we don't have that

[Anne Baanen]

We do, it just goes via docs#equiv_like.to_embedding_like :)

[Anne Baanen]

The specific thing that we don't have is being able to say extends foo_equiv_class, bar_hom_class.

[Jireh Loreaux]

I think one way to keep the equiv_like proofs easy is just to have a custom constructor for equiv_like which eats the current version and spits out the new version with the fun_like coe_injective field. Of course, we probably wouldn't want to have such a constructor for every extension of equiv_like, so this may lead to slightly ugly proofs like the one below. And of course this isn't quite as intuitive, so we would need to add something to the documentation to the effect of "always use the custom constructor when creating instances."

instance : add_equiv_class F A B :=
{ map_add := sorry,
  .. custom_constructor
  { coe := sorry,
    inv := sorry,
    left_inv := sorry,
    right_inv := sorry,
    coe_injective := sorry } }

[Jireh Loreaux]

does this seem reasonable?

[Jireh Loreaux]

I just saw your code note in equiv_like about your reasoning for including the inv in the coe_injective field, sorry!

[Jireh Loreaux]

This is what it would look like:

import data.fun_like.basic
import tactic.congr

-- this would be the basic setup

variables {E α β : Type*}

structure equiv_like.core (E α β : Type*) :=
(coe : E → α → β)
(inv : E → β → α)
(left_inv  : ∀ e, function.left_inverse (inv e) (coe e))
(right_inv : ∀ e, function.right_inverse (inv e) (coe e))
-- The `inv` hypothesis makes this easier to prove with `congr'`
(coe_injective' : ∀ e g, coe e = coe g → inv e = inv g → e = g)

lemma equiv_like.inv_eq_of_coe_eq (h : equiv_like.core E α β) {e₁ e₂ : E}
  (h_eq : h.coe e₁ = h.coe e₂) : h.inv e₁ = h.inv e₂ :=
funext $ λ x, h.left_inv e₂ (h.inv e₁ x) ▸ (congr_arg (h.inv e₂) (h_eq ▸ h.right_inv e₁ x))

class equiv_like (E : Type*) (α β : out_param Type*) extends fun_like E α (λ _, β) :=
(inv : E → β → α)
(left_inv  : ∀ e, function.left_inverse (inv e) (coe e))
(right_inv : ∀ e, function.right_inverse (inv e) (coe e))

variables (E)
def equiv_like.of_core (h : equiv_like.core E α β) : equiv_like E α β :=
{ coe := h.coe,
  coe_injective' := λ e₁ e₂ he, h.coe_injective' _ _ he (equiv_like.inv_eq_of_coe_eq h he),
  inv := h.inv,
  left_inv := h.left_inv,
  right_inv := h.right_inv }

----- then an example to see how it works in practice

class add_equiv_class (E : Type*) (α β : out_param Type*) [has_add α] [has_add β]
  extends equiv_like E α β :=
(map_add : ∀ e : E, ∀ x y : α, e (x + y) = e x + e y)

structure add_equiv (α β : Type*) [has_add α] [has_add β] :=
(to_fun : α → β)
(inv_fun : β → α)
(left_inv : function.left_inverse inv_fun to_fun)
(right_inv : function.right_inverse inv_fun to_fun)
(map_add' : ∀ x y, to_fun (x + y) = to_fun x + to_fun y)

instance add_equiv.add_equiv_class {α β : Type*} [has_add α] [has_add β] :
  add_equiv_class (add_equiv α β) α β :=
{ map_add := λ f, f.map_add',
  .. (equiv_like.of_core (add_equiv α β)
  { coe := λ e, e.to_fun,
    coe_injective' := λ e₁ e₂ h₁ h₂, by { cases e₁; cases e₂; congr' },
    inv := λ e, e.inv_fun,
    left_inv := λ e, e.left_inv,
    right_inv := λ e, e.right_inv, }) }

[Jireh Loreaux]

Another way, almost certainly better: rename the current equiv_like.coe_injective' field to equiv_like.coe_inv_injective, and then have autofill the equiv_like.coe_injective' (with the fun_like.coe_injective' definition) with the necessary lemma.

[Jireh Loreaux]

(deleted)

[Frédéric Dupuis]

Why not just have a lemma that proves fun_like.coe_injective' from the current equiv_like.coe_injective', that we would then systematically apply, instead of doing this with a whole structure?

[Frédéric Dupuis]

Also, if we make equiv_like extend fun_like, my guess is that the coe_injective' proof would almost always come from the corresponding hom anyway, so we would almost never actually have to prove it "by hand".

[Yaël Dillies]

What are you trying to achieve, Jireh? I don't understand how this has to do with what class extends what.

[Jireh Loreaux]

Frédéric Dupuis said:

Also, if we make equiv_like extend fun_like, my guess is that the coe_injective' proof would almost always come from the corresponding hom anyway, so we would almost never actually have to prove it "by hand".

No, Anne has a point here, it would be (comparatively) hard to prove the fun_like.coe_injective' field when creating an instance of equiv_like for some kind of equiv type. (if you don't understand, try it directly and you'll realize why it's hard.)

[Jireh Loreaux]

Yaël Dillies said:

What are you trying to achieve, Jireh? I don't understand how this has to do with what class extends what.

The point is to make equiv_like extend fun_like, and that way you can write things like class new_equiv_class extends old_equiv_class, some_hom_class, which we currently can't do.

[Jireh Loreaux]

Give me a few minutes and I'll have something nice working that should be almost a drop-in replacement.

[Yaël Dillies]

Okay, but why do you care about the extension mechanism? This is an implementation detail, even from the point of view of API writing!

[Jireh Loreaux]

I'm not sure how what I just said doesn't explain why I care. Yes, of course this is an implementation detail, but the point is I'm looking to improve the implementation slightly.

[Yaël Dillies]

I am trying to un-xy, and you just gave me another x!

[Jireh Loreaux]

Read the second paragraph of the first post in the thread. If that doesn't explain it, then I'm not sure why we're not understanding each other.

[Yaël Dillies]

So, I tried smul_hom_class and that led to an error because I can't extend both smul_hom_class and ring_equiv_class since equiv_like and fun_like have different coe_injective fields.

Why can't you copy over the fields? This is the standard procedure when you can't use extends.

[Jireh Loreaux]

Of course you can! I don't want to. I want things to Just Workᵀᴹ. This is just one small way to make that happen.

[Jireh Loreaux]

It's certainly not a dire point.

[Jireh Loreaux]

I'm not sure why this is broken, presumably it has something to do with the show, but if I could fix whatever the issue here is, this change would essentially amount to a renaming of coe_injective' to coe_inv_injective' wherever an instance of some_equiv_class is declared.

import data.fun_like.basic
import tactic.congr

variables {E α β : Type*}

open function

lemma equiv_like.coe_injective_of_coe_inv (coe' : E → α → β) (inv' : E → β → α)
  (hl : ∀ e, left_inverse (inv' e) (coe' e))
  (hr : ∀ e, right_inverse (inv' e) (coe' e))
  (h : ∀ e₁ e₂, coe' e₁ = coe' e₂ → inv' e₁ = inv' e₂ → e₁ = e₂) :
  injective coe' :=
λ e₁ e₂ he, h e₁ e₂ he $ funext $ λ x, hl e₂ (inv' e₁ x) ▸ congr_arg (inv' e₂) (he ▸ hr e₁ x)

class equiv_like (E : Type*) (α β : out_param Type*) extends fun_like E α (λ _, β) :=
(inv : E → β → α)
(left_inv  : ∀ e, function.left_inverse (inv e) (coe e))
(right_inv : ∀ e, function.right_inverse (inv e) (coe e))
(coe_inv_injective' : ∀ e g, coe e = coe g → inv e = inv g → e = g)
(coe_injective' := equiv_like.coe_injective_of_coe_inv (show E → α → β, from coe) inv left_inv
  right_inv coe_inv_injective')

structure equiv (α β : Type*) :=
(to_fun : α → β)
(inv_fun : β → α)
(left_inv : function.left_inverse inv_fun to_fun)
(right_inv : function.right_inverse inv_fun to_fun)

instance equiv.equiv_class {α β : Type*} :
  equiv_like (equiv α β) α β :=
{ coe := λ e, e.to_fun,
  inv := λ e, e.inv_fun,
  left_inv := λ e, e.left_inv,
  right_inv := λ e, e.right_inv,
  coe_inv_injective' := sorry, }

[Jireh Loreaux]

Any help fixing it is appreciated, although it seems like I'm the only one who values this! :rofl:

[Jireh Loreaux]

okay, I would actually really appreciate if someone can debug the code immediately above (I have edited it slightly), because it feels like an actual bug in Lean to me, but I know virtually nothing. Note that with pp.all true the two types that it is complaining about are verbatim the same; I know for certain because I copied them to two files and diffed them.

[Jireh Loreaux]

cc @Mario Carneiro, is this an actual bug, or am I just really stupid somehow?

[Jireh Loreaux]

sorry, I just noticed there is also this error, but I'm not sure why it's happening: Error updating: deep recursion was detected at 'expression replacer' (potential solution: increase stack space in your system).

[Reid Barton]

I don't know what to make of the fact that ?coe_inv_injective' appears in that type

[Jireh Loreaux]

In case you didn't read the whole thread (expected), this almost certainly has something to do with line 21, note that coe_injective' is a field of fun_like, the class that this equiv_like is extending. Have I done something we're not allowed to do?

[Mario Carneiro]

yeah I think reid found the bug. The type of the metavariable refers to the metavariable itself, so you can't assign it

[Mario Carneiro]

if you put something other than sorry there, or remove it, or type ascribe it the error may go away

[Jireh Loreaux]

with the additional import tactic.congr and replacing the sorry by the usual proof that goes here, namely: λ e g h₁ h₂, by { cases e; cases g; congr' }, then this fails with

tactic failed, result contains meta-variables
state:
no goals

[Eric Rodriguez]

what does recover do?

[Jireh Loreaux]

Same type mismatch as before, although this time without the deep recursion problem. The metavariable ?coe_inv_injective' still appears in the type.

[Jireh Loreaux]

Is this just something we're not capable of doing (i.e., assigning default values to fields of structures we're extending)?

[Yaël Dillies]

It is definitely possible, but I've encountered problems doing so myself.

[Jireh Loreaux]

Ha! fixed with set_option old_structure_command true, which I probably wanted anyway. :face_palm:

[Jireh Loreaux]

The real fix is not extracting that lemma equiv_like.coe_injective_of_coe_inv.

[Jireh Loreaux]

#16161 is essentially a drop-in replacement for equiv_like.

[Eric Wieser]

And of course this isn't quite as intuitive, so we would need to add something to the documentation to the effect of "always use the custom constructor when creating instances."

But conversely, users of {! !} will now be prompted to provide both versions of the coe_injective field; so the new version will also need something in the documentation explaining that coe_injective should not be provided explicitly.

[Yaël Dillies]

In fact, I've been doing the reverse change in other structures throughout the library: If making A extend B results in a redundant field, do not extend B and write the instance manually.

[Eric Wieser]

@Jireh Loreaux, do you have an example based on #16161 that demonstrates a situation where class new_equiv_class extends old_equiv_class, some_hom_class is useful? I note that you don't change any of the existing typeclasses to use this spelling; was that to keep the PR small, or because none of the existing typeclasses fit into this pattern?

[Yaël Dillies]

And there are many common examples as well. Eg docs#group doesn't extend docs#cancel_monoid but instead we have the manual docs#group.to_cancel_monoid. Or again docs#ring doesn't extend docs#semiring.

[Eric Wieser]

I think the difference here is that those all share a common has_mul ancestor though, so you can still extend them all at once later without duplicate field name conflicts.

[Eric Wieser]

We don't have a barely_fun_like ancestor to share the coe field of equiv_like and fun_like

[Eric Wieser]

If we did, then I think Jireh's problem would be solvable using renaming to solve the conflict in the non-data fields

[Yaël Dillies]

Eric Wieser said:

I think the difference here is that those all share a common has_mul ancestor though, so you can still extend them all at once later without duplicate field name conflicts.

But we never do! because that would still result in redundant fields, however far in the hierarchy you're going.

[Eric Wieser]

But at least in user code, you could do that. You're right though, the cases probably doesn't come up in mathlib

[Yaël Dillies]

I maintain that whether a typeclass extends another or not is an implementation detail, even from the implementation perspective.

[Yaël Dillies]

The tradeoff here is "easeness to extend structure A" vs "easeness to provide instances/definitions of structure A". Most likely, the latter is more common.

[Jireh Loreaux]

To answer the @ mention: the example that caused me to look at this in the first place was redefining alg_equiv_class so that it works for both unital and non-unital (even non-associative) algebras. For this it should (or could) be extends ring_equiv_class, smul_hom_class.

[Jireh Loreaux]

I tried to do that, it didn't work, I went hunting and realized it should be possible to make equiv_like extend fun_like, hence this PR.

[Jireh Loreaux]

Yaël, I contend that it's just as easy to provide instances now as it was before. I made sure that this would be a drop-in replacement.

[Jireh Loreaux]

And Eric, I'm not sure of other examples, but yes, I was trying to keep the PR small and make sure nothing really worked differently.

[Jireh Loreaux]

Eric Wieser said:

But conversely, users of {! !} will now be prompted to provide both versions of the coe_injective field; so the new version will also need something in the documentation explaining that coe_injective should not be provided explicitly.

I thought I had this explanation in the PR already; :thinking: maybe I git stashed that documentation somewhere.

[Yaël Dillies]

I still feel like this is a move in the wrong direction. Many less people will try extending equiv_like than there will be people proving equiv_like instances.

[Jireh Loreaux]

To me, extending it makes more sense, despite the fact that I concede your contention that instances are more common than extensions. I fully expected equiv_like to extend fun_like because I think of it has some_fun_like + an inverse, where the fun_like assumptions that go in the equiv_like are as weak as possible, not necessarily the one for the hom class.

But look, I agree it's just an implementation detail. It's one that I quite like to have this way, but I am content to be overruled as well. It's a collaboration after all, so if people don't prefer it then that's fine.

[Yaël Dillies]

I fully expected equiv_like to extend fun_like because I think of it has some_fun_like + an inverse

Actually, this pattern basically never holds:

• docs#order_equiv doesn't extend docs#order_hom
• docs#mul_equiv doesn't extend docs#monoid_hom
• docs#homeomorph doesn't extend docs#continuous_map

Maybe your expectation comes from this set-theoretic idea of using bijections, rather than equivalences?

[Jireh Loreaux]

Yaël, that's not what I meant. I mean that I think of mul_equiv_class as mul_hom_class + equiv_like. I think of ring_equiv_class as mul_hom_class + add_equiv_class, etc. I do not think of them as extending the corresponding hom, only the hom which is the "right" one. I know that the pattern you described doesn't hold; hence my desire to redefine alg_equiv_class in the first place.

[Jireh Loreaux]

The point is: we only ever assume properties about the coe function, not the inv (aside from the fact that it's an inverse).

[Yaël Dillies]

Wrong: docs#homeomorph

[Jireh Loreaux]

aha, touché. That is the canonical example after all, I should have been more careful.

[Jireh Loreaux]

In any case, if people don't want it, then we just don't merge it. You're welcome to set up a poll if you wish.

[Frédéric Dupuis]

I don't follow the argument against this change. I can see this being not very useful and not worth the effort in the worst case, but since the work is already done, why not?

[Yaël Dillies]

As I said above, I already performed the analogous change in the opposite direction for other classes, like docs#boolean_algebra.

[Anne Baanen]

Perhaps the conclusion we should be drawing from this discussion is that the Hierarchy Builder people are onto something with their notion of Factory (which corresponds in Lean to something like the {..s} notation for defining a structure).

[Jireh Loreaux]

Sorry, I don't understand that comment. Can you elaborate?

[Anne Baanen]

The problem we're kind of running into here is that we have no good way to customize the relation between fun_likes and equiv_likes, because the built-in structure syntax { inv := inv, .. (by apply_instance : fun_like whatever) } doesn't work. Hierarchy Builder's factories by default work something like Lean's built-in structure syntax but can be overridden to do the right thing here.