From ea47c3430845908e7f5b145d03b9fff6bcf98562 Mon Sep 17 00:00:00 2001
From: Bram van den Heuvel <bram.vdh1999@gmail.com>
Date: Mon, 13 Jul 2026 16:48:56 +0200
Subject: [PATCH] Create initial proof builder POC

---
 checker/proof.py | 121 ++++++++++++++++++-
 checker/props.py | 304 +++++++++++++++++++++++++++++++++++++++++++----
 checker/terms.py |  74 +++++++++++-
 proof_checker.py |  63 +++++++++-
 4 files changed, 523 insertions(+), 39 deletions(-)

diff --git a/checker/proof.py b/checker/proof.py
index 251c805..c743d9e 100644
--- a/checker/proof.py
+++ b/checker/proof.py
@@ -3,10 +3,12 @@
 """
 
 from __future__ import annotations
+from typing import Callable
 
 from dataclasses import dataclass
 from .context import Context
-from .props import And, Eq, Or, Prop
+from .props import And, Eq, Exists, ForAll, Or, Prop
+from .terms import Const, Term
 
 class ProofCheckerFailedException(Exception):
     pass
@@ -20,14 +22,26 @@ class Proof:
     context : Context
     statement : Prop
 
-    def check(self) -> None:
+    def __repr__(self) -> str:
+        return (
+            # "Γ" +
+            ", ".join([ str(p) for p in self.context.props]) +
+            " ⊢ " +
+            str(self.statement)
+        )
+
+    def check(self, is_lemma : bool = False, to_stdout : bool = False) -> None:
         """
             Check whether the proof is self-sufficient. That is, the proof
             relies on zero context in order to be considered true.
         """
         if self.context.isempty():
+            if to_stdout:
+                print(f"Successfully proved that {self}")
             return
-        
+        elif is_lemma:
+            if to_stdout:
+                print(f"Proved lemma: {self}")
         else:
             raise ProofCheckerFailedException(
                 f"Proof still relies on {len(self.context.props)} assumptions."
@@ -107,6 +121,105 @@ def assume(statement : Prop) -> Proof:
         statement=statement,
     )
 
+def eq_l(proof : Proof, eq : Eq, statement : Prop) -> Proof:
+    """
+        Use an equality to the left of the statement to substitute values.
+
+        $$
+            Γ ⊢ P[y]
+        -----------------
+         Γ, x = y ⊢ P[x]
+        $$
+
+        :param proof: The proof supporting the claim.
+        :type proof: Proof
+        :param eq: The equality, where the statement on the left is meant to be
+            replaced by the statement on the right.
+        :type eq: Eq
+        :param statement: The final statement that one should end up at.
+        :type statement: Prop
+    """
+    if proof.statement.normalize() != statement.normalize().replace(old=eq.x, new=eq.y).normalize():
+        raise ProofCheckerFailedException(
+            f"Failed to arrive at {proof.statement} "
+            f"when substituting {eq} into {statement}"
+        )
+    
+    return Proof(
+        context=proof.context.with_prop(eq),
+        statement=statement,
+    )
+
+def forall_l(proof : Proof, statement : Callable[[Term], Prop], term : Term) -> Proof:
+    """
+        Generalize a hypothesis by making a term more generalized.
+
+        $$
+         Γ, P[x] ⊢ Q
+        --------------
+         Γ, ∀x.P ⊢ Q
+        $$
+
+        :param proof: The proof with the hypothesis to generalize.
+        :type proof: Proof
+        :param statement: The statement to generalize.
+        :type statement: Callable[[Term], Proof]
+        :param term: The term to substitute.
+        :type term: Term
+        :return: The generalized proof.
+        :rtype: Proof
+    """
+    s = statement(term)
+
+    # TODO: Return new proof
+    return proof
+
+def forall_r(proof : Proof, statement : Callable[[Term], Prop], free_var_name : str) -> Proof:
+    """
+        Generalize a proof for all instances of a given value.
+
+        $$
+             Γ ⊢ P[x]
+        -----------------
+         Γ ⊢ \forall x.P
+        $$
+
+        :param proof: The proof to generalize.
+        :type proof: Proof
+        :param statement: The forall-statement.
+        :type statement: Callable[[Term], Prop]
+        :param free_var_name: The free variable that can be generalized.
+        :type free_var_name: str
+        :return: The generalized proof.
+        :rtype: Proof
+    """
+    fv = Const(free_var_name)
+    nfv = Const("not_" + free_var_name)
+
+    # Make sure the free variable isn't bound within the statement
+    s = statement(nfv)
+    if s.contains(fv):
+        raise ProofCheckerFailedException(
+            f"Some occurrences of {free_var_name} were found to not be "
+            f"substituted in {s}"
+        )
+    
+    # Make sure the free variable doesn't appear in the context
+    s = statement(fv)
+    for p in proof.context.props:
+        if p.contains(fv):
+            raise ProofCheckerFailedException(
+                f"Free variable {fv} was found in context hypothesis: {p}"
+            )
+    
+    # Make sure the proof statement matches the statement with the free variable
+    if s != proof.statement:
+        raise ProofCheckerFailedException(
+            f"Expected proof to prove that {s}, found {proof.statement} instead."
+        )
+    
+    return Proof(context=proof.context, statement=Exists(statement))
+
 def from_assumption(ctx : Context, statement : Prop) -> Proof:
     """
         Gain a proof by including the statement in the assumptions.
