checking if two Exprs are defeq

Stream: metaprogramming / tactics

[Bryan Gin-ge Chen]

Given two Exprs (in my specific use case, one is tgtDecl.type for a certain tgtDecl : ConstantInfo and the other is generated from another decl : Constantinfo via the to_additive machinery), is there an easy way to check whether they're defeq?

I tried the obvious thing of using isDefEq expr1 expr2 but ran into the issue (mentioned as a possibility by @Kyle Miller in #lean4 > Checking defeq in Command @ 💬 ) that the unverse variables sometimes happen to have different names which then causes the defeq check to fail.

This is extracted from #mathlib4 > Order dual tactic @ 💬. @Aaron Liu did give some suggestions in that thread but due to my inexperience I wasn't able to turn them into concrete code. Sorry!

[Kyle Miller]

Given that they are both from ConstantInfos, we have the lists of universe level parameters available — do you expect the universe levels to match up, or do you think they're going to be permutations?

[Kyle Miller]

If the match up, we could start by renaming all the levels in one of the expressions, and then go ahead with isDefEq.

[Bryan Gin-ge Chen]

Good question; I can't think of any cases where they would end up permuted, but maybe I'm missing some bizarre use case.

[Kyle Miller]

If you zip up the parameter lists to make the mapping, docs#Lean.Expr.replaceLevel seems useful

[Kyle Miller]

Actually, docs#Lean.Expr.instantiateLevelParams seems even better

[Kyle Miller]

Expr.initiateLevelParams decl.type decl.levelParams (tgtDecl.levelParams.map mkLevelParam)

[Kyle Miller]

Or docs#Lean.ConstantInfo.instantiateTypeLevelParams, which lets you write decl.initiateTypeLevelParams (tgtDecl.levelParams.map mkLevelParam)

[Bryan Gin-ge Chen]

Awesome! I ended up going with the first variant:

/-- Run applyReplacementFun on the type of given `srcDecl` and return the resulting `Expr` -/
def checkDeclType (b : BundledExtensions)
    (tgt : Name) (srcDecl tgtDecl : ConstantInfo) (reorder : List (List Nat) := []) :
    MetaM (Expr × Bool) := do
  let mut decl := srcDecl.updateName tgt
  if 0 ∈ reorder.flatten then
    decl := decl.updateLevelParams decl.levelParams.swapFirstTwo
  let decl_type := decl.type.instantiateLevelParams
    decl.levelParams (tgtDecl.levelParams.map mkLevelParam)
  let exp ← applyReplacementFun b <| ← reorderForall reorder
    <| ← expand b <| ← unfoldAuxLemmas decl_type
  return ⟨exp, ← isDefEq exp tgtDecl.type⟩

This now works perfectly on all the examples that were failing before! Thanks so much!