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