Papers With

← All papers
First page of DSLean: A Framework for Type-Correct Interoperability Between Lean 4 and External DSLs

DSLean: A Framework for Type-Correct Interoperability Between Lean 4 and External DSLs

Tate Rowney, Riyaz Ahuja, Jeremy Avigad, Sean Welleck

cs.LO Feb 20, 2026 · v3
tooling tactic-automation
Read PDF arXiv abstract Code
TL;DR
Implements DSLean in Lean 4 metaprogramming for bidirectional translation with external DSLs, used to build gappa, desolve, and lean_m2 tactics.
Abstract
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.
Problem

Lean tactics that rely on external solvers must translate between Lean expressions and the solver's domain-specific language. Writing these translations takes bespoke meta-level parsing and elaboration code that is hard to maintain and requires Lean metaprogramming expertise.

Approach

DSLean is a framework written entirely in Lean. Users declare equivalences between external syntax patterns and Lean terms. Translation out of Lean works by recursively partially matching expressions against these patterns. Translation into Lean parses raw text with Lean's native parser and combines the matched pieces via metavariable unification, which enforces type-correctness and handles implicit arguments, polymorphism, and postponed elaboration.

Results

Three tactics were built on DSLean. gappa translates Rocq-syntax certificates from the Gappa interval arithmetic solver into Lean proofs. desolve uses SageMath to obtain general solutions to ordinary differential equations. lean_m2 uses Macaulay2 to supply witnesses for ring ideal membership and Gröbner basis problems. Each tactic has a short, readable implementation.