Domain-specific languages (DSLs) mediate interactions between interactive proof assistants and external automation, but translating between the prover's internal representation and such DSLs is a tedious engineering chore. To simplify this task, we present DSLean, a framework for bidirectional translation between expressions in the Lean proof assistant and external syntax. DSLean requires only a specification of an external language and its Lean equivalents, abstracting away meta-level implementation details. We demonstrate DSLean's capabilities by implementing three new automation tactics, providing access to external solvers for interval arithmetic, ordinary differential equations, and ring ideal membership.

翻译：领域特定语言（DSL）在交互式证明助手与外部自动化工具之间起到中介作用，但将证明助手的内部表示与此类DSL进行相互转换是一项繁琐的工程任务。为简化这一过程，本文提出DSLean，一个用于在Lean证明助手的表达式与外部语法之间进行双向转换的框架。DSLean仅需提供外部语言及其在Lean中等价物的规范，从而抽象掉元级的实现细节。我们通过实现三个新的自动化策略来展示DSLean的能力，这些策略提供了对区间算术、常微分方程及环理想成员关系的外部求解器的访问。