logicaffeine_proof/

lib.rs

#![cfg_attr(docsrs, feature(doc_cfg))]
#![doc = include_str!("../README.md")]

// Number-theory / cryptanalysis substrate — factoring, elliptic/isogeny, lattice, order-finding.
// These are prover tools (the hardness lens behind isogeny/ait/oracle), not runtime crypto; they
// depend only on `logicaffeine_base::numeric`.
pub mod cyclotomic;
pub mod elliptic;
pub mod factor;
pub mod fp2;
pub mod hyperelliptic;
pub mod lattice;
pub mod period;

pub mod arith;
pub mod cdcl;
pub mod cnf;
pub mod dimacs;
pub mod proof;
pub mod proof_emit;
pub mod complexity;
pub mod ait;
pub mod isogeny;
pub mod coalgebra;
pub mod groupoid;
pub mod category_collapse;
pub mod two_group;
pub mod proof_rewrite;
pub mod trace_determinism;
pub mod progress_complex;
pub mod cubical;
pub mod kan_complex;
pub mod two_type;
pub mod eilenberg_maclane;
pub mod postnikov;
pub mod steenrod;
pub mod pr;
pub mod affine;
pub mod affine_gfp;
pub mod families;
pub mod gf2;
pub mod hypercube;
pub mod census;
pub mod cofactor;
pub mod res_width;
pub mod rup;
pub mod sat;
pub mod satcli;
pub mod solve;
pub mod xor_drat;
pub mod xor_engine;
pub mod bmc;
pub mod cardinality;
pub mod counting_principle;
pub mod matching;
pub mod ordering;
pub mod parity_cardinality;
pub mod pigeonhole;
pub mod pseudo_boolean;
pub mod symmetry;
pub mod symmetry_detect;
pub mod sym_certify;
pub mod sym_dynamic;
pub mod lyapunov;
pub mod inprocess;
pub mod sdcl;
pub mod xorsat;
pub mod lll;
pub mod modp;
pub mod modm;
pub mod orbit_stability;
pub mod polycalc;
pub mod polycalc_gfp;
pub mod polycalc_zm;
pub mod sos;
pub mod permgroup;
pub mod sym_break;
pub mod hornsat;
pub mod twosat;
pub mod interval_sched;
pub mod register_alloc;
pub mod optimize;
pub mod certifier;
pub mod counterexample;
pub mod crush;
pub mod decide;
pub mod development;
pub mod discrimination;
pub mod lemma_index;
pub mod engine;
pub mod simp;
pub mod formula;
pub mod tactic;
pub mod tactic_script;
pub mod rule_search;
pub mod linarith_solve;
pub mod omega_solve;
pub mod grounding;
pub mod grid_solver;
pub mod error;
pub mod hints;
pub mod unify;
pub mod verify;

#[cfg(feature = "verification")]
pub mod oracle;
#[cfg(feature = "verification")]
mod modal_translation;

pub use engine::BackwardChainer;
pub use error::ProofError;
pub use hints::{suggest_hint, SocraticHint, SuggestedTactic};
pub use unify::Substitution;

use std::fmt;

// =============================================================================
// PROOF TERM - Owned representation of logical terms
// =============================================================================

/// Owned term representation for proof manipulation.
///
/// Decoupled from arena-allocated `Term<'a>` to allow proof trees to persist
/// beyond the lifetime of the parsing arena.
///
/// # See Also
///
/// * [`ProofExpr`] - Expression-level representation containing `ProofTerm`s
/// * [`unify::unify_terms`] - Unification algorithm for terms
/// * [`unify::Substitution`] - Maps variables to terms
/// * [`certifier::certify`] - Converts proof trees to kernel terms
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
pub enum ProofTerm {
    /// A constant symbol (e.g., "Socrates", "42")
    Constant(String),

    /// A variable symbol (e.g., "x", "y")
    Variable(String),

    /// A function application (e.g., "father(x)", "add(1, 2)")
    Function(String, Vec<ProofTerm>),

