Generalize normalize function

.gitignore

@@ -0,0 +1 @@
+__pycache__/

checker/__init__.py

@@ -0,0 +1,15 @@
+"""
+    This module hosts various elements that are necessary to create a proof
+    checker.
+"""
+
+from .props import And, Implies, Prop
+from .terms import Term, register_known_const
+
+__all__ = [
+    "And",
+    "Implies",
+    "Prop",
+    "Term",
+    "register_known_const",
+]

checker/context.py

@@ -0,0 +1,101 @@
+"""
+    The Context helps handle multiple hypotheses in a given proof context.
+"""
+
+from __future__ import annotations
+
+from .props import Prop
+from dataclasses import dataclass
+
+@dataclass(frozen=True)
+class Context:
+    """
+        Base Context that contains multiple assumptions for a given proof.
+    """
+
+    props : set[Prop]
+
+    def contains(self, prop : Prop) -> bool:
+        """
+            Determine whether a proposition is given in the context.
+
+            :param prop: The proposition to consider.
+            :type prop: Prop
+            :return: Whether the proposition is contained in the context.
+            :rtype: bool
+        """
+        return prop in self.props
+
+    @classmethod
+    def empty(cls):
+        return cls(props=set())
+    
+    def isempty(self) -> bool:
+        """
+            Determine whether the context is empty.
+        """
+        return len(self.props) == 0
+    
+    def issubseteq(self, other : Context) -> bool:
+        """
+            Determine whether this context is a subset of another context.
+
+            :param other: The potentially larger context.
+            :type other: Context
+            :return: Whether this context is a subset.
+            :rtype: bool
+        """
+        return self.props.issubset(other.props)
+    
+    def issuperseteq(self, other : Context) -> bool:
+        """
+            Determine whether this context has another context as its subset.
+
+            :param other: The potentially contained context.
+            :type other: Context
+            :return: Whether the context is a subset of this one.
+            :rtype: bool
+        """
+        return other.issubseteq(self)
+    
+    def union(self, other : Context) -> Context:
+        """
+            Create a context that contains the propositions of two contexts.
+
+            :param other: The other context.
+            :type other: Context
+            :return: A context containing the propositions of both contexts.
+            :type: Context
+        """
+        return Context(props=self.props.union(other.props))
+    
+    def with_prop(self, prop : Prop) -> Context:
+        """
+            Add a new proposition to the context.
+
+            :param prop: Proposition to add.
+            :type prop: Prop
+            :return: A context with the proposition included.
+            :rtype: Context
+        """
+        if prop in self.props:
+            return self
+        else:
+            new_props = [ p for p in self.props ]
+            new_props.append(prop)
+            return Context(props=set(new_props))
+
+    def without_prop(self, prop : Prop) -> Context:
+        """
+            Remove a proposition from the context, if it was present at all.
+
+            :param prop: Proposition to remove.
+            :type prop: Prop
+            :return: A context without the proposition.
+            :rtype: Context
+        """
+        if prop not in self.props:
+            return self
+        else:
+            new_props = [ p for p in self.props if p != prop ]
+            return Context(props=set(new_props))

checker/lib/__init__.py

@@ -0,0 +1,10 @@
+"""
+    The library contains basic functions and proofs that you might want to
+    rely on.
+"""
+
+from .basic import kernel_from_int
+
+__all__ = [
+    "kernel_from_int",
+]

checker/lib/basic.py

@@ -0,0 +1,66 @@
+"""
+    Library containing all the basic functions
+"""
+
+# 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
+
+# -----------------------------------------------------------------------------
+# Identity function
+# -----------------------------------------------------------------------------
+# Always returns its input.
+id_func = Lambda(lambda x : x)
+register_known_const("id", id_func)
+register_known_const("identity", id_func)
+
+# # -----------------------------------------------------------------------------
+# # Equality
+# # -----------------------------------------------------------------------------
+# equality = Lambda(Lambda(EqT(lhs=Var(1), rhs=Var(0))))
+
+# register_known_const("eq", equality)
+# register_known_const("==", equality)
+
+# -----------------------------------------------------------------------------
+# Bool
+# -----------------------------------------------------------------------------
+
+bool_t = L2(lambda x, y : x).normalize()
+bool_f = L2(lambda x, y : y).normalize()
+if_statement = L3(lambda x, y, z : A2(x, y, z)).normalize()
+not_statement = L1(lambda b : A2(b, bool_f, bool_t)).normalize()
+
+register_known_const("Bool.False", bool_f)
+register_known_const("Bool.True", bool_t)
+register_known_const("Bool.elim", if_statement)
+register_known_const("Bool.if", if_statement)
+register_known_const("Bool.not", not_statement)
+
+def is_bool(x : Term) -> Prop:
+    return Or(Eq(x=x, y=bool_f), Eq(x=x, y=bool_t))
+
+# -----------------------------------------------------------------------------
+# Nat
+# -----------------------------------------------------------------------------
+
+zero = Const("Nat.Zero")
+succ = Const("Nat.Succ")
+
+def kernel_from_int(n : int) -> Term:
+    if n < 0:
+        raise ValueError(
+            "Int is not Nat"
+        )
+
+    t = zero
+    for _ in range(n):
+        t = A1(succ, t)
+
+    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),
+#     )

checker/proof.py

