Zulip Chat Archive

Stream: general

Topic: notation

Reid Barton (Feb 28 2018 at 15:41):

Does anyone have a suggestion for Lean-friendly notation corresponding to TeX ff_* and ff^*?
(Meaning whatever you want them to mean, but for example, post- and pre-composition with the morphism ff.)

Reid Barton (Feb 28 2018 at 15:42):

Apparently there are no Unicode subscript or superscript asterisk characters

Reid Barton (Feb 28 2018 at 16:17):

f^* works okay for ff^*, but f_* isn't as nice because f_ parses as a single identifier, so it needs a space.

Andrew Ashworth (Feb 28 2018 at 17:04):

you could cheat and use _, which is not _

Sebastian Ullrich (Feb 28 2018 at 17:07):

Or use one of the up/down arrows

Kevin Buzzard (Feb 08 2020 at 15:47):

Any mathematician : "Let RR be a ring and let AA and BB be RR-algebras. Then...". Lean: {R : Type*} [comm_ring R] {A : Type*} [comm_ring A] {B : Type*} [comm_ring B] [algebra R A] [algebra R B]. Can we somehow make this Lean code look less scary to mathematicians? Of course RR is a type, that's why it's called RR. I wouldn't write "let xx be a ring", that would be madness!

Jason Rute (Feb 08 2020 at 16:14):

I'm not saying Lean should do this, but in Scala this thing with type classes comes up often and they have created a separate notation for it.
Assume Ring is a type class in Scala with a field add and that + knows to look at add in rings to implement addition. Then one can write the following verbose definition in Scala.

def double[R](x: R)(implicit ringOfR: Ring[R]) = x + x

Notice that in Scala [R] is a type parameter, (x:R) is a regular parameter, and (implicit ringOfR: Ring[R]) is an implicit parameter (very similar to Lean's type class parameters).

One can also instead use the following shorthand type class notation where we "treat" R as if it is an element of Ring:

def double[R: Rign](x: R) = x + x

Now, this notation might be less ambiguous in Scala than in Lean, since Scala treats type parameters and regular parameters differently with different notation (i.e. Scala is not dependently typed).

A similar issue exists with sets in Lean. (A type class is to Types as sets are to Props.) We can write the convenient notation

example (s : set ) :  a  s, a = a := sorry

But if we apply intro twice we get the messy notation

example (s : set ) (a : ) (H : a  s) : a = a := sorry

One could imagine an alternative notation where one writes

example (s : set ) (a  s) : a = a := sorry

I'm not claiming the Lean notation should change, but it is food for thought...

Rob Lewis (Feb 08 2020 at 16:25):

One could imagine an alternative notation where one writes

example (s : set ) (a  s) : a = a := sorry

This actually works exactly as you wrote it. I've never been sure if it's intentional or a "feature" enabled by the bounded quantifier syntax. Given that the a ∈ s hypothesis gets the default name H, I don't think it's something we should encourage in mathlib.

Mario Carneiro (Feb 08 2020 at 16:25):

Here's the relevant lean 3 issue: https://github.com/leanprover/lean/issues/1522

Mario Carneiro (Feb 08 2020 at 16:26):

which would have allowed us to write just [algebra R A] [algebra R B]

Reid Barton (Feb 08 2020 at 19:46):

Bundling helps somewhat, e.g., {R : CommRing} etc., though it's tricky in algebra since you typically have a lot of different levels of structure floating around

Johan Commelin (Feb 15 2021 at 12:45):

How does Lean decide whether it will use my local notation for pretty printing in the goal state?

Johan Commelin (Feb 15 2021 at 12:46):

I currently have

variables (C : system_of_complexes)

/-- `C.d` is the differential `C c i ⟶ C c (i+1)` for a system of complexes `C`. -/
def differential (c : 0) (i j : ) (hij : i + 1 = j) :
  C c i  C c j :=
(C.obj $ op c).d i  congr_hom _ rfl hij

local notation `d` := differential _ _ _ _ (by int_magic)

Johan Commelin (Feb 15 2021 at 12:46):

Here int_magic is a custom tactic that shouldn't be relevant (maybe it is?!)

Johan Commelin (Feb 15 2021 at 12:47):

I can succesfully use d when entering statements, but Lean doesn't use d in the goal window.

Gabriel Ebner (Feb 15 2021 at 12:59):

The Lean 3 pretty-printer is not particularly clever, it tries to syntactically match the notation. In your case it looks for a by int_magic in the goal state.

Johan Commelin (Feb 15 2021 at 13:03):

Ok, so this will never work :sad:

Gabriel Ebner (Feb 15 2021 at 13:04):

You could use auto params.

Johan Commelin (Feb 15 2021 at 13:15):

Except that those don't play well with bundled functions...

Johan Commelin (Feb 15 2021 at 13:15):

Probably the best investment of my time is porting mathlib to Lean4

Johan Commelin (Feb 15 2021 at 13:16):

That will solve these issues in a more principled way :laughing:

Last updated: Aug 03 2023 at 10:10 UTC