Modify declaration in place

Stream: metaprogramming / tactics

[Calle Sönne]

I want to make an attribute that modifies a definition declaration in place (by changing its type to something defeq). What functions would I need to use to do the modification? Should I use addDecl using the same name as the tagged definition to overwrite it?

[Damiano Testa]

I don't think that you can override an existing declaration.

[Calle Sönne]

Is there a way to modify it using modifyEnv?

[Damiano Testa]

I have never tried to do anything of this sort, but I suspect that you should try hard to "catch" the declaration before it is added to the environment, rather than expunging it after the fact.

[Damiano Testa]

Can you say a little more what it is that you are trying to do?

[Damiano Testa]

(Also, note that every "explicit" declaration may add several "behind-the-scenes" declarations to the enviroment, so removing just the one that you see may leave you in a weird state with unwanted stuff still present.)

[Calle Sönne]

Given a class such as e.g.

/-- An open immersion of PresheafedSpaces is an open embedding `f : X ⟶ U ⊆ Y` of the underlying
spaces, such that the sheaf map `Y(V) ⟶ f _* X(V)` is an iso for each `V ⊆ U`.
-/
class PresheafedSpace.IsOpenImmersion {X Y : PresheafedSpace C} (f : X ⟶ Y) : Prop where
  /-- the underlying continuous map of underlying spaces from the source to an open subset of the
    target. -/
  base_open : OpenEmbedding f.base
  /-- the underlying sheaf morphism is an isomorphism on each open subset -/
  c_iso : ∀ U : Opens X, IsIso (f.c.app (op (base_open.isOpenMap.functor.obj U)))

I want to create an attribute @[MorphismProperty] which changes the type of this class to MorphismProperty (PresheafedSpace C). MorphismProperty is defined as:

/-- A `MorphismProperty C` is a class of morphisms between objects in `C`. -/
def MorphismProperty :=
  ∀ ⦃X Y : C⦄ (_ : X ⟶ Y), Prop

So the problem is that I cant immediately define it with type MorphismProperty _ as it is not of type Type.

[Calle Sönne]

There is a naive solution where you define PresheafedSpace.IsOpenImmersionAux as above, then add an abbrev PresheafedSpace.IsOpenImmersion with type MorphismProperty (PresheafedSpace C). But I was hoping for some automation to make this nicer.

[Calle Sönne]

Damiano Testa said:

I have never tried to do anything of this sort, but I suspect that you should try hard to "catch" the declaration before it is added to the environment, rather than expunging it after the fact.

Is this possible to do with attributes?

[Damiano Testa]

Without having thought too much about this, you may be able to write a macro that automatically adds more declarations to the enviroment.

[Andrew Yang]

It would work if we could somehow make

@[MorphismProperty]
class Foo {X Y : Scheme} (f : X ⟶ Y) : Prop where

expand to

class Foo.class {X Y : Scheme} (f : X ⟶ Y) : Prop where

abbrev Foo : MorphismProperty Scheme := Foo.class

But I have no idea if this is possible or not.

[Calle Sönne]

yes that would be great

[Damiano Testa]

That may not be so hard.

[Damiano Testa]

So, you would like to generate an "intermediate" class with .class as tail of its name, but everything else as given in the initial syntax and then the abbreviation?

[Damiano Testa]

Let me see if I can write a prototype for this.

[Calle Sönne]

yeah exactly!

[Calle Sönne]

and I guess at this point it wouldn't even need to be an attribute, but could be a command/macro of some sort

[Damiano Testa]

Can you try this and see if it has a chance of doing something correctly?

