382 lines
12 KiB
Python
382 lines
12 KiB
Python
"""
|
||
The proofs module contains various methods to construct a proof.
|
||
"""
|
||
|
||
from __future__ import annotations
|
||
from typing import Callable
|
||
|
||
from dataclasses import dataclass
|
||
from .context import Context
|
||
from .props import And, Eq, Exists, ForAll, Or, Prop
|
||
from .terms import Const, Term
|
||
|
||
class ProofCheckerFailedException(Exception):
|
||
pass
|
||
|
||
@dataclass(frozen=True)
|
||
class Proof:
|
||
"""
|
||
Base class to construct a proof.
|
||
"""
|
||
|
||
context : Context
|
||
statement : Prop
|
||
|
||
def __repr__(self) -> str:
|
||
return (
|
||
# "Γ" +
|
||
", ".join([ str(p) for p in self.context.props]) +
|
||
" ⊢ " +
|
||
str(self.statement)
|
||
)
|
||
|
||
def check(self, is_lemma : bool = False, to_stdout : bool = False) -> 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():
|
||
if to_stdout:
|
||
print(f"Successfully proved that {self}")
|
||
return
|
||
elif is_lemma:
|
||
if to_stdout:
|
||
print(f"Proved lemma: {self}")
|
||
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 eq_l(proof : Proof, eq : Eq, statement : Prop) -> Proof:
|
||
"""
|
||
Use an equality to the left of the statement to substitute values.
|
||
|
||
$$
|
||
Γ ⊢ P[y]
|
||
-----------------
|
||
Γ, x = y ⊢ P[x]
|
||
$$
|
||
|
||
:param proof: The proof supporting the claim.
|
||
:type proof: Proof
|
||
:param eq: The equality, where the statement on the left is meant to be
|
||
replaced by the statement on the right.
|
||
:type eq: Eq
|
||
:param statement: The final statement that one should end up at.
|
||
:type statement: Prop
|
||
"""
|
||
if proof.statement.normalize() != statement.normalize().replace(old=eq.x, new=eq.y).normalize():
|
||
raise ProofCheckerFailedException(
|
||
f"Failed to arrive at {proof.statement} "
|
||
f"when substituting {eq} into {statement}"
|
||
)
|
||
|
||
return Proof(
|
||
context=proof.context.with_prop(eq),
|
||
statement=statement,
|
||
)
|
||
|
||
def forall_l(proof : Proof, statement : Callable[[Term], Prop], term : Term) -> Proof:
|
||
"""
|
||
Generalize a hypothesis by making a term more generalized.
|
||
|
||
$$
|
||
Γ, P[x] ⊢ Q
|
||
--------------
|
||
Γ, ∀x.P ⊢ Q
|
||
$$
|
||
|
||
:param proof: The proof with the hypothesis to generalize.
|
||
:type proof: Proof
|
||
:param statement: The statement to generalize.
|
||
:type statement: Callable[[Term], Proof]
|
||
:param term: The term to substitute.
|
||
:type term: Term
|
||
:return: The generalized proof.
|
||
:rtype: Proof
|
||
"""
|
||
s = statement(term)
|
||
|
||
# TODO: Return new proof
|
||
return proof
|
||
|
||
def forall_r(proof : Proof, statement : Callable[[Term], Prop], free_var_name : str) -> Proof:
|
||
"""
|
||
Generalize a proof for all instances of a given value.
|
||
|
||
$$
|
||
Γ ⊢ P[x]
|
||
-----------------
|
||
Γ ⊢ \forall x.P
|
||
$$
|
||
|
||
:param proof: The proof to generalize.
|
||
:type proof: Proof
|
||
:param statement: The forall-statement.
|
||
:type statement: Callable[[Term], Prop]
|
||
:param free_var_name: The free variable that can be generalized.
|
||
:type free_var_name: str
|
||
:return: The generalized proof.
|
||
:rtype: Proof
|
||
"""
|
||
fv = Const(free_var_name)
|
||
nfv = Const("not_" + free_var_name)
|
||
|
||
# Make sure the free variable isn't bound within the statement
|
||
s = statement(nfv)
|
||
if s.contains(fv):
|
||
raise ProofCheckerFailedException(
|
||
f"Some occurrences of {free_var_name} were found to not be "
|
||
f"substituted in {s}"
|
||
)
|
||
|
||
# Make sure the free variable doesn't appear in the context
|
||
s = statement(fv)
|
||
for p in proof.context.props:
|
||
if p.contains(fv):
|
||
raise ProofCheckerFailedException(
|
||
f"Free variable {fv} was found in context hypothesis: {p}"
|
||
)
|
||
|
||
# Make sure the proof statement matches the statement with the free variable
|
||
if s != proof.statement:
|
||
raise ProofCheckerFailedException(
|
||
f"Expected proof to prove that {s}, found {proof.statement} instead."
|
||
)
|
||
|
||
return Proof(context=proof.context, statement=Exists(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.y.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,
|
||
)
|