Expr equal up to mvars

Stream: lean4

[Marcus Rossel]

Is there a way to check whether two Exprs are equal up to renaming of mvars? So something like:

import Lean
open Lean Meta Elab Term

#eval show TermElabM Unit from do
  let (_, _, comm₁) ← forallMetaTelescope <| ← inferType <| ← elabTerm (← `(Nat.add_comm)) none
  let (_, _, comm₂) ← forallMetaTelescope <| ← inferType <| ← elabTerm (← `(Nat.add_comm)) none
  println! equalUpToMVars comm₁ comm₂ -- prints true

[Jovan Gerbscheid]

In the implementation of type class resolution, type class goals are stored in a HashMap up to metavariable renaming. They use the function docs#Lean.Meta.SynthInstance.mkTableKey to rename the metavariables. So this should do the job:

import Lean
open Lean Meta Elab Term SynthInstance

#eval show TermElabM Unit from do
  let (_, _, comm₁) ← forallMetaTelescope <| ← inferType <| ← elabTerm (← `(Nat.add_comm)) none
  let (_, _, comm₂) ← forallMetaTelescope <| ← inferType <| ← elabTerm (← `(Nat.add_comm)) none
  println! (← mkTableKey (← instantiateMVars comm₁)) == (← mkTableKey (← instantiateMVars comm₂)) -- prints true

[Marcus Rossel]

Wow, that is not the answer I was expecting :big_smile: Thanks!

[Kyle Miller]

I'd be wary of making use of APIs like this not for their intended purpose.

By the way, this does not check that the mvars can be permuted. For example, this prints true:

#eval show TermElabM Unit from do
  let comm₁ ← elabTerm (← `((_ : Int))) none
  let comm₂ ← elabTerm (← `((_ : Nat))) none
  println! (← mkTableKey (← instantiateMVars comm₁)) == (← mkTableKey (← instantiateMVars comm₂))

[Kyle Miller]

Another function you could use is docs#Lean.Meta.abstractMVars and then check that the results are ==.