karpal_verify/
lean.rs

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

karpal_verify/
lean.rs