@@ -230,7 +343,7 @@ def reflexivity(eq : Eq) -> Proof:
             demonstrate that the two sides are equal.
     """
     l = eq.x.normalize()
-    r = eq.x.normalize()
+    r = eq.y.normalize()
 
     if l == r:
         return Proof(
diff --git a/checker/props.py b/checker/props.py
index c6c4498..4ff430e 100644
--- a/checker/props.py
+++ b/checker/props.py
@@ -5,7 +5,7 @@
 from __future__ import annotations
 from typing import Callable
 
-from .terms import Term
+from .terms import USABLE_VAR_NAMES, Const, Term, Var, ecsl
 from dataclasses import dataclass
 
 class Prop:
@@ -15,42 +15,88 @@ class Prop:
         proposition.
     """
 
-    def as_assumption(self, goal : Prop) -> list[list[tuple[list[Prop], Prop]]]:
+    def __repr__(self) -> str:
         """
-            Propositions can simplify the proof by creating simpler theorems
-            and sub-lemmas to prove instead. If this proposition is part of
-            the assumptions, this function helps transform the goal into
-            simpler sub-goals.
+            Create a representation of a proposition.
 
-            :return: Tuples of added assumptions with a new goal.
-            :rtype: list[list[tuple[list[Prop], Prop]]]
+            :return: String representation of the proposition.
+            :rtype: str
         """
-        return []
+        return self.to_str(vars=set())
 
-    def as_proof(self) -> list[list[tuple[list[Prop], Prop]]]:
+    def contains(self, term : Term) -> bool:
         """
-            Determine which hypotheses are required in the context to prove
-            this proposition.
+            Determine whether a given term, value or variable is contained or
+            described by this proposition.
 
-            The function returns a list of various methods to prove the
-            proposition. If any of the methods is an empty list, it means
-            the proposition requires no assumptions and can instead be
-            computed.
-
-            :return: Methods to prove this proposition.
-            :rtype: list[tuple[list[Prop], Prop]]
+            :param term: The term to look for.
+            :type term: Term
+            :return: Whether the term is contained in this proposition.
+            :rtype: bool
         """
-        return []
+        return False
+    
+    def normalize(self) -> Prop:
+        """
+            Simplify the terms of a proposition.
+        """
+        return self
+    
+    def replace(self, old : Term, new : Term) -> Prop:
+        """
+            Find any occurrence of a given term, and replace it with the new
+            term.
+
+            :param old: The term to replace.
+            :type old: Term
+            :param new: The term to replace it with.
+            :type new: Term
+            :return: The proposition with the term replaced.
+            :rtype: Prop
+        """
+        return self
+
+    def to_str(self, vars : set[str]) -> str:
+        return "<undefined prop>"
 
 @dataclass(frozen=True)
 class And(Prop):
     """
-        The logical and-operator `P ^ Q`.
+        The logical and-operator `P ∧ Q`.
     """
 
     P : Prop
     Q : Prop
 
