a dedup linter?

Stream: general

[Mario Carneiro]

What we want to avoid is anything that is O(n^2)

[Mario Carneiro]

False negatives here are because the expr ordering is fairly strict and might not pick up on theorems that we would say are the same but differ in some behind the scenes detail like variable names

[Notification Bot]

This topic was moved here from #new members > Starting to contribute to mathlib by Jalex Stark

[Jalex Stark]

okay, so I guess we can a little bit farther by computing a normal form for exprs that forgets variable names. informally speaking, the algorithm is like
Fix a canonical infinite list of names.
for a given expr, put an order on the variables names by traversing the expr tree and writing them down in the order you see them
rename the nth variable in this expr list to the nth variable in the canonical list

[Jalex Stark]

but this approach doesn't seem like it will get you to a much coarser notion of equivalence than this uh "syntactic equality up to renaming variables"

[Mario Carneiro]

I think expr.lt already does something like this. I would try just using it and see if it needs tweaking after

[Johan Commelin]

@Jalex Stark Maybe you can make all variables explicit during this step, because that might be another source of "the same, but not syntactially so"

[Johan Commelin]

And if the order of two assumptions doesn't matter to the type checker, sort them by their types. That might take care of permutations of the variables.

[Jalex Stark]

Initially with that suggestion I was worried about dependence of later args on earlier ones. But we're just trying to construct a function on expr whose preinages form the right equivalence relation. We don't need the image to be something we can elaborate! (I'll not sure "elaborate" is the right concept.)

[Rob Lewis]

expr.alpha_eqv compares expressions ignoring binder type and bound variable names.

#eval expr.alpha_eqv `(λ {x : ℕ}, 0) `(λ y : ℕ, 0)

[Jalex Stark]

I guess the next step is to peek into the implementation of expr.alpha_eqv and see whether it is already computing normal form exprs and checking expr equality, since that's really what's needed for the linter.