    /// A group/tuple of terms (e.g., "(x, y)")
    Group(Vec<ProofTerm>),

    /// Reference to a bound variable in a pattern context.
    /// Distinct from Variable (unification var) and Constant (global name).
    /// Prevents variable capture bugs during alpha-conversion.
    BoundVarRef(String),
}

impl fmt::Display for ProofTerm {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            ProofTerm::Constant(s) => write!(f, "{}", s),
            ProofTerm::Variable(s) => write!(f, "{}", s),
            ProofTerm::Function(name, args) => {
                write!(f, "{}(", name)?;
                for (i, arg) in args.iter().enumerate() {
                    if i > 0 {
                        write!(f, ", ")?;
                    }
                    write!(f, "{}", arg)?;
                }
                write!(f, ")")
            }
            ProofTerm::Group(terms) => {
                write!(f, "(")?;
                for (i, t) in terms.iter().enumerate() {
                    if i > 0 {
                        write!(f, ", ")?;
                    }
                    write!(f, "{}", t)?;
                }
                write!(f, ")")
            }
            ProofTerm::BoundVarRef(s) => write!(f, "#{}", s),
        }
    }
}

// =============================================================================
// PROOF EXPRESSION - Owned representation of logical expressions
// =============================================================================

/// Owned expression representation for proof manipulation.
///
/// Supports all `LogicExpr` variants to enable full language coverage.
/// This is the "proposition" side of the Curry-Howard correspondence.
///
/// # See Also
///
/// * [`ProofTerm`] - Terms embedded within expressions (predicate arguments)
/// * [`unify::unify_exprs`] - Expression-level unification with alpha-equivalence
/// * [`unify::beta_reduce`] - Normalizes lambda applications
/// * [`certifier::certify`] - Converts expressions to kernel types
/// * [`DerivationTree`] - Proof trees conclude with a `ProofExpr`
#[derive(Debug, Clone, PartialEq)]
pub enum ProofExpr {
    // --- Core FOL ---

    /// Atomic predicate: P(t1, t2, ...)
    Predicate {
        name: String,
        args: Vec<ProofTerm>,
        world: Option<String>,
    },

    /// Identity: t1 = t2
    Identity(ProofTerm, ProofTerm),

    /// Propositional atom
    Atom(String),

    // --- Logical Connectives ---

    /// Conjunction: P ∧ Q
    And(Box<ProofExpr>, Box<ProofExpr>),

    /// Disjunction: P ∨ Q
    Or(Box<ProofExpr>, Box<ProofExpr>),

    /// Implication: P → Q
    Implies(Box<ProofExpr>, Box<ProofExpr>),

    /// Biconditional: P ↔ Q
    Iff(Box<ProofExpr>, Box<ProofExpr>),

    /// Negation: ¬P
    Not(Box<ProofExpr>),

    // --- Quantifiers ---

    /// Universal quantification: ∀x P(x)
    ForAll {
        variable: String,
        body: Box<ProofExpr>,
    },

    /// Existential quantification: ∃x P(x)
    Exists {
        variable: String,
        body: Box<ProofExpr>,
    },

    // --- Modal Logic ---

    /// Modal operator: □P or ◇P (with world semantics)
    Modal {
        domain: String,
        force: f32,
        flavor: String,
        body: Box<ProofExpr>,
    },

    /// Counterfactual conditional: P □→ Q. Quantifies the consequent over the
    /// closest antecedent-worlds (a similarity ordering), so it is strictly
    /// distinct from material implication in both directions.
    Counterfactual {
        antecedent: Box<ProofExpr>,
        consequent: Box<ProofExpr>,
    },

    // --- Temporal Logic ---

    /// Temporal operator: Past(P), Future(P), Always(P), Eventually(P), Next(P)
    Temporal {
        operator: String,
        body: Box<ProofExpr>,
    },

    /// Binary temporal operator: Until(P,Q), Release(P,Q), WeakUntil(P,Q)
    TemporalBinary {
        operator: String,
        left: Box<ProofExpr>,
        right: Box<ProofExpr>,
    },