+    def __repr__(self) -> str:
+        """
+            Create a representation of a proposition.
+
+            :return: String representation of the proposition.
+            :rtype: str
+        """
+        return self.to_str(vars=set())
+
+    def contains(self, term: Term) -> bool:
+        return self.P.contains(term) or self.Q.contains(term)
+    
+    def normalize(self) -> Prop:
+        """
+            Simplify the terms of a proposition.
+        """
+        return And(P=self.P.normalize(), Q=self.Q.normalize())
+    
+    def replace(self, old: Term, new: Term) -> Prop:
+        return And(
+            P=self.P.replace(old=old, new=new),
+            Q=self.Q.replace(old=old, new=new),
+        )
+    
+    def to_str(self, vars: set[str]) -> str:
+        p_str = ecsl(self.P.to_str(vars=vars))
+        q_str = ecsl(self.Q.to_str(vars=vars))
+        return f"{p_str} ∧ {q_str}"
+
 @dataclass(frozen=True)
 class Eq(Prop):
     """
@@ -60,11 +106,34 @@ class Eq(Prop):
     x : Term
     y : Term
 
-    def as_assumption(self, goal: Prop) -> list[list[tuple[list[Prop], Prop]]]:
-        return []
+    def __repr__(self) -> str:
+        """
+            Create a representation of a proposition.
+
+            :return: String representation of the proposition.
+            :rtype: str
+        """
+        return self.to_str(vars=set())
+
+    def contains(self, term: Term) -> bool:
+        return self.x.contains(term) or self.y.contains(term)
     
-    def as_proof(self) -> list[list[tuple[list[Prop], Prop]]]:
-        return super().as_proof()
+    def normalize(self) -> Prop:
+        """
+            Simplify the terms of a proposition.
+        """
+        return Eq(x=self.x.normalize(), y=self.y.normalize())
+    
+    def replace(self, old: Term, new: Term) -> Prop:
+        return Eq(
+            x=self.x.replace(old=old, new=new),
+            y=self.y.replace(old=old, new=new),
+        )
+
+    def to_str(self, vars : set[str]) -> str:
+        x_str = ecsl(self.x.to_str(vars={ key : Var() for key in vars }))
+        y_str = ecsl(self.y.to_str(vars={ key : Var() for key in vars }))
+        return f"{x_str} = {y_str}"
 
 @dataclass(frozen=True)
 class Exists(Prop):
@@ -75,6 +144,69 @@ class Exists(Prop):
 
     x : Callable[[Term], Prop]
 
+    def __repr__(self) -> str:
+        """
+            Create a representation of a proposition.
+
+            :return: String representation of the proposition.
+            :rtype: str
+        """
+        return self.to_str(vars=set())
+
+    def contains(self, term : Term) -> bool:
+        i, c = 0, Const("")
+
+        while i == 0 or term.contains(c):
+            i += 1
+            c = Const("temp_exists_variable_{i}")
+
+        return self.x(c).contains(term=term)
+    
+    def normalize(self) -> Prop:
+        """
+            Simplify the terms of a proposition.
+        """
+        return Exists(lambda n : self.x(n).normalize())
+    
+    def replace(self, old: Term, new: Term) -> Prop:
+        def replaced_func(input_term : Term) -> Prop:
+            c = unique_const(input_term=input_term)
+            return (
+                self.x(c)
+                    .replace(old=old, new=new)
+                    .replace(old=c, new=input_term)
+            )
+        
+        def unique_const(input_term : Term) -> Term:
+            """
+                Get a unique const value that doesn't interfere with either the
+                old term that needs to be replaced, nor with the input term. 
+            """
+            i, c = 0, Const("")
+
+            while i == 0 or input_term.contains(c) or old.contains(c):
+                i += 1
+                c = Const(f"temp_unique_value_{i}")
+            
+            return c
+
+        return Exists(replaced_func)
+    
+    def to_str(self, vars : set[str]) -> str:
+        for c in USABLE_VAR_NAMES:
+            if c in vars:
+                continue
+            
+            vars.add(c)
+            s = self.x(Const(c)).to_str(vars=vars)
+            vars.remove(c)
+
+            return "∃" + c + "." + ecsl(s)
+        else:
+            raise ValueError(
+                "Ran out of usable var names!"
+            )
+
 @dataclass(frozen=True)
 class ForAll(Prop):
     """
