notation over field

Stream: lean4

[Tomas Skrivan]

In calculus and linear algebra you have to specify the field over which you are working over and over. I find this annoying. Especially when doing physics we almost exclusively work over real numbers. Specifying it everywhere just adds noise and is tedious. Here is my solution to that:

Init file

initialize currentFieldName : IO.Ref Name ← IO.mkRef default

elab "open_notation_over_field" K:ident : command => do
  currentFieldName.set K.getId
  Lean.Elab.Command.elabCommand <| ←
   `(open NotationOverField)

Example use on continuous linear map

namespace NotationOverField
open Lean Elab Term
scoped elab X:term " →L " Y:term : term => do
  let K ← NotationOverField.currentFieldName.get
  let K := mkIdent K
  elabTerm (← `(term| $X →L[$K] $Y)) none
end NotationOverField

open_notation_over_field Real

#check ℝ →L ℝ

There are two downsides

1. then notation ℝ →L ℝ is not a macro anymore
2. the global reference currentFieldName can have a some random value from imported files which might work or not

Is there a way to set the value of currentFieldName just for the current file? Reset it once you are done elaborating the file where you call open_notation_over_field K.

Maybe using IO.Ref is a bad approach, can this be done in a different way?

[Kyle Miller]

How about this?

import Mathlib

syntax "currentBaseRing%" : term

macro_rules | `(currentBaseRing%) => Lean.Macro.throwError "\
  There is no current base ring for this notation. \
  To set one, add the following local macro rules \
  and adjust '𝕜' to be your desired base ring.\
  \n\n  local macro_rules | `(currentBaseRing%) => `(𝕜)"

notation:25 M " →L " M₂ => ContinuousLinearMap (RingHom.id currentBaseRing%) M M₂

#check ℝ →L ℝ
/-
There is no current base ring for this notation. To set one, add the following local macro rules
and adjust '𝕜' to be your desired base ring.

  local macro_rules | `(currentBaseRing%) => `(𝕜)
-/

local macro_rules | `(currentBaseRing%) => `(ℝ)

#check ℝ →L ℝ
-- ℝ →L[ℝ] ℝ : Type

[Kyle Miller]

Since it's a local macro rule, it's also scoped to the current section/namespace.

[Tomas Skrivan]

Ahh this is a much neater solution! And gives a nice error.

[Adam Topaz]

What about this:

import Mathlib

syntax "currentBaseRing%" : term

macro_rules | `(currentBaseRing%) => Lean.Macro.throwError "
  There is no current base ring for this notation.
  To set one, add the following local macro rules
  and adjust '𝕜' to be your desired base ring.
  \n\n  local macro_rules | `(currentBaseRing%) => `(𝕜)"

notation:25 M " →L " M₂ => ContinuousLinearMap (RingHom.id currentBaseRing%) M M₂

#check ℝ →L ℝ
/-
There is no current base ring for this notation. To set one, add the following local macro rules
and adjust '𝕜' to be your desired base ring.

  local macro_rules | `(currentBaseRing%) => `(𝕜)
-/

macro "set_base_ring" r:term : command =>
  `(local macro_rules | `(currentBaseRing%) => `($r))

set_base_ring ℝ

#check ℝ →L ℝ

[Adam Topaz]

modulo modifying Kyle's error message...

[Kyle Miller]

(Did you remove the trailing \s because you're you using an old Mathlib? Those eliminate the whitespace at the beginning of the following line.)

[Adam Topaz]

Yeah I'm probably using an older mathlib

[Adam Topaz]

it's in some scrap project I have on my machine

[Kyle Miller]

In case you need this on an older Lean, this is what you could write instead of using \:

macro_rules | `(currentBaseRing%) => Lean.Macro.throwError s!"{
  ""}There is no current base ring for this notation. {
  ""}To set one, add the following local macro rules {
  ""}and adjust '𝕜' to your desired base ring.{
  ""}\n\n  local macro_rules | `(currentBaseRing%) => `(𝕜)"

[Kyle Miller]

(I'm glad that's not the style anymore!)

[Kim Morrison]

This is appealing. (Works fine with variables too.)

[Kim Morrison]

I'm a little concerned that adding local macros in the files in this manner does make maintenance harder: you can't move lemmas around as easily.

[Kim Morrison]

(The problem is only as bad as the same problem caused by variable.)

[Adam Topaz]

the behavior seems similar to parameter in lean3

[Tomas Skrivan]

Scott Morrison said:

