## Stream: general

### Topic: mysteries of the lean 3 parser

#### Mario Carneiro (Jun 12 2021 at 08:56):

this exists:

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


#### Mario Carneiro (Jun 15 2021 at 08:48):

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


#### Mario Carneiro (Jun 15 2021 at 09:01):

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 (Jun 15 2021 at 09:08):

Whaaat?

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


#### Mario Carneiro (Jun 15 2021 at 09:50):

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 (Jun 16 2021 at 01:20):

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 (Jun 16 2021 at 02:27):

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 (Jun 16 2021 at 04:49):

I can't make sense of any of this

#### Mario Carneiro (Jun 16 2021 at 04:56):

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 (Jun 18 2021 at 02:33):

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


Apparently long form attributes accept multiple bracket lists...

#### Mario Carneiro (Jun 18 2021 at 02:34):

attribute def foo := 1


...or no bracket lists

#### Mario Carneiro (Jun 18 2021 at 04:09):

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 (Jun 18 2021 at 07:01):

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

#### Mario Carneiro (Jun 18 2021 at 18:06):

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 (Jun 18 2021 at 18:18):

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

#### Mario Carneiro (Jun 18 2021 at 18:24):

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 (Jun 18 2021 at 18:50):

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 (Jun 18 2021 at 18:53):

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 (Jun 18 2021 at 18:56):

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 (Jun 18 2021 at 19:02):

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

#### Eric Wieser (Jun 18 2021 at 19:05):

Do structure fields accept them?

nope

#### Bhavik Mehta (Jun 19 2021 at 18:56):

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 (Jun 19 2021 at 19:00):

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

#### Mario Carneiro (Jun 19 2021 at 19:00):

looking at it now that still seems like it should work

#### Mario Carneiro (Jun 19 2021 at 19:03):

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 (Jun 19 2021 at 19:04):

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 (Jun 21 2021 at 12:59):

(::) 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 (Jun 21 2021 at 13:01):

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 (Jun 21 2021 at 15:34):

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

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


#### Mario Carneiro (Jun 21 2021 at 17:04):

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 (Jun 21 2021 at 21:53):

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 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 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 (Jun 22 2021 at 04:49):

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

#### Eric Rodriguez (Jul 05 2021 at 23:48):

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 (Jul 05 2021 at 23:53):

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 (Jul 07 2021 at 05:07):

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 (Jul 07 2021 at 15:01):

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 (Jul 09 2021 at 03:46):

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 (Jul 21 2021 at 00:18):

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 (Jul 21 2021 at 01:40):

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

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


#### Mario Carneiro (Jul 23 2021 at 18:52):

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


local notations where you least expect them

#### Mario Carneiro (Jul 23 2021 at 18:56):

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


This one is probably a bit misleading...

#### Mario Carneiro (Jul 30 2021 at 00:04):

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 (Jul 30 2021 at 07:54):

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 (Jul 30 2021 at 13:34):

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 (Aug 03 2021 at 11:54):

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 (Aug 03 2021 at 11:54):

(the #eval failure is reposted here)

Last updated: Dec 20 2023 at 11:08 UTC