cauchy schwartz for vec3. andE tactic. speiclaize doesn't keep by default. More tactics return formulas

Author: philzook58

src/kdrag/solvers/synth/__init__.py

@@ -48,6 +48,11 @@ def cegis_simple(spec: smt.ExprRef) -> Optional[list[smt.ExprRef]]:
             raise Exception("Unknown result from solver", res)
 
 
+"""
+cegis with solve definitions exposed to verifier vs
+
+"""
+
 """
 Top down
 Bottom up / Contextual compression

src/kdrag/tactics.py

@@ -844,6 +844,33 @@ def boolsimp(self) -> "ProofState":
         self.goals[-1] = goalctx._replace(ctx=newctx, goal=newgoal)
         return self
 
+    def forward(self, n: int | smt.BoolRef) -> smt.BoolRef:
+        """
+        Remove the hypothesis of an implication in the context
+
+        >>> p,q,r = smt.Bools("p q r")
+        >>> l = Lemma(smt.Implies(smt.And(p, smt.Implies(p, q)), r))
+        >>> _  = l.intros()
+        >>> l.split(at=0)
+        [p, Implies(p, q)] ?|= r
+        >>> l.forward(1)
+        q
+        >>> l
+        [p, q] ?|= r
+        """
+        # TODO: extra by paramters? Give an exact index to use modus ponens?
+        goalctx = self.top_goal()
+        (at, formula) = goalctx.ctx_find(n)
+        if smt.is_implies(formula):
+            hyp, conc = formula.children()
+            self.have(hyp, by=[])
+            self.goals[-1] = goalctx._replace(
+                ctx=goalctx.ctx[:at] + [conc] + goalctx.ctx[at + 1 :]
+            )
+            return conc
+        else:
+            raise ValueError("forward failed. Not an implication", formula)
+
     def emt(self):
         """
         Use egraph based equality modulo theories to simplify the goal.
@@ -1059,17 +1086,7 @@ def obtain(self, n: int | smt.QuantifierRef) -> smt.ExprRef | list[smt.ExprRef]:
         """
         goalctx = self.top_goal()
         ctx, goal = goalctx.ctx, goalctx.goal
-        if isinstance(n, smt.QuantifierRef):
-            for i, f in enumerate(ctx):
-                if f.eq(n):
-                    n = i
-                    break
-            else:
-                raise ValueError("obtain failed. Formula not in context", n)
-        assert isinstance(n, int)
-        if n < 0:
-            n = len(ctx) + n
-        formula = ctx[n]
+        n, formula = goalctx.ctx_find(n)
         if isinstance(formula, smt.QuantifierRef) and formula.is_exists():
             self.pop_goal()
             fs, obtain_lemma = kd.kernel.obtain(formula)
@@ -1123,33 +1140,36 @@ def contract(self) -> "ProofState":
         self.goals[-1] = self.goalctx._replace(ctx=newctx)
         return self
 
-    def specialize(self, n: int | smt.QuantifierRef, *ts):
+    def specialize(self, n: int | smt.QuantifierRef, *ts, keep=False) -> smt.BoolRef:
         """
         Instantiate a universal quantifier in the context.
 
         >>> x,y = smt.Ints("x y")
         >>> l = Lemma(smt.Implies(smt.ForAll([x],x == y), True))
-        >>> l.intros()
+        >>> hyp = l.intros()
+        >>> hyp
         ForAll(x, x == y)
         >>> l
         [ForAll(x, x == y)] ?|= True
-        >>> l.specialize(0, smt.IntVal(42))
-        [ForAll(x, x == y), 42 == y] ?|= True
+        >>> l.specialize(hyp, smt.IntVal(42))
+        42 == y
+        >>> l
+        [42 == y] ?|= True
         """
         goalctx = self.top_goal()
-        if isinstance(n, smt.QuantifierRef):
-            for i, f in enumerate(goalctx.ctx):
-                if f.eq(n):
-                    n = i
-                    break
-            else:
-                raise ValueError("Specialize failed. Formula not in context", n)
-        thm = goalctx.ctx[n]
+        (n, thm) = goalctx.ctx_find(n)
         if isinstance(thm, smt.QuantifierRef) and thm.is_forall():
             l = kd.kernel.specialize(ts, thm)
             self.add_lemma(l)
-            self.goals[-1] = goalctx._replace(ctx=goalctx.ctx + [l.thm.arg(1)])
-            return self
+            # kernel.specialize returns Implies(forall x, P, P[t/x])
+            newformula = l.thm.arg(1)
+            if keep:
+                self.goals[-1] = goalctx._replace(ctx=goalctx.ctx + [newformula])
+            else:
+                self.goals[-1] = goalctx._replace(
+                    ctx=goalctx.ctx[:n] + [newformula] + goalctx.ctx[n + 1 :]
+                )
+            return newformula
         else:
             foralls = {
                 n: formula
@@ -1184,6 +1204,28 @@ def ext(self, at=None):
         else:
             raise ValueError("Ext failed. Target is not an equality", target)
 
+    def andE(self, n: int | smt.BoolRef) -> list[smt.BoolRef]:
+        """
+        Eliminate an `And` in the context.
+
+        >>> p,q = smt.Bools("p q")
+        >>> l = Lemma(smt.Implies(smt.And(p, q), p))
+        >>> _ = l.intros()
+        >>> p,q = l.andE(0)
+        >>> l
+        [p, q] ?|= p
+        """
+        goalctx = self.top_goal()
+        (at, formula) = goalctx.ctx_find(n)
+        if smt.is_and(formula):
+            children = formula.children()
+            self.goals[-1] = goalctx._replace(
+                ctx=goalctx.ctx[:at] + children + goalctx.ctx[at + 1 :]
+            )
+            return children
+        else:
+            raise ValueError("andE failed. Not an and", formula)
+
     def split(self, at=None) -> "ProofState":
         """
         `split` breaks apart an `And` or bi-implication `==` goal.