@@ -83,6 +215,69 @@ class ForAll(Prop):
 
     x : Callable[[Term], Prop]
 
+    def __repr__(self) -> str:
+        """
+            Create a representation of a proposition.
+
+            :return: String representation of the proposition.
+            :rtype: str
+        """
+        return self.to_str(vars=set())
+
+    def contains(self, term : Term) -> bool:
+        i, c = 0, Const("")
+
+        while i == 0 or term.contains(c):
+            i += 1
+            c = Const("temp_forall_variable_{i}")
+
+        return self.x(c).contains(term=term)
+    
+    def normalize(self) -> Prop:
+        """
+            Simplify the terms of a proposition.
+        """
+        return ForAll(lambda n : self.x(n).normalize())
+    
+    def replace(self, old: Term, new: Term) -> Prop:
+        def replaced_func(input_term : Term) -> Prop:
+            c = unique_const(input_term=input_term)
+            return (
+                self.x(c)
+                    .replace(old=old, new=new)
+                    .replace(old=c, new=input_term)
+            )
+        
+        def unique_const(input_term : Term) -> Term:
+            """
+                Get a unique const value that doesn't interfere with either the
+                old term that needs to be replaced, nor with the input term. 
+            """
+            i, c = 0, Const("")
+
+            while i == 0 or input_term.contains(c) or old.contains(c):
+                i += 1
+                c = Const(f"temp_unique_value_{i}")
+            
+            return c
+
+        return ForAll(replaced_func)
+    
+    def to_str(self, vars : set[str]) -> str:
+        for c in USABLE_VAR_NAMES:
+            if c in vars:
+                continue
+            
+            vars.add(c)
+            s = self.x(Const(c)).to_str(vars=vars)
+            vars.remove(c)
+
+            return "∀" + c + "." + ecsl(s)
+        else:
+            raise ValueError(
+                "Ran out of usable var names!"
+            )
+
 @dataclass(frozen=True)
 class Implies(Prop):
     """
@@ -92,6 +287,35 @@ class Implies(Prop):
     P : Prop
     Q : Prop
 
+    def __repr__(self) -> str:
+        """
+            Create a representation of a proposition.
+
+            :return: String representation of the proposition.
+            :rtype: str
+        """
+        return self.to_str(vars=set())
+
+    def contains(self, term: Term) -> bool:
+        return self.P.contains(term) or self.Q.contains(term)
+    
+    def normalize(self) -> Prop:
+        """
+            Simplify the terms of a proposition.
+        """
+        return Implies(P=self.P.normalize(), Q=self.Q.normalize())
+    
+    def replace(self, old: Term, new: Term) -> Prop:
+        return Implies(
+            P=self.P.replace(old=old, new=new),
+            Q=self.Q.replace(old=old, new=new),
+        )
+    
+    def to_str(self, vars: set[str]) -> str:
+        p_str = ecsl(self.P.to_str(vars=vars))
+        q_str = ecsl(self.Q.to_str(vars=vars))
+        return f"{p_str} → {q_str}"
+
 @dataclass(frozen=True)
 class Or(Prop):
     """
@@ -100,5 +324,33 @@ class Or(Prop):
 
     P : Prop
     Q : Prop
-    
+
+    def __repr__(self) -> str:
+        """
+            Create a representation of a proposition.
+
+            :return: String representation of the proposition.
+            :rtype: str
+        """
+        return self.to_str(vars=set())
+
+    def contains(self, term: Term) -> bool:
+        return self.P.contains(term) or self.Q.contains(term)
+    
+    def normalize(self) -> Prop:
+        """
+            Simplify the terms of a proposition.
+        """
+        return Or(P=self.P.normalize(), Q=self.Q.normalize())
+
+    def replace(self, old: Term, new: Term) -> Prop:
+        return Or(
+            P=self.P.replace(old=old, new=new),
+            Q=self.Q.replace(old=old, new=new),
+        )
+
+    def to_str(self, vars: set[str]) -> str:
+        p_str = ecsl(self.P.to_str(vars=vars))
+        q_str = ecsl(self.Q.to_str(vars=vars))
+        return f"{p_str} ∨ {q_str}"
 
