pub enum InferenceRule {
Show 46 variants
PremiseMatch,
ModusPonens,
ModusTollens,
ConjunctionIntro,
ConjunctionElim,
DisjunctionIntro,
DisjunctionElim,
ExFalso,
ImpliesIntro,
BicondIntro,
DoubleNegation,
ClassicalReductio,
UniversalInst(String),
UniversalInstTerm(ProofTerm),
UniversalIntro {
variable: String,
var_type: String,
},
ExistentialIntro {
witness: String,
witness_type: String,
},
ModalAccess,
ModalGeneralization,
TemporalTransitivity,
TemporalInduction,
TemporalUnfolding,
EventualityProgress,
UntilInduction,
StructuralInduction {
variable: String,
ind_type: String,
step_var: String,
},
InductionScheme {
variable: String,
ind_type: String,
cases: Vec<InductionCase>,
},
LeTrans,
LeRefl,
LeAddMono,
LinFalse,
LeMulNonneg,
LeSub,
LtSuccLe,
LtAdd1Le,
Rewrite {
from: ProofTerm,
to: ProofTerm,
},
EqualitySymmetry,
EqualityTransitivity,
Reflexivity,
ArithDecision,
NativeDecide,
Axiom,
OracleVerification(String),
ReductioAdAbsurdum,
Contradiction,
ExistentialElim {
witness: String,
},
CaseAnalysis {
case_formula: Box<ProofExpr>,
},
DisjunctionCases,
}Variants§
PremiseMatch
Direct match with a known fact in the Context/KnowledgeBase. Logic: Γ, P ⊢ P
ModusPonens
Logic: P → Q, P ⊢ Q
ModusTollens
Logic: ¬Q, P → Q ⊢ ¬P
ConjunctionIntro
Logic: P, Q ⊢ P ∧ Q
ConjunctionElim
Logic: P ∧ Q ⊢ P (or Q)
DisjunctionIntro
Logic: P ⊢ P ∨ Q
DisjunctionElim
Logic: P ∨ Q, P → R, Q → R ⊢ R
ExFalso
Logic: ⊥ ⊢ anything (ex falso quodlibet). The single premise concludes False.
ImpliesIntro
Logic: assume P, derive Q ⊢ P → Q (implication introduction / →I). The single premise proves Q with P bound as a local hypothesis.
BicondIntro
Logic: prove P → Q and Q → P ⊢ P ↔ Q (biconditional introduction / ↔I).
DoubleNegation
Logic: ¬¬P ⊢ P (and P ⊢ ¬¬P)
ClassicalReductio
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.
UniversalInst(String)
Logic: ∀x P(x) ⊢ P(c) Stores the specific term ‘c’ used to instantiate the universal.
UniversalInstTerm(ProofTerm)
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.
UniversalIntro
Logic: Γ, x:T ⊢ P(x) implies Γ ⊢ ∀x:T. P(x) Stores variable name and type name for Lambda construction.
ExistentialIntro
Logic: P(w) ⊢ ∃x.P(x) Carries the witness and its type for kernel certification.
ModalAccess
Logic: □P (in w0), Accessible(w0, w1) ⊢ P (in w1) “Necessity Elimination” / “Distribution”
ModalGeneralization
Logic: If P is true in ALL accessible worlds ⊢ □P “Necessity Introduction”
TemporalTransitivity
Logic: t1 < t2, t2 < t3 ⊢ t1 < t3
TemporalInduction
Logic: P(s₀), ∀s(P(s) → P(next(s))) ⊢ G(P) Standard k-induction for hardware safety properties.
TemporalUnfolding
Logic: G(P) ⊢ P ∧ X(G(P)) Fixpoint unfolding of Always.
EventualityProgress
Logic: P(w) ⊢ F(P) for witness world w Prove Eventually by exhibiting a reachable witness.
UntilInduction
Logic: Induction on trace length for P U Q
StructuralInduction
Logic: P(0), ∀k(P(k) → P(S(k))) ⊢ ∀n P(n) Stores the variable name, its inductive type, and the step variable used.
InductionScheme
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.
LeTrans
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.
LeRefl
⊢ a ≤ a over Int. Certifies to le_refl a.
LeAddMono
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₁.
LinFalse
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.
LeMulNonneg
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.
LeSub
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.
LtSuccLe
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.
LtAdd1Le
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.
Rewrite
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.
EqualitySymmetry
Symmetry of Equality: a = b ⊢ b = a
EqualityTransitivity
Transitivity of Equality: a = b, b = c ⊢ a = c
Reflexivity
Reflexivity of Equality: a = a (after normalization) Used when both sides of an identity reduce to the same normal form.
ArithDecision
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.
NativeDecide
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.
Axiom
“The User Said So.” Used for top-level axioms.
OracleVerification(String)
“The Machine Said So.” (Z3 Oracle) The string contains the solver’s justification.
ReductioAdAbsurdum
Proof by Contradiction (Reductio ad Absurdum) Logic: Assume ¬C, derive P ∧ ¬P (contradiction), conclude C Or: Assume P, derive Q ∧ ¬Q, conclude ¬P
Contradiction
Contradiction detected in premises: P and ¬P both hold Logic: P, ¬P ⊢ ⊥ (ex falso quodlibet)
ExistentialElim
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).
CaseAnalysis
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.
DisjunctionCases
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.
Trait Implementations§
Source§impl Clone for InferenceRule
impl Clone for InferenceRule
Source§fn clone(&self) -> InferenceRule
fn clone(&self) -> InferenceRule
1.0.0 (const: unstable) · Source§fn clone_from(&mut self, source: &Self)
fn clone_from(&mut self, source: &Self)
source. Read more