Zulip Chat Archive

Stream: general

Topic: notation for sets


Eric Rodriguez (Jul 27 2022 at 12:02):

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 (Jul 27 2022 at 15:51):

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 (Jul 27 2022 at 16:14):

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

Kyle Miller (Jul 27 2022 at 16:17):

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 (Jul 27 2022 at 16:19):

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 (Jul 27 2022 at 16:19):

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 (Jul 27 2022 at 16:23):

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

Eric Rodriguez (Jul 27 2022 at 16:25):

what are the rules?

Eric Wieser (Jul 27 2022 at 16:26):

show X, from x elaborates like @id X x

Eric Wieser (Jul 27 2022 at 16:27):

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

Eric Wieser (Jul 27 2022 at 16:27):

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

Eric Rodriguez (Jul 27 2022 at 16:29):

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 (Jul 27 2022 at 16:29):

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

Eric Wieser (Jul 27 2022 at 16:29):

The : X) is erased before typechecking happens

Eric Wieser (Jul 27 2022 at 16:30):

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

Eric Rodriguez (Jul 27 2022 at 16:30):

right I see

Eric Rodriguez (Jul 27 2022 at 16:30):

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

Eric Wieser (Jul 27 2022 at 16:33):

It's a macro

Eric Wieser (Jul 27 2022 at 16:33):

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 (Jul 27 2022 at 16:34):

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 (Jul 27 2022 at 16:51):

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.


Last updated: Dec 20 2023 at 11:08 UTC