268 lines
7.9 KiB
Python
268 lines
7.9 KiB
Python
"""
|
||
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 {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,
|
||
)
|