    // --- Lambda Calculus (CIC extension) ---

    /// Lambda abstraction: λx.P
    Lambda {
        variable: String,
        body: Box<ProofExpr>,
    },

    /// Function application: (f x)
    App(Box<ProofExpr>, Box<ProofExpr>),

    // --- Event Semantics ---

    /// Neo-Davidsonian event: ∃e(Verb(e) ∧ Agent(e,x) ∧ ...)
    NeoEvent {
        event_var: String,
        verb: String,
        roles: Vec<(String, ProofTerm)>,
    },

    // --- Peano / Inductive Types (CIC Extension) ---

    /// Data Constructor: Zero, Succ(n), Cons(h, t), etc.
    /// The building blocks of inductive types.
    Ctor {
        name: String,
        args: Vec<ProofExpr>,
    },

    /// Pattern Matching: match n { Zero => A, Succ(k) => B }
    /// Eliminates inductive types by case analysis.
    Match {
        scrutinee: Box<ProofExpr>,
        arms: Vec<MatchArm>,
    },

    /// Recursive Function (Fixpoint): fix f. λn. ...
    /// Defines recursive functions over inductive types.
    Fixpoint {
        name: String,
        body: Box<ProofExpr>,
    },

    /// Typed Variable: n : Nat
    /// Signals to the prover that induction may be applicable.
    TypedVar {
        name: String,
        typename: String,
    },

    // --- Higher-Order Pattern Unification ---

    /// Meta-variable (unification hole) to be solved during proof search.
    /// Represents an unknown expression, typically a function or predicate.
    /// Example: Hole("P") in ?P(x) = Body, to be solved as P = λx.Body
    Hole(String),

    /// Embedded term (lifts ProofTerm into ProofExpr context).
    /// Used when a term appears where an expression is expected.
    /// Example: App(Hole("P"), Term(BoundVarRef("x")))
    Term(ProofTerm),

    // --- Fallback ---

    /// Unsupported construct (with description for debugging)
    Unsupported(String),
}

// =============================================================================
// MATCH ARM - A single case in pattern matching
// =============================================================================

/// A single arm in a match expression.
/// Example: Succ(k) => Add(k, m)
#[derive(Debug, Clone, PartialEq)]
pub struct MatchArm {
    /// The constructor being matched: "Zero", "Succ", "Cons", etc.
    pub ctor: String,

    /// Variable bindings for constructor arguments: ["k"] for Succ(k)
    pub bindings: Vec<String>,

    /// The expression to evaluate when this arm matches
    pub body: ProofExpr,
}

