In the context of interactive theorem provers based on a dependent type theory, automation tactics (dedicated decision procedures, call of automated solvers, ...) are often limited to goals which are exactly in some expected logical fragment. This very often prevents users from applying these tactics in other contexts, even similar ones. This paper discusses the design and the implementation of pre-processing operations for automating formal proofs in the Coq proof assistant. It presents the implementation of a wide variety of predictible, atomic goal transformations, which can be composed in various ways to target different backends. A gallery of examples illustrates how it helps to expand significantly the power of automation engines.

翻译：在基于依赖类型理论的交互式定理证明器中，自动化策略（专用决策过程、自动求解器调用等）通常仅限于完全符合某些预期逻辑片段的目标。这往往导致用户无法在其他情境（即便是相似情境）中应用这些策略。本文讨论了在Coq证明助手中自动化形式证明的预处理操作的设计与实现。它实现了一系列可预测的原子目标变换，这些变换可通过多种方式组合以适配不同的后端模块。通过一组实例展示，该方法显著扩展了自动化引擎的能力。