moved complex up. Universal type as open datatype

Author: philzook58

src/kdrag/__init__.py

@@ -224,6 +224,38 @@ def Some(x: smt.ExprRef) -> smt.DatatypeRef:
     return OptionSort(x.sort()).Some(x)
 
 
+Complex = datatype.Struct("C", ("re", smt.RealSort()), ("im", smt.RealSort()))
+
+z, w, u, z1, z2 = smt.Consts("z w u z1 z2", Complex)
+complex_add = notation.add.define([z1, z2], Complex.C(z1.re + z2.re, z1.im + z2.im))
+complex_mul = notation.mul.define(
+    [z1, z2], Complex.C(z1.re * z2.re - z1.im * z2.im, z1.re * z2.im + z1.im * z2.re)
+)
+complex_div = notation.div.define(
+    [z1, z2],
+    Complex.C(
+        (z1.re * z2.re + z1.im * z2.im) / (z2.re**2 + z2.im**2),
+        (z1.im * z2.re - z1.re * z2.im) / (z2.re**2 + z2.im**2),
+    ),
+)
+J = Complex.C(0, 1)
+complex_one = Complex.C(1, 0)
+
+
+def ComplexSort() -> smt.DatatypeSortRef:
+    """
+    >>> C = ComplexSort()
+    >>> z, w = smt.Consts("z w", C)
+    >>> full_simp(J + J)
+    C(0, 2)
+    >>> full_simp(J * J)
+    C(-1, 0)
+    >>> full_simp(J / J)
+    C(1, 0)
+    """
+    return Complex
+
+
 def Assoc(f, T=None) -> smt.BoolRef:
     """
     >>> Assoc(smt.Function("f", smt.IntSort(), smt.IntSort(), smt.IntSort()))

src/kdrag/contrib/pcode/asmspec.py

@@ -661,8 +661,18 @@ def __init__(self, spec: AsmSpec):
     def auto(self, n, **kwargs):
         vc = self.vcs[n]
         self.pfs.append(
-            vc.verify(self.ctx, **kwargs)
+            kd.kernel.prove(
+                vc.vc(self.ctx),
+                by=(
+                    [vc.verify(self.ctx, **kwargs)]
+                    + [f.defn for f in self.ctx.definitions]
+                ),
+            )
         )  # TODO: This makes an ctx.definitions unfolded proof, which isn't what is expected?
+        return self
+
+    def __repr__(self):
+        return f"AsmProofState(num_vcs={len(self.vcs)}, num_pfs={len(self.pfs)})"
 
     def lemma(self, n) -> VCProofState:
         return VCProofState(self.vcs[n], self.ctx, _parent=self)

src/kdrag/parsers/microlean.py

@@ -192,6 +192,8 @@ def expr(tree, env: Env) -> smt.ExprRef:
             return expr(left, env) / expr(right, env)
         case Tree("eq", [left, right]):
             return smt.Eq(expr(left, env), expr(right, env))
+        case Tree("neq", [left, right]):
+            return expr(left, env) != expr(right, env)  # type: ignore
         case Tree("le", [left, right]):
             return expr(left, env) <= expr(right, env)
         case Tree("lt", [left, right]):

src/kdrag/theories/real/complex.py

@@ -2,26 +2,13 @@
 import kdrag.smt as smt
 import kdrag.theories.real as real
 
-C = kd.Struct("C", ("re", smt.RealSort()), ("im", smt.RealSort()))
-
+C = kd.ComplexSort()
 z, w, u, z1, z2 = smt.Consts("z w u z1 z2", C)
-add = kd.define("add", [z1, z2], C.C(z1.re + z2.re, z1.im + z2.im))
-kd.notation.add.register(C, add)
-mul = kd.define(
-    "mul", [z1, z2], C.C(z1.re * z2.re - z1.im * z2.im, z1.re * z2.im + z1.im * z2.re)
-)
-kd.notation.mul.register(C, mul)
+add = kd.complex_add
+mul = kd.complex_mul
+div = kd.complex_div
 conj = kd.define("conj", [z], C.C(z.re, -z.im))
 
-
-div = kd.notation.div.define(
-    [z1, z2],
-    C.C(
-        (z1.re * z2.re + z1.im * z2.im) / (z2.re**2 + z2.im**2),
-        (z1.im * z2.re - z1.re * z2.im) / (z2.re**2 + z2.im**2),
-    ),
-)
-
 C0 = C.C(0, 0)
 C1 = C.C(1, 0)
 Ci = C.C(0, 1)

src/kdrag/theories/univ.py

@@ -2,131 +2,6 @@
 import kdrag.smt as smt
 import functools
 
-_Type0 = kd.Inductive("Type0")
-_Type0.declare("Int", ("int", smt.IntSort()))
-_Type0.declare("Bool", ("bool", smt.BoolSort()))
-_Type0.declare("Real", ("real", smt.RealSort()))
-Type0 = _Type0.create()
-_x = smt.Const("x", Type0)
-
-Type0Set = smt.FullSet(Type0)
-Int0 = smt.Lambda([_x], _x.is_Int)
-Nat0 = smt.Lambda([_x], smt.And(Int0(_x), _x.int >= 0))
-Bool0 = smt.Lambda([_x], _x.is_Bool)
-Real0 = smt.Lambda([_x], _x.is_Real)
-Unit0 = smt.Lambda([_x], smt.And(_x.is_Bool, _x.bool == smt.BoolVal(True)))
-
-# Polymorphic definitions
-neg = kd.notation.neg.define(
-    [_x],
-    kd.cond(
-        (_x.is_Bool, Type0.Bool(_x.bool)),
-        (_x.is_Int, Type0.Int(-_x.int)),
-        (_x.is_Real, Type0.Real(-_x.real)),
-    ),
-)
-
-"""
-
-def from_dt(dt : smt.DatatypeSortRef) -> smt.ExprRef:
-    # encode x to tagged sequences
-    kd.cond(
-      *[dt.recognizer(i), smt.Concat(smt.Unit(Type0.IntVal(i)), smt.Unit(dt.accessor(i,0)(x))) for i in range(dt.num_constructors())])
-      )
-def to_set(dt : smt.DatatypeSortRef) -> smt.ExprRef:
-    # set corresponding to encoding
-    # smt.Exists([z], from_dt(dt)(z) == x)
-    # but there is a more computational version.
-kd.prove(forall([x], to_set(dt)(from_dt(dt))) # encoding is in encoding.
-def to_dt(dt : smt.DatatypeSortRef) -> smt.ExprRef:
-    # decode tagged sequences to x
-
-class OpenFuncDecl:
-    name : str
-    domains : tuple[smt.SortRef]
-    range : smt.SortRef
-    head : smt.FuncDeclRef
-    last : smt.FuncDeclRef
-    defns : list[smt.FuncDeclRef] = []
-    undef : smt.FuncDeclRef
-    def __init__(self, name : str, *sorts : smt.SortRef):
-        self.name = name
-        self.defns = []
-        self.undef = kd.FuncDecl(name, sorts, sorts[-1])
-    def define(self, vs, cond, body) -> smt.FuncDeclRef:
-        assert [v.sort() ==  s for v,s in zip(vs, self.sorts]
-        assert body.sort() == self.range
-        newundef = smt.FreshFunction(*[v.sort() for v in vs], self.range)
-        self.defns.append(kd.define(self.last.name(), vs, smt.If(cond, body, newundef(*vs)))
-        self.undef = newundef
-        
-
-def Seq(T : smt.FuncRef) -> smt.QuantifierRef:
-    x = smt.FreshConst("x", T.domain())
-    return smt.Lambda([x], smt.And(x.is_Seq, smt.SeqFoldLeftsmt.True, T, (x.seq)
-def Vec(n, T : smt.FuncRef) -> smt.QuantifierRef:
-    x = smt.FreshConst("x", T.domain())
-    return smt.Lambda([x], smt.And(Seq(T)(x), smt.Length(x.seq) == n))
-def Id(T, x, y) -> smt.QuantifierRef:
-    p = smt.FreshConst("p", T.domain())
-    return smt.Lambda([p], smt.And(Unit(p) , x == y))
-
-
-
-Type1 = kd.Inductive("Type1")
-Type1.declare("Type0", ("type0", Type0))
-Type1.declare("Seq", ("seq", Type1))
-Type1Sort = smt.DatatypeSort("Type1")
-# We could have deeper recursion at the same universe level
-# Type1.declare(
-#    "Array", ("array", smt.ArraySort(smt.ArraySort(Type1Sort, Type0), Type1Sort))
-# )
-Type1.declare("Array", ("array", smt.ArraySort(Type0, Type1Sort)))
-Type1 = Type1.create()
-
-def Int(x : smt.ExprRef) -> smt.BoolRef:
-
-
-def level(x : smt.ExprRef) -> smt.IntRef:
-    x.sort().name()
-"""
-
-
-def Int(l: int) -> smt.QuantifierRef:
-    """
-    >>> Int(0)
-    Lambda(x, is(Int, x))
-    >>> Int(1)
-    Lambda(x, And(is(Type0, x), is(Int, type0(x))))
-    """
-    assert l >= 0
-    if l == 0:
-        return Int0
-    else:
-        Typel = Type(l)
-        x = smt.Const("x", Typel)
-        return smt.Lambda(
-            [x], smt.And(Typel.recognizer(0)(x), Int(l - 1)(Typel.accessor(0, 0)(x)))
-        )
-
-
-@functools.cache
-def Type(l: int) -> smt.DatatypeSortRef:
-    """
-    A generic value type at universe level l.
-    >>> Type(1)
-    Type1
-    """
-    if l == 0:
-        return Type0
-    else:
-        TypeN = kd.Inductive(f"Type{l}")
-        TypeN.declare(f"Type{l - 1}", (f"type{l - 1}", Type(l - 1)))
-        TypeNSort = smt.DatatypeSort(f"Type{l}")
-        TypeN.declare("Seq", ("seq", smt.SeqSort(TypeNSort)))
-        TypeN.declare("Array", ("array", smt.ArraySort(Type(l - 1), TypeNSort)))
-        return TypeN.create()
-
 
 """
 A different style using an open datatype instead
@@ -164,3 +39,35 @@ def poly_ax(s: smt.SortRef) -> kd.Proof:
     # assert positive_poly(s)
     x = smt.Const("x", s)
     return kd.axiom(smt.ForAll([x], cast(s, box(x)) == x, patterns=[cast(s, box(x))]))
+
+
+"""
+Specialize some to an inductive datatype so we get built in support for injectors.
+"""
+
+Type = kd.Inductive("Type")
+_Type = smt.DatatypeSort("Type")
+Type.declare("Bool", ("bool", smt.BoolSort()))
+Type.declare("Int", ("int", smt.IntSort()))
+Type.declare("Real", ("real", smt.RealSort()))
+Type.declare("Seq", ("seq", smt.SeqSort(_Type)))
+Type.declare("Array", ("array", smt.ArraySort(Poly, _Type)))
+# Maybe RFun Real -> Type
+# IntFun Int -> Type
+
+Type = Type.create()
+
+# Probably unsound
+# type_poly_ax = poly_ax(Type)
+_x = smt.Const("x", Type)
+Int = smt.Lambda([_x], _x.is_Int)
+Real = smt.Lambda([_x], _x.is_Real)
+Bool = smt.Lambda([_x], _x.is_Bool)
+
+"""
+S = smt.Const("S", smt.SetSort(Type))
+mul = smt.Const("mul", smt.ArraySort(Type, Type, Type))
+semigroup = kd.define(
+    "semigroup", [S, mul], smt.And(kd.Closed(S, mul), kd.Assoc(mul, T=S))
+)
+"""