added Eq workaround to __eq__ flipping

Author: philzook58

kdrag/kernel.py

@@ -148,14 +148,16 @@ def define(name: str, args: list[smt.ExprRef], body: smt.ExprRef) -> smt.FuncDec
         def_ax = axiom(
             smt.ForAll(
                 args + vs,
-                f(*args)[tuple(vs)] == smt.substitute_vars(body.body(), *reversed(vs)),
+                smt.Eq(
+                    f(*args)[tuple(vs)], smt.substitute_vars(body.body(), *reversed(vs))
+                ),
             ),
             by="definition",
         )
     elif len(args) == 0:
-        def_ax = axiom(f() == body, by="definition")
+        def_ax = axiom(smt.Eq(f(), body), by="definition")
     else:
-        def_ax = axiom(smt.ForAll(args, f(*args) == body), by="definition")
+        def_ax = axiom(smt.ForAll(args, smt.Eq(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)
@@ -196,7 +198,7 @@ def consider(x: smt.ExprRef) -> Proof:
     Axiom schema. We may give a fresh name to any constant. An "anonymous" form of define.
     Pointing out the interesting terms is sometimes the essence of a proof.
     """
-    return axiom(smt.FreshConst(x.sort(), prefix="consider") == x)
+    return axiom(smt.Eq(smt.FreshConst(x.sort(), prefix="consider"), x))
 
 
 def instan(ts: list[smt.ExprRef], pf: Proof) -> Proof:
@@ -297,4 +299,4 @@ 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(lam[args] == smt.substitute_vars(lam.body(), *reversed(args)))
+    return axiom(smt.Eq(lam[args], smt.substitute_vars(lam.body(), *reversed(args))))

kdrag/smt.py

@@ -72,3 +72,13 @@ def _qsort(self):
     )
 
 config.solver = Solver
+
+
+def Eq(x, y):
+    """Python __eq__ resolution rules flips the order if y is a subclass of x.
+    This function corrects that."""
+    e = x == y
+    if type(x) is not type(y) and issubclass(type(y), type(x)):
+        return e.decl()(e.arg(1), e.arg(0))
+    else:
+        return e

tests/test_kernel.py

@@ -209,14 +209,14 @@ def test_Lemma():
     even = kd.define("even", [x], smt.Exists([y], x == 2 * y))
     odd = kd.define("odd", [x], smt.Exists([y], x == 2 * y + 1))
 
-    evdef2 = kd.lemma(
+    evdef2 = kd.kernel.lemma(
         smt.ForAll([x], even(x) == smt.Exists([y], x == 2 * y)), by=[even.defn]
     )
     l = kd.Lemma(kd.QForAll([x], even(x), even(x + 2)))
     x1 = l.intros()
     l.intros()
-    l.apply(even.defn, rev=True)
-    l.rewrite(even.defn, at=0, rev=True)
+    l.apply(even.defn)
+    l.rewrite(even.defn, at=0)
     y1 = l.einstan(0)
     l.exists(y1 + 1)
     l.auto()
@@ -229,8 +229,8 @@ def test_Lemma():
     [
         x1 := l.intros(),
         l.intros(),
-        l.apply(even.defn, rev=True),
-        l.rewrite(even.defn, at=0, rev=True),
+        l.apply(even.defn),
+        l.rewrite(even.defn, at=0),
         y1 := l.einstan(0),
         l.exists(y1 + 1),
         l.auto(),
@@ -264,6 +264,13 @@ def test_Lemma():
     l.qed()
 
 
+def test_eq():
+    x, y = smt.Ints("x y")
+    assert smt.Eq(smt.IntVal(2) + smt.IntVal(3), smt.IntVal(5)).arg(1).eq(smt.IntVal(5))
+    assert smt.Eq((x >= 14), smt.Exists([y], x == 2 * y)).arg(0).eq(x >= 14)
+    assert smt.Eq((x >= 14), x >= 13).arg(0).eq(x >= 14)
+
+
 def test_pred():
     Even = kd.Record(
         "Even", ("val", kd.Z), ("div2", kd.Z), pred=lambda x: 2 * x.div2 == x.val
@@ -292,7 +299,7 @@ def test_beta():
     )
     t = smt.Lambda([x], x)
     assert kd.kernel.beta_conv(t, smt.IntVal(42)).thm.eq(
-        t[smt.IntVal(42)] == smt.IntVal(42)
+        smt.Eq(t[smt.IntVal(42)], smt.IntVal(42))
     )
 
 

tests/test_solver.py

@@ -292,6 +292,8 @@ def test_tptp():
     )
 
 
+"""
+TODO: Not installing aprove in CI?
 def test_aprove():
     plus = smt.Function("plus", smt.IntSort(), smt.IntSort(), smt.IntSort())
     x, y, z = smt.Ints("x y z")
@@ -300,3 +302,4 @@ def test_aprove():
     kd.solvers.aprove.run_aprove(
         [x, y], [plus(x, zero) == x, plus(x, succ(y)) == succ(plus(x, y))]
     )
+"""