impl fmt::Display for ProofExpr {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            ProofExpr::Predicate { name, args, world } => {
                write!(f, "{}", name)?;
                if !args.is_empty() {
                    write!(f, "(")?;
                    for (i, arg) in args.iter().enumerate() {
                        if i > 0 {
                            write!(f, ", ")?;
                        }
                        write!(f, "{}", arg)?;
                    }
                    write!(f, ")")?;
                }
                if let Some(w) = world {
                    write!(f, " @{}", w)?;
                }
                Ok(())
            }
            ProofExpr::Identity(left, right) => write!(f, "{} = {}", left, right),
            ProofExpr::Atom(s) => write!(f, "{}", s),
            ProofExpr::And(left, right) => write!(f, "({} ∧ {})", left, right),
            ProofExpr::Or(left, right) => write!(f, "({} ∨ {})", left, right),
            ProofExpr::Implies(left, right) => write!(f, "({} → {})", left, right),
            ProofExpr::Iff(left, right) => write!(f, "({} ↔ {})", left, right),
            ProofExpr::Not(inner) => write!(f, "¬{}", inner),
            ProofExpr::ForAll { variable, body } => write!(f, "∀{} {}", variable, body),
            ProofExpr::Exists { variable, body } => write!(f, "∃{} {}", variable, body),
            ProofExpr::Modal { domain, force, flavor, body } => {
                write!(f, "□[{}/{}/{}]{}", domain, force, flavor, body)
            }
            ProofExpr::Counterfactual { antecedent, consequent } => {
                write!(f, "({} □→ {})", antecedent, consequent)
            }
            ProofExpr::Temporal { operator, body } => write!(f, "{}({})", operator, body),
            ProofExpr::TemporalBinary { operator, left, right } => {
                write!(f, "TemporalBinary({}, {}, {})", operator, left, right)
            }
            ProofExpr::Lambda { variable, body } => write!(f, "λ{}.{}", variable, body),
            ProofExpr::App(func, arg) => write!(f, "({} {})", func, arg),
            ProofExpr::NeoEvent { event_var, verb, roles } => {
                write!(f, "∃{}({}({})", event_var, verb, event_var)?;
                for (role, term) in roles {
                    write!(f, " ∧ {}({}, {})", role, event_var, term)?;
                }
                write!(f, ")")
            }
            ProofExpr::Ctor { name, args } => {
                write!(f, "{}", name)?;
                if !args.is_empty() {
                    write!(f, "(")?;
                    for (i, arg) in args.iter().enumerate() {
                        if i > 0 {
                            write!(f, ", ")?;
                        }
                        write!(f, "{}", arg)?;
                    }
                    write!(f, ")")?;
                }
                Ok(())
            }
            ProofExpr::Match { scrutinee, arms } => {
                write!(f, "match {} {{ ", scrutinee)?;
                for (i, arm) in arms.iter().enumerate() {
                    if i > 0 {
                        write!(f, ", ")?;
                    }
                    write!(f, "{}", arm.ctor)?;
                    if !arm.bindings.is_empty() {
                        write!(f, "({})", arm.bindings.join(", "))?;
                    }
                    write!(f, " => {}", arm.body)?;
                }
                write!(f, " }}")
            }
            ProofExpr::Fixpoint { name, body } => write!(f, "fix {}.{}", name, body),
            ProofExpr::TypedVar { name, typename } => write!(f, "{}:{}", name, typename),
            ProofExpr::Unsupported(desc) => write!(f, "⟨unsupported: {}⟩", desc),
            ProofExpr::Hole(name) => write!(f, "?{}", name),
            ProofExpr::Term(term) => write!(f, "{}", term),
        }
    }
}

// =============================================================================
// INFERENCE RULE - The logical moves available to the prover
// =============================================================================

/// The "Lever" - The specific logical move made at each proof step.
///
/// This enum captures HOW we moved from premises to conclusion. Each variant
/// corresponds to a different proof strategy or logical rule.
///
/// # See Also
///
/// * [`DerivationTree`] - Each node contains an `InferenceRule`
/// * [`certifier::certify`] - Maps inference rules to kernel terms
/// * [`hints::suggest_hint`] - Suggests applicable rules when stuck
/// * [`BackwardChainer`] - The engine that selects and applies rules
///
/// One constructor's case in a generic induction scheme
/// ([`InferenceRule::InductionScheme`]). The derivation's premises align 1:1 with
/// the cases, in the inductive's constructor-registration order.
#[derive(Debug, Clone, PartialEq)]
pub struct InductionCase {
    /// The constructor this case eliminates (e.g. `"Succ"`, `"Node"`).
    pub constructor: String,
    /// The constructor's arguments, in order — each bound in the case body.
    pub args: Vec<InductionArg>,
}

/// One argument of a constructor in an [`InductionCase`].
#[derive(Debug, Clone, PartialEq)]
pub struct InductionArg {
    /// The name bound for this argument in the case body.
    pub name: String,
    /// Whether this argument is itself of the inductive type — a recursive
    /// position, which therefore carries an induction hypothesis.
    pub recursive: bool,
}

#[derive(Debug, Clone, PartialEq)]
pub enum InferenceRule {
    // --- Basic FOL ---

    /// Direct match with a known fact in the Context/KnowledgeBase.
    /// Logic: Γ, P ⊢ P
    PremiseMatch,

    /// Logic: P → Q, P ⊢ Q
    ModusPonens,

    /// Logic: ¬Q, P → Q ⊢ ¬P
    ModusTollens,

