logicaffeine_proof/
decide.rs

1//! `decide` — proof by evaluation for closed decidable goals.
2//!
3//! The router below is untrusted: it evaluates the goal with machine
4//! arithmetic and, only when the goal is TRUE, builds the derivation whose
5//! leaves re-derive that truth through certified channels — `ArithDecision`
6//! (the proof-producing arithmetic oracle) for ground `Int` identities,
7//! `NativeDecide` (the kernel's trusted-evaluator route via the `reduceBool`
8//! hook and a `Decidable` instance) for ground comparisons and Bool
9//! equalities. Propositional structure recurses through the ordinary intro
10//! rules. A false, open, or unsupported goal yields `None` — decide declines,
11//! it never guesses.
12
13use crate::{DerivationTree, InferenceRule, ProofExpr, ProofTerm};
14
15/// Evaluate a ground integer term: numeric constants and `add`/`sub`/`mul`/
16/// `div`/`mod` trees over them. Checked arithmetic — overflow declines.
17fn eval_int(t: &ProofTerm) -> Option<i64> {
18    match t {
19        ProofTerm::Constant(s) => s.parse::<i64>().ok(),
20        ProofTerm::Function(op, args) if args.len() == 2 => {
21            let a = eval_int(&args[0])?;
22            let b = eval_int(&args[1])?;
23            match op.as_str() {
24                "add" => a.checked_add(b),
25                "sub" => a.checked_sub(b),
26                "mul" => a.checked_mul(b),
27                "div" => a.checked_div(b),
28                "mod" => a.checked_rem(b),
29                _ => None,
30            }
31        }
32        _ => None,
33    }
34}
35
36fn ground_bool(t: &ProofTerm) -> Option<bool> {
37    match t {
38        ProofTerm::Constant(s) if s == "true" => Some(true),
39        ProofTerm::Constant(s) if s == "false" => Some(false),
40        _ => None,
41    }
42}
43
44/// Evaluate a ground comparison term `le(a, b)`/`lt`/`ge`/`gt` to its truth.
45fn eval_comparison(t: &ProofTerm) -> Option<bool> {
46    let ProofTerm::Function(name, args) = t else { return None };
47    if args.len() != 2 {
48        return None;
49    }
50    let a = eval_int(&args[0])?;
51    let b = eval_int(&args[1])?;
52    match name.as_str() {
53        "le" => Some(a <= b),
54        "lt" => Some(a < b),
55        "ge" => Some(a >= b),
56        "gt" => Some(a > b),
57        _ => None,
58    }
59}
60
61/// Decide a closed goal: `Some(tree)` iff the goal evaluates TRUE, where the
62/// tree's leaves certify through `ArithDecision`/`NativeDecide` and its
63/// structure through the intro rules.
64pub(crate) fn decide_expr(goal: &ProofExpr) -> Option<DerivationTree> {
65    match goal {
66        ProofExpr::Identity(l, r) => {
67            // Ground comparison in the canonical encoding `le(a, b) = true`
68            // (or `= false`): the kernel evaluator re-derives it.
69            if let (Some(truth), Some(claimed)) = (eval_comparison(l), ground_bool(r)) {
70                return (truth == claimed)
71                    .then(|| DerivationTree::leaf(goal.clone(), InferenceRule::NativeDecide));
72            }
73            // Ground Int identity: the arithmetic oracle re-derives it.
74            if let (Some(a), Some(b)) = (eval_int(l), eval_int(r)) {
75                return (a == b)
76                    .then(|| DerivationTree::leaf(goal.clone(), InferenceRule::ArithDecision));
77            }
78            // Ground Bool identity: the kernel evaluator re-derives it.
79            if let (Some(a), Some(b)) = (ground_bool(l), ground_bool(r)) {
80                return (a == b)
81                    .then(|| DerivationTree::leaf(goal.clone(), InferenceRule::NativeDecide));
82            }
83            None
84        }
85        ProofExpr::And(l, r) => {
86            let lt = decide_expr(l)?;
87            let rt = decide_expr(r)?;
88            Some(DerivationTree::new(
89                goal.clone(),
90                InferenceRule::ConjunctionIntro,
91                vec![lt, rt],
92            ))
93        }
94        ProofExpr::Or(l, r) => {
95            let side = decide_expr(l).or_else(|| decide_expr(r))?;
96            Some(DerivationTree::new(
97                goal.clone(),
98                InferenceRule::DisjunctionIntro,
99                vec![side],
100            ))
101        }
102        // An implication holds by weakening whenever its consequent decides
103        // true. (A false antecedent is NOT decided here: proving ¬A needs a
104        // refutation channel — `of_decide_eq_false` — a documented follow-up.)
105        ProofExpr::Implies(_, r) => {
106            let rt = decide_expr(r)?;
107            Some(DerivationTree::new(
108                goal.clone(),
109                InferenceRule::ImpliesIntro,
110                vec![rt],
111            ))
112        }
113        _ => None,
114    }
115}
logicaffeine_proof/decide.rs

logicaffeine_proof/
decide.rs