@@ -0,0 +1,268 @@
+"""
+    The proofs module contains various methods to construct a proof.
+"""
+
+from __future__ import annotations
+
+from dataclasses import dataclass
+from .context import Context
+from .props import And, Eq, Or, Prop
+
+class ProofCheckerFailedException(Exception):
+    pass
+
+@dataclass(frozen=True)
+class Proof:
+    """
+        Base class to construct a proof.
+    """
+
+    context : Context
+    statement : Prop
+
+    def check(self) -> 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():
+            return
+        
+        else:
+            raise ProofCheckerFailedException(
+                f"Proof still relies on {len(self.context.props)} assumptions."
+            )
+
+def and_l(proof : Proof, a : Prop, b : Prop) -> Proof:
+    """
+        Create a proof that collects two hypotheses and collects them in a
+        logical AND proposition.
+
+        $$
+         Γ, A, B ⊢ C
+        --------------
+         Γ, A ∧ B ⊢ C
+        $$
+
+        :param proof: The original proof, including two statements to combine.
+        :type proof: Proof
+        :param a: The first proposition to combine.
+        :type a: Prop
+        :param b: The second proposition to combine.
+        :type b: Prop
+        :return: A proof that combines the two hypotheses in an AND proposition.
+        :rtype: Proof
+        :raises ProofCheckerFailedException: One of the two propositions was
+            not found in the context.
+    """
+    if not proof.context.contains(a):
+        raise ProofCheckerFailedException(
+            f"Could not find proposition {a} in the proof's context."
+        )
+    if not proof.context.contains(b):
+        raise ProofCheckerFailedException(
+            f"Could not find proposition {b} in the proof's context."
+        )
+    
+    return Proof(
+        context=proof.context.without_prop(a).without_prop(b).with_prop(And(a, b)),
+        statement=proof.statement,
+    )
+
+def and_r(proof1 : Proof, proof2 : Proof) -> Proof:
+    """
+        Create a proof that demonstrates that the statements of two proofs are
+        both true.
+
+        $$
+         Γ ⊢ A  Γ' ⊢ B
+        ---------------
+         Γ, Γ' ⊢ A ∧ B
+        $$
+
+        :param proof1: The first proof.
+        :type proof1: Proof
+        :param proof2: The second proof.
+        :type proof2: Proof
+        :return: A proof demonstrating that both proofs are true.
+        :rtype: Proof
+    """
+    return Proof(
+        context=proof1.context.union(proof2.context),
+        statement=And(proof1.statement, proof2.statement),
+    )
+
+def assume(statement : Prop) -> Proof:
+    """
+        Gain a tautological proof that proves a statement by assuming
+        it's true.
+
+        :param statement: A propositional statement to prove.
+        :type statement: Prop
+        :return: A tautological proof.
+        :rtype: Proof
+    """
+    return from_assumption(
+        ctx=Context.empty().with_prop(prop=statement),
+        statement=statement,
+    )
+
+def from_assumption(ctx : Context, statement : Prop) -> Proof:
+    """
+        Gain a proof by including the statement in the assumptions.
+        This is a trivial proof that one typically phrases as such:
+
+        $$
+        Γ, A  ⊢ A
+        $$
+
+        :param ctx: The proof's context.
+        :type ctx: Context
+        :param statement: The statement to prove.
+        :type statement: Prop
+        :raises ProofCheckerFailedException: The statement was not included
+            as an assumption in the context.
+    """
+    if not ctx.contains(statement):
+        raise ProofCheckerFailedException(
+            f"The statement {statement} was not included in the context."
+        )
+    
+    return Proof(context=ctx, statement=statement)
+
+def or_l(proof_a : Proof, proof_b : Proof, a : Prop, b : Prop) -> Proof:
+    """
+        Create a proof that builds a generalized OR-statement in the context.
+
+        $$
+         Γ, A ⊢ C   Γ, B ⊢ C
+        ----------------------
+             Γ, A ∨ B ⊢ C 
+        $$
+
+        :param proof_a: The first proof.
+        :type proof_a: Proof
+        :param proof_b: The second proof.
+        :type proof_b: Proof
+        :param a: The proposition from the first proof.
+        :type a: Prop
+        :param b: The proposition from the second proof.
+        :type b: Prop
+        :return: A proof demonstrating a statement given that either proposition
+            a or b is true.
+        :rtype: Proof
+    """
+    statement = proof_a.statement
+
+    if statement != proof_b.statement:
+        raise ProofCheckerFailedException(
+            "For proof constructor `or_l`, the statements of the two proofs "
+            "must match: {proof_a.statement} and {proof_b.statement} do not "
+            "match."
+        )
+    if not proof_a.context.contains(a):
+        raise ProofCheckerFailedException(
+            f"Proposition {a} not found in context of the first proof."
+        )
+    if not proof_b.context.contains(b):
+        raise ProofCheckerFailedException(
+            f"Proposition {b} not found in context of the second proof."
+        )
+    
+    return Proof(
+        context=(
+            proof_a.context.union(proof_b.context)
+                   .without_prop(a).without_prop(b).with_prop(Or(a, b))
+        ),
+        statement=proof_a.statement,
+    )
+
+
+def or_r(proof : Proof, a : Prop, b : Prop) -> Proof:
+    """
+        Create a proof that demonstrates that a generalization is true.
+
+        $$
+           Γ ⊢ A
+        -----------
+         Γ ⊢ A ∨ B
+        $$
+
+        :param proof: The proof that demonstrates that the generalization is
+            correct.
+        :type proof: Proof
+        :param a: The proposition on the left side of the OR-statement.
+        :type a: Prop
+        :param b: The proposition on the right side of the OR-statement.
+        :type b: Prop
+        :return: A proof demonstrating that either of the two statements is
+            correct.
+        :rtype: Proof
+        :raises ProofCheckerFailedException: Neither proposition is proven by
+            the proof.
+    """
+    if proof.statement != a and proof.statement != b:
+        raise ProofCheckerFailedException(
+            f"The given proof proves neither {a} nor {b}."
+        )
+    
+    return Proof(
+        context=proof.context,
+        statement=Or(a, b),
+    )
+
+def reflexivity(eq : Eq) -> Proof:
+    """
+        Create a proof that demonstrates that one value is equal to oneself.
+        Typically, the statement is written slightly differently, but
+        normalizes to the same value. (e.g. 2 + 3 = 4 + 1)
+
+        $$
+        -----------
+         Γ ⊢ t = t
+        $$
+
+        :param eq: The equality that can be normalized.
+        :type eq: Eq
+        :return: A proof demonstrating that the two sides are equal.
+        :rtype: Proof
+        :raises ProofCheckerFailedException: The proof checker was unable to
+            demonstrate that the two sides are equal.
+    """
+    l = eq.x.normalize()
+    r = eq.x.normalize()
+
+    if l == r:
+        return Proof(
+            context=Context.empty(),
+            statement=eq,
+        )
+    else:
+        # diff_l, diff_r = l.reduce_on_equality(r)
+        raise ProofCheckerFailedException(
+            f"Could not normalize {eq.x} = {eq.y}, got stuck at {l} = {r}"
+            # f"Could not normalize {eq.x} = {eq.y}, got stuck at {diff_l} = {diff_r}"
+        )
+
+def suppose(ctx : Context, proof : Proof) -> Proof:
+    """
+        Create a proof with more assumptions than were originally necessary to
+        construct the proof.
+
+        $$
+          Γ ⊢ A
+        ----------
+        Γ, Γ' ⊢ A
+        $$
+
+        :param ctx: Additional context with additional proofs.
+        :type ctx: Context
+        :param proof: The proof to give more assumptions and context.
+        :type proof: Proof
+        :return: The proof with additional context.
+        :rtype: Proof
+    """
+    return Proof(
+        context=proof.context.union(ctx),
+        statement=proof.statement,
+    )

checker/props.py

