Create contains, eq and replace operations

checker/lib/basic.py

@@ -3,8 +3,11 @@
 """
 
 # from ..proof import Context, Proof
-from ..props import Eq, Or, Prop
-from ..terms import App, Const, A1, A2, L1, L2, L3, Lambda, Term, Var, register_known_const
+from ..props import Eq, Exists, Or, Prop
+from ..terms import (
+    App, Const, A1, A2, L1, L2, L3, Lambda, Term,
+    register_known_const, register_known_norm
+)
 
 # -----------------------------------------------------------------------------
 # Identity function
@@ -59,8 +62,35 @@ def kernel_from_int(n : int) -> Term:
 
     return t
 
-# def is_nat(x : Term) -> Prop:
-#     return Or(
-#         Eq(x=x, y=zero),
-#         Eq(bool_f, bool_t) # TODO: Construct x = Succ n where isNat(n),
-#     )
+def is_nat(x : Term) -> Prop:
+    return Or(
+        Eq(x=x, y=zero),
+        Exists(lambda n : Eq(x=x, y=A1(Const("Nat.Succ"), n))),
+    )
+
+def __nat_add(t : Term) -> Term:
+    match t:
+        case App(f=Const("Nat.add"), x=Const("Nat.Zero")):
+            return id_func
+    
+        case App(f=Const("Nat.add"), x=App(f=Const("Nat.Succ"), x=a)):
+            return L1(lambda b : A1(succ, A2(Const("Nat.add"), a, b)))
+    
+        case _:
+            return t
+register_known_norm(__nat_add)
+
+def __nat_leq(t : Term) -> Term:
+    match t:
+        case App(f=Const("Nat.leq"), x=Const("Nat.Zero")):
+            return bool_t
+        
+        case App(App(f=Const("Nat.leq"), x=_), x=Const("Nat.Zero")):
+            return bool_f
+
+        case App(f=App(f=Const("Nat.leq"), x=App(f=Const("Nat.Succ"), x=a)), x=App(f=Const("Nat.Succ"), x=b)):
+            return A2(Const("Nat.leq"), a, b)
+        
+        case _:
+            return t
+register_known_norm(__nat_leq)

checker/props.py

@@ -3,6 +3,7 @@
 """
 
 from __future__ import annotations
+from typing import Callable
 
 from .terms import Term
 from dataclasses import dataclass
@@ -65,6 +66,23 @@ class Eq(Prop):
     def as_proof(self) -> list[list[tuple[list[Prop], Prop]]]:
         return super().as_proof()
 
+@dataclass(frozen=True)
+class Exists(Prop):
+    """
+        Create a statement that demonstrates there exists an x such that the
+        given statement is true.
+    """
+
+    x : Callable[[Term], Prop]
+
+@dataclass(frozen=True)
+class ForAll(Prop):
+    """
+        Create a statement that is true for all x
+    """
+
+    x : Callable[[Term], Prop]
+
 @dataclass(frozen=True)
 class Implies(Prop):
     """

checker/terms.py

@@ -4,7 +4,7 @@
 """
 
 from __future__ import annotations
-from typing import Callable
+from typing import Callable, Generator
 
 import copy
 
@@ -24,6 +24,24 @@ USABLE_VAR_NAMES = [
     'μ', 'ν', 'ξ', 'ο', 'π', 'ρ', 'σ', 'τ', 'υ', 'φ', 'χ', 'ψ', 'ω'
 ]
 
+def contains(haystack : Term, needle : Term) -> bool:
+    """
+        Determine whether a given small term value is contained in a bigger
+        term.
+
+        :param haystack: The term to search through.
+        :type haystack: Term
+        :param needle: The term to find.
+        :type needle: Term
+        :return: Whether the needle was found in the haystack.
+        :rtype: bool
+    """
+    for term in haystack.rec_iter():
+        if term == needle:
+            return True
+    else:
+        return False
+
 def normalize(term : Term) -> Term:
     """
         Create a normalization function. This function simplifies functions as
@@ -78,6 +96,21 @@ def std_norm_iter(term : Term) -> Term:
             return term
 _known_norms.append(std_norm_iter)
 
+def replace(term : Term, old : Term, new : Term) -> Term:
+    """
+        Find and replace occurrences of a sub-term in a given term.
+
+        :param term: The original term to update.
+        :type term: Term
+        :param old: The term to find and replace.
+        :type old: Term
+        :param new: The new term to replace the old one with.
+        :type new: Term
+        :return: The replaced term result.
+        :rtype: Term
+    """
+    return traverse_bottom_up(f=lambda t : new if t == old else t, term=term)
+
 def traverse(f : Callable[[Term], Term], term : Term) -> Term:
     """
         Traverse through the tree back-and-forth, aiming to run the given