open Lean Elab Command in
elab "toMorProp " cmd:command : command => do
  let oldName := (cmd.raw.find? (·.isOfKind ``Parser.Command.declId)).getD default
  let className := mkIdentFrom oldName (oldName[0].getId ++ `class)
  -- replaces the given name with `name.class`
  let withClassName ← cmd.raw.replaceM fun s => if s.isOfKind ``Parser.Command.declId then return some className else return none
  -- elaborates the `.class` syntax
  elabCommand withClassName
  let newAbbrev ← `(command| abbrev $(⟨oldName⟩) : $(mkIdent `MorphismProperty) $(mkIdent `Scheme) := $className)
  elabCommand newAbbrev

toMorProp
class Foo {X Y : Scheme} (f : X ⟶ Y) : Prop where

[Damiano Testa]

(This is very simple-minded, there is quite a bit of space for improvement, but if it works in easy situations, then I can look into making it more robust.)

[Kyle Miller]

Yeah, attributes can't change declarations, but they can add new declarations. @Andrew Yang's can be modified where it reads something like

@[MorphismProperty Foo]
class FooClass {X Y : Scheme} (f : X ⟶ Y) : Prop where

That Foo is optional, but it seems like a nice way to say what name you want for the abbrev.

[Kyle Miller]

@Damiano Testa Your elab can be a macro:

open Lean in
macro "toMorProp " cmd:command : command => do
  let oldName := (cmd.raw.find? (·.isOfKind ``Parser.Command.declId)).getD default
  let className := mkIdentFrom oldName (oldName[0].getId ++ `class)
  -- replaces the given name with `name.class`
  let withClassName ← cmd.raw.replaceM fun s => if s.isOfKind ``Parser.Command.declId then return some className else return none
  let newAbbrev ← `(command| abbrev $(⟨oldName⟩) : $(mkIdent `MorphismProperty) $(mkIdent `Scheme) := $className)
  return ⟨mkNullNode #[withClassName, newAbbrev]⟩

[Kyle Miller]

(That's completely untested!)

[Damiano Testa]

Oh, with macro the elabCommands are automatic for the resulting syntax?

[Kyle Miller]

Yeah, and in particular elabCommand is what is responsible for expanding command macros.

[Kyle Miller]

It also has special support for macros that expand a command into multiple commands, via mkNullNode.

[Damiano Testa]

Ok, I did not know whether that mkNullNode was a "common" way of merging two commands into one -- thanks!

[Kyle Miller]

There's also special support for `(...) syntax where if it fails to parse as a term quotation, it parses as a command quotation, and it also supports multiple commands, like in `($(⟨withClassName⟩):command $newAbbrev). This uses a null node too.

[Damiano Testa]

I knew about term falling back to command, but I did not know about commandSeq!

[Kyle Miller]

This explains why you can write `(def a := 1 def b := 2) but not `(command| def a := 1 def b := 2)

[Damiano Testa]

Is there a performance cost to taking advantage of these special cases, or is this the idiomatic way of proceeding?

[Kyle Miller]

If there is, it's likely negligible

[Calle Sönne]

Thanks a lot! Will play around with this for a bit

[Calle Sönne]

Damiano Testa said:

Can you try this and see if it has a chance of doing something correctly?

open Lean Elab Command in
elab "toMorProp " cmd:command : command => do
  let oldName := (cmd.raw.find? (·.isOfKind ``Parser.Command.declId)).getD default
  let className := mkIdentFrom oldName (oldName[0].getId ++ `class)
  -- replaces the given name with `name.class`
  let withClassName ← cmd.raw.replaceM fun s => if s.isOfKind ``Parser.Command.declId then return some className else return none
  -- elaborates the `.class` syntax
  elabCommand withClassName
  let newAbbrev ← `(command| abbrev $(⟨oldName⟩) : $(mkIdent `MorphismProperty) $(mkIdent `Scheme) := $className)
  elabCommand newAbbrev

toMorProp
class Foo {X Y : Scheme} (f : X ⟶ Y) : Prop where

This almost works, one needs to use strict-implicit (or explicit) binders for {X Y : Scheme}, otherwise it doesn't work

[Linyu Yang]

Thank you all so much! @Calle Sönne @Damiano Testa @Kyle Miller

I was also wondering whether there was a method to run some command macro last night, and today I find your suggestions. Here is what I wanted to do last night (add a Haskell-style definition syntax to Lean4) and I succeeded this morning:

open Lean Elab Command in
elab "[hs| " name:ident " :: " type:term " ; "
  name1:ident " := " value:term " ]" : command
  => do
  logInfo "definition with haskell syntax!"
  if name == name1
  then
    let cmd ← `(command| def $name : $type := $value)
    elabCommand cmd
  else logInfo "are you talking about the same term?"

[hs|
x :: Nat ;
x := 3
]

#check x   -- x : Nat

[Damiano Testa]

Calle Sönne said:

Damiano Testa said:

This almost works, one needs to use strict-implicit (or explicit) binders for {X Y : Scheme}, otherwise it doesn't work

Do you have a #mwe showing where this fails?

[Calle Sönne]

import Mathlib.CategoryTheory.MorphismProperty.Basic
import Mathlib.AlgebraicGeometry.Scheme
import Lean

open CategoryTheory AlgebraicGeometry

open Lean Elab Command in
elab "mkMorphismProperty " cmd:command : command => do
  let oldName := (cmd.raw.find? (·.isOfKind ``Parser.Command.declId)).getD default
  let className := mkIdentFrom oldName (oldName[0].getId ++ `class)
  -- replaces the given name with `name.class`
  let withClassName ← cmd.raw.replaceM fun s =>
    if s.isOfKind ``Parser.Command.declId then return some className else return none
  -- elaborates the `.class` syntax
  elabCommand withClassName
  let newAbbrev ←
    `(command| abbrev $(⟨oldName⟩) : $(mkIdent `MorphismProperty) $(mkIdent `Scheme) := $className)
  elabCommand newAbbrev

mkMorphismProperty
class Foo {X Y : Scheme} (f : X ⟶ Y) : Prop where

Here is one

[Damiano Testa]

I have looked into this a little. First, I found a small bug in the previous code, here is a fix for that other bug (just using an ident where a declId was expected):

elab "mkMorphismProperty " cmd:command : command => do
  let oldName := (cmd.raw.find? (·.isOfKind ``Parser.Command.declId)).getD default
  let className := mkIdentFrom oldName (oldName[0].getId ++ `class)
  let classNameId ← `(declId| $className)
  -- replaces the given name with `name.class`
  let withClassName ← cmd.raw.replaceM fun s =>
    if s.isOfKind ``Parser.Command.declId then return some classNameId else return none
  -- elaborates the `.class` syntax
  elabCommand withClassName
  let newAbbrev ←
    `(command| abbrev $(⟨oldName⟩) : $(mkIdent `MorphismProperty) $(mkIdent `Scheme) := @$className)
  elabCommand newAbbrev

[Damiano Testa]

Second, it looks like MorphismProperty expects strict-implicit binders itself and I think that this is the source of the issue.

[Damiano Testa]

I am really not sure how "good" this change is, but the example that you gave is fixed by adding a @ here:

    `(command| abbrev $(⟨oldName⟩) : $(mkIdent `MorphismProperty) $(mkIdent `Scheme) := @$className)

[Damiano Testa]

(Note the @ at the end, just before $className. I also edited the code above to include this modification.)

[Calle Sönne]

Thanks!

[Damiano Testa]

I think that Kyle's suggestion is better: the "typed" command remains untouched and parsed as is, the "auto-generated one" is completely straightforward and you get a chance to provide a name. Here is an implementation in a similar spirit to the above:

import Mathlib.CategoryTheory.MorphismProperty.Basic
import Mathlib.AlgebraicGeometry.Scheme

open Lean Elab Command in
elab "mkMorphismProperty" tk:("?")? id:(ident ppSpace)? cmd:command : command => do
  let oldName := ((cmd.raw.find? (·.isOfKind ``Parser.Command.declId)).getD default)[0]
  let newName := match id with
                  | some id => id
                  | none =>
                    if let .str a b := oldName.getId then
                      if b.endsWith "Class" then mkIdent (.str a (b.dropRight "Class".length))
                      else
                        default
                    else
                      default
  if newName == default then
    logWarning m!"'mkMorphismProperty' can only autogenerate a name if '{oldName}' ends in 'Class'. \
                  Please provide an explicit name."
  else
  if newName.raw[0].getId == (id.getD default).getId then
    logInfoAt (id.getD default) "The autogenerated name coincides with the provided name: you may omit it."
  -- syntax for `abbrev id : MorphismProperty Scheme := oldName`
  let newAbbrev ←
    `(command| abbrev $newName : $(mkIdent `MorphismProperty) $(mkIdent `Scheme) := @$(⟨oldName⟩))
  if tk.isSome then
    logInfo m!"Autogenerated declaration '{newName}':\n\n{newAbbrev}"
  elabCommand (mkNullNode #[cmd, newAbbrev])

macro "mkMorphismProperty?" id:(ident ppSpace)? cmd:command : command => `(mkMorphismProperty ? $(id)? $cmd)

open CategoryTheory AlgebraicGeometry

-- success
mkMorphismProperty
class FooClass {X Y : Scheme} (f : X ⟶ Y) : Prop where

-- success, but unneeded name
mkMorphismProperty Foo2
class Foo2Class {X Y : Scheme} (f : X ⟶ Y) : Prop where

-- success and verbose
mkMorphismProperty?
class Foo1Class {X Y : Scheme} (f : X ⟶ Y) : Prop where

-- fail
mkMorphismProperty
class FooClass1 {X Y : Scheme} (f : X ⟶ Y) : Prop where

[Calle Sönne]

Thanks! Although there will be more general morphism properties where the arguments are not just the objects of some previously defined category + a morphism (for example the category the morphism takes place in could be an argument). So what I was planning to do was use your original approach, run elabCommand withClassName, then analyze that declaration & use it to define the abbrev (so its important that they get declared separately)

[Damiano Testa]

Ok, that is fine. What I think improves robustness is if the macro/elab does not modify the given command, so that you know that what you typed is certainly part of what gets elaborated, plus possibly some more that depends on that command.

[Damiano Testa]

So, the elab takes cmd and elaborates it as is, and then does extra things. And the user can control the names of the new declarations that are added and also can peek at them by using some ? flag, like in the latest prototype.

[Damiano Testa]

This way, you can inspect what it really is that you are adding easily.

[Damiano Testa]

(This is good for later users, but also for debugging.)

[Calle Sönne]

Yes, good point!