@@ -0,0 +1,86 @@
+"""
+    This module hosts propositions.
+"""
+
+from __future__ import annotations
+
+from .terms import Term
+from dataclasses import dataclass
+
+class Prop:
+    """
+        A proposition is a logical statement. It can be proven by the proof
+        checker, or it can be used as a hypothesis to prove another
+        proposition.
+    """
+
+    def as_assumption(self, goal : Prop) -> list[list[tuple[list[Prop], Prop]]]:
+        """
+            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: Tuples of added assumptions with a new goal.
+            :rtype: list[list[tuple[list[Prop], Prop]]]
+        """
+        return []
+
+    def as_proof(self) -> list[list[tuple[list[Prop], Prop]]]:
+        """
+            Determine which hypotheses are required in the context to prove
+            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]]
+        """
+        return []
+
+@dataclass(frozen=True)
+class And(Prop):
+    """
+        The logical and-operator `P ^ Q`.
+    """
+
+    P : Prop
+    Q : Prop
+
+@dataclass(frozen=True)
+class Eq(Prop):
+    """
+        Compare whether two terms are equal.
+    """
+
+    x : Term
+    y : Term
+
+    def as_assumption(self, goal: Prop) -> list[list[tuple[list[Prop], Prop]]]:
+        return []
+    
+    def as_proof(self) -> list[list[tuple[list[Prop], Prop]]]:
+        return super().as_proof()
+
+@dataclass(frozen=True)
+class Implies(Prop):
+    """
+        The logical operator `P -> Q`.
+    """
+
+    P : Prop
+    Q : Prop
+
+@dataclass(frozen=True)
+class Or(Prop):
+    """
+        The logical and-operator `P v Q`.
+    """
+
+    P : Prop
+    Q : Prop
+    
+

checker/terms.py

