Add pi notation back ?

Stream: mathlib4

[Anatole Dedecker]

Should we add a notation (maybe scoped) to allow pi notation again ? It seems very weird to read that docs4#Pi.module is about the module structure on ∀ i, M ior (i : I) → M i ...

[Eric Wieser]

I think this is probably low enough priority that we can revisit it after the port; but I agree it's pretty weird to have pi in all the names when we no longer use the symbol with that name.

[Patrick Massot]

About this pi notation issue, does anyone has code doing that I could paste in my teaching material? There is no way I can use ∀ i, M i for a product of types.

[Eric Wieser]

I assume you also don't like using (i : I) → M i?

[Kyle Miller]

Here's a scoped notation and pretty printer for pi notation, as a synonym for forall:

import Lean
import Std.Tactic.OpenPrivate

namespace PiNotation
open Lean.Parser Term
open Lean.PrettyPrinter.Delaborator

@[scoped term_parser]
def piNotation := leading_parser:leadPrec
  unicodeSymbol "Π" "Pi" >>
  many1 (ppSpace >> (binderIdent <|> bracketedBinder)) >>
  optType >> ", " >> termParser

@[scoped macro piNotation] def replacePiNotation : Lean.Macro
  | .node info _ args => return .node info ``Lean.Parser.Term.forall args
  | _ => Lean.Macro.throwUnsupported

@[scoped delab forallE]
def delabPi : Delab := do
  let stx ← delabForall
  match stx with
  | `($group:bracketedBinder → Π $groups*, $body) => `(Π $group $groups*, $body)
  | `($group:bracketedBinder → $body) => `(Π $group, $body)
  | _ => pure stx

end PiNotation

open PiNotation

#check Π (i : Nat), Fin i
-- Π (i : Nat), Fin i : Type
#check Π {i : Nat}, Fin i
-- Π {i : Nat}, Fin i : Type
#check Π i j : Nat, Fin i × Fin j
-- Π (i j : Nat), Fin i × Fin j : Type
#check Π (p : Prop) [Decidable p], if p then Bool else Unit
-- Π (p : Prop) [inst : Decidable p], if p then Bool else Unit : Type

[Kyle Miller]

(@Patrick Massot I just updated this to have a pretty printer too)

[Patrick Massot]

Amazing, thanks!

[Eric Wieser]

I was surprised to find your code above still correctly prints Π i : Nat, i = i as ∀ (i : Nat), i = i; where's the detection of Type vs Prop happening?

[Kyle Miller]

It's calling the main delabForall, so it's happening here: | `($group:bracketedBinder → $body) =>

[Eric Wieser]

And I guess you can golf the delaborator to

@[scoped delab forallE]
def delabPi : Delab := do
  let stx ← delabForall
  match stx with
  | `($group:bracketedBinder → Π $groups*, $body) => `(Π $group $groups*, $body)
  | `($group:bracketedBinder → $body) => `(Π $group, $body)
  | _ => pure stx

which avoids re-matching against the output you just generated

[Eric Wieser]

Does repeating :bracketedBinder on the RHS as you do in your example make any difference?

[Kyle Miller]

Probably not here. It's just to make sure the antiquote parses as the right sort of thing when there's ambiguity, and I don't have a good sense of when these hints are needed (omitting them sometimes gives you compilable but wrong code)

[Scott Morrison]

PR?

[Patrick Massot]

Scott, where do you want this to be PRed? More importantly, don't we want this by default at least in mathlib? It would be a bit silly to have open PiNotation on top of every mathlib file.

[Scott Morrison]

I was assuming we would just put it in mathlib, and rejigger so it's not behind a namespace?