Add Lean 4 backend [AI-assisted]

.gitignore

@@ -25,3 +25,44 @@ ocaml-lib/_build_zarith
 tex-lib/lem-libs*.tex
 
 
+# Lean backend build artifacts
+.lake/
+library/*.lean
+!library/gen_lean_constants.lean
+# Generated LemLib files are now tracked (needed for Lake git dependency).
+# Regenerate with: make lean-libs
+# lean-lib/LemLib/[A-Z]*.lean
+tests/backends/*.lean
+tests/backends/*_auxiliary.lean
+tests/backends/*.ml
+tests/backends/*.v
+tests/backends/*.tex
+tests/backends/*.html
+tests/backends/*.thy
+tests/backends/*Script.sml
+tests/backends/lean-test/[A-Z]*.lean
+tests/backends/lean-test/*_auxiliary.lean
+tests/comprehensive/Test_*.lean
+tests/comprehensive/*_auxiliary.lean
+tests/comprehensive/lean-test/Test_*.lean
+tests/comprehensive/lean-test/*_auxiliary.lean
+examples/cpp/Cmm.lean
+examples/cpp/Cmm_auxiliary.lean
+examples/ppcmem-model/*.lean
+examples/ppcmem-model/*_auxiliary.lean
+!examples/ppcmem-model/lakefile.lean
+
+# Build artifacts
+_build/
+main.native
+
+# Coverage
+coverage-report/
+.coverage-switch/
+
+# Local files
+TODO.md
+
+# Tool directories
+.claude/
+_opam/

Makefile

@@ -26,6 +26,7 @@ install:
 	cp -R hol-lib "$(INSTALL_DIR)/share/lem"
 #	cp -R html-lib "$(INSTALL_DIR)/share/lem"
 	cp -R isabelle-lib "$(INSTALL_DIR)/share/lem"
+	cp -R lean-lib "$(INSTALL_DIR)/share/lem"
 #	cp -R tex-lib "$(INSTALL_DIR)/share/lem"
 
 uninstall:
@@ -46,7 +47,7 @@ lem_dep.pdf: lem_dep.tex
 	pdflatex lem_dep.tex
 
 # this runs Lem on the Lem library (library/*.lem), leaving the
-# generated OCaml, Coq, HOL4, and Isabelle files to ocaml-libs,
+# generated OCaml, Coq, HOL4, Isabelle, and Lean 4 files to ocaml-libs,
 # hol-libs, etc.
 libs_phase_1: 
 	$(MAKE) -C library
@@ -62,6 +63,7 @@ libs_phase_2:
 	$(MAKE) hol-libs
 	$(MAKE) coq-libs
 	$(MAKE) isa-libs
+	$(MAKE) lean-libs
 
 hol-libs: 
 #	$(MAKE) -C library hol-libs
@@ -77,13 +79,44 @@ isa-libs:
 #	$(MAKE) -C library isa-libs
 	isabelle build -d isabelle-lib -b LEM
 
-coq-libs: 
+coq-libs:
 #	$(MAKE) -C library coq-libs
 	cd coq-lib; coqc -R . Lem coqharness.v
 	cd coq-lib; coq_makefile -f coq_makefile.in > Makefile
 	$(MAKE) -C coq-lib
 
-tex-libs: 
+lean-libs:
+	$(MAKE) -C library lean-libs
+
+# Run the full Lean backend test suite:
+#   1. Build the compiler
+#   2. Regenerate and compile the Lean library (lean-lib/)
+#   3. Backend tests (tests/backends/ — 12 .lem files)
+#   4. Comprehensive tests (tests/comprehensive/ — 48 .lem files, 300+ assertions)
+#   5. ppcmem-model example (examples/ppcmem-model/ — 10 .lem files)
+#   6. cpp example (examples/cpp/ — 1 large .lem file, ~1930 lines generated)
+lean-tests: bin/lem lean-libs
+	cd lean-lib && lake build
+	$(MAKE) -C tests/backends leantests
+	$(MAKE) -C tests/comprehensive lean
+	cd examples/ppcmem-model && \
+		../../lem -wl ign -lean \
+			bitwiseCompatibility.lem \
+			machineDefUtils.lem \
+			machineDefFreshIds.lem \
+			machineDefValue.lem \
+			machineDefTypes.lem \
+			machineDefInstructionSemantics.lem \
+			machineDefStorageSubsystem.lem \
+			machineDefThreadSubsystem.lem \
+			machineDefSystem.lem \
+			machineDefAxiomaticCore.lem && \
+		lake build
+	cd examples/cpp && \
+		../../lem -wl ign -lean cmm.lem && \
+		lake build
+
+tex-libs:
 #	$(MAKE) -C library tex-libs
 	cd tex-lib; pdflatex lem-libs.tex
 	cd tex-lib; pdflatex lem-libs.tex
@@ -261,6 +294,7 @@ distrib: src/ast.ml version
 	mkdir $(DDIR)/library/isabelle
 	mkdir $(DDIR)/library/ocaml
 	cp library/*.lem $(DDIR)/library/
+	cp library/*_constants $(DDIR)/library/
 	cp library/isabelle/constants $(DDIR)/library/isabelle/
 	cp library/isabelle/*.lem $(DDIR)/library/isabelle/
 	cp library/hol/constants $(DDIR)/library/hol/
@@ -271,6 +305,9 @@ distrib: src/ast.ml version
 	cp ocaml-lib/*.mli $(DDIR)/ocaml-lib	
 	cp ocaml-lib/*.mllib $(DDIR)/ocaml-lib	
 	cp ocaml-lib/Makefile $(DDIR)/ocaml-lib	
+	mkdir $(DDIR)/lean-lib
+	cp lean-lib/*.lean $(DDIR)/lean-lib
+	-cp lean-lib/lean-toolchain $(DDIR)/lean-lib
 	mkdir $(DDIR)/tex-lib
 	cp tex-lib/lem.sty $(DDIR)/tex-lib
 	cp Makefile-distrib $(DDIR)/Makefile
@@ -299,6 +336,7 @@ clean:
 	-rm -f coq-lib/Makefile
 	-rm -f coq-lib/coqharness.vo
 	-rm -f coq-lib/coqharness.glob
+	-rm -rf lean-lib/.lake lean-lib/build
 	-rm -rf src/version.ml lem library/lib_cache src/share_directory.ml
 	#-rm -rf lem_dep.tex lem_dep.pdf lem_dep.aux lem_dep.log
 

README.md

@@ -3,8 +3,8 @@
 Lem is a tool for lightweight executable mathematics, for writing,
 managing, and publishing large-scale portable semantic definitions,
 with export to LaTeX, executable code (currently OCaml) and
-interactive theorem provers (currently Coq, HOL4, and Isabelle/HOL,
-though the generated Coq is not necessarily idiomatic).  It is also
+interactive theorem provers (currently Coq, HOL4, Isabelle/HOL, and
+Lean 4).  It is also
 intended as an intermediate language for generating definitions from
 domain-specific tools, and for porting definitions between interactive
 theorem proving systems.
@@ -86,6 +86,7 @@ Running `make` only generates Lem. It not generate the libraries needed to use L
 - for HOL4 : `make hol-libs`
 - for Isabelle: `make isa-libs`
 - for Coq : `make coq-libs`
+- for Lean 4 : `make lean-libs`
 
 These targets depend on the corresponding tool being installed. If you
 just want to generate the input that Lem gives to these tools, please
@@ -113,6 +114,7 @@ Lem has been tested against the following versions of the backend software:
   * Coq: 8.16.0
   * Isabelle 2022
   * HOL: HOL4 Kananaskis 14
+  * Lean: 4.28.0 (via Lake build system)
 
 ## Examples
 

doc/manual/Makefile

@@ -8,6 +8,7 @@ INPUT_FILES := \
     backend_hol.md \
     backend_isa.md \
     backend_coq.md \
+    backend_lean.md \
     backend_tex.md \
     backend_html.md \
   library.md \

doc/manual/backend_lean.md

@@ -0,0 +1,81 @@
+## Lean 4
+
+The command line option `-lean` instructs Lem to generate Lean 4 output. A module with name `Mymodule` generates a file `Mymodule.lean` and possibly `Mymodule_auxiliary.lean`.
+
+### Compilation
+Lem-generated Lean code depends on a Lem-specific Lean library found in the `lean-lib/` directory. This library (`LemLib`) provides helper definitions used by the generated output, such as set and map operations, comparison functions, and numeric utilities. Running `make lean-libs` in Lem's main directory generates Lean versions of the Lem library files into the `lean-lib/LemLib/` subdirectory. The generated library modules live under the `LemLib` namespace (e.g. `LemLib.Bool`, `LemLib.Pervasives`), and imports in generated code use this qualified form.
+
+To compile the generated code, set up a [Lake](https://lean-lang.org/lean4/doc/setup.html) project that depends on `LemLib`. A minimal `lakefile.lean` looks like:
+
+    import Lake
+    open Lake DSL
+
+    package MyProject where
+      version := v!"0.1.0"
+
+    require LemLib from "path/to/lem/lean-lib"
+
+    @[default_target]
+    lean_lib MyLib where
+      roots := #[`MyModule]
+
+Then run `lake build` to compile. Lem has been tested against Lean 4.28.0.
+
+### Auxiliary Files
+Lean auxiliary files contain executable tests generated from *assertions* in the input files, as well as proof obligations from *lemmata* and *theorems*. They are compiled alongside the main files by `lake build`. Assertions generate `#eval` commands that check the boolean expression at build time, printing PASS/FAIL results. Lemmata and theorems generate `theorem` declarations with `by decide`, which succeeds for decidable propositions. The command line option `-auxiliary_level auto` allows generating only the executable assertion tests.
+
+### Recursive Definitions
+Recursive function definitions are marked `partial` in the generated Lean output by default, since Lean 4 requires termination proofs for non-partial definitions. This is conservative but correct: the generated code will compile without requiring termination proofs. For functions that are structurally recursive (and therefore trivially terminating), using `declare {lean} termination_argument` with `automatic` avoids the `partial` annotation, allowing Lean to verify termination automatically.
+
+### Inductive Relations
+Lem inductive relation definitions are translated to Lean `inductive` types with a `Prop`-valued conclusion. For example, a Lem relation `indreln add : nat -> nat -> nat -> bool` generates `inductive add : Nat → Nat → Nat → Prop where`. Mutually recursive inductive relations (defined with `and`) are wrapped in Lean's `mutual`/`end` blocks.
+
+### Machine Words
+Lem's `mword` type (machine words parameterised by bit width) is mapped to Lean's `BitVec` type. All standard machine word operations (arithmetic, bitwise, comparison, conversion) have Lean target representations in the library. The `int32` and `int64` types are mapped to distinct newtype wrappers (`LemInt32`, `LemInt64`) around `Int`.
+
+### Automatic Derivation
+The Lean backend automatically derives `BEq` and `Ord` instances for generated inductive types and records, provided none of their constructor arguments have function types and the type is not part of a mutual block. This allows equality testing and comparison on most generated types without manual instance declarations. Types that cannot use `deriving` (e.g. those with function-typed fields or mutual definitions) get `sorry`-based stub instances at low priority instead.
+
+### Inhabited Instances
+The backend generates `Inhabited` instances for all types. When a safe constructor is available (nullary, or non-self-referential), it provides a real default value. When no safe constructor exists, the backend generates a `noncomputable instance` using the `DAEMON` axiom from LemLib. This satisfies Lean's `Inhabited` requirement for `partial def` without causing init-time panics, and without requiring typeclass constraints or `unsafe` code.
+
+Types containing `DAEMON`-backed types as direct constructor arguments may trigger compile errors ("depends on noncomputable definition"). This is intentional: these types genuinely have no computable default. The fix is `skip_instances` (see below) or marking downstream code as `noncomputable`.
+
+### Skipping Instance Generation
+The `skip_instances` declaration suppresses all auto-generated typeclass instances for a type:
+
+    declare {lean} skip_instances type my_type
+
+This skips generation of `Inhabited`, `BEq`, `Ord`, `SetType`, `Eq0`, and `Ord0` instances. The user provides these instances in a hand-written Lean file included in their Lake project. This is useful for types where the user needs full control over instance implementations (e.g. real BEq/Ord for mutual types, or computable Inhabited for types that would otherwise get DAEMON).
+
+The declaration is scoped to the Lean backend (`{lean}`) and has no effect on other backends.
+
+### Effectful Target Representations
+Functions mapped via `target_rep` to side-effecting implementations (mutable counters, global state) should be marked with the `effectful` declaration. This prevents Lean's compiler from merging multiple calls to the same function:
+
+    declare lean target_rep function fresh_int u = `CerberusFresh.freshIntIO`
+    declare {lean} effectful val fresh_int
+
+The target function should return `BaseIO α`. The backend wraps each call site in `runEffectful(...)` to extract the result. Arguments must be passed through in the target_rep body — see the general `target_rep` documentation in `backend_linking.md`.
+
+### Extra Imports
+The `extra_import` declaration injects an import into the generated Lean file:
+
+    declare {lean} extra_import `MyHandwrittenInstances`
+
+This causes the generated `.lean` file to include `import MyHandwrittenInstances` in its import list. Use this when a generated module needs to see typeclass instances (e.g. BEq, Ord) from a hand-written Lean file. Place the declaration in the consuming `.lem` file, not the file that defines the types, to avoid circular imports.
+
+### Automatic Renaming
+Lean 4 types and values share a single namespace, unlike many other backends. The Lean backend automatically renames constants that would collide with type names in the same module or in imported modules. Additionally, certain names that clash with Lean 4 standard library type classes (such as `Add`, `Sub`, `Neg`, `Mul`, `Div`, `Mod`, `Pow`, `Min`, `Max`, `Abs`, `Not`, `Append`) are automatically renamed to avoid ambiguity.
+
+### Relationship to Coq Backend
+The Lean backend is structurally modelled on the Coq backend, as Lean 4 and Coq are similar in many respects. Key differences in the generated output include:
+
+- Lean 4 syntax: `structure`/`where` for records, `inductive` for datatypes, `def` for definitions
+- Unicode operators: `→`, `×`, `∀`, `∃` instead of ASCII equivalents
+- Native record update syntax: `{ r with field := value }`
+- Constructors brought into scope via `export TypeName` after each `inductive` definition
+- `Inhabited` typeclass instances generated for all types (uses `noncomputable` DAEMON axiom for types without safe constructors)
+- `BEq` and `Ord` derivation for types without function-typed arguments
+- `sorry` for undefined/opaque terms instead of Coq's `DAEMON`
+- `partial` for recursive definitions by default (can be overridden with `termination_argument`)

doc/manual/backend_linking.md

@@ -23,6 +23,7 @@ A `target_rep` declaration allows specifing which _existing_ target function sho
     declare hol      target_rep function not x = `~` x
     declare isabelle target_rep function not x = `\<not>` x
     declare coq      target_rep function not = `negb`
+    declare lean     target_rep function not = `not`
 
     declare html     target_rep function not = `&not;`
     declare tex      target_rep function not b = `$\neg$` b
@@ -39,10 +40,11 @@ A `target_rep` declaration allows specifing which _existing_ target function sho
 ## Target Representations of Types
 
     type map 'k 'v
-    declare ocaml    target_rep type map = `Pmap.map` 
-    declare isabelle target_rep type map = `Map.map` 
+    declare ocaml    target_rep type map = `Pmap.map`
+    declare isabelle target_rep type map = `Map.map`
     declare hol      target_rep type map = `fmap`
     declare coq      target_rep type map = `fmap`
+    declare lean     target_rep type map = `Fmap`
 
 
 ## Infix Operations
@@ -57,6 +59,7 @@ A `target_rep` declaration allows specifing which _existing_ target function sho
     declare ocaml    target_rep function (&&) = infix `&&`
     declare isabelle target_rep function (&&) = infix `\<and>`
     declare coq      target_rep function (&&) = infix `&&`
+    declare lean     target_rep function (&&) = infix `&&`
     declare html     target_rep function (&&) = infix `&and;`
     declare tex      target_rep function (&&) = infix `$\wedge$`
 

doc/manual/introduction.md

@@ -3,7 +3,7 @@
 Lem is a lightweight tool for writing, managing, and publishing large scale
 semantic definitions. It is also intended as an intermediate language for
 generating definitions from domain-specific tools, and for porting definitions
-between interactive theorem proving systems (such as Coq, HOL4, and Isabelle).
+between interactive theorem proving systems (such as Coq, HOL4, Isabelle, and Lean 4).
 
 The language combines features familiar from functional programming languages with logical constructs. 
 From functional programming languages we take
@@ -30,7 +30,7 @@ inductive relations, and for assertions.
 
 Lem typechecks its input and can 
 generate executable OCaml, 
-theorem prover definitions in Coq, HOL4 and Isabelle/HOL, 
+theorem prover definitions in Coq, HOL4, Isabelle/HOL, and Lean 4,
 typeset definitions in LaTeX, and simple HTML.
 
 ## Supported software
@@ -41,6 +41,7 @@ Lem is tested against the following versions of the backend software:
   * Coq: 8.4pl3 and 8.4pl2
   * Isabelle: Isabelle-2013-2
   * HOL: HOL4 Kananaskis 9
+  * Lean: 4.28.0
 
 Older or newer versions of this software may work correctly with Lem, but are unsupported.
 

doc/manual/invocation.md

@@ -6,14 +6,15 @@ The most basic usage of Lem is running a command like
 
 This command loads the lem files `input1.lem` through `inputn.lem` and outputs their translation to target `target` in the same directory as the input files. Multiple target arguments are possible. For example
 
-    lem name1.lem name2.lem -ocaml -hol -isa -coq 
+    lem name1.lem name2.lem -ocaml -hol -isa -coq -lean
 
 creates the following files (assuming there are no type errors, and no explicit renaming in the source files):
-  
+
   - `name1.ml` and `name2.ml` for target `ocaml`
   - `name1Script.sml`, `name2Script.sml` for target `hol`
   - `Name1.thy`, `Name2.thy` for target `isa`
   - `name1.v`, `name2.v` for target `coq`
+  - `Name1.lean`, `Name2.lean` for target `lean`
 
 There are auxiliary files generated as well, which are discussed later.
 
@@ -27,6 +28,7 @@ The following command line options tell Lem to generate output for certain backe
 - `-hol`  generate HOL4 output
 - `-isa`  generate Isabelle/HOL output
 - `-coq`  generate Coq output
+- `-lean` generate Lean 4 output
 
 - `-tex`  generate LaTeX output for each module separately. This means that for each input file, a separate output `.tex` file is created. These files contain the pretty-printed input.
 
@@ -59,7 +61,7 @@ By default Lem generates all available auxiliary output. The command-line option
 `-auxiliary_level auto` causes only automatically processable output like testing code of assertions to be generated. `-auxiliary_level none` turns off the generation of auxiliary files. One can also turn off the generation of the main files and only generate the auxiliary ones using `-only_auxiliary`. 
 
 ## Updating Existing Output
-When using multi-file Lem developments, it might be handy to only update the output files that really changed. This allows the build-tools of backends like OCaml, HOL, Isabelle or Coq to only recompile files that really need to. Lem supports this via the command line option `-only_changed_output`.
+When using multi-file Lem developments, it might be handy to only update the output files that really changed. This allows the build-tools of backends like OCaml, HOL, Isabelle, Coq or Lean to only recompile files that really need to. Lem supports this via the command line option `-only_changed_output`.
 
 ## Warnings
 Lem can print warning messages about various things. Common warnings are about unused variables, name clashes that required automatic renaming of some entities or the need for pattern compilation, but there are many more. Warning options start with the prefix `wl`. They can be set to 4 different values

doc/manual/language.md

@@ -208,13 +208,14 @@
 ## Target Descriptions
 
     target ::=  {{ Backend target names }}
-      | hol             
-      | isabelle        
-      | ocaml   
-      | coq             
-      | tex             
-      | html    
-      | lem     
+      | hol
+      | isabelle
+      | ocaml
+      | coq
+      | lean
+      | tex
+      | html
+      | lem
 
     targets  ::=  {{ Backend target name lists }}
       | { target1 ; .. ; targetn }