From 362e82474cc250111e94059e01f1722cf14a28bd Mon Sep 17 00:00:00 2001 From: Bram van den Heuvel Date: Sun, 5 Jul 2026 23:10:09 +0200 Subject: [PATCH] Create a proof BUILDER more than a checker - lol --- checker/context.py | 95 ++++++++++++++++++++ checker/proof.py | 217 ++++++++++++++++++++++++++++++++++++++------- checker/props.py | 56 ++---------- 3 files changed, 285 insertions(+), 83 deletions(-) create mode 100644 checker/context.py diff --git a/checker/context.py b/checker/context.py new file mode 100644 index 0000000..fd02dc9 --- /dev/null +++ b/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)) diff --git a/checker/proof.py b/checker/proof.py index 57c9926..2a083db 100644 --- a/checker/proof.py +++ b/checker/proof.py @@ -4,54 +4,203 @@ from __future__ import annotations -import .props as p - -from .props import Context, Prop +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 -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: - """ - Create a new proof that uses reflexivity. This axiom defines that - variables equal oneselves. +def and_r(proof1 : Proof, proof2 : Proof) -> Proof: + """ + Create a proof that demonstrates that the statements of two proofs are + both true. - :param ctx: The context with which one wants to prove this. - :type ctx: Context - :param goal: The equality that needs to be proven. - :type goal: Prop - :raises ProofCheckerFailedException: The proof checker cannot - verify the goal. - """ + $$ + Γ ⊢ A Γ' ⊢ B + --------------- + Γ, Γ' ⊢ A ∧ B + $$ - match goal: - case p.Eq(): - lhs = goal.x.normalize() - rhs = goal.y.normalize() + :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), + ) - if lhs == rhs: - self.ctx = ctx - self.goal = goal - else: - l, r = lhs.reduce_on_equality(rhs) +def assume(statement : Prop) -> Proof: + """ + Gain a tautological proof that proves a statement by assuming + it's true. - raise ProofCheckerFailedException( - f"Could not prove that {lhs} = {rhs}. Got stuck on {l} = {r}." - ) - - case _: - raise ProofCheckerFailedException( - "Reflexivity can only prove that t = t. Found another prop type than `Eq`." - ) + :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_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, + ) diff --git a/checker/props.py b/checker/props.py index 5236bec..2fd8cfe 100644 --- a/checker/props.py +++ b/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]]]: - return [ - [ ( [], self.P ) - , ( [ self.Q ], goal) - ], - ] - - def as_proof(self) -> list[list[tuple[list[Prop], Prop]]]: - return [ - [ ( [ self.P ], self.Q ) - ], - ] +@dataclass(frozen=True) +class Or(Prop): + """ + The logical and-operator `P v Q`. + """ -# @dataclass(frozen=True) -# class Or(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 [ - -# ] + P : Prop + Q : Prop