notation for sets

Stream: general

[Eric Rodriguez]

Often, when you write {x, y, z} as an argument, the typechecker goes insane unless you specify exactly what type they're meant to be; I wonder if this could be remedied with some notation {...}ₛ that specifically says it's a set? And maybe something similar for finset (I can't seem to find a subscript f, so maybe ᶠ would have to do?)

[Junyan Xu]

The code that parses these notations is in the C++ Lean code, not in mathlib, so I guess it's not that easy to add something custom. (It depends on has_insert/has_singleton/has_emptc instances.)

[Kyle Miller]

At least there's ({x, y, z} : set _), which generalizes.

[Kyle Miller]

I've thought it would be fun/useful to have the X, x as a synonym for (x : X), using the usual parsing rules for constructs with a comma. It saves needing to put a parenthesis way at the end of an expression.

[Eric Rodriguez]

Junyan Xu said:

The code that parses these notations is in the C++ Lean code, not in mathlib, so I guess it's not that easy to add something custom. (It depends on has_insert/has_singleton/has_emptc instances.)

oh, that's a shame, I thought there'd be recursive notation :/

[Eric Rodriguez]

Kyle Miller said:

I've thought it would be fun/useful to have the X, x as a synonym for (x : X), using the usual parsing rules for constructs with a comma. It saves needing to put a parenthesis way at the end of an expression.

isn't this what show X, from x is meant to be? Although I've noticed it sometimes gets stuck in proof terms

[Kyle Miller]

show has different elaboration rules, too. the would just be a synonym for a type ascription.

[Eric Rodriguez]

what are the rules?

[Eric Wieser]

show X, from x elaborates like @id X x

[Eric Wieser]

Which is to say, it produces a bona fide term of type X

[Eric Wieser]

(x : X) produces a term of whatever type x was elaborated to in the presence of the hint X

[Eric Rodriguez]

Eric Wieser said:

(x : X) produces a term of whatever type x was elaborated to in the presence of the hint X

I'm confused how this is different - or can (x : X) typecheck to another type?

[Eric Wieser]

variables {α : Type*} (a : α)
#check (a : αᵃᵒᵖ)
#check (show αᵃᵒᵖ, from a)

[Eric Wieser]

The : X) is erased before typechecking happens

[Eric Wieser]

It's only there to provide a hint while elaborating the things inside the brackets

[Eric Rodriguez]

right I see

[Eric Rodriguez]

how come show isn't just notation for @id then?

[Eric Wieser]

It's a macro

[Eric Wieser]

run_cmd do
  e ← tactic.to_expr ``(show unitᵃᵒᵖ, from unit.star),
  tactic.trace e.to_raw_fmt

 [macro annotation
  (app
    (lam this default
      (app (const add_opposite [0]) (const unit []))
      (var 0))
    (const unit.star []))]

[Kyle Miller]

Found precisely how show parses: https://github.com/leanprover-community/lean/blob/bf12a6c9b74846b532a248617eae692d2c13f18b/src/frontends/lean/builtin_exprs.cpp#L516

show X, from x is exactly (λ (this : X), this) x, and then it's given the show annotation (a macro, like Eric said). There's some code, for example in the pretty printer, that prevents beta reduction, and the pretty printer recognizes this annotation and prints it back out as a show.

[Kyle Miller]

Type ascriptions are also macros. Here's where they're elaborated: https://github.com/leanprover-community/lean/blob/bf12a6c9b74846b532a248617eae692d2c13f18b/src/frontends/lean/elaborator.cpp#L830

(x : X) elaborates in the following way:

1. elaborate X without any expected type.
2. ensure that X is a type, inserting a has_coe_to_sort coercion if necessary.
3. try to synthesize any pending type class instances.
4. elaborate x with the elaborated X as the expected type.
5. letting X' be the type of the elaborated x, check to see if X is defeq to X'. If so, we're done elaborating. If not, we try to insert a coercion from X' to X.

(Expected types during elaboration are, as far as I understand, just suggestions to help direct the elaborator.)

One consequence is that it's happy with X' and X being defeq, but sometimes (like for typeclasses) you want to control X' syntactically. The (id x : X) trick is supposed to cause x to syntactically have X as its type. I guess show X, from x should be similar, but it uses function argument elaboration rules instead.