Types up to variable renaming

Stream: Is there code for X?

[Anthony Bordg]

Is there code for determining whether two types are the same (say, up to definitional equality, or maybe even literally) up to renaming of the variables that appear in these types?

[Ruben Van de Velde]

Equality of types is not likely to be a concept you want to work with

[Anthony Bordg]

(This is not for a formalization project).

[Yaël Dillies]

Maybe this question belongs in #metaprogramming / tactics ?

[Anthony Bordg]

Yes, possibly; since there may already exist some code for that (e.g. in Lean.Meta?) I thought I should try here first.

[Kyle Miller]

Could you give some examples of interesting pairs with answers of 'yes' and 'no'? There are a few things you could be meaning here, and that would pin it down (and give people some test cases to work toward)

[Jireh Loreaux]

The implementation of docs#Lean.Parser.Tactic.guardTarget is probably relevant. isn't renaming just α-equivalence?

[Kyle Miller]

@Jireh Loreaux If I remember correctly, all that means is that it uses ==, which ignores binder names; if you check just the de Bruijn indices you get alpha equivalence checking for free.

[Kyle Miller]

If there were a way to reliably abstract the variables to create lambdas that close them, in some fixed order, that would be a way to check for this kind of alpha equivalence.

[Kyle Miller]

A reason I'm asking for some positive and negative pairs is that I'd like to see what's special about types vs general expressions.

[Yaël Dillies]

Yaël Dillies said:

Maybe this question belongs in #metaprogramming / tactics ?

I'm just suggesting this because which stream you post in influences the default reply that ruben-bot posts :robot:

[Ruben Van de Velde]

:robot:

[Anthony Bordg]

Jireh Loreaux said:

The implementation of docs#Lean.Parser.Tactic.guardTarget is probably relevant. isn't renaming just α-equivalence?

Yes, this is simply $\alpha$-equivalence. I will try to refine what I really want to achieve, but $\alpha$-equiv is certainly part of it.

[Anthony Bordg]

One limitation of #guard_expr e =ₐ e' is that it expects two pure expressions e and e'. Can one use #guard_expr with the outputs of some function (that would take as input the name of a def/theorem and returns its associated expression as output)?

[Aaron Liu]

Maybe by_elab?

[Anthony Bordg]

Kyle Miller said:

A reason I'm asking for some positive and negative pairs is that I'd like to see what's special about types vs general expressions.

If you imply that I should consider the lambda expression associated with an identifier instead of its type, I think you're right.

[Eric Wieser]

Or possibly delta%?

[Anthony Bordg]

by_elab seems to work fine. For instance:

def name1 : ℕ → (ℕ → ℕ) → ℕ := λ n f ↦ f n
def name2 : ℕ → (ℕ → ℕ) → ℕ := λ m g ↦ g m

def getDeclExpr (n : Name) : MetaM Expr := do
  let env ← getEnv
  match env.find? n with
  | some decl =>
    match decl.value? with
    | some val => return val
    | none     => throwError "Declaration {n} has no value (might be opaque or a constant)"
  | none => throwError "Declaration {n} not found"

#guard_expr (by_elab getDeclExpr `name1) =ₐ (by_elab getDeclExpr `name2)