    /// Logic: P, Q ⊢ P ∧ Q
    ConjunctionIntro,

    /// Logic: P ∧ Q ⊢ P (or Q)
    ConjunctionElim,

    /// Logic: P ⊢ P ∨ Q
    DisjunctionIntro,

    /// Logic: P ∨ Q, P → R, Q → R ⊢ R
    DisjunctionElim,

    /// Logic: ⊥ ⊢ anything (ex falso quodlibet). The single premise concludes `False`.
    ExFalso,

    /// Logic: assume P, derive Q ⊢ P → Q (implication introduction / →I). The
    /// single premise proves Q with P bound as a local hypothesis.
    ImpliesIntro,

    /// Logic: prove P → Q and Q → P ⊢ P ↔ Q (biconditional introduction / ↔I).
    BicondIntro,

    /// Logic: ¬¬P ⊢ P (and P ⊢ ¬¬P)
    DoubleNegation,

    /// Logic: classical reductio (proof by contradiction) — assume ¬G, derive ⊥ ⊢ G,
    /// discharged through the `dne` axiom. The single premise concludes `False` with
    /// ¬G bound as a local hypothesis.
    ClassicalReductio,

    // --- Quantifiers ---

    /// Logic: ∀x P(x) ⊢ P(c)
    /// Stores the specific term 'c' used to instantiate the universal.
    UniversalInst(String),

    /// Logic: ∀x P(x) ⊢ P(t) at an arbitrary witness TERM (a compound like
    /// `add(a, Zero)`, not just a name). `UniversalInst` keeps the name-only
    /// fast path; this carries the full term for instantiations that
    /// `simp`/`crush` produce by matching.
    UniversalInstTerm(ProofTerm),

    /// Logic: Γ, x:T ⊢ P(x) implies Γ ⊢ ∀x:T. P(x)
    /// Stores variable name and type name for Lambda construction.
    UniversalIntro { variable: String, var_type: String },

    /// Logic: P(w) ⊢ ∃x.P(x)
    /// Carries the witness and its type for kernel certification.
    ExistentialIntro {
        witness: String,
        witness_type: String,
    },

    // --- Modal Logic (World Moves) ---

    /// Logic: □P (in w0), Accessible(w0, w1) ⊢ P (in w1)
    /// "Necessity Elimination" / "Distribution"
    ModalAccess,

    /// Logic: If P is true in ALL accessible worlds ⊢ □P
    /// "Necessity Introduction"
    ModalGeneralization,

    // --- Temporal Logic ---

    /// Logic: t1 < t2, t2 < t3 ⊢ t1 < t3
    TemporalTransitivity,

    /// Logic: P(s₀), ∀s(P(s) → P(next(s))) ⊢ G(P)
    /// Standard k-induction for hardware safety properties.
    TemporalInduction,

    /// Logic: G(P) ⊢ P ∧ X(G(P))
    /// Fixpoint unfolding of Always.
    TemporalUnfolding,

    /// Logic: P(w) ⊢ F(P) for witness world w
    /// Prove Eventually by exhibiting a reachable witness.
    EventualityProgress,

    /// Logic: Induction on trace length for P U Q
    UntilInduction,

    // --- Peano / Inductive Reasoning (CIC seed) ---

    /// Logic: P(0), ∀k(P(k) → P(S(k))) ⊢ ∀n P(n)
    /// Stores the variable name, its inductive type, and the step variable used.
    StructuralInduction {
        variable: String,  // "n" - the induction variable
        ind_type: String,  // "Nat" - the inductive type
        step_var: String,  // "k" - the predecessor variable (for IH matching)
    },

    /// Logic: generic structural induction over ANY inductive type. Generalizes
    /// [`InferenceRule::StructuralInduction`] (fixed to the nullary-base + unary-step
    /// Nat shape) to an arbitrary constructor set — one premise per constructor, in
    /// registration order, each recursive argument carrying its own induction
    /// hypothesis. Certifies to a `Fix` over an N-ary `Match`: the dependent
    /// eliminator the kernel re-checks for coverage, case types, and termination.
    InductionScheme {
        variable: String,          // the induction variable, e.g. "t"
        ind_type: String,          // the inductive type, e.g. "Tree"
        cases: Vec<InductionCase>, // one per constructor, in registration order
    },