@@ -1243,21 +1285,22 @@ def cb():
         else:
             (at, hyp) = goalctx.ctx_find(at)
             if smt.is_or(hyp):
+                # Make N new goals for each disjunct
                 self.pop_goal()
                 for c in hyp.children():
                     self.goals.append(
                         goalctx._replace(ctx=ctx[:at] + [c] + ctx[at + 1 :], goal=goal)
                     )
-            elif smt.is_and(hyp):
+            elif smt.is_and(hyp):  # TODO: phase this out in favor of andE.
                 self.pop_goal()
                 self.goals.append(
                     goalctx._replace(
                         ctx=ctx[:at] + ctx[at].children() + ctx[at + 1 :], goal=goal
                     )
                 )
+                return self
             else:
                 raise ValueError("Split failed on", ctx[at], "in context", ctx)
-            return self
 
     def left(self, n=0):
         """

src/kdrag/theories/real/__init__.py

@@ -124,6 +124,7 @@ def abstract_arith(t: smt.ExprRef) -> smt.ExprRef:
 abs = kd.define("absR", [x], smt.If(x >= 0, x, -x))
 sgn = kd.define("sgn", [x], smt.If(x > 0, 1, smt.If(x < 0, -1, 0)))
 
+abs_if_pos = kd.prove(ForAll([x], x >= 0, abs(x) == x), by=[abs.defn])
 sgn_abs = kd.prove(ForAll([x], abs(x) * sgn(x) == x), by=[abs.defn, sgn.defn])
 abs_le = kd.prove(
     ForAll([x, y], (abs(x) <= y) == smt.And(-y <= x, x <= y)), by=[abs.defn]
@@ -262,9 +263,13 @@ def abstract_arith(t: smt.ExprRef) -> smt.ExprRef:
 )
 
 sqr = kd.define("sqr", [x], x * x)
+sqr_pos = kd.prove(
+    ForAll([x], sqr(x) >= 0),
+    by=[sqr.defn],
+)
+sqr_neg = kd.prove(smt.ForAll([x], sqr(-x) == sqr(x)), by=[sqr.defn])
 
-
-sqrt = kd.define("sqrt", [x], x**0.5)
+sqrt = kd.define("sqrt", [x], x ** "1/2")
 
 _l = kd.Lemma(kd.QForAll([x], x >= 0, sqrt(x) >= 0))
 _ = _l.fix()
@@ -274,6 +279,8 @@ def abstract_arith(t: smt.ExprRef) -> smt.ExprRef:
 
 sqrt_define = kd.prove(smt.ForAll([x], sqrt(x) == x**0.5), by=[sqrt.defn, pow.defn])
 
+sqrt_one = kd.prove(sqrt(1) == 1, by=[sqrt.defn])
+sqrt_zero = kd.prove(sqrt(0) == 0, by=[sqrt.defn])
 _l = kd.Lemma(kd.QForAll([x], x >= 0, sqrt(x) ** 2 == x))
 _ = _l.fix()
 _l.unfold()
@@ -284,12 +291,31 @@ def abstract_arith(t: smt.ExprRef) -> smt.ExprRef:
     kd.QForAll([x], x >= 0, sqr(sqrt(x)) == x), by=[sqrt_square, sqr.defn]
 )
 
+
+sqrt_mul = kd.prove(
+    kd.QForAll([x, y], x >= 0, y >= 0, sqrt(x * y) == sqrt(x) * sqrt(y)),
+    by=[sqrt.defn, mul.defn],
+)
+sqrt_mono = kd.prove(
+    kd.QForAll([x, y], x >= 0, y >= 0, x <= y, sqrt(x) <= sqrt(y)),
+    by=[sqrt.defn],
+)
+
 _l = kd.Lemma(kd.QForAll([x], x >= 0, sqrt(sqr(x)) == x))
 _ = _l.fix()
 _l.unfold()
 _l.auto()
 sqrt_sqr = _l.qed()
 
+sqrt_sqr_neg = kd.prove(
+    kd.QForAll([x], x <= 0, sqrt(sqr(x)) == -x), by=[sqrt_sqr, sqr_neg]
+)
+
+sqrt_sqr_abs = kd.prove(
+    kd.QForAll([x], sqrt(sqr(x)) == abs(x)),
+    by=[abs.defn, sqrt_sqr, sqrt_sqr_neg, sqr_pos],
+)
+
 exp = smt.Function("exp", R, R)  # smt.Const("exp", kd.R >> kd.R)
 exp_add = kd.axiom(smt.ForAll([x, y], exp(x + y) == exp(x) * exp(y)))
 exp_lower = kd.axiom(

src/kdrag/theories/real/complex.py

@@ -10,8 +10,11 @@
 conj = kd.define("conj", [z], C.C(z.re, -z.im))
 
 C0 = C.C(0, 0)
+zero = C0
 C1 = C.C(1, 0)
+one = C1
 Ci = C.C(0, 1)
+j = Ci
 
 add_zero = kd.prove(smt.ForAll([z], z + C0 == z), by=[add.defn])
 mul_zero = kd.prove(smt.ForAll([z], z * C0 == C0), by=[mul.defn])
@@ -21,6 +24,9 @@
     smt.ForAll([z, w, u], (z + (w + u)) == ((z + w) + u)), by=[add.defn]
 )
 mul_comm = kd.prove(smt.ForAll([z, w], z * w == w * z), by=[mul.defn])
+mul_assoc = kd.prove(
+    smt.ForAll([z, w, u], (z * (w * u)) == ((z * w) * u)), by=[mul.defn]
+)
 
 # unstable perfoamnce.
 # mul_div = kd.prove(ForAll([z,w], Implies(w != C0, z == z * w / w)), by=[div.defn, mul.defn], timeout=1000)

src/kdrag/theories/real/geometry.py

@@ -2,15 +2,15 @@
 import kdrag.smt as smt
 
 # import kdrag.theories.real as real
-import kdrag.theories.real.vec as vec
+import kdrag.theories.real.vec2 as vec2
 import kdrag.theories.set as set_
 
 
-Point2D = vec.Vec2
+Point2D = vec2.Vec2
 p, q, a, b, c = smt.Consts("p q a b c", Point2D)
 
 r = smt.Real("r")
-circle = kd.define("circle", [c, r], smt.Lambda([p], vec.norm2(p - c) == r * r))
+circle = kd.define("circle", [c, r], smt.Lambda([p], vec2.norm2(p - c) == r * r))
 
 Shape = set_.Set(Point2D)
 

src/kdrag/theories/real/lim_algebra.py

@@ -62,7 +62,7 @@ def has_lim_smul(l):
     n = l.fix()
     l.assumes(n > N1)
     forall_n = kd.QForAll([n_var], n_var > N1, real.abs(a[n_var] - x) < eps1)
-    l.specialize(forall_n, n)
+    l.specialize(forall_n, n, keep=True)
     l.have(real.abs(a[n] - x) < eps1, by=[])
     l.unfold(seq.smul)
     l.simp()
@@ -167,10 +167,10 @@ def has_lim_mul(l):
     l.unfold(seq.has_lim, at=0)
     l.unfold(seq.has_lim, at=1)
     l.specialize(0, eps1)
-    l.specialize(1, eps2)
+    l.specialize(1, eps2, keep=True)
 
     l.have(smt.RealVal(1) > 0, by=[])
-    l.specialize(1, smt.RealVal(1))
+    l.specialize(1, smt.RealVal(1), keep=True)
 
     N1 = smt.Int("N")
     N2 = smt.Int("N")

src/kdrag/theories/real/seq.py

@@ -171,8 +171,12 @@ def cumsum_const(l):
 # cumsum pownat = 1 - x^(n + 1) / (1 - x)
 # cumsum_diff - the fundamental theorem of calculus for sequences
 
+"""
 
 # TODO: cumsum_comm = cumsum(lambda x, cumsum(lammbda y, a[x,y]) ) ???
+
+
+# TODO: unstable
 @kd.Theorem(
     "forall (a : RSeq) (x : Real) (n : Int), cumsum (smul x a) n = smul x (cumsum a) n"
 )
@@ -200,6 +204,7 @@ def cumsum_smul(l):
     l.unfold(cumsum, smul)
     l.simp()
     l.auto(by=[smul.defn, cumsum.defn])
+"""
 
 
 @kd.Theorem(