Designing Proof Deautomation for Rocq

<p dir="ltr">Proof assistant users rely on automation to reduce the burden of writing and maintaining proofs. By design, automation hides the details of intermediate proof steps, making proofs shorter and more robust. However, we observed in a need-finding study that users sometimes do want to examine the details of these intermediate steps, especially to understand how the proof works or why it has failed. To support such activities, we describe a proof deautomation procedure that reconstructs the underlying steps of an automated proof. We discuss the design considerations that shaped our approach to deautomation — in particular, the requirement that deautomation should remain informative even for failing proofs.</p>