eunify and putting more in prelude

Author: philzook58

src/kdrag/__init__.py

@@ -15,6 +15,7 @@
 from . import datatype
 from . import rewrite
 from . import tactics
+import functools
 
 
 Proof = kernel.Proof
@@ -74,6 +75,95 @@
 RSeq = Z >> R
 RFun = R >> R
 
+
+def seq(*args):
+    """
+    Helper to construct sequences.
+    >>> seq(1, 2, 3)
+    Concat(Unit(1), Concat(Unit(2), Unit(3)))
+    >>> seq(1)
+    Unit(1)
+    """
+    if len(args) == 0:
+        raise ValueError(
+            "seq() requires at least one argument. use smt.Empty(sort) instead."
+        )
+    elif len(args) == 1:
+        return smt.Unit(smt._py2expr(args[0]))
+    else:
+        return smt.Concat(*[smt.Unit(smt._py2expr(a)) for a in args])
+
+
+Nat = Inductive("Nat")
+Nat.declare("Z")
+Nat.declare("S", ("pred", Nat))
+Nat = Nat.create()
+
+
+def NatSort() -> smt.DatatypeSortRef:
+    global Nat
+    assert isinstance(Nat, smt.DatatypeSortRef)
+    return Nat
+
+
+@functools.cache
+def ListSort(Elt: smt.SortRef) -> smt.DatatypeSortRef:
+    """
+    >>> ListSort(smt.IntSort())
+    List_Int...
+    """
+    T = Inductive("List_" + Elt.name())
+    T.declare("Nil")
+    T.declare("Cons", ("head", Elt), ("tail", T))
+    return T.create()
+
+
+def list(*args: smt.ExprRef) -> smt.DatatypeRef:
+    """
+    Helper to construct List values
+    >>> list(1, 2, 3)
+    Cons(1, Cons(2, Cons(3, Nil)))
+    """
+    if len(args) == 0:
+        raise ValueError("list() requires at least one argument")
+    LT = ListSort(smt._py2expr(args[0]).sort())
+    acc = LT.Nil
+    for a in reversed(args):
+        acc = LT.Cons(a, acc)
+    return acc
+
+
+@functools.cache
+def OptionSort(T: smt.SortRef) -> smt.DatatypeSortRef:
+    """
+    Define an Option type for a given type T
+    >>> OInt = OptionSort(smt.IntSort())
+    >>> OInt.Some(1)
+    Some(1)
+    >>> OInt.None_
+    None_
+    >>> OInt.Some(1).val
+    val(Some(1))
+    """
+    Option = Inductive("Option_" + T.name())
+    Option.declare("None_")
+    Option.declare("Some", ("val", T))
+    return Option.create()
+
+
+# I guess I could make this a SortDispatch for regularity. I just don't see why I'd need to overload in any way but the default
+def Some(x: smt.ExprRef) -> smt.DatatypeRef:
+    """
+    Helper to create Option values
+    >>> Some(42)
+    Some(42)
+    >>> Some(42).sort()
+    Option_Int
+    """
+    x = smt._py2expr(x)
+    return OptionSort(x.sort()).Some(x)
+
+
 __all__ = [
     "prove",
     "axiom",

src/kdrag/contrib/junk_drawer/list.py

@@ -5,46 +5,16 @@
 """
 
 import kdrag as kd
-import functools
 import kdrag.smt as smt
 
 
-@functools.cache
-def List(sort: smt.SortRef) -> smt.DatatypeSortRef:
-    """
-    Build List sort
-    >>> IntList = List(smt.IntSort())
-    >>> IntList.Cons(1, IntList.Nil)
-    Cons(1, Nil)
-    """
-    dt = kd.Inductive("List_" + sort.name())
-    dt.declare("Nil")
-    dt.declare("Cons", ("head", sort), ("tail", dt))
-    return dt.create()
-
-
-def list(*args: smt.ExprRef) -> smt.DatatypeRef:
-    """
-    Helper to construct List values
-    >>> list(1, 2, 3)
-    Cons(1, Cons(2, Cons(3, Nil)))
-    """
-    if len(args) == 0:
-        raise ValueError("list() requires at least one argument")
-    LT = List(smt._py2expr(args[0]).sort())
-    acc = LT.Nil
-    for a in reversed(args):
-        acc = LT.Cons(a, acc)
-    return acc
-
-
 def Cons(x: smt.ExprRef, xs: smt.DatatypeRef) -> smt.DatatypeRef:
     """
     Helper to construct Cons values
     >>> Cons(1, Nil(smt.IntSort()))
     Cons(1, Nil)
     """
-    LT = List(smt._py2expr(x).sort())
+    LT = kd.ListSort(smt._py2expr(x).sort())
     return LT.Cons(x, xs)
 
 
@@ -54,7 +24,7 @@ def Nil(sort: smt.SortRef) -> smt.DatatypeRef:
     >>> Nil(smt.IntSort())
     Nil
     """
-    return List(sort).Nil
+    return kd.ListSort(sort).Nil
 
 
 def Unit(x: smt.ExprRef) -> smt.DatatypeRef:
@@ -66,5 +36,5 @@ def Unit(x: smt.ExprRef) -> smt.DatatypeRef:
     List_Int
     """
     x = smt._py2expr(x)
-    LT = List(x.sort())
+    LT = kd.ListSort(x.sort())
     return LT.Cons(x, LT.Nil)

src/kdrag/kernel.py

@@ -564,7 +564,7 @@ def Inductive(name: str) -> smt.Datatype:
     dt = smt.Datatype(name)
     oldcreate = dt.create
 
-    def create():
+    def create() -> smt.DatatypeSortRef:
         dt = oldcreate()
         # Sanity check no duplicate names. Causes confusion.
         names = set()

src/kdrag/notation.py

@@ -300,7 +300,45 @@ def GenericDispatch(default_factory) -> SortDispatch:
 """Sort based dispatch for `Exists` quantifier."""
 # smt.ExprRef.exists = lambda vs, body: exists(vs, body)
 
-induct = SortDispatch(name="induct")
+
+def induct_seq(a: smt.SeqRef, P) -> kd.kernel.Proof:
+    """
+    >>> x = smt.Const("x", smt.SeqSort(smt.IntSort()))
+    >>> induct(x, lambda s: smt.Length(s) >= 0)
+    |= Implies(And(Length(Empty(Seq(Int))) >= 0,
+                ForAll(z!..., Length(Unit(z!...)) >= 0),
+                ForAll([x!..., y!...],
+                       Implies(And(Length(x!...) >= 0,
+                                   Length(y!...) >= 0),
+                               Length(Concat(x!..., y!...)) >= 0))),
+            Length(x) >= 0)
+    """
+    assert isinstance(a, smt.SeqRef)
+    sort = a.sort()
+    T = sort.basis()
+    z = smt.FreshConst(T, prefix="z")
+    x, y = smt.FreshConst(sort, prefix="x"), smt.FreshConst(sort, prefix="y")
+    return kd.axiom(
+        smt.Implies(
+            smt.And(
+                P(smt.Empty(sort)),
+                QForAll([z], P(smt.Unit(z))),
+                QForAll([x, y], P(x), P(y), P(smt.Concat(x, y))),
+            ),
+            # -------------------------------------------------
+            P(a),
+        )
+    )
+
+
+def induct_default(x, P):
+    if isinstance(x, smt.SeqRef):
+        return induct_seq(x, P)
+    else:
+        raise NotImplementedError("No default induct implementation for sort", x.sort())
+
+
+induct = SortDispatch(name="induct", default=induct_default)
 """Sort based dispatch for induction principles. Should instantiate an induction scheme for variable x and predicate P"""
 smt.ExprRef.induct = lambda x, P: induct(x, P)  # type: ignore
 

src/kdrag/theories/list.py

@@ -6,19 +6,9 @@
 
 import kdrag as kd
 import kdrag.smt as smt
-import functools
 
 
-@functools.cache
-def ListSort(Elt: smt.SortRef) -> smt.DatatypeSortRef:
-    """
-    >>> ListSort(smt.IntSort())
-    List_Int...
-    """
-    T = kd.Inductive("List_" + Elt.name())
-    T.declare("Nil")
-    T.declare("Cons", ("head", Elt), ("tail", T))
-    return T.create()
+ListSort = kd.ListSort
 
 
 class List:

src/kdrag/theories/nat.py

@@ -6,10 +6,7 @@
 import kdrag.smt as smt
 import kdrag.theories.int as int_  # int is more primitive. We import it's induction principle here.
 
-Nat = kd.Inductive("Nat")
-Nat.declare("Z")
-Nat.declare("S", ("pred", Nat))
-Nat = Nat.create()
+Nat = kd.Nat
 
 
 S = Nat.S

src/kdrag/theories/option.py

@@ -3,45 +3,29 @@
 
 """
 
-import functools
 import kdrag.smt as smt
 import kdrag as kd
 
 
-@functools.cache
-def OptionSort(T: smt.SortRef) -> smt.DatatypeSortRef:
-    """
-    Define an Option type for a given type T
-    >>> OInt = OptionSort(smt.IntSort())
-    >>> OInt.Some(1)
-    Some(1)
-    >>> OInt.None_
-    None_
-    >>> OInt.Some(1).val
-    val(Some(1))
-    """
-    Option = kd.Inductive("Option_" + T.name())
-    Option.declare("None_")
-    Option.declare("Some", ("val", T))
-    return Option.create()
+OptionSort = kd.OptionSort
 
 
 def is_option(x: smt.DatatypeRef) -> bool:
     """
     Check if a value is an Option
-    >>> is_option(Some(42))
+    >>> is_option(kd.Some(42))
     True
     >>> is_option(42)
     False
     """
-    return smt._py2expr(x).sort().name().startswith("Option_")
+    return isinstance(x, smt.DatatypeRef) and x.sort().name().startswith("Option_")
 
 
 # This should also perhaps be a SortDispatch
 def get(x: smt.DatatypeRef, default: smt.ExprRef) -> smt.ExprRef:
     """
     Get the value of an Option, or a default value if it is None_
-    >>> get(Some(42), 0)
+    >>> get(kd.Some(42), 0)
     If(is(Some, Some(42)), val(Some(42)), 0)
     """
     default = smt._py2expr(default)
@@ -54,23 +38,13 @@ def get(x: smt.DatatypeRef, default: smt.ExprRef) -> smt.ExprRef:
     return smt.If(x.is_Some, x.val, default)
 
 
-# I guess I could make this a SortDispatch for regularity. I just don't see why I'd need to overload in any way but the default
-def Some(x: smt.ExprRef) -> smt.DatatypeRef:
-    """
-    Helper to create Option values
-    >>> Some(42)
-    Some(42)
-    >>> Some(42).sort()
-    Option_Int
-    """
-    x = smt._py2expr(x)
-    return OptionSort(x.sort()).Some(x)
-
-
 def None_(T: smt.SortRef) -> smt.DatatypeRef:
     """
     Helper to create Option None_ values
     >>> None_(smt.IntSort())
     None_
     """
     return OptionSort(T).None_
+
+
+Some = kd.Some

src/kdrag/theories/seq.py

@@ -38,6 +38,7 @@ def induct_list(x: smt.SeqRef, P):
     )
 
 
+"""
 def induct(T: smt.SortRef, P) -> kd.kernel.Proof:
     z = smt.FreshConst(T, prefix="z")
     sort = smt.SeqSort(T)
@@ -50,24 +51,11 @@ def induct(T: smt.SortRef, P) -> kd.kernel.Proof:
         )  # -------------------------------------------------
         == kd.QForAll([x], P(x))
     )
+"""
 
+induct = kd.notation.induct_seq
 
-def seq(*args):
-    """
-    Helper to construct sequences.
-    >>> seq(1, 2, 3)
-    Concat(Unit(1), Concat(Unit(2), Unit(3)))
-    >>> seq(1)
-    Unit(1)
-    """
-    if len(args) == 0:
-        raise ValueError(
-            "seq() requires at least one argument. use smt.Empty(sort) instead."
-        )
-    elif len(args) == 1:
-        return smt.Unit(smt._py2expr(args[0]))
-    else:
-        return smt.Concat(*[smt.Unit(smt._py2expr(a)) for a in args])
+seq = kd.seq
 
 
 def Cons(x: smt.ExprRef, tl: smt.SeqSortRef):