Zulip Chat Archive

Stream: general

Topic: a dedup linter?

Mario Carneiro (Aug 17 2020 at 01:22):

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

Mario Carneiro (Aug 17 2020 at 01:24):

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 (Aug 17 2020 at 02:05):

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

Jalex Stark (Aug 17 2020 at 02:43):

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 (Aug 17 2020 at 02:44):

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 (Aug 17 2020 at 03:18):

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

Johan Commelin (Aug 17 2020 at 03:49):

@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 (Aug 17 2020 at 03:50):

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 (Aug 17 2020 at 10:09):

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 (Aug 17 2020 at 10:17):

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

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

Jalex Stark (Aug 17 2020 at 21:19):

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.

Last updated: Dec 20 2023 at 11:08 UTC