Zulip Chat Archive

Stream: general

Topic: fug or beature?

Johan Commelin (Sep 19 2020 at 17:43):

variable (n : ℕ)

local notation `F` := fin n

variable {n}

lemma xyzzy : F = F := rfl

#check @xyzzy
-- xyzzy : ∀ (n : ℕ), fin n = fin n

Mario Carneiro (Sep 19 2020 at 17:48):

I am more surprised when this works than when it fails

Mario Carneiro (Sep 19 2020 at 17:48):

like what are you expecting to happen here?

Mario Carneiro (Sep 19 2020 at 17:49):

somehow you have to take an arbitrary expression and notice all the ways it could be interpreted as an instantiation of a local notation expression

Mario Carneiro (Sep 19 2020 at 17:49):

it seems like a pretty expensive prospect

Rob Lewis (Sep 19 2020 at 17:49):

I think the question is why n is explicit in xyzzy.

Mario Carneiro (Sep 19 2020 at 17:50):

aha, that opens up so many more questions

Mario Carneiro (Sep 19 2020 at 17:50):

like what does the n in the local notation refer to?

Mario Carneiro (Sep 19 2020 at 17:51):

local notations don't have a context

Johan Commelin (Sep 19 2020 at 18:16):

Shouldn't it just unfold the notation, and then do what it usually does?

Johan Commelin (Sep 19 2020 at 18:19):

We've been using this a lot in the Witt vector project. \bbW R is notation for witt_vector p R. You've fixed p once and forall, so you really don't want to be typing it all the time.

Johan Commelin (Sep 19 2020 at 18:19):

But then, for some lemmas, it is clear that you might want to vary the binding on p.

Kevin Buzzard (Sep 19 2020 at 18:33):

You can't use parameters to do the p thing?

Johan Commelin (Sep 19 2020 at 18:34):

parameters are a lean 3.4.2 thing right? As in, lean 3.5.* should help us move towards lean 4 which doesn't have parameters.

Kevin Buzzard (Sep 19 2020 at 18:41):

Have you talked to Sebastian about whether this will still be an issue in Lean 4?

Johan Commelin (Sep 19 2020 at 18:42):

Nope

Mario Carneiro (Sep 20 2020 at 03:17):

I think you shouldn't avoid using parameters if this is the only reason

Mario Carneiro (Sep 20 2020 at 03:17):

We will have the flexibility to work something out in lean 4

Mario Carneiro (Sep 20 2020 at 03:18):

if parameters continue to fill a useful role we should find a way to emulate them or get their principal benefits by other means

Last updated: Dec 20 2023 at 11:08 UTC