Zulip Chat Archive

Stream: general

Topic: disable TC by some sigil


Johan Commelin (Apr 15 2021 at 06:38):

I know that Lean 4 is around the corner, so hacking on Lean 3 is of limited use. But I'm wondering, how hard would it be to add the following feature:
If foobar is some name, then @foobar makes all arguments explicit, but it still runs TC on the typeclass arguments.
Can we have something like @!foobar to disable TC (roughly by replacing all the TC arguments with (id _))?
This would be extremely useful when TC is for some reason unhelpful and you want type inference to do the job instead.

Johan Commelin (Apr 15 2021 at 06:38):

I'm mainly wondering: is this a < 20-line patch to Lean 3. Or more like a 2500-line patch?

Gabriel Ebner (Apr 15 2021 at 07:46):

It's about a 100-line change, but spread over several modules. You need to add the @! token, you need to add macro annotation to store it in the pre-expression, and finally you need to add support to the elaborator. I would start by searching for @@ and using the copy-and-paste development methodology.

Gabriel Ebner (Apr 15 2021 at 07:46):

But why can't you just use id _?

Johan Commelin (Apr 15 2021 at 07:47):

Because then I need to figure out whether it's underscore 7 and 12 or 6 and 11

Gabriel Ebner (Apr 15 2021 at 07:49):

I've always found that to be the easy part (just move over the underscores and check which one is a type class). The part that I dread is figuring out whether you need 12 or 13 underscores and if they come before or after the explicit arguments..

Johan Commelin (Apr 15 2021 at 07:50):

Right, and it it's all just underscores, then rw [@!foobar] is a lot easier and faster to write.

Johan Commelin (Apr 15 2021 at 07:51):

Because then you can omit 13 underscores to begin with

Johan Commelin (Apr 15 2021 at 07:54):

https://github.com/leanprover-community/lean-liquid/blob/master/src/breen_deligne/suitable.lean#L699-L715
It's more like 7 or 8 underscores, but you get the point.

Gabriel Ebner (Apr 15 2021 at 08:17):

Johan Commelin said:

Right, and it it's all just underscores, then rw [@!foobar] is a lot easier and faster to write.

Hmm, this doesn't work because @foobar and @!foobar elaborate to the same expression. (The difference only kicks in for @foobar _ _ _ _ _ _ _ and @!foobar _ _ _ _ _ _ _.)

Johan Commelin (Apr 15 2021 at 08:19):

Aha, so it would be a 2500-line patch to the elaborator?

Gabriel Ebner (Apr 15 2021 at 08:23):

It's more a question of "I don't know what you want it to do".

Johan Commelin (Apr 15 2021 at 08:28):

Well, I guess the elaborator could notice "hey, I see @!, let's insert (id _) for all TC arguments"

Gabriel Ebner (Apr 15 2021 at 08:30):

Can you be more concrete? What should #check @!add_comm output?

Gabriel Ebner (Apr 15 2021 at 08:31):

I believe in Lean 2 there was a sigil which turned all arguments implicit. Maybe that's what you're after (with disabling TC inference).

Johan Commelin (Apr 15 2021 at 08:32):

Aha, I see what you mean. Does the following make sense:

#check @add_comm
-- add_comm : ∀ {G : Type u_2} [_inst_1 : add_comm_semigroup G] (a b : G), a + b = b + a

#check @!add_comm
-- add_comm : ∀ {G : Type u_2} {_inst_1 : add_comm_semigroup G} (a b : G), a + b = b + a

Gabriel Ebner (Apr 15 2021 at 08:33):

That's hard. It would have to return something like id (∀ {G : Type u_2} {_inst_1 : add_comm_semigroup G} (a b : G), a+b=b+a) @add_comm

Johan Commelin (Apr 15 2021 at 08:35):

Hmm, I see.

Eric Wieser (Apr 15 2021 at 09:05):

Would this be easier with a tactic, by no_tc @lemma_name?

Jannis Limperg (Apr 15 2021 at 11:07):

I just hacked a tactic like this together on the notc branch: https://github.com/leanprover-community/mathlib/blob/notc/src/tactic/no_typeclasses.lean

Johan, would the test case at the bottom of that file work for you?

Jannis Limperg (Apr 17 2021 at 11:14):

Ping @Johan Commelin

Johan Commelin (Apr 17 2021 at 11:15):

@Jannis Limperg wow, I somehow missed your previous message. Thanks for the ping!

Johan Commelin (Apr 17 2021 at 11:15):

Let me look at that file

Jannis Limperg (Apr 17 2021 at 11:15):

No worries, I figured. :)

Johan Commelin (Apr 17 2021 at 11:16):

Can I now rw [by no_typeclasses @test]?

Johan Commelin (Apr 17 2021 at 11:16):

I guess that would just work, right?

Johan Commelin (Apr 17 2021 at 11:16):

(Assuming test is a bit more interesting)

Johan Commelin (Apr 17 2021 at 11:19):

I guess this could be combined with the machinery in https://github.com/leanprover-community/lean-liquid/blob/master/src/hacks_and_tricks/by_exactI_hack.lean to turn it into a sigil.

Jannis Limperg (Apr 17 2021 at 11:20):

It seems like the rw works. You get subgoals for α, testclass α and a : α if type inference doesn't figure them out.

Jannis Limperg (Apr 17 2021 at 11:22):

I can try to make this a user_notation as well (but probably not today).


Last updated: Aug 03 2023 at 10:10 UTC