    // --- Linear arithmetic (order) ---

    /// `a ≤ b`, `b ≤ c` ⊢ `a ≤ c` over `Int`. The middle term is recovered from
    /// the first premise's conclusion. Certifies to `le_trans a b c p₀ p₁`.
    /// Inequalities are encoded as the Prop `Eq Bool (le a b) true`.
    LeTrans,

    /// `⊢ a ≤ a` over `Int`. Certifies to `le_refl a`.
    LeRefl,

    /// `a ≤ b`, `c ≤ d` ⊢ `a + c ≤ b + d` over `Int`. The four operands are read
    /// from the conclusion `le(add a c, add b d) = true`; `premise[0]` proves
    /// `a ≤ b`, `premise[1]` proves `c ≤ d`. Certifies to `le_add_mono a b c d p₀ p₁`.
    LeAddMono,

    /// Linear contradiction: `premise[0]` proves `le(m, n) = true` for ground `m > n`
    /// (so `le m n ⇝ false`, the Prop is `Eq Bool false true`). Concludes `⊥` via the
    /// `Bool` no-confusion discriminator. Lets contradictory bounds prove anything.
    LinFalse,

    /// `0 ≤ k`, `a ≤ b` ⊢ `k·a ≤ k·b` — scale an inequality by a non-negative `k`.
    /// Operands from the conclusion `le(mul k a, mul k b) = true`; `premise[0]` proves
    /// `0 ≤ k`, `premise[1]` proves `a ≤ b`. Certifies to `le_mul_nonneg k a b p₀ p₁`.
    /// A Farkas-reconstruction primitive.
    LeMulNonneg,

    /// `a ≤ b` ⊢ `0 ≤ b - a` — move an inequality to one side. Operands from the
    /// conclusion `le(0, sub b a) = true`; `premise[0]` proves `a ≤ b`. Certifies to
    /// `le_sub a b p₀`. The Farkas "collect to a single side" primitive.
    LeSub,

    /// `a < b` ⊢ `(a + 1) ≤ b` — integer DISCRETENESS. Operands from the conclusion
    /// `le(add a 1, b) = true`; `premise[0]` proves `a < b` (`lt(a,b) = true`).
    /// Certifies to `lt_succ_le a b p₀`. This is the one step rational Fourier-Motzkin
    /// lacks — the `omega` primitive that refutes strict systems the rational solver
    /// reports satisfiable.
    LtSuccLe,

    /// `a < (b + 1)` ⊢ `a ≤ b` — the upper-side discreteness companion. Operands
    /// from the conclusion `le(a, b) = true`; `premise[0]` proves `a < b+1`
    /// (`lt(a, add b 1) = true`). Certifies to `lt_add1_le a b p₀`. Preferred over
    /// `LtSuccLe` when the strict bound is already `b+1`, since it cancels the
    /// constant instead of propagating it into the Farkas reconstruction.
    LtAdd1Le,

    // --- Equality ---

    /// Leibniz's Law / Substitution of Equals
    /// Logic: a = b, P(a) ⊢ P(b)
    /// The equality proof is in `premise\[0\]`, the P(a) proof is in `premise\[1\]`.
    /// Carries the original term and replacement term for certification.
    Rewrite {
        from: ProofTerm,
        to: ProofTerm,
    },

    /// Symmetry of Equality: a = b ⊢ b = a
    EqualitySymmetry,

    /// Transitivity of Equality: a = b, b = c ⊢ a = c
    EqualityTransitivity,

    /// Reflexivity of Equality: a = a (after normalization)
    /// Used when both sides of an identity reduce to the same normal form.
    Reflexivity,

