Attempt to implement basic library

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):
     """

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)),
+    )
+)