diff --git a/checker/terms.py b/checker/terms.py
index cdab253..009e90b 100644
--- a/checker/terms.py
+++ b/checker/terms.py
@@ -42,6 +42,38 @@ def contains(haystack : Term, needle : Term) -> bool:
     else:
         return False
 
+def ecsl(s : str) -> str:
+    """
+        Encapsulate something if it contains non-encapsulated spaces.
+
+        :param s: The string to potentially encapsulate.
+        :type s: str
+        :return: An encapsulated string.
+        :rtype: str
+    """
+    def needs_encapsulation() -> bool:
+        if " " not in s:
+            return False
+
+        level = 0
+
+        for c in s:
+            match c:
+                case " ":
+                    if level <= 0:
+                        return True
+                case "(":
+                    level += 1
+                case ")":
+                    level -= 1
+        else:
+            return False
+    
+    if needs_encapsulation():
+        return "(" + s + ")"
+    else:
+        return s
+
 def normalize(term : Term) -> Term:
     """
         Create a normalization function. This function simplifies functions as
@@ -210,6 +242,17 @@ class Term:
         """
         return self.to_str(vars={})
     
+    def contains(self, needle : Term) -> bool:
+        """
+            Determine whether this term is or contains any given term.
+
+            :param needle: The term to look for.
+            :type needle: Term
+            :return: Whether the term is found.
+            :rtype: bool
+        """
+        return contains(haystack=self, needle=needle)
+    
     def normalize(self) -> Term:
         return normalize(term=self)
     
@@ -220,7 +263,7 @@ class Term:
         yield self
 
     def to_str(self, vars : dict[str, Var]) -> str:
-        return "<undefined>"
+        return "<undefined term>"
 
 @dataclass(frozen=True)
 class App(Term):
@@ -244,10 +287,24 @@ class App(Term):
         yield from self.x.rec_iter()
 
     def to_str(self, vars: dict[str, Var]) -> str:
+        # Reformat pre-defined common functions
+        match self:
+            case App(f=App(f=Const("Nat.add"), x=a), x=b):
+                return f"{ecsl(a.to_str(vars=vars))} + {ecsl(b.to_str(vars=vars))}"
+        
+        # Display numbers
+        n, c = 0, self
+        while isinstance(c, App) and c.f == Const("Nat.Succ"):
+            n, c = n + 1, c.x
+        if c == Const("Nat.Zero"):
+            return str(n)
+        # elif n > 0:
+        #     return f"{ecsl(c.to_str(vars=vars))} + {n}"
+
         f_str = self.f.to_str(vars=vars)
         x_str = self.x.to_str(vars=vars)
 
-        return f_str + " " + (f"({x_str})" if " " in x_str else x_str)
+        return f_str + " " + ecsl(x_str)
 
 A1 = lambda fn, a : App(f=fn, x=a)
 A2 = lambda fn, a, b : App(f=A1(fn, a), x=b)
@@ -274,6 +331,8 @@ class Const(Term):
         return self.to_str(vars={})
 
     def to_str(self, vars: dict[str, Var]) -> str:
+        if self.name == "Nat.Zero":
+            return "0"
         return self.name
 
 class Lambda(Term):
@@ -357,7 +416,7 @@ class Lambda(Term):
         s = self.out.to_str(vars=vars)
 
         del vars[char]
-        return "λ" + char + "." + (f"({s})" if " " in s else s)
+        return "λ" + char + "." + ecsl(s)
 
 L1 = lambda f : Lambda(lambda x : f(x))
 L2 = lambda f : Lambda(lambda x : L1(lambda y : f(x, y)))
@@ -398,10 +457,13 @@ if __name__ == "__main__":
     # x
     print(Const("x"))
 
+    # λx.x
+    print(Lambda(lambda a : a))
+
     # λx.(f x)
     print(Lambda(lambda a : App(f=Const("f"), x=a)))
 
