mysteries of the lean 3 parser

Stream: general

[Mario Carneiro]

this exists:

#reduce [whnf] 2 -- (1.add 0).succ

[Mario Carneiro]

infix f:1 := (=) -- ok
infix f := (=) -- ok
infix + := (=) -- ok
infix +:1 := (=) -- parse fail

[Mario Carneiro]

Oh boy, notations have a lot of easter eggs. This exists:

notation `foo`:50 x:prev := x
#print notation foo
-- `foo`:50 _:50 := #0

I guess it's useful?

[Mario Carneiro]

Whaaat?

notation 42 := false
#eval if 42 then 1 else 0

[Mario Carneiro]

Oh, a segfault. Haven't seen one of those in a while.

def F := 0
notation `foo` binders:2 := F
#check foo (x y : ℕ)

(note: I have no idea what I'm doing here)

[Mario Carneiro]

well this is fun:

def foo {α β} (a : α) (b : β) := true
notation `Λ` binders `, ` b:scoped ` :Λ` binders `, ` c:scoped := foo b c

#check Λ x:ℕ, x < 2 :Λ y, y < 2
-- Λ (x y : ℕ), x < 2 :Λ (x y : ℕ), y < 2 : Prop
#check Λ (x y : ℕ), x < 2 :Λ (x y : ℕ), y < 2
-- Λ (x y x y : ℕ), x < 2 :Λ (x y x y : ℕ), y < 2 : Prop
#check Λ (x y x y : ℕ), x < 2 :Λ (x y x y : ℕ), y < 2
-- Λ (x y x y x y x y : ℕ), x < 2 :Λ (x y x y x y x y : ℕ), y < 2 : Prop

[Mario Carneiro]

pretty sure this is a bug:

universes u v
def foo : unit := ()
def unit.bla (u : unit) := ()

set_option pp.all true
#check foo.bla.bla.bla.{u v}.{u v v+1}.{42}

[Johan Commelin]

I can't make sense of any of this

[Mario Carneiro]

This is all white box testing BTW. I've been reading the parser code and every time I see something odd I try to make a test case. In this case, the problem is that lean has a fallback approach to disambiguating a namespaced name like nat.add from a projection on a constant like list.nil.tail, and every time the fallback is called it parses a level list, possibly discarding the one from the previous iteration. As a result, you can get this weird behavior where you can stick multiple level lists on a multi-fallback name expression, and they will be parsed but the level list itself is discarded

[Mario Carneiro]

attribute [intro] [simp] def foo := 1

Apparently long form attributes accept multiple bracket lists...

[Mario Carneiro]

attribute def foo := 1

...or no bracket lists

[Mario Carneiro]

private local attribute protected def foo := 1

apparently local attribute can have modifiers, and can also be a modifier on another declaration. So you can use this to make otherwise impossible definitions like a private protected def, which amusingly can't be referred to because it has a crazy namespace and also can't be referenced except through that namespace

[Jesse Michael Han]

"i have discovered a truly marvelous proof of this, which, however, is a private local attribute protected theorem"

[Mario Carneiro]

set_option old_structure_cmd true
structure bar := (x : nat)
structure foo extends private to_bar' : bar renaming x -> y := (x : nat)

I don't think all of these features are simultaneously useful, but extends has a few seldom used knobs:

• For a class, the parent coercion will be marked @[instance], unless private is set
• to_bar' : bar instead of just bar allows you to change the name of the parent coercion field. It seems to be ignored if old_structure_cmd is set
• renaming x -> y lets you rename fields that are being splatted into the structure when old_structure_cmd is set

[Eric Wieser]

That private sounds like it might be useful for making the canonical parent projection be coe by hiding the real one completely

[Mario Carneiro]

Despite the name, it doesn't actually make anything private in the sense of a private def. It only removes the @[instance] attribute on the parent projection

[Mario Carneiro]

You might know that structure allows defining local notations as additional fields, which can be used in later fields. But did you know that inductive also supports local notations? Here is the syntax:

inductive prov : ℕ → ℕ → Prop
infix `⊢`:50 := prov
| le {a b : ℕ} : a ≤ b → a ⊢ b

mutual inductive prov', defeq
infix `⊢`:50 := prov'

with prov' : ℕ → ℕ → Prop
| le {a b : ℕ} : a ≤ b → a ⊢ b

with defeq : ℕ → ℕ → Prop
| eq {a b : ℕ} : a = b → defeq a b

Unfortunately, it only supports one notation command, so make it count.

[Marc Huisinga]

Mario Carneiro said:

You might know that structure allows defining local notations as additional fields, which can be used in later fields. But did you know that inductive also supports local notations? Here is the syntax:

inductive prov : ℕ → ℕ → Prop
infix `⊢`:50 := prov
| le {a b : ℕ} : a ≤ b → a ⊢ b

mutual inductive prov', defeq
infix `⊢`:50 := prov'

with prov' : ℕ → ℕ → Prop
| le {a b : ℕ} : a ≤ b → a ⊢ b

with defeq : ℕ → ℕ → Prop
| eq {a b : ℕ} : a = b → defeq a b

Unfortunately, it only supports one notation command, so make it count.

I used this for my BSc thesis. Very handy when defining large inductives :)

