Notation for polynomial variables

Stream: mathlib4

[Johan Commelin]

I also want to advertise that you can now write

name_poly_vars X, Y, Z over R

to get nice syntax for polynomial variables in an MVPolynomial ring

[Kenny Lau]

i guess what i'm really asking is, would I be wasting my time if I tried to write algebra myself

[Yaël Dillies]

@Johan Commelin does that mean #27196 is redundant?

[Johan Commelin]

No, because that is not about MVPolynomial.

[Johan Commelin]

But I'm sure name_poly_vars can be beefed up.

[Johan Commelin]

I could imagine a syntax like

name_poly_vars R[X, Y, Z] -- MVPoly
name_poly_vars Int[q] -- Poly
name_poly_vars A[S][T]  -- Poly (Poly)

[Kenny Lau]

it doesn't seem that hard to do looking at the source

[Arend Mellendijk]

Kenny Lau said:

i guess what i'm really asking is, would I be wasting my time if I tried to write algebra myself

Probably. I'm just now working on it again, so maybe wait and see if I've given up on it in two weeks :sweat_smile:

[Kenny Lau]

#28349 implements the polynomial notation with two caveats:

1. I have not figured out how to remove the space (please teach me if you know how) (fixed thanks to Aaron)
2. I have not fixed the existing notation because I want to get this approved first, which means the PR will error for now

Usage:

variable (R : Type) [CommRing R]
name_poly_vars R [X,Y,Z]
name_poly_vars R [s][t][u]
#check Y -- Y : MvPolynomial (Fin 3) R
#check t -- t : Polynomial (Polynomial (Polynomial R))

[Kenny Lau]

cc @Johan Commelin @Yaël Dillies

[Aaron Liu]

Kenny Lau said:

1. I have not figured out how to remove the space (please teach me if you know how)

You seem to have a conflict with docs#GetElem notation

[Kenny Lau]

