knuckledragger
+Modules
++ | + |
+ | Importing this module will add some syntactic sugar to Z3. |
+
+ | + |
+ | + |
diff --git a/.buildinfo b/.buildinfo new file mode 100644 index 0000000..bcd376d --- /dev/null +++ b/.buildinfo @@ -0,0 +1,4 @@ +# Sphinx build info version 1 +# This file hashes the configuration used when building these files. When it is not found, a full rebuild will be done. +config: 0fc2a8f3ba14656c553ca4e2e4ef7ec2 +tags: 645f666f9bcd5a90fca523b33c5a78b7 diff --git a/.doctrees/_autosummary/knuckledragger.doctree b/.doctrees/_autosummary/knuckledragger.doctree new file mode 100644 index 0000000..fe1fa43 Binary files /dev/null and b/.doctrees/_autosummary/knuckledragger.doctree differ diff --git a/.doctrees/_autosummary/knuckledragger.kernel.axiom.doctree b/.doctrees/_autosummary/knuckledragger.kernel.axiom.doctree new file mode 100644 index 0000000..6b9ed23 Binary files /dev/null and b/.doctrees/_autosummary/knuckledragger.kernel.axiom.doctree differ diff --git a/.doctrees/_autosummary/knuckledragger.kernel.define.doctree b/.doctrees/_autosummary/knuckledragger.kernel.define.doctree new file mode 100644 index 0000000..6252a77 Binary files /dev/null and b/.doctrees/_autosummary/knuckledragger.kernel.define.doctree differ diff --git a/.doctrees/_autosummary/knuckledragger.kernel.doctree b/.doctrees/_autosummary/knuckledragger.kernel.doctree new file mode 100644 index 0000000..8de6c95 Binary files /dev/null and b/.doctrees/_autosummary/knuckledragger.kernel.doctree differ diff --git a/.doctrees/_autosummary/knuckledragger.kernel.is_proof.doctree b/.doctrees/_autosummary/knuckledragger.kernel.is_proof.doctree new file mode 100644 index 0000000..e9c0e53 Binary files /dev/null and b/.doctrees/_autosummary/knuckledragger.kernel.is_proof.doctree differ diff --git a/.doctrees/_autosummary/knuckledragger.kernel.lemma.doctree b/.doctrees/_autosummary/knuckledragger.kernel.lemma.doctree new file mode 100644 index 0000000..97e557e Binary files /dev/null and b/.doctrees/_autosummary/knuckledragger.kernel.lemma.doctree differ diff --git a/.doctrees/_autosummary/knuckledragger.notation.QExists.doctree b/.doctrees/_autosummary/knuckledragger.notation.QExists.doctree new file mode 100644 index 0000000..a83a293 Binary files /dev/null and b/.doctrees/_autosummary/knuckledragger.notation.QExists.doctree differ diff --git a/.doctrees/_autosummary/knuckledragger.notation.QForAll.doctree b/.doctrees/_autosummary/knuckledragger.notation.QForAll.doctree new file mode 100644 index 0000000..6af51af Binary files /dev/null and b/.doctrees/_autosummary/knuckledragger.notation.QForAll.doctree differ diff --git a/.doctrees/_autosummary/knuckledragger.notation.doctree b/.doctrees/_autosummary/knuckledragger.notation.doctree new file mode 100644 index 0000000..473afe0 Binary files /dev/null and b/.doctrees/_autosummary/knuckledragger.notation.doctree differ diff --git a/.doctrees/_autosummary/knuckledragger.notation.lookup_cons_recog.doctree b/.doctrees/_autosummary/knuckledragger.notation.lookup_cons_recog.doctree new file mode 100644 index 0000000..cb7bf8d Binary files /dev/null and b/.doctrees/_autosummary/knuckledragger.notation.lookup_cons_recog.doctree differ diff --git a/.doctrees/_autosummary/knuckledragger.theories.Int.doctree b/.doctrees/_autosummary/knuckledragger.theories.Int.doctree new file mode 100644 index 0000000..2c573e1 Binary files /dev/null and b/.doctrees/_autosummary/knuckledragger.theories.Int.doctree differ diff --git a/.doctrees/_autosummary/knuckledragger.theories.List.doctree b/.doctrees/_autosummary/knuckledragger.theories.List.doctree new file mode 100644 index 0000000..a52f6f9 Binary files /dev/null and b/.doctrees/_autosummary/knuckledragger.theories.List.doctree differ diff --git a/.doctrees/_autosummary/knuckledragger.theories.Nat.doctree b/.doctrees/_autosummary/knuckledragger.theories.Nat.doctree new file mode 100644 index 0000000..b938594 Binary files /dev/null and b/.doctrees/_autosummary/knuckledragger.theories.Nat.doctree differ diff --git a/.doctrees/_autosummary/knuckledragger.theories.Nat.induct.doctree b/.doctrees/_autosummary/knuckledragger.theories.Nat.induct.doctree new file mode 100644 index 0000000..1d16855 Binary files /dev/null and b/.doctrees/_autosummary/knuckledragger.theories.Nat.induct.doctree differ diff --git a/.doctrees/_autosummary/knuckledragger.theories.Real.doctree b/.doctrees/_autosummary/knuckledragger.theories.Real.doctree new file mode 100644 index 0000000..7f5c3a7 Binary files /dev/null and b/.doctrees/_autosummary/knuckledragger.theories.Real.doctree differ diff --git a/.doctrees/_autosummary/knuckledragger.theories.Seq.doctree b/.doctrees/_autosummary/knuckledragger.theories.Seq.doctree new file mode 100644 index 0000000..c2f72a3 Binary files /dev/null and b/.doctrees/_autosummary/knuckledragger.theories.Seq.doctree differ diff --git a/.doctrees/_autosummary/knuckledragger.theories.doctree b/.doctrees/_autosummary/knuckledragger.theories.doctree new file mode 100644 index 0000000..068f676 Binary files /dev/null and b/.doctrees/_autosummary/knuckledragger.theories.doctree differ diff --git a/.doctrees/_autosummary/knuckledragger.utils.doctree b/.doctrees/_autosummary/knuckledragger.utils.doctree new file mode 100644 index 0000000..0f7a33f Binary files /dev/null and b/.doctrees/_autosummary/knuckledragger.utils.doctree differ diff --git a/.doctrees/_autosummary/knuckledragger.utils.expr_to_tptp.doctree b/.doctrees/_autosummary/knuckledragger.utils.expr_to_tptp.doctree new file mode 100644 index 0000000..bd09364 Binary files /dev/null and b/.doctrees/_autosummary/knuckledragger.utils.expr_to_tptp.doctree differ diff --git a/.doctrees/_autosummary/knuckledragger.utils.lemma_db.doctree b/.doctrees/_autosummary/knuckledragger.utils.lemma_db.doctree new file mode 100644 index 0000000..c149eaf Binary files /dev/null and b/.doctrees/_autosummary/knuckledragger.utils.lemma_db.doctree differ diff --git a/.doctrees/_autosummary/knuckledragger.utils.lemma_smt.doctree b/.doctrees/_autosummary/knuckledragger.utils.lemma_smt.doctree new file mode 100644 index 0000000..fd28fb2 Binary files /dev/null and b/.doctrees/_autosummary/knuckledragger.utils.lemma_smt.doctree differ diff --git a/.doctrees/_autosummary/knuckledragger.utils.lemma_tptp.doctree b/.doctrees/_autosummary/knuckledragger.utils.lemma_tptp.doctree new file mode 100644 index 0000000..0879866 Binary files /dev/null and b/.doctrees/_autosummary/knuckledragger.utils.lemma_tptp.doctree differ diff --git a/.doctrees/_autosummary/knuckledragger.utils.open_binder.doctree b/.doctrees/_autosummary/knuckledragger.utils.open_binder.doctree new file mode 100644 index 0000000..c545200 Binary files /dev/null and b/.doctrees/_autosummary/knuckledragger.utils.open_binder.doctree differ diff --git a/.doctrees/_autosummary/knuckledragger.utils.z3_sort_tptp.doctree b/.doctrees/_autosummary/knuckledragger.utils.z3_sort_tptp.doctree new file mode 100644 index 0000000..860a059 Binary files /dev/null and b/.doctrees/_autosummary/knuckledragger.utils.z3_sort_tptp.doctree differ diff --git a/.doctrees/environment.pickle b/.doctrees/environment.pickle new file mode 100644 index 0000000..c5734cd Binary files /dev/null and b/.doctrees/environment.pickle differ diff --git a/.doctrees/index.doctree b/.doctrees/index.doctree new file mode 100644 index 0000000..a25a95f Binary files /dev/null and b/.doctrees/index.doctree differ diff --git a/.nojekyll b/.nojekyll new file mode 100644 index 0000000..e69de29 diff --git a/_autosummary/knuckledragger.html b/_autosummary/knuckledragger.html new file mode 100644 index 0000000..1c9bb70 --- /dev/null +++ b/_autosummary/knuckledragger.html @@ -0,0 +1,133 @@ + + +
+ + + +Assert an axiom.
+Axioms are necessary and useful. But you must use great care.
+thm – The axiom to assert.
by – A python object explaining why the axiom should exist. Often a string explaining the axiom.
Define a non recursive definition. Useful for shorthand and abstraction.
+name – The name of the term to define.
args – The arguments of the term.
defn – The definition of the term.
A tuple of the defined term and the proof of the definition.
+tuple[z3.FuncDeclRef, __Proof]
+Module Attributes
+
|
+defn holds definitional axioms for function symbols. |
+
Functions
+
|
+Assert an axiom. |
+
|
+Define a non recursive definition. |
+
|
++ |
|
+Prove a theorem using a list of previously proved lemmas. |
+
Classes
+
|
++ |
Exceptions
+
|
++ |
import z3
+from dataclasses import dataclass
+from typing import Any
+import logging
+
+logger = logging.getLogger("knuckeldragger")
+
+
+@dataclass(frozen=True)
+class Proof(z3.Z3PPObject):
+ thm: z3.BoolRef
+ reason: list[Any]
+ admit: bool
+
+ def _repr_html_(self):
+ return "⊦" + repr(self.thm)
+
+ def __repr__(self):
+ return "|- " + repr(self.thm)
+
+
+# It is unlikely that users should be accessing the `Proof` constructor directly.
+# This is not ironclad. If you really want the Proof constructor, I can't stop you.
+__Proof = Proof
+Proof = None
+
+
+def is_proof(p):
+ return isinstance(p, __Proof)
+
+
+class LemmaError(Exception):
+ pass
+
+
+def lemma(
+ thm: z3.BoolRef, by: list[Proof] = [], admit=False, timeout=1000, dump=False
+) -> Proof:
+ """Prove a theorem using a list of previously proved lemmas.
+
+ In essence `prove(Implies(by, thm))`.
+
+ :param thm: The theorem to prove.
+ Args:
+ thm (z3.BoolRef): The theorem to prove.
+ by (list[Proof]): A list of previously proved lemmas.
+ admit (bool): If True, admit the theorem without proof.
+
+ Returns:
+ Proof: A proof object of thm
+
+ >>> lemma(BoolVal(True))
+
+ >>> lemma(RealVal(1) >= RealVal(0))
+
+ """
+ if admit:
+ logger.warn("Admitting lemma {}".format(thm))
+ return __Proof(thm, by, True)
+ else:
+ s = z3.Solver()
+ s.set("timeout", timeout)
+ for n, p in enumerate(by):
+ if not isinstance(p, __Proof):
+ raise LemmaError("In by reasons:", p, "is not a Proof object")
+ s.assert_and_track(p.thm, "by_{}".format(n))
+ s.assert_and_track(z3.Not(thm), "knuckledragger_goal")
+ if dump:
+ print(s.sexpr())
+ res = s.check()
+ if res != z3.unsat:
+ if res == z3.sat:
+ raise LemmaError(thm, "Countermodel", s.model())
+ raise LemmaError("lemma", thm, res)
+ else:
+ core = s.unsat_core()
+ assert z3.Bool("knuckledragger_goal") in core
+ if len(core) < len(by) + 1:
+ print("WARNING: Unneeded assumptions. Used", core)
+ return __Proof(thm, by, False)
+
+
+def axiom(thm: z3.BoolRef, by=[]) -> Proof:
+ """Assert an axiom.
+
+ Axioms are necessary and useful. But you must use great care.
+
+ Args:
+ thm: The axiom to assert.
+ by: A python object explaining why the axiom should exist. Often a string explaining the axiom.
+ """
+ return __Proof(thm, by, admit=True)
+
+
+@dataclass(frozen=True)
+class Defn:
+ name: str
+ args: list[z3.ExprRef]
+ body: z3.ExprRef
+ ax: Proof
+
+
+defns: dict[z3.FuncDecl, Defn] = {}
+"""
+defn holds definitional axioms for function symbols.
+"""
+z3.FuncDeclRef.defn = property(lambda self: defns[self].ax)
+
+
+def define(name: str, args: list[z3.ExprRef], body: z3.ExprRef) -> z3.FuncDeclRef:
+ """Define a non recursive definition. Useful for shorthand and abstraction.
+
+ Args:
+ name: The name of the term to define.
+ args: The arguments of the term.
+ defn: The definition of the term.
+
+ Returns:
+ tuple[z3.FuncDeclRef, __Proof]: A tuple of the defined term and the proof of the definition.
+ """
+ sorts = [arg.sort() for arg in args] + [body.sort()]
+ f = z3.Function(name, *sorts)
+ if len(args) > 0:
+ def_ax = axiom(z3.ForAll(args, f(*args) == body), by="definition")
+ else:
+ def_ax = axiom(f(*args) == body, by="definition")
+ # assert f not in __sig or __sig[f].eq( def_ax.thm) # Check for redefinitions. This is kind of painful. Hmm.
+ # Soft warning is more pleasant.
+ defn = Defn(name, args, body, def_ax)
+ if f not in defns or defns[f].ax.thm.eq(def_ax.thm):
+ defns[f] = defn
+ else:
+ print("WARNING: Redefining function", f, "from", defns[f].ax, "to", def_ax.thm)
+ defns[f] = defn
+ return f
+
Prove a theorem using a list of previously proved lemmas.
+In essence prove(Implies(by, thm)).
+thm (z3.BoolRef) – The theorem to prove.
thm – The theorem to prove.
by (list[Proof]) – A list of previously proved lemmas.
admit (bool) – If True, admit the theorem without proof.
A proof object of thm
+Proof
+>>> lemma(BoolVal(True))
+
>>> lemma(RealVal(1) >= RealVal(0))
+
Importing this module will add some syntactic sugar to Z3.
+Expr overload by single dispatch
Bool supports &, |, ~
Sorts supports >> for ArraySort
Datatypes support accessor notation
Functions
+
|
+Quantified Exists |
+
|
+Quantified ForAll |
+
|
+Enable "dot" syntax for fields of z3 datatypes |
+
Classes
+
|
+Sort dispatch is modelled after functools.singledispatch It allows for dispatching on the sort of the first argument |
+
"""Importing this module will add some syntactic sugar to Z3.
+
+- Expr overload by single dispatch
+- Bool supports `&`, `|`, `~`
+- Sorts supports `>>` for ArraySort
+- Datatypes support accessor notation
+"""
+
+import z3
+
+
+z3.BoolRef.__and__ = lambda self, other: z3.And(self, other)
+z3.BoolRef.__or__ = lambda self, other: z3.Or(self, other)
+z3.BoolRef.__invert__ = lambda self: z3.Not(self)
+
+
+def QForAll(vars, hyp, conc):
+ """Quantified ForAll
+
+ Shorthand for `ForAll(vars, Implies(hyp, conc))`
+
+ """
+ return z3.ForAll(vars, z3.Implies(hyp, conc))
+
+
+def QExists(vars, hyp, conc):
+ """Quantified Exists
+
+ Shorthand for `Exists(vars, And(hyp, conc))`
+
+ """
+ return z3.Exists(vars, z3.And(hyp, conc))
+
+
+z3.SortRef.__rshift__ = lambda self, other: z3.ArraySort(self, other)
+
+
+class SortDispatch:
+ """
+ Sort dispatch is modelled after functools.singledispatch
+ It allows for dispatching on the sort of the first argument
+ """
+
+ def __init__(self, default=None):
+ self.methods = {}
+ self.default = default
+
+ def register(self, sort, func):
+ self.methods[sort] = func
+
+ def __call__(self, *args, **kwargs):
+ return self.methods.get(args[0].sort(), self.default)(*args, **kwargs)
+
+
+add = SortDispatch(z3.ArithRef.__add__)
+z3.ExprRef.__add__ = lambda x, y: add(x, y)
+
+sub = SortDispatch(z3.ArithRef.__sub__)
+z3.ExprRef.__sub__ = lambda x, y: sub(x, y)
+
+mul = SortDispatch(z3.ArithRef.__mul__)
+z3.ExprRef.__mul__ = lambda x, y: mul(x, y)
+
+div = SortDispatch(z3.ArithRef.__div__)
+z3.ExprRef.__truediv__ = lambda x, y: div(x, y)
+
+and_ = SortDispatch()
+z3.ExprRef.__and__ = lambda x, y: and_(x, y)
+
+or_ = SortDispatch()
+z3.ExprRef.__or__ = lambda x, y: or_(x, y)
+
+lt = SortDispatch(z3.ArithRef.__lt__)
+z3.ExprRef.__lt__ = lambda x, y: lt(x, y)
+
+le = SortDispatch(z3.ArithRef.__le__)
+z3.ExprRef.__le__ = lambda x, y: le(x, y)
+
+
+"""
+mul = SortDispatch(z3.ArithRef.__mul__)
+z3.ExprRef.__mul__ = mul
+
+sub = SortDispatch(z3.ArithRef.__sub__)
+z3.ExprRef.__sub__ = sub
+
+matmul = SortDispatch()
+z3.ExprRef.__matmul__ = matmul
+
+le = SortDispatch()
+z3.ExprRef.__le__ = le
+"""
+
+
+def lookup_cons_recog(self, k):
+ """
+ Enable "dot" syntax for fields of z3 datatypes
+ """
+ sort = self.sort()
+ recog = "is_" == k[:3] if len(k) > 3 else False
+ for i in range(sort.num_constructors()):
+ cons = sort.constructor(i)
+ if recog:
+ if cons.name() == k[3:]:
+ recog = sort.recognizer(i)
+ return recog(self)
+ else:
+ for j in range(cons.arity()):
+ acc = sort.accessor(i, j)
+ if acc.name() == k:
+ return acc(self)
+
+
+z3.DatatypeRef.__getattr__ = lookup_cons_recog
+
from z3 import IntSort
+from knuckledragger import lemma, axiom
+
+Z = IntSort()
+
+
Defines an algebraic datatype for the Peano natural numbers and useful functions and properties.
+Module Attributes
+
|
+Nat = succ(pred Nat) | zero) |
+
Functions
+
|
+An induction axiom schema for natural numbers. |
+
"""
+Defines an algebraic datatype for the Peano natural numbers and useful functions and properties.
+"""
+
+from z3 import Datatype, ForAll, And, Implies, Consts, If, Function, IntSort, Ints
+from knuckledragger import axiom, lemma, define
+import knuckledragger.notation as notation
+
+Z = IntSort()
+x, y = Ints("x y")
+
+
+Nat = Datatype("Nat")
+"""Nat = succ(pred Nat) | zero)"""
+Nat.declare("zero")
+Nat.declare("succ", ("pred", Nat))
+Nat = Nat.create()
+
+
+n, m, k = Consts("n m k", Nat)
+
+
+def induct(P):
+ """An induction axiom schema for natural numbers."""
+ return axiom(
+ Implies(
+ And(P(Nat.zero), ForAll([n], Implies(P(n), P(Nat.succ(n))))),
+ # -----------------------------------------------------------
+ ForAll([n], P(n)),
+ ),
+ ("nat_induction", P),
+ )
+
+
+reify = Function("reify", Nat, Z)
+# """reify Nat Z maps a natural number to the built in Z3 integers"""
+reify_def = axiom(
+ ForAll([n], reify(n) == If(Nat.is_zero(n), 0, reify(Nat.pred(n)) + 1))
+)
+
+
+reflect = Function("reflect", Z, Nat)
+# """reflect Z Nat maps an integer to a natural number"""
+# reflect_def = axiom(
+# ForAll([x], reflect(x) == If(x <= 0, Nat.zero, Nat.succ(reflect(x - 1))))
+# )
+reflect = define("reflect", [x], If(x <= 0, Nat.zero, Nat.succ(reflect(x - 1))))
+
+reflect_reify = lemma(
+ ForAll([n], reflect(reify(n)) == n),
+ by=[reflect.defn, reify_def, induct(lambda n: reflect(reify(n)) == n)],
+)
+
+reify_ge_0 = lemma(
+ ForAll([n], reify(n) >= 0), by=[reify_def, induct(lambda n: reify(n) >= 0)]
+)
+
+zero_homo = lemma(reify(Nat.zero) == 0, by=[reify_def])
+
+succ_homo = lemma(
+ ForAll([n], reify(Nat.succ(n)) == 1 + reify(n)),
+ by=[reify_def, induct(lambda n: reify(Nat.succ(n)) == 1 + reify(n))],
+)
+
+
+add = Function("add", Nat, Nat, Nat)
+add_def = axiom(
+ ForAll([n, m], add(n, m) == If(Nat.is_zero(n), m, Nat.succ(add(Nat.pred(n), m))))
+)
+notation.add.register(Nat, add)
+
+
+add_0_n = lemma(ForAll([n], Nat.zero + n == n), by=[add_def])
+
import z3
+from z3 import ForAll, Function
+from knuckledragger import lemma, axiom
+import knuckledragger as kd
+
+R = z3.RealSort()
+RFun = z3.ArraySort(R, R)
+RSeq = z3.ArraySort(z3.IntSort(), R)
+
+x, y, z = z3.Reals("x y z")
+
+plus = Function("plus", R, R, R)
+plus_def = axiom(ForAll([x, y], plus(x, y) == x + y), "definition")
+
+plus_0 = lemma(ForAll([x], plus(x, 0) == x), by=[plus_def])
+plus_comm = lemma(ForAll([x, y], plus(x, y) == plus(y, x)), by=[plus_def])
+plus_assoc = lemma(
+ z3.ForAll([x, y, z], plus(x, plus(y, z)) == plus(plus(x, y), z)), by=[plus_def]
+)
+
+mul = Function("mul", R, R, R)
+mul_def = axiom(ForAll([x, y], mul(x, y) == x * y), "definition")
+
+mul_zero = lemma(ForAll([x], mul(x, 0) == 0), by=[mul_def])
+mul_1 = lemma(ForAll([x], mul(x, 1) == x), by=[mul_def])
+mul_comm = lemma(ForAll([x, y], mul(x, y) == mul(y, x)), by=[mul_def])
+mul_assoc = lemma(
+ ForAll([x, y, z], mul(x, mul(y, z)) == mul(mul(x, y), z)), by=[mul_def]
+)
+mul_distrib = lemma(
+ ForAll([x, y, z], mul(x, plus(y, z)) == plus(mul(x, y), mul(x, z))),
+ by=[mul_def, plus_def],
+)
+
+
+abs = kd.define("abs", [x], z3.If(x >= 0, x, -x))
+
+abs_idem = kd.lemma(ForAll([x], abs(abs(x)) == abs(x)), by=[abs.defn])
+abd_neg = kd.lemma(ForAll([x], abs(-x) == abs(x)), by=[abs.defn])
+abs_ge_0 = kd.lemma(ForAll([x], abs(x) >= 0), by=[abs.defn])
+
+nonneg = kd.define("nonneg", [x], abs(x) == x)
+nonneg_ge_0 = kd.lemma(ForAll([x], nonneg(x) == (x >= 0)), by=[nonneg.defn, abs.defn])
+
+max = kd.define("max", [x, y], z3.If(x >= y, x, y))
+max_comm = kd.lemma(ForAll([x, y], max(x, y) == max(y, x)), by=[max.defn])
+max_assoc = kd.lemma(
+ ForAll([x, y, z], max(x, max(y, z)) == max(max(x, y), z)), by=[max.defn]
+)
+max_idem = kd.lemma(ForAll([x], max(x, x) == x), by=[max.defn])
+max_ge = kd.lemma(ForAll([x, y], max(x, y) >= x), by=[max.defn])
+max_ge_2 = kd.lemma(ForAll([x, y], max(x, y) >= y), by=[max.defn])
+
from knuckledragger.theories.Nat import Nat
+from knuckledragger.theories.Real import R
+from z3 import ArraySort
+
+"""A Sequence type of Nat -> R"""
+Seq = ArraySort(Nat, R)
+
Functions
+
|
++ |
|
+Scan all modules for Proof objects and return a dictionary of them. |
+
|
+Replacement for lemma that returns smtlib string for experimentation with other solvers |
+
|
+Returns tptp strings |
+
|
++ |
|
++ |
Classes
+
|
+calc is for equational reasoning. |
+
from knuckledragger.kernel import lemma, is_proof
+import z3
+import subprocess
+import sys
+
+
+class Calc:
+ """
+ calc is for equational reasoning.
+ One can write a sequence of formulas interspersed with useful lemmas.
+ """
+
+ def __init__(self, vars, lhs):
+ # TODO: hyps=None for conditional rewriting. assumpt, assume=[]
+ self.vars = vars
+ self.terms = [lhs]
+ self.lemmas = []
+
+ def ForAll(self, body):
+ if len(self.vars) == 0:
+ return body
+ else:
+ return z3.ForAll(self.vars, body)
+
+ def eq(self, rhs, by=[]):
+ self.lemmas.append(lemma(self.ForAll(self.terms[-1] == rhs), by=by))
+ self.terms.append(rhs)
+ return self
+
+ # TODO: lt, le, gt, ge chaining. Or custom op.
+
+ def __repr__(self):
+ return "... = " + repr(self.terms[-1])
+
+ def qed(self):
+ return lemma(self.ForAll(self.terms[0] == self.terms[-1]), by=self.lemmas)
+
+
+def lemma_smt(thm: z3.BoolRef, by=[], sig=[]) -> list[str]:
+ """
+ Replacement for lemma that returns smtlib string for experimentation with other solvers
+ """
+ output = []
+ output.append(";;declarations")
+ for f in sig:
+ if isinstance(f, z3.FuncDeclRef):
+ output.append(f.sexpr())
+ elif isinstance(f, z3.SortRef):
+ output.append("(declare-sort " + f.sexpr() + " 0)")
+ elif isinstance(f, z3.ExprRef):
+ output.append(f.decl().sexpr())
+ output.append(";;axioms")
+ for e in by:
+ if is_proof(e):
+ output.append("(assert " + e.thm.sexpr() + ")")
+ output.append(";;goal")
+ output.append("(assert " + z3.Not(thm).sexpr() + ")")
+ output.append("(check-sat)")
+ return output
+
+
+def open_binder(l: z3.QuantifierRef):
+ vars = [
+ z3.Const(l.var_name(i).upper(), l.var_sort(i))
+ for i in reversed(range(l.num_vars()))
+ ]
+ return vars, z3.substitute_vars(l.body(), *vars)
+
+
+def expr_to_tptp(expr: z3.ExprRef):
+ if isinstance(expr, z3.IntNumRef):
+ return str(expr.as_string())
+ elif isinstance(expr, z3.QuantifierRef):
+ vars, body = open_binder(expr)
+ body = expr_to_tptp(body)
+ vs = ", ".join([v.sexpr() + ":" + z3_sort_tptp(v.sort()) for v in vars])
+ if expr.is_forall():
+ return f"(![{vs}] : {body})"
+ elif expr.is_exists():
+ return f"(?[{vs}] : {body})"
+ elif expr.is_lambda():
+ return f"(^[{vs}] : {body})"
+ children = list(map(expr_to_tptp, expr.children()))
+ head = expr.decl().name()
+ if head == "true":
+ return "$true"
+ elif head == "false":
+ return "$false"
+ elif head == "and":
+ return "({})".format(" & ".join(children))
+ elif head == "or":
+ return "({})".format(" | ".join(children))
+ elif head == "=":
+ return "({} = {})".format(children[0], children[1])
+ elif head == "=>":
+ return "({} => {})".format(children[0], children[1])
+ elif head == "not":
+ return "~({})".format(children[0])
+ elif head == "ite":
+ return "$ite({}, {}, {})".format(*children)
+ elif head == "<":
+ return "$less({},{})".format(*children)
+ elif head == "<=":
+ return "$lesseq({},{})".format(*children)
+ elif head == ">":
+ return "$greater({},{})".format(*children)
+ elif head == ">=":
+ return "$greatereq({},{})".format(*children)
+ elif head == "+":
+ return "$sum({},{})".format(*children)
+ elif head == "-":
+ return "$difference({},{})".format(*children)
+ elif head == "*":
+ return "$product({},{})".format(*children)
+ elif head == "/":
+ return "$quotient({},{})".format(*children)
+ else:
+ if len(children) == 0:
+ return head
+ return f"{head}({', '.join(children)})"
+
+
+z3.ExprRef.tptp = expr_to_tptp
+
+
+def z3_sort_tptp(sort: z3.SortRef):
+ match sort.name():
+ case "Int":
+ return "$int"
+ case "Bool":
+ return "$o"
+ case "Real":
+ return "$real"
+ case "Array":
+ return "({} > {})".format(
+ z3_sort_tptp(sort.domain()), z3_sort_tptp(sort.range())
+ )
+ case x:
+ return x.lower()
+
+
+z3.SortRef.tptp = z3_sort_tptp
+
+
+def lemma_tptp(thm: z3.BoolRef, by=[], sig=[], timeout=None, command=None):
+ """
+ Returns tptp strings
+ """
+ output = []
+ for f in sig:
+ if isinstance(f, z3.FuncDeclRef):
+ dom = " * ".join([f.domain(i).tptp() for i in range(f.arity())])
+ output.append(f"tff(sig, type, {f.name()} : ({dom}) > {f.range().tptp()}).")
+ elif isinstance(f, z3.SortRef):
+ output.append(f"tff(sig, type, {f.tptp()} : $tType).")
+ elif isinstance(f, z3.ExprRef):
+ output.append(f"tff(sig, type, {f.sexpr()} : {f.sort().tptp()}).")
+ for e in by:
+ if is_proof(e):
+ output.append(f"tff(hyp, axiom, {e.thm.tptp()} ).")
+ output.append(f"tff(goal,conjecture,{thm.tptp()} ).")
+ if command == None:
+ return output
+ else:
+ with open("/tmp/temp.p", "w") as f:
+ f.writelines(output)
+ command.append("/tmp/temp.p")
+ res = subprocess.run(
+ command,
+ timeout=timeout,
+ capture_output=True,
+ )
+ return res
+
+
+def lemma_db():
+ """Scan all modules for Proof objects and return a dictionary of them."""
+ db = {}
+ for modname, mod in sys.modules.items():
+ thms = {name: thm for name, thm in mod.__dict__.items() if is_proof(thm)}
+ if len(thms) > 0:
+ db[modname] = thms
+ return db
+
' + + '' + + _("Hide Search Matches") + + "
" + ) + ); + }, + + /** + * helper function to hide the search marks again + */ + hideSearchWords: () => { + document + .querySelectorAll("#searchbox .highlight-link") + .forEach((el) => el.remove()); + document + .querySelectorAll("span.highlighted") + .forEach((el) => el.classList.remove("highlighted")); + localStorage.removeItem("sphinx_highlight_terms") + }, + + initEscapeListener: () => { + // only install a listener if it is really needed + if (!DOCUMENTATION_OPTIONS.ENABLE_SEARCH_SHORTCUTS) return; + + document.addEventListener("keydown", (event) => { + // bail for input elements + if (BLACKLISTED_KEY_CONTROL_ELEMENTS.has(document.activeElement.tagName)) return; + // bail with special keys + if (event.shiftKey || event.altKey || event.ctrlKey || event.metaKey) return; + if (DOCUMENTATION_OPTIONS.ENABLE_SEARCH_SHORTCUTS && (event.key === "Escape")) { + SphinxHighlight.hideSearchWords(); + event.preventDefault(); + } + }); + }, +}; + +_ready(() => { + /* Do not call highlightSearchWords() when we are on the search page. + * It will highlight words from the *previous* search query. + */ + if (typeof Search === "undefined") SphinxHighlight.highlightSearchWords(); + SphinxHighlight.initEscapeListener(); +}); diff --git a/genindex.html b/genindex.html new file mode 100644 index 0000000..b272aac --- /dev/null +++ b/genindex.html @@ -0,0 +1,307 @@ + + + + + ++ |
+ |
+ |
+ | + |
+ | + |
+ | + |
|
+
+ |
+ | + |
+ |
Knuckledragger is an attempt at creating a down to earth, highly automated interactive proof assistant in python. It is not attempting to be the most interesting, expressive, or flexible logic in the world. The goal is to support applications like software verification, calculus, equational reasoning, and numerical bounds. A no-install colab tutorial is available here
+python3 -m pip install git+https://github.com/philzook58/knuckledragger.git
+
Or to install locally
+git clone https://github.com/philzook58/knuckledragger.git
+cd knuckledragger
+python3 -m pip install -e .
+
It is not desirable or within my capabilities to build a giant universe in which to live. The goal is to take a subtle blade and bolt together things that already exist.
+Using widespread and commonly supported languages gives a huge leg up in terms of tooling and audience. Python is the modern lingua franca of computing. It has a first class interactive experience and extensive bindings to projects in other languages.
+Core functionality comes from Z3. The Z3 python api is a de facto standard. The term and formula data structures of knuckledragger are literally Z3 python terms and formula. To some degree, knuckledragger is a metalayer to guide Z3 through proofs it could perhaps do on its own, but it would get lost.
+A hope is to be able to use easy access to Jupyter, copilot, ML ecosystems, sympy, cvxpy, numpy, scipy, Julia, Prolog, Maude, calcium, flint, Mathematica, and sage will make metaprogramming in this system very powerful. I maintain the option to just trust these results but hopefully they can be translated into arguments the kernel can understand.
+The core logic is more or less multi-sorted first order logic aka SMT-LIB2.
+Big features that ATPs do not often support are induction, definitions, and other axiom schema. Knuckledragger supports these.
+Other theorem provers of interest: cvc5, Vampire, eprover, Twee, egglog, nanoCoP.
+The de Bruijn criterion is going to be bent or broken in certain senses. Attention is paid to what is kernel and what is not. Proof objects are basically trees recording chains of lemmas discharged by Automated Theorem Prover (ATP) calls. Soundness will be attempted, accidental misuse will be made difficult but not impossible.
+Isabelle and ACL2 are the strongest influences. If you want dependent type theory, you are at a level of investment and sophistication that is behooves you to be in another system. Should there be a strong automated DTT solver someday, I will reconsider.
+I maintain the right to change my mind about anything.
++ | + |
+ k | ||
+ |
+ knuckledragger | + |
+ |
+ knuckledragger.kernel | + |
+ |
+ knuckledragger.notation | + |
+ |
+ knuckledragger.theories | + |
+ |
+ knuckledragger.theories.Int | + |
+ |
+ knuckledragger.theories.List | + |
+ |
+ knuckledragger.theories.Nat | + |
+ |
+ knuckledragger.theories.Real | + |
+ |
+ knuckledragger.theories.Seq | + |
+ |
+ knuckledragger.utils | + |