Checking defeq in Command

Stream: lean4

[Adam Topaz]

I would like to write a command which checks whether two declarations in the current environment have defeq types. It seems, however, that docs#Lean.Meta.isDefEq is in the MetaM monad. Is there some function that does this which can be run in CommandElabM?

[Joachim Breitner]

It doesn't get automatically lifted? If not, maybe try liftTermElabM

[Adam Topaz]

can you lift from MetaM to CommandElabM?

[Scott Morrison]

You could just go all the way to IO with something like:

    let ctx := { fileName, fileMap := default }
    let state := { env := env }
    -- From `IO` to `CoreM`:
    Prod.fst <$> (CoreM.toIO · ctx state) do
        -- From `CoreM` to `MetaM`:
        MetaM.run' (ctx := {}) (s := {}) do

[Adam Topaz]

Ok, yes, I was hoping to avoid constructing some empty MetaM context from scratch, but maybe that's the only way?

[Henrik Böving]

given the implementation of liftTermElabM https://github.com/leanprover/lean4/blob/a7efe5b60e86b26fefd4795b46d66af369b97329/src/Lean/Elab/Command.lean#L391-L414 and all the additional care taken for macro scopes I don't think that's a good idea

[Scott Morrison]

(I had that ready to copy and paste, but presumable you can get there from CommandElabM even more easily.)

[Henrik Böving]

why not go joachim's path?

[Adam Topaz]

Henrik Böving said:

I don't think that's a good idea

Sorry, what are you referring to here?

[Scott Morrison]

liftTermElabM is what you want.

[Scott Morrison]

Your MetaM tactic lifts for free to TermElabM, which is even higher up the monad stack, and then liftTermElabM lets you run that from CommandElabM.

[Adam Topaz]

Gotcha. I'll try it out. Thanks!

[Henrik Böving]

Adam Topaz said:

Henrik Böving said:

I don't think that's a good idea

Sorry, what are you referring to here?

well liftTermElabM goes through a lot of effort to do macro scopes related stuff here while the straight to IO approach just doesn't care about that at all so I would assume you can provoke scenarios where stuff breaks.

[Scott Morrison]

I would guess that checking isDefEq on two already elaborated types is fairly safe to do brutally, but why do the guesswork?

[Adam Topaz]

Thanks all, liftTermElabM works perfectly fine for my application. Pasting this here in case it helps anyone else in the future:

import Lean

open Lean Elab Meta Command Term

def A : Nat → Nat := sorry
def B : Nat → Nat := sorry
def C : Nat := sorry

#eval show CommandElabM Unit from do
  let env ← getEnv
  let some A := env.find? `A | unreachable!
  let some B := env.find? `B | unreachable!
  let some C := env.find? `C | unreachable!
  let A := A.type
  let B := B.type
  let C := C.type
  let b1 ← liftTermElabM (isDefEq A B)
  let b2 ← liftTermElabM (isDefEq A C)
  if b1 then IO.println "A and B have the same type"
  if !b2 then IO.println "A and C have different types"

[Kyle Miller]

@Adam Topaz There's a small issue with your code, where if you have universe variables then it will require that they have the exact same names.

[Adam Topaz]

I think I'm okay with that.

[Kyle Miller]

Just to mention it, if you're ok with constants being defeq after some specialization of their universe level parameters, then you could do something like

let b1 ← liftTermElabM do
  let Aty ← inferType (← mkConstWithFreshMVarLevels `A)
  let Bty ← inferType (← mkConstWithFreshMVarLevels `B)
  isDefEq Aty Bty

It might be over-specialized though.

[Adam Topaz]

Is there any particular reason why we don't have an instance of MonadLiftT MetaM CommandElabM?

[Kyle Miller]

I'm not sure you generally want to run MetaM functions with an empty context and no metavariable assignments every time. liftTermElabM (and runTermElabM, which initializes the context with variables) at least delimits where this new context is created.