karpal_verify/
lean.rs

1// Copyright (C) 2026 Industrial Algebra
2// SPDX-License-Identifier: Apache-2.0
3
4#[cfg(not(feature = "std"))]
5use alloc::{
6    collections::BTreeSet,
7    format,
8    string::{String, ToString},
9    vec,
10    vec::Vec,
11};
12#[cfg(feature = "std")]
13use std::{collections::BTreeSet, format, string::String, vec::Vec};
14
15use crate::{
16    Obligation, ObligationBundle,
17    obligation::{Sort, Term},
18};
19
20/// Marker for the Lean 4 backend.
21pub struct Lean4;
22
23/// A Lean module import.
24#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord)]
25pub struct LeanImport {
26    pub module: String,
27}
28
29impl LeanImport {
30    pub fn new(module: impl Into<String>) -> Self {
31        Self {
32            module: module.into(),
33        }
34    }
35}
36
37/// A Lean-safe alias for a raw symbol name from the obligation IR.
38#[derive(Debug, Clone, PartialEq, Eq)]
39pub struct LeanAlias {
40    pub alias: String,
41    pub target: String,
42}
43
44impl LeanAlias {
45    pub fn new(alias: impl Into<String>, target: impl Into<String>) -> Self {
46        Self {
47            alias: alias.into(),
48            target: target.into(),
49        }
50    }
51}
52
53/// Prelude metadata emitted ahead of theorem declarations.
54#[derive(Debug, Clone, PartialEq, Eq, Default)]
55pub struct LeanPrelude {
56    pub imports: Vec<LeanImport>,
57    pub aliases: Vec<LeanAlias>,
58}
59
60impl LeanPrelude {
61    pub fn new() -> Self {
62        Self::default()
63    }
64
65    pub fn with_import(mut self, module: impl Into<String>) -> Self {
66        let import = LeanImport::new(module);
67        if !self.imports.contains(&import) {
68            self.imports.push(import);
69        }
70        self
71    }
72
73    pub fn with_alias(mut self, alias: impl Into<String>, target: impl Into<String>) -> Self {
74        let alias = LeanAlias::new(alias, target);
75        if !self
76            .aliases
77            .iter()
78            .any(|existing| existing.target == alias.target)
79        {
80            self.aliases.push(alias);
81        }
82        self
83    }
84
85    pub fn for_obligations(obligations: &[Obligation]) -> Self {
86        let mut prelude = Self::new();
87        let mut symbols = BTreeSet::new();
88
89        for obligation in obligations {
90            collect_term_symbols(&obligation.conclusion, &mut symbols);
91            for assumption in &obligation.assumptions {
92                collect_term_symbols(assumption, &mut symbols);
93            }
94        }
95
96        for symbol in symbols {
97            if !is_lean_identifier(&symbol) {
98                prelude = prelude.with_alias(alias_name(&symbol), symbol);
99            }
100        }
101
102        prelude
103    }
104
105    pub fn symbol_name(&self, target: &str) -> String {
106        self.aliases
107            .iter()
108            .find(|alias| alias.target == target)
109            .map(|alias| alias.alias.clone())
110            .unwrap_or_else(|| render_identifier(target))
111    }
112}
113
114/// Structured Lean theorem metadata derived from an obligation.
115#[derive(Debug, Clone, PartialEq, Eq)]
116pub struct LeanTheorem {
117    pub obligation_name: String,
118    pub theorem_name: String,
119    pub property: String,
120    pub origin_summary: String,
121    pub declaration_start_line: usize,
122    pub declaration_end_line: usize,
123}
124
125impl LeanTheorem {
126    pub fn witness_ref(&self, module_name: &str) -> String {
127        format!("{module_name}.{}", self.theorem_name)
128    }
129
130    pub fn contains_line(&self, line: usize) -> bool {
131        (self.declaration_start_line..=self.declaration_end_line).contains(&line)
132    }
133
134    pub fn with_line_span(mut self, start_line: usize, end_line: usize) -> Self {
135        self.declaration_start_line = start_line;
136        self.declaration_end_line = end_line.max(start_line);
137        self
138    }
139}
140
141/// Structured Lean export result.
142#[derive(Debug, Clone, PartialEq, Eq)]
143pub struct LeanExport {
144    pub module_name: String,
145    pub source: String,
146    pub prelude: LeanPrelude,
147    pub theorems: Vec<LeanTheorem>,
148}
149
150/// Generated Lean package metadata for writing a runnable project scaffold.
151#[derive(Debug, Clone, PartialEq, Eq)]
152pub struct LeanProject {
153    pub package_name: String,
154    pub toolchain: String,
155    pub requires_mathlib: bool,
156}
157
158impl LeanProject {
159    pub fn new(package_name: impl Into<String>) -> Self {
160        Self {
161            package_name: package_name.into(),
162            toolchain: "leanprover/lean4:stable".into(),
163            requires_mathlib: false,
164        }
165    }
166
167    pub fn for_export(export: &LeanExport) -> Self {
168        let mut project = Self::new(sanitize(&export.module_name).to_lowercase());
169        project.requires_mathlib = export
170            .prelude
171            .imports
172            .iter()
173            .any(|import| import.module == "Mathlib");
174        project
175    }
176
177    pub fn with_toolchain(mut self, toolchain: impl Into<String>) -> Self {
178        self.toolchain = toolchain.into();
179        self
180    }
181
182    pub fn with_mathlib(mut self, requires_mathlib: bool) -> Self {
183        self.requires_mathlib = requires_mathlib;
184        self
185    }
186
187    pub fn render_lakefile(&self) -> String {
188        let mut lines = vec![
189            format!("package {}", render_identifier(&self.package_name)),
190            String::new(),
191        ];
192
193        if self.requires_mathlib {
194            lines.push("require mathlib from git".into());
195            lines.push("  \"https://github.com/leanprover-community/mathlib4.git\"".into());
196            lines.push(String::new());
197        }
198
199        lines.push(format!(
200            "@[default_target]\nlean_lib {}",
201            render_identifier(&self.package_name)
202        ));
203        lines.join("\n")
204    }
205
206    pub fn render_toolchain(&self) -> String {
207        self.toolchain.clone()
208    }
209}
210
211impl LeanExport {
212    pub fn theorem_for_obligation(&self, obligation_name: &str) -> Option<&LeanTheorem> {
213        self.theorems
214            .iter()
215            .find(|theorem| theorem.obligation_name == obligation_name)
216    }
217
218    pub fn theorem_names(&self) -> Vec<String> {
219        self.theorems
220            .iter()
221            .map(|theorem| theorem.theorem_name.clone())
222            .collect()
223    }
224
225    pub fn project(&self) -> LeanProject {
226        LeanProject::for_export(self)
227    }
228}
229
230impl Lean4 {
231    /// Export a list of obligations as a Lean 4 module skeleton.
232    pub fn export_module(module_name: &str, obligations: &[Obligation]) -> String {
233        export_module(module_name, obligations)
234    }
235
236    /// Export a list of obligations as a Lean 4 module skeleton with explicit prelude metadata.
237    pub fn export_module_with_prelude(
238        module_name: &str,
239        obligations: &[Obligation],
240        prelude: LeanPrelude,
241    ) -> String {
242        export_with_prelude(module_name, obligations, prelude).source
243    }
244
245    /// Export a list of obligations as structured Lean metadata plus source.
246    pub fn export(module_name: &str, obligations: &[Obligation]) -> LeanExport {
247        export(module_name, obligations)
248    }
249
250    /// Export a list of obligations as structured Lean metadata plus source with explicit prelude metadata.
251    pub fn export_with_prelude(
252        module_name: &str,
253        obligations: &[Obligation],
254        prelude: LeanPrelude,
255    ) -> LeanExport {
256        export_with_prelude(module_name, obligations, prelude)
257    }
258
259    /// Export a bundle of obligations as a Lean 4 module skeleton.
260    pub fn export_bundle(module_name: &str, bundle: &ObligationBundle) -> String {
261        export_module(module_name, bundle.obligations())
262    }
263
264    /// Export a bundle of obligations as structured Lean metadata plus source.
265    pub fn export_bundle_structured(module_name: &str, bundle: &ObligationBundle) -> LeanExport {
266        export(module_name, bundle.obligations())
267    }
268
269    /// Derive Lean package metadata from a structured export.
270    pub fn project(export: &LeanExport) -> LeanProject {
271        LeanProject::for_export(export)
272    }
273}
274
275pub fn export(module_name: &str, obligations: &[Obligation]) -> LeanExport {
276    export_with_prelude(
277        module_name,
278        obligations,
279        LeanPrelude::for_obligations(obligations),
280    )
281}
282
283pub fn export_with_prelude(
284    module_name: &str,
285    obligations: &[Obligation],
286    prelude: LeanPrelude,
287) -> LeanExport {
288    let mut theorems = Vec::new();
289    let mut lines = Vec::new();
290
291    for import in &prelude.imports {
292        lines.push(format!("import {}", import.module));
293    }
294    if !prelude.imports.is_empty() {
295        lines.push(String::new());
296    }
297
298    lines.push(format!("namespace {}", module_name));
299    lines.push(String::new());
300
301    for alias in &prelude.aliases {
302        lines.push(format!(
303            "abbrev {} := {}",
304            alias.alias,
305            render_identifier(&alias.target)
306        ));
307    }
308    if !prelude.aliases.is_empty() {
309        lines.push(String::new());
310    }
311
312    for obligation in obligations {
313        let theorem = LeanTheorem::from(obligation);
314        let theorem_start_line = lines.len() + 3;
315        let theorem_text = render_theorem(obligation, &theorem, &prelude);
316        let theorem_line_count = theorem_text.lines().count();
317        let theorem_end_line = theorem_start_line + theorem_line_count.saturating_sub(1);
318
319        lines.push(format!("-- property: {}", obligation.property));
320        lines.push(format!("-- origin: {}", obligation.summary()));
321        lines.push(theorem_text);
322        lines.push(String::new());
323
324        theorems.push(theorem.with_line_span(theorem_start_line, theorem_end_line));
325    }
326
327    lines.push(format!("end {}", module_name));
328
329    LeanExport {
330        module_name: module_name.into(),
331        source: lines.join("\n"),
332        prelude,
333        theorems,
334    }
335}
336
337pub fn export_module(module_name: &str, obligations: &[Obligation]) -> String {
338    export(module_name, obligations).source
339}
340
341pub fn export_module_with_prelude(
342    module_name: &str,
343    obligations: &[Obligation],
344    prelude: LeanPrelude,
345) -> String {
346    export_with_prelude(module_name, obligations, prelude).source
347}
348
349fn render_theorem(obligation: &Obligation, theorem: &LeanTheorem, prelude: &LeanPrelude) -> String {
350    let binders = obligation
351        .declarations
352        .iter()
353        .map(|decl| {
354            format!(
355                "({} : {})",
356                render_identifier(&decl.name),
357                render_sort(&decl.sort)
358            )
359        })
360        .collect::<Vec<_>>()
361        .join(" ");
362
363    let assumptions = obligation
364        .assumptions
365        .iter()
366        .enumerate()
367        .map(|(idx, term)| format!("(h{} : {})", idx + 1, render_term(term, prelude)))
368        .collect::<Vec<_>>()
369        .join(" ");
370
371    let mut header = format!("theorem {}", theorem.theorem_name);
372    if !binders.is_empty() {
373        header.push(' ');
374        header.push_str(&binders);
375    }
376    if !assumptions.is_empty() {
377        header.push(' ');
378        header.push_str(&assumptions);
379    }
380    header.push_str(&format!(
381        " : {} := by",
382        render_term(&obligation.conclusion, prelude)
383    ));
384    header.push_str("\n  sorry");
385    header
386}
387
388fn render_sort(sort: &Sort) -> String {
389    match sort {
390        Sort::Bool => "Bool".to_string(),
391        Sort::Int => "Int".to_string(),
392        Sort::Real => "Rat".to_string(),
393        Sort::Named(name) => render_identifier(name),
394    }
395}
396
397fn render_term(term: &Term, prelude: &LeanPrelude) -> String {
398    match term {
399        Term::Var(name) => render_identifier(name),
400        Term::Bool(true) => "True".to_string(),
401        Term::Bool(false) => "False".to_string(),
402        Term::Int(value) => value.to_string(),
403        Term::App { function, args } => {
404            let function = prelude.symbol_name(function);
405            if args.is_empty() {
406                function
407            } else {
408                format!(
409                    "({} {})",
410                    function,
411                    args.iter()
412                        .map(|term| render_term(term, prelude))
413                        .collect::<Vec<_>>()
414                        .join(" ")
415                )
416            }
417        }
418        Term::Eq(left, right) => format!(
419            "{} = {}",
420            render_term(left, prelude),
421            render_term(right, prelude)
422        ),
423        Term::And(terms) => match terms.as_slice() {
424            [] => "True".to_string(),
425            [term] => render_term(term, prelude),
426            _ => terms
427                .iter()
428                .map(|term| render_term(term, prelude))
429                .collect::<Vec<_>>()
430                .join(" ∧ "),
431        },
432        Term::Or(terms) => match terms.as_slice() {
433            [] => "False".to_string(),
434            [term] => render_term(term, prelude),
435            _ => terms
436                .iter()
437                .map(|term| render_term(term, prelude))
438                .collect::<Vec<_>>()
439                .join(" ∨ "),
440        },
441        Term::Not(inner) => format!("¬{}", parenthesize(inner, prelude)),
442        Term::Implies(lhs, rhs) => format!(
443            "{} → {}",
444            parenthesize(lhs, prelude),
445            render_term(rhs, prelude)
446        ),
447    }
448}
449
450fn parenthesize(term: &Term, prelude: &LeanPrelude) -> String {
451    match term {
452        Term::Var(_) | Term::Bool(_) | Term::Int(_) | Term::App { .. } => {
453            render_term(term, prelude)
454        }
455        _ => format!("({})", render_term(term, prelude)),
456    }
457}
458
459fn collect_term_symbols(term: &Term, symbols: &mut BTreeSet<String>) {
460    match term {
461        Term::Var(_) | Term::Bool(_) | Term::Int(_) => {}
462        Term::App { function, args } => {
463            symbols.insert(function.clone());
464            for arg in args {
465                collect_term_symbols(arg, symbols);
466            }
467        }
468        Term::Eq(left, right) | Term::Implies(left, right) => {
469            collect_term_symbols(left, symbols);
470            collect_term_symbols(right, symbols);
471        }
472        Term::And(terms) | Term::Or(terms) => {
473            for term in terms {
474                collect_term_symbols(term, symbols);
475            }
476        }
477        Term::Not(inner) => collect_term_symbols(inner, symbols),
478    }
479}
480
481fn render_identifier(name: &str) -> String {
482    if is_lean_identifier(name) {
483        name.to_string()
484    } else {
485        format!("«{}»", name.replace('»', "_"))
486    }
487}
488
489fn alias_name(name: &str) -> String {
490    let mut alias = String::from("sym_");
491    alias.push_str(&sanitize(name));
492    alias
493}
494
495fn is_lean_identifier(name: &str) -> bool {
496    let mut chars = name.chars();
497    let Some(first) = chars.next() else {
498        return false;
499    };
500
501    if !(first.is_ascii_alphabetic() || first == '_') {
502        return false;
503    }
504
505    chars.all(|c| c.is_ascii_alphanumeric() || c == '_' || c == '\'')
506}
507
508fn sanitize(name: &str) -> String {
509    name.chars()
510        .map(|c| {
511            if c.is_ascii_alphanumeric() || c == '_' {
512                c
513            } else {
514                '_'
515            }
516        })
517        .collect()
518}
519
520impl From<&Obligation> for LeanTheorem {
521    fn from(obligation: &Obligation) -> Self {
522        Self {
523            obligation_name: obligation.name.clone(),
524            theorem_name: sanitize(&obligation.name),
525            property: obligation.property.into(),
526            origin_summary: obligation.summary(),
527            declaration_start_line: 0,
528            declaration_end_line: 0,
529        }
530    }
531}
532
533#[cfg(test)]
534mod tests {
535    use super::*;
536    use crate::obligation::{Origin, VerificationTier};
537    use karpal_proof::IsCommutative;
538
539    #[test]
540    fn exports_theorem_skeleton() {
541        let obligation = Obligation::for_property::<IsCommutative>(
542            "sum/commutative",
543            Origin::new("karpal-algebra", "AbelianGroup for i16"),
544            VerificationTier::External,
545            Term::eq(
546                Term::app("combine", [Term::var("a"), Term::var("b")]),
547                Term::app("combine", [Term::var("b"), Term::var("a")]),
548            ),
549        )
550        .with_decl("a", Sort::Int)
551        .with_decl("b", Sort::Int);
552
553        let text = export_module("KarpalVerify", &[obligation]);
554        assert!(text.contains("namespace KarpalVerify"));
555        assert!(text.contains("theorem sum_commutative"));
556        assert!(text.contains("sorry"));
557    }
558
559    #[test]
560    fn structured_export_tracks_theorem_identity() {
561        let obligation = Obligation::associativity(
562            "sum-assoc",
563            Origin::new("karpal-core", "Semigroup for i32"),
564            Sort::Int,
565            "combine",
566        );
567
568        let export = export("KarpalVerify", &[obligation]);
569        assert_eq!(export.module_name, "KarpalVerify");
570        assert_eq!(export.theorems.len(), 1);
571        assert_eq!(export.theorems[0].theorem_name, "sum_assoc");
572        assert_eq!(
573            export.theorems[0].witness_ref("KarpalVerify"),
574            "KarpalVerify.sum_assoc"
575        );
576        assert!(export.theorems[0].declaration_start_line > 0);
577        assert!(
578            export.theorems[0].declaration_end_line >= export.theorems[0].declaration_start_line
579        );
580        assert!(export.source.contains("theorem sum_assoc"));
581    }
582
583    #[test]
584    fn derived_prelude_aliases_invalid_symbols() {
585        let obligation = Obligation::for_property::<IsCommutative>(
586            "sum/commutative",
587            Origin::new("karpal-algebra", "AbelianGroup for i16"),
588            VerificationTier::External,
589            Term::eq(
590                Term::app("combine-op", [Term::var("a"), Term::var("b")]),
591                Term::app("combine-op", [Term::var("b"), Term::var("a")]),
592            ),
593        )
594        .with_decl("a", Sort::Int)
595        .with_decl("b", Sort::Int);
596
597        let export = export("KarpalVerify", &[obligation]);
598        assert_eq!(export.prelude.aliases.len(), 1);
599        assert_eq!(export.prelude.aliases[0].alias, "sym_combine_op");
600        assert_eq!(export.prelude.aliases[0].target, "combine-op");
601        assert!(
602            export
603                .source
604                .contains("abbrev sym_combine_op := «combine-op»")
605        );
606        assert!(
607            export
608                .source
609                .contains("(sym_combine_op a b) = (sym_combine_op b a)")
610        );
611    }
612
613    #[test]
614    fn explicit_prelude_renders_imports_before_namespace() {
615        let obligation = Obligation::associativity(
616            "sum-assoc",
617            Origin::new("karpal-core", "Semigroup for i32"),
618            Sort::Int,
619            "combine",
620        );
621        let prelude = LeanPrelude::new().with_import("Mathlib");
622
623        let text = export_module_with_prelude("KarpalVerify", &[obligation], prelude);
624        assert!(text.starts_with("import Mathlib\n\nnamespace KarpalVerify"));
625    }
626
627    #[test]
628    fn project_derives_mathlib_requirement_from_prelude() {
629        let obligation = Obligation::associativity(
630            "sum-assoc",
631            Origin::new("karpal-core", "Semigroup for i32"),
632            Sort::Int,
633            "combine",
634        );
635        let export = export_with_prelude(
636            "KarpalVerify",
637            &[obligation],
638            LeanPrelude::new().with_import("Mathlib"),
639        );
640        let project = export.project();
641
642        assert_eq!(project.package_name, "karpalverify");
643        assert!(project.requires_mathlib);
644        assert!(
645            project
646                .render_lakefile()
647                .contains("require mathlib from git")
648        );
649        assert_eq!(project.render_toolchain(), "leanprover/lean4:stable");
650    }
651}
karpal_verify/lean.rs

karpal_verify/
lean.rs