This is appealing. (Works fine with variables too.)

Yes exactly, the point is that you do

variable (K : Type) [Ring K]
set_base_ring K

And then you forget about it

[Kim Morrison]

We just need autoImplicit for typeclasses, and can just write set_base_ring K! (Mostly joking.)

[Kyle Miller]

Here's a hack, not sure how well it works in practice:

import Mathlib

class CurrentBaseRing (R : outParam <| Type*)

syntax "currentBaseRing%" : term

open Lean Meta in
elab_rules : term | `(currentBaseRing%) => do
  let R ← mkFreshTypeMVar
  let res? ← synthInstance? <| Expr.app (← mkConstWithFreshMVarLevels ``CurrentBaseRing) R
  if res?.isSome then
    return R
  else
    throwError "\
      There is no current base ring for this notation. \
      To set one, add\
      \n\n  variable [CurrentBaseRing 𝕜]\
      \n\nwith an appropriate `𝕜`."

notation:25 M " →L " M₂ => ContinuousLinearMap (RingHom.id currentBaseRing%) M M₂

#check ℝ →L ℝ
/-
There is no current base ring for this notation. To set one, add

  variable [CurrentBaseRing 𝕜]

with an appropriate `𝕜`.
-/

variable [CurrentBaseRing ℝ]
#check ℝ →L ℝ
-- ℝ →L[ℝ] ℝ : Type

[Adam Topaz]

Lean 4 is fun :)

[Adam Topaz]

We can take this further:

import Mathlib

class BaseTopologicalRing (R : outParam <| Type*) extends
  CommRing R, TopologicalSpace R, TopologicalRing R

syntax "currentBaseRing%" : term

open Lean Meta in
elab_rules : term | `(currentBaseRing%) => do
  let R ← mkFreshTypeMVar
  let res? ← synthInstance? <| Expr.app (← mkConstWithFreshMVarLevels ``BaseTopologicalRing) R
  if res?.isSome then
    return R
  else
    throwError "foobar"

notation:25 M " →L " M₂ => ContinuousLinearMap (RingHom.id currentBaseRing%) M M₂

variable [BaseTopologicalRing R]
#check R →L R

[Adam Topaz]

Alternatively we could synthesize the additional required instances in the elaborator instead of the class.

[Eric Wieser]

That looks like a bad idea to me, since the resulting lemmas then actually mention BaseTopologicalRing unlike Kyle's solution where the typeclass is an invisible implementation detail to downstream users

[Adam Topaz]

ok, so let's do it in the elaborator

[Eric Wieser]

I think

class BaseTopologicalRing (R : outParam <| Type*) [CommRing R] [TopologicalSpace R] [TopologicalRing R]

would be fine

[Adam Topaz]

well, what I'm trying to get to work is that writing variable [BaseRing R] would either synthesize a preexisting instance and set the base ring, or if it can't find such an instance, at the variable to the local context.

[Adam Topaz]

I guess what I wrote above would not do that, so it was wrong for various reasons.

[Kyle Miller]

You could use variable? for this:

import Mathlib.Tactic

import Mathlib

class BaseTopologicalRing (R : outParam <| Type*)
  [CommRing R] [TopologicalSpace R] [TopologicalRing R]

syntax "currentBaseRing%" : term

open Lean Meta in
elab_rules : term | `(currentBaseRing%) => do
  let fn ← mkConstWithFreshMVarLevels ``BaseTopologicalRing
  let (args, _, _) ← forallMetaTelescope (← inferType fn)
  let R := args[0]!
  let res? ← synthInstance? <| mkAppN fn args
  if res?.isSome then
    return R
  else
    throwError "\
      There is no current base ring for this notation. \
      To set one, add\
      \n\n  variable [BaseTopologicalRing 𝕜]`\
      \n\nwith an appropriate `𝕜`."

notation:25 M " →L " M₂ => ContinuousLinearMap (RingHom.id currentBaseRing%) M M₂

#check ℝ →L ℝ
/-
There is no current base ring for this notation. To set one, add

  variable [CurrentBaseRing 𝕜]`

with an appropriate `𝕜`.
-/

section
variable [BaseTopologicalRing ℝ]
#check ℝ →L ℝ
-- ℝ →L[ℝ] ℝ : Type
end

section
variable (𝕜 : Type*)
variable? [BaseTopologicalRing 𝕜]
#check 𝕜 →L 𝕜
-- 𝕜 →L[𝕜] 𝕜 : Type u_1
end