Zulip Chat Archive

Stream: general

Topic: add a new superclass, need some new @s


view this post on Zulip Scott Morrison (Mar 22 2021 at 01:33):

We've currently got three PRs open where someone has added a new super-class to an existing class, and then in unexpected places they've need to write an extra @ to get a lemma to fire.

These are at

Could we get e.g. @Mario Carneiro, @Gabriel Ebner, or @Rob Lewis to help diagnose?

view this post on Zulip Riccardo Brasca (Mar 22 2021 at 09:19):

The same happened to me here https://github.com/leanprover-community/mathlib/pull/6746

view this post on Zulip Anne Baanen (Mar 22 2021 at 13:46):

For #6786 it looks like there is a subproblem with a diamond (semiring -> monoid_with_zero -> has_zero and semiring -> non_unital_non_assoc_semiring -> has_zero) that the elaborator needs to do a lot of work on. Somehow it doesn't use the rest of the expression to infer missing metavariables, instead choosing nat as a default value. I think the problem has turned from first-order to higher-order unification, and that higher-order unification makes some unfortunate choices here.

view this post on Zulip Kevin Buzzard (Mar 22 2021 at 13:52):

Could there be a cheap fix involving lowering or raising a priority?

view this post on Zulip Anne Baanen (Mar 22 2021 at 13:55):

I expect that changing priorities would fix one half of usages and break the other half. It might well be possible that the fixed half is exactly the lemmas that are in mathlib now, and the broken half the ones that are added later.

view this post on Zulip Kevin Buzzard (Mar 22 2021 at 13:55):

Unification hints?

view this post on Zulip Gabriel Ebner (Mar 22 2021 at 14:22):

I also think that there's a problematic diamond at play here. But the issue is not related to higher-order unification, it is plain old first-order unification:

view this post on Zulip Gabriel Ebner (Mar 22 2021 at 14:22):

The first example in that PR requires unifying 0 and 0, which is obviously hard.

view this post on Zulip Gabriel Ebner (Mar 22 2021 at 14:24):

It's hard because these two come from the two edges of the diamond. Essentially (skipping a few intermediate type classes):

@has_zero.zero ?m_1 (field.to_has_zero ?m_2) =?= @has_zero.zero ?m_1 (monoid_with_zero.to_has_zero ?m_3)

view this post on Zulip Gabriel Ebner (Mar 22 2021 at 14:26):

The problem is that Lean needs to assign ?m_2 : field ?m_1 or ?m_3 : monoid_with_zero ?m_1.
But there is no obvious choice for ?m_2 or ?m_3. Or at least none that Lean could find by unfolding field.to_has_zero.

view this post on Zulip Gabriel Ebner (Mar 22 2021 at 14:43):

Kevin Buzzard said:

Unification hints?

@[unify]
def unif_hint {α : Type} [i : monoid_with_zero α] [j : semiring α] : unification_hint :=
{ pattern := non_unital_non_assoc_semiring.to_mul_zero_class α 
    @monoid_with_zero.to_mul_zero_class α i,
  constraints := [semiring.to_monoid_with_zero α  i] }

view this post on Zulip Gabriel Ebner (Mar 22 2021 at 14:44):

Unfortunately, unification hints are pretty broken in Lean 3. For example, the hint above doesn't work if you replace Type by Type*...

view this post on Zulip Eric Wieser (Mar 22 2021 at 14:53):

That probably explains why I've never had any luck doing anything with a unification hint, as Type* is muscle memory at this point.

view this post on Zulip Gabriel Ebner (Mar 22 2021 at 14:55):

AFAICT the Lean 4 unification hints have exactly the same bug. I'm trying it out now.

view this post on Zulip Gabriel Ebner (Mar 22 2021 at 15:47):

I can't reconstruct this issue in Lean 4. Mostly because Lean 4 will completely refuse to elaborate terms if it can't synthesize all instance arguments. For example, you just can't use cases le_or_gt _ _ in Lean 4.

view this post on Zulip Oliver Nash (Mar 22 2021 at 17:53):

Thanks @Gabriel Ebner for the explanation (which I have yet to digest) and especially for adding this commit while I was tied up with other things. You saved me a lot of time :-)

view this post on Zulip Riccardo Brasca (Mar 23 2021 at 12:35):

Something interesting happen in one of my PR, see https://github.com/leanprover-community/mathlib/pull/6831#discussion_r599508067

If you don't want to look at the two PR here is what happened: in #6746 I introduced semi_normed_group, and several lemmas stopped working. The solution was almost always to use some extra @. The PR got bigger and bigger, so I decided to split it, and in #6831 I generalized Lipschitz maps for pseudo_emetric_space (this was part of the other PR). Now, some of the problems appeared also in this PR (this is already interesting, since I thought they come from the new class semi_normed_group, while they come from Lipschitz maps). Even more interesting, a new problem appeared (of the same nature), the one in the above comment. Now, I know that it will disappear when everything is generalized to semi_normed_group, so I now think that also the other ones will go away if everything is stated in the correct generality.


Last updated: May 06 2021 at 21:09 UTC