I will present joint work with Pierre Boutillier, Hugo Herbelin, and Meven Lennon-Bertrand. We are implementing a new algorithm, described in Pierre's PhD thesis and further developed during Meven's internship, for pattern-matching elaboration in Coq. This algorithm starts from a richer form of pattern-matching than what is currently available by default in Coq, handling deep and multiple pattern-matching with dependent types, as proposed by Thierry Coquand in the 1990s, while targeting the same elementary form of pattern-matching present in the Coq kernel.

Most of the design challenges for this algorithm come from handling the equalities that appear at each level of deconstruction of dependent inductive values. I will compare three approaches: one proposed by Healfdene Goguen, Conor McBride, and James McKinna, which relies on the equivalence axiom between homogeneous and heterogeneous equalities (equivalent to the Uniqueness of Identity Proofs); a refinement proposed by Jesper Cockx, which avoids the need for axioms; and the encoding by small inversion, which moves the proofs of deconstruction of the dependencies from the term level to the type level. While these algorithms give an encoding of dependent pattern-matching into the Coq kernel, this discussion leads us to think about what could be a better primitive form of pattern-matching.

Formal theorem proving is challenging for humans as well as for machines. Thanks to recent advances in LLM capabilities, we believe natural language can serve as a universal interface for reasoning about formal proofs. In this talk, 1) we introduce Pétanque, a new lightweight environment to interact with the Coq theorem prover; 2) we present two interactive proof protocols leveraging natural language as an intermediate representation for designing proof steps; 3) we implement beam search over these interaction protocols, using natural language to rerank proof candidates; and 4) we use Pétanque to benchmark our search algorithms on different datasets. We will then discuss the limitations of our approach and possible future directions.