[Mario Carneiro]

Inductive constructors accept doc strings:

/-- This documents foo -/
inductive foo : ℕ → Prop
/-- This documents foo.zero -/
| zero : foo 0
/-- This documents foo.one -/
| one : foo 1

[Yaël Dillies]

We actually get doc blames in nolint.txt for not providing those!

[Eric Wieser]

Do structure fields accept them?

[Mario Carneiro]

nope

[Bhavik Mehta]

I'm not sure if this counts as the same sort of lean 3 parser mystery, but I came across:

constant foo : Type
constant foo.bar : foo → Prop

variables (X : foo)
variable [X.bar] -- works
variables [X.bar] -- fails

which surprised me: it means we can't do

variables (X : foo) [X.bar]

as well

[Mario Carneiro]

oh, good catch, I didn't notice that when looking at the code

[Mario Carneiro]

looking at it now that still seems like it should work

[Mario Carneiro]

Oh, I see, it parses X.bar as a name, sees a ] and decides this must be a variable binder update even though it hasn't resolved the variable yet

[Mario Carneiro]

The variable command has an exception for this because it came up in the past wrt variable [io.interface], but the fix was not propagated to variables as well

[Mario Carneiro]

(::) is a token, probably because of the (: ... :) pattern notation, even though it doesn't have any special meaning beyond the usual interpretation as a section of the list.cons function. However the implementation is a bit different, and so adding whitespace to break the token changes the result slightly:

#check ( < )  -- has_lt.lt : ?M_1 → ?M_1 → Prop
#check (<)    -- has_lt.lt : ?M_1 → ?M_1 → Prop

#check ( :: ) -- list.cons : ?M_1 → list ?M_1 → list ?M_1
#check (::)   -- λ (_x : ?M_1) (_y : list ?M_1), _x :: _y : ?M_1 → list ?M_1 → list ?M_1

[Mario Carneiro]

However, because this override is specific to ::, other notations beginning with : don't get the same treatment, and the (: can end up breaking them:

def foo := nat.lt
infix `:>`:50 := foo

#check ( :> ) -- foo : ℕ → ℕ → Prop
#check (:>) -- invalid expression

[Mario Carneiro]

Apparently you can write set comprehensions using either ∈ or in:

#check {x in (∅ : set ℕ) | true}
-- {x ∈ ∅ | true} : set ℕ

[Mario Carneiro]

You might know that you can change tactic classes using begin [class] tacs, ... end. But this also works in the middle of a tactic proof, if you put the class after a { ... }:

example : true :=
begin
  skip, -- this is a tactic
  { [smt]
    eblast }, -- this is a smt_tactic
end

[Mario Carneiro]

It turns out #print is a bit more featureful than you might be aware. Also #help exists

#print "hello world" -- prints "hello world"; only works with string literals
#print raw (1 + by skip) -- prints pexprs without elaboration
#print options -- print lean command line options
#print trust -- print trust level (0 = most paranoid)
-- #print key_equivalences -- crash lean
#print nat.add -- prints the definition of nat.add
#print definition nat.add -- prints nat.add for people who like to spell out "definition"
#print instances inhabited -- prints all instances of inhabited typeclass
#print classes -- prints all typeclasses
#print attributes -- prints all attributes
#print prefix nat.add -- prints all definitions starting with nat.add
#print aliases -- prints all aliases, created by "export" command
#print axioms -- prints all axioms in the current environment (there are more than 3 things in this list)
#print axioms classical.em -- prints all axioms used by a given theorem
#print fields group -- prints all fields in a structure
#print notation -- prints all notation
#print notation , -> -- prints all notation using the tokens `,` or `->`
#print inductive nat -- same as `#print nat` but only works for inductives
#print [ext] -- print all declarations marked `@[ext]`
#print [recursor] nat.rec -- print diagnostics for a recursor
#print [unify] -- print all unification hints
#print [simp] functor_norm -- print all simp lemmas in the functor_norm simp set? it doesn't work
#print [congr] functor_norm -- congr lemmas are apparently also related to the simp sets; also doesn't work
#print < -- Same as `#print notation <`

