Improving Proof Automation with E-Graphs for Goal Simplification: Experiments and Challenges
2024-10-17
One of the challenges in using proof assistants for verifying software or hardware systems lies in the lack of robust automation to discharge (or simplify) reasonably easy goals. There are many cases where a proof requires only a mix of simple symbolic evaluation and unification to be solved. Specifically, proof obligations can often feel like doing 10 repetitive and not particularly interesting exercises. After the first or second case, it can become boring for the proof engineer. In this talk, we will report on our exploration of simplifying goals in Coq using a proof-search technique based on E-graphs.
Thomas Bourgeat is an Assistant Professor at EPFL.