@@ -96,7 +129,7 @@ def traverse(f : Callable[[Term], Term], term : Term) -> Term:
     a, b = Term(), term
 
     while a != b:
-        a, b = b, traverse_bottom_up(f=f, term=traverse_top_down(f=f, term=term))
+        a, b = b, traverse_bottom_up(f=f, term=traverse_top_down(f=f, term=b))
     
     return b
 
@@ -171,12 +204,6 @@ class Term:
         Base class for all terms.
     """
 
-    def __eq__(self, other) -> bool:
-        """
-            Determine whether two terms are equal.
-        """
-        return str(self) == str(other)
-
     def __repr__(self) -> str:
         """
             Create a representation of a term.
@@ -186,6 +213,12 @@ class Term:
     def normalize(self) -> Term:
         return normalize(term=self)
     
+    def replace(self, old : Term, new : Term) -> Term:
+        return replace(term=self, old=old, new=new)
+    
+    def rec_iter(self) -> Generator[Term, None, None]:
+        yield self
+
     def to_str(self, vars : dict[str, Var]) -> str:
         return "<undefined>"
 
@@ -205,6 +238,11 @@ class App(Term):
         """
         return self.to_str(vars={})
     
+    def rec_iter(self) -> Generator[Term, None, None]:
+        yield self
+        yield from self.f.rec_iter()
+        yield from self.x.rec_iter()
+
     def to_str(self, vars: dict[str, Var]) -> str:
         f_str = self.f.to_str(vars=vars)
         x_str = self.x.to_str(vars=vars)
@@ -246,6 +284,18 @@ class Lambda(Term):
     out : Term
     var : Var
 
+    def __eq__(self, value: object) -> bool:
+        if not isinstance(value, Lambda):
+            return False
+        
+        for c in USABLE_VAR_NAMES:
+            if not contains(self.out, Const(c)):
+                return self.substitute(Const(c)) == value.substitute((Const(c)))
+        else:
+            raise ValueError(
+                "Ran out of usable variables for comparing lambda structures"
+            )
+
     def __init__(self, f : Callable[[Var], Term]) -> None:
         self.var = Var()
         self.out = f(self.var)
@@ -256,6 +306,10 @@ class Lambda(Term):
         """
         return self.to_str(vars={})
     
+    def rec_iter(self) -> Generator[Term, None, None]:
+        yield self
+        yield from self.out.rec_iter()
+    
     def replace_content(self, term : Term) -> Lambda:
         """
             Replace the content of the lambda function with the given term.
@@ -427,3 +481,15 @@ if __name__ == "__main__":
     g = L1(lambda b : A2(b, bool_f, bool_t))
     print(g)
     print(g.normalize())
+
+    print("\nFIND & REPLACE")
+    print(30 * "=")
+
+    h = A3(Const("f"), Const("x"), Const("y"), Const("z"))
+    i = A3(Const("f"), Const("x"), Const("b"), Const("z")).replace(
+        old=Const("b"), new=Const("y"),
+    )
+
+    print(h)
+    print(i)
+    assert h == i

proof_checker.py

@@ -1,5 +1,6 @@
 from checker import lib, proof, props
-from checker.terms import App, Const
+from checker.terms import A2, App, Const
+from checker.lib.basic import kernel_from_int
 
 # Prove : true == not false
 p = proof.reflexivity(
@@ -18,3 +19,11 @@ p = proof.reflexivity(
     )
 )
 p.check()
+
+# Prove : 4 + 1 == 2 + 3
+p = proof.reflexivity(
+    props.Eq(
+        x=A2(Const("Nat.add"), kernel_from_int(4), kernel_from_int(1)),
+        y=A2(Const("Nat.add"), kernel_from_int(2), kernel_from_int(3)),
+    )
+)