I think ideally the parser should just parse the first word unless it starts with (?

[Kenny Lau]

is this desirable?

[Aaron Liu]

what do you mean by "word"

[Kenny Lau]

identifier

[Aaron Liu]

that can probably work

[Kenny Lau]

do you want to PR to my PR?

[Aaron Liu]

I can try it

[Aaron Liu]

kckennylau/mathlib4#9

[Kenny Lau]

Thanks!

[Johan Commelin]

@Kenny Lau Cool! This looks good to me.

But I also have another feature request. Could we make it so that the command also make R[X,Y,Z] available as notation for MVPolynomial (Fin 3) R?

[Kenny Lau]

on it

[Kenny Lau]

hmm, I have run into a small problem:

[Kenny Lau]

import Mathlib.Util.Notation3

local notation3 "(Fin 37)[d,e]" => Int
-- invalid atom
-- invalid syntax node kind

[Kenny Lau]

apparently mathlib doesn't like brackets

[Kenny Lau]

but I have come up with an alternate solution:

import Mathlib.Util.Notation3

axiom Polynomial : Type → Type
axiom MvPolynomial : Type → Type → Type
axiom MvPolynomial.X {σ R : Type} (i : σ) : MvPolynomial σ R

variable (R S : Type)

local notation3 R "[d,e]" => MvPolynomial (Fin 2) R
local notation3 "d" => (MvPolynomial.X 0 : MvPolynomial (Fin 2) R)

#check (rfl : R[d,e] = MvPolynomial (Fin 2) R) -- rfl : R[d,e] = R[d,e]
#check (rfl : S[d,e] = MvPolynomial (Fin 2) S) -- rfl : S[d,e] = S[d,e]
#check Fin 37[d,e] -- Fin 37[d,e] : Type
#check (Fin 37)[d,e] -- Fin 37[d,e] : Type
#check d -- d : R[d,e]

[Kenny Lau]

(I tested name collision, name collision is fine)

[Kenny Lau]

@Johan Commelin is this acceptable? (the side effect is that for the R[d,e] notation it now doesn't matter what you put in the R, which would be inconsistent with how d still requires R...)

[Kenny Lau]

corollary: brackets now don't actually matter

[Kenny Lau]

Kenny Lau said:

apparently mathlib doesn't like brackets

after more testing, it's actually that notation3 doesn't spaces in strings and doesn't like words that start with a number

[Kenny Lau]

so there might be no other way out

[Eric Wieser]

Any notation using brackest should use noWs as well

[Eric Wieser]

Which means you can't use notation and have to use syntax instead, and write your own app_unexpander

[Adam Topaz]

Does this notation allow R[X][Y,Z][W]?

[Kenny Lau]

good point

[Kenny Lau]

do we need this?

[Kenny Lau]

i guess it would be good to have it

[Adam Topaz]

Eventually we want all the things. Including R[X][[Y,Z]][W](t)

[Kenny Lau]

btw there was one implicit assumption that i always assumed, maybe it's good to voice it out eventually:

[Kenny Lau]

this notation basically just bans MvPolynomial (Fin 1) because of ambiguity

[Kenny Lau]

I think R[q] should just always be Polynomial R

[Adam Topaz]

Yeah, I agree with that…. unless we want to redefine Polynomial;)

[Kenny Lau]

what should we call it? the current name I just had is 'polyesque'

[Aaron Liu]

Kenny Lau said:

this notation basically just bans MvPolynomial (Fin 1) because of ambiguity

You can put a trailing comma, like how one-tuples are done in python

[Aaron Liu]

This also allows MvPolynomial (Fin 0)

[Kenny Lau]

so like this?
MvPolynomial (Fin 0) R = R[,]
MvPolynomial (Fin 1) R = R[x,]
MvPolynomial (Fin 2) R = R[x,y]

[Aaron Liu]

Well I guess R[] works too

[Kenny Lau]

ok i've finally put the pieces together to make a headstart:

import Lean
import Qq

open Lean Elab Tactic Command Qq

syntax polyesque_head := ident <|> ("(" term ")")

-- syntax to allow specifying `MvPolynomial (Fin 1) R` with `R[t,]` and `Polynomial R` with `R[t]`
syntax polyesque_mv? := sepBy(ident,",",",",allowTrailingSep)

syntax polynomial_mv? := "[" polyesque_mv? "]"
syntax power_series_mv? := "[[" polyesque_mv? "]]"
syntax rat_func := "(" ident ")"
syntax laurent_series := "((" ident "))"

syntax polyesque_body := polynomial_mv? <|> power_series_mv? <|> rat_func <|> laurent_series

syntax (name := polyesque) polyesque_head noWs polyesque_body+ : term

@[term_elab polyesque] def polyesqueElab : Term.TermElab := fun stx e ↦ do
  return toExpr (toString stx)

#check R[]
#check R[X,]
#check R[X]
#check R[[X]]
#check R(X)[Y][[a,b]]((d))
#check (Fin 37)(X)[Y][[a,b]]((d))

[Kenny Lau]

what should i do here? should i store something in the global environment, or should i try to override the elaborator locally?

[Kenny Lau]

(and how do i do either of these?)

[Eric Wieser]

import Lean
import Qq

def Polynomial (R : Type) : Type := sorry

def Polynomial.X : Polynomial R := sorry
def Polynomial.C (r : R) : Polynomial R := sorry

syntax (name := Polynomial.syntax) (priority := high) term:100 noWs "[" ident "]" : term

open Lean Elab Term

@[term_elab Polynomial.syntax] def polyesqueElab : Term.TermElab := fun stx ty? ↦ do
  match stx with
  | `($R[$i]) =>
    let e ← elabTerm (← `(Polynomial $R)) ty?
    return .mdata (.mk [(`var_name, .ofName i.getId)]) e
  | _ => throwUnsupportedSyntax

/-- Construct a named variable. -/
syntax "v%" noWs ident : term

syntax "v_internal%" noWs ident : term

elab_rules <= ty
| `(v%$i:ident) => do
    let e ← try
      withoutErrToSorry <| elabTerm (← `(v_internal%$i)) ty
    catch ex =>
      exceptionToSorry ex ty

elab_rules <= ty
| `(v_internal%$i:ident) => do
  let .mdata d ty := ty | throwErrorAt i "Not a valid variable name"
  if .some i.getId = d.get? `var_name then
    elabTerm (← `(Polynomial.X)) ty
  else
    elabTerm (← `(Polynomial.C (v_internal%$i))) ty

#check (v%X : Nat[X])
#check (v%X : Nat[X])
#check (v%Y : Nat[X][Y])
#check (v%Z : Nat[X][Y])

[Johan Commelin]

Kenny Lau said:

what should i do here? should i store something in the global environment, or should i try to override the elaborator locally?

I think this should be as local as possible. Different files/sections may want different names for their polynomial variables.

[Kenny Lau]

Johan Commelin said:

Kenny Lau said:

what should i do here? should i store something in the global environment, or should i try to override the elaborator locally?

I think this should be as local as possible. Different files/sections may want different names for their polynomial variables.

yes but I meant store something in the environment so that my elaborator in NamePolyVars.Lean can output different things depending on the environment in different files, while only changing that environment locally in different files

[Kenny Lau]

basically, something like local attributes (that change something global locally)

[Kenny Lau]

man, Lean's lack of documentation is really unfortunate for learners like me, mathlib's policy of enforcing a docstring on every def is really shining out here

[Kenny Lau]

I go to https://leanprover-community.github.io/mathlib4_docs/Lean/ScopedEnvExtension.html#Lean.ScopedEnvExtension.Entry and there is zero docstring

[Kenny Lau]

great, my first test went into stack overflow, i didn't even know this is possible

[Kenny Lau]

(deleted)

[Kenny Lau]

(i debugged this in the local setup instead of the web, and it turned out it's because i can't do the testing in the same file where i initialised the commands)

[Kenny Lau]

ok, i now have working code to set local attributes

[Kenny Lau]

import Lean

open Lean Elab.Command Elab.Term

structure NAT : Type where
  val : Nat
deriving Inhabited

abbrev Test := SimpleScopedEnvExtension Nat NAT

initialize test : Test ←
  registerSimpleScopedEnvExtension {
    addEntry old new := ⟨new⟩
    initial := ⟨0⟩
  }

def getNum : CoreM Nat := do
  return (test.getState (← getEnv)).val

def setNum (n : Nat) : CoreM Unit := do
  trace[debug] m!"Setting {n}"
  test.add n .local

syntax (name := setNumCmd) "#set_num" num : command

@[command_elab setNumCmd]
def setNumCmdElab : CommandElab := fun stx ↦ do
  let `(#set_num $n:num) := stx
    | throwError "unrecognised syntax"
  liftCoreM <| setNum n.getNat

syntax (name := getNumCmd) "get_num%" : term

@[term_elab getNumCmd]
def getNumCmdElab : TermElab := fun stx e ↦ do
  return mkNatLit (← getNum)

[Kenny Lau]

(in a different file:)

import Mathlib.Sandbox.TestEnv

section foo1

#eval get_num% -- 0
#set_num 3
#eval get_num% -- 3

end foo1

section foo2

#eval get_num% -- 0
#set_num 37
#eval get_num% -- 37

end foo2

#eval get_num% -- 0
#set_num 333
#eval get_num% -- 333

section foo3

#eval get_num% -- 333
#set_num 34
#eval get_num% -- 34

end foo3

[Kenny Lau]

Kenny Lau said:

syntax laurent_series := "((" ident "))"

I can't type )) anymore, should we use unicode? ⸨⸩

[Kenny Lau]

do we want a replacement for ratFunc as well?

[Kenny Lau]

LaurentSeries actually uses R⸨X⸩

[Yakov Pechersky]

Can you use a syntax category so that parens are only parsed in such a way within a specific syntax context?

[Kenny Lau]

Yakov Pechersky said:

Can you use a syntax category so that parens are only parsed in such a way within a specific syntax context?

no, because you're supposed to be able to write R[X,Y] for MvPolynomial (Fin 2) R after you delcare it using name_poly_vars

[Kenny Lau]

I don't see a way to do that without making that syntax available globally

[Notification Bot]

71 messages were moved here from #mathlib4 > Tactic for polynomial/algebra by Eric Wieser.

[Kenny Lau]

thanks!

[Notification Bot]

A message was moved from this topic to #mathlib4 > Redefining polynomial by Eric Wieser.

[Eric Wieser]

Kenny, what are your thoughts on my v% trick above?

[Kenny Lau]

I thought it would be better to use notation so that we don't need to write the extra v%

[Kenny Lau]

and also I thought we want to only be able to use R[X][Y] after declaring it

[Kenny Lau]

@Johan Commelin so there’s a slight issue, basically I don’t want the tactic to import polynomial and laurent series and ratfunc etc (6 different modules here), and as a result, I would need to do a slightly unhygienic thing of referring to the Ident `MvPowerSeries.C rather than the real thing that exists in the MvPowerSeries module

(I discussed this with @Bhavik Mehta as well)

[Aaron Liu]

Kenny Lau said:

referring to the Ident `MvPowerSeries.C rather than the real thing that exists in the MvPowerSeries module

These are the same thing?

[Aaron Liu]

the inf and sup delabs docs#Mathlib.Meta.delabInf and docs#Mathlib.Meta.delabSup do something similar with docs#LinearOrder

[Eric Wieser]

I would expect you to let these things register themselves when imported?

[Aaron Liu]

Eric Wieser said:

I would expect you to let these things register themselves when imported?

what does this mean?

[Eric Wieser]

@Aaron Liu, delaborators are different; it's ok to ask "is this this thing that's not yet imported", but it's worse to say "your code elaborates to this thing that's not imported"

[Eric Wieser]

Aaron Liu said:

Eric Wieser said:

I would expect you to let these things register themselves when imported?

what does this mean?

The same way any other syntax works?

[Eric Wieser]

Don't register it all at once, register it piecewise with handlers

[Aaron Liu]

oh ok

[Aaron Liu]

Eric Wieser said:

Aaron Liu, delaborators are different; it's ok to ask "is this this thing that's not yet imported", but it's worse to say "your code elaborates to this thing that's not imported"

You could check if it exists, and if it doesn't throw an error saying you need to import something

[Aaron Liu]

(this is also what run_meta and other commands do)

[Eric Wieser]

I think supporting user-defined variable-definers at the same time is a good idea

[Kenny Lau]

@Eric Wieser well it already checks whether MvPolynomial.C exists when it runs the command to add the notations for the formal variables

[Kenny Lau]

it has been suggested to me that Lean.mkCIdent is a more hygenic version that checks for global constants; are there any drawbacks?

[Aaron Liu]

docs#Lean.mkCIdent

[Aaron Liu]

the downside is that it's not hygienic

[Aaron Liu]

well, it is hygienic but it uses the same hygiene every time

[Aaron Liu]

it also loses source information

[Aaron Liu]

docs#Lean.mkCIdentFrom would be better

[Aaron Liu]

why can't you just use a syntax quotation?

[Kenny Lau]

@Aaron Liu https://live.lean-lang.org/#codez=JYWwDg9gTgLgBAGQKYEMB2AoDATJAzOPCCARjgC4BeOAORRiyQBsUAjOAIhiQGcYSOFONygg4lAHxxsEDHESo0AOgCiLVkoAqSUUuZttolWh4BXKMDQBzTQE8wSOAApACYRwABk6KkAlD7hKaBBoSIzqnNx8AEyC5MI6YpLSsvLI6KrqWgl66oYgxmYW1nYOzm6e3lF+AUEhWLgElRTUdAwYAMQAxgAWSJ0A1vF8ZAC0IwDu0P08HT19g5EwUXBjeCjATDxAA

[Aaron Liu]

oh yeah

[Aaron Liu]

that's how hygiene works

[Kenny Lau]

right

[Kenny Lau]

what would you do?

[Aaron Liu]

me?

[Aaron Liu]

I would write an elab writer

[Aaron Liu]

instead of notation

[Aaron Liu]

or maybe a macro writer

[Aaron Liu]

or maybe this should just be extensible

[Kenny Lau]

hmm i could see some part of that

[Kenny Lau]

so, basically, i have no code yet this is all in my head

basically in Polynomial.lean I would be able to write something like

register_poly_vars "[" X "]" Polynomial.C Polynomial.X

and in MvPowerSeries.lean:

register_poly_vars "[[" X, ... "]]" MvPowerSeries.C 2 MvPolynomial.X

?

[Aaron Liu]

sure

[Kenny Lau]

is this what you have in mind?

[Aaron Liu]

that works

[Kenny Lau]

I guess one flaw is that then this file would be imported by the 6 files, so this file would suddenly become very low in the import hierarchy

[Aaron Liu]

is that bad?

[Kim Morrison]

Kenny Lau said:

I go to https://leanprover-community.github.io/mathlib4_docs/Lean/ScopedEnvExtension.html#Lean.ScopedEnvExtension.Entry and there is zero docstring

docstring PRs very welcome as you decipher what things mean :-)

[Kenny Lau]

hmm at that point do we still need Polynomial.X? :melting_face:

[Kenny Lau]

just write name_poly_vars R[X] at the start of every file

[Kenny Lau]

or better, make R[X] a scoped name_poly_vars declaration?

[Aaron Liu]

Kenny Lau said:

hmm at that point do we still need Polynomial.X? :melting_face:

then how would you name theorems about it

[Johan Commelin]

To be fair, it could be called var. Although I'm not a big fan... it's 2 chars longer...

[Yaël Dillies]

There's a world where Polynomial R is defined as AddMonoidAlgebra R Nat, and then (almost) everything is proved at the level of AddMonoidAlgebra, where X doesn't make sense

[Kenny Lau]

I have come across a new roadblock. Let's take (Fin 37)[t] as example:

1. We want t to mean Polynomial.X.
2. We want (Fin 37)[t] to mean Polynomial
3. We want to be able to extend this notation, so that (Fin 37)[u] would still make sense on the level of syntax

Then the problem is that after the notation t is declared (step 1), then t is no longer a valid identifier, so that the following (auto-generated, don't worry) code fails:

axiom Polynomial : Type → Type
axiom Polynomial.X {R : Type} : Polynomial R

syntax poly := "(" term ")" noWs "[" ident "]"
syntax poly : term

local notation "t" => (Polynomial.X : Polynomial (Fin 37))
#check t -- Polynomial.X : Polynomial (Fin 37)
#check (Fin 37)[t] -- ❌ unexpected token 't'; expected identifier
#check (Fin 37)[u] -- ✔ not implemented

I am now considering a workaround, which is to instead hardcode the notation "[t]" in poly:

syntax poly := "(" term ")" noWs "[t]"

but this feels a bit cursed. What are your opinions?

[Kenny Lau]

cc @Aaron Liu

[Aaron Liu]

I have some ideas

[Kenny Lau]

I wouldn't be surprised

[Kenny Lau]

it works!!!! i have my first working code :melt:

[Aaron Liu]

what did you do

[Kenny Lau]

what i said

[Aaron Liu]

that feels a bit cursed

[Kenny Lau]

well you didn't tell me your ideas

[Aaron Liu]

I'm working on it

[Kenny Lau]

My code can now do:

import Mathlib.Tactic.Ring.NamePolyVars

-- set_option trace.name_poly_vars true

axiom Polynomial : Type → Type
axiom Polynomial.C {R : Type} : R → Polynomial R
axiom Polynomial.X {R : Type} : Polynomial R

#register_poly_vars "[" X "]" Polynomial Polynomial.C Polynomial.X

variable (R : Type)

#name_poly_vars R[t]

#check t
#check R[t] -- Polynomial R : Type

axiom MvPolynomial : Type → Type → Type
axiom MvPolynomial.C {σ R : Type} : R → MvPolynomial σ R
axiom MvPolynomial.X {σ R : Type} (i : σ) : MvPolynomial σ R

#register_poly_vars "[" X, ... "]" MvPolynomial MvPolynomial.C MvPolynomial.X

#name_poly_vars R[x,y]
#check x
#check y
#check R[x,y] -- MvPolynomial (Fin 2) R : Type

#name_poly_vars R[a,b][C]
#check a
#check b
#check C
#check R[a,b][C] -- Polynomial (MvPolynomial (Fin 2) R) : Type

[Aaron Liu]

unfortunately my ideas are not working so we might have to use the cursed grouping

[Kenny Lau]

@Aaron Liu do you know what's the magic to have the pretty printer use the new notation?

[Aaron Liu]

write a delab (or an unexpander)

[Kenny Lau]

@Aaron Liu I tried to learn both, but I could not get either to work, here is my code that does not work:

import Qq
import Mathlib.Lean.PrettyPrinter.Delaborator

universe u

axiom Polynomial : Type u → Type u
axiom Polynomial.C {R : Type u} : R → Polynomial R
axiom Polynomial.X {R : Type u} : Polynomial R

variable (R S : Type u)

local notation "t" => (Polynomial.X : Polynomial R)
#check t

@[app_unexpander Polynomial.X]
def Polynomial.unexpandX : Lean.PrettyPrinter.Unexpander
  | `((Polynomial.X : Polynomial «$R»)) => `(t)
  | _ => throw ()

#check Polynomial.X (R := R)
#check Polynomial.X (R := S)

open Lean PrettyPrinter Delaborator SubExpr
open Qq

@[app_delab Polynomial.X]
def Polynomial.delabX : Delab := do
  let ⟨.succ u, ~q(Polynomial $R), e⟩ ← inferTypeQ (← getExpr)
    | throwError ""
  let x ← elabTermEnsuringTypeQ (← `(t)) q(Polynomial $R)
  annotateGoToSyntaxDef (← `(t))

#check Polynomial.X (R := R)
#check Polynomial.X (R := S)

[Kenny Lau]

Would you like to teach me how to fix it?

[Aaron Liu]

oh this might be tricky

[Aaron Liu]

yeah I have no idea how to make this work

[Kenny Lau]

@Eric Wieser would you have any idea? to summarise, in the code above I introduce local notation t for Polynomial.X (R := R), and I want a delab/unexpander to print t for Polynomial.X (R := R) but not for Polynomial.X (R := S).

[Kenny Lau]

I should also say that the full working code is now available in #28349

[Kenny Lau]

cc @Yaël Dillies

[Kenny Lau]

though idk if I should make it work with scoped notation like you wanted in bivariates...

[Kenny Lau]

it's a bit complicated because in the code the base ring is a fixed free variable

[Kenny Lau]

I think the current idea is to just write

variable (R : Type*) [Semiring R]
#name_poly_vars R[X][Y]

at the top of every file importing Bivariate?

[Yaël Dillies]

Yes, I think that's perfectly fine

[Yaël Dillies]

Would be cool if there was a way to say "R(X]|Y] will mean Polynomial (Polynomial R) for all rings R", as this shows up in Toric, but if we have to do #name_poly_vars R[X][Y] #name_poly_vars S[X][Y] once then it's fine

[Kenny Lau]

it's definitely possible, but my impression was that the consensus is against that

[Kenny Lau]

Yaël Dillies said:

Would be cool if there was a way to say "R(X]|Y] will mean Polynomial (Polynomial R) for all rings R", as this shows up in Toric, but if we have to do #name_poly_vars R[X][Y] #name_poly_vars S[X][Y] once then it's fine

(you should also make the variable names different)

[Kenny Lau]

i think this is a good point to bring up

[Kenny Lau]

import Mathlib


section Proposal1

local notation "X" => Polynomial.X

variable (R S : Type*) [CommRing R] [CommRing S]

#check (X : Polynomial R)
#check (X : Polynomial S)

end Proposal1


section Proposal2

variable (R S : Type*) [CommRing R] [CommRing S]

local notation "X" => (Polynomial.X : Polynomial R)
#check (X : Polynomial R)
#check (X : Polynomial S) -- error

end Proposal2

[Kenny Lau]

the current code is for proposal2, and that's what i've written as well, but it seems like you want proposal 1

[Kenny Lau]

I think there's a potential drawback for proposal1 where you would do

#name_poly_vars R[X][Y]
#name_poly_vars R[a][b][c]

and then X for b would typecheck

[Yaël Dillies]

Kenny Lau said:

I think there's a potential drawback for proposal1 where you would do

#name_poly_vars R[X][Y]
#name_poly_vars R[a][b][c]

and then X for b would typecheck

Does it really happen that you simultaneously consider different polynomial rings over the same ring?

[Yaël Dillies]

My use case really is to deal with things like base change, where I transfer information about some polynomial ring to some other polynomial ring over a different ring

[Kenny Lau]

I don't really mind either way but I would prefer if there's a consensus because I can't maintain two copies of the same code

[Kenny Lau]

@Yaël Dillies I have an alternate proposal to encompass both:

In my PR, there's currently already a workaround, to use (_) for the ring so that it can fit in any type:

section Test1

name_poly_vars (_)[a,b][C]

variable (R : Type)

noncomputable example : Vector (Polynomial (MvPolynomial (Fin 2) R)) 3 :=
  have : Polynomial (MvPolynomial (Fin 2) R) = (_)[a,b][C] := rfl
  have : Polynomial.C (MvPolynomial.X (R := R) 0) = a := rfl
  have : Polynomial.C (MvPolynomial.X (R := R) 1) = b := rfl
  have : (Polynomial.X : Polynomial (MvPolynomial (Fin 2) R)) = C := rfl
  #v[a, b, C]

end Test1

but obviously this is suboptimal, so I propose a proposal 3 where I would enable:

name_poly_vars _[a,b][C]

to do the thing you want, with special support so that you can later type R[a,b][C] and also S[a,b][C] and have Lean recognise the notation.

[Kenny Lau]

(cc @Johan Commelin is this ok to you?)

[Johan Commelin]

@Kenny Lau I like proposal 3 :smiley:

[Kenny Lau]

@Johan Commelin @Yaël Dillies I've updated #28349 to allow for name_poly_vars _[a,b][C] to mean do this for all rings

[Adam Topaz]

@Aaron Liu @Kenny Lau Is #28349 ready to be reviewed or are you still actively working on it?

[Kenny Lau]

Adam Topaz said:

Aaron Liu Kenny Lau Is #28349 ready to be reviewed or are you still actively working on it?

it is ready to be reviewed

[Kenny Lau]

@Johan Commelin Adam has raised a point on the syntax for registering the notation. Which one do you prefer?

Proposal 1:

• register_poly_vars "[" X "]" Polynomial Polynomial.C Polynomial.X
• register_poly_vars "[" X, ... "]" MvPolynomial MvPolynomial.C MvPolynomial.X

Proposal 2:

• register_poly_var "[" "]" Polynomial Polynomial.C Polynomial.X
• register_mv_poly_vars "[" "]" MvPolynomial MvPolynomial.C MvPolynomial.X

[Kenny Lau]

cc @Eric Wieser

[Adam Topaz]

To add a bit of context, I think the X in proposal 1 could only lead to confusion, since the actual notation doesn’t actually involve X after the command is issued (you need a separate command to declare the var names). These commands are just there to register the delimiters such as [ and ].

I think a nicer approach would be to have just one command, and to detect whether the notation is single or multi variable by checking the type of the functions that are specified after the delimiters, but that would require a bit more metaprogramming.

[Kenny Lau]

@Adam Topaz As I explained in the PR, I didn't like the last approach because that's like mixing syntax with evaluation

[Adam Topaz]

Thats the whole point of elaboration, isn’t it?

[Kenny Lau]

no, the whole PR is strictly syntax

[Adam Topaz]

I can give an implementation later today (hopefully) if you would like to try it out

[Kenny Lau]

@Adam Topaz I'm not saying it can't be done, I'm saying that the entirety of my PR is operating within syntax. See for example my function to build the X term, which is just syntactical function application

[Kenny Lau]

there's no type checking done anywhere, because the whole point is just to build notation

[Kenny Lau]

so it feels wrong to suddenly jump out of syntax.

[Kenny Lau]

another example is how I allow for underscores in the syntax, which aren't filled in at all until Lean decides to elaborate it

[Kenny Lau]

the undescore in register_poly_vars "[[" X "]]" PowerSeries (PowerSeries.C _) PowerSeries.X

[Adam Topaz]

Ok, I guess I don’t really understand the objection then. Are you saying that having one command that detects how to modify the env extension is not a good idea for some reason? Or are you saying that you want to leave this PR as primarily syntax/notation manipulation and think about the suggestion in a follow up PR?

[Kenny Lau]

I'm saying these commands should operate entirely within syntax

[Kenny Lau]

they should be purely syntax -> syntax, so all the syntax info (in this case, whether it's 1v or mv) should be provided by syntax, not by further type checking of the terms provided

[Adam Topaz]

Can you explain why you want them to only operate within syntax?

[Kenny Lau]

because the output is in syntax, i.e. the notation commands (here)

[Kenny Lau]

also like these should work regardless of whether Polynomial.C is implemented as a ring hom or just as a function, the command shouldn't care about these "implementation details"

[Adam Topaz]

So in particular you want to allow register_poly_vars “[“ X “]” foo bar even if foo and bar don’t exist?

[Eric Wieser]

Note that there is precedent for jumping back and forth between syntax and elaboration; variable elaborates its arguments, even though they are ultimately reused as syntax

[Kenny Lau]

Adam Topaz said:

So in particular you want to allow register_poly_vars “[“ X “]” foo bar even if foo and bar don’t exist?

ideally, but Lean actually doesn't really allow that (due to "hygiene")

[Eric Wieser]

Kenny Lau said:

also like these should work regardless of whether Polynomial.C is implemented as a ring hom or just as a function, the command shouldn't care about these "implementation details"

I forsee this being a little tricky with PowerSeries, where the objects themselves can be applied as functions with some defeq abuse

[Eric Wieser]

Which is not an argument against the metaprogramming, only for writing a test for this case

[Kenny Lau]

Kenny Lau said:

the undescore in register_poly_vars "[[" X "]]" PowerSeries (PowerSeries.C _) PowerSeries.X

(hey looks like this was recently fixed in #27889)

[Kenny Lau]

Eric Wieser said:

Which is not an argument against the metaprogramming, only for writing a test for this case

well... I just don't think it's a good thing...

[María Inés de Frutos Fernández]

Johan Commelin said:

I also want to advertise that you can now write

name_poly_vars X, Y, Z over R

to get nice syntax for polynomial variables in an MVPolynomial ring

Nice! Do we have the analogue for MvPowerSeries?

[Kenny Lau]

@María Inés de Frutos Fernández that is my PR #28349 which is currently being discussed

[María Inés de Frutos Fernández]

Awesome, thanks!

[Kenny Lau]

we're having a small disagreement over the way to declare multivariate notation vs univariate

[Adam Topaz]

Okay, I'm at my office now so I can write a bit more. Here is what I propose. We have a single command register_vars (or whatever) that has the following usage by default: register_vars "[" "]" foo bar. This command should try to deduce whether to register single or multi variables by looking at the types of foo and bar and checking if the type looks like the Polynomial case or the MvPolynomial case.

There will be edge cases where no such determination can be made for whatever reason. In such cases, the command would throw an error and require require the user to provide a configuration option approximately like register_vars (mv := true) "[" "]" foo bar.

[Adam Topaz]

When such a configuration is provided, no further elaboration of foo or bar is done, and the command behaves as it does now, depending on whether mv := true or mv := false.

[Kenny Lau]

@Adam Topaz I would prefer (for the same reasons) to just have (mv := true|false) without the type checking

[Kenny Lau]

(additionally we can also default to false)

[Eric Wieser]

Another syntax proposal would be

register_poly_vars "[" _ "]" Polynomial Polynomial.C Polynomial.X
register_poly_vars "[" _,+ "]" MvPolynomial MvPolynomial.C MvPolynomial.X

[Eric Wieser]

Since we already have ,+ as a combinator for regular syntax

[Adam Topaz]

Okay, at the end of the day, I don't think this automatic detection is that important, so I would be fine with either (mv := ...) or _/_,+ (but not X because I do think it could lead to confusion)

[Kenny Lau]

@Johan Commelin please pick one :upside_down:

[Eric Wieser]

Can you remind me why we need a custom registration function here? What goes wrong with something like

macro R:term _:noWs "[" vars:poly_var,* "]" : term => makePolyHandler `(Polynomial) `(Polynomial.C) `(Polynomial.X) R vars

[Kenny Lau]

aren't you doing the same thing then

[Kenny Lau]

but also making it harder for the average Lean user (who knows nothing about metaprogramming) to register a new polynomial-like functor

[Kenny Lau]

oh, and also, your code just registers the syntax for R[q], but not for q

[Eric Wieser]

Right, I'm only suggesting a replacement for register_poly_vars

[Kenny Lau]

also it behaves differently than the specified behaviour, your code makes the notation R[q] globally available

[Kenny Lau]

my register_poly_vars only adds to the env extension

[Johan Commelin]

I think mv := ... is easier for the average user than _,+

[Kenny Lau]

@Eric Wieser your suggestion seems to work:

import Lean
import Qq

open Lean Elab Term Parser.Term Qq

axiom Polynomial : Type → Type
axiom Polynomial.X {R} : Polynomial R

variable {R : Type}

declare_syntax_cat poly_var

syntax "t" : poly_var

syntax (name := decode_poly_var) poly_var : term

@[term_elab decode_poly_var]
def decodePolyVar : TermElab := fun stx typ ↦ do
  let .node _ _ #[.node _ _ #[.atom _ str]] := stx
    | throwError m!"Unrecognised polynomial-like notation: {stx}"
  if str = "t" then elabTerm (← `(Polynomial.X)) typ else
    throwError m!"{str}"

syntax (name := polyesque) ident "[" poly_var "]" : term

@[term_elab polyesque]
def decodePolyesque : TermElab := fun stx typ ↦ do
  let `(polyesque|$R:ident [$v:poly_var]) := stx
    | throwError m!"Unrecognised polynomial-like notation: {stx}"
  let .node _ _ #[.atom _ str] := v.raw
    | throwError m!"Unrecognised polynomial-like variable: {v}"
  if str = "t" then elabTerm (← `(Polynomial $R)) typ else
    throwError m!"{str}"

#print Syntax
#check t
#check R[t]

[Kenny Lau]

@Adam Topaz expressed concerns on storing this as string, which you also agreed with

[Kenny Lau]

but I don't see a way to store this other than the string [t]

[Kenny Lau]

i actually think it's the best way, it prevents someone from declaring [t as the open brackets and ] as the closing brackets (i.e. prevents collisions)

[Kenny Lau]

you need something hashable to look up whether a notation has been declared, and string is the best way to do this

[Eric Wieser]

Do you need to look up if the notation is declared? Why not let the standard notation overloading deal with this?

[Kenny Lau]

@Eric Wieser if someone declares
#name_poly_vars R[a,b][C]
then #check R[d,e][f] should error

[Kenny Lau]

so given d e f, I need to look up in the table whether d e f specifically are declared

[Kenny Lau]

the best way to store that information imo is the string [d,e][f]

[Eric Wieser]

I'd argue that R[a,b][D] should error on the D, which means you should store a structured object you can do a partial lookup on

[Kenny Lau]

I would disagree. you're saying that R[a,b] should not error, but I think it should error.

[Eric Wieser]

Is this legal? def foo (x : R[a,b]) (y : R[a,b][c]) : R[a,b][c] := C x + y?

[Kenny Lau]

I don't think it should be legal.

[Kenny Lau]

One reason could be that this would make a mean two things

[Kenny Lau]

a would mean both MvPolynomial.X 0 and Polynomial.C (MvPolynomial.X 0)

[Kenny Lau]

as cursed as this would be, I would prefer:
def foo (x : R[p,q]) (y : R[a,b][c]) : R[a,b][c] := C x + y

[Jovan Gerbscheid]

Kenny Lau said:

Then the problem is that after the notation t is declared (step 1), then t is no longer a valid identifier, so that the following code fails

Would the following suffice as a solution to your problem? We add a syntax category poly_var, and we locally add specific variables to this syntax category. This syntax category is allowed to give a term, and then we make the macro act on this when it is a term.

axiom Polynomial : Type → Type
axiom Polynomial.X {R : Type} : Polynomial R

declare_syntax_cat poly_var
syntax poly_var : term

syntax poly := "(" term ")" noWs "[" poly_var "]"
syntax poly : term

local syntax "t" : poly_var
local macro_rules | `(t) => `((Polynomial.X : Polynomial (Fin 37)))

#check t -- Polynomial.X : Polynomial (Fin 37)
#check (Fin 37)[t] -- ✔ not implemented
#check (Fin 37)[u] -- ❌ unexpected identifier; expected poly_var

[Kenny Lau]

yep that works

[Kenny Lau]

@Jovan Gerbscheid could you explain to me how the :max magic works?

[Kenny Lau]

do you intend to remove the other use of term_decl as well?

[Kenny Lau]

also i forgot about macro_rules, thanks for the reminder

[Jovan Gerbscheid]

When declaring a syntax parser, it is often useful to tell Lean about precedence. For example using infixl:65 for + expands to something like

syntax:65 term:65 " + " term:66 : term

When parsing a term, to figure out if it is valid syntax, there is always the current precedence level, and each syntax has a precedence level in which it is allowed.
For example a + b is allowed in precedence 65 or lower. The a is then parsed with precedence 65, and the b is parsed with precedence 66. This means that nested addition in the left is allowed, but not in the right.

In function applications, like f a, a is parsed with the highest possible precedence, which is max, or 1024. So to allow our notation here, we need to set the precedence of our syntax to max.

[Jovan Gerbscheid]

Kenny Lau said:

do you intend to remove the other use of term_decl as well?

If possible, yes

[Kenny Lau]

So if I have a + b * c, basically b is located at a higher precedence therefore a + b doesn't activate? is that a correct understanding?

[Kenny Lau]

i'm trying to understand what you mean by a syntax being "allowed"

[Jovan Gerbscheid]

Yes, Lean might consider parsing a + b * c bracketed like (a + b) * c, but it will reject this option, because the first argument of the _ * _ notation is parsed at precedence 70, and a + b has precedence 65, which is smaller than 70 and thus rejected.

[Kenny Lau]

so if it's :max then it's always allowed

[Jovan Gerbscheid]

Yes. For example, the bracket notation (_) has this :max precedence, so it is accepted in any place, and the inside is parsed with minimal precedence, so any syntax in there will always be accepted.

[Jovan Gerbscheid]

Kenny Lau said:

so if it's :max then it's always allowed

In particular, if the whole notation is marked with :max, then it is always allowed.

On the other hand if a part of a notation is marked with :max, then this uses is the most restrictive kind of parsing.

[Kenny Lau]

@Jovan Gerbscheid how do i write that line local macro_rules | `(t) = ... dynamically?

[Kenny Lau]

i now have:

def String.toPolyVar (s : String) : PolyVar :=
  ⟨.node default default #[.atom default s]⟩

[Kenny Lau]

not sure if this is correct

[Jovan Gerbscheid]

It seems to be very awkward to refer to a syntax which is being defined on the fly. This is the solution I have now:

import Lean
open Lean Elab Command

axiom Polynomial : Type → Type
axiom Polynomial.X {R : Type} : Polynomial R

declare_syntax_cat poly_var
syntax poly_var : term

abbrev PolyVar := TSyntax `poly_var

syntax poly := "(" term ")" noWs "[" poly_var "]"

def mkPolyVar (s : String) (stxName : Name) : PolyVar :=
  ⟨.node default stxName #[.atom default s]⟩

syntax poly : term

run_cmd do
  let var := "t"
  let stxNameId := mkIdent (.mkStr `UniqueString var) -- TODO: make this name hygienic
  elabCommand (← `(command|
    local syntax (name := $stxNameId) $(quote var):str : poly_var))
  let stxName ← liftCoreM <| realizeGlobalConstNoOverload stxNameId
  let var := mkPolyVar var stxName
  elabCommand (← `(command|
    local macro_rules
    | `($var:poly_var) => `((Polynomial.X : Polynomial (Fin 37)))))

#check t -- Polynomial.X : Polynomial (Fin 37)
#check (Fin 37)[t] -- ✔ not implemented
#check (Fin 37)[u] -- ❌ unexpected identifier; expected poly_var

[Kenny Lau]

thanks

[Jovan Gerbscheid]

Here's a cleaner solution I've found now, using Command.elabSyntax:

import Lean
open Lean Elab Command

axiom Polynomial : Type → Type
axiom Polynomial.X {R : Type} : Polynomial R

declare_syntax_cat poly_var
syntax poly_var : term

abbrev PolyVar := TSyntax `poly_var

syntax poly := "(" term ")" noWs "[" poly_var "]"

syntax poly : term

run_cmd do
  let var := "t"
  let kind ← elabSyntax (← `(command| local syntax $(quote var):str : poly_var))
  let var := ⟨mkNode kind #[mkAtom var]⟩
  elabCommand (← `(command|
    local macro_rules
    | `($var:poly_var) => `((Polynomial.X : Polynomial (Fin 37)))))

#check t -- Polynomial.X : Polynomial (Fin 37)
#check (Fin 37)[t] -- ✔ not implemented
#check (Fin 37)[u] -- ❌ unexpected identifier; expected poly_var

[Kenny Lau]

oh wow they made a specialised function just for this situation

[Eric Wieser]

Alternatively, should we just allow every ident to be a poly_var, and have the elaborator do the lookup in an environment extension?

[Kenny Lau]

well this approach seems to eliminate the need for env ext

[Kenny Lau]

Eric Wieser said:

Alternatively, should we just allow every ident to be a poly_var, and have the elaborator do the lookup in an environment extension?

well...

import Lean
open Lean Elab Command

declare_syntax_cat poly_var
syntax ident : poly_var
syntax poly_var : term

def foo (a : Nat → Nat) (b : Nat) : Nat := a b

[Jovan Gerbscheid]

Eric Wieser said:

Alternatively, should we just allow every ident to be a poly_var, and have the elaborator do the lookup in an environment extension?

Originally, I also wanted to just use the ident syntax category. But the problem is that those identifiers that are declared to be polynomial variables do not get parsed as ident.

I would still be happy to allow other idents in the syntax if that helps improve error messages.

[Kenny Lau]

I now realised that ident <|> poly_var might work in one situation

[Kenny Lau]

actually no that doesn't really save any lines

[Eric Wieser]

Whoops, I forgot we care about q and not just R[q], indeed my suggestion is stupid

[Jovan Gerbscheid]

There are 2 places where we want to parse polynomial variables:

1. As loose expressions. For this we need a local notation.
2. Inside of the brackets of R[a,b]. For this we are forced to jump through hoops to be able to parse those same variables. Here we could use poly_var, or use poly_var <|> ident if that helps give better error messages.

[Kenny Lau]

I have discovered a new tech:

import Lean

axiom Polynomial : Type → Type

open Lean Syntax Elab Command

declare_syntax_cat poly_var
syntax term:max "[" poly_var "]" : term

elab "#asdf" : command => do
  let R : Term ← `($$head)
  let pR : Term ← `(Polynomial $R)
  have n := "t"
  let kind ← elabSyntax <| ← `(command| local syntax $(quote n):str : poly_var)
  let nv : TSyntax `poly_var := ⟨.node default kind #[.atom default n]⟩
  elabCommand <| ← `(command| local macro_rules
    | `($R[$nv:poly_var]) => `($pR) )

variable (R : Type)
#check R[t]

#asdf

#check R[t]

double-quoting for the win

[Eric Wieser]

Why is head mentioned only once there?

[Kenny Lau]

@Eric Wieser pR contains another $head (hidden in $R := $head)

[Kenny Lau]

the code essentially does:

local syntax "t" : poly_var
local macro_rules | `($head[t]) => `(Polynomial $head)

but dynamically

[Jovan Gerbscheid]

Great! So we now don't need to implement a global elaborator/macro for the R[t] syntax either. It can also be declared as a local macro.

[Kenny Lau]

yes, that is my plan

[Jovan Gerbscheid]

We can also have the syntax term:max "[" poly_var "]" : term be scoped to some PolyNotation namespace. And the #asdf command can run the command open scoped PolyNotation. This way, the syntax can't get in the way of people trying to index arrays.

[Kenny Lau]

Jovan Gerbscheid said:

the syntax can't get in the way of people trying to index arrays.

you already can't, poly_var is very restrictive

[Kenny Lau]

i don't know about the scoped syntax suggestion... I already don't like how ⊗ for TensorProduct is scoped

[Jovan Gerbscheid]

In this case the user wouldn't even notice whether it is scoped, because they already need to turn in on using a special command.

[Jovan Gerbscheid]

Kenny Lau said:

Jovan Gerbscheid said:

the syntax can't get in the way of people trying to index arrays.

you already can't, poly_var is very restrictive

But what if you have a : Std.HashMap (Polynomial Nat) Nat, and t is a polynomial variable in Nat[t]. then a[t] could do the wrong thing.

[Kenny Lau]

import Lean
import Qq

axiom Polynomial : Type → Type

open Lean Syntax Elab Command Term Qq

declare_syntax_cat poly_var
syntax (name := test) term:max "[" poly_var "]" : term

-- local syntax "t" : poly_var
-- local macro_rules | `($head[t]) => `(Polynomial $head)

elab "#asdf" : command => do
  let R : Term ← `($$head)
  let pR : Term ← `(Polynomial $R)
  have n := "t"
  let kind ← elabSyntax <| ← `(command| local syntax $(quote n):str : poly_var)
  let nv : TSyntax `poly_var := ⟨.node default kind #[.atom default n]⟩
  elabCommand <| ← `(command| local macro_rules
    | `($R[$nv:poly_var]) => `($pR) )

@[term_elab test] def testElab : TermElab := fun stx typ ↦ do
  logInfo "triggered"
  return q(false)

variable (R : Type)
#check R[t]

#asdf

#check R[t]
#check (Fin 3)[t]
#check _[t]
#check ((Fin 3)[t])[t]

[Kenny Lau]

check how "triggered" is never triggered

[Kenny Lau]

Jovan Gerbscheid said:

But what if you have a : Std.HashMap (Polynomial Nat) Nat, and t is a polynomial variable in Nat[t]. then a[t] could do the wrong thing.

but this would happen regardless of whether you scope the notation...

[Kenny Lau]

also if you declare it using Nat[t] then a[t] wouldn't trigger

[Kenny Lau]

I made it an option to match against all head or one specific head

[Kenny Lau]

name_poly_vars Nat[p,q] only matches on Nat

[Kenny Lau]

name_poly_vars _[p,q] matches on any head

[Jovan Gerbscheid]

Let's say we've declared name_poly_vars R[x] and name_poly_vars S[y]. Then if I write R[y], this will be valid syntax, but there won't be a macro for it, and no elaborator, so it will give a silly error message. Do we need an elaborator that just throws an error, as a fall-back in this case?

[Kenny Lau]

import Lean
import Qq

axiom Polynomial : Type → Type

open Lean Syntax Elab Command Term Qq

declare_syntax_cat poly_var

syntax "#check_poly_var " poly_var : command

syntax (name := test) term:max noWs "[" poly_var "]" : term

-- local syntax "t" : poly_var
-- local macro_rules | `($head[t]) => `(Polynomial $head)

elab "#asdf " head:term:max noWs "[" var:ident "]" : command => do
  let n : String := var.getId.toString
  logInfo n
  let kind ← elabSyntax <| ← `(command| local syntax $(quote n):str : poly_var)
  let nv : TSyntax `poly_var := ⟨.node default kind #[.atom default n]⟩
  elabCommand <| ← `(command| local macro_rules
    | `($head[$nv:poly_var]) => `(Polynomial $head) )

@[term_elab test] def testElab : TermElab := fun stx typ ↦ do
  logInfo "triggered"
  return q(false)

variable (R S : Type)

-- local syntax "x" : poly_var
-- local macro_rules | `(R[x]) => `(Polynomial R)

#asdf R[x]
-- error: expected no space before

[Kenny Lau]

I'm getting a strange error message here...

[Kenny Lau]

it seems like the term:max approach fails to circumvent the existing get-index notation

[Kenny Lau]

but why did it work in the last code snippet i sent??

[Aaron Liu]

GetElem is max

[Kenny Lau]

so it seems like we're stuck with term_decl then?

[Kenny Lau]

(but then why did it work before?)

[Jovan Gerbscheid]

I think Lean may have special support "left recursive" syntax, such as

syntax (name := test) term:max "[" poly_var "]" : term

[Eric Rodriguez]

i think max+1 works

[Eric Rodriguez]

(untested)

[Kenny Lau]

...

[Eric Rodriguez]

it's very "infinity plus one" vibes

[Jovan Gerbscheid]

I tried, but I think it doesn't work. I think max and max+1 behave the same.

[Kenny Lau]

no they behave differently

[Kenny Lau]

import Lean

axiom Polynomial : Type → Type

open Lean Syntax Elab Command Term

declare_syntax_cat poly_var

syntax (name := test) term:max noWs "[" poly_var "]" : term

elab "#asdf " head:term:(max+1) noWs "[" var:ident "]" : command => do
  let n : String := var.getId.toString
  logInfo n
  let kind ← elabSyntax <| ← `(command| local syntax $(quote n):str : poly_var)
  let nv : TSyntax `poly_var := ⟨.node default kind #[.atom default n]⟩
  elabCommand <| ← `(command| local macro_rules
    | `($head[$nv:poly_var]) => `(Polynomial $head) )

variable (R : Type)

-- local syntax "x" : poly_var
-- local macro_rules | `(R[x]) => `(Polynomial R)

#asdf R[x]
-- error: unexpected token at this precedence level; consider parenthesizing the term

[Kenny Lau]

the error message is different

[Jovan Gerbscheid]

Oops, my bad. I guess it just rejects any synax then, haha

[Kenny Lau]

man working with meta is quite exhausting, there's like much less knowledge in the community than normal lean code, i think any mathematician would crash out if this was the situation in main mathlib

[Kenny Lau]

if i was instead asking "how to take the square root of e" i would receive 10 correct answers by the next minute

[Kenny Lau]

i feel like i'm restricted every step of the way

[Jovan Gerbscheid]

Kenny Lau said:

so it seems like we're stuck with term_decl then?

It seems so

[Jovan Gerbscheid]

By the way, you can use mkNode and mkAtom instead of .node and .atom to avoid having to write default.

[Kenny Lau]

thanks

[Kenny Lau]

/me has now realised that if term:max doesn't work then the double quotation tech $$head would also not work...

[Kenny Lau]

lemme cook up an mwe...

[Kenny Lau]

import Lean

open Lean

/-- An unambiguous term declaration, which is `_`, an identifier, or a term enclosed in brackets -/
syntax term_decl := hole <|> ident <|> ("(" term ")")

/-- A type synonym for a term declaration, used to avoid ambiguity in the syntax. -/
abbrev TermDecl : Type := TSyntax ``term_decl

macro t:term_decl : term =>
  match t with
  | `($u:hole) => `(term| $u:hole)
  | `($k:ident) => `(term| $k:ident)
  | `(($t:term)) => `(term| ($t:term))
  | _ => default

def fib : Nat → Nat
  | 0 => 0
  | 1 => 1
  | n+2 => fib n + fib (n + 1)
-- error: unexpected identifier; expected command

[Kenny Lau]

it seems like trying to interpret any term_decl as a term somehow breaks everything

[Kenny Lau]

@Jovan Gerbscheid could you help me here?

[Kenny Lau]

to see why this is needed:

import Lean

open Lean

/-- An unambiguous term declaration, which is `_`, an identifier, or a term enclosed in brackets -/
syntax term_decl := hole <|> ident <|> ("(" term ")")

/-- A type synonym for a term declaration, used to avoid ambiguity in the syntax. -/
abbrev TermDecl : Type := TSyntax ``term_decl

declare_syntax_cat poly_var
syntax term_decl noWs "[" poly_var "]" : term

axiom Polynomial : Type → Type

local syntax "t" : poly_var
local macro_rules
  | `($head:term_decl[t]) => `(term|Polynomial $head:term)
/-
Application type mismatch: The argument
  head
has type
  TSyntax `term_decl
but is expected to have type
  TSyntax `term
in the application
  head.raw
-/

macro td:term_decl : term =>
  match td with
  | `($u:hole) => `(term| $u:hole)
  | `($k:ident) => `(term| $k:ident)
  | `(($tm:term)) => `(term| ($tm:term))
  | _ => default

def fib : Nat → Nat
  | 0 => 0
  | 1 => 1
  | n+2 => fib n + fib (n + 1)
-- error: unexpected identifier; expected command

[Jovan Gerbscheid]

Interpreting term_decl as term seems like a very bad idea to me.

[Kenny Lau]

what's the safe way to do that?

[Kenny Lau]

honestly i don't know why this is happening in the first place, why can Lean only interpret x[y] one way?

[Kenny Lau]

why can't lean see x[y] and try both getelems and polynomial?

[Kenny Lau]

like i want to use term:max but this clash is making it not possible

[Jovan Gerbscheid]

I would define a function TermDecl → Term, and run that manually.

[Kenny Lau]

that's what i did the first time, but it doesn't work with $head because it doesn't match any of the three cases

[Jovan Gerbscheid]

I think we saw above that it is possible to use term for R[t] notation, but that we can't use it for the name_poly_vars command itself.

[Kenny Lau]

ok lemme calm my nerves and try again

[Kenny Lau]

@Jovan Gerbscheid you are correct!

[Kenny Lau]

do you know why this is the case?

[Jovan Gerbscheid]

Jovan Gerbscheid said:

I think Lean may have special support "left recursive" syntax, such as

syntax (name := test) term:max "[" poly_var "]" : term

I think it is because the left-recursiveness doing something special

[Kenny Lau]

why does it work where it works then

[Kenny Lau]

@Jovan Gerbscheid i'm still getting strange errors after switching to term:max

[Kenny Lau]

i can't quite minimalise it but basically in random places in my file i get the error expected no space before

[Kenny Lau]

the relevant part of my code is

syntax polyesque := term:max noWs polyesque_notation+
syntax polyesque : term

[Jovan Gerbscheid]

I see, I guess it might not work after all. I've been trying to get it to work even with using term_decl and I'm in the mud with all these quotations of quotations.

[Kenny Lau]

the fallback i have in my head is that given an input #asdf _[t] i would manually declare the syntax three times for each case of term_decl

[Kenny Lau]

so i would do:

local macro_rules | `(_[t]) => `(Polynomial _)
local macro_rules | `($i:ident[t]) => `(Polynomial $i)
local macro_rules | `(($u:term)[t]) => `(Polynomial ($u))

[Jovan Gerbscheid]

Oh, that seems not too bad actually

[Kenny Lau]

well but that means I need to repeat code three times

[Kenny Lau]

or i guess not really but like

[Kenny Lau]

this feels really suboptimal

[Jovan Gerbscheid]

For the term, we don't even want the _[t] case

[Kenny Lau]

i think it's fine, like i think (foo : _[t]) should be legal

[Kenny Lau]

if lean already knows foo : Polynomial (Fin 37)

[Jovan Gerbscheid]

But if Lean already knows it, then why write the type annotation?

[Kenny Lau]

i don't really see the harm in permitting that

[Jovan Gerbscheid]

If we had declare_poly_vars Nat[t], then should _[t] mean the same as Nat[t]?

[Kenny Lau]

no

[Kenny Lau]

the special support only happens when you use _ in the command

[Jovan Gerbscheid]

Why not, Lean already has the information that t is a polynomial variable over Nat, so _[t] is uniquely determined to mean the name as Nat[t]. Or are you saying that this syntax won't be allowed?

[Kenny Lau]

i don't plan to add it

[Thomas Murrills]

This might be off-base, but have you tried wrapping polyesque (at one level or another) in atomic()? (The idea being that we want to insist on “full” backtracking if polyesque is attempted and fails.)

(This isn’t based on much more than seeing an intermediate error at the top level when unexpected, and might be redundant or the “wrong” solution if splitting into cases works; apologies, I’m on mobile at the moment. Just wanted to mention it in case it’s relevant. :) )

[Kenny Lau]

thanks for the suggestion

[Jovan Gerbscheid]

Looking in mathlib, I found this syntax, which looks promisingly similar to what we want:

@[inherit_doc OreLocalization]
scoped syntax:1075 term noWs atomic("[" term "⁻¹" noWs "]") : term
macro_rules | `($R[$S⁻¹]) => ``(OreLocalization $S $R)

(Though I wouldn't know where the atomic is supposed to go in general)

[Kenny Lau]

1075 looks like a hack

[Jovan Gerbscheid]

hmm, it is larger than max, so I think it should just be max :sweat_smile:

[Jovan Gerbscheid]

Also the first term should probably be term:max instead, but I think this notation hasn't been stress tested/used enough for that

[Jovan Gerbscheid]

Also, there is

@[inherit_doc AddMonoidAlgebra]
scoped syntax:max (priority := high) term noWs "[" term "]" : term

which doesn't even use atomic (but it is scoped)

[Kenny Lau]

Kenny Lau said:

so i would do:

local macro_rules | `(_[t]) => `(Polynomial _)
local macro_rules | `($i:ident[t]) => `(Polynomial $i)
local macro_rules | `(($u:term)[t]) => `(Polynomial ($u))

update: this approach now works!

[Jovan Gerbscheid]

You can drop the brackets in the last line right?

local macro_rules | `(($u:term)[t]) => `(Polynomial $u)

[Kenny Lau]

i suppose theoretically it is possible, i just wanted to be safer lol

[Jovan Gerbscheid]

Oh right, it will technically work, but could look a bit weird

[Kenny Lau]

@Jovan Gerbscheid i've pushed the new refactored code, i basically touched 90% of the lines

[Kenny Lau]

i'll get to your comments now but in the meantime you can also have a look again if you would like to

[Notification Bot]

Riccardo Brasca has marked this topic as resolved.

[Kenny Lau]

huh?

[Riccardo Brasca]

Sorry I didn't want to mark it as solved

[Notification Bot]

Riccardo Brasca has marked this topic as unresolved.

[Kenny Lau]

The linter is complaining that the repr functions have an unused prec : Nat argument. How do I disable the linter?

[Aaron Liu]

take a _ : Nat argument instead?

[Jovan Gerbscheid]

For simpNF, we use the @[nolint simpNF] attribute. I presume the same could work here, to tag those declarations. I think this is a new issue since the new toolchain.

[Kenny Lau]

@Aaron Liu they are auto generated using deriving Repr

[Aaron Liu]

oh no

[Kenny Lau]

@Jovan Gerbscheid is there a solution without importing Batteries.Tactic.Lint.Basic?

[Jovan Gerbscheid]

Probably not. You can add a comment to the import that it is a workaround

[Kenny Lau]

do you know anyone who might be interested to solve this issue?

[Jovan Gerbscheid]

Well, or just not deriving Repr :)

[Kenny Lau]

that works for me

[Jovan Gerbscheid]

It seems likely someone has taken a look at the problem or filed an issue already given how easy it is to encounter :man_shrugging:

[Kenny Lau]

well, it's also likely that the repr deriver is in core and the lint is in batteries and they have conflicting interests

[Jovan Gerbscheid]

Do we have a strategy for delaborating these notations? The problem is that there are not enough explicit arguments to figure out the types of the terms, so on the syntax level, we can't figure out which polynomial variable we are supposed to use.

[Kenny Lau]

I don't even know how that would be done in theory, last time we looked into this we pretty much gave up, I don't think there's a way to 1. make a delaborator trigger conditionally (as opposed to triggered by every instance of vecCons), and 2. make it match on a declared free variable (need to make it output true for Polynomial R but false for Polynomial Nat, where R is introduced as variable (R : Type))

[Kenny Lau]

consider the following challenge:

axiom Polynomial : Type -> Type

[insert code here]

variable (R S : Type)
#declare R
#check Polynomial R -- R[t]
#check Polynomial S -- Polynomial S

[Kenny Lau]

@Jovan Gerbscheid can you add code to the [insert code here] so that the two #check commands output the thing in the comment?

[Kenny Lau]

@Jovan Gerbscheid can you PR to my PR?

[Jovan Gerbscheid]

Here's a solution:

import Lean
open Lean Elab Command Parser.Tactic

axiom Polynomial : Type -> Type

declare_syntax_cat poly_var
syntax "t" : poly_var
syntax (name := test) (priority := high) ident "[" poly_var "]" : term

-- @[app_unexpander Polynomial]
-- def bar : Lean.PrettyPrinter.Unexpander
--   | `($_ $nat:ident) => match nat with
--     | `(Nat) => `($nat:ident[t])
--     | _ => throw ()
--   | _ => throw ()

-- #check Polynomial Nat -- Nat[t]

elab "declare" id:ident : command => do
  elabCommand (← `(command|
    @[app_unexpander Polynomial]
    def foo : Lean.PrettyPrinter.Unexpander
      | `($$_ $$R:ident) => match R with
        | `($id) => `($$R:ident[t])
        | _ => throw ()
      | _ => throw ()))

variable (R S : Type)
declare R
#check Polynomial R -- R[t]
#check Polynomial S -- Polynomial S

[Kenny Lau]

interesting

[Kenny Lau]

looks like we can once again avoid env ext!

[Kenny Lau]

is that stackable?

[Kenny Lau]

it is!

[Jovan Gerbscheid]

It should probably be marked private/local

[Kenny Lau]

I was about to ask, how does it work at all? I do #check foo and it doesn't show anything

[Kenny Lau]

yeah looks like anything eval'ed is passed through some hygiene

[Jovan Gerbscheid]

Yes it gets some hygienic macro scope attached to foo

[Jovan Gerbscheid]

Jovan Gerbscheid said:

It should probably be marked private/local

@[local app_unexpander Polynomial] seems to do the trick

[Jovan Gerbscheid]

Although there is no harm in also making it a private def

[Kenny Lau]

import Lean
open Lean Elab Command Parser.Tactic

axiom Polynomial : Type -> Type

declare_syntax_cat poly_var
syntax "t" : poly_var
syntax (name := test) (priority := high) (ident <|> atomic("(" term ")")) atomic("[" poly_var "]") : term

elab "declare " id:ident : command => do
  elabCommand (← `(command|
    @[app_unexpander Polynomial]
    def foo : Lean.PrettyPrinter.Unexpander
      | `($$_ $$R:ident) => match R with
        | `($id) => `($$R:ident[t])
        | _ => throw ()
      | _ => throw ()))
  elabCommand <| ← `(command| #check foo)

elab "declare' " "(" u:term ")" : command => do
  elabCommand (← `(command|
    @[app_unexpander Polynomial]
    def foo : Lean.PrettyPrinter.Unexpander
      | `($$_ $$u:term) => match u with
        | `($u) => `(($$u:term)[t])
        | _ => throw ()
      | _ => throw ()))
  elabCommand <| ← `(command| #check foo)

variable (R S T : Type)
declare R
declare S
declare' (Nat)
#check Polynomial R -- R[t]
#check Polynomial S -- S[t]
#check Polynomial T -- Polynomial T
#check Polynomial Nat -- (Nat)[t]

[Kenny Lau]

uh it seems to be not stackable the other way...

import Lean
open Lean Elab Command Parser.Tactic

axiom Polynomial : Type -> Type

declare_syntax_cat poly_var
syntax "t" : poly_var
syntax (name := test) (priority := high) (ident <|> atomic("(" term ")")) atomic("[" poly_var "]") : term

elab "declare' " u:term : command => do
  elabCommand (← `(command|
    @[app_unexpander Polynomial]
    def foo : Lean.PrettyPrinter.Unexpander
      | `(Polynomial (Polynomial $$u:term)) => match u with
        | `($u) => `(($$u:term)[t])
        | _ => throw ()
      | _ => throw ()))
  elabCommand <| ← `(command| #check foo)

declare' Nat
#check Polynomial (Polynomial Nat)
-- expected: (Nat)[t]
-- actual: Polynomial (Polynomial Nat)

[Jovan Gerbscheid]

It seems to work if you split the matching up. Maybe it hasn't inserted parentheses yet in the syntax at this point.

elab "declare' " u:term : command => do
  elabCommand (← `(command|
    @[app_unexpander Polynomial]
    def foo : Lean.PrettyPrinter.Unexpander
      | `(Polynomial $$v) => match v with
        | `(Polynomial $$u) => match u with
          | `($u) => `(($$u:term)[t])
          | _ => throw ()
        | _ => throw ()
      | _ => throw ()))
  elabCommand <| ← `(command| #check foo)

Also using u to mean two things here is quite confusing.

[Kenny Lau]

oh no, custom matching...

[Kenny Lau]

how do i make it match n times?

[Jovan Gerbscheid]

Recursively construct the above syntax? :melting_face:

[Aaron Liu]

this is all quite cursed

[Kenny Lau]

right, it's just a function Syntax -> PrettyPrinter.UnexpandM Syntax right

[Kenny Lau]

i can builid any function i want

[Aaron Liu]

yes you can

[Kenny Lau]

Jovan Gerbscheid said:

It seems to work if you split the matching up. Maybe it hasn't inserted parentheses yet in the syntax at this point.

I think I want to understand this more first.

[Kenny Lau]

is there no way to put in parentheses that are not supposed to be part of syntax?

[Kenny Lau]

also is there anyway to put debugging things inside Unexpander? it's complaining failed to synthesize
MonadTrace PrettyPrinter.UnexpandM

[Aaron Liu]

what I do is I put the thing I want into the output syntax

[Kenny Lau]

ah right ok that works

[Jovan Gerbscheid]

If you can construct the syntax without parentheses in the syntax, then you can do it without nested matches. For example:

elab "declare' " u:term : command => do
  elabCommand (← `(command|
    @[app_unexpander Polynomial]
    def foo : Lean.PrettyPrinter.Unexpander
      | `(Polynomial $(← `(Polynomial $$u))) => match u with
        | `($u) => `(($$u:term)[t])
        | _ => throw ()
      | _ => throw ()))
  elabCommand <| ← `(command| #check foo)

[Kenny Lau]

oh god

[Kenny Lau]

yeah actually i think i can do that

[Kenny Lau]

i think it's exactly the functor that i already have

[Kenny Lau]

@Jovan Gerbscheid well there's a side effect that I need to obtain the functor as an ident in order to use it in @[app_unexpander Polynomial] but currently I take in the functor (e.g. MvPolynomial) as a term

[Kenny Lau]

this is because MvPowerSeries.C used to take in an extra argument so it had to be passed in as (MvPowerSeries.C _) (fixed a month ago)

[Kenny Lau]

like, i'm sure it's fine with the current 6 functors (lol) that their functors are actually usable as ident

[Jovan Gerbscheid]

What do you mean with taking the functor as an ident?

[Kenny Lau]

so currently the syntax is register_poly_vars "[" "]" Polynomial Polynomial.C Polynomial.X

[Aaron Liu]

the @[app_unexpander foobar] syntax expects foobar to be an ident

[Kenny Lau]

the Polynomial there is taken in as a term:max currently

[Jovan Gerbscheid]

If you think there are real use cases where it is not an ident, then I would suggest not implementing the unexpander for those cases. You can do a match to get the ident if it is an ident.

[Kenny Lau]

i don't think there are real use cases where it is not an ident (idk how many more functors we'll get) but i guess it's a good idea to do the matching in any case

[Kenny Lau]

are there more functors than the 6?

[Jovan Gerbscheid]

The easier thing is to just ask for an ident directly. And also for Polynomial.X and Polynomial.C

[Kenny Lau]

as I explained earlier, that would not have worked one month ago

[Jovan Gerbscheid]

Good thing it works now :)

[Kenny Lau]

well...

[Jovan Gerbscheid]

Which 6 are we talking about by the way? I knew about Polynomial, Powerseries and the multivariate versions

[Kenny Lau]

R[t] ((mv) polynomial)
R[[t]] ((mv) power series)
R(t) (rat func)
R((t)) (laurent series)

[Aaron Liu]

docs#RatFunc

[Aaron Liu]

docs#LaurentSeries

[Jovan Gerbscheid]

Ah right, so we have 4 * 2 = 8?

[Kenny Lau]

last two have no mv version (yet)

[Aaron Liu]

oh no

[Jovan Gerbscheid]

That sounds like missing API!

[Aaron Liu]

it's not missing until someone needs them

[Kenny Lau]

btw will anyone complain if i leave the name of the unexpander as foo

[Aaron Liu]

what are you naming foo

[Aaron Liu]

can you name it something reasonable

[Jovan Gerbscheid]

It will be a private def and it will get macro scopes, but at least maybe give it a descriptive name like unexpand.

[Jovan Gerbscheid]

If you want to mimic how notation does it, then use aux_def:

elab "declare" id:ident : command => do
  elabCommand (← `(command|
    @[local app_unexpander Polynomial]
    private aux_def unexpand Polynomial : Lean.PrettyPrinter.Unexpander := fun
      | `($$_ $$R:ident) => match R with
        | `($id) => `($$R:ident[t])
        | _ => throw ()
      | _ => throw ()))

[Kenny Lau]

so now my code works for polynomial but fails for polynomial, so i turned everything to string, the pattern in the unexpander is:

(Term.app
     `Polynomial
     [(Term.app
       (Term.app `MvPolynomial [(Term.app `Fin._@.MathlibTest.NamePolyVars.3111633584._hygCtx._hyg.2 [(num "2")])])
       [(ident.antiquot "$" [] `i._@.MathlibTest.NamePolyVars.3111633584._hygCtx._hyg.2 (antiquotName ":" "ident"))])])

and the actual term to be matched is:

(Term.app `Polynomial [(Term.app `MvPolynomial [(Term.app `Fin [(num \"2\")]) `R])])

[Kenny Lau]

they kinda look the same, is Fin the problematic part? but the forward elaboration uses Fin too and there's no problem

[Kenny Lau]

how do I tell Lean that Fin is just Fin?

[Jovan Gerbscheid]

Does it work if you replace Fin by $$_?

[Jovan Gerbscheid]

Kenny Lau said:

how do I tell Lean that Fin is just Fin?

I think you can use $(mkIdent ``Fin)

[Kim Morrison]

I haven't been reading all this, but: please don't overload or complicate the meaning of [ ]. These are for constructing lists, and getelem notation, and everyone else should be using other symbols.

[Aaron Liu]

but it's what mathematicians write on paper

[Kenny Lau]

i'm sure mathlib would disagree and say that it's the notation for polynomial

[Kenny Lau]

btw it's also used in OreLocalization and AddMonoidAlgebra

[Jovan Gerbscheid]

Note that this particular notation has to be turned on locally using a command, so there is no need to worry about it accidentally popping up in usual getelem notation. (Similarly with (Add)MonoidAlgebra and OreLocalization, which are scoped)

[Kim Morrison]

Yes, it's of course what we write on paper, but it's not what we should write in Lean. :woman_shrugging:

[Kenny Lau]

bruh i found out what caused the issue

[Kenny Lau]

Term.app a [b c] doesn't match Term.app (Term.app a [b]) [c]

[Kenny Lau]

import Lean

axiom MvPolynomial : Type → Type → Type

open Lean Elab Command

elab "#declare" : command => do
  let t₁₁ : Term ← `(MvPolynomial Nat)
  let t₁₂ : Term ← `(Nat)
  let t₁ : Term ← `($t₁₁ $t₁₂) -- Term.app (Term.app a [b]) [c]
  let t₂ : Term := ← `(MvPolynomial Nat Nat) -- Term.app a [b c]
  elabCommand <| ← `(command|
    @[local app_unexpander MvPolynomial]
    def unexpand : Lean.PrettyPrinter.Unexpander
      | `($t₁) => `("1")
      | `($t₂) => `("2")
      | _ => `("3"))

#declare
#check MvPolynomial Nat Nat -- guess the output

[Kenny Lau]

minimised

[Kenny Lau]

great so now that's fixed, but now a new problem arised, it adds a dagger

[Jovan Gerbscheid]

Where does it add a dagger?

[Kenny Lau]

import Lean

axiom Polynomial : Type → Type

open Lean Elab Command

elab "#declare" i:ident : command => do
  let term : Term ← `(Polynomial $i)
  elabCommand <| ← `(command|
    @[local app_unexpander Polynomial]
    def unexpand : Lean.PrettyPrinter.Unexpander
      | `($term) => `($i)
      | _ => `("3"))

variable (R : Type)
#declare R
#check Polynomial R -- R✝ : Type

[Kenny Lau]

minimised

[Kenny Lau]

further minimised:

import Lean

axiom Polynomial : Type → Type

open Lean Elab Command

variable (R : Type)

@[local app_unexpander Polynomial]
def unexpand : Lean.PrettyPrinter.Unexpander
  | `(Polynomial R) => `(R)
  | _ => `("3")

#check Polynomial R -- R✝ : Type

[Jovan Gerbscheid]

I think this is why I had the double match in my version. I want to return the R form the Polynomial R syntax that the user wrote down. You are returning the R from the #declare command.

[Kenny Lau]

aha ok so this works:

import Lean

axiom Polynomial : Type → Type

open Lean Elab Command

variable (R : Type)

@[local app_unexpander Polynomial]
def unexpand : Lean.PrettyPrinter.Unexpander
  | `(Polynomial $i:ident) => match i with
    | `(R) => `($i)
    | _ => `("2")
  | _ => `("3")

#check Polynomial R -- R : Type

[Kenny Lau]

right i guess i understand why you need to match twice

[Robin Arnez]

But don't match on Polynomial:

Unexpanders should match the function name against an antiquotation $_ so as to be independent of the specific pretty printing of the name.

Note: This linter can be disabled with set_option linter.suspiciousUnexpanderPatterns false

I don't know why the linter warning disappears when you use local app_unexpander

[Kenny Lau]

yeah i saw that warning but it's a little bit more complicated to change it to $_

[Robin Arnez]

Really? Why so?

[Robin Arnez]

You mean because of nesting..?

[Kenny Lau]

it's not impossible, it's just more code

[Kenny Lau]

everything you see here is dynamically generated

[Kenny Lau]

and i don't see people changing Polynomial

[Jovan Gerbscheid]

The real issue is the nesting, because in Polynomial (Polynomial _) I think we really do need to match on the second Polynomial

[Robin Arnez]

Well I guess this could be a concern:

namespace A

axiom Polynomial : Nat

-- doesn't trigger unexpander when matching on `Polynomial`
#check _root_.Polynomial R -- _root_.Polynomial R : Type

but really, this will probably not be relevant

[Kenny Lau]

i mean, the warning is also very specific, there are other ways to change the pretty printing other than just changing the initial constant?

[Robin Arnez]

Well, when using app_unexpander I believe it guarantees that you get an app node with all of the explicit arguments. The individual arguments may be pretty-printed in any weird way though, yes

[Jovan Gerbscheid]

Well, it also gets messed up by set_option pp.explicit true. But I don't think that's a problem

[Kenny Lau]

maybe that's a feature!

[Jovan Gerbscheid]

It does have the funny side effect that Polynomial (R : Type) [Semiring R] : Type and Polynomial (R : Type) : Type behave differently in this scenario.

[Kenny Lau]

@Jovan Gerbscheid I have pushed the unexpander. Not sure if you missed the previous message, but could you please PR to my PR?

[Kenny Lau]

Jovan Gerbscheid said:

It does have the funny side effect that Polynomial (R : Type) [Semiring R] : Type and Polynomial (R : Type) : Type behave differently in this scenario.

I've added Semiring to the tests

[Jovan Gerbscheid]

Here's the PR: https://github.com/kckennylau/mathlib4/pull/14

[Kenny Lau]

thanks!

[Jovan Gerbscheid]

(I'll work out the merge conflict)

[Robin Arnez]

Jovan Gerbscheid schrieb:

Well, it also gets messed up by set_option pp.explicit true. But I don't think that's a problem

Doesn't it just not use unexpanders with pp.explicit?

[Jovan Gerbscheid]

Oh yeah you're right

[Jovan Gerbscheid]

Here's another: https://github.com/kckennylau/mathlib4/pull/15

[Kenny Lau]

thanks!

[Kenny Lau]

@Jovan Gerbscheid uh... why do you want to ban _[x,y]?

[Jovan Gerbscheid]

I want to ban if from the unexpander, because I don't think that the pretty printer will ever produce a _.

[Jovan Gerbscheid]

Also, for the _ in the macro for _[x,y], I made it so that the newly produced syntax contains the same _ as the original _[x,y] syntax, which is better for hover information

[Kenny Lau]

your PR contains

elabMacroRulesAndTrace (← `(polyesque| $$h:hole$body:polyesque_notation*)) (← `($$h:hole))

[Kenny Lau]

you changed the expander too

[Jovan Gerbscheid]

Oh oops

[Kenny Lau]

also, are all holes the same? (are all electrons the same?)

[Jovan Gerbscheid]

When you hover over a hole, you can often see how it was filled in by Lean, which is very useful :)

[Kenny Lau]

hmm i never knew that

[Kenny Lau]

oh wow it does work!

[Kenny Lau]

axiom T : Nat → Type
axiom Tn (n : Nat) : T n

noncomputable foo : T 3 :=
  Tn _

[Kenny Lau]

Jovan Gerbscheid said:

I want to ban if from the unexpander, because I don't think that the pretty printer will ever produce a _.

axiom Polynomial : Type → Type

@[app_unexpander Polynomial]
def unexpand : Lean.PrettyPrinter.Unexpander
  | x => `($(Lean.Quote.quote s!"{x}"))

#check Polynomial _
-- "(Term.app `Polynomial [(Term.syntheticHole \"?\" `m.1)])" : Type

[Kenny Lau]

is this a hole?

[Jovan Gerbscheid]

No, ?m.1 is not a syntactic hole. A syntactic hole is just _.

[Kenny Lau]

interesting

[Kenny Lau]

axiom Polynomial : Type → Type

@[app_unexpander Polynomial]
def unexpand : Lean.PrettyPrinter.Unexpander
  | `(Polynomial $h:hole) => `($(Lean.Quote.quote s!"h: {h}"))
  | `(Polynomial $i:ident) => `($(Lean.Quote.quote s!"i: {i}"))
  | `(Polynomial $t:term) => `($(Lean.Quote.quote s!"t: {t}"))
  | x => `($(Lean.Quote.quote s!"x: {x}"))

#check Polynomial _ -- "t: (Term.syntheticHole \"?\" `m.1)" : Type

[Kenny Lau]

yep you're right

[Kenny Lau]

it would be very funny to see (?m.1)[t] though

[Jovan Gerbscheid]

I'm testing it and seeing (?m.145 this✝² this✝¹ this✝ this)[a,b][C] = (?m.147 this✝² this✝¹ this✝ this)[a,b][C] :)

[Jovan Gerbscheid]

I think the last main challenge is to get the delaborator for the polynomial variables to work. It would be great if we could do this in the same way as with the polynomial types. But the problem is that there is some information missing in the syntax.

variable (R S : Type) [Semiring R] [Semiring S]

name_poly_vars R[x]
name_poly_vars S[y]

#check x -- Polynomial.X : R[x]
#check y -- Polynomial.X : S[y]

As you can see, x and y are currently printed the same by the pretty printer.

So we will need to write a delab instead of a app_unexpander. I imagine it like this:

1. Delaborate the term as usual
2. Delaborate the type of the term
3. Do a match with the syntax of the term and the type. If it matches one of the declared variables, then return that variable. Otherwise return the term syntax.

This delaborator would be tagged with @[app_delab Polynomial.X] and @[app_delab Polynomial.C] and friends.

[Kenny Lau]

are Polynomial.X and R[x] treated separately?

[Jovan Gerbscheid]

In what sense?

[Kenny Lau]

well i see them together in the #check output

[Jovan Gerbscheid]

Polynomial.X is what it delaborates to. R[x] is what the type delaborates to.

[Kenny Lau]

hmm...

[Kenny Lau]

so how do you access the type?

[Kenny Lau]

i guess u need to use inferType etc?

[Jovan Gerbscheid]

In a delaborator, you get access to the Expr, so you can do inferType. Then we can delaborate both it and its type.

[Kenny Lau]

how do delab and unexpander interact?

[Jovan Gerbscheid]

delab happens first, and then the unexpanders

[Kenny Lau]

delab is Expr -> Syntax?

[Jovan Gerbscheid]

Exactly

[Kenny Lau]

then why don't we use delab for R[x,y] too?

[Jovan Gerbscheid]

You mentioned earlier that you want this stuff to operate on the syntax level and not on the expression level. So this is what is most convenient with that constraint.

I could also imagine an implementation where we would do some Expr matching instead of Syntax matching, which would then live naturally in a delab

[Kenny Lau]

@Jovan Gerbscheid can we import Batteries.Tactic.Lint.Misc instead of Mathlib.Init?

[Jovan Gerbscheid]

Every file in Mathlib has to import Mathlib.Init

[Kenny Lau]

then why didn't it complain before?

[Jovan Gerbscheid]

Maybe we don't have automation that checks this?

[Kenny Lau]

so what you said is like a policy that is not checked by CI?

[Jovan Gerbscheid]

Hmm, good question. I think it would be good to have a linter that checks that every file imports, or is imported by, Mathlib.Init.

[Kenny Lau]

also please check my comment on https://github.com/kckennylau/mathlib4/pull/15/files

[Kenny Lau]

@Jovan Gerbscheid I don't understand what's happening here, why is

local macro_rules | `(t) => `((Polynomial.X : _))`

better than

local macro_rules | `(t) => `((Polynomial.X : Polynomial _))`

?

[Jovan Gerbscheid]

Oh sorry, I think I messed that up

[Jovan Gerbscheid]

pushed a fix

[Kenny Lau]

thanks!

[Jovan Gerbscheid]

Should we also allow the space-separated syntax name_poly_vars R[a,b][C] _[x,y,z]?

[Kenny Lau]

uh... i don't know

[Kenny Lau]

import Mathlib.Init

@[class] axiom Semiring : Type → Type

axiom Polynomial (R : Type) [Semiring R] : Type
axiom Polynomial.C {R : Type} [Semiring R] : R → Polynomial R
axiom Polynomial.X {R : Type} [Semiring R] : Polynomial R

axiom MvPolynomial (σ R : Type) [Semiring R] : Type
axiom MvPolynomial.C {σ R : Type} [Semiring R] : R → MvPolynomial σ R
axiom MvPolynomial.X {σ R : Type} [Semiring R] (i : σ) : MvPolynomial σ R

@[instance] axiom Nat.semiring : Semiring Nat

open Lean PrettyPrinter.Delaborator Elab Term

syntax poly_var := "t"
syntax poly_var : term
syntax ident "[" poly_var "]" : term

@[app_delab Polynomial.X] def foo : Delab := do
  let e ← SubExpr.getExpr
  let eT ← Lean.Meta.inferType e
  let type ← `(Polynomial Nat) -- the target type
  let typeE ← Lean.Elab.Term.elabTerm type none
  if ← Lean.Meta.isDefEq eT typeE then
    -- todo: match `e` as well
    `(t)
  else delab

#check Polynomial.X
#check (Polynomial.X : Polynomial Nat)

[Kenny Lau]

@Jovan Gerbscheid hi i'm having problem here because TermElabM and DelabM are incompatible monads

[Kenny Lau]

image.png

[Jovan Gerbscheid]

Well, we want to delab and not to elab

[Kenny Lau]

yes, but my strategy is to first elab `(Polynomial Nat) and see if it matches the given tyype of the given expression

[Jovan Gerbscheid]

Oh huh, I see. My idea was to delab the type, and see if it matches with `(Polynomial Nat)

[Kenny Lau]

that sounds bad

[Kenny Lau]

as we saw earlier (MvPolynomial (Fin 2)) R and MvPolynomial (Fin 2) R are different syntaxes

[Jovan Gerbscheid]

I thought you said a while ago that you didn't want to elab things because you wanted to do everything at the syntax level

[Kenny Lau]

maybe syntax is just bad

[Kenny Lau]

will it convert it to Nat[t]?

[Jovan Gerbscheid]

Kenny Lau said:

as we saw earlier (MvPolynomial (Fin 2)) R and MvPolynomial (Fin 2) R are different syntaxes

But we know how to deal with this right? I.e. always use MVPolynomial (Fin 2) R

[Jovan Gerbscheid]

Kenny Lau said:

will it convert it to Nat[t]?

Oh that's a good point

[Kenny Lau]

also how do i call the delaborator? to my surprise Delab is not defined as Expr -> DelabM Term

[Kenny Lau]

but rather you need to access the Expr via (<- getExpr)

[Jovan Gerbscheid]

Although I'm not sure now, since I said earlier that delab runs before the app unexpanders

[Kenny Lau]

Jovan Gerbscheid said:

you wanted to do everything at the syntax level

I wanted to do Syntax -> CoreM Syntax at the syntax level, but now we're building a function Expr -> DelabM Syntax so it makes sense to do things at the Expr level? idk

[Jovan Gerbscheid]

I think you can do withType delab, and it will give you the delaborated type.

[Jovan Gerbscheid]

However to delaborate the expression itself, you want to just call delab, but that will cause an infinite loop...

[Kenny Lau]

I just want to call delab with a custom Expr

[Kenny Lau]

I still feel like it makes sense to call elab rather than call delab

[Jovan Gerbscheid]

Kenny Lau said:

I just want to call delab with a custom Expr

It doesn't work like that, because the delaborator doesn't just create the Syntax, it also creates hover information, and this information is tied to locations in the Expr, and to locations in the Syntax and the monad keeps track of all of this.

[Kenny Lau]

i mean intuitively i'm doing:

1. given the expression to delaborate,
2. check if t elaborates to the given expression (matching type)
3. if yes, return t
4. otherwise use the default delaborator

[Kenny Lau]

Jovan Gerbscheid said:

It doesn't work like that

ok, so surely it makes sense to elab?

[Jovan Gerbscheid]

Are you planning to do Expr matching for both the expression itself and for its type?

[Kenny Lau]

oh look Lean.PrettyPrinter.delab exists and is exactly what i'm looking for

[Jovan Gerbscheid]

Because at that point, just doing Expr matching with the expression itself is enough

[Kenny Lau]

how do i check if two Terms are the same?

[Jovan Gerbscheid]

The bad way would be try elabCommand (← `(example : $stx1 = $stx2 := rfl)) :laughing:

[Kenny Lau]

well it looks like Lean.Syntax.structEq is what i'm looking for and it's also the BEq instance

[Kenny Lau]

nope that doesn't ignore hygiene

[Kenny Lau]

maybe your way is the correct way

[Jovan Gerbscheid]

Well that way is bad because we were explicitly trying to avoid elaboration

[Kenny Lau]

ah no i know how to do it now

[Kenny Lau]

one of them is now an explicit pattern

[Kenny Lau]

import Mathlib.Init

@[class] axiom Semiring : Type → Type

axiom Polynomial (R : Type) [Semiring R] : Type
axiom Polynomial.C {R : Type} [Semiring R] : R → Polynomial R
axiom Polynomial.X {R : Type} [Semiring R] : Polynomial R

axiom MvPolynomial (σ R : Type) [Semiring R] : Type
axiom MvPolynomial.C {σ R : Type} [Semiring R] : R → MvPolynomial σ R
axiom MvPolynomial.X {σ R : Type} [Semiring R] (i : σ) : MvPolynomial σ R

@[instance] axiom Nat.semiring : Semiring Nat

open Lean PrettyPrinter.Delaborator Elab Term

syntax poly_var := "t"
syntax poly_var : term
syntax ident "[" poly_var "]" : term

@[app_delab Polynomial.X] def foo : Delab := do
  let e ← SubExpr.getExpr
  let eT ← Lean.Meta.inferType e
  let eTS ← PrettyPrinter.delab eT
  if let `(Polynomial Nat) := eTS then -- the target type as an explicit pattern
    -- todo: match `e` as well
    `(t)
  else delab

#check Polynomial.X
#check (Polynomial.X : Polynomial Nat)

[Kenny Lau]

this works!

[Kenny Lau]

@Jovan Gerbscheid are you happy with this code?

[Jovan Gerbscheid]

How are you planning to make the if let `(Polynomial Nat) := eTS then work in general though?

[Kenny Lau]

i have that explicit pattern in general

[Kenny Lau]

that's the typeIdent

[Jovan Gerbscheid]

But how does that deal with nested things like Polynomial (MvPolynomial (Fin 4) _)?

[Kenny Lau]

that is still one pattern

[Jovan Gerbscheid]

Aha, I had thought that this would be a globally defined delaborator, but you want to generate one on the fly for each variable defined with declare_poly_vars.

[Kenny Lau]

yes

[Kenny Lau]

oh no trying to match e sends it to stackoverflow because delab calls this function again

[Kenny Lau]

is there a way to tell delab to not call this function?

[Jovan Gerbscheid]

A hacky way to accomplish this is to define a Boolean Lean.Option (like the ones used in set_option). Then it is false by default, but you set it to true when calling the delaborator recursively.

[Kenny Lau]

how do other applications do it?

[Kenny Lau]

or is this cutting edge?

[Jovan Gerbscheid]

The other applications use app unexpanders :laughing:

[Kenny Lau]

i think i'm running into brackets problems again, can i tell `() to not use brackets?

[Jovan Gerbscheid]

You can use separate `() blocks, if that's what you mean. And then put the result of one in the other, so that you don't need to write brackets explicitly.

[Jovan Gerbscheid]

Essentially $(← `(...)) is a way to write bracketless brackets

[Kenny Lau]

if i do that it tells me i can't use bind there; if i build the term before that it tells me redundant alternative

[Jovan Gerbscheid]

The error about not being able to use ← under binders can be fixed by moving the ← to outside the binder

[Kenny Lau]

please have a look at the codes:

[Kenny Lau]

import Mathlib.Init

axiom Real : Type
@[class] axiom Semiring : Type → Type

axiom Polynomial (R : Type) [Semiring R] : Type
axiom Polynomial.C {R : Type} [Semiring R] : R → Polynomial R
axiom Polynomial.X {R : Type} [Semiring R] : Polynomial R

axiom MvPolynomial (σ R : Type) [Semiring R] : Type
axiom MvPolynomial.C {σ R : Type} [Semiring R] : R → MvPolynomial σ R
axiom MvPolynomial.X {σ R : Type} [Semiring R] (i : σ) : MvPolynomial σ R

@[instance] axiom Nat.semiring : Semiring Nat
@[instance] axiom Real.semiring : Semiring Real
@[instance] axiom Polynomial.semiring (R : Type) [Semiring R] : Semiring (Polynomial R)
@[instance] axiom MvPolynomial.semiring (σ R : Type) [Semiring R] : Semiring (MvPolynomial σ R)

open Lean PrettyPrinter.Delaborator Elab Term

syntax poly_var := "a" <|> "b" <|> "c"
syntax poly_var : term
syntax ident "[" poly_var "]" : term

@[app_delab Polynomial.X] def delabC : Delab := do
  let e ← SubExpr.getExpr
  let eT ← Lean.Meta.inferType e
  let eTS ← PrettyPrinter.delab eT
  let t₁ ← `(Fin 2)
  let t₂ ← `(MvPolynomial $t₁ Nat)
  let t₃ ← `(Polynomial $t₂)
  if let `($t₃) := eTS then -- the target type as an explicit pattern
    -- if let `(Polynomial.X) := eS then
    `(c)
  else `("1")

-- @[app_delab MvPolynomial.X] def delabA : Delab := do

-- Nat[a,b][c]

#check (Polynomial.X : Polynomial (MvPolynomial (Fin 2) Nat))
#check (Polynomial.X : Polynomial (MvPolynomial (Fin 2) Real))

"redundant alternative"

[Kenny Lau]

import Mathlib.Init

axiom Real : Type
@[class] axiom Semiring : Type → Type

axiom Polynomial (R : Type) [Semiring R] : Type
axiom Polynomial.C {R : Type} [Semiring R] : R → Polynomial R
axiom Polynomial.X {R : Type} [Semiring R] : Polynomial R

axiom MvPolynomial (σ R : Type) [Semiring R] : Type
axiom MvPolynomial.C {σ R : Type} [Semiring R] : R → MvPolynomial σ R
axiom MvPolynomial.X {σ R : Type} [Semiring R] (i : σ) : MvPolynomial σ R

@[instance] axiom Nat.semiring : Semiring Nat
@[instance] axiom Real.semiring : Semiring Real
@[instance] axiom Polynomial.semiring (R : Type) [Semiring R] : Semiring (Polynomial R)
@[instance] axiom MvPolynomial.semiring (σ R : Type) [Semiring R] : Semiring (MvPolynomial σ R)

open Lean PrettyPrinter.Delaborator Elab Term

syntax poly_var := "a" <|> "b" <|> "c"
syntax poly_var : term
syntax ident "[" poly_var "]" : term

@[app_delab Polynomial.X] def delabC : Delab := do
  let e ← SubExpr.getExpr
  let eT ← Lean.Meta.inferType e
  let eTS ← PrettyPrinter.delab eT
  let t₁ ← `(Fin 2)
  let t₂ ← `(MvPolynomial $t₁ Nat)
  let t₃ ← `(Polynomial $t₂)
  if let `(Polynomial $(← `(MvPolynomial $(← `(Fin 2)) Nat))) := eTS then -- the target type as an explicit pattern
    -- if let `(Polynomial.X) := eS then
    `(c)
  else `("1")

-- @[app_delab MvPolynomial.X] def delabA : Delab := do

-- Nat[a,b][c]

#check (Polynomial.X : Polynomial (MvPolynomial (Fin 2) Nat))
#check (Polynomial.X : Polynomial (MvPolynomial (Fin 2) Real))

"<- over binder"

[Jovan Gerbscheid]

In the first option, I think you need to use double dollar signs: No that seems wrong

@[app_delab Polynomial.X] def delabC : Delab := do
  let e ← SubExpr.getExpr
  let eT ← Lean.Meta.inferType e
  let eTS ← PrettyPrinter.delab eT
  let t₁ ← `(Fin 2)
  let t₂ ← `(MvPolynomial $t₁ Nat)
  let t₃ ← `(Polynomial $t₂)
  if let `($$t₃) := eTS then -- the target type as an explicit pattern
    -- if let `(Polynomial.X) := eS then
    `(c)
  else `("1")

[Kenny Lau]

then both tests don't match (return "1")

[Jovan Gerbscheid]

Ok, so I think in this example, you are going to have to split up the match/if let into multiple parts, because I don't know how to not but the brackets there. But when you will be automatically generating this delaborator, I think you won't have this issue, because you will create the syntax with no brackets.

[Kenny Lau]

I think with this approach the t3 etc cease to be patterns and are now Lean objects of Term

[Kenny Lau]

i see

[Kenny Lau]

import Mathlib.Init

axiom Real : Type
@[class] axiom Semiring : Type → Type

axiom Polynomial (R : Type) [Semiring R] : Type
axiom Polynomial.C {R : Type} [Semiring R] : R → Polynomial R
axiom Polynomial.X {R : Type} [Semiring R] : Polynomial R

axiom MvPolynomial (σ R : Type) [Semiring R] : Type
axiom MvPolynomial.C {σ R : Type} [Semiring R] : R → MvPolynomial σ R
axiom MvPolynomial.X {σ R : Type} [Semiring R] (i : σ) : MvPolynomial σ R

@[instance] axiom Nat.semiring : Semiring Nat
@[instance] axiom Real.semiring : Semiring Real
@[instance] axiom Polynomial.semiring (R : Type) [Semiring R] : Semiring (Polynomial R)
@[instance] axiom MvPolynomial.semiring (σ R : Type) [Semiring R] : Semiring (MvPolynomial σ R)

open Lean PrettyPrinter.Delaborator Elab Term

syntax poly_var := "a" <|> "b" <|> "c"
syntax poly_var : term
syntax ident "[" poly_var "]" : term

elab "#declare" : command => do
  let t₁ ← `(Fin 2)
  let t₂ ← `(MvPolynomial $t₁ Nat)
  let t₃ ← `(Polynomial $t₂)
  Command.elabCommand <| ← `(command|
    @[app_delab Polynomial.X] def delabC : Delab := do
      let e ← SubExpr.getExpr
      let eT ← Lean.Meta.inferType e
      let eTS ← PrettyPrinter.delab eT
      if let `($t₃) := eTS then -- the target type as an explicit pattern
        `(c)
      else `("1")
  )
  -- Command.elabCommand <| ← `(command| #print delabC)

-- @[app_delab Polynomial.X] def delabC : Delab := do
--   let e ← SubExpr.getExpr
--   let eT ← Lean.Meta.inferType e
--   let eTS ← PrettyPrinter.delab eT
--   let t₁ ← `(Fin 2)
--   let t₂ ← `(MvPolynomial $t₁ Nat)
--   let t₃ ← `(Polynomial $t₂)
--   if let `($t₃) := eTS then -- the target type as an explicit pattern
--     -- if let `(Polynomial.X) := eS then
--     `(c)
--   else `("1")

-- @[app_delab MvPolynomial.X] def delabA : Delab := do

-- Nat[a,b][c]

#declare

#check (Polynomial.X : Polynomial (MvPolynomial (Fin 2) Nat))
#check (Polynomial.X : Polynomial (MvPolynomial (Fin 2) Real))

[Kenny Lau]

now Lean doesn't know what Polynomial.X is

[Kenny Lau]

the errors are getting stranger

[Kenny Lau]

"@[app_delab c] first performs name resolution on c in the current scope."

[Kenny Lau]

it seems like this might be the problem

[Kenny Lau]

it might be impossible to define app_delab dynamically

[Jovan Gerbscheid]

You should use $(mkIdent ``Polynomial.X) instead of Polynomial.X

[Jovan Gerbscheid]

Although it might work without the mkIdent when you already have the ident that was given by the user.

[Kenny Lau]

ah ok lemme try

[Kenny Lau]

is there a function that returns the "head" of a Term similar to Lean.Expr.getAppFn?

[Jovan Gerbscheid]

Head as in head of an application? You can do that with usual syntax matching.

[Kenny Lau]

well (a b) c and a b c are considered different syntaxes

[Kenny Lau]

you'll need to do like recursive syntax matching

[Kenny Lau]

also Term.app doesn't seem to be a constructor

[Kenny Lau]

import Mathlib.Init

namespace Lean.TSyntax

partial def getHead (t : Term) : Term :=
  match t with
  | `($a $_) => a.getHead
  | `(($a)) => a.getHead
  | x => x

end Lean.TSyntax

axiom A : Type → Type → Type

elab "get_head% " t:term:max : command => do
  let head := t.getHead
  Lean.logInfo head

get_head% (A Nat Nat) -- A Nat Nat
get_head% ((A Nat) Nat) -- A

[Kenny Lau]

I can't get it to work if it has multiple arguments

[Aaron Liu]

Look at the signature of app

[Aaron Liu]

You need to match the many arguments

[Kenny Lau]

I also can't find out anything about Term.app, the only result on loogle is Lean.Parser.Term.app which i don't think it's the real Term.app

[Kenny Lau]

I also can't match against Term.app a b directly

[Kenny Lau]

aha repr seems to return more info

[Jovan Gerbscheid]

You should match with `($f $args*)

[Jovan Gerbscheid]

The * is what @Aaron Liu means with the many arguments

[Kenny Lau]

aha, thanks!

[Kenny Lau]

how could i have found this out on my own?

[Jovan Gerbscheid]

Ehhh, by reading enough Lean source code I guess...

[Kenny Lau]

import Mathlib.Init

namespace Lean.TSyntax

partial def getHead (t : Term) : Term :=
  match t with
  | `(($a)) => a.getHead
  | `($f $_*) => f.getHead
  | x => x

end Lean.TSyntax

axiom A : Type → Type → Type
set_option pp.all true

elab "get_head% " t:term:max : command => do
  let head := t.getHead
  Lean.logInfo head

get_head% (A Nat Nat) -- A
get_head% ((A Nat) Nat) -- A

[Kenny Lau]

so now this works -- do we have any use for it?

[Jovan Gerbscheid]

Well that's what I wanted to ask - what do you need this for?

[Kenny Lau]

dynamically find out the head of the term in order to build the corresponding delab/unexpander dynamically

[Jovan Gerbscheid]

Oh, yeah that makes sense

[Jovan Gerbscheid]

I was still thinking that we could switch to taking the Polynomial.X and Polynomial.C as ident, so then we could just use that ident

[Kenny Lau]

btw don't run the following code :upside_down:

import Mathlib.Init

namespace Lean.TSyntax

partial def binaryHell : CoreM Term := do
  `($(← binaryHell) $(← binaryHell))

end Lean.TSyntax

elab "#explode" : command => do
  Lean.logInfo (← Lean.Elab.Command.liftCoreM Lean.TSyntax.binaryHell)

#explode

[Kenny Lau]

Jovan Gerbscheid said:

I was still thinking that we could switch to taking the Polynomial.X and Polynomial.C as ident, so then we could just use that ident

well I would repeat the argument that this would not have worked one month ago

[Kenny Lau]

(i.e. it seems less flexible)

[Kenny Lau]

what's wrong with using getHead?

[Jovan Gerbscheid]

Well and I would repeat the argument that it has been fixed one month ago, so we can use the fact that everything is good now...

[Jovan Gerbscheid]

Kenny Lau said:

what's wrong with using getHead?

There's nothing wrong with it, but if we didn't need to then it would be less code.

[Kenny Lau]

well what if someone in the future writes MvRatFunc.X with the wrong type signature

[Kenny Lau]

Jovan Gerbscheid said:

it would be less code

you still need some code to figure out the head of each expression

[Kenny Lau]

but now you're proposing to do it indirectly

[Kenny Lau]

not from the term we built, but from the syntax that was passed in the command

[Kenny Lau]

and not using a unified function, but by inspecting how we built the term

[Jovan Gerbscheid]

Kenny Lau said:

well what if someone in the future writes MvRatFunc.X with the wrong type signature

Well they wouldn't, because we have made a decision on what the mathlib standard is. So if they have a compelling argument why it should be different, then we should change it everywhere, which I don't see happening anymore.

[Kenny Lau]

also morally Polynomial is not just a simple function, it also implicitly takes in [Semiring R], so it's more than just the ident...

[Kenny Lau]

also what if someone figures out a way to unify all of those functors and now Polynomial R is instead BigFunctor .polynomial R

[Jovan Gerbscheid]

Well we kind of already have this. Polynomial R is secretly just AddMonoidAlgebra R Nat, but for some reason the arguments of AddMonoidAlgebra are backwards from what would be needed to make this notation work. And X is AddMonoidAlgebra.single 1 1, while C is AddMonoidAlgebra.single 0.

@Yaël Dillies has some plans to make Polynomial an abbrev for this.

But somehow I don't think that our notation is going to be that useful/intuitive for AddMonoidAlgebras.

[Jovan Gerbscheid]

I think it doesn't make much sense to make the notation more general/complicated for a use case that we don't even know about.

[Kenny Lau]

Jovan Gerbscheid said:

a use case that we don't even know about.

LaurentSeries has no .X, and in fact it's actually single 1 1

[Kenny Lau]

PowerSeries.coe_X

[Kenny Lau]

import Mathlib

#check PowerSeries
#check MvPowerSeries
#check Polynomial
#check MvPolynomial
#check RatFunc
#check LaurentSeries

#check PowerSeries.C
#check MvPowerSeries.C
#check Polynomial.C
#check MvPolynomial.C
#check RatFunc.C
#check LaurentSeries.C

#check PowerSeries.X
#check MvPowerSeries.X
#check Polynomial.X
#check MvPolynomial.X
#check RatFunc.X
#check LaurentSeries.X

[Kenny Lau]

Jovan Gerbscheid said:

it has been fixed one month ago

we shouldn't write code that depends on every part of mathlib cooperating with each other

[Jovan Gerbscheid]

Well, I guess LaurentSeries is a bit cursed then. If it is so little used that it doesn't have this API, then I wouldn't bother writing delaborators for it either.

[Jovan Gerbscheid]

Kenny Lau said:

we shouldn't write code that depends on every part of mathlib cooperating with each other

I think we should, no?

[Kenny Lau]

also even if we make them ident I still think we should be using getHead

[Jovan Gerbscheid]

I get now that there is an advantage to taking the X and C as a term, but I don't understand what you mean by using getHead on an ident

[Kenny Lau]

I'm proposing to use getHead on the expression Polynomial (MvPolynomial (Fin 2) R) in order to figure out the constant identifier Polynomial

[Kenny Lau]

instead of looking at the last step of the for loop when you receive the syntax R[a,b][c]

[Jovan Gerbscheid]

Kenny Lau said:

we shouldn't write code that depends on every part of mathlib cooperating with each other

I think if all of the parts of mathlib do the same things is different ways, it will become horribly unusable.

[Kenny Lau]

I agree, but they do, and we should be prepared

[Kenny Lau]

we can't make every PR depend on each other, then no PR will ever get merged

[Jovan Gerbscheid]

Kenny Lau said:

use getHead on the expression Polynomial (MvPolynomial (Fin 2) R)

That works too, it doesn't matter that much, but that does require defining getHead :)

[Kenny Lau]

which we will also use on every .C and .X expression

[Kenny Lau]

import Mathlib.Init

axiom Real : Type
@[class] axiom Semiring : Type → Type

axiom Polynomial (R : Type) [Semiring R] : Type
axiom Polynomial.C {R : Type} [Semiring R] : R → Polynomial R
axiom Polynomial.X {R : Type} [Semiring R] : Polynomial R

axiom MvPolynomial (σ R : Type) [Semiring R] : Type
axiom MvPolynomial.C {σ R : Type} [Semiring R] : R → MvPolynomial σ R
axiom MvPolynomial.X {σ R : Type} [Semiring R] (i : σ) : MvPolynomial σ R

@[instance] axiom Nat.semiring : Semiring Nat
@[instance] axiom Real.semiring : Semiring Real
@[instance] axiom Polynomial.semiring (R : Type) [Semiring R] : Semiring (Polynomial R)
@[instance] axiom MvPolynomial.semiring (σ R : Type) [Semiring R] : Semiring (MvPolynomial σ R)

open Lean PrettyPrinter.Delaborator Elab Term

namespace Lean.TSyntax

partial def getHead (t : Term) : Term :=
  match t with
  | `(($a)) => a.getHead
  | `($f $_*) => f.getHead
  | x => x

end Lean.TSyntax

syntax poly_var := "a" <|> "b" <|> "c"
syntax poly_var : term
syntax ident "[" poly_var "]" : term

elab "#make_delab" result:poly_var tgt:term:max poly:term:max : command => do
  let t₁ ← `(MvPolynomial $(← `(Fin 2)) Nat)
  let type ← `($poly $t₁)
  let `($tgtHead:ident) := tgt.getHead | return ()
  Command.elabCommand <| ← `(command|
    @[app_delab $tgtHead] def delab37 : Delab := do
      let e ← SubExpr.getExpr
      let eT ← Lean.Meta.inferType e
      let eTS ← PrettyPrinter.delab eT
      if let `($type) := eTS then -- the target type as an explicit pattern
        -- if let `($tgt) := eS then
        `($result:poly_var)
      else delab
  )

#make_delab c Polynomial.X Polynomial

#check (Polynomial.X : Polynomial (MvPolynomial (Fin 2) Nat))
#check (Polynomial.X : Polynomial (MvPolynomial (Fin 2) Real))

[Kenny Lau]

partially working code here

[Kenny Lau]

i haven't implemented the bool hack so that delab won't call itself

[Kenny Lau]

@Jovan Gerbscheid is this code good enough and would you like to write the bool hack?

[Jovan Gerbscheid]

Btw are you sure that you're not supposed to match the type with R[x]?

[Kenny Lau]

Jovan Gerbscheid said:

Btw are you sure that you're not supposed to match the type with R[x]?

well i was told that delab happens before unexpander

[Kenny Lau]

but it doesn't really matter, if it becomes R[x] then i can match that as well

[Kenny Lau]

i have access to both Terms

[Kenny Lau]

(typeIdent and polyesqueIdent)

[Jovan Gerbscheid]

Also I wonder if the Bool hack could cause unexpected problems...

[Kenny Lau]

who might know a non hacky way to do this?

[Aaron Liu]

Don't recursively call

[Kenny Lau]

what do i call instead?

[Aaron Liu]

no idea

[Aaron Liu]

This all seems very tricky

[Kenny Lau]

like, in the unexpander we had throw () to mean "don't use this unexpander"

[Kenny Lau]

but nobody has told me what the corresponding syntax is for delab

[Aaron Liu]

Use a delab

[Aaron Liu]

Kenny Lau said:

but nobody has told me what the corresponding syntax is for delab

Try failure

[Kenny Lau]

aha! that works, thanks

[Kenny Lau]

ah, ok, that works for the alternative, but i still need to actually call the "default" delab on this term

[Aaron Liu]

what do you mean

[Aaron Liu]

if you're running the delab function and it fails one delab it will try the next one

[Kenny Lau]

the algorithm is:

1. given expression e
2. find its type eT
3. delab eT using the default delab and see if it matches Polynomial Nat
4. delab e using the default delab and see if it matches Polynomial.X
5. if both are yes, then return t
6. otherwise use the default delab

[Kenny Lau]

so you've solved step 6, but there's still step 4

[Aaron Liu]

that seems like a bad algorithm

[Kenny Lau]

yeah maybe we should really convert syntax to expr instead of the other way

[Aaron Liu]

why are you running delab in the delab

[Aaron Liu]

I guess this issue is really complicated

[Kenny Lau]

@Aaron Liu so is this a better algorithm?

1. elaborate Polynomial.X : Polynomial Nat to an expression tgt (outside the Delab)
2. check if e matches against tgt
3. if yes, return t
4. if no, use the default delab

[Aaron Liu]

why are you running elab in the delab

[Kenny Lau]

no, step 1 is done outside

[Aaron Liu]

is that even possible

[Kenny Lau]

it is not possible

[Aaron Liu]

Kenny Lau said:

no, step 1 is done outside

This sounds doable but there may be are edge cases

[Kenny Lau]

i guess Semiring R might be an issue?

[Kenny Lau]

what's the edge case you're thinking about

[Aaron Liu]

if you declare a polyvars for a free variable

[Aaron Liu]

will the fvarid be preserved

[Aaron Liu]

what if you abstract over it

[Kenny Lau]

i can make that match against $R

[Kenny Lau]

step 1 is making a pattern

[Aaron Liu]

what if there's another instance

[Thomas Murrills]

Is there a reason not to guide delaboration just by matching on the Expr contents directly?

[Aaron Liu]

Thomas Murrills said:

Is there a reason not to guide delaboration just by matching on the Expr contents directly?

how do you check you have the correct ring

[Kenny Lau]

Thomas Murrills said:

Is there a reason not to guide delaboration just by matching on the Expr contents directly?

because the whole point of this is operating on the level of syntax, one benefit of which is that we don't ever have to worry about synthesising the Semiring instances

[Aaron Liu]

Kenny Lau said:

Thomas Murrills said:

Is there a reason not to guide delaboration just by matching on the Expr contents directly?

because the whole point of this is operating on the level of syntax, one benefit of which is that we don't ever have to worry about synthesising the Semiring instances

now I'm confused

[Kenny Lau]

up until this point i have never had to touch Expr

[Aaron Liu]

you don't need to synthesize any instances during delab or unexpand

[Kenny Lau]

what's your algorithm?

[Aaron Liu]

too many edge cases I don't know what to do with

[Aaron Liu]

I guess they're not really edge cases

[Kenny Lau]

Thomas Murrills said:

Is there a reason not to guide delaboration just by matching on the Expr contents directly?

is this the same algorithm as the one here? #mathlib4 > Notation for polynomial variables @ 💬

[Aaron Liu]

they're just cases

[Aaron Liu]

too many things where I don't know what's the desired outcome

[Kenny Lau]

Aaron Liu said:

what if there's another instance

$R is only used in its own delab

[Aaron Liu]

I guess once I'm back at a keyboard I show you and you decide what wants to happen does that sound good

[Kenny Lau]

sure

[Thomas Murrills]

Kenny Lau said:

Thomas Murrills said:

Is there a reason not to guide delaboration just by matching on the Expr contents directly?

is this the same algorithm as the one here? #mathlib4 > Notation for polynomial variables @ 💬

I think so, as long as you’re getting the ingredients in step 1 from $poly/the arguments to the outer command. Why do you say it’s not possible?

[Kenny Lau]

@Thomas Murrills it's only possible outside the Delab, because termElab happens in the TermElabM monad which cannot be lifted to DelabM

[Kenny Lau]

@Thomas Murrills would you like to try writing the code if i give you the specification?

[Aaron Liu]

I could write the code if given a specification that covers every possible case but

[Aaron Liu]

every possible case is really strong

[Thomas Murrills]

Kenny Lau said:

Thomas Murrills it's only possible outside the Delab, because termElab happens in the TermElabM monad which cannot be lifted to DelabM

Right, I meant your proposal to elaborate it outside. Which probably still gets you into a tricky place if you want to do it in an on-the-fly manner by adding a new declaration for the delaborator (you might have to e.g. quote the resulting expr into the body of a new declaration), without something like an environment extension to look up information in…

[Kenny Lau]

well we can start small, we don't need to do every case first

[Kenny Lau]

yes, but that approach is working well for the unexpander in the other cases

[Thomas Murrills]

Kenny Lau said:

Thomas Murrills would you like to try writing the code if i give you the specification?

I would but I’m likely unavailable for at least two days :grinning_face_with_smiling_eyes:However, it’s probably worth writing down a spec anyway, as it will function as/be fairly close to the documentation that will go with this.

[Kenny Lau]

import Mathlib.Init
import Qq

axiom Real : Type
@[class] axiom Semiring : Type → Type

axiom Polynomial (R : Type) [Semiring R] : Type
axiom Polynomial.C {R : Type} [Semiring R] : R → Polynomial R
axiom Polynomial.X {R : Type} [Semiring R] : Polynomial R

axiom MvPolynomial (σ R : Type) [Semiring R] : Type
axiom MvPolynomial.C {σ R : Type} [Semiring R] : R → MvPolynomial σ R
axiom MvPolynomial.X {σ R : Type} [Semiring R] (i : σ) : MvPolynomial σ R

@[instance] axiom Nat.semiring : Semiring Nat
@[instance] axiom Real.semiring : Semiring Real
@[instance] axiom Polynomial.semiring (R : Type) [Semiring R] : Semiring (Polynomial R)
@[instance] axiom MvPolynomial.semiring (σ R : Type) [Semiring R] : Semiring (MvPolynomial σ R)

open Lean PrettyPrinter.Delaborator Elab Term Qq

syntax poly_var := "a" <|> "b" <|> "c"
syntax poly_var : term

@[app_delab Polynomial.C] def polyDelab1 : Delab := do
  -- insert code here
  failure

@[app_delab Polynomial.X] def polyDelab2 : Delab := do
  -- insert code here
  failure

#check (Polynomial.C (MvPolynomial.X 0) : Polynomial (MvPolynomial (Fin 2) Nat)) -- a
#check (Polynomial.C (MvPolynomial.X 1) : Polynomial (MvPolynomial (Fin 2) Nat)) -- b
#check (Polynomial.X : Polynomial (MvPolynomial (Fin 2) Nat)) -- c
#check (Polynomial.X : Polynomial (MvPolynomial (Fin 2) Real)) -- Polynomial.X

[Kenny Lau]

this is the spec

[Kenny Lau]

@Thomas Murrills since you can't write code, do you see an algorithm for this?

[Aaron Liu]

your spec is weird

[Aaron Liu]

you want the exact same term to delaborate two different ways

[Kenny Lau]

oops sorry fixed that

[Thomas Murrills]

The real spec is actually way more general than this, right? As in, you want a way to modify elaboration/delaboration according to a local command, right? (I think that affects how this should be approached)

[Kenny Lau]

yes

[Kenny Lau]

I mean the problem in its essence is:

1. Given newStx : Term
2. Given targetStx : Term, targetType : Term
3. Make sure that newStx elaborates to targetStx : targetType
4. Make sure that targetStx : targetType delaborates back to newStx

[Kenny Lau]

3 can be done entirely on the level of syntax, but 4 requires knowing the type, which is not an available information on the syntax level

[Kenny Lau]

because like just the syntax 1 can have type Nat, Int, Rat, and Real

[Kenny Lau]

current attempt:

@[app_delab Polynomial.X] def polyDelab2 : Delab := do
  let e ← getExpr
  let ⟨1, ~q(Polynomial (MvPolynomial (Fin 2) Nat)), ~q(Polynomial.X)⟩ ← inferTypeQ e | failure
  `(c)

[Kenny Lau]

uh... I might have created a monster

import Mathlib.Init
import Qq

axiom Real : Type
@[class] axiom Semiring : Type → Type

axiom Polynomial (R : Type) [Semiring R] : Type
axiom Polynomial.C {R : Type} [Semiring R] : R → Polynomial R
axiom Polynomial.X {R : Type} [Semiring R] : Polynomial R

axiom MvPolynomial (σ R : Type) [Semiring R] : Type
axiom MvPolynomial.C {σ R : Type} [Semiring R] : R → MvPolynomial σ R
axiom MvPolynomial.X {σ R : Type} [Semiring R] (i : σ) : MvPolynomial σ R

@[instance] axiom Nat.semiring : Semiring Nat
@[instance] axiom Real.semiring : Semiring Real
@[instance] axiom Polynomial.semiring (R : Type) [Semiring R] : Semiring (Polynomial R)
@[instance] axiom MvPolynomial.semiring (σ R : Type) [Semiring R] : Semiring (MvPolynomial σ R)

open Lean PrettyPrinter.Delaborator Elab Term Qq SubExpr

syntax poly_var := "a" <|> "b" <|> "c"
syntax poly_var : term
syntax ident "[" poly_var "]" : term

@[app_delab Polynomial.C] def polyDelab1 : Delab := do
  -- insert code here
  failure

elab "#declare " polyX:ident : command => do
  let termS ← `(Polynomial.X)
  let typeS ← `(Polynomial (MvPolynomial (Fin 2) Nat))
  Command.elabCommand <| ← `(command|
  @[app_delab $polyX] def polyDelab2 : Delab := do
    let e ← getExpr
    let (typeE, _) ← TermElabM.run <| elabTerm (← `($typeS)) none
    let (termE, _) ← TermElabM.run <| elabTermEnsuringType (← `($termS)) typeE
    if ← Meta.isDefEq termE e then `(c) else failure)

-- #check (Polynomial.C (MvPolynomial.X 0) : Polynomial (MvPolynomial (Fin 2) Nat)) -- a
-- #check (Polynomial.C (MvPolynomial.X 1) : Polynomial (MvPolynomial (Fin 2) Nat)) -- b

#declare Polynomial.X

#check (Polynomial.X : Polynomial (MvPolynomial (Fin 2) Nat)) -- c
#check (Polynomial.X : Polynomial (MvPolynomial (Fin 2) Real)) -- Polynomial.X

[Kenny Lau]

@Aaron Liu what's your expert opinion on this code?

[Aaron Liu]

it won't work for if you declare where the ring is a variable

[Aaron Liu]

it at least be unlikely to work

[Kenny Lau]

actually it does work, change the Nat in my code to _ and both give c

[Aaron Liu]

did you use a variable

[Kenny Lau]

also the two TermElabM.run lines can be combined into one:

    let (termE, _) ← TermElabM.run <| elabTerm (← `(($termS : $typeS))) none

[Kenny Lau]

oh, right lemme test that

[Kenny Lau]

ok it doesn't work :smile:

[Kenny Lau]

do you see how to make it work?

[Aaron Liu]

depends on what you want to do in the edge cases

[Kenny Lau]

well my spec is now:

variable (R S : Type) [Semiring R] [Semiring S]
#declare R Polynomial.X
#check (Polynomial.X : Polynomial (MvPolynomial (Fin 2) R)) -- c
#check (Polynomial.X : Polynomial (MvPolynomial (Fin 2) S)) -- Polynomial.X
#check (Polynomial.X : Polynomial (MvPolynomial (Fin 2) Nat)) -- Polynomial.X
#check (Polynomial.X : Polynomial (MvPolynomial (Fin 2) Real)) -- Polynomial.X

[Kenny Lau]

the problematic part of the code is TermElabM.run right

[Kenny Lau]

which monad has access to the variables?

[Kenny Lau]

i know TermElabM does, so the question now is whether MetaM does

[Aaron Liu]

it's in the termelabm read-only state I think

[Kenny Lau]

so there's no way for DelabM to get it then basically?

[Aaron Liu]

who knows it might technically be possible

[Kenny Lau]

well but CommandElabM can get it

[Kenny Lau]

import Lean

open Lean Elab Command Meta

variable {α : Type u} {f : α → α}
variable (n : Nat)

#eval
  runTermElabM fun xs => do
    for x in xs do
      IO.println s!"{← ppExpr x} : {← ppExpr (← inferType x)}"
/-
α : Type u
f : α → α
n : Nat
-/

(not my code)

[Kenny Lau]

the problem is that i've found no other function that can deal with xs : List Expr and do anything meaningful with them

[Aaron Liu]

Kenny Lau said:

the problem is that i've found no other function that can deal with xs : List Expr and do anything meaningful with them

huh what do you mean by that

[Kenny Lau]

xs : List Expr is storing all the variables but i couldn't find any function that takes in List Expr and Syntax and return... i guess TermElabM Expr

[Kenny Lau]

like the elabTerm function is indeed Syntax -> TermElabM Expr but it doesn't take in an additional List Expr right

[Aaron Liu]

@loogle Lean.Elab.TermElabM, List

[loogle]

:exclamation: unknown identifier 'Lean.Elab.TermElabM'
Did you mean "Lean.Elab.TermElabM", List?

[Aaron Liu]

the downside to these namespaces

[Aaron Liu]

is actually Lean.Elab.Term.TermElabM

[Aaron Liu]

well you can always docs#Lean.Elab.Term.TermElabM.run

[Kenny Lau]

import Lean

open Lean Elab Command Meta

variable {α : Type u} {f : α → α}
variable (n : Nat)

elab "#asdf" t:term : command => runTermElabM fun xs => do
  let e ← Term.elabTerm t none
  logInfo e

#asdf n * n

this works and i have no idea why

[Aaron Liu]

why wouldn't it work

[Aaron Liu]

this makes sense to me

[Kenny Lau]

because it did nothing with the xs

[Aaron Liu]

it's in the state though right

[Kenny Lau]

import Mathlib.Init
import Qq

axiom Real : Type
@[class] axiom Semiring : Type → Type

axiom Polynomial (R : Type) [Semiring R] : Type
axiom Polynomial.C {R : Type} [Semiring R] : R → Polynomial R
axiom Polynomial.X {R : Type} [Semiring R] : Polynomial R

axiom MvPolynomial (σ R : Type) [Semiring R] : Type
axiom MvPolynomial.C {σ R : Type} [Semiring R] : R → MvPolynomial σ R
axiom MvPolynomial.X {σ R : Type} [Semiring R] (i : σ) : MvPolynomial σ R

@[instance] axiom Nat.semiring : Semiring Nat
@[instance] axiom Real.semiring : Semiring Real
@[instance] axiom Polynomial.semiring (R : Type) [Semiring R] : Semiring (Polynomial R)
@[instance] axiom MvPolynomial.semiring (σ R : Type) [Semiring R] : Semiring (MvPolynomial σ R)

open Lean PrettyPrinter.Delaborator Elab Term Qq SubExpr

syntax poly_var := "a" <|> "b" <|> "c"
syntax poly_var : term
syntax ident "[" poly_var "]" : term

def polyDelab37 (termE : Expr) : Delab := do
  if ← Meta.isDefEq termE (← getExpr) then `(c) else failure

elab "#declare " R:ident polyX:ident : command => do
  let termS ← `(Polynomial.X)
  let typeS ← `(Polynomial (MvPolynomial (Fin 2) $R))
  let termE ← Command.runTermElabM fun _ => do
    Term.elabTerm (← `(($termS : $typeS))) none
  let delab := polyDelab37 termE
  _ -- uh...

variable (R S : Type) [Semiring R] [Semiring S]

#declare R Polynomial.X

#check (Polynomial.X : Polynomial (MvPolynomial (Fin 2) R))
#check (Polynomial.X : Polynomial (MvPolynomial (Fin 2) S))
#check (Polynomial.X : Polynomial (MvPolynomial (Fin 2) Nat))
#check (Polynomial.X : Polynomial (MvPolynomial (Fin 2) Real))

[Kenny Lau]

@Aaron Liu I now have a live Delab object called delab but I don't know how to tell pp to use it

[Kenny Lau]

I can't tag it dynamically with @[app_delab $polyX]

[Aaron Liu]

You can run the delab on an expr to get a syntax

[Kenny Lau]

but that doesn't actually tell pp to now use that syntax

[Aaron Liu]

well don't go through expr pp if you want a different delab function

[Kenny Lau]

the point is i need to tag something with @[app_delab] so that it actually triggers when I run the testcases at the bottom

[Aaron Liu]

It's in an environment extension probably

[Aaron Liu]

see if you can hack that

[Aaron Liu]

You can whatsnew in to see what gets added to

[Kenny Lau]

def foo : Lean.PrettyPrinter.Delaborator.Delab :=
failure

-- Lean.declRangeExt extension: 1 new entries

-- Lean.Compiler.LCNF.baseExt extension: 1 new entries

-- Lean.Compiler.LCNF.monoExt extension: 2 new entries

-- Lean.IR.declMapExt extension: 3 new entries

-- Lean.IR.UnreachableBranches.functionSummariesExt extension: 2 new entries

-- Lean.Compiler.LCNF.UnreachableBranches.functionSummariesExt extension: 2 new entries

-- Lean.PrettyPrinter.Delaborator.delabAttribute extension: 1 new entries

[Aaron Liu]

found it

[Aaron Liu]

now we go to docs#Lean.PrettyPrinter.Delaborator.delabAttribute

[Kenny Lau]

i love this hacking

[Jovan Gerbscheid]

I'm not sure if you realize this or not, but the same R declared with variable (R : Type) will have a different FVarId in each declaration. So you can't just elaborate Polynomial.X : Polynomial R one time, and then reuse the resulting Expr. Because the Expr that you want to get is different every time.

[Kenny Lau]

i mean, this is why going into Expr is a bad idea...

[Kenny Lau]

but it doesn't seem like we have any other choice

[Kenny Lau]

so you're saying that this will just not work?

[Aaron Liu]

we could hook the command elaborator

[Aaron Liu]

store the fvarid somewhere and update it each time

[Aaron Liu]

we could index into the context in order

[Aaron Liu]

there are so many ways

[Jovan Gerbscheid]

Another silly idea I have is that you could modify the delaborator to include the type as an extra argument in Polynomial.X. And then once you have the type, use the app unexpander to either

• detect that it should be a variable, and put the variable there
• remove this silly extra argument

[Aaron Liu]

I don't understand

[Aaron Liu]

how does this help us verify the ring

[Jovan Gerbscheid]

I propose to write a stupid delaborator that turns (Polynomial.X : Polynomial (MvPolynomial (Fin 2) R)) into Polynomial.X (MvPolynomial (Fin 2) R).

[Aaron Liu]

makes sense

[Jovan Gerbscheid]

And then we use an app unexpander to either get rid of the extra argument, or make it a variable

[Aaron Liu]

but how do we decide which one to do

[Jovan Gerbscheid]

Well, we now have in principle enough information to decide that. (and we can tweak what information exactly we'd want)

[Kenny Lau]

Jovan Gerbscheid said:

I propose to write a stupid delaborator that turns (Polynomial.X : Polynomial (MvPolynomial (Fin 2) R)) into Polynomial.X (MvPolynomial (Fin 2) R).

I like this idea, but i'm not sure if the other big names would

[Kenny Lau]

surely there's a non hacky way to solve this problem

[Aaron Liu]

I really don't see how doing this helps at all

[Aaron Liu]

we're not really adding anything new

[Aaron Liu]

all of this is possible without the stupid delab

[Kenny Lau]

the algorithm here is that firstly the given expr Polynomial.X : anything will first turn into the stupid syntax Polynomial.X anything, and very importantly now we're in the level of syntax and we have enough information to verify if it's part of the newly declared variables

[Aaron Liu]

How do we verify that?

[Kenny Lau]

and since we're now in syntax, we can then use unexpander instead of delab

[Jovan Gerbscheid]

The crucial problem is that the app unexpander, under normal conditions, can't tell these two appart:

variable (R S : Type) [Semiring R] [Semiring S]

name_poly_vars R[x]
name_poly_vars S[y]

#check x -- Polynomial.X : R[x]
#check y -- Polynomial.X : S[y]

Because it just sees Polynomial.X, instead of also seeing its type.

[Aaron Liu]

so why do we need the unexpander at all

[Aaron Liu]

why not just do everything in delab

[Kenny Lau]

because none of us has figured out a way to do it in delab

[Aaron Liu]

I still don't know how you're verifying the type

[Jovan Gerbscheid]

Well it should work in delab, but there is this annoying infinite loop issue, which can be fixed only in a hacky way

[Aaron Liu]

is it just a syntactic match?

[Jovan Gerbscheid]

Yes, we want to match the syntax

[Aaron Liu]

I hope it's not just a syntactic match

[Jovan Gerbscheid]

But I think there might be a better hack to fix the infinite loop issue than just a Bool. Instead we can use the fact that the delaborator keeps track of a SubExpr.Pos (which is just Nat). So we can store in the options this number, and avoid an infinite loop like that. And we can default to 0, because SubExpr.Pos is never 0. (We could also use an IO.Ref, or an environment extension, but I doubt that makes much of a difference)

[Kenny Lau]

@Kim Morrison would you know of a non-hacky way to do this?

[Kim Morrison]

Sorry, at this point I have no idea what "this" even refers to!

[Kenny Lau]

@Kim Morrison here's a specification:

import Mathlib.Init
import Qq

axiom Polynomial (R : Type) : Type
axiom Polynomial.X {R : Type} : Polynomial R

variable (R S : Type)

open Lean PrettyPrinter.Delaborator Elab Term SubExpr Qq Command

elab "#declare " i:ident polyX:ident : command => do
  elabCommand <| ← `(command|
    @[app_delab $polyX] def polyDelab : Delab := do
      /- insert code here? -/ failure)

#declare R Polynomial.X -- you're gonna need this for hygiene

#check (Polynomial.X : Polynomial R) -- Expected: 1 : Polynomial R
#check (Polynomial.X : Polynomial S) -- Expected: Polynomial.X : Polynomial S

[Kenny Lau]

basically, we're looing for a way to conditionally delaborate/unexpand a term based on user specification

[Kenny Lau]

so in the example above, we want Polynomial.X : Polynomial R to become 1, but Polynomial.X : Polynomial S to be untouched

[Kenny Lau]

I've figured out how to do it if R is a constant like Nat, but i'm stuck when it's a variable

[Kenny Lau]

this might be impossible... lemme try to prove it:

1. We want the delab to be generated once by the command #declare R Polynomial.X
2. A delab is essentially (not really) a function Expr -> DelabM Term
3. But the Expr that corresponds to the variable R is not constant, it changes after every declaration.

[Kenny Lau]

so we might need to use @Jovan Gerbscheid's other idea to actually generate the syntax to tag the type in the Term

[Kenny Lau]

Jovan's proposal is this:
Given Polynomial.X : Polynomial R:

1. delab -> Polynomial.X (Polynomial R)
2. unexpand -> 1

Given Polynomial.X : Polynomial S:

1. delab -> Polynomial.X (Polynomial S)
2. unexpand -> Polynomial.X

[Kenny Lau]

@Kim Morrison what do you think about this?

[Kim Morrison]

Kenny Lau said:

so in the example above, we want Polynomial.X : Polynomial R to become 1, but Polynomial.X : Polynomial S to be untouched

That seems like a very bad thing to want...?

[Kenny Lau]

well I essentially did the forward direction already in the PR

[Kim Morrison]

Which PR?

[Kenny Lau]

I made t expand to Polynomial.X : Polynomial R

[Kenny Lau]

#28349

[Kim Morrison]

I would like to be convinced, via a clear and readable document laying out the behaviour, that this is not going to badly confuse users and introduce significant fragility. I am currently very sceptical.

[Kenny Lau]

this = the PR or the delab?

[Kenny Lau]

honestly i'm happy for the PR to proceed without the delab

[Kenny Lau]

i'm not entirely sure why @Jovan Gerbscheid wants the delab

[Kim Morrison]

The PR.

[Kenny Lau]

@Kim Morrison The PR allows the user to type in a command like name_poly_vars R[a,b][C], and does the following:

1. register a, b, and C as declared variables, which are stored in the poly_var syntax category. Essentially:

local syntax "a" : poly_var
local syntax "b" : poly_var
local syntax "C" : poly_var

2. compute the term that these variables are supposed to expand to, which are:

local macro_rules
| `(a) => `(Polynomial.C (MvPolynomial.X 0))
| `(b) => `(Polynomial.C (MvPolynomial.X 1))
| `(C) => `(Polynomial.X)

3. Additionally, the same thing is done for the type itself:

local macro_rules
| `(R[a,b][C]) => `(Polynomial (MvPolynomial (Fin 2) R))

4. More specifications: the ring specified R can be a section variable or a term like Fin 37 or a combination of both like Fin n.
5. And if instead a hole _ is specified, then we process all of the above cases.

As preamble, to make the above work, we have the following syntax declarations:

declare_syntax_cat : poly_var
syntax poly_var : term
syntax (ident <|> "(" term ")") atomic("[" poly_var,+ "]")+ : term

And as a final remark we allow for other functors other than Polynomial or MvPolyonomial, which would require other types of brackets, but that part is not user-facing, so pretend that the above code also works with other types of brackets.

[Kenny Lau]

in summary, this PR did what mathematicians wanted to do for a long time: to refer to a complicated polynomial-esque ring like Polynomial (MvPolynomial (Fin 2) R) by R[a,b][c]

[Kenny Lau]

@Jovan Gerbscheid

import Mathlib.Init
import Qq

axiom Polynomial (R : Type) : Type
axiom Polynomial.X {R : Type} : Polynomial R

open Lean PrettyPrinter Delaborator Elab Term SubExpr Qq Command

elab "#declare " i:ident poly:ident polyX:ident : command => do
  elabCommand <| ← `(command|
    @[app_delab $polyX] def polyXDelab : Delab := do
      let e ← getExpr
      let eT ← Meta.inferType e
      let (``$polyX, #[_]) := e.getAppFnArgs | failure
      let (``$poly, #[R]) := eT.getAppFnArgs | failure
      let type ← PrettyPrinter.delab R
      if let `($i) := type then `(1) else failure)

variable (R S : Type)

#declare R Polynomial Polynomial.X -- for hygiene

#check (Polynomial.X : Polynomial R) -- 1 : Polynomial R
#check (Polynomial.X : Polynomial S) -- Polynomial.X : Polynomial S

[Kenny Lau]

static qq version:

import Mathlib.Init
import Qq

axiom Polynomial (R : Type) : Type
axiom Polynomial.X {R : Type} : Polynomial R

open Lean PrettyPrinter Delaborator Elab Term SubExpr Qq Command

variable (R S : Type)

@[app_delab Polynomial.X] def polyXDelab : Delab := do
  let ⟨1, ~q(Polynomial $rr), ~q(Polynomial.X)⟩ ← inferTypeQ (← getExpr) | failure
  let type ← PrettyPrinter.delab rr
  if let `(R) := type then `(1) else failure

#check (Polynomial.X : Polynomial R) -- 1 : Polynomial R
#check (Polynomial.X : Polynomial S) -- Polynomial.X : Polynomial S

[Kenny Lau]

I want to make this dynamic but Lean is complaining about $rr (and $$rr doesn't solve it)

[Adam Topaz]

@Kenny Lau @Jovan Gerbscheid I have to admit that I completely lost track of this thread. Why do you need to generate delaborators now?

[Jovan Gerbscheid]

So in my opinion, elaborators are one half of the story and delaborators are the other half. I want to see the thing I write in the infoview.

[Adam Topaz]

That I understand. But generating delaborators as done above seems very hacky.

[Adam Topaz]

E.g. the current name_poly_vars command uses notation3 under the hood, which takes care of delaboration.

[Kenny Lau]

how does notation3 do it?

[Adam Topaz]

you can take a look at the code here: https://github.com/leanprover-community/mathlib4/blob/9fd7af820ab2c2d0ae8164bdd98d6c19b0600afd/Mathlib/Util/Notation3.lean#L520

[Adam Topaz]

It's complex. You probably don't want to reinvent the wheel here.

[Kenny Lau]

yeah that's why i was asking to see if you have already gone through the code and could summarise the main part

[Kenny Lau]

or are you saying my PR should just call notation3?

[Adam Topaz]

Yes, I think so.

[Adam Topaz]

IIUC it attempts to create a Mathlib.Notation3.Matcher, and uses that to build the delaborator. The code starts on line 625 of the linked file.

[Jovan Gerbscheid]

Thanks a lot for suggesting this! I forgot about the fact that notation3 creates such an advanced delaborator on the fly. I can get the following to work:

import Mathlib

variable (R S : Type) [Semiring R] [Semiring S]

local notation3 "t" => (Polynomial.X : Polynomial R)
local notation3 "u" => (Polynomial.X : Polynomial S)
#check t -- t : Polynomial R
#check u -- u : Polynomial S

[Jovan Gerbscheid]

https://github.com/kckennylau/mathlib4/pull/16

[Jovan Gerbscheid]

I ended up not using notation3 directly, but copying a bit of the code, and using its expression matcher.

[Kenny Lau]

@Jovan Gerbscheid wow, very nice! do you understand how it works (and could you explain it to me?)

[Kenny Lau]

(also, merged)

[Jovan Gerbscheid]

Yes, the notation3 command creates a delab on the fly (unlike notation, which creates an app unexpander). When writing down the notation3 command, it elaborates the RHS, to turn it into an expression. Then based on this expression in creates the delaborator. The delaborator decides whether to fire or not based on the shape of the expression. Remember that I earlier said that this was going to be hard?

Jovan Gerbscheid said:

I'm not sure if you realize this or not, but the same R declared with variable (R : Type) will have a different FVarId in each declaration. So you can't just elaborate Polynomial.X : Polynomial R one time, and then reuse the resulting Expr. Because the Expr that you want to get is different every time.

Well, it has some smartness built in to keep track of the FVarIds correctly.

[Kenny Lau]

@Jovan Gerbscheid but how does it know about the type?

[Jovan Gerbscheid]

Because it works at the expression level, if the expression is the correct thing, the type is automatically also the correct thing

[Kenny Lau]

thanks!

[Kenny Lau]

@Jovan Gerbscheid would you like to look at the PR?

[Jovan Gerbscheid]

Yes, I've made another cleanup PR: https://github.com/kckennylau/mathlib4/pull/17

[Jovan Gerbscheid]

I'm not sure if we want to change the name of the command name_poly_vars. I think it acts like a fancy version of the variable command, so I'd think it should be called something along the lines of poly_variable.

[Kenny Lau]

thanks, merged

[Kenny Lau]

I'm fine with poly_variable

[Jovan Gerbscheid]

Here's another slight issue with the notation:

name_poly_vars R[t]
variable (l : List R[t])
#check l[t]

This complains because it parses l[t] using syntax:max polyesque : term, and there's no elaborator for it. So either we need to restrict the syntax sufficiently that there is always a macro_rules for it, or if that doesn't work, we need to implement an elaborator that gives a clearer error message here.

[Jovan Gerbscheid]

If we switch to poly_variable, then how should we call register_poly_vars? Maybe register_poly_notation?

[Kenny Lau]

@Jovan Gerbscheid

import Mathlib.Init

axiom Polynomial : Type → Type

open Lean Elab Term

syntax poly_var := "t"
syntax polyesque := ident noWs atomic("[" poly_var "]")
syntax:max (name := polyesqueFallback) polyesque : term

@[term_elab polyesqueFallback] def polyesqueFallbackMacro : TermElab := fun stx _ ↦ do
  throw <| .error stx m!"{stx} is not a declared polynomial-like notation."

variable (R : Type)
local macro_rules | `(R[t]) => `(Polynomial R)

#check R[t]

variable (l : List R[t])
#check l[t]

[Kenny Lau]

Jovan Gerbscheid said:

If we switch to poly_variable, then how should we call register_poly_vars? Maybe register_poly_notation?

sure

[Jovan Gerbscheid]

Yes, that works. You can just use throwError (which doesn't need a m!) (naming-wise I would rather call the syntax itself polyesque_term, and polyesqueFallbackMacro isn't actually a macro).

Can you also add a test for this?

[Jovan Gerbscheid]

I'd also be in favour of scoping the polyesque_term and syntax poly_var : term into some namespace, and then poly_variable can open scoped that namespace. This is just to avoid that the parser does extra unnecessary work when not working with polynomials.

[Kenny Lau]

Jovan Gerbscheid said:

and then poly_variable can open scoped that namespace

earlier I rejected the idea, but with this new observation now I think it's a good idea!

[Kenny Lau]

@Jovan Gerbscheid I have made all the changes you requested:

1. renamed the two commands to poly_variable and register_poly_notation.
2. added the fallback elaborator (and a test for it).
3. added "a lot more detail" to the docstring of poly_variable.
4. scoped the two syntax : terms.
5. moved the file out of the Ring/ folder into Mathlib/Tactic/PolyVariable.lean.
6. fixed the algebraic geometry docstrings.

[Jovan Gerbscheid]

(I think there was an accidental addition that causes CI to complain)

[Kenny Lau]

@Jovan Gerbscheid you mean, for everyone?

[Jovan Gerbscheid]

No, I meant in your PR

[Jovan Gerbscheid]

in Mathlib.lean

[Kenny Lau]

oh...

[Kenny Lau]

remind me to not use mk_all, it ignores the gitignore stuff

[Kenny Lau]

fixed

[Damiano Testa]

It should ignore the gitignore stuff, if you use lake exe mk_all --git.

[Kenny Lau]

https://github.com/leanprover-community/mathlib4/pull/28349#discussion_r2373145955
@Sébastien Gouëzel Should we discuss it here?

[Sébastien Gouëzel]

Yes, let's discuss it here. With the current implementation, when writing R[X][Y], then X is not the generator of R[X], but its image in R[X][Y]. Formally, X is Polynomial.C (Polynomial.X (R := R)). Setting aside all questions about the implementation, or whether we should avoid new notations with brackets, I am a little bit surprised by this design choice. What is the rationale behind this?

[Kenny Lau]

Well my rationale was that our interest is the big ring R[X][Y] (which is isomorphic to R[X,Y]) so X and Y should both be referring to elements of the big ring.

[Kenny Lau]

I don't actually know why R[X][Y] was developed in that Bivariate file rather than R[X,Y] (and then subsequently in the elliptic curve files).

[Kenny Lau]

I did not write the bivariate and elliptic curve files.

[Kenny Lau]

another example: #29497 talks about the ring A = {f ∈ k(t)⟦Y⟧ | f(0) ∈ k}, and then A[X]. there are two instances of PowerSeries.C RatFunc.X in that file and no mention of just RatFunc.X alone. But then it gets more complicated with A[X]. I think in the new scheme it would be:

poly_variable k(t)⟦Y⟧
def A : Subring k(t)⟦Y⟧ := sorry
poly_variable A[X]

[Sébastien Gouëzel]

I don't understand your last example. You mention A[X], so X would be something like a polynomial variable, but then you talk about RatFunc.X(so A(X), rather?) and then PowerSeries.C RatFunc.X(so A(X)[[z]]?)

[Kenny Lau]

sorry, I'm referring to:

t : k(t) := RatFunc.X
t : k(t)⟦Y⟧ := PowerSeries.C RatFunc.X

[Kenny Lau]

I'm pointing out that in the PR they never mentioned the first one (just RatFunc.X), and mentioned the second one twice (PowerSeries.C RatFunc.X)

[Kenny Lau]

A[X] appears as one more layer of complication in the PR, the PR basically talks about both the ring A and then A[X]

[Sébastien Gouëzel]

My point is that, if we talk about R[X][Y], it's precisely because we want to do something in the ring R[X] (and for that we need X in R[X]) and then use its properties to get something in R[X][Y]. Otherwise, we would use R[X, Y].

[Kenny Lau]

my point is that the PR talks about A and A[X], as two rings (so it would make sense to have two poly_variable commands), but Bivariate only talks about one ring R[X][Y] and not the smaller ring R[X] (so it would make sense to just have one poly_variable command).

[Kenny Lau]

feel free to read the bivariate file, I don't think they used the smaller ring R[X].

[Kenny Lau]

well, never is a strong word, they do have some auxiliary lemmas on that (e.g. Polynomial.evalEval_C)

[Kenny Lau]

I think my preferred choice is that if you do want to talk about the smaller ring R[X], then you should do poly_variable twice:

poly_variable R[t]
poly_variable R[x][y]

and yes I think you should have two different names for t and x, because even though mathematically they might be ZFC-equal, in Lean's type theory they are different objects.

[Kenny Lau]

I think whether or not you care about Polynomial.X (R := R) more or Polynomial.C Polynomial.X more, there should still be a way to refer to Polynomial.C Polynomial.X by one letter. (if I understand correctly, your proposal is to instead refer to it as Polynomial.C x.)

[Sébastien Gouëzel]

Well, when we have a ring A, an element a in A and we want to refer to it in A[Y], we use C a. That's the design we have in mathlib. I don't understand why you would want to do it differently when A = R[X] and a = X. The bivariate file is probably a little bit weird in this respect because it's used to craft by hand a two variables polynomial ring (instead of just using R[X, Y] which would probably be a better idea), but mathematically most of the time we use R[X][Y] and not R[X, Y] it's precisely because we don't want the two variables to play the same role.

[Kenny Lau]

Well, I don't know as much mathematics as you do, but I think one of my mental models of R[x1, ..., xn] is just R[x1][x2][x3]...[xn], in fact I'm sure some theorems implicitly use this "definition" (in the land of notation abuse that is widely accepted in maths),

And apart from this example there is also the k(t)⟦Y⟧ above where t and Y have play an equal role. I don't know if there are other examples of these "stacked polynomial-like rings", so more examples are welcome.

In any case your usecase can be done via:

poly_variable R[X]
poly_variable (R[X])[Y]

[Sébastien Gouëzel]

Kenny Lau said:

In any case your usecase can be done via:

poly_variable R[X]
poly_variable (R[X])[Y]

Ah, that's the important information! If the syntax allows both, then it's perfectly fine. This is the kind of thing that should definitely be discussed in the file-level docstring.

[Kenny Lau]

@Kim Morrison I don't think PR is a great place for discussion, can we continue the discussion here?

[Kenny Lau]

For reference, they said that they don't want iterated brackets to be supported.

[Kenny Lau]

is that the secret maintainer stream's opinion or your own opinion? I don't know what the consensus is in the secret maintainers' stream

[Kenny Lau]

@Sébastien Gouëzel well the syntax is very flexible and I feel like the fact that it allows this is a corollary and I can't foresee every possible usecase to be included in the docstring but sure I can include this case.

[Kenny Lau]

I have now added a long explanation in the beginning of the file to explain how the command works.

[Thomas Murrills]

This functionality looks great, and it's wonderful to see all the problems that have been solved here! I would like to give the meta code a thorough review, if it is welcome.

However, my first comment is general: I am concerned about the heavy reliance on syntax throughout. I worry that this makes the notation potentially fragile, and susceptible to behaving in unexpected ways as a result.

For example, I think users would expect identifiers leading the polynomial type to behave like identifiers elsewhere (and it would be nice if they did), but reliance on pure syntax at certain stages breaks things here:

axiom Foo.Bar : Type
@[instance] axiom Foo.Bar.semiring : Semiring Foo.Bar

poly_variable Foo.Bar[x,y,z][C]

namespace Foo

/- Elaborates, but does not delaborate correctly: -/
#check Foo.Bar[x,y,z][C] -- Polynomial (MvPolynomial (Fin 3) Bar) : Type
/- Does not elaborate -/
#check Bar[x,y,z][C] -- Bar[x,y,z][C] is not a declared polynomial-like notation.

My suspicion is that something like this is not an isolated edge case, but an instance of broader fragility arising from working in syntax when the meaning in this specific situation seems to lie naturally at the Expr level.

In contrast, by working with Exprs, we would automatically respect namespacing for idents, allow different syntax to refer to the same base ring, be able to log more descriptive errors, and be able to handle different delaboration results for the same base ring robustly (due to e.g. different prettyprinting options). (We could also open the door to more complex use cases down the line, like ring expressions with holes, which I suspect would be useful, and more general multivariate handling.)

It would also be easier to address the issue raised by @Sébastien Gouëzel, which could be addressed by having x elaborate to an expression of either type R[x] or R[x][y] based on the expected type (using a sensible default if the expected type does not exist or does not match). I also believe the code itself might be simpler and more maintainable (but the jury is really out on this until it's implemented).

You and Jovan have done a lot of work on this already, though, so I realize what it means to suggest changes to the core approach (and am certainly in no position to insist on it)! But if you and/or the maintainers think that this is a reasonable take, I would be happy to either contribute to this PR or answer questions about an Expr-level implementation. (I'd also be happy to outline the algorithm I'm imagining.)

Or, if you disagree, would you mind explaining why syntax is a reasonable choice here and does not introduce fragility? (Indeed, sometimes syntax transformations are appropriate, due to e.g. the ability to exploit cleverness and robustness in the elaboration of the resulting syntax!) I'll also note that I'm interested in the general case, not just this specific issue I found to illustrate the point.

[Kenny Lau]

@Thomas Murrills thanks a lot for your feedback! my rationale of using syntax is that it allows for more flexibility, such as:

1. not having to think about whether Polynomial.C is a function or a ring hom (the .C are actually quite uniform in this regard: they are all ring homs)
2. not having to think about which instances to synthesize, where this time actually the different functors assume different instances: PowerSeries and MvPowerSeries assumes nothing, Polynomial assumes Semiring, MvPolynomial assumes CommSemiring, RatFunc assumes CommRing, and LaurentSeries assumes Zero.

It is unfortunate that this leads to namespace issues as you have discovered, but I don't see how to make the base ring an Expr without having to also build Expr for the whole type... I thought ``Foo.Bar usually solves issues like this.

Do you understand what's happening in the following code?

import Mathlib.Util.Notation3

axiom Foo.Bar : Type

notation3 "%67" => Foo.Bar

#check %67
#check Foo.Bar

namespace Foo

#check %67
#check Foo.Bar
#check Bar

end Foo

I don't think it's a good idea to have x mean different things with different expected types; this would require writing type ascriptions everywhere, and introduces an extra layer of confusion. I don't think one should view R[x] as a subtype of R[x][y] in the context of Lean.

[Thomas Murrills]

Kenny Lau said:

1. not having to think about whether Polynomial.C is a function or a ring hom (the .C are actually quite uniform in this regard: they are all ring homs)

I see; I do indeed consider that a good example of when to use syntax, since we're relying on (d)elaboration complexity in Polynomial.C syntax applications. :) It's possible, though, that we should still elaborate the application at poly_variable, then store and use/match against the resulting Expr instead of hoping that the syntax we choose (d)elaborates everywhere correctly. (Note also that @[app_delab Polynomial.C] has no problem seeing through DFunLike.coe.)

2. not having to think about which instances to synthesize, where this time actually the different functors assume different instances: PowerSeries and MvPowerSeries assumes nothing, Polynomial assumes Semiring, MvPolynomial assumes CommSemiring, RatFunc assumes CommRing, and LaurentSeries assumes Zero.

I'm a little confused by this. I don't believe we'd have to worry about which instances have to be synthesized when working at the Expr level; most of that is taken care of in uniform ways by the relevant parts of the meta API. Where are you worried about having to do this?

[Kenny Lau]

@Thomas Murrills how would you synthesize the Semiring R to make a valid expression that we read as Polynomial R?

[Kenny Lau]

i'm referring to the step where the command is supposed to build the correct Expr that say R[x,y] should expand to

[Thomas Murrills]

You mean during poly_variable, or when elaborating R[x,y] later?

[Kenny Lau]

well I suppose that poly_variable would build the expression once, and later when you type R[x,y] it will just use the same expression that it built... wait this wouldn't work for section variables

[Kenny Lau]

I think the fact that we support section variables is another point for keeping this within syntax

[Thomas Murrills]

Right, you would need to abstract the variables, then fill them back in. But depending on the implementation, the right telescoping function and/or application functions create mvars for the instance arguments (and either synthesize them or let us synthesize them) without needing to go one-by-one.

[Kenny Lau]

do you know which function does that? I might have seen such a function, my metaprogramming knowledge is not very deep

[Kenny Lau]

(I also don't know what's an effective way to look for something like this, I don't think the metaprogramming documentation is very complete)

[Thomas Murrills]

docs#Lean.Meta.mkAppM and docs#Lean.Meta.lambdaMetaTelescope come to mind off the top of my head as relevant here; mkAppM synthesizes instances immediately, but an alternative (standard) strategy is to make sure the metavariables created for the instance-implicit arguments have been added to the list of pending metavariables (in the TermElabM state), and make sure that these get synthesized later in elaboration (see e.g. docs#Lean.Elab.Term.withSynthesize)

[Kenny Lau]

thansk for the pointers!

[Thomas Murrills]

Kenny Lau said:

I think the fact that we support section variables is another point for keeping this within syntax

There's an issue with these that I've written down as one of my review comments, but haven't raised yet to keep focused! Namely:

• In the following:
  variable (R : Type) [Semiring R] poly_variable R[x] example {R : Type} [Semiring R] : R[x] := ...
  I would expect that R[x] would refer to the R that's accessible in the local context at the type, not the variable. But maybe this is a notation3 issue? (Note that delaboration breaks here as well.)

[Kenny Lau]

what does that output?

[Kenny Lau]

Thomas Murrills said:

• I would expect that R[x] would refer to the R that's accessible in the local context at the type, not the variable

I would expect otherwise... syntax already has some good built-in hygiene

[Thomas Murrills]

But normally, the identifier R at that point in the type would refer to the accessible R, not the shadowed R. I don't consider referring to the shadowed R as referring to the "correct" R here (since variables are just there to be automatically-added free variables in each theorem's local context, not the "same" variable for each theorem).

[Kenny Lau]

so, going back to the namespace issue, is that something that can be fixed at the level of syntax? I think right now the namespace issue is a point for Expr, but still Syntax feels better for the stuff with instances

[Kenny Lau]

Thomas Murrills said:

But normally, the identifier R at that point in the type would refer to the accessible R

I feel like you're probably a bit underestimating the power of hygiene, it was in fact a bit tricky for me to deal with as well

[Thomas Murrills]

I think you might be misunderstanding my point; I'm claiming that R should refer to the accessible R, and referring to the inaccessible, shadowed R is not good behavior. :)

[Kenny Lau]

well, I disagree with this point, I think poly_variable should create notations that point to one fixed ring (and a list of fixed elements of that ring) and its meaning shouldn't change depending on context

[Kenny Lau]

actually your usecase is covered by poly_variable _[t] which I forgot to mention in the docstring

[Thomas Murrills]

The command variable (R : Type), though, does not create "one fixed ring". Rather, it allows each theorem to have a free variable R : Type in its local context. So referring to the R introduced by variable does not actually achieve the goal of referring to "one fixed ring".

[Kenny Lau]

hmm....

[Kenny Lau]

maybe we disagree on what variable means :melt:

[Thomas Murrills]

Further, sometimes theorems deliberately shadow variables to change the plicity or argument order (and thus exclude them from the resulting type), which is why this is not just a contrived example. :)

[Kenny Lau]

so, going back to your interpretation, if you choose to interpret variable R as "any arbitrary ring", does poly_variable _[t] cover this usage?

[Thomas Murrills]

No; I believe R should not be "any arbitrary ring", but "any ring in the local context with the name R and correct type"

[Kenny Lau]

well... I understand where you're coming from, sometimes I also have to shadow variables, but I feel like it's actually rather a limitation of Lean that when you shadow variables they kind of still exist in the local context (with a dagger attached), so then I have come to interpret them as actually new variables

[Kenny Lau]

I think I try to avoid shadowing variables as much as possible due to this, so you will see mathlib files structured like:

variable {R : Type*}

section CommSemiring
variable [CommSemiring R]

some lemmas ...

end CommSemiring

section Field
variable [Field R]

some more lemmas ...

end Field

[Thomas Murrills]

Consider the following to see the behavior of variable I'm talking about:

variable (R : Type)
def bar : R := sorry
def bar' : R := sorry
#check bar -- bar (R : Type) : R
#check bar' -- bar' (R : Type) : R
def foo {R : Type} : R := sorry
#check foo -- foo {R : Type} : R
theorem baz {R : Prop} : R := sorry
#check baz -- baz {R : Prop} : R

bar winds up with its own argument R which is unrelated to the R in bar'. Further, when foo changes the plicity or baz changes the type so that the shadowed R no longer appears in the type, it is not present in the type of the resulting declaration (the user expects it to be gone).

[Kenny Lau]

and expanding on my previous point I've come to adopt the practice of using variable {R} or variable {R} in

[Thomas Murrills]

I agree that this is good style when possible, but does not allow fine-tuning of argument order. :)

[Kenny Lau]

I think I would also like to know what other people think about shadowing variables

[Kenny Lau]

Thomas Murrills said:

I agree that this is good style when possible, but does not allow fine-tuning of argument order. :)

again, a limitation of Lean :melt:

[Thomas Murrills]

I also would not want to insist on this style before the notation behaves as the user probably expects.

[Kenny Lau]

well I think me and you are expecting different things

[Thomas Murrills]

Kenny Lau said:

Thomas Murrills said:

I agree that this is good style when possible, but does not allow fine-tuning of argument order. :)

again, a limitation of Lean :melt:

Is it? :grinning_face_with_smiling_eyes: I think being able to just write the type signature as you want it, knowing that variables inaccessible to you are gone, is actually a feature!

[Kenny Lau]

they are gone in the resulting type, but you can still see them inside the declaration

[Kenny Lau]

image.png

[Thomas Murrills]

Sure, but shadowed. No usage of R in syntax will refer to it, which is why the usage of R in polynomial syntax referring to it is, imo, unexpected.

[Kenny Lau]

Indeed, I understand your reasoning, so I understand why you would expect what you expect, but that doesn't change the fact that I interpret things differently, so I expect different things.

[Kenny Lau]

let me give you another example:

axiom Bar : Type

poly_variable Bar[t]

namespace Foo

axiom Bar : Type

#check Bar[t]

end FOo

What would you expect here?

[Thomas Murrills]

Kenny Lau said:

so, going back to the namespace issue, is that something that can be fixed at the level of syntax? I think right now the namespace issue is a point for Expr, but still Syntax feels better for the stuff with instances

My intuition says the elaboration issue can possibly(?) be fixed without too much trouble—the delaboration issue is harder. The real issue to me is that it feels like we're taping leaks shut on a somewhat fragile hull, rather than working at the appropriate level of abstraction. But I agree that syntax manipulations certainly have their place in this PR, given your point about Polynomial.C—my concern is where. :) (Alternatively, there should/could be meta API somewhere that handles DFunLike.coe coercions when applying constants automatically, which would make these sorts of applications straightforward.)

[Kenny Lau]

Thomas Murrills said:

my concern is where

I think as we have discussed above, elaborating the base ring seems to be better in Expr-land, but then calculating the big ring and the terms afterwards seems to be suited in Syntax-land, but then this puts us in an impossible situation...

[Kenny Lau]

Thomas Murrills said:

My intuition says the elaboration issue can possibly(?) be fixed without too much trouble—the delaboration issue is harder.

is the issue that constants and variables are indistinguishable on the level of the syntax? as in, they are both `(term|$i:ident)

[Kenny Lau]

like I agree that if constants vs. variables are indistinguishable in Syntax then they are better suited for Expr

[Thomas Murrills]

Kenny Lau said:

let me give you another example:

axiom Bar : Type

poly_variable Bar[t]

namespace Foo

axiom Bar : Type

#check Bar[t]

end FOo

What would you expect here?

I would expect this to be unrelated to how variable is handled, since resolving a global constant in the current namespace is to me a different process than resolving an identifier in the local context with respect to variable shadowing. :grinning_face_with_smiling_eyes:

But to address this case as well, I would actually want it to resolve the ident as it would when not in the notation, i.e. as Foo.Bar, and then error—the same way Polynomial Bar would error. Having Bar[t] mean a different Bar than the current Bar is, I think, confusing. It might make me think I had declared the notation when I hadn't. (A more helpful approach would be to find all possible resolutions of the constant, then tell me that while Foo.Bar doesn't work, Bar does.)

[Kenny Lau]

Thomas Murrills said:

I would expect this to be unrelated to how variable is handled, since resolving a global constant in the current namespace is to me a different process than resolving an identifier in the local context with respect to variable shadowing.

Indeed, I understand your point, but I think my brain treats them the same

[Kenny Lau]

Thomas Murrills said:

resolve the ident

ok, fair enough, what if it's a term involving an ident?

axiom Wrapper : Type → Type
axiom Bar : Type
axiom Foo.Bar : Type

poly_variable (Wrapper Bar)[t]
namespace Foo
#check (Wrapper Bar)[t]
end Foo

[Thomas Murrills]

Kenny Lau said:

Thomas Murrills said:

my concern is where

I think as we have discussed above, elaborating the base ring seems to be better in Expr-land, but then calculating the big ring and the terms afterwards seems to be suited in Syntax-land, but then this puts us in an impossible situation...

A pattern I might expect here is to do our necessary syntax manipulations first, within a larger TermElabM elaborator. We can possibly have the best of both worlds. :)

[Kenny Lau]

I would also like to have a substitutable syntax but I don't think I have found it

[Kenny Lau]

like ideally I want a syntax i : Term <- `(Polynomial (Polynomial $a)) and then have i.subst (a := <- `(R))

[Kenny Lau]

even if I have that (I used to do that by storing an Array of the functor Terms), I don't think I can apply it to an Expr...

[Thomas Murrills]

Kenny Lau said:

Thomas Murrills said:

My intuition says the elaboration issue can possibly(?) be fixed without too much trouble—the delaboration issue is harder.

is the issue that constants and variables are indistinguishable on the level of the syntax? as in, they are both `(term|$i:ident)

I think the issue is that the idents we get from delaboration are different (since they depend on the namespace we're in) than the ones we are matching against. We could try normalizing both to their global forms first, but I don't think we would have to worry about this if delaborating from Exprs directly.

[Thomas Murrills]

Kenny Lau said:

Thomas Murrills said:

resolve the ident

ok, fair enough, what if it's a term involving an ident?

axiom Wrapper : Type → Type
axiom Bar : Type
axiom Foo.Bar : Type

poly_variable (Wrapper Bar)[t]
namespace Foo
#check (Wrapper Bar)[t]
end Foo

I'd expect idents to resolve to the same thing in all cases, personally! I.e., this should fail for the same reasons I think the prior example should fail—because Bar should now refer to Foo.Bar.

[Kenny Lau]

I feel like you want some sort of syntactic behaviour (by having Bar as an ident rather than the expression .const Bar []), but you also want some sort of expression behaviour; or rather, you want to do some sort of further matching when elaborating a declared notation, rather than just storing one term; this would also put more pressure on the delaborator.

[Thomas Murrills]

Kenny Lau said:

like ideally I want a syntax i : Term <- `(Polynomial (Polynomial $a)) and then have i.subst (a := <- `(R))

This sort of thing is rather straightforward when working with Exprs. :grinning_face_with_smiling_eyes: First we abstract the fvars to get a lambda expression (there is API for this), then later we form expression applications with the thing we want to substitute in and beta-reduce. (Or, we form a lambda telescope, then assign the mvars.) (There is API for all of this as well.)

[Kenny Lau]

I take it that you're not in the qq camp?

[Thomas Murrills]

Kenny Lau said:

I feel like you want some sort of syntactic behaviour (by having Bar as an ident rather than the expression .const Bar []), but you also want some sort of expression behaviour; or rather, you want to do some sort of further matching when elaborating a declared notation, rather than just storing one term; this would also put more pressure on the delaborator.

I think your intuition is probably good here, and I do think that this is one of the junctures at which Syntax can be helpful; it really depends on the stage of elaboration we're at, and what we're elaborating, imo. Without talking more about which part of the situation we're addressing here exactly, it's hard for me to say if I agree or disagree, though. :grinning_face_with_smiling_eyes:

[Kenny Lau]

so, basically, after poly_variable ($term)[t], you want ($term)[t] to elaborate to the following:

1. elaborate ($term) here (instead of at the point of the poly_variable command) to an expression termE : Expr
2. then do some expression-level transformation (using some of the magic functions above) to form what amounts to q(Polynomial $termE) but not really (or maybe really)

[Kenny Lau]

the problem seems to be that for 1, the string you see is not the full syntax; so the code R actually becomes two different syntaxes in two different contexts, so the pseudocode above won't even trigger

[Kenny Lau]

so now it's not an issue of syntax or expr, you're asking for something impossible here

[Thomas Murrills]

Kenny Lau said:

I take it that you're not in the qq camp?

I am actually sQquarely in the Qq camp! :grinning_face_with_smiling_eyes: It might certainly help out in this sort of situation in general. But it does help the most when you want to construct specific expressions (possibly with nonspecific antiquotations, of course) at elaboration time of your meta code.

At the level of generality we're working at here, with very general expressions at just about every stage, I think Qq might be of limited utility, though. (I could be wrong here though, and would be happy to be.) (If we were constructing these notations by hand on a per-instance basis, I'd think differently.)

[Kenny Lau]

for 1 you're instead asking for the level of the code (code -> syntax -> expr -> virtual machine), where the bytes of the source code literally matches the string Wrapper Bar

[Thomas Murrills]

for 1, the string you see is not the full syntax; so the code R actually becomes two different syntaxes in two different contexts, so the pseudocode above won't even trigger

I'm a bit lost here. Are you talking about specifically for expressions which involve section variables?

[Kenny Lau]

whichever case, section variables or namespace constants

[Thomas Murrills]

Ah, I just caught

(instead of at the point of the poly_variable command)

No, I would imagine elaborating at the point of the poly_variable command.

[Thomas Murrills]

I can write down a high-level outline for the algorithm I have in mind, which might be the most clear here. :grinning_face_with_smiling_eyes:

[Thomas Murrills]

However, my high-level outline was formed before you brought up the usefulness of syntax in forming these applications re: ring homs and the like. Let me break to eat, think it over so that I don't waste your time suggesting something incomplete, and get back to you with something more concrete. :)

[Kenny Lau]

import Mathlib.Util.Notation3
import Qq

axiom Polynomial : Type → Type

open Qq Lean Elab Command

elab "#declare " poly:term : command => do
  elabCommand <| ← `(elab "%67" : term => do
    return q($poly Int))

#declare Polynomial
#check %67

[Kenny Lau]

@Thomas Murrills what do you think about this?

[Thomas Murrills]

(I'd also still like to bring up some review comments, but will hold off on those until we finish this dicussion! :) )

[Thomas Murrills]

Kenny Lau said:

import Mathlib.Util.Notation3
import Qq

axiom Polynomial : Type → Type

open Qq Lean Elab Command

elab "#declare " poly:term : command => do
  elabCommand <| ← `(elab "%67" : term => do
    return q($poly Int))

#declare Polynomial
#check %67

(First reaction, the nested Qq within an elab within a quotation within another elab looks rather cursed to me :sweat_smile:)

[Kenny Lau]

I think the point is to show you antiquoting of term in qq

[Kenny Lau]

which seems to be what you want

[Thomas Murrills]

So, I am a little wary of the approach of "construct the syntax of the specific command we would use if we were defining a single notation, then elaborate it" as opposed to "do the thing we want to do directly, in general". I feel that acting directly is a little more maintainable.

I'd like to think a bit more before suggesting anything, since there are a couple of different approaches available. (For example, for elaborating the polynomial ring: when encountering R[x,y,z][w] in poly_variable, one could store the polynomial ring expression in the env extension; then during elaboration, infer the functors from the bracketing, apply them on the syntax level, elaborate, then attempt to match against the stored expr. Or one could attempt to elaborate & store the base ring, match against that when elaborating and then apply the functors on the Expr level, etc.)

[Thomas Murrills]

I'm going to return to this tomorrow (edit: Tuesday is actually when I am first free again!), but I'll also leave tonight with some other review comments/questions. (I'll put each one in a separate message, so they can easily be responded to!) If some internals are going to change, it might not make sense to address them yet, but at least they can be discussed.

[Thomas Murrills]

• poly_variable R[x] should probably check that the required instances are actually available for R, and error if not; instead, the user is only made aware of this later, when attempting to use the notation.

[Thomas Murrills]

• I would expect poly_variable R[x,y][z] to also set up R[x,y]. Is there a reason it doesn't?

[Thomas Murrills]

• I believe the error messages in the following situations could be improved:
  • When re-using a variable name in a poly_variable declaration (e.g. poly_variable R[x] and then poly_variable S[x]). Currently the error is unexpected token 'x'; expected poly_closing. A better error message could be achieved by parsing a poly_var <|> ident, then logging a descriptive error on poly_vars (ideally, telling the user which notation it is registered in).
  • When writing incorrect type notation—e.g. R[x,y][z] when only R[x,y][w] is registered. It would be helpful to tell the user which notations were registered for R/R[x,y].

[Thomas Murrills]

And finally, a softer question:

• Are we sure it ought to be named poly_variable instead of e.g. poly_notation? :eyes: It does name the variables, but it also sets up the syntax for the type. Its functionality is also not very similar to variable, and the "variables" of a polynomial are very different beasts than the free variables of variable. (If we like poly_notation, it might make sense to change register_poly_notation to something like register_poly_brackets.)

[Kenny Lau]

Thomas Murrills said:

• poly_variable R[x] should probably check that the required instances are actually available for R, and error if not; instead, the user is only made aware of this later, when attempting to use the notation.

this would make sense if we are building Expr, but wouldn't make sense if we are building syntax. note that the existing name_poly_vars also doesn't check the comm_semiring instance.

[Kenny Lau]

Thomas Murrills said:

• I would expect poly_variable R[x,y][z] to also set up R[x,y]. Is there a reason it doesn't?

see the whole discussion above with @Sébastien Gouëzel. Some people (including him) hold the opinion that R[x,y][t] means we are talking about two rings, but some people (including me) have the opposite opinion that R[x,y][t] means one big ring. The concrete difference is whether x belongs to a subring R[x,y] or the big ring R[x,y][t].

And I noted that his interpretation can be done by the following:

poly_variable R[x,y]
poly_variable (R[x,y])[t]

To which he said that I should document this, which I did.

But personally I prefer:

poly_variable R[a,b]
poly_variable R[x,y][t]

that is, I would prefer to use a completely different letter to refer to the element of the subring.

[Kenny Lau]

Thomas Murrills said:

• A better error message could be achieved by parsing a poly_var <|> ident

I agree with this.

[Kenny Lau]

Thomas Murrills said:

• When writing incorrect type notation—e.g. R[x,y][z] when only R[x,y][w] is registered. It would be helpful to tell the user which notations were registered for R/R[x,y].

That sounds too advanced. You're basically suggesting autocorrection. VSCode does have autocompletion features (when you hit ctrl+space) and if you have a way to hack into that I'm all for it.

[Kenny Lau]

Thomas Murrills said:

• Are we sure it ought to be named poly_variable

I am not attached to any names.

[Thomas Murrills]

Great, thanks for answering those questions!

I've had a chance to think about this (apologies—busy time for me, which spilled over into this week). I wanted to clear my head on this by outlining what exactly the necessary tasks and obligations are at different stages. I arrived at the following:

• when elaborating syntax for a type, we have enough information, in principle (given the positions of the brackets and number of variables they contain, and relying only on the global state created by register_poly_notation), to determine the big ring. Our task, after inferring the expression, is to validate that the bracket sequence is locally registered for the given base ring, and validate that the provided variable names appear as they do in the locally registered syntax.
• when elaborating syntax for a variable, we need to recall the ring it is a generator of, and construct that generator.
• when delaborating an expression, we have to identify the expression as representing a locally registered polynomial ring or variable, and recall the variable names, then construct all the appropriate syntax.

I'm hoping that breaking it down this way lets us more easily consider when using an Expr approach might be more or less fragile than a Syntax approach.

(Note also that the first bullet shows why it is not too advanced in principle to

tell the user which notations were registered for R/R[x,y]

depending on how we set things up. If we can look up the bracket sequences and variable names registered by matching against the base ring, we can match as much as we can, and report what would be valid on the mismatch. I am specifically talking about error messages here, by the way, not autocomplete!)

[Thomas Murrills]

If we did want to take an Expr-based approach here, here's an outline describing what that could look like.

Expr-based outline

• at parsing:
  • (no change required) parse everything that looks like some kind of registered notation (when notation is active).
• at poly_variable:
  • elaborate base ring term
    • if fvars present, abstract to lambda as appropriate, and remember them (with care)
    • store (resulting, abstracted) base ring expr in an env extension (to be matched on at reducible defeq)
    • associate it (in said extension) with:
      • a sequence of something like: Functor × PolyVarSeq, where
        • Functor tells us the Name of the functor corresponding to the bracket pair, as well as the .X constant and the .C constant
        • PolyVarSeq holds the (sequence of) variable name(s)/syntax(es) in whatever form is appropriate
    • elaborate result to check that instances get synthesized/notation works (and add hover info)
    • note: could also allow mvars in the base ring, and abstract/track those too, like fvars; if so, do not insist that instances are synthesized
  • (probably no change required) add local syntax for polynomial variable names
• at elaboration
  • of types:
    • Elaborate base ring term; check base rings in env extension for a match (handling variables as well)
    • deduce functors (using global state set up by register_poly_notation) bracket pair by bracket pair, and match to the functor sequence stored for the base ring; validate that written variable names match registered variable names. Report any mismatches along with available "correct" syntax for the base ring.
  • of variable names:
    • have a single, global, scoped elaborator for poly_vars which looks up the syntax in the env extension (the state will probably be very small, so a linear scan is probably fine)
    • if allowing multiple types: and constructs the appropriate application. (Note: it is not too hard to coerce a ring hom to a function on the Expr level.)
      • match expected type to possible recorded types. if no match, use a chosen default.
• at register_poly_notation
  • associate the bracket pair with the functor, .X, and .C constant names
  • set up fixed delaborators for the functor, .X, and .C notation (note: app delaborators can see through DFunLike.coe) which will inspect the state set up by poly_variable and match against the extracted base ring

I realize this is basically a rewrite, though. (I'd be happy to contribute, but would not want to step on any toes!) While I do think an Expr-based approach would make the notation more robust, predictable, and featureful (e.g. better error messages), I am ultimately not in a position to make the call on whether this PR as-is should or should not make it into Mathlib. An Expr-based approach is just my personal recommendation after considering the PR, but I'll defer to maintainers—and to whether you agree with this approach or not. :)