is there an easy way to compare 2 defined functions

Stream: new members

[V S]

This might be a very stupid question, but I want to make sure that I'm not missing anything. Say I have two functions f and g, one of which is defined using def constructions, the other is either from Mathlib or also using def but is not written in the same way as a first one. Is there an easy way (a tactic that attempts that, maybe) to check whether they are equivalent?
For example, a proper divisor of natural n is a natural divisor that does not equal n. There is a def Nat.properDivisors in Mathlib and this could also be written like def properDivisors (n : Nat) : Set Nat := {x | x |n ∧ x ≠ n} (although in this example there might be a problem with Set/Finset kind of thing). Even if I use def ProperDivisors ... and write the same definition as in Mathlib, I still can't use a lemma like 'm.properDivisors = ...' to get 'properDivisors m = ...'. Constructs that are obviously equivalent for a human can be written using many different forms and I want to understand with what one can get away with in this regard

[Philippe Duchon]

That's a classical undecidable problem in computer science - in general, telling whether two given programs compute the same result for all possible inputs is undecidable.

Of course in specific cases you may be able to prove that this function and that other function are equivalent, that's not a problem. Like, you can write addition on the natural numbers by recursion on the first or second arguments, and prove that the two are equivalent even though the general problem is undecidable.

In Lean, you can of course write the statement that the two functions are equivalent as \forall x, f x = g x; you can even (I believe) use it in code to write a function whose result depends on that, but your function will then be "non computable" - you won't be able to evaluate it.

[V S]

Philippe Duchon said:

That's a classical undecidable problem in computer science - in general, telling whether two given programs compute the same result for all possible inputs is undecidable.

Of course in specific cases you may be able to prove that this function and that other function are equivalent, that's not a problem. Like, you can write addition on the natural numbers by recursion on the first or second arguments, and prove that the two are equivalent even though the general problem is undecidable.

In Lean, you can of course write the statement that the two functions are equivalent as \forall x, f x = g x; you can even (I believe) use it in code to write a function whose result depends on that, but your function will then be "non computable" - you won't be able to evaluate it.

I see, thank you for clarifications! I thought that there might be something useful for these specific cases, but it's probably up to the person writing in Lean to pick the better function out of all possibilities

[V S]

For some reason I am unable to close the topic, but it should be considered closed I guess

[Kenny Lau]

V S said:

Constructs that are obviously equivalent for a human

You need to understand that Lean is not a human, and it needs everything to be specified exactly. So you can't just have a rule that checks "by vibes" that two definitions are the same and allow you to automatically replace one with the other.

However once you proved that your two definitions are equivalent (still not the same, because one returns Set and one returns Finset), then you can freely rewrite one to the other.