@@ -0,0 +1,429 @@
+"""
+    Terms are values in an equation. They can be constants, variables,
+    functions, operators, and many more.
+"""
+
+from __future__ import annotations
+from typing import Callable
+
+import copy
+
+from dataclasses import dataclass
+
+# Known const values that can be substituted into other values.
+_known_consts : dict[str, Term] = {}
+
+# Known functions to normalize certain specific terms with given shapes.
+_known_norms : list[Callable[[Term], Term]] = []
+
+USABLE_VAR_NAMES = [
+    'x', 'y', 'z', 'a', 'b', 'c', 'd', 'e', 'f', 'g', 'h', 'i', 'j', 'k', 'l',
+    'm', 'n', 'o', 'p', 'q', 'r', 's', 't', 'u', 'v', 'w',
+    'α', 'β', 'γ', 'δ', 'ε', 'ζ', 'η', 'θ', 'ι', 'κ',
+    # 'λ', # Avoid confusion
+    'μ', 'ν', 'ξ', 'ο', 'π', 'ρ', 'σ', 'τ', 'υ', 'φ', 'χ', 'ψ', 'ω'
+]
+
+def normalize(term : Term) -> Term:
+    """
+        Create a normalization function. This function simplifies functions as
+        much as possible.
+    """
+    def norm_iter(term : Term) -> Term:
+        """
+            Normalize a single term. Use both the standard normalization scheme
+        """
+        for func in _known_norms:
+            term = func(term)
+        
+        return term
+
+    return traverse(f=norm_iter, term=term)
+
+def register_known_const(name : str, value : Term) -> None:
+    _known_consts[name] = value
+
+def register_known_norm(func : Callable[[Term], Term]) -> None:
+    _known_norms.append(func)
+
+def std_norm_iter(term : Term) -> Term:
+    """
+        Normalize a single term. Trust that all children values have
+        already been normalized, or that they will be normalized later on.
+
+        :param term: The term to normalize.
+        :type term: Term
+        :return: A normalized version of the term.
+        :rtype: Term
+    """
+    match term:
+        case App():
+            match term.f:
+                case Lambda():
+                    return term.f.substitute(value=term.x)
+                
+                case _:
+                    return term
+        
+        case Const():
+            return _known_consts.get(term.name, term)
+        
+        case Lambda():
+            return term
+        
+        case Var():
+            return term
+    
+        case Term():
+            return term
+_known_norms.append(std_norm_iter)
+
+def traverse(f : Callable[[Term], Term], term : Term) -> Term:
+    """
+        Traverse through the tree back-and-forth, aiming to run the given
+        function as thoroughly as possible to manipulate the term tree.
+
+        The function quits once no more operations are created.
+        **WARNING:** This means the tree might traverse forever.
+
+        :param f: The traversal function that replaces terms.
+        :type f: Callable[[Term], Term]
+        :param term: The term to traverse.
+        :type term: Term
+        :return: The result of the traversed term.
+        :rtype: Term
+    """
+    a, b = Term(), term
+
+    while a != b:
+        a, b = b, traverse_bottom_up(f=f, term=traverse_top_down(f=f, term=term))
+    
+    return b
+
+def traverse_bottom_up(f : Callable[[Term], Term], term : Term) -> Term:
+    """
+        Traverse a term from the bottom up, replacing values with whatever the
+        inserted function returns.
+
+        :param f: The traversal function that replaces terms.
+        :type f: Callable[[Term], Term]
+        :param term: The term to traverse.
+        :type term: Term
+        :return: The result of the traversed term.
+        :rtype: Term
+    """
+    match term:
+        case App():
+            return f(App(
+                f=traverse_bottom_up(f=f, term=term.f),
+                x=traverse_bottom_up(f=f, term=term.x)),
+            )
+        
+        case Const():
+            return f(term)
+        
+        case Lambda():
+            return term.replace_content(
+                traverse_bottom_up(f=f, term=term.out)
+            )
+        
+        case Var():
+            return f(term)
+        
+        case Term():
+            return f(term)
+
+def traverse_top_down(f : Callable[[Term], Term], term : Term) -> Term:
+    """
+        Traverse a term from the top down, replacing values with whatever the
+        inserted function returns.
+
+        :param f: The traversal function that replaces terms.
+        :type f: Callable[[Term], Term]
+        :param term: The term to traverse.
+        :type term: Term
+        :return: The result of the traversed term.
+        :rtype: Term
+    """
+    t = f(term)
+
+    match t:
+        case App():
+            return App(
+                f=traverse_top_down(f=f, term=t.f),
+                x=traverse_top_down(f=f, term=t.x),
+            )
+        
+        case Const():
+            return t
+        
+        case Lambda():
+            return t.replace_content(traverse_top_down(f=f, term=t.out))
+        
+        case Var():
+            return t
+
+        case Term():
+            return t
+
+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.
+        """
+        return self.to_str(vars={})
+    
+    def normalize(self) -> Term:
+        return normalize(term=self)
+
+    def to_str(self, vars : dict[str, Var]) -> str:
+        return "<undefined>"
+
+@dataclass(frozen=True)
+class App(Term):
+    """
+        An App is the application of a function with an argument.
+        You could consider it the inverse of the lambda function.
+    """
+
+    f : Term
+    x : Term
+
+    def __repr__(self) -> str:
+        """
+            Create a representation of a term.
+        """
+        return self.to_str(vars={})
+
+    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)
+
+        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)
+A3 = lambda fn, a, b, c : App(f=A2(fn, a, b), x=c)
+A4 = lambda fn, a, b, c, d : App(f=A3(fn, a, b, c), x=d)
+A5 = lambda fn, a, b, c, d, e : App(f=A4(fn, a, b, c, d), x=e)
+A6 = lambda fn, a, b, c, d, e, f : App(f=A5(fn, a, b, c, d, e), x=f)
+A7 = lambda fn, a, b, c, d, e, f, g : App(f=A6(fn, a, b, c, d, e, f), x=g)
+A8 = lambda fn, a, b, c, d, e, f, g, h : App(f=A7(fn, a, b, c, d, e, f, g), x=h)
+
+@dataclass(frozen=True)
+class Const(Term):
+    """
+        Constants are 0-ary functions. They can represent variables, constants
+        or other values that generally take no input.
+    """
+
+    name : str
+
+    def __repr__(self) -> str:
+        """
+            Create a representation of a term.
+        """
+        return self.to_str(vars={})
+
+    def to_str(self, vars: dict[str, Var]) -> str:
+        return self.name
+
+class Lambda(Term):
+    """
+        Lambdas a nameless 1-ary functions.
+    """
+
+    out : Term
+    var : Var
+
+    def __init__(self, f : Callable[[Var], Term]) -> None:
+        self.var = Var()
+        self.out = f(self.var)
+
+    def __repr__(self) -> str:
+        """
+            Create a representation of a term.
+        """
+        return self.to_str(vars={})
+    
+    def replace_content(self, term : Term) -> Lambda:
+        """
+            Replace the content of the lambda function with the given term.
+            The new term may still contain the lambda's var as an argument.
+
+            :param term: The term to insert in a lambda function.
+            :type term: Term
+            :return: The new Lambda function.
+            :rtype: Lambda
+        """
+        return Lambda(
+            lambda x : traverse_bottom_up(
+                f=lambda t : x if t is self.var else t,
+                term=term,
+            )
+        )
+
+    def substitute(self, value : Term) -> Term:
+        """
+            Substitute all variables of a given index number.
+
+            :param value: The value to replace the variable with.
+            :type value: Term
+            :return: A resolved lambda where the term has been substituted.
+            :rtype: Term
+        """
+        return traverse_bottom_up(
+            f=lambda t : value if t is self.var else t,
+            term=self.out,
+        )
+    
+    def to_str(self, vars: dict[str, Var]) -> str:
+        char = ''
+
+        for c in USABLE_VAR_NAMES:
+            if c not in vars:
+                char = c
+                vars[c] = self.var
+                break
+        else:
+            raise ValueError(
+                f"Cannot represent a lambda function that's over {len(USABLE_VAR_NAMES)} layers deep!"
+            )
+        
+        s = self.out.to_str(vars=vars)
+
+        del vars[char]
+        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)))
+L3 = lambda f : Lambda(lambda x : L2(lambda y, z : f(x, y, z)))
+L4 = lambda f : Lambda(lambda x : L3(lambda y, z, a : f(x, y, z, a)))
+L5 = lambda f : Lambda(lambda x : L4(lambda y, z, a, b : f(x, y, z, a, b)))
+L6 = lambda f : Lambda(lambda x : L5(lambda y, z, a, b, c : f(x, y, z, a, b, c)))
+L7 = lambda f : Lambda(lambda x : L6(lambda y, z, a, b, c, d : f(x, y, z, a, b, c, d)))
+L8 = lambda f : Lambda(lambda x : L7(lambda y, z, a, b, c, d, e : f(x, y, z, a, b, c, d, e)))
+
+@dataclass(frozen=True)
+class Var(Term):
+
+    """
+        A variable is a value that can be substituted by a lambda function.
+
+        Each lambda function stores a unique var, which can then point to a new
+        structure later on.
+    """
+
+    def __repr__(self) -> str:
+        """
+            Create a representation of a term.
+        """
+        return self.to_str(vars={})
+
+    def to_str(self, vars: dict[str, Var]) -> str:
+        for i, v in vars.items():
+            if v is self:
+                return i
+        else:
+            return "[ERROR:UNKNOWN_VAR]"
+
+if __name__ == "__main__":
+    print("REPRESENTATIONS")
+    print(30 * "=")
+
+    # x
+    print(Const("x"))
+
+    # λx.(f x)
+    print(Lambda(lambda a : App(f=Const("f"), x=a)))
+
+    # λx.(λy.(x y))
+    print(Lambda(lambda b : Lambda(lambda c : App(f=b, x=c))))
+
+    # Nat.Succ (Nat.Succ Nat.Zero)
+    print(App(f=Const("Nat.Succ"), x=App(f=Const("Nat.Succ"), x=Const("Nat.Zero"))))
+
+    
+    print("\nNORMALIZATIONS")
+    print(30 * "=")
+
+    # foo
+    a = App(f=Lambda(lambda x : x), x=Const("foo"))
+    print(a)
+    print(a.normalize())
+
+    # f x
+    b = App(
+        f=App(
+            f=Lambda(
+                lambda f : Lambda(
+                    lambda x : App(
+                        f=f, x=x
+                    )
+                )
+            ),
+            x=Const("f"),
+        ),
+        x= Const("x"),
+    )
+    print(b)
+    print(b.normalize())
+
+    # a b c
+    c = App(
+        f=App(
+            f=App(
+                f=Lambda(
+                    lambda x : Lambda(
+                        lambda y : Lambda(
+                            lambda z : App(
+                                f=App(f=x, x=y), x=z
+                            )
+                        )
+                    )
+                ),
+                x=Const("a"),
+            ),
+            x=Const("b"),
+        ),
+        x=Const("c"),
+    )
+    print(c)
+    print(c.normalize())
+
+    #
+    d = L3(lambda x, y, z : A2(x, y, z))
+    print(d)
+    print(d.normalize())
+
+    
+    print("\nSHORTHAND NOTATION")
+    print(30 * "=")
+
+    # λ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))
+    f = L3(lambda a, b, c : A3(L3(lambda a, b, c : A2(a, b, c)), a, b, c))
+    print(f)
+    print(f.normalize())
+    assert e == f.normalize()
+
+    # not
+    bool_t = L2(lambda x, y : x).normalize()
+    bool_f = L2(lambda x, y : y).normalize()
+    g = L1(lambda b : A2(b, bool_f, bool_t))
+    print(g)
+    print(g.normalize())

low.c

@@ -1,529 +0,0 @@
-#include <stdio.h>
-#include <stdint.h>
-#include <stdlib.h>
-#include <string.h>
-
-// Structures defined in this file
-typedef struct BlockHeader BlockHeader;
-typedef struct Closure Closure;
-typedef struct Frame Frame;
-typedef struct Text Text;
-typedef struct UnionType UnionType;
-typedef struct Var Var;
-
-// You can change this number to decide how much memory the program is allowed
-//   0 - 193 bytes   -> The program refuses to start
-// 194 - 217 bytes   -> The program starts but doesn't do anything
-// 218 +     bytes   -> The program runs successfully
-#define MEM_SIZE 193   //1024 * 1024 // 1 MB
-
-#define EXIT_GRACEFULLY 0
-#define EXIT_MEMORY_LIMIT_TOO_LOW 11
-#define EXIT_COULD_NOT_INIT_MEMORY 12
-#define EXIT_OUT_OF_MEMORY_DURING_INITIALIZATION 13
-
-#define EXIT_IMPOSSIBLE_FUNCTION_PHASE 77
-#define EXIT_IMPOSSIBLE_FUNCTION_ID 78
-#define EXIT_IMPOSSIBLE_FUNCTION_NO_CONTINUATION 79
-
-#define EXIT_IF_NULL(ptr) ({                                                   \
-    if (!ptr) {                                                                \
-        free(memory);                                                          \
-        printf("Failed to initialize program: out of memory\n");               \
-        exit(EXIT_OUT_OF_MEMORY_DURING_INITIALIZATION);                        \
-    }                                                                          \
-})
-
-/* ============================================================================
- *                                  MEMORY
- * ============================================================================
- */
-
-// Memory block structure
-// This block functions as a header for memory allocations on the heap
-typedef struct BlockHeader {
-    int free;
-    struct BlockHeader *next;
-} BlockHeader;
-
-#define BLOCK_SIZE(header) ({                                                  \
-    size_t s;                                                                  \
-    if (header->next) {                                                        \
-        s = (uint8_t *)(header->next) - (uint8_t *)header;                     \
-    } else {                                                                   \
-        s = (uint8_t *)(stack_top) - (uint8_t *)header;                        \
-    }                                                                          \
-    s - sizeof(BlockHeader);                                                   \
-})
-
-// Global memory pool
-static uint8_t *memory = NULL;
-static uintptr_t heap_base;
-static uintptr_t heap_top;
-static uintptr_t stack_base;
-static uintptr_t stack_top;
-
-// Initialize the custom memory manager
-void init_memory() {
-    if (MEM_SIZE < sizeof(BlockHeader) + 1) {
-        printf("Memory limit is too low!\n");
-        exit(EXIT_MEMORY_LIMIT_TOO_LOW);
-    }
-
-    memory = (uint8_t *)malloc(MEM_SIZE);
-    if (!memory) {
-        printf("Memory allocation failed!\n");
-        exit(EXIT_COULD_NOT_INIT_MEMORY);
-    }
-    heap_base = (uintptr_t)memory;
-    heap_top = heap_base;
-    stack_base = (uintptr_t)(memory + MEM_SIZE);
-    stack_top = stack_base;
-
-    BlockHeader *curr = (BlockHeader *)heap_base;
-    curr->free = 1;
-    curr->next = NULL;
-}
-
-// Macro for allocating a number of bytes on the heap
-#define HEAP_ALLOC(nbytes) ({                                                  \
-    void *ptr = NULL;                                                          \
-    BlockHeader *curr = (BlockHeader *)heap_base;                              \
-    while(curr) {                                                              \
-        size_t size = (BLOCK_SIZE(curr));                                      \
-        if (curr->free && size >= (nbytes)) {                                  \
-            /* If there's enough memory left over, split off into two */       \
-            if (size >= (nbytes) + sizeof(BlockHeader) + 1) {                  \
-                BlockHeader *new_block = (BlockHeader *)(                      \
-                    (uint8_t *)curr + sizeof(BlockHeader) + (nbytes)           \
-                );                                                             \
-                new_block->free = 1;                                           \
-                new_block->next = curr->next;                                  \
-                curr->next = new_block;                                        \
-                if ((uint8_t *)heap_top < (uint8_t *)new_block) {                                    \
-                    heap_top = (uintptr_t)new_block + sizeof(BlockHeader);                           \
-                }                                                              \
-            }                                                                  \
-            /* Assign block to new memory */                                   \
-            curr->free = 0;                                                    \
-            ptr = (uint8_t *)curr + sizeof(BlockHeader);                       \
-            break;                                                             \
-        }                                                                      \
-        /* Otherwise, go to the next block */                                  \
-        curr = curr->next;                                                     \
-    }                                                                          \
-    ptr;                                                                       \
-})
-
-// Macro for freeing bytes at a given address on the heap
-#define HEAP_FREE(ptr) ({                                                      \
-    if (ptr) {                                                                 \
-        BlockHeader *block = (BlockHeader *)(                                  \
-            (uint8_t *)(ptr) - sizeof(BlockHeader)                             \
-        );                                                                     \
-        block->free = 1;                                                       \
-        /* Merge adjacent free blocks */                                       \
-        BlockHeader *curr = (BlockHeader *)heap_base;                          \
-        while (curr) {                                                         \
-            if (curr->free && curr->next && curr->next->free) {                \
-                curr->size += sizeof(BlockHeader) + curr->next->size;          \
-                curr->next = curr->next->next;                                 \
-            } else {                                                           \
-                curr = curr->next;                                             \
-            }                                                                  \
-        }                                                                      \
-    }                                                                          \
-})
-
-// Pointer for debugging: print the heap to stdout
-#define HEAP_PRINT_WIDTH 60
-#define HEAP_PRINT() ({                                                        \
-    BlockHeader *curr = (BlockHeader *)heap_base;                              \
-    while (curr) {                                                             \
-        size_t size = BLOCK_SIZE(curr);                                        \
-        printf("BlockHeader at address %ld (physical %p): %lu byte",           \
-            (uint8_t *)curr - memory, curr, size                               \
-        );                                                                     \
-        if (size == 1) { printf(" of "); } else { printf("s of "); }           \
-        if (curr->free) {                                                      \
-            printf("free memory\n    ");                                       \
-        } else {                                                               \
-            printf("reserved memory\n    ");                                   \
-        }                                                                      \
-        unsigned char *content = (uint8_t *)curr;                              \
-        for (int i = 0; i < size + sizeof(BlockHeader); i++) {                 \
-            if (i == sizeof(BlockHeader)) { printf("| "); }                    \
-            printf("%02X ", content[i]);                                       \
-            if (i > HEAP_PRINT_WIDTH) { printf("..."); break; }                \
-        }                                                                      \
-        printf("\n    ");                                                      \
-        for (int i = 0; i < size + sizeof(BlockHeader); i++) {                 \
-            if (i == sizeof(BlockHeader)) { printf("| "); }                    \
-            if (content[i] == 0) { printf("   ");                              \
-            } else if (content[i] >= 32 && content[i] < 127) {                 \
-                printf("%c  ", content[i]);                                    \
-            } else { printf("__ "); }                                          \
-            if (i > HEAP_PRINT_WIDTH) { printf("..."); break; }                              \
-        }                                                                      \
-        printf("\n");                                                          \
-        curr = curr->next;                                                     \
-    }                                                                          \
-})
-
-#define SPACE_FILL(n) for (int i=0; i<n; i++) { printf(" "); }
-
-// Macro for allocating a number of bytes on the stack
-#define STACK_ALLOC(nbytes) ({                                                 \
-    void *ptr = NULL;                                                          \
-    if (stack_top >= heap_top + (nbytes)) {                                    \
-        stack_top -= (nbytes);                                                 \
-        ptr = (void *)stack_top;                                               \
-    }                                                                          \
-    ptr;                                                                       \
-})
-
-#define STACK_PRINT_VARIABLE_MAX 5
-#define STACK_PRINT(topPtr) ({                                                 \
-    Frame *cursor = topPtr;                                                    \
-    while (cursor) {                                                           \
-        Frame *next = cursor->cont;                                            \
-        size_t size;                                                           \
-        if (next) {                                                            \
-            size = (uint8_t *)(next) - (uint8_t *)(cursor);                    \
-        } else {                                                               \
-            size = (uint8_t *)(stack_base) - (uint8_t *)(cursor);              \
-        }                                                                      \
-        printf("Stack layer at offset -%ld (phsyical %p): %ld byte",           \
-            (uint8_t *)(stack_base) - (uint8_t *)(cursor), cursor, size        \
-        );                                                                     \
-        if (size == 1) { printf("\n    "); } else { printf("s\n    "); }       \
-        unsigned char *content = (uint8_t *)cursor;                            \
-        printf("| Code ID"); SPACE_FILL(sizeof(CodeID)*3 - 7 - 1);             \
-        printf("| Phase"); SPACE_FILL(sizeof(int)*3 - 5 - 2);                  \
-        printf("| Prev out"); SPACE_FILL(sizeof(Var *)*3-8 - 2);               \
-        printf("| Continuation"); SPACE_FILL(sizeof(Frame *)*3-12 - 1);        \
-        for (int i = 0; i < size - sizeof(Frame); i++) {                       \
-            printf("| Variable %d", i + 2); SPACE_FILL(2);                     \
-            if (i + 2 == STACK_PRINT_VARIABLE_MAX) { break; }                  \
-        }                                                                      \
-        printf("|\n    | ");                                                   \
-        for (int i = 0; i < sizeof(Frame); i++) {                              \
-            printf("%02X ", content[i]);                                       \
-        }                                                                      \
-        for (int i = sizeof(Frame); i < size; i++) {                           \
-            if ((i - sizeof(Frame)) % sizeof(Var) == 0) { printf("|"); }       \
-            printf("%02X ", content[i]);                                       \
-            if (i - sizeof(Frame) == STACK_PRINT_VARIABLE_MAX * sizeof(Var)) { \
-                break;                                                         \
-            }                                                                  \
-        }                                                                      \
-        printf("|\n");                                                         \
-        cursor = cursor->cont;                                                 \
-    }                                                                          \
-})
-// #define STACK_PRINT ({                                                         \
-//     printf("Stack from base %p to top %p:\n", (void *)stack_base, (void *)stack_top); \
-//     uint8_t *curr = (uint8_t *)stack_top;                                      \
-//     while ((uintptr_t)curr < stack_base) {                                     \
-//         printf("Address %ld (physical %p): \n    ", curr - memory, curr);             \
-//         for (int i = 0; i < STACK_PRINT_WIDTH && (uintptr_t)(curr + i) < stack_base; i++) { \
-//             printf("%02X ", curr[i]);                                          \
-//         }                                                                      \
-//         printf("\n    ");                                                      \
-//         for (int i = 0; i < STACK_PRINT_WIDTH && (uintptr_t)(curr + i) < stack_base; i++) { \
-//             if (curr[i] == 0) {                                                \
-//                 printf("   ");                                                 \
-//             } else if (curr[i] >= 32 && curr[i] < 127) {                       \
-//                 printf("%c  ", curr[i]);                                       \
-//             } else {                                                           \
-//                 printf("__ ");                                                 \
-//             }                                                                  \
-//         }                                                                      \
-//         printf("\n");                                                          \
-//         curr += STACK_PRINT_WIDTH;                                             \
-//     }                                                                          \
-// })
-
-
-// Macro for freeing a number of bytes on the stack
-#define STACK_FREE(nbytes) ({                                                  \
-    stack_top += (nbytes);                                                     \
-})
-
-#define MEM_DIAGNOSTICS(curr) ({                                               \
-    printf("----------------------------\n");                                  \
-    printf("Heap base at address %ld (physical %p)\n",                         \
-        (uint8_t *)heap_base - (uint8_t *)memory, (uint8_t *)heap_base                    \
-    );                                                                         \
-    printf("Heap top at address %ld (physical %p)\n",                          \
-        (uint8_t *)heap_top - (uint8_t *)memory, (uint8_t *)heap_top                      \
-    );                                                                         \
-    HEAP_PRINT();                                                              \
-    printf("----------------------------\n");                                  \
-    printf("Heap base at address %ld (physical %p)\n",                         \
-        (uint8_t *)heap_base - (uint8_t *)memory, (uint8_t *)heap_base                    \
-    );                                                                         \
-    printf("Heap top at address %ld (physical %p)\n",                          \
-        (uint8_t *)heap_top - (uint8_t *)memory, (uint8_t *)heap_top                      \
-    );                                                                         \
-    printf("Stack top at address %ld (physical %p)\n",                         \
-        (uint8_t *)stack_top - (uint8_t *)memory, (uint8_t *)stack_top                    \
-    );                                                                         \
-    printf("Stack base at address %ld (physical %p)\n",                        \
-        (uint8_t *)stack_base - (uint8_t *)memory, (uint8_t *)stack_base                  \
-    );                                                                         \
-    printf("----------------------------\n");                                  \
-    if (curr) {                                                                \
-        STACK_PRINT(curr);                                                     \
-    } else {                                                                   \
-        printf("Stack is NULL!\n");                                            \
-    }                                                                          \
-    printf("Stack top at address %ld (physical %p)\n",                         \
-        (uint8_t *)stack_top - (uint8_t *)memory, (uint8_t *)stack_top                    \
-    );                                                                         \
-    printf("Stack base at address %ld (physical %p)\n",                        \
-        (uint8_t *)stack_base - (uint8_t *)memory, (uint8_t *)stack_base                  \
-    );                                                                         \
-    printf("----------------------------\n");                                  \
-})
-
-
-/* ============================================================================
- *                            VARIABLES & VALUES
- * ============================================================================
- */
-
-// Types of values that can be stored in the heap
-typedef union {
-    int i;
-    char c;
-    Closure *f;
-    Text *t;
-    UnionType *u;
-} Value;
-
-#define HEAP_ALLOC_VALUE() HEAP_ALLOC(sizeof(Value))
-
-// Types of variables stored in a frame
-typedef enum {
-    ORIGINAL_VARIABLE,
-    MUTABLE_REFERENCE,
-    IMMUTABLE_REFERENCE
-} VarType;
-
-// Variable
-typedef struct Var {
-    VarType var_type;
-    Value *value;
-} Var;
-
-#define HEAP_ALLOC_VARIABLE() HEAP_ALLOC(sizeof(Var))
-
-// Names of functions
-typedef enum {
-    CODE_F,
-    CODE_G,
-    CODE_H,
-    CODE_EXIT  // Indicates termination
-} CodeID;
- 
-// A closure can represent a function that has yet to gather all inputs
-typedef struct Closure {
-    CodeID code_id;
-    Var variables[];
-} Closure;
-
-// A Text struct represents a string
-typedef struct Text {
-    size_t len;
-    char s[];
-} Text;
-
-// A Union type represents a type that can be one of several values.
-// For example:
-//      type Maybe a = Just a | Nothing
-typedef struct UnionType {
-    int name;
-    Value values[];
-} UnionType;
-
-#define HEAP_ALLOC_CLOSURE(code_id, arity) ({                                  \
-    Closure *c = HEAP_ALLOC(sizeof(Closure) + arity * sizeof(Var));            \
-    if (c) {                                                                   \
-        c->code_id = code_id;                                                  \
-    }                                                                          \
-    c;                                                                         \
-})
-
-#define HEAP_ALLOC_TEXT(length) ({                                                \
-    Text *t = HEAP_ALLOC(sizeof(Text) + length * sizeof(char));                \
-    if (t) {                                                                   \
-        t->len = length;                                                       \
-        for (int i = 0; i < length; i++) {                                     \
-            t->s[i] = '\0';                                                    \
-        }                                                                      \
-    }                                                                          \
-    t;                                                                         \
-})
-
-#define HEAP_ALLOC_UNION_TYPE(name, arity) ({                                  \
-    UnionType *u = HEAP_ALLOC(sizeof(UnionType) + arity * sizeof(Value));      \
-    if (u) {                                                                   \
-        u->name = name;                                                        \
-    }                                                                          \
-    u;                                                                         \
-})
-
-// Function arity
-#define ARITY_F 1
-#define ARITY_G 1
-#define ARITY_H 1
-#define ARITY_EXIT 1
-
-typedef struct Frame {
-    // Function to execute
-    CodeID code_id;
-    
-    // Phase of the function
-    int phase;
-    
-    // Return variable from previous frame
-    Var *prevOut;
-    
-    // CPS-style next frame to execute
-    struct Frame *cont;
-    
-    // Previously captured variables
-    Var variables[];
-} Frame;
-
-#define FRAME_SIZE(arity) sizeof(Frame) + (arity - 1) * sizeof(Var)
-
-#define STACK_ALLOC_FRAME(code_name, arity) ({                                 \
-    Frame *f = STACK_ALLOC(FRAME_SIZE(arity));                                 \
-    if(f) {                                                                    \
-        f->code_id = code_name;                                                \
-        f->phase = 0;                                                          \
-        f->prevOut = NULL;                                                     \
-        f->cont = NULL;                                                        \
-    }                                                                          \
-    f;                                                                         \
-})
-
-#define STACK_FREE_FRAME(arity) STACK_FREE(FRAME_SIZE(arity))
-
-int main(void) {
-    init_memory();
-    
-    Text *t = HEAP_ALLOC_TEXT(50);                          EXIT_IF_NULL(t);
-    Value *v = HEAP_ALLOC_VALUE();                          EXIT_IF_NULL(v);
-    Var *var = HEAP_ALLOC_VARIABLE();                       EXIT_IF_NULL(var);
-    Frame *fnsh = STACK_ALLOC_FRAME(CODE_EXIT, ARITY_EXIT); EXIT_IF_NULL(fnsh);
-    Frame *curr = STACK_ALLOC_FRAME(CODE_H, ARITY_H);       EXIT_IF_NULL(curr);
-    
-    sprintf(t->s, "Kaokkokos shall prevail by the hands of Alkbaard!");
-    
-    v->t = t;
-    var->var_type = ORIGINAL_VARIABLE;
-    var->value = v;
-    curr->prevOut = var;
-    curr->cont = fnsh;
-    
-    // STACK_PRINT(curr);
-    
-    while (curr) {
-        // MEM_DIAGNOSTICS(curr);
-        switch (curr->code_id) {
-            case CODE_F: {
-                // f(x) = print(x) and return x
-                Var *x = curr->prevOut;
-                Frame *next = curr->cont;
-                STACK_FREE_FRAME(ARITY_F);
-    
-                if (x) {
-                    printf("%s\n", x->value->t->s);
-                } else {
-                    printf("NULL: Out of memory!\n");
-                }
-    
-                curr = next;
-                break;
-            }
-            case CODE_G: {
-                // g(x) = String.upper(x)
-                Var *x = curr->prevOut;
-                Frame *next = curr->cont;
-                STACK_FREE_FRAME(ARITY_G);
-
-                if (x) {
-                    for (int i = 0; i < x->value->t->len; i++) {
-                        char c = x->value->t->s[i];
-                        if (c >= 'a' && c <= 'z') {
-                            x->value->t->s[i] = c - ('a' - 'A');
-                        }
-                    }
-
-                    next->prevOut = x;
-                }
-
-                curr = next;
-                break;
-            }
-            case CODE_H : {
-                // h(x) = f(g(x))
-                Var *x = curr->prevOut;
-                Frame *next = curr->cont;
-                STACK_FREE_FRAME(ARITY_H);
-
-                if (x) {
-                    Frame *f = STACK_ALLOC_FRAME(CODE_F, ARITY_F);
-                    
-                    if (f) {
-                        Frame *g = STACK_ALLOC_FRAME(CODE_G, ARITY_G);
-
-                        if (g) {
-                            f->cont = next;
-
-                            g->prevOut = x;
-                            g->cont = f;
-                            curr = g;
-                        } else {
-                            // No memory available! Free f & exit this function
-                            STACK_FREE_FRAME(ARITY_F);
-                            next->prevOut = NULL;
-                            curr = next;
-                        }
-                    } else {
-                        // No memory available! Exit this function
-                        next->prevOut = NULL;
-                        curr = next;
-                    }
-                } else {
-                    // prevOut is NULL - we were out of memory!
-                    curr = next;
-                }
-
-                break;
-            }
-            case CODE_EXIT: {
-                // HEAP_PRINT();
-                free(memory);
-                exit(EXIT_GRACEFULLY);
-                break;
-            }
-            default: {
-                free(memory);
-                printf("ERROR: Reached impossible function id!\n");
-                exit(EXIT_IMPOSSIBLE_FUNCTION_ID);
-                break;
-            }
-        }
-    }
-
-    free(memory);
-    
-    printf("ERROR: Reached function with no continuation!\n");
-
-    return EXIT_IMPOSSIBLE_FUNCTION_NO_CONTINUATION;
-}
-

proof.py

@@ -1,351 +0,0 @@
-from __future__ import annotations
-from typing import Any, Callable, Union
-
-from dataclasses import dataclass
-
-# -----------------------------------------------------------------------------
-# Terms
-# -----------------------------------------------------------------------------
-
-class Term:
-    pass
-
-@dataclass(frozen=True)
-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)
-A3 = lambda fn, a, b, c : App(f=A2(fn, a, b), x=c)
-A4 = lambda fn, a, b, c, d : App(f=A3(fn, a, b, c), x=d)
-A5 = lambda fn, a, b, c, d, e : App(f=A4(fn, a, b, c, d), x=e)
-A6 = lambda fn, a, b, c, d, e, f : App(f=A5(fn, a, b, c, d, e), x=f)
-A7 = lambda fn, a, b, c, d, e, f, g : App(f=A6(fn, a, b, c, d, e, f), x=g)
-A8 = lambda fn, a, b, c, d, e, f, g, h : App(f=A7(fn, a, b, c, d, e, f, g), x=h)
-
-@dataclass(frozen=True)
-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:
-    return A0("Bool.Truth")
-
-def Contradiction() -> Term:
-    return A0("Bool.Contradiction")
-
-# --- List constructors ---
-
-def Nil() -> Term:
-    return A0("List.Nil")
-
-def Cons(head : Term, tail : Term) -> Term:
-    return A2("List.Cons", head, tail)
-
-# --- Nat constructors ---
-
-def Zero() -> Term:
-    return A0("Nat.Zero")
-
-def Succ(n : Term) -> Term:
-    return A1("Nat.Succ", n)
-
-def kernel_from_int(n : int) -> Term:
-    if n == 0:
-        return Zero()
-    elif n < 0:
-        raise ValueError("Int is not Nat")
-    else:
-        return Succ(kernel_from_int(n-1))
-
-# -----------------------------------------------------------------------------
-# Propositions
-# -----------------------------------------------------------------------------
-
-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:
-    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):
-    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
-# -----------------------------------------------------------------------------
-
-@dataclass(frozen=True)
-class F:
-    arity : int
-    func : Callable[..., Term | None]
-
-F_ = lambda a : lambda f : F(arity=a, func=f)
-F0, F1, F2, F3 = F_(0), F_(1), F_(2), F_(3)
-F4, F5, F6, F7 = F_(4), F_(5), F_(6), F_(7)
-
-def apply_rules() -> dict[str, F]:
-    def __bool_not(x : Term) -> Term | None:
-        match x:
-            case Const("Bool.Truth"):
-                return Contradiction()
-            
-            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(A2("Nat.add", x_, y))
-
-    def __nat_iszero(x : Term) -> Term | None:
-        match x:
-            case Const("Nat.Zero"):
-                return Truth()
-            
-            case App(f=Const("Nat.Succ")):
-                return Contradiction()
-
-    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():
-            f = normalize(term.f)
-            x = normalize(term.x)
-
-            cursor = term
-            items = [ term ]
-
-            while True:
-                match cursor.f:
-                    case App():
-                        cursor = cursor.f
-                        items.append(cursor)
-                    
-                    case Const():
-                        name = cursor.f.name
-                        rule = apply_rules().get(name, None)
-
-                        if rule is None:
-                            return App(f, x) # Unknown function
-                        if len(items) != rule.arity:
-                            # If len(items) is too small, we don't have
-                            # enough inputs yet to evaluate the function
-                            # If len(items) is too large, we already evaluated
-                            # the function before and couldn't optimize.
-                            return App(f, x)
-                        
-                        out = rule.func(*reversed([i.x for i in items]))
-
-                        return normalize(out) if out is not None else App(f, x)
-
-        case Const():
-            return term
-
-        case Term():
-            return term
-
-# -----------------------------------------------------------------------------
-# Proof checker
-# -----------------------------------------------------------------------------
-
-ProofCheck = Union["Proven", "ProveFailure"]
-
-@dataclass(frozen=True)
-class Proven:
-    pass
-
-@dataclass(frozen=True)
-class ProveFailure:
-    s : str
-
-def check(goal: Prop, proof : Proof, ctx : Context) -> Prop:
-    return proof.apply(goal, ctx)
-
-# -----------------------------------------------------------------------------
-# -----------------------------------------------------------------------------
-# -----------------------------------------------------------------------------
-
-if __name__ == "__main__":
-    # 2 + 3 == 5
-    print(check(
-        Eq(
-            lhs=A2("Nat.add", kernel_from_int(2), kernel_from_int(3)),
-            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
-    print(check(
-        Eq(
-            lhs=A2("Nat.add", Zero(), Const("x")),
-            rhs=Const("x")
-        ),
-        Refl(),
-        Context(props=[]),
-    ))
-
-    # x + 0 == x
-    print(check(
-        Eq(
-            lhs=A2("Nat.add", Const("x"), Zero()),
-            rhs=Const("x")
-        ),
-        Refl(),
-        Context(props=[]),
-    ))

proof_checker.py

@@ -0,0 +1,20 @@
+from checker import lib, proof, props
+from checker.terms import App, Const
+
+# Prove : true == not false
+p = proof.reflexivity(
+    props.Eq(
+        x=Const("Bool.True"),
+        y=App(f=Const("Bool.not"), x=Const("Bool.False"))
+    )
+)
+p.check()
+
+# Prove : false == not true
+p = proof.reflexivity(
+    props.Eq(
+        x=Const("Bool.False"),
+        y=App(f=Const("Bool.not"), x=Const("Bool.True"))
+    )
+)
+p.check()