#help -- help help
#help options -- print `set_option` options and descriptions
#help commands -- print all commands

[Johan Commelin]

I think that long ago, I knew about #help.

[Eric Rodriguez]

notation `/--'`x := 55 * x

example : (110:ℕ) = /--'2 := rfl

/--' testing -/

so as it turns out you can override comment notation... the example complies, the block comment there doesn't work

[Eric Rodriguez]

even more amazlingly, you can do it with the close-comment block and seemingly get no issues:

notation `-/` := 55

example : (55:ℕ) = -/ := rfl

/- testing -/

example : true := by trivial

the syntax highlighter even deals with it (!)

[Mario Carneiro]

Apparently you can put negative attributes on a definition, although it's hard to come up with an example where this makes a difference.

local attribute [-simp] def foo := 1
-- cannot remove attribute [simp]: no prior declaration on foo

local attribute [simp] def bar := 1
#print bar -- @[_simp_cache, simp] def bar : ℕ := 1

local attribute [simp, -simp] def baz := 1
#print baz -- @[_simp_cache] def baz : ℕ := 1

[Bhavik Mehta]

So that last example adds baz to the simp cache but doesn't mark it as simp? Does this relate to the C++ implementation of simp?

[Mario Carneiro]

example : ℕ → ℕ :=
λ (notation `foo`:20 := 1) a, foo -- works

example : ℕ → ℕ :=
λ (notation `foo`:20 := 1), λ a, foo -- fails because the first lambda looks 0-ary to lean

[Mario Carneiro]

Having observed that the lean grammar can contain commands inside string literals inside expressions inside commands, I had to play with that, and it turns out that things are a little weirder than you might expect:

import tactic

meta def tactic.interactive.emit_code (_ : interactive.parse (do
  s ← lean.parser.pexpr,
  s ← tactic.to_expr s,
  s ← tactic.eval_expr string s,
  lean.parser.emit_code_here s)) : tactic unit :=
tactic.triv

namespace foo

example : true := by emit_code "
  #where -- we are in namespace foo

  -- example foo : true := trivial  -- fails
  example := by triv                -- this works though
  #check true                       -- true : _
  #check by exact true              -- true : Prop

  example := by emit_code \"
    #print \\\"inception\\\"
    -- end foo -- uncomment this to get a segfault
  \"

  end foo
"

end foo -- fails, closed namespace foo already

[Mario Carneiro]

here's another fun variation, a command parsing quine:

def foo := "example := by emit_code foo"
example := by emit_code foo

[Mario Carneiro]

example : ℕ → ℕ → ℕ → true :=
begin
  assume (notation `foo`:20 := ℕ) (x y z : foo),
  trivial
end

local notations where you least expect them

[Mario Carneiro]

example : ∀ x < 3, true :=
begin
  assume x < 3,
  trivial
end

This one is probably a bit misleading...

[Mario Carneiro]

bound variable capture in binder collections:

example : (∀ x y < 5, x < 6) = (∀ (x y : ℕ), x < 5 → y < 5 → x < 6) := rfl
example : (∀ x x < 5, x < 6) = (∀ (x y : ℕ), y < 5 → y < 5 → y < 6) := rfl
example : (∀ _ _ < 5, _x < 6) = (∀ (x y : ℕ), y < 5 → y < 5 → y < 6) := rfl

[Gabriel Ebner]

I'm more surprised that x y < 5 bounds both x and y. Why do we learn about all these cool features only now?

[Bhavik Mehta]

I thought this was already used in mathlib, especially with set membership (in fact I thought I saw code from you yourself Gabriel using this feature!)

[Eric Wieser]

Notation captures field notation without resolving it to a symbol name until the notation is used:

notation a `+'` b := a.foo + b.foo

def X := unit
def Y := unit

def X.foo (x : X) : nat := 1
def Y.foo (y : Y) : int := 2

variables (x : X) (y : Y)

#check x +' x  -- int
#check y +' y  -- nat
#eval (x +' x)  -- cannot evaluate function: 0 arguments given but expected 1
#eval (y +' y)  -- cannot evaluate function: 0 arguments given but expected 1

[Eric Wieser]

(the #eval failure is reposted here)