    /// Arithmetic decision: an `Int` equality discharged by the proof-producing
    /// arithmetic oracle ([`crate::arith::prove_int_eq`]) into a kernel-checked
    /// proof (computation + the ring axioms). The conclusion is the `Identity`.
    ArithDecision,

    /// Proof by kernel evaluation: a closed decidable proposition (a ground
    /// comparison or Bool/Nat equality) discharged via `native_decide`. The
    /// leaf carries only the claim; certification re-runs the evaluator and
    /// the kernel checks the resulting `of_decide_eq_true`/`ofReduceBool`
    /// term, so a lying leaf is rejected.
    NativeDecide,

    // --- Fallbacks ---

    /// "The User Said So." Used for top-level axioms.
    Axiom,

    /// "The Machine Said So." (Z3 Oracle)
    /// The string contains the solver's justification.
    OracleVerification(String),

    /// Proof by Contradiction (Reductio ad Absurdum)
    /// Logic: Assume ¬C, derive P ∧ ¬P (contradiction), conclude C
    /// Or: Assume P, derive Q ∧ ¬Q, conclude ¬P
    ReductioAdAbsurdum,

    /// Contradiction detected in premises: P and ¬P both hold
    /// Logic: P, ¬P ⊢ ⊥ (ex falso quodlibet)
    Contradiction,

    // --- Quantifier Elimination ---

    /// Existential Elimination (Skolemization in a proof context)
    /// Logic: ∃x.P(x), [c fresh] P(c) ⊢ Goal implies ∃x.P(x) ⊢ Goal
    /// The witness c must be fresh (not appearing in Goal).
    ExistentialElim { witness: String },

    /// Case Analysis on a formula `C` whose two cases both reach absurdity.
    /// Logic: (C → ⊥), (¬C → ⊥) ⊢ ⊥ — note this is the *intuitionistic* form
    /// (build `¬C` and `¬¬C`, then apply), so certifying it needs no excluded
    /// middle. Used for self-referential paradoxes like the Barber Paradox.
    ///
    /// `case_formula` carries the actual proposition `C` (not a rendered string)
    /// so the certifier can build the case lambdas' parameter types and bind `C`
    /// / `¬C` as local hypotheses in each branch.
    CaseAnalysis { case_formula: Box<ProofExpr> },

    /// Logic: `A ∨ B`, `A ⊢ C`, `B ⊢ C` ⊢ `C` — disjunction elimination to a common
    /// conclusion (here always `⊥`, for the grounded-grid contradiction prover).
    /// Premises: `[A∨B, left-branch (C assuming A), right-branch (C assuming B)]`.
    /// Unlike `DisjunctionElim` (disjunctive syllogism, which needs a refuted
    /// disjunct) this eliminates BOTH disjuncts by case analysis — the move a grid's
    /// of-pair / either-or / closure clause needs. The disjuncts (and, when a disjunct
    /// is a conjunction, each of its conjuncts) are bound as local hypotheses in the
    /// respective branch, so a branch may reference them directly.
    DisjunctionCases,
}

// =============================================================================
// DERIVATION TREE - The recursive proof structure
// =============================================================================

/// The "Euclidean Structure" - A recursive tree representing the proof.
///
/// This is the object returned by the Prover. It allows the UI to render
/// a step-by-step explanation (Natural Language Generation).
///
/// # Structure
///
/// Each node contains:
/// - `conclusion`: The proposition proved at this step
/// - `rule`: The logical rule applied (how we know the conclusion)
/// - `premises`: Sub-proofs justifying the rule's requirements
/// - `substitution`: Variable bindings from unification
///
/// # See Also
///
/// * [`BackwardChainer::prove`] - Creates derivation trees
/// * [`InferenceRule`] - The rules that justify each step
/// * [`ProofExpr`] - The conclusion type
/// * [`certifier::certify`] - Converts trees to kernel terms
/// * [`hints::suggest_hint`] - Suggests next steps when stuck
#[derive(Debug, Clone)]
pub struct DerivationTree {
    /// The logical statement proved at this node.
    pub conclusion: ProofExpr,

    /// The rule applied to justify this conclusion.
    pub rule: InferenceRule,

