From ffc79f4372abe5c80b4c344d8eb3d4beaa95ad10 Mon Sep 17 00:00:00 2001
From: Bram van den Heuvel <bram.vdh1999@gmail.com>
Date: Mon, 29 Jun 2026 14:50:51 +0200
Subject: [PATCH] Simplify & generalize types to "App" & "Const" types

---
 proof.py | 97 +++++++++++++++++++-------------------------------------
 1 file changed, 32 insertions(+), 65 deletions(-)

diff --git a/proof.py b/proof.py
index c3046dd..86909db 100644
--- a/proof.py
+++ b/proof.py
@@ -19,41 +19,29 @@ class App(Term):
 class Const(Term):
     name : str
 
-@dataclass(frozen=True)
-class Var(Term):
-    name : str
-
 # --- Bool constructors ---
 
-Bool = Union["Truth", "Contradiction"]
+def Truth() -> Term:
+    return Const("Bool.Truth")
 
-@dataclass(frozen=True)
-class Truth(Term):
-    pass
-
-@dataclass(frozen=True)
-class Contradiction(Term):
-    pass
+def Contradiction() -> Term:
+    return Const("Bool.Contradiction")
 
 # --- Nat constructors ---
 
-Nat = Union["Zero", "Succ"]
+def Zero() -> Term:
+    return Const("Nat.Zero")
 
-@dataclass(frozen=True)
-class Zero(Term):
-    pass
+def Succ(n : Term) -> Term:
+    return App(Const("Nat.Succ"), n)
 
-@dataclass(frozen=True)
-class Succ(Term):
-    n : Term
-
-def kernel_from_int(n : int) -> Nat:
+def kernel_from_int(n : int) -> Term:
     if n == 0:
         return Zero()
     elif n < 0:
         raise ValueError("Int is not Nat")
     else:
-        return Succ(n=kernel_from_int(n=n-1))
+        return Succ(kernel_from_int(n-1))
 
 # -----------------------------------------------------------------------------
 # Propositions
@@ -87,40 +75,44 @@ class F:
     arity : int
     func : Callable[..., Term | None]
 
+F_ = lambda a : lambda f : F(arity=a, func=f)
+F0, F1, F2, F3 = F_(0), F_(1), F_(2), F_(3)
+F4, F5, F6, F7 = F_(4), F_(5), F_(6), F_(7)
+
 def apply_rules() -> dict[str, F]:
     def __bool_not(x : Term) -> Term | None:
         match x:
-            case Truth():
+            case Const("Bool.Truth"):
                 return Contradiction()
             
-            case Contradiction():
+            case Const("Bool.Contradiction"):
                 return Truth()
     
     def __nat_add(x : Term, y : Term) -> Term | None:
         match x:
-            case Zero():
+            case Const("Nat.Zero"):
                 return y
             
-            case Succ():
+            case App(f=Const("Nat.Succ"), x=x_):
                 return Succ(
-                    n=normalize(App(
-                        f=App(Const("Nat.add"), x=x.n),
+                    App(
+                        f=App(Const("Nat.add"), x_),
                         x=y,
-                    ))
+                    )
                 )
     
     def __nat_iszero(x : Term) -> Term | None:
         match x:
-            case Zero():
+            case Const("Nat.Zero"):
                 return Truth()
             
-            case Succ():
+            case App(f=Const("Nat.Succ")):
                 return Contradiction()
     
     return {
-        "Bool.not": F(arity=1, func=__bool_not),
-        "Nat.add" : F(arity=2, func=__nat_add),
-        "Nat.isZero" : F(arity=1, func=__nat_iszero),
+        "Bool.not": F1(__bool_not),
+        "Nat.add" : F2(__nat_add),
+        "Nat.isZero" : F1(__nat_iszero),
     }
                 
 
@@ -154,37 +146,12 @@ def normalize(term : Term) -> Term:
                         
                         out = rule.func(*reversed([i.x for i in items]))
 
-                        return out if out is not None else App(f, x)
-
-                    case Contradiction():
-                        if len(items) != 2:
-                            # Either evaluating too early or too late
-                            return term
-                        
-                        # Return the "second" item
-                        return x
-
-                    case Truth():
-                        if len(items) != 2:
-                            # Either evaluating too early or too late
-                            return App(f, x)
-                        
-                        # Return the "first" item
-                        return cursor.x
+                        return normalize(out) if out is not None else App(f, x)
 
         case Const():
             return term
-        
-        case Succ():
-            return Succ(n=normalize(term.n))
-        
-        case Term():
-            return term
 
-        case Var():
-            return term
-        
-        case Zero():
+        case Term():
             return term
 
 # -----------------------------------------------------------------------------
@@ -216,8 +183,8 @@ if __name__ == "__main__":
     # 0 + x == x
     print(check(
         Eq(
-            lhs=App(f=App(f=Const("Nat.add"), x=Zero()), x=Var("x")),
-            rhs=Var("x")
+            lhs=App(f=App(f=Const("Nat.add"), x=Zero()), x=Const("x")),
+            rhs=Const("x")
         ),
         Refl(),
     ))
@@ -225,8 +192,8 @@ if __name__ == "__main__":
     # x + 0 == x
     print(check(
         Eq(
-            lhs=App(f=App(f=Const("Nat.add"), x=Var("x")), x=Zero()),
-            rhs=Var("x")
+            lhs=App(f=App(f=Const("Nat.add"), x=Const("x")), x=Zero()),
+            rhs=Const("x")
         ),
         Refl(),
     ))