Create a proof BUILDER more than a checker - lol

checker/context.py

@@ -0,0 +1,95 @@
+"""
+    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 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/proof.py

@@ -4,54 +4,203 @@
 
 from __future__ import annotations
 
-import .props as p
+from dataclasses import dataclass
-
+from .context import Context
-from .props import Context, Prop
+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
 
-class Reflexivity(Proof):
+def and_l(proof : Proof, a : Prop, b : Prop) -> Proof:
     """
-        Reflectivity proof checker that solves t = t.
+        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 __init__(self, ctx : Context, goal : Prop) -> None:
+def and_r(proof1 : Proof, proof2 : Proof) -> Proof:
-        """
+    """
-            Create a new proof that uses reflexivity. This axiom defines that
+        Create a proof that demonstrates that the statements of two proofs are
-            variables equal oneselves.
+        both true.
 
-            :param ctx: The context with which one wants to prove this.
+        $$
-            :type ctx: Context
+         Γ ⊢ A  Γ' ⊢ B
-            :param goal: The equality that needs to be proven.
+        ---------------
-            :type goal: Prop
+         Γ, Γ' ⊢ A ∧ B
-            :raises ProofCheckerFailedException: The proof checker cannot
+        $$
-                verify the goal.
-        """
 
-        match goal:
+        :param proof1: The first proof.
-            case p.Eq():
+        :type proof1: Proof
-                lhs = goal.x.normalize()
+        :param proof2: The second proof.
-                rhs = goal.y.normalize()
+        :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),
+    )
 
-                if lhs == rhs:
+def assume(statement : Prop) -> Proof:
-                    self.ctx = ctx
+    """
-                    self.goal = goal
+        Gain a tautological proof that proves a statement by assuming
-                else:
+        it's true.
-                    l, r = lhs.reduce_on_equality(rhs)
 
-                    raise ProofCheckerFailedException(
+        :param statement: A propositional statement to prove.
-                        f"Could not prove that {lhs} = {rhs}. Got stuck on {l} = {r}."
+        :type statement: Prop
-                    )
+        :return: A tautological proof.
-            
+        :rtype: Proof
-            case _:
+    """
-                raise ProofCheckerFailedException(
+    return from_assumption(
-                    "Reflexivity can only prove that t = t. Found another prop type than `Eq`."
+        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_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 {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

@@ -7,17 +7,6 @@ from __future__ import annotations
 from .terms import Term
 from dataclasses import dataclass
 
-@dataclass(frozen=True)
-class Context:
-    """
-        The Context is a collection of propositions. These are the hypotheses
-        that are used to arrive at a proof.
-    """
-    props : list["Prop"]
-
-    def with_prop(self, new_prop : "Prop") -> Context:
-        return Context(props=[ prop for prop in self.props ] + [ new_prop ])
-
 class Prop:
     """
         A proposition is a logical statement. It can be proven by the proof
@@ -61,19 +50,6 @@ class And(Prop):
     P : Prop
     Q : Prop
 
-    def as_assumption(self, goal: Prop) -> list[list[tuple[list[Prop], Prop]]]:
-        return [
-            [ ( [ self.P, self.Q ], goal )
-            ],
-        ]
-    
-    def as_proof(self) -> list[list[tuple[list[Prop], Prop]]]:
-        return [
-            [ ( [], self.P )
-            , ( [], self.Q )
-            ],
-        ]
-
 class Eq(Prop):
     """
         Compare whether two terms are equal.
@@ -97,31 +73,13 @@ class Implies(Prop):
     P : Prop
     Q : Prop
 
-    def as_assumption(self, goal : Prop) -> list[list[tuple[list[Prop], Prop]]]:
+@dataclass(frozen=True)
-        return [
+class Or(Prop):
-            [ ( [], self.P )
+    """
-            , ( [ self.Q ], goal)
+        The logical and-operator `P v Q`.
-            ],
+    """
-        ]
-    
-    def as_proof(self) -> list[list[tuple[list[Prop], Prop]]]:
-        return [
-            [ ( [ self.P ], self.Q )
-            ],
-        ]
 
-# @dataclass(frozen=True)
+    P : Prop
-# class Or(Prop):
+    Q : Prop
-#     """
-#         The logical and-operator `P v Q`.
-#     """
-
-#     P : Prop
-#     Q : Prop
-
-#     def as_assumption(self, goal: Prop) -> list[list[tuple[list[Prop], Prop]]]:
-#         return [
-
-#         ]