checker/proof.py

@@ -3,12 +3,10 @@
 """
 
 from __future__ import annotations
-from typing import Callable
 
 from dataclasses import dataclass
 from .context import Context
-from .props import And, Eq, Exists, ForAll, Or, Prop
+from .props import And, Eq, Or, Prop
-from .terms import Const, Term
 
 class ProofCheckerFailedException(Exception):
     pass
@@ -22,26 +20,14 @@ class Proof:
     context : Context
     statement : Prop
 
-    def __repr__(self) -> str:
+    def check(self) -> None:
-        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."
@@ -121,105 +107,6 @@ 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.
@@ -343,7 +230,7 @@ def reflexivity(eq : Eq) -> Proof:
             demonstrate that the two sides are equal.
     """
     l = eq.x.normalize()
-    r = eq.y.normalize()
+    r = eq.x.normalize()
 
     if l == r:
         return Proof(

checker/props.py

@@ -5,7 +5,7 @@
 from __future__ import annotations
 from typing import Callable
 
-from .terms import USABLE_VAR_NAMES, Const, Term, Var, ecsl
+from .terms import Term
 from dataclasses import dataclass
 
 class Prop:
@@ -15,88 +15,42 @@ class Prop:
         proposition.
     """
 
-    def __repr__(self) -> str:
+    def as_assumption(self, goal : Prop) -> list[list[tuple[list[Prop], Prop]]]:
         """
-            Create a representation of a proposition.
+            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.
 
-            :return: String representation of the proposition.
+            :return: Tuples of added assumptions with a new goal.
-            :rtype: str
+            :rtype: list[list[tuple[list[Prop], Prop]]]
         """
-        return self.to_str(vars=set())
+        return []
 
-    def contains(self, term : Term) -> bool:
+    def as_proof(self) -> list[list[tuple[list[Prop], Prop]]]:
         """
-            Determine whether a given term, value or variable is contained or
+            Determine which hypotheses are required in the context to prove
-            described by this proposition.
+            this proposition.
 
-            :param term: The term to look for.
+            The function returns a list of various methods to prove the
-            :type term: Term
+            proposition. If any of the methods is an empty list, it means
-            :return: Whether the term is contained in this proposition.
+            the proposition requires no assumptions and can instead be
-            :rtype: bool
+            computed.
-        """
-        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.
+            :return: Methods to prove this proposition.
-            :type old: Term
+            :rtype: list[tuple[list[Prop], Prop]]
-            :param new: The term to replace it with.
-            :type new: Term
-            :return: The proposition with the term replaced.
-            :rtype: Prop
         """
-        return self
+        return []
-
-    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):
     """
@@ -106,34 +60,11 @@ class Eq(Prop):
     x : Term
     y : Term
 
-    def __repr__(self) -> str:
+    def as_assumption(self, goal: Prop) -> list[list[tuple[list[Prop], Prop]]]:
-        """
+        return []
-            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 normalize(self) -> Prop:
+    def as_proof(self) -> list[list[tuple[list[Prop], Prop]]]:
-        """
+        return super().as_proof()
-            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):
@@ -144,69 +75,6 @@ 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):
     """
@@ -215,69 +83,6 @@ 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):
     """
@@ -287,35 +92,6 @@ 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):
     """
@@ -324,33 +100,5 @@ 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}"
 

checker/terms.py

@@ -42,38 +42,6 @@ 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
@@ -242,17 +210,6 @@ 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)
     
@@ -263,7 +220,7 @@ class Term:
         yield self
 
     def to_str(self, vars : dict[str, Var]) -> str:
-        return "<undefined term>"
+        return "<undefined>"
 
 @dataclass(frozen=True)
 class App(Term):
@@ -287,24 +244,10 @@ 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 + " " + ecsl(x_str)
+        return f_str + " " + (f"({x_str})" if " " in x_str else x_str)
 
 A1 = lambda fn, a : App(f=fn, x=a)
 A2 = lambda fn, a, b : App(f=A1(fn, a), x=b)
@@ -331,8 +274,6 @@ 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):
@@ -416,7 +357,7 @@ class Lambda(Term):
         s = self.out.to_str(vars=vars)
 
         del vars[char]
-        return "λ" + char + "." + ecsl(s)
+        return "λ" + char + "." + (f"({s})" if " " in s else s)
 
 L1 = lambda f : Lambda(lambda x : f(x))
 L2 = lambda f : Lambda(lambda x : L1(lambda y : f(x, y)))
@@ -457,13 +398,10 @@ 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)
@@ -526,12 +464,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())

proof_checker.py

@@ -1,7 +1,6 @@
 from checker import lib, proof, props
-from checker.terms import A1, A2, App, Const
+from checker.terms import A2, App, Const
 from checker.lib.basic import kernel_from_int
-from checker.props import Eq
 
 # Prove : true == not false
 p = proof.reflexivity(
@@ -10,7 +9,7 @@ p = proof.reflexivity(
         y=App(f=Const("Bool.not"), x=Const("Bool.False"))
     )
 )
-p.check(to_stdout=True)
+p.check()
 
 # Prove : false == not true
 p = proof.reflexivity(
@@ -19,7 +18,7 @@ p = proof.reflexivity(
         y=App(f=Const("Bool.not"), x=Const("Bool.True"))
     )
 )
-p.check(to_stdout=True)
+p.check()
 
 # Prove : 4 + 1 == 2 + 3
 p = proof.reflexivity(
@@ -28,59 +27,3 @@ 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)