Zulip Chat Archive

Stream: general

Topic: Can `unification_hint` help with casting?


view this post on Zulip Eric Wieser (Jan 05 2021 at 18:19):

If I have a (a : alternating_map R M N ι) and want to cast it to a multilinear_map, I seem to have no choice but to spell out (a : multilinear_map R (λ i : ι, M) N) which is a mouthful. Is there any way I can train the unifier to let me put underscores in there? Ideally I could write(a : multilinear_map _ _ _) and lean would work it out.

view this post on Zulip Kevin Buzzard (Jan 05 2021 at 18:22):

The problem I guess is that in theory there could be a coercion to some other multilinear map too

view this post on Zulip Kevin Buzzard (Jan 05 2021 at 18:22):

so is this what unification hints do?

view this post on Zulip Eric Wieser (Jan 05 2021 at 18:26):

In part this is me trying to answer the question "what do unification hints do"

view this post on Zulip Kevin Buzzard (Jan 05 2021 at 18:28):

I heard very early on in Lean 4 development that they weren't planning on having them so I never took them seriously. Now it turns out that they are there in Lean 4 too so perhaps it's time I figured out what they are.

view this post on Zulip Eric Wieser (Jan 05 2021 at 18:30):

I went back through the zulip history and found:

  • The tests in lean 3, which are completely contrived and seem mostly to be "these are a backdoor for irreducible", which probably is a useful trick to know
  • The lean-omin notes on them
  • That Lean Together 2019 workshop that I dropped the link to

view this post on Zulip Bryan Gin-ge Chen (Jan 05 2021 at 19:01):

If you figure them out (and they seem useful), please write something up for the community webpage!

view this post on Zulip Johan Commelin (Jan 06 2021 at 09:11):

@Kenny Lau see Eric's post for some pointers about unification hints. :up:

view this post on Zulip Cyril Cohen (Jan 07 2021 at 22:59):

There is actually a research paper about them: https://www.cs.unibo.it/~sacerdot/PAPERS/tphol09.pdf

view this post on Zulip Eric Wieser (Feb 17 2021 at 08:49):

Some more motivation for the original question - can unification hints make this legal?

import data.equiv.ring

-- fails without filling the underscores. Can we teach lean to guess?
example {M N : Type*} [semiring M] [semiring N] (f : M ≃+* N) := (f : _ →+* _)

Last updated: May 11 2021 at 22:14 UTC