    /// The sub-proofs that validate the requirements of the rule.
    /// Example: ModusPonens will have 2 children (The Implication, The Antecedent).
    pub premises: Vec<DerivationTree>,

    /// The depth of the tree (used for complexity limits).
    pub depth: usize,

    /// Substitution applied at this step (for unification-based rules).
    pub substitution: unify::Substitution,
}

impl DerivationTree {
    /// Constructs a new Proof Node.
    /// Automatically calculates depth based on children.
    pub fn new(
        conclusion: ProofExpr,
        rule: InferenceRule,
        premises: Vec<DerivationTree>,
    ) -> Self {
        let max_depth = premises.iter().map(|p| p.depth).max().unwrap_or(0);
        Self {
            conclusion,
            rule,
            premises,
            depth: max_depth + 1,
            substitution: unify::Substitution::new(),
        }
    }

    /// A leaf node (usually a Premise, Axiom, or Oracle result).
    pub fn leaf(conclusion: ProofExpr, rule: InferenceRule) -> Self {
        Self::new(conclusion, rule, vec![])
    }

    /// Set the substitution for this derivation step.
    pub fn with_substitution(mut self, subst: unify::Substitution) -> Self {
        self.substitution = subst;
        self
    }

    /// Renders the proof as a text-based tree (for debugging/CLI).
    pub fn display_tree(&self) -> String {
        self.display_recursive(0)
    }

    fn display_recursive(&self, indent: usize) -> String {
        let prefix = "  ".repeat(indent);

        let rule_name = match &self.rule {
            InferenceRule::UniversalInst(var) => format!("UniversalInst({})", var),
            InferenceRule::UniversalInstTerm(term) => format!("UniversalInst({})", term),
            InferenceRule::UniversalIntro { variable, var_type } => {
                format!("UniversalIntro({}:{})", variable, var_type)
            }
            InferenceRule::ExistentialIntro { witness, witness_type } => {
                format!("∃Intro({}:{})", witness, witness_type)
            }
            InferenceRule::StructuralInduction { variable, ind_type, step_var } => {
                format!("Induction({}:{}, step={})", variable, ind_type, step_var)
            }
            InferenceRule::OracleVerification(s) => format!("Oracle({})", s),
            InferenceRule::Rewrite { from, to } => format!("Rewrite({} → {})", from, to),
            InferenceRule::EqualitySymmetry => "EqSymmetry".to_string(),
            InferenceRule::EqualityTransitivity => "EqTransitivity".to_string(),
            r => format!("{:?}", r),
        };

        let mut output = format!("{}└─ [{}] {}\n", prefix, rule_name, self.conclusion);

        for premise in &self.premises {
            output.push_str(&premise.display_recursive(indent + 1));
        }
        output
    }
}

impl fmt::Display for DerivationTree {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        write!(f, "{}", self.display_tree())
    }
}

// =============================================================================
// PROOF GOAL - The target state for backward chaining
// =============================================================================

/// The Goal State for the Backward Chainer.
///
/// Represents a "hole" in the proof that needs to be filled. During backward
/// chaining, goals are decomposed into subgoals until they match known facts.
///
/// # Fields
///
/// * `target` - What we are trying to prove
/// * `context` - Local assumptions (e.g., antecedents of implications we've entered)
///
/// # See Also
///
/// * [`BackwardChainer::prove`] - Takes a goal and produces a derivation tree
/// * [`DerivationTree`] - The result of successfully proving a goal
/// * [`ProofExpr`] - The target type
#[derive(Debug, Clone)]
pub struct ProofGoal {
    /// What we are trying to prove right now.
    pub target: ProofExpr,

    /// The local assumptions available (e.g., inside an implication).
    pub context: Vec<ProofExpr>,
}

impl ProofGoal {
    pub fn new(target: ProofExpr) -> Self {
        Self {
            target,
            context: Vec::new(),
        }
    }

    pub fn with_context(target: ProofExpr, context: Vec<ProofExpr>) -> Self {
        Self { target, context }
    }
}