Improve proof readability

proof.py

@@ -15,6 +15,38 @@ 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)
@@ -29,6 +61,15 @@ 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:
@@ -68,21 +109,84 @@ 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:
-    pass
+    def apply(self, goal : Prop, ctx : Context) -> Prop:
+        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):
-    pass
+    def apply(self, goal : Prop, ctx : Context) -> Prop:
+        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
@@ -106,18 +210,29 @@ 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(
+                return Succ(A2("Nat.add", x_, y))
-                    App(
-                        f=App(Const("Nat.add"), x_),
-                        x=y,
-                    )
-                )
 
     def __nat_iszero(x : Term) -> Term | None:
         match x:
@@ -129,11 +244,12 @@ 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():
@@ -176,13 +292,18 @@ def normalize(term : Term) -> Term:
 # Proof checker
 # -----------------------------------------------------------------------------
 
-def check(goal: Prop, proof : Proof) -> bool:
+ProofCheck = Union["Proven", "ProveFailure"]
-    match ( goal, proof ):
-        case ( Eq(), Refl() ):
-            return normalize(goal.lhs) == normalize(goal.rhs)
 
-        case _:
+@dataclass(frozen=True)
-            return False
+class Proven:
+    pass
+
+@dataclass(frozen=True)
+class ProveFailure:
+    s : str
+
+def check(goal: Prop, proof : Proof, ctx : Context) -> Prop:
+    return proof.apply(goal, ctx)
 
 # -----------------------------------------------------------------------------
 # -----------------------------------------------------------------------------
@@ -196,6 +317,17 @@ 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
@@ -205,6 +337,7 @@ if __name__ == "__main__":
             rhs=Const("x")
         ),
         Refl(),
+        Context(props=[]),
     ))
 
     # x + 0 == x
@@ -214,4 +347,5 @@ if __name__ == "__main__":
             rhs=Const("x")
         ),
         Refl(),
+        Context(props=[]),
     ))