Mathlib.Tactic.Lift steals the token `to`

Stream: mathlib4

[Kim Morrison]

import Mathlib.Tactic.Lift

structure Foo where
  to : Unit

produces

unexpected token 'to'; expected command

Is someone able to fix this for us? Or have we just decided that to is not an acceptable field name if using Mathlib?

[Andrew Yang]

syntax (name := lift) "lift " term " to " term (" using " term)?
  (" with " ident (ppSpace colGt ident)? (ppSpace colGt ident)?)? : tactic

structure Foo where
  to : Unit

This is the culprit but why does a syntax in the tactic category trigger here?

[Edward van de Meent]

Personally I think both. imo to seem very non-descriptive as a name, but I imagine that downstream projects should have freedom to do whatever they want, so the tactic shouldn't reserve it

[Alex Meiburg]

It would be a very reasonable name in a pair ti / to, i.e. a collection of "t in" and "t out" - $t_{i}$ and $t_{o}$ are definitely something I've seen in plenty of papers. (Granted they could be tᵢ and tₒ.)

[Edward van de Meent]

(did you mean to post this somewhere else?)

[Ruben Van de Velde]

No, it's relevant to naming things to (or t\_o)

[Eric Wieser]

&" to " fixes this

[Damiano Testa]

I am in favour of adding &. In general, forbidding two letter identifiers seems like it should be avoided.

[Yury G. Kudryashov]

What does & do?

[Aaron Liu]

It makes the token not reserved

[Aaron Liu]

@loogle "nonreserved"

[loogle]

:search: Lean.ParserDescr.nonReservedSymbol, Lean.ParserDescr.nonReservedSymbol.sizeOf_spec, and 13 more

[Kim Morrison]

Eric Wieser said:

&" to " fixes this

Sorry, I should have said in my original message that this doesn't work: we get lots of "unexpected token" errors when setting up the elab_rules. (I didn't diagnose any further.)

[Eric Wieser]

I tried it with Andrew's mwe and it seemed to work

[Robin Arnez]

It doesn't work:

syntax (name := lift) "lift " term &" to " term (" using " term)?
  (" with " ident (ppSpace colGt ident)? (ppSpace colGt ident)?)? : tactic

example : True := by
  lift 3 to 3 -- parses `to` as a name instead of a keyword

[Eric Wieser]

syntax (name := lift) "lift " term:arg &" to " term (" using " term)? works

[Eric Wieser]

But I guess breaks lift f a to

[Robin Arnez]

Yeah but it comes at a cost:

syntax (name := lift) "lift " term:arg &" to " term (" using " term)?
  (" with " ident (ppSpace colGt ident)? (ppSpace colGt ident)?)? : tactic

example : True := by
  lift 1 + 5 to 3 -- invalid token "+", expected "to"

[Robin Arnez]

Yeah right

[Robin Arnez]

Yeah, right so is it possible to have

structure Foo where
  to : Unit

example : True := by
  lift f a to 3

Hmm...

[Robin Arnez]

Okay this seems to work:

import Lean.Parser

open Lean Parser

@[inline]
def Lean.Parser.ParserContext.mk (core : ParserContextCore) : ParserContext := by
  constructor
  assumption

def withKeyword (tk : String) : Parser → Parser := withFn fun f c s =>
  let c' : ParserContext := .mk { c with tokens := c.tokens.insert tk tk }
  f c' s

def termWithTo : Parser := leading_parser withKeyword "to" (categoryParser `term 0)

syntax (name := lift) "lift " termWithTo &" to " term (" using " term)?
  (" with " ident (ppSpace colGt ident)? (ppSpace colGt ident)?)? : tactic

structure Foo where
  to : Unit

example : True := by
  lift f a to 3

[Eric Wieser]

That fails on lift (fun to => to) a to 3

[Eric Wieser]

But that's better than the status quo!

[Kevin Buzzard]

Eric Wieser said:

That fails on lift (fun to => to) a to 3

Anyone who tries that deserves pain anyway :-)

[Mario Carneiro]

Kim Morrison said:

import Mathlib.Tactic.Lift

structure Foo where
  to : Unit

produces

unexpected token 'to'; expected command

Is someone able to fix this for us? Or have we just decided that to is not an acceptable field name if using Mathlib?

I recall this being a major point of discussion when lift was first added with this keyword. Yes, this is making to into a keyword and this means it can't be used in field names unless you use guillemets, just as you can't use with and as as variable names

[Mario Carneiro]

Because of the way it is used, you can't use &"to" here

[Mario Carneiro]

that trick doesn't always work or else there would be no need for keywords in the first place

[Mario Carneiro]

(certainly I have wanted to use as as a name on many occasions, e.g. in list functions with a and as)

[Ruben Van de Velde]

Can we do lift x → X?

[Mario Carneiro]

no, -> is already valid in expression position, it means a function type

[Eric Wieser]

lift x : X could work?

[Edward van de Meent]

we could do lift X from x, i think?

[Mario Carneiro]

I'm just not sure why we are resurrecting this conversation

[Mario Carneiro]

we had a poll and everything IIRC, we decided at the time to go with making this into a keyword

[Mario Carneiro]

it's a very short english preposition, arguably not that different from as, from, with, using

[Mario Carneiro]

and it is nice to not have to contort grammar in tactics using an extremely short lexicon of prepositions

[Aaron Liu]

The nonReservedSymbol parser seems to take an additional includeIdent argument, would setting that to true help here?

[Robin Arnez]

The problem is not the "to" but the term before it parsing more than it should, so that shouldn't help.

[Robin Arnez]

Also, as is not a keyword I don't think..?

[Mario Carneiro]

you're right, maybe I got confused with ML where as is a keyword. at is also a keyword in lean