group theory axioms

kdrag/notation.py

@@ -67,14 +67,7 @@ def define(self, args, body):
 smt.ExprRef.__sub__ = lambda x, y: sub(x, y)
 
 mul = SortDispatch(name="mul")
-
-
-def test(x, y):
-    print("mul", x, x.sort(), y)
-    return mul(x, y)
-
-
-smt.ExprRef.__mul__ = lambda x, y: test(x, y)  # mul(x, y)
+smt.ExprRef.__mul__ = lambda x, y: mul(x, y)
 
 rmul = SortDispatch(name="rmul")
 smt.ExprRef.__rmul__ = lambda x, y: rmul(x, y)

kdrag/tactics.py

@@ -37,7 +37,7 @@ def trans(self, y):
                 else:
                     return False
 
-    def __init__(self, vars, lhs, assume=[]):
+    def __init__(self, vars: list[smt.ExprRef], lhs: smt.ExprRef, assume=[]):
         self.vars = vars
         self.lhs = lhs
         self.iterm = lhs  # intermediate term

kdrag/theories/algebra/group.py

@@ -1,13 +1,52 @@
 import kdrag as kd
 import kdrag.smt as smt
 
+# https://en.wikipedia.org/wiki/Group_(mathematics)
+
 G = smt.DeclareSort("G")
 mul = smt.Function("mul", G, G, G)
 kd.notation.mul.register(G, mul)
 e = smt.Const("e", G)
 inv = smt.Function("inv", G, G)
 x, y, z = smt.Consts("x y z", G)
 
-mul_id = kd.axiom(smt.ForAll([x], x * e == x))
-inv_mul = kd.axiom(smt.ForAll([x], inv(x) * x == x))
 mul_assoc = kd.axiom(smt.ForAll([x, y, z], x * (y * z) == (x * y) * z))
+id_left = kd.axiom(smt.ForAll([x], e * x == x))
+inv_left = kd.axiom(smt.ForAll([x], inv(x) * x == e))
+
+c = kd.Calc([x], e, assume=[smt.ForAll([y], y * x == y)])
+c.eq(e * x)
+c.eq(x, by=[id_left])
+id_unique1 = c.qed()
+
+c = kd.Calc([x], x * inv(x))
+c.eq(e * (x * inv(x)), by=[id_left])
+c.eq((inv(inv(x)) * inv(x)) * (x * inv(x)), by=[inv_left])
+c.eq(inv(inv(x)) * ((inv(x) * x) * inv(x)), by=[mul_assoc])
+c.eq(inv(inv(x)) * (e * inv(x)), by=[inv_left])
+c.eq(inv(inv(x)) * inv(x), by=[id_left])
+c.eq(e, by=[inv_left])
+inv_right = c.qed()
+
+c = kd.Calc([x], x * e)
+c.eq(x * (inv(x) * x), by=[inv_left])
+c.eq((x * inv(x)) * x, by=[mul_assoc])
+c.eq(e * x, by=[inv_right])
+c.eq(x, by=[id_left])
+id_right = c.qed()
+
+c = kd.Calc([x], e, assume=[smt.ForAll([y], x * y == y)])
+c.eq(x * e)
+c.eq(x, by=[id_right])
+id_unique2 = c.qed()
+
+c = kd.Calc([x, y], y, assume=[y * x == e])
+c.eq(y * e, by=[id_right])
+c.eq(y * (x * inv(x)), by=[inv_right])
+c.eq((y * x) * inv(x), by=[mul_assoc])
+c.eq(e * inv(x), by=[inv_right])
+c.eq(inv(x), by=[id_left])
+inv_unique1 = c.qed()
+
+
+abelian = kd.define("abelian", [], smt.ForAll([x, y], x * y == y * x))

pyproject.toml

@@ -16,4 +16,4 @@ homepage = "https://github.com/philzook58/knuckledragger"
 
 
 [project.optional-dependencies]
-dev = ["pytest>=6.0", "nbclient"]
+dev = ["pytest>=6.0", "nbclient", "jupyter"]