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, Clone)]
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    /// Optional names for the premises, parallel to `premises`. A `Given (h): …`
30    /// names that premise `h`, so a `Proof:` script can refer to it as `cases h`
31    /// rather than the positional `hp0`. `None` for an unnamed `Given:`.
32    pub premise_names: Vec<Option<String>>,
33
34    /// The goal to prove (Prove statement)
35    pub goal: &'a LogicExpr<'a>,
36
37    /// The proof strategy to use
38    pub strategy: ProofStrategy,
39}
40
41/// Proof strategies for theorem verification.
42#[derive(Debug, Clone, PartialEq)]
43pub enum ProofStrategy {
44    /// Automatic proof search using backward chaining.
45    /// The prover will try all available inference rules.
46    Auto,
47
48    /// Induction on a variable (for inductive types like Nat, List).
49    /// Example: `Proof: Induction on n.`
50    Induction(String),
51
52    /// Direct application of a specific rule.
53    /// Example: `Proof: ModusPonens.`
54    ByRule(String),
55
56    /// An explicit tactic-script proof, written in the English-esque vernacular and
57    /// run by the tactic framework. Example:
58    /// `Proof: Assume h. By cases on h, right, by assumption. Left, by assumption.`
59    Script(String),
60}
61
62impl Default for ProofStrategy {
63    fn default() -> Self {
64        ProofStrategy::Auto
65    }
66}
logicaffeine_language/ast/theorem.rs

logicaffeine_language/ast/
theorem.rs
