logicaffeine_proof/
omega_solve.rs

1//! `omega` — linear INTEGER arithmetic, the discreteness-aware layer over the
2//! rational Farkas core.
3//!
4//! Rational Fourier-Motzkin ([`crate::linarith_solve`]) decides satisfiability
5//! over ℚ; it is sound for ℤ but INCOMPLETE, because it cannot use the one fact
6//! that distinguishes the integers: a strict `a < b` is a non-strict `a+1 ≤ b`,
7//! since nothing lives strictly between consecutive integers. The classic
8//! witness is `x < y ∧ y < x+1` — rationally satisfiable (`x=0, y=½`), integer
9//! UNSAT.
10//!
11//! This module supplies exactly that missing step. It rewrites every strict
12//! hypothesis `a < b` to `a+1 ≤ b` through the kernel axiom `lt_succ_le` (a
13//! certified [`InferenceRule::LtSuccLe`] node), then hands the enlarged set of
14//! `≤`-facts to the existing Farkas refutation ([`crate::engine::cert_farkas`]).
15//! The result is one kernel-checked `⊥` derivation, so `omega` is exactly as
16//! trusted as `linarith` — it just sees more contradictions.
17
18use crate::engine::{as_le_pair, cert_farkas, le_eq};
19use crate::{DerivationTree, InferenceRule, ProofExpr, ProofTerm};
20
21/// If `e` is a strict inequality `lt(a, b) = true`, return `(a, b)`.
22fn as_lt_pair(e: &ProofExpr) -> Option<(ProofTerm, ProofTerm)> {
23    if let ProofExpr::Identity(lhs, rhs) = e {
24        if let (ProofTerm::Function(name, args), ProofTerm::Constant(t)) = (lhs, rhs) {
25            if name == "lt" && args.len() == 2 && t == "true" {
26                return Some((args[0].clone(), args[1].clone()));
27            }
28        }
29    }
30    None
31}
32
33/// `a + 1` as a proof term.
34fn succ(a: &ProofTerm) -> ProofTerm {
35    ProofTerm::Function("add".to_string(), vec![a.clone(), ProofTerm::Constant("1".to_string())])
36}
37
38/// If `t` is `add(b, 1)`, return `b` — the shape `lt_add1_le` cancels.
39fn as_succ(t: &ProofTerm) -> Option<ProofTerm> {
40    if let ProofTerm::Function(name, args) = t {
41        if name == "add" && args.len() == 2 && args[1] == ProofTerm::Constant("1".to_string()) {
42            return Some(args[0].clone());
43        }
44    }
45    None
46}
47
48/// Rewrite a known fact to an equivalent (or stronger) `≤`-fact for the Farkas
49/// core. A `≤`-fact passes through. A strict `a < b` becomes `≤` via integer
50/// discreteness: when the bound is already `b′+1` we cancel it to the clean
51/// `a ≤ b′` (`lt_add1_le`), keeping the reconstructed terms small; otherwise it
52/// tightens to `a+1 ≤ b` (`lt_succ_le`). Anything else is dropped.
53fn to_le_fact(prop: &ProofExpr, proof: &DerivationTree) -> Option<(ProofExpr, DerivationTree)> {
54    if as_le_pair(prop).is_some() {
55        return Some((prop.clone(), proof.clone()));
56    }
57    if let Some((a, b)) = as_lt_pair(prop) {
58        if let Some(b_inner) = as_succ(&b) {
59            // a < b′ + 1  ⊢  a ≤ b′
60            let concl = le_eq(a, b_inner);
61            let tree =
62                DerivationTree::new(concl.clone(), InferenceRule::LtAdd1Le, vec![proof.clone()]);
63            return Some((concl, tree));
64        }
65        // a < b  ⊢  a + 1 ≤ b
66        let concl = le_eq(succ(&a), b);
67        let tree = DerivationTree::new(concl.clone(), InferenceRule::LtSuccLe, vec![proof.clone()]);
68        return Some((concl, tree));
69    }
70    None
71}
72
73/// Refute a set of integer hypotheses (`≤` and strict `<`), returning a
74/// kernel-checked `⊥` derivation when they are jointly unsatisfiable over ℤ.
75///
76/// Strictly stronger than [`cert_farkas`]: it first discreteness-tightens every
77/// strict hypothesis, so it catches contradictions the rational core misses.
78/// Returns `None` when the (tightened) system is rationally satisfiable — i.e.
79/// genuinely has an integer model on the fragment covered here.
80pub(crate) fn omega_close(known: &[(ProofExpr, DerivationTree)]) -> Option<DerivationTree> {
81    let le_facts: Vec<(ProofExpr, DerivationTree)> = known
82        .iter()
83        .filter_map(|(p, t)| to_le_fact(p, t))
84        .collect();
85    // Only worth the extra pass if at least one strict fact was tightened;
86    // otherwise the caller's own `cert_farkas` already tried this exact set.
87    let tightened = known.iter().any(|(p, _)| as_lt_pair(p).is_some());
88    if !tightened {
89        return None;
90    }
91    cert_farkas(&le_facts)
92}
93
94/// Does `omega_close` see hypotheses at all — any `≤`/`<` fact? Used by the
95/// tactic to give a precise "not an arithmetic goal" error.
96pub(crate) fn has_arith_facts(known: &[(ProofExpr, DerivationTree)]) -> bool {
97    known
98        .iter()
99        .any(|(p, _)| as_le_pair(p).is_some() || as_lt_pair(p).is_some())
100}
logicaffeine_proof/omega_solve.rs

logicaffeine_proof/
omega_solve.rs
