Add Lean 4 backend [AI-assisted]

[septract]

Summary

Add a new backend targeting Lean 4, allowing Lem definitions to be exported as Lean 4 code. This brings the set of supported targets to: OCaml, Coq, HOL4, Isabelle/HOL, Lean 4, LaTeX, and HTML.

The backend is structurally modelled on the Coq backend, adapted for Lean 4 syntax and semantics. Tested against Lean 4.28.0 via the Lake build system.

What's included

• src/lean_backend.ml (~2400 lines) — main backend translating Lem AST to Lean 4 syntax
• lean-lib/ — LemLib Lean 4 runtime library (~720 lines): sets, maps, comparisons, numeric utilities, BitVec operations for machine words
• library/lean_constants — Lean 4 reserved words and typeclass names
• 368 Lean target reps across 28 library files (vs 309 for Coq) — every Coq target rep has a Lean equivalent, plus extras for Lean-specific features
• Supporting changes to 21 shared source files (all guarded behind Target_lean checks — see "Shared code safety" below)
• Documentation in doc/manual/backend_lean.md and updates to README.md
• make lean-libs target generating Lean library files from Lem's standard library
• scripts/lean_coverage.sh — bisect_ppx coverage script used to identify and close untested codepaths (~87% line coverage on lean_backend.ml)

Test suite

• 12 backend tests: Types, Pats, Pats3, Classes2, Classes3, Exps, Coq_test, Coq_exps_test, Record_test, Op, Let_rec, Indreln2 — all generate valid Lean and compile via Lake (57 jobs)
• 44 comprehensive tests with 424 runtime assertions covering: arithmetic, strings, lists, sets, maps, pattern matching, type definitions, type classes, mutual recursion, vectors, machine words (BitVec), cross-module imports, and more
• 2 real-world examples:
  • examples/cpp/ — C++ concurrency model (Cmm.lean, ~1930 generated lines, 34 Lake jobs, 0 errors)
  • examples/ppcmem-model/ — PowerPC memory model (10 .lem files, 10/10 compile, 43 Lake jobs, 0 errors)

Notable design decisions

• Whitespace-sensitive output: Lem's block formatting disabled for Lean; explicit spaces used instead
• UTF-8 output: Meta_utf8 variant in output.ml for correct encoding of →, ×, ∀, ∃
• Constructor scoping: export TypeName (Ctor1 Ctor2 ...) after each inductive — Lean's open is file-local, so export is needed for importers to see constructors
• Termination: recursive functions default to partial def unless a declare {lean} termination_argument = automatic annotation is present; 10 library functions were annotated total, and 3 more redirect to total LemLib wrappers. Only 2 genuinely partial defs remain (unfoldr, leastFixedPointUnbounded)
• deriving BEq, Ord: auto-derived for simple types (non-mutual, no function-typed constructor args); sorry-based instances as fallback for mutual types (Lean's deriving doesn't support mutual inductives)
• Machine words: mword maps to Lean's BitVec with 36 operations implemented in LemLib; int32/int64 use distinct newtype wrappers (LemInt32/LemInt64)
• Type/value namespace unification: Lean shares a single namespace (unlike Lem/Coq/OCaml). rename_top_level.ml seeds constant renaming with type names to handle collisions. Cross-module names included via full env.t_env scan
• Typeclass name avoidance: lean_constants includes Add, Sub, Mul, etc. to prevent clashes with Lean stdlib
• Propositional equality in indreln: == (BEq) converted to = (Prop) in inductive relation antecedents, handling both Lem AST decomposition paths
• n+k pattern rejection: is_lean_pattern_match in patterns.ml triggers guard-based desugaring instead of unsupported n+k patterns
• Tab sanitization: Lean 4 forbids tabs; all whitespace tokens sanitized automatically

Shared code safety

Changes to shared source files are guarded to only affect the Lean backend:

• typed_ast_syntax.ml: class path collection in used_types — only consumed by Lean-specific code in rename_top_level.ml
• rename_top_level.ml: Tc_class renaming returns early for non-Lean targets
• target_trans.ml: class names added to avoid set only when target is Target_lean
• output.ml: block token type kept as Kwd (preserves Coq/HOL/Isabelle spacing); UTF-8 encoding fix (of_string) is universal but correct
• target_binding.ml: e_env fallback only fires when primary lookup fails (low risk, all targets)

Verified: all 6 non-Lean backends (OCaml, Coq, HOL, Isabelle, HTML, LaTeX) produce byte-for-byte identical output on all test files compared to master. Zero regressions.

Known limitations (won't fix)

• 2 genuinely partial def in generated library: unfoldr (user-supplied termination), leastFixedPointUnbounded (iterates until fixpoint). Correctly partial.
• sorry-based instances for mutual types: Lean deriving can't handle mutual inductives. Documented with /- mutual type -/ comments.
• Duplicate Nat/Int instances in Num.lean: nat/natural both map to Nat, int/integer both to Int. Inherent to Lem's design, same in all backends.
• Overlapping BEq instances: from Eq0, SetType, MapKeyType — three paths to BEq a. Lem typeclass design tradeoff.
• O(n²) set operations: list-based representation, same as Coq backend.
• coq_backend_skips.lem: non-positive inductive — fundamental Lean restriction.
• Generated output spacing: double spaces, extra parens — inherited from Lem's output pipeline, affects all backends.

Test plan

• make -C src — compiler builds cleanly
• 12/12 backend tests generate valid Lean and lake build succeeds (57 Lake jobs)
• 44/44 comprehensive tests pass with 424 runtime assertions verified
• lake build in lean-lib/ — LemLib compiles (33 Lake jobs)
• make lean-libs — all library files generated successfully
• examples/cpp/ — Cmm.lean generates and compiles (34 Lake jobs)
• examples/ppcmem-model/ — 10/10 files generate and compile (43 Lake jobs)
• All 6 non-Lean backends produce byte-for-byte identical output vs master (60 file comparisons across OCaml, Coq, HOL, Isabelle, HTML, LaTeX — 0 differences)

🤖 Generated with Claude Code

Co-Authored-By: Claude Opus 4.6 noreply@anthropic.com