notation

Stream: general

[Reid Barton]

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

[Reid Barton]

Apparently there are no Unicode subscript or superscript asterisk characters

[Reid Barton]

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

[Andrew Ashworth]

you could cheat and use ＿, which is not _

[Sebastian Ullrich]

Or use one of the up/down arrows

[Kevin Buzzard]

Any mathematician : "Let $R$ be a ring and let $A$ and $B$ be $R$-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 $R$ is a type, that's why it's called $R$. I wouldn't write "let $x$ be a ring", that would be madness!

[Jason Rute]

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]

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]

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

[Mario Carneiro]

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

[Reid Barton]

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]

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

[Johan Commelin]

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]

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

[Johan Commelin]

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

[Gabriel Ebner]

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]

Ok, so this will never work :sad:

[Gabriel Ebner]

You could use auto params.

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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