Lean 4 notation

Stream: general

[Sebastian Ullrich]

That notation would introduce ambiguity with the singleton set notation

[Anne Baanen]

Would the notation {p * q * p\-1 * q\-1 | p q : α} work?

[Kevin Buzzard]

I would be equally happy with this, because that is another notation which is completely acceptable to mathematicians -- it's clear to read.

[Anne Baanen]

It would require some C++ hacking though, apparenly binders cannot appear after the things they bind

[Sebastian Ullrich]

No problem in Lean 4

[Kevin Buzzard]

Another notation question, this time where Lean is being too good:

-- Let G be a group
variables (G : Type u) [group G]
-- A mathematician:
-- "The Abelianization *of G* is the quotient blah blah blah"
-- Works in Lean 3:
def abelianization : Type u :=
quotient_group.quotient (commutator G)
-- Can't get it to work (maybe I'm bad at variables?)
def abelianization (G) : Type u :=
quotient_group.quotient (commutator G)

[Kenny Lau]

your (G) overrides the G outside

[Kenny Lau]

so there is no group instance

[Kevin Buzzard]

I think that when a mathematician says "let G be a group" they still want access to the notation "a subgroup of G is ..." when making definitions like subgroup, rather than having the reader having to figure out that we're talking about a subgroup of a group as opposed to of a foo.

[Anne Baanen]

Anne Baanen said:

It would require some C++ hacking though, apparenly binders cannot appear after the things they bind

It's a giant mess and broken in many places, but I made syntax for set replacement notation work:

def successors : set nat := {(x + 1) | x}
lemma successors_correct : successors = {x | ∃ y, y + 1 = x} := rfl

I chose to require parentheses around the expression to avoid backtracking and possibly ambiguity. It parses the expression before the binder, so Lean will do ugly things if x is a definition somewhere else.

[Anne Baanen]

Do we actually want this right now, or wait for :four_leaf_clover:?

[Johan Commelin]

I wouldn't classify it as high priority :wink:

[Mario Carneiro]

does {(x + 1) | x < 0} work? :P

[Anne Baanen]

Not yet! Even {(x + 1) | x : nat} doesn't work yet. I'm trying to figure out whether I can get the parser to go back to parsing the expression after it has finished with the binders.

[Kevin Buzzard]

I don't need it. I am preparing a performance, not writing code. I can say "I have been told by experts that we will be able to write it in this more familiar way in Lean 4".

[Anne Baanen]

Aha: we can parse every variable as being in the local scope, then use patexpr_to_expr to update the references.

[Anne Baanen]

After applying patexpr_to_expr, the rest was not too difficult:

def between_1_and_5 : set nat := {(x + 1) | x < 5}
lemma between_1_and_5_correct : between_1_and_5 = {y | ∃ (x : nat) (h : x < 5), x + 1 = y} := rfl

[Sebastian Ullrich]

And here is the corresponding Lean 4 implementation (in two lines, after reimplementing the existing Lean 3 notations):

new_frontend

declare_syntax_cat quantifierBinder
syntax ident* (" : " term)? : quantifierBinder
syntax ident " < " term : quantifierBinder

syntax "∃" quantifierBinder ", " term : term
macro_rules
| `(∃ $xs:ident* : $τ, $P) => xs.foldrM (fun x P => `(Exists (fun ($x : $τ) => $P))) P
| `(∃ $xs:ident*, $P)      => `(∃ $xs:ident* : _, $P)
| `(∃ $x:ident < $e, $P)   => `(∃ $x:ident, $x:ident < $e ∧ $P)

axiom Set : Type → Type
axiom Set.sep {α : Type} (p : α → Prop) (s : Set α) : Set α
axiom Set.univ {α : Type} : Set α
macro "{" x:ident " | " p:term "}" : term =>
`(Set.sep (fun $x => $p) Set.univ)

macro "{" e:term " | " b:quantifierBinder "}" : term =>
`({y | ∃ $b, y = $e })

#check {a | a ≠ a}
#check {a * b | a b : Nat}
#check ({a * b | a b} : Set Nat)
#check {a | a < 10}  -- ambiguous
#check {2 * a | a < 10}

{a * b | a b} without a type ascription looks pretty strange and probably shouldn't be allowed. The other interesting one is {a | a < 10}, which can be read either way (filtering all a by a predicate vs. selecting a for all a < 10) and thus is ambiguous. Not sure there is a good solution for that except for merging both notations into a single one that first tries one interpretation, then the other one.

[Anne Baanen]

Created PR lean#402.