Commit working changes (attempted scripts)
parent
0612e320b0
commit
16490af209
|
|
@ -0,0 +1,15 @@
|
|||
"""
|
||||
This module hosts various elements that are necessary to create a proof
|
||||
checker.
|
||||
"""
|
||||
|
||||
from .props import And, Implies, Prop
|
||||
from .terms import Term, register_known_const
|
||||
|
||||
__all__ = [
|
||||
"And",
|
||||
"Implies",
|
||||
"Prop",
|
||||
"Term",
|
||||
"register_known_const",
|
||||
]
|
||||
|
|
@ -0,0 +1,57 @@
|
|||
"""
|
||||
The proofs module contains various methods to construct a proof.
|
||||
"""
|
||||
|
||||
from __future__ import annotations
|
||||
|
||||
import .props as p
|
||||
|
||||
from .props import Context, Prop
|
||||
|
||||
class ProofCheckerFailedException(Exception):
|
||||
pass
|
||||
|
||||
class Proof:
|
||||
"""
|
||||
Base class to construct a proof.
|
||||
"""
|
||||
|
||||
# -----------------------------------------------------------------------------
|
||||
|
||||
class Reflexivity(Proof):
|
||||
"""
|
||||
Reflectivity proof checker that solves t = t.
|
||||
"""
|
||||
|
||||
def __init__(self, ctx : Context, goal : Prop) -> None:
|
||||
"""
|
||||
Create a new proof that uses reflexivity. This axiom defines that
|
||||
variables equal oneselves.
|
||||
|
||||
: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.
|
||||
"""
|
||||
|
||||
match goal:
|
||||
case p.Eq():
|
||||
lhs = goal.x.normalize()
|
||||
rhs = goal.y.normalize()
|
||||
|
||||
if lhs == rhs:
|
||||
self.ctx = ctx
|
||||
self.goal = goal
|
||||
else:
|
||||
l, r = lhs.reduce_on_equality(rhs)
|
||||
|
||||
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`."
|
||||
)
|
||||
|
|
@ -0,0 +1,127 @@
|
|||
"""
|
||||
This module hosts propositions.
|
||||
"""
|
||||
|
||||
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
|
||||
checker, or it can be used as a hypothesis to prove another
|
||||
proposition.
|
||||
"""
|
||||
|
||||
def as_assumption(self, goal : Prop) -> list[list[tuple[list[Prop], Prop]]]:
|
||||
"""
|
||||
Propositions can simplify the proof by creating simpler theorems
|
||||
and sub-lemmas to prove instead. If this proposition is part of
|
||||
the assumptions, this function helps transform the goal into
|
||||
simpler sub-goals.
|
||||
|
||||
:return: Tuples of added assumptions with a new goal.
|
||||
:rtype: list[list[tuple[list[Prop], Prop]]]
|
||||
"""
|
||||
return []
|
||||
|
||||
def as_proof(self) -> list[list[tuple[list[Prop], Prop]]]:
|
||||
"""
|
||||
Determine which hypotheses are required in the context to prove
|
||||
this proposition.
|
||||
|
||||
The function returns a list of various methods to prove the
|
||||
proposition. If any of the methods is an empty list, it means
|
||||
the proposition requires no assumptions and can instead be
|
||||
computed.
|
||||
|
||||
:return: Methods to prove this proposition.
|
||||
:rtype: list[tuple[list[Prop], Prop]]
|
||||
"""
|
||||
return []
|
||||
|
||||
@dataclass(frozen=True)
|
||||
class And(Prop):
|
||||
"""
|
||||
The logical and-operator `P ^ Q`.
|
||||
"""
|
||||
|
||||
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.
|
||||
"""
|
||||
|
||||
x : Term
|
||||
y : Term
|
||||
|
||||
def as_assumption(self, goal: Prop) -> list[list[tuple[list[Prop], Prop]]]:
|
||||
return []
|
||||
|
||||
def as_proof(self) -> list[list[tuple[list[Prop], Prop]]]:
|
||||
return super().as_proof()
|
||||
|
||||
@dataclass(frozen=True)
|
||||
class Implies(Prop):
|
||||
"""
|
||||
The logical operator `P -> Q`.
|
||||
"""
|
||||
|
||||
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`.
|
||||
# """
|
||||
|
||||
# P : Prop
|
||||
# Q : Prop
|
||||
|
||||
# def as_assumption(self, goal: Prop) -> list[list[tuple[list[Prop], Prop]]]:
|
||||
# return [
|
||||
|
||||
# ]
|
||||
|
||||
|
||||
|
|
@ -0,0 +1,188 @@
|
|||
"""
|
||||
Terms are values in an equation. They can be constants, variables,
|
||||
functions, operators, and many more.
|
||||
"""
|
||||
|
||||
from __future__ import annotations
|
||||
|
||||
import copy
|
||||
|
||||
from dataclasses import dataclass
|
||||
|
||||
__known_consts : dict[str, Term] = {
|
||||
}
|
||||
|
||||
def register_known_const(name : str, value : Term) -> None:
|
||||
__known_consts[name] = value
|
||||
|
||||
class Term:
|
||||
"""
|
||||
Base class for all terms.
|
||||
"""
|
||||
|
||||
def normalize(self) -> Term:
|
||||
"""
|
||||
Function to return a simplified version of the term.
|
||||
"""
|
||||
return self
|
||||
|
||||
def reduce_on_equality(self, other : Term) -> tuple[Term, Term]:
|
||||
"""
|
||||
Reduce parts that the two items are equal on.
|
||||
"""
|
||||
return self, other
|
||||
|
||||
def substitute(self, index : int, value : Term) -> Term:
|
||||
"""
|
||||
Substitute all variables of a given index number.
|
||||
|
||||
:param index: The variable's index.
|
||||
:type index: int
|
||||
:param value: The value to replace the variable with.
|
||||
:type value:
|
||||
"""
|
||||
return self
|
||||
|
||||
@dataclass(frozen=True)
|
||||
class App(Term):
|
||||
"""
|
||||
An App is the application of a function with an argument.
|
||||
You could consider it the inverse of the lambda function.
|
||||
"""
|
||||
|
||||
f : Term
|
||||
x : Term
|
||||
|
||||
def normalize(self) -> Term:
|
||||
f = self.f.normalize()
|
||||
x = self.x.normalize()
|
||||
|
||||
default = App(f=f, x=x)
|
||||
|
||||
match f:
|
||||
case App():
|
||||
return default
|
||||
|
||||
case Const():
|
||||
return default
|
||||
|
||||
case Lambda():
|
||||
return f.resolve(x)
|
||||
|
||||
case Term():
|
||||
return default
|
||||
|
||||
case Var():
|
||||
return default
|
||||
|
||||
def reduce_on_equality(self, other: Term) -> tuple[Term, Term]:
|
||||
if not isinstance(other, App):
|
||||
return self, other
|
||||
|
||||
f1, f2 = self.f.normalize(), other.f.normalize()
|
||||
x1, x2 = self.x.normalize(), other.x.normalize()
|
||||
|
||||
match ( f1 == f2, x1 == x2 ):
|
||||
case ( True, True ):
|
||||
return Term(), Term()
|
||||
|
||||
case ( True, False ):
|
||||
return x1.reduce_on_equality(x2)
|
||||
|
||||
case ( False, True ):
|
||||
return f1.reduce_on_equality(f2)
|
||||
|
||||
case ( False, False ):
|
||||
return self, other
|
||||
|
||||
def substitute(self, index : int, value : Term) -> Term:
|
||||
"""
|
||||
Substitute all variables of a given index number.
|
||||
|
||||
:param index: The variable's index.
|
||||
:type index: int
|
||||
:param value: The value to replace the variable with.
|
||||
:type value:
|
||||
"""
|
||||
return App(
|
||||
f=self.f.substitute(index=index, value=value),
|
||||
x=self.x.substitute(index=index, value=value),
|
||||
)
|
||||
|
||||
@dataclass(frozen=True)
|
||||
class Const(Term):
|
||||
"""
|
||||
Constants are 0-ary functions. They can represent variables, constants
|
||||
or other values that generally take no input.
|
||||
"""
|
||||
|
||||
name : str
|
||||
|
||||
def normalize(self) -> Term:
|
||||
if self.name in __known_consts:
|
||||
return copy.deepcopy(__known_consts.get(self.name, self))
|
||||
else:
|
||||
return self
|
||||
|
||||
@dataclass(frozen=True)
|
||||
class Lambda(Term):
|
||||
"""
|
||||
Lambdas a nameless 1-ary functions.
|
||||
"""
|
||||
|
||||
out : Term
|
||||
|
||||
def normalize(self) -> Term:
|
||||
return Lambda(out=self.out.normalize())
|
||||
|
||||
def reduce_on_equality(self, other: Term) -> tuple[Term, Term]:
|
||||
match other:
|
||||
case Lambda():
|
||||
return self.out, other.out
|
||||
case _:
|
||||
return self, other
|
||||
|
||||
def resolve(self, value : Term) -> Term:
|
||||
"""
|
||||
Resolve this lambda function by inserting a value.
|
||||
|
||||
:param value: The value to substitute.
|
||||
"""
|
||||
return self.substitute(index=-1, value=value)
|
||||
|
||||
def substitute(self, index : int, value : Term) -> Term:
|
||||
"""
|
||||
Substitute all variables of a given index number.
|
||||
|
||||
:param index: The variable's index.
|
||||
:type index: int
|
||||
:param value: The value to replace the variable with.
|
||||
:type value:
|
||||
"""
|
||||
if index == -1:
|
||||
# We're resolving this lambda function!
|
||||
return self.out.substitute(index=index + 1, value=value)
|
||||
else:
|
||||
return Lambda(out=self.out.substitute(index=index + 1, value=value))
|
||||
|
||||
@dataclass(frozen=True)
|
||||
class Var(Term):
|
||||
"""
|
||||
A variable is a value that can be substituted by a lambda function.
|
||||
"""
|
||||
|
||||
index : int
|
||||
|
||||
def substitute(self, index : int, value : Term) -> Term:
|
||||
"""
|
||||
Substitute all variables of a given index number.
|
||||
|
||||
:param index: The variable's index.
|
||||
:type index: int
|
||||
:param value: The value to replace the variable with.
|
||||
:type value:
|
||||
"""
|
||||
if self.index == index:
|
||||
return copy.deepcopy(value)
|
||||
else:
|
||||
return self
|
||||
78
proof.py
78
proof.py
|
|
@ -147,6 +147,9 @@ class Assumption(Proof):
|
|||
class Refl(Proof):
|
||||
def apply(self, goal : Prop, ctx : Context) -> Prop:
|
||||
match goal:
|
||||
case Contradict():
|
||||
return goal
|
||||
|
||||
case Eq():
|
||||
l = normalize(goal.lhs)
|
||||
r = normalize(goal.rhs)
|
||||
|
|
@ -171,10 +174,68 @@ class Refl(Proof):
|
|||
f"Couldn't normalize {goal.lhs} = {goal.rhs} any further than to {l} = {r}"
|
||||
)
|
||||
|
||||
case Trivial():
|
||||
return goal
|
||||
|
||||
case Prop():
|
||||
return goal
|
||||
|
||||
@dataclass(frozen=True)
|
||||
class Rewrite(Proof):
|
||||
m : Term
|
||||
s : Term
|
||||
|
||||
def apply(self, goal : Prop, ctx : Context) -> Prop:
|
||||
if Eq(lhs=self.m, rhs=self.s) not in ctx.props:
|
||||
if Eq(lhs=self.s, rhs=self.m) not in ctx.props:
|
||||
return Contradict(
|
||||
"Cannot prove base proposition"
|
||||
f"Could not find justification why you would be able to substitute {self.m} with {self.s}"
|
||||
)
|
||||
|
||||
match goal:
|
||||
case Contradict():
|
||||
return goal
|
||||
|
||||
case Eq(lhs=lhs, rhs=rhs):
|
||||
return Eq(
|
||||
lhs=self.find_and_replace(lhs),
|
||||
rhs=self.find_and_replace(rhs),
|
||||
)
|
||||
|
||||
case Prop():
|
||||
return goal
|
||||
|
||||
case Trivial():
|
||||
return goal
|
||||
|
||||
def find_and_replace(self, term : Term) -> Term:
|
||||
if term == self.m or term == self.s:
|
||||
return self.s
|
||||
|
||||
match term:
|
||||
case App(f=f, x=x):
|
||||
return App(
|
||||
f=self.find_and_replace(f),
|
||||
x=self.find_and_replace(x),
|
||||
)
|
||||
|
||||
case Const():
|
||||
return term
|
||||
|
||||
case Term():
|
||||
return term
|
||||
|
||||
@dataclass(frozen=True)
|
||||
class Script(Proof):
|
||||
steps : list[Proof]
|
||||
|
||||
def apply(self, goal: Prop, ctx: Context) -> Prop:
|
||||
state = goal
|
||||
|
||||
for step in self.steps:
|
||||
state = step.apply(state, ctx)
|
||||
|
||||
return state
|
||||
|
||||
# -----------------------------------------------------------------------------
|
||||
# Context
|
||||
|
|
@ -349,3 +410,18 @@ if __name__ == "__main__":
|
|||
Refl(),
|
||||
Context(props=[]),
|
||||
))
|
||||
|
||||
# x + 4 = 6 when x = 2
|
||||
print(check(
|
||||
goal=Eq(
|
||||
lhs=A2("Nat.add", Const("x"), kernel_from_int(4)),
|
||||
rhs=kernel_from_int(6),
|
||||
),
|
||||
proof=Script([
|
||||
Rewrite(m=Const("x"), s=kernel_from_int(2)),
|
||||
Refl()
|
||||
]),
|
||||
ctx=Context([
|
||||
Eq(Const("x"), kernel_from_int(2)),
|
||||
]),
|
||||
))
|
||||
|
|
|
|||
Loading…
Reference in New Issue