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

TL;DR

DSLean is a framework that simplifies the creation of bidirectional translations between Lean 4 and external domain-specific languages, enabling easier integration of external solvers and automation tactics.

Contribution

It introduces a generic framework that abstracts implementation details, allowing seamless interoperability between Lean 4 and external DSLs with minimal specification effort.

Findings

Successfully implemented three automation tactics using DSLean

Enabled access to external solvers for complex mathematical problems

Simplified the process of translating between Lean and external languages

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.