Checking theorem equivalence

Stream: lean4

[Shubhra Mishra]

Is there a way to check if two theorems are equivalent (a.k.a. if A, then B and if B, then A) in lean4?

image.png

[Ruben Van de Velde]

All true theorems are equivalent

[Alex J. Best]

In the case of your example your two theorems are exactly the same up to renaming of variables. In type theory this is called alpha equivalence. It is certainly possible to write meta-programs that check whether two proved theorems have alpha equivalent types if that is the only thing you want to check for, but there are many more things that humans might consider equivalent that are more subtle than alpha equivalence. As far as I know there is no Lean 4 code to do this just yet, but it shouldn't be too hard to write it
I see now that there is another difference between your theorems, the use of mul_comm, so this is indeed a more subtle problem, that isnt really well defined without more examples!

[Shreyas Srinivas]

Syntactically they are not equivalent, because (a+b)*(a-b) is not identical to (a-b)*(a+b). They are proven equivalent by the commutativity of multiplication. But as Alex and Ruben's different responses indicates, the equivalence is upto you to define. There are many forms of equivalence. Your two theorems are equivalent upto a renaming of variables and commutativity. But they are also equivalent by virtue of being true.

[Shubhra Mishra]

thank you so much! i asked the question because i was wondering if given two formal statements (one of which is an LLM-produced autoformalization, and the second of which is a ground truth formalization), i thought that one way to check how "correct" an autoformalization is could be by checking the two statements: "if A, then B" and "if B, then A". however, as ruben pointed out, any two theorems that are true would lead us to "if true, then true" and "if true, then true," so my idea was flawed. are there other ways to evaluate if two formalizations are "equivalent"? even with manual inspection, isn't it a bit vague what someone might consider a good formalization, and what someone might not? sorry if this is a basic question — i'm fairly new to the world of rigorously formalized math, so still trying to understand it all. thank you! :)

[Shubhra Mishra]

and thank you ruben, alex, and shreyas for your help!

[Shreyas Srinivas]

You are on the right track. If A and B are two propositions, it is fair to say they are equivalent in some sense if A <-> B. It's just that this need not be a straightforward equality in math (not just lean). You might have different additional assumptions for both implications.

[Utensil Song]

The existence of exact?, simp?, aesop? indicate that equivalence up to alpha equivalence + each of them(i.e. what manipulative rules and heuristics are allowed to use) + import(i.e. what lemmas are they allowed to use) is well defined and can be checked by Lean by proving one with sorry then prove the other one using alpha equivalence and the logic in these automation, then swap them.

(Defining them as Prop, and use Lean to prove iff is also applicable for some cases but variables make this a little more invasive to the statement, so if the intention is to keep the statement literal, the solution suggested above will be more feasible. Anyway, this comment is just the proof of the existence of such ability in Lean, not an computable implementation.)

[Utensil Song]

It seems that the intention is to check if these 2 statement are as close as possible, so the definition might be equivalence up to alpha equivalence + exact? or simp? but check if it's just simp only.