kdrag.theories.logic.axioms
Axioms that could be in the Kernel, but aren’t needed for everyday functioning of Knuckledragger
Functions
|
Beta conversion for lambda calculus. |
|
Congruence of function symbols. |
|
The purpose of this is to seed the solver with interesting terms. |
|
Prove reflexivity of equality |
|
Prove symmetry of equality |
|
Prove transitivity of equality |
|
Congruence for exists binders |
|
|
|
Congruence for forall binders |
|
|
|
|
|
Project out of an And proof |
|
|
|
Rename bound variables and also attach triggers |
|
Substitute schematic variables in a theorem. |
|
Unfold a definitional equation. |
- kdrag.theories.logic.axioms.beta_conv(lam: QuantifierRef, *args) Proof
Beta conversion for lambda calculus.
- Parameters:
lam (QuantifierRef)
- Return type:
- kdrag.theories.logic.axioms.cong(f: FuncDeclRef, *args: Proof) Proof
Congruence of function symbols. If f is a function symbol, then f(x) == f(y) if x == y.
>>> x = smt.Int("x") >>> y = smt.Real("y") >>> f = smt.Function("f", smt.IntSort(), smt.RealSort(), smt.IntSort()) >>> cong(f, eqrefl(x), eqrefl(y)) |= f(x, y) == f(x, y)
- kdrag.theories.logic.axioms.consider(x: ExprRef) Proof
The purpose of this is to seed the solver with interesting terms. Axiom schema. We may give a fresh name to any constant. An “anonymous” form of define. Pointing out the interesting terms is sometimes the essence of a proof.
- Parameters:
x (ExprRef)
- Return type:
- kdrag.theories.logic.axioms.eqrefl(x: ExprRef) Proof
Prove reflexivity of equality
>>> x = smt.Int("x") >>> eqrefl(x) |= x == x
- Parameters:
x (ExprRef)
- Return type:
- kdrag.theories.logic.axioms.eqsym(eq: Proof) Proof
Prove symmetry of equality
>>> x, y = smt.Ints("x y") >>> eq = kd.axiom(x == y) >>> eqsym(eq) |= y == x
- kdrag.theories.logic.axioms.eqtrans(eq1: Proof, eq2: Proof) Proof
Prove transitivity of equality
>>> x, y, z = smt.Ints("x y z") >>> eq1 = kd.axiom(x == y) >>> eq2 = kd.axiom(y == z) >>> eqtrans(eq1, eq2) |= x == z
- kdrag.theories.logic.axioms.exists_cong(vs: list[ExprRef], pf: Proof) Proof
Congruence for exists binders
>>> x = smt.Bool("x") >>> exists_cong([x], kd.prove(x | x == x)) |= (Exists(x, Or(x, x))) == (Exists(x, x))
- kdrag.theories.logic.axioms.ext(*sorts: SortRef) Proof
>>> ext(smt.IntSort(), smt.IntSort()) |= ForAll([f, g], (f == g) == (ForAll(x0, f[x0] == g[x0]))) >>> ext(smt.IntSort(), smt.RealSort(), smt.IntSort()) |= ForAll([f, g], (f == g) == (ForAll([x0, x1], Select(f, x0, x1) == Select(g, x0, x1))))
- Parameters:
sorts (SortRef)
- Return type:
- kdrag.theories.logic.axioms.forall_cong(vs: list[ExprRef], pf: Proof) Proof
Congruence for forall binders
>>> x = smt.Bool("x") >>> forall_cong([x], kd.prove(x | x == x)) |= (ForAll(x, Or(x, x))) == (ForAll(x, x))
- kdrag.theories.logic.axioms.lambda_cong(vs: list[ExprRef], pf: Proof) Proof
>>> x = smt.Int("x") >>> lambda_cong([x], kd.prove(x + 1 == 1 + x)) |= (Lambda(x, x + 1)) == (Lambda(x, 1 + x))
- kdrag.theories.logic.axioms.neg_ext(*sorts: SortRef) Proof
>>> neg_ext(smt.IntSort(), smt.IntSort()) |= ForAll([f, g], f != g == (Exists(x0, f[x0] != g[x0]))) >>> neg_ext(smt.IntSort(), smt.RealSort(), smt.IntSort()) |= ForAll([f, g], f != g == (Exists([x0, x1], Select(f, x0, x1) != Select(g, x0, x1))))
- Parameters:
sorts (SortRef)
- Return type:
- kdrag.theories.logic.axioms.proj(p: Proof, n: int) Proof
Project out of an And proof
>>> x = smt.Int("x") >>> p = kd.prove(smt.And(x > x - 1, x > x - 2, x > x - 3)) >>> proj(p, 0) |= x > x - 1 >>> proj(p, 2) |= x > x - 3
- kdrag.theories.logic.axioms.rename_vars(t: QuantifierRef, vs: list[ExprRef]) tuple[QuantifierRef, Proof]
>>> x,y = smt.Ints("x y") >>> rename_vars(smt.ForAll([x, y], x + 1 > y), [y,x]) (ForAll([y, x], y + 1 > x), |= (ForAll([x, y], x + 1 > y)) == (ForAll([y, x], y + 1 > x))) >>> rename_vars(smt.Exists([x], x + 1 > y), [y]) Traceback (most recent call last): ... ValueError: ('Cannot rename vars to ones that already occur in term', [y], Exists(x, x + 1 > y))
- Parameters:
t (QuantifierRef)
vs (list[ExprRef])
- Return type:
tuple[QuantifierRef, Proof]
- kdrag.theories.logic.axioms.rename_vars2(pf: Proof, vs: list[ExprRef], patterns=[], no_patterns=[]) Proof
Rename bound variables and also attach triggers
>>> x,y = smt.Ints("x y") >>> f = smt.Function("f", smt.IntSort(), smt.IntSort()) >>> rename_vars2(kd.prove(smt.ForAll([x, y], x + 1 > x)), [y,x], patterns=[x+y]) |= ForAll([y, x], y + 1 > y) >>> rename_vars2(kd.prove(smt.Exists([x], x + 1 > y)), [y]) Traceback (most recent call last): ... ValueError: ('Cannot rename vars to ones that already occur in term', [y], Exists(x, x + 1 > y))
- kdrag.theories.logic.axioms.substitute_fresh_vars(pf: Proof, *subst) Proof
Substitute schematic variables in a theorem. This is is single step instead of generalizing to a Forall and then eliminating it.
>>> x = kd.FreshVar("x", smt.IntSort()) >>> y = kd.FreshVar("y", smt.IntSort()) >>> substitute_fresh_vars(kd.kernel.prove(x == x), (x, smt.IntVal(42)), (y, smt.IntVal(43))) |= 42 == 42
- kdrag.theories.logic.axioms.unfold(e: ExprRef, defn_eqs: Sequence[Proof])
Unfold a definitional equation. The order of variables is off from what kd.define returns.
>>> x = smt.Int("x") >>> y = smt.Real("y") >>> f = smt.Function("test_f", smt.IntSort(), smt.RealSort(), smt.RealSort()) >>> defn = kd.axiom(smt.ForAll([y,x], f(x,y) == (x + 2*y))) >>> unfold(f(7,8), [defn]) |= test_f(7, 8) == ToReal(7) + 2*8
- Parameters:
e (ExprRef)
defn_eqs (Sequence[Proof])