-    # λx.(λy.(x y))
+    # λx.λy.(x y)
     print(Lambda(lambda b : Lambda(lambda c : App(f=b, x=c))))
 
     # Nat.Succ (Nat.Succ Nat.Zero)
@@ -464,12 +526,12 @@ if __name__ == "__main__":
     print("\nSHORTHAND NOTATION")
     print(30 * "=")
 
-    # λx.(λy.(λz.(x y z))
+    # λx.λy.λz.(x y z)
     e = L3(lambda a, b, c : App(f=App(f=a, x=b), x=c))
     print(e)
 
 
-    # λx.(λy.(λz.(x y z))
+    # λx.λy.λz.(x y z)
     f = L3(lambda a, b, c : A3(L3(lambda a, b, c : A2(a, b, c)), a, b, c))
     print(f)
     print(f.normalize())
diff --git a/proof_checker.py b/proof_checker.py
index 683110a..0b05fdb 100644
--- a/proof_checker.py
+++ b/proof_checker.py
@@ -1,6 +1,7 @@
 from checker import lib, proof, props
-from checker.terms import A2, App, Const
+from checker.terms import A1, A2, App, Const
 from checker.lib.basic import kernel_from_int
+from checker.props import Eq
 
 # Prove : true == not false
 p = proof.reflexivity(
@@ -9,7 +10,7 @@ p = proof.reflexivity(
         y=App(f=Const("Bool.not"), x=Const("Bool.False"))
     )
 )
-p.check()
+p.check(to_stdout=True)
 
 # Prove : false == not true
 p = proof.reflexivity(
@@ -18,7 +19,7 @@ p = proof.reflexivity(
         y=App(f=Const("Bool.not"), x=Const("Bool.True"))
     )
 )
-p.check()
+p.check(to_stdout=True)
 
 # Prove : 4 + 1 == 2 + 3
 p = proof.reflexivity(
@@ -27,3 +28,59 @@ p = proof.reflexivity(
         y=A2(Const("Nat.add"), kernel_from_int(2), kernel_from_int(3)),
     )
 )
+p.check(to_stdout=True)
+
+# Prove : 0 + x = x
+p = proof.reflexivity(
+    props.Eq(
+        x=A2(Const("Nat.add"), kernel_from_int(0), Const("x")),
+        y=Const("x"),
+    )
+)
+p.check(to_stdout=True)
+
+# Prove : x + 0 = x
+
+# # SHOULD RAISE EXCEPTION
+# p = proof.reflexivity(
+#     props.Eq(
+#         x=A2(Const("Nat.add"), Const("x"), kernel_from_int(0)),
+#         y=Const("x"),
+#     )
+# )
+# p.check(to_stdout=True)
+
+case_1 = proof.eq_l(
+    proof=proof.reflexivity(
+        Eq(
+            x = A2(Const("Nat.add"), Const("Nat.Zero"), Const("Nat.Zero")),
+            y = Const("Nat.Zero")
+        )
+    ),
+    eq=Eq(x=Const("x"), y=Const("Nat.Zero")),
+    statement=Eq(
+        x=A2(Const("Nat.add"), Const("x"), Const("Nat.Zero")),
+        y=Const("x")
+    ),
+)
+case_1.check(is_lemma=True, to_stdout=True)
+
+case_2 = proof.eq_l(
+    proof=proof.eq_l(
+        proof=proof.reflexivity(Eq(
+            x=A1(Const("Nat.Succ"), Const("n")),
+            y=A1(Const("Nat.Succ"), Const("n")),
+        )),
+        eq=Eq(x=A2(Const("Nat.add"), Const("n"), Const("Nat.Zero")), y=Const("n")),
+        statement=Eq(
+            x=A2(Const("Nat.add"), A1(Const("Nat.Succ"), Const("n")), Const("Nat.Zero")),
+            y=A1(Const("Nat.Succ"), Const("n")),
+        ),
+    ),
+    eq=Eq(x=Const("x"), y=A1(Const("Nat.Succ"), Const("n"))),
+    statement=Eq(
+        x=A2(Const("Nat.add"), Const("x"), Const("Nat.Zero")),
+        y=Const("x"),
+    ),
+)
+case_2.check(is_lemma=True, to_stdout=True)