logicaffeine_language/ast/
theorem.rs

1//! Theorem and proof block AST types.
2//!
3//! This module defines the AST for theorem blocks in the vernacular proof language:
4//!
5//! ```text
6//! ## Theorem: Socrates_Mortality
7//! Given: All men are mortal.
8//! Given: Socrates is a man.
9//! Prove: Socrates is mortal.
10//! Proof: Auto.
11//! ```
12//!
13//! # Key Types
14//!
15//! - **[`TheoremBlock`]**: Contains premises, goal, and proof strategy
16//! - **[`ProofStrategy`]**: How to prove (Auto, Manual, By lemmas)
17
18use super::logic::LogicExpr;
19
20/// A theorem block containing premises, goal, and proof strategy.
21#[derive(Debug)]
22pub struct TheoremBlock<'a> {
23    /// The name of the theorem (e.g., "Socrates_Mortality")
24    pub name: String,
25
26    /// Premises (Given statements) - logical expressions to assume true
27    pub premises: Vec<&'a LogicExpr<'a>>,
28
29    /// The goal to prove (Prove statement)
30    pub goal: &'a LogicExpr<'a>,
31
32    /// The proof strategy to use
33    pub strategy: ProofStrategy,
34}
35
36/// Proof strategies for theorem verification.
37#[derive(Debug, Clone, PartialEq)]
38pub enum ProofStrategy {
39    /// Automatic proof search using backward chaining.
40    /// The prover will try all available inference rules.
41    Auto,
42
43    /// Induction on a variable (for inductive types like Nat, List).
44    /// Example: `Proof: Induction on n.`
45    Induction(String),
46
47    /// Direct application of a specific rule.
48    /// Example: `Proof: ModusPonens.`
49    ByRule(String),
50}
51
52impl Default for ProofStrategy {
53    fn default() -> Self {
54        ProofStrategy::Auto
55    }
56}
logicaffeine_language/ast/theorem.rs

logicaffeine_language/ast/
theorem.rs
