moved inductive into kernel

README.md

@@ -156,20 +156,20 @@ For more on interactive theorem proving (This is a lot to take in)
 - [Knuckledragger Update: ATP for Python Interactive Theorem Proving](https://www.philipzucker.com/knuckledrag2/)
 - [Knuckledragger: Experimenting with a Python Proof Assistant](https://www.philipzucker.com/python-itp/)
 
-## Knuckledragger isn't Python
+## Comparison to Other Systems
 
-The design is based around the chaining of calls to z3. Python is a useful platform, but the core of the design can be ported to many languages.
-
-- [SBV](https://hackage.haskell.org/package/sbv-11.0/docs/Data-SBV-Tools-KnuckleDragger.html) - Haskell
-- Yours here!
+- [Z3](https://github.com/Z3Prover/z3): Superset of the capabilities of Z3 since it is built on top of it. Enables rigorous chaining of Z3 calls. Better facilities for higher order and quantifier reasoning.
+- [sympy](https://www.sympy.org/) and sage: More manual manipulation is to be expected, but also more logically sound. Everything is integrated in a cohesive fabric of first order logic.
+- Lean and Coq: No dependent types, larger trusted code base, a higher baseline of automation.
+- [Isabelle](https://isabelle.in.tum.de/) and [HOLpy](https://gitee.com/bhzhan/holpy): Similar in many respects. Lack of parametric types. Weaker higher order reasoning. Knuckledragger is a library, not a framework. Heavy reuse of already existing python things whenever possible (Jupyter, z3py, sympy, python idioms). Seamlessly integrated with z3py.
 
 ## Design
 
 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](https://github.com/Z3Prover/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 smt through proofs it could perhaps do on its own, but it would get lost.
+Core functionality comes from [Z3](https://github.com/Z3Prover/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 smt 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](https://jupyter.org/), [copilot](https://copilot.microsoft.com/), ML ecosystems, [sympy](https://www.sympy.org/), [cvxpy](https://www.cvxpy.org/), [numpy](https://numpy.org/), [scipy](https://scipy.org/), [egglog](https://egglog-python.readthedocs.io/latest/), [Julia](https://github.com/JuliaPy/PythonCall.jl), [Prolog](https://www.swi-prolog.org/pldoc/man?section=janus-call-prolog), [Maude](https://fadoss.github.io/maude-bindings/), [calcium](https://fredrikj.net/calcium/), [flint](https://fredrikj.net/python-flint/), [Mathematica](https://reference.wolfram.com/language/WolframClientForPython/), and [sage](https://www.sagemath.org/) 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.
 
@@ -194,6 +194,10 @@ TODO: A no-install WIP colab tutorial is available [here](http://colab.research.
     1. Knuckledragger does enable you to model your algorithms and extract/interpret them to python.
     2. A subset of purely-function, strongly-typed python can be reflected directly into the Knuckledragger logic.
     3. Domain specific modelling of important python ecosystem libraries is a WIP.
+- Is Knuckledragger python specific?
+  - Python is a useful and important platform, but the core of the design can be ported to many languages. The design is based around the chaining of calls to z3 which gets you a lot of distance for free.
+    - [SBV](https://hackage.haskell.org/package/sbv-11.0/docs/Data-SBV-Tools-KnuckleDragger.html) - Haskell
+    - Yours here!
 
 ## License & Citation
 

kdrag/__init__.py

@@ -38,7 +38,7 @@
 cond = notation.cond
 
 
-Inductive = datatype.Inductive
+Inductive = kernel.Inductive
 
 
 Record = datatype.Record

kdrag/datatype.py

@@ -1,11 +1,10 @@
 """
 Convenience features for datatypes.
 
-You should use these instead of raw `smt.Datatype`. This also maintains a record of exisitng datatypes
+You should use these instead of raw `smt.Datatype`. This also maintains a record of existing datatypes
 so that you don't clobber old ones, a possible source of unsoundness.
 
 - Datatypes support accessor notation `l.is_cons`, `l.hd`, `l.tl` etc.
-- Generic Inductive axiom schema available via `induct_inductive`
 - x._replace() syntax on single constructor datatypes
 
 >>> import kdrag.theories.nat as nat
@@ -21,6 +20,7 @@
 import kdrag.smt as smt
 import kdrag as kd
 import typing
+from kdrag.kernel import Inductive
 
 
 def _lookup_constructor_recog(
@@ -256,78 +256,6 @@ def datatype_match_(x, *cases, default=None):
 smt.DatatypeRef.match_ = datatype_match_  # type: ignore
 
 
-def induct_inductive(x: smt.DatatypeRef, P: smt.QuantifierRef) -> kd.kernel.Proof:
-    """Build a basic induction principle for an algebraic datatype"""
-    DT = x.sort()
-    assert isinstance(DT, smt.DatatypeSortRef)
-    """assert (
-        isisntance(P,QuantififerRef) and P.is_lambda()
-    )  # TODO: Hmm. Actually it should just be arraysort"""
-    hyps = []
-    for i in range(DT.num_constructors()):
-        constructor = DT.constructor(i)
-        args = [
-            smt.FreshConst(constructor.domain(j), prefix=DT.accessor(i, j).name())
-            for j in range(constructor.arity())
-        ]
-        acc = P(constructor(*args))
-        for arg in args:
-            if arg.sort() == DT:
-                acc = kd.QForAll([arg], P(arg), acc)
-            else:
-                acc = kd.QForAll([arg], acc)
-        hyps.append(acc)
-    conc = P(x)
-    return kd.axiom(smt.Implies(smt.And(hyps), conc), by="induction_axiom_schema")
-
-
-_records = {}
-
-
-def Inductive(name: str) -> smt.Datatype:
-    """
-    Declare datatypes with auto generated induction principles. Wrapper around z3.Datatype
-
-    >>> Nat = Inductive("Nat")
-    >>> Nat.declare("zero")
-    >>> Nat.declare("succ", ("pred", Nat))
-    >>> Nat = Nat.create()
-    >>> Nat.succ(Nat.zero)
-    succ(zero)
-    """
-    counter = 0
-    n = name
-    while n in _records:
-        counter += 1
-        n = name + "!" + str(counter)
-    name = n
-    assert name not in _records
-    dt = smt.Datatype(name)
-    oldcreate = dt.create
-
-    def create():
-        dt = oldcreate()
-        # Sanity check no duplicate names. Causes confusion.
-        names = set()
-        for i in range(dt.num_constructors()):
-            cons = dt.constructor(i)
-            n = cons.name()
-            if n in names:
-                raise Exception("Duplicate constructor name", n)
-            names.add(n)
-            for j in range(cons.arity()):
-                n = dt.accessor(i, j).name()
-                if n in names:
-                    raise Exception("Duplicate field name", n)
-                names.add(n)
-        kd.notation.induct.register(dt, induct_inductive)
-        _records[name] = dt
-        return dt
-
-    dt.create = create
-    return dt
-
-
 def Record(
     name: str, *fields: tuple[str, smt.SortRef], pred=None
 ) -> smt.DatatypeSortRef:

kdrag/kernel.py

@@ -2,6 +2,7 @@
 The kernel hold core proof datatypes and core inference rules. By and large, all proofs must flow through this module.
 """
 
+import kdrag as kd
 import kdrag.smt as smt
 from dataclasses import dataclass
 from typing import Any, Iterable, Sequence
@@ -125,6 +126,7 @@ class Defn:
     ax: Proof
 
 
+_datatypes = {}
 defns: dict[smt.FuncDeclRef, Defn] = {}
 """
 defn holds definitional axioms for function symbols.
@@ -337,3 +339,72 @@ def beta_conv(lam: smt.QuantifierRef, *args) -> Proof:
     assert len(args) == lam.num_vars()
     assert smt.is_quantifier(lam) and lam.is_lambda()
     return axiom(smt.Eq(lam[args], smt.substitute_vars(lam.body(), *reversed(args))))
+
+
+def induct_inductive(x: smt.DatatypeRef, P: smt.QuantifierRef) -> Proof:
+    """Build a basic induction principle for an algebraic datatype"""
+    DT = x.sort()
+    assert isinstance(DT, smt.DatatypeSortRef)
+    """assert (
+        isisntance(P,QuantififerRef) and P.is_lambda()
+    )  # TODO: Hmm. Actually it should just be arraysort"""
+    hyps = []
+    for i in range(DT.num_constructors()):
+        constructor = DT.constructor(i)
+        args = [
+            smt.FreshConst(constructor.domain(j), prefix=DT.accessor(i, j).name())
+            for j in range(constructor.arity())
+        ]
+        acc = P(constructor(*args))
+        for arg in args:
+            if arg.sort() == DT:
+                acc = kd.QForAll([arg], P(arg), acc)
+            else:
+                acc = kd.QForAll([arg], acc)
+        hyps.append(acc)
+    conc = P(x)
+    return axiom(smt.Implies(smt.And(hyps), conc), by="induction_axiom_schema")
+
+
+def Inductive(name: str) -> smt.Datatype:
+    """
+    Declare datatypes with auto generated induction principles. Wrapper around z3.Datatype
+
+    >>> Nat = Inductive("Nat")
+    >>> Nat.declare("zero")
+    >>> Nat.declare("succ", ("pred", Nat))
+    >>> Nat = Nat.create()
+    >>> Nat.succ(Nat.zero)
+    succ(zero)
+    """
+    counter = 0
+    n = name
+    while n in _datatypes:
+        counter += 1
+        n = name + "!" + str(counter)
+    name = n
+    assert name not in _datatypes
+    dt = smt.Datatype(name)
+    oldcreate = dt.create
+
+    def create():
+        dt = oldcreate()
+        # Sanity check no duplicate names. Causes confusion.
+        names = set()
+        for i in range(dt.num_constructors()):
+            cons = dt.constructor(i)
+            n = cons.name()
+            if n in names:
+                raise Exception("Duplicate constructor name", n)
+            names.add(n)
+            for j in range(cons.arity()):
+                n = dt.accessor(i, j).name()
+                if n in names:
+                    raise Exception("Duplicate field name", n)
+                names.add(n)
+        kd.notation.induct.register(dt, induct_inductive)
+        _datatypes[name] = dt
+        return dt
+
+    dt.create = create
+    return dt

kdrag/utils.py

@@ -348,7 +348,9 @@ def is_subterm(t: smt.ExprRef, t2: smt.ExprRef) -> bool:
 
 def sorts(t: smt.ExprRef):
     """Generate all sorts in a term"""
-    for t in subterms(t, into_binder=True):
+    for t in subterms(
+        t, into_binder=True
+    ):  # TODO: May want to get sorts of quantified variables that don't appear in bodies.
         yield t.sort()
 
 
@@ -367,6 +369,9 @@ def is_value(t: smt.ExprRef):
         or smt.is_true(t)
         or smt.is_false(t)
         or smt.is_string_value(t)
+        or smt.is_fp_value(t)
+        or smt.is_fprm_value(t)
+        or (smt.is_constructor(t) and all(is_value(c) for c in t.children()))
     )
 
 

tests/test_kernel.py

@@ -290,7 +290,7 @@ def test_induct():
     List = List.create()
     x = smt.Const("x", List)
     assert (
-        kd.datatype.induct_inductive(x, smt.Lambda([x], smt.BoolVal(True))) is not None
+        kd.kernel.induct_inductive(x, smt.Lambda([x], smt.BoolVal(True))) is not None
     )