karpal_verify/
lean.rs

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

karpal_verify/
lean.rs
