Autosubst-ocaml

Autosubst-OCaml is an OCaml reimplementation of the Autosubst 2 code generator, designed to automate the tedious process of formalizing substitution and renaming for languages with binders in Coq. It produces Coq source code that includes inductive type definitions, substitution and renaming operations, lemmas about their behavior, and a tactic for solving substitution equations, significantly reducing manual proof effort in metatheoretic developments.

Key Features

• Language Representation — Generates (mutual) inductive types for syntax using de Bruijn indices, supporting both well-scoped and unscoped variants.
• Substitution & Renaming — Automatically defines capture-avoiding substitution and renaming functions for de Bruijn variables.
• Behavioral Lemmas — Produces lemmas describing substitution composition and extensionality, without relying on functional extensionality.
• Equation Solver — Provides an asimpl tactic to simplify and solve assumption-free substitution equations in proofs.
• Variadic & Polyadic Syntax — Supports variadic and polyadic syntax constructs and functors like list, prod, cod, and option.

Philosophy

The tool prioritizes reducing boilerplate and manual proof work in formal metatheory, enabling researchers and developers to focus on higher-level reasoning rather than low-level substitution details.