proof.py

@@ -15,38 +15,6 @@ class App(Term):
     f : Term
     x : Term
 
-    def __repr__(self):
-        match self.f:
-            case App(f=Const("Nat.add"), x=a):
-                return f"{a} + {self.x}"
-            case App(f=Const("List.cons"), x=a):
-                return f"{a} :: {self.x}"
-            case Const("Nat.Succ"):
-                cursor, i = self, 0
-
-                while True:
-                    match cursor:
-                        case App(f=Const("Nat.Succ")):
-                            cursor = cursor.x
-                            i += 1
-                        case Const("Nat.Zero"):
-                            return str(i)
-                        case _:
-                            xs = str(cursor)
-                            if " " in xs:
-                                xs = "(" + xs + ")"
-                            return "{xs} + {i}"
-            case _:
-                fs = str(self.f)
-                xs = str(self.x)
-
-                if " " in fs:
-                    fs = "(" + fs + ")"
-                if " " in xs:
-                    xs = "(" + xs + ")"
-                
-                return f"{fs} xs"
-
 A0 = lambda fn : Const(fn)
 A1 = lambda fn, a : App(f=A0(fn), x=a)
 A2 = lambda fn, a, b : App(f=A1(fn, a), x=b)
@@ -61,15 +29,6 @@ A8 = lambda fn, a, b, c, d, e, f, g, h : App(f=A7(fn, a, b, c, d, e, f, g), x=h)
 class Const(Term):
     name : str
 
-    def __repr__(self) -> str:
-        match self.name:
-            case "List.Nil":
-                return "[]"
-            case "Nat.Zero":
-                return "0"
-            case _:
-                return self.name
-
 # --- Bool constructors ---
 
 def Truth() -> Term:
@@ -109,84 +68,21 @@ def kernel_from_int(n : int) -> Term:
 class Prop:
     pass
 
-@dataclass(frozen=True)
-class Contradict(Prop):
-    s : str
-
 @dataclass(frozen=True)
 class Eq(Prop):
     lhs : Term
     rhs : Term
 
-@dataclass(frozen=True)
-class Trivial(Prop):
-    pass
-    # def __repr__(self) -> str:
-    #     return "<trivial>"
-
 # -----------------------------------------------------------------------------
 # Proofs
 # -----------------------------------------------------------------------------
 
 class Proof:
-    def apply(self, goal : Prop, ctx : Context) -> Prop:
+    pass
-        return (
-            Contradict("Cannot prove using the base class")
-        )
-
-@dataclass(frozen=True)
-class Assumption(Proof):
-    def apply(self, goal : Prop, ctx : Context) -> Prop:
-        return (
-            Trivial() if goal in ctx.props else
-            Contradict(f"Couldn't find proposition `{goal}` in assumptions")
-        )
-
 
 @dataclass(frozen=True)
 class Refl(Proof):
-    def apply(self, goal : Prop, ctx : Context) -> Prop:
+    pass
-        match goal:
-            case Eq():
-                l = normalize(goal.lhs)
-                r = normalize(goal.rhs)
-
-                if l == r:
-                    return Trivial()
-                else:
-                    # Reduce to differing parts
-                    while True:
-                        match ( l, r ):
-                            case ( App(), App() ):
-                                if l.x == r.x:
-                                    l, r = l.f, r.f
-                                elif l.f == r.f:
-                                    l, r = l.x, r.x
-                                else:
-                                    break
-                            case _:
-                                break
-
-                    return Contradict(
-                        f"Couldn't normalize {goal.lhs} = {goal.rhs} any further than to {l} = {r}"
-                    )
-            
-            case Prop():
-                return Contradict(
-                    "Cannot prove base proposition"
-                )
-
-# -----------------------------------------------------------------------------
-# Context
-# -----------------------------------------------------------------------------
-# The context is a set of information you already know.
-
-@dataclass(frozen=True)
-class Context:
-    props : list[Prop]
-
-    def with_prop(self, prop : Prop):
-        return Context([ p for p in self.props ] + [ prop ])
 
 # -----------------------------------------------------------------------------
 # Normalization function
@@ -210,29 +106,18 @@ def apply_rules() -> dict[str, F]:
             case Const("Bool.Contradiction"):
                 return Truth()
     
-    def __list_isempty(x : Term) -> Term | None:
-        match x:
-            case Const("List.Nil"):
-                return Truth()
-        
-            case App(f=App(f=Const("List.Cons"))):
-                return Contradiction()
-    
-    def __list_length(x : Term) -> Term | None:
-        match x:
-            case Const("List.Nil"):
-                return Zero()
-            
-            case App(f=App(f=Const("List.Cons"), x=head), x=tail):
-                return Succ(A1("List.length", tail))
-
     def __nat_add(x : Term, y : Term) -> Term | None:
         match x:
             case Const("Nat.Zero"):
                 return y
             
             case App(f=Const("Nat.Succ"), x=x_):
-                return Succ(A2("Nat.add", x_, y))
+                return Succ(
+                    App(
+                        f=App(Const("Nat.add"), x_),
+                        x=y,
+                    )
+                )
     
     def __nat_iszero(x : Term) -> Term | None:
         match x:
@@ -244,12 +129,11 @@ def apply_rules() -> dict[str, F]:
     
     return {
         "Bool.not": F1(__bool_not),
-        "List.isEmpty": F1(__list_isempty),
-        "List.length": F1(__list_length),
         "Nat.add" : F2(__nat_add),
         "Nat.isZero" : F1(__nat_iszero),
     }
                 
+
 def normalize(term : Term) -> Term:
     match term:
         case App():
@@ -292,18 +176,13 @@ def normalize(term : Term) -> Term:
 # Proof checker
 # -----------------------------------------------------------------------------
 
-ProofCheck = Union["Proven", "ProveFailure"]
+def check(goal: Prop, proof : Proof) -> bool:
+    match ( goal, proof ):
+        case ( Eq(), Refl() ):
+            return normalize(goal.lhs) == normalize(goal.rhs)
     
-@dataclass(frozen=True)
+        case _:
-class Proven:
+            return False
-    pass
-
-@dataclass(frozen=True)
-class ProveFailure:
-    s : str
-
-def check(goal: Prop, proof : Proof, ctx : Context) -> Prop:
-    return proof.apply(goal, ctx)
 
 # -----------------------------------------------------------------------------
 # -----------------------------------------------------------------------------
@@ -317,17 +196,6 @@ if __name__ == "__main__":
             rhs=kernel_from_int(5),
         ),
         Refl(),
-        Context(props=[]),
-    ))
-
-    # 2 + 3 == 7
-    print(check(
-        Eq(
-            lhs=A2("Nat.add", kernel_from_int(2), kernel_from_int(3)),
-            rhs=kernel_from_int(7),
-        ),
-        Refl(),
-        Context(props=[]),
     ))
 
     # 0 + x == x
@@ -337,7 +205,6 @@ if __name__ == "__main__":
             rhs=Const("x")
         ),
         Refl(),
-        Context(props=[]),
     ))
 
     # x + 0 == x
@@ -347,5 +214,4 @@ if __name__ == "__main__":
             rhs=Const("x")
         ),
         Refl(),
-        Context(props=[]),
     ))