Towards General White-Box Automation: A Typeclass-Guided Context Cleaner

This conference talk from CoqPL 2025 explores the development of "cdestruct," a context cleaner designed as a step toward general white-box automation in Coq. Presented by Thibaut Pérami from the University of Cambridge, the talk addresses a gap in the Coq ecosystem for general white-box proof search engines comparable to Isabelle's fastforce family or Lean's aesop. Learn how cdestruct works to simplify proof contexts using user-specified hints, serving as a foundation for more comprehensive proof automation. The presentation discusses the design decisions behind this tool, drawing from experience in low-level semantics, verification, and other proof assistant ecosystems. Discover how this approach could potentially overcome limitations in existing tools like CoqHammer's sauto tactic by improving extensibility and usability for complex proofs.