Patrick Nicodemus (Apr 27 2023 at 23:17): Patrick Nicodemus (Apr 27 2023 at 23:17):Often it's complained that mathcomp/ssreflect is hard to automate. I think that a large portion of the problem is the presence of many different representations for logically equivalent statements.
For example, negation of a boolean can be written as (~~ b) = true, ~ (b = true), or b = false. One could also choose to represent it as if b then False else True. This got me wondering more generally how automation in theorem proving generally deals with the problems of many distinct representations of logically equivalent sentences.
In an ideal world, in a proof theory textbook, etc., you do not worry about this stuff.
But in the practice I think it is a really substantial barrier to automation, because it substantially increases the length of the proof and the size of the search space - in order to apply theorem X you must have the conclusion in the right form, else the automation tool will not know that it can apply X.
The frequent interruptions to logical reasoning that come with changing the representation is mildly frustrating when handwriting a proof, but it is much more frustrating when trying to figure out how to automate the proof. There is a common dictum to automate whenever possible but I often feel like I have no idea how to write automation which is cognizant of the many different representations of logically equivalent statements because it seems that it will blow up the search space for proofs beyond what is feasible. How do we solve this problem? Can E-graphs be used for something like this?
Last updated: Oct 04 2023 at 20:01 UTC