Bram
/
new-lang
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Compare commits

base: Bram:main
Branches Tags
Bram:main
Bram:dev
..
compare: Bram:dev
Branches Tags
Bram:main
Bram:dev

No commits in common. "main" and "dev" have entirely different histories.
main ... dev

4 changed files with 37 additions and 521 deletions
Show Stats Expand all files Collapse all files

121
checker/proof.py
View File

@ -3,12 +3,10 @@
"""
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
from .props import And, Eq, Or, Prop
class ProofCheckerFailedException(Exception):
pass
@ -22,26 +20,14 @@ class 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:
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():
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."
@ -121,105 +107,6 @@ def assume(statement : Prop) -> Proof:
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.
@ -343,7 +230,7 @@ def reflexivity(eq : Eq) -> Proof:
demonstrate that the two sides are equal.
"""
l = eq.x.normalize()
r = eq.y.normalize()
r = eq.x.normalize()
if l == r:
return Proof(

300
checker/props.py
View File

@ -5,7 +5,7 @@
from __future__ import annotations
from typing import Callable
from .terms import USABLE_VAR_NAMES, Const, Term, Var, ecsl
from .terms import Term
from dataclasses import dataclass
class Prop:
@ -15,88 +15,42 @@ class Prop:
proposition.
"""
def __repr__(self) -> str:
def as_assumption(self, goal : Prop) -> list[list[tuple[list[Prop], Prop]]]:
"""
Create a representation of a proposition.
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: String representation of the proposition.
:rtype: str
:return: Tuples of added assumptions with a new goal.
:rtype: list[list[tuple[list[Prop], Prop]]]
"""
return self.to_str(vars=set())
return []
def contains(self, term : Term) -> bool:
def as_proof(self) -> list[list[tuple[list[Prop], Prop]]]:
"""
Determine whether a given term, value or variable is contained or
described by this proposition.
Determine which hypotheses are required in the context to prove
this proposition.
:param term: The term to look for.
:type term: Term
:return: Whether the term is contained in this proposition.
:rtype: bool
"""
return False
def normalize(self) -> Prop:
"""
Simplify the terms of a proposition.
"""
return self
def replace(self, old : Term, new : Term) -> Prop:
"""
Find any occurrence of a given term, and replace it with the new
term.
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.
:param old: The term to replace.
:type old: Term
:param new: The term to replace it with.
:type new: Term
:return: The proposition with the term replaced.
:rtype: Prop
:return: Methods to prove this proposition.
:rtype: list[tuple[list[Prop], Prop]]
"""
return self
def to_str(self, vars : set[str]) -> str:
return "<undefined prop>"
return []
@dataclass(frozen=True)
class And(Prop):
"""
The logical and-operator `P ∧ Q`.
The logical and-operator `P ^ Q`.
"""
P : Prop
Q : Prop
def __repr__(self) -> str:
"""
Create a representation of a proposition.
:return: String representation of the proposition.
:rtype: str
"""
return self.to_str(vars=set())
def contains(self, term: Term) -> bool:
return self.P.contains(term) or self.Q.contains(term)
def normalize(self) -> Prop:
"""
Simplify the terms of a proposition.
"""
return And(P=self.P.normalize(), Q=self.Q.normalize())
def replace(self, old: Term, new: Term) -> Prop:
return And(
P=self.P.replace(old=old, new=new),
Q=self.Q.replace(old=old, new=new),
)
def to_str(self, vars: set[str]) -> str:
p_str = ecsl(self.P.to_str(vars=vars))
q_str = ecsl(self.Q.to_str(vars=vars))
return f"{p_str} ∧ {q_str}"
@dataclass(frozen=True)
class Eq(Prop):
"""
@ -106,34 +60,11 @@ class Eq(Prop):
x : Term
y : Term
def __repr__(self) -> str:
"""
Create a representation of a proposition.
:return: String representation of the proposition.
:rtype: str
"""
return self.to_str(vars=set())
def contains(self, term: Term) -> bool:
return self.x.contains(term) or self.y.contains(term)
def as_assumption(self, goal: Prop) -> list[list[tuple[list[Prop], Prop]]]:
return []
def normalize(self) -> Prop:
"""
Simplify the terms of a proposition.
"""
return Eq(x=self.x.normalize(), y=self.y.normalize())
def replace(self, old: Term, new: Term) -> Prop:
return Eq(
x=self.x.replace(old=old, new=new),
y=self.y.replace(old=old, new=new),
)
def to_str(self, vars : set[str]) -> str:
x_str = ecsl(self.x.to_str(vars={ key : Var() for key in vars }))
y_str = ecsl(self.y.to_str(vars={ key : Var() for key in vars }))
return f"{x_str} = {y_str}"
def as_proof(self) -> list[list[tuple[list[Prop], Prop]]]:
return super().as_proof()
@dataclass(frozen=True)
class Exists(Prop):
@ -144,69 +75,6 @@ class Exists(Prop):
x : Callable[[Term], Prop]
def __repr__(self) -> str:
"""
Create a representation of a proposition.
:return: String representation of the proposition.
:rtype: str
"""
return self.to_str(vars=set())
def contains(self, term : Term) -> bool:
i, c = 0, Const("")
while i == 0 or term.contains(c):
i += 1
c = Const("temp_exists_variable_{i}")
return self.x(c).contains(term=term)
def normalize(self) -> Prop:
"""
Simplify the terms of a proposition.
"""
return Exists(lambda n : self.x(n).normalize())
def replace(self, old: Term, new: Term) -> Prop:
def replaced_func(input_term : Term) -> Prop:
c = unique_const(input_term=input_term)
return (
self.x(c)
.replace(old=old, new=new)
.replace(old=c, new=input_term)
)
def unique_const(input_term : Term) -> Term:
"""
Get a unique const value that doesn't interfere with either the
old term that needs to be replaced, nor with the input term.
"""
i, c = 0, Const("")
while i == 0 or input_term.contains(c) or old.contains(c):
i += 1
c = Const(f"temp_unique_value_{i}")
return c
return Exists(replaced_func)
def to_str(self, vars : set[str]) -> str:
for c in USABLE_VAR_NAMES:
if c in vars:
continue
vars.add(c)
s = self.x(Const(c)).to_str(vars=vars)
vars.remove(c)
return "∃" + c + "." + ecsl(s)
else:
raise ValueError(
"Ran out of usable var names!"
)
@dataclass(frozen=True)
class ForAll(Prop):
"""
@ -215,69 +83,6 @@ class ForAll(Prop):
x : Callable[[Term], Prop]
def __repr__(self) -> str:
"""
Create a representation of a proposition.
:return: String representation of the proposition.
:rtype: str
"""
return self.to_str(vars=set())
def contains(self, term : Term) -> bool:
i, c = 0, Const("")
while i == 0 or term.contains(c):
i += 1
c = Const("temp_forall_variable_{i}")
return self.x(c).contains(term=term)
def normalize(self) -> Prop:
"""
Simplify the terms of a proposition.
"""
return ForAll(lambda n : self.x(n).normalize())
def replace(self, old: Term, new: Term) -> Prop:
def replaced_func(input_term : Term) -> Prop:
c = unique_const(input_term=input_term)
return (
self.x(c)
.replace(old=old, new=new)
.replace(old=c, new=input_term)
)
def unique_const(input_term : Term) -> Term:
"""
Get a unique const value that doesn't interfere with either the
old term that needs to be replaced, nor with the input term.
"""
i, c = 0, Const("")
while i == 0 or input_term.contains(c) or old.contains(c):
i += 1
c = Const(f"temp_unique_value_{i}")
return c
return ForAll(replaced_func)
def to_str(self, vars : set[str]) -> str:
for c in USABLE_VAR_NAMES:
if c in vars:
continue
vars.add(c)
s = self.x(Const(c)).to_str(vars=vars)
vars.remove(c)
return "∀" + c + "." + ecsl(s)
else:
raise ValueError(
"Ran out of usable var names!"
)
@dataclass(frozen=True)
class Implies(Prop):
"""
@ -287,35 +92,6 @@ class Implies(Prop):
P : Prop
Q : Prop
def __repr__(self) -> str:
"""
Create a representation of a proposition.
:return: String representation of the proposition.
:rtype: str
"""
return self.to_str(vars=set())
def contains(self, term: Term) -> bool:
return self.P.contains(term) or self.Q.contains(term)
def normalize(self) -> Prop:
"""
Simplify the terms of a proposition.
"""
return Implies(P=self.P.normalize(), Q=self.Q.normalize())
def replace(self, old: Term, new: Term) -> Prop:
return Implies(
P=self.P.replace(old=old, new=new),
Q=self.Q.replace(old=old, new=new),
)
def to_str(self, vars: set[str]) -> str:
p_str = ecsl(self.P.to_str(vars=vars))
q_str = ecsl(self.Q.to_str(vars=vars))
return f"{p_str} → {q_str}"
@dataclass(frozen=True)
class Or(Prop):
"""
@ -324,33 +100,5 @@ class Or(Prop):
P : Prop
Q : Prop
def __repr__(self) -> str:
"""
Create a representation of a proposition.
:return: String representation of the proposition.
:rtype: str
"""
return self.to_str(vars=set())
def contains(self, term: Term) -> bool:
return self.P.contains(term) or self.Q.contains(term)
def normalize(self) -> Prop:
"""
Simplify the terms of a proposition.
"""
return Or(P=self.P.normalize(), Q=self.Q.normalize())
def replace(self, old: Term, new: Term) -> Prop:
return Or(
P=self.P.replace(old=old, new=new),
Q=self.Q.replace(old=old, new=new),
)
def to_str(self, vars: set[str]) -> str:
p_str = ecsl(self.P.to_str(vars=vars))
q_str = ecsl(self.Q.to_str(vars=vars))
return f"{p_str} ∨ {q_str}"

74
checker/terms.py
View File

@ -42,38 +42,6 @@ def contains(haystack : Term, needle : Term) -> bool:
else:
return False
def ecsl(s : str) -> str:
"""
Encapsulate something if it contains non-encapsulated spaces.
:param s: The string to potentially encapsulate.
:type s: str
:return: An encapsulated string.
:rtype: str
"""
def needs_encapsulation() -> bool:
if " " not in s:
return False
level = 0
for c in s:
match c:
case " ":
if level <= 0:
return True
case "(":
level += 1
case ")":
level -= 1
else:
return False
if needs_encapsulation():
return "(" + s + ")"
else:
return s
def normalize(term : Term) -> Term:
"""
Create a normalization function. This function simplifies functions as
@ -242,17 +210,6 @@ class Term:
"""
return self.to_str(vars={})
def contains(self, needle : Term) -> bool:
"""
Determine whether this term is or contains any given term.
:param needle: The term to look for.
:type needle: Term
:return: Whether the term is found.
:rtype: bool
"""
return contains(haystack=self, needle=needle)
def normalize(self) -> Term:
return normalize(term=self)
@ -263,7 +220,7 @@ class Term:
yield self
def to_str(self, vars : dict[str, Var]) -> str:
return "<undefined term>"
return "<undefined>"
@dataclass(frozen=True)
class App(Term):
@ -287,24 +244,10 @@ class App(Term):
yield from self.x.rec_iter()
def to_str(self, vars: dict[str, Var]) -> str:
# Reformat pre-defined common functions
match self:
case App(f=App(f=Const("Nat.add"), x=a), x=b):
return f"{ecsl(a.to_str(vars=vars))} + {ecsl(b.to_str(vars=vars))}"
# Display numbers
n, c = 0, self
while isinstance(c, App) and c.f == Const("Nat.Succ"):
n, c = n + 1, c.x
if c == Const("Nat.Zero"):
return str(n)
# elif n > 0:
# return f"{ecsl(c.to_str(vars=vars))} + {n}"
f_str = self.f.to_str(vars=vars)
x_str = self.x.to_str(vars=vars)
return f_str + " " + ecsl(x_str)
return f_str + " " + (f"({x_str})" if " " in x_str else x_str)
A1 = lambda fn, a : App(f=fn, x=a)
A2 = lambda fn, a, b : App(f=A1(fn, a), x=b)
@ -331,8 +274,6 @@ class Const(Term):
return self.to_str(vars={})
def to_str(self, vars: dict[str, Var]) -> str:
if self.name == "Nat.Zero":
return "0"
return self.name
class Lambda(Term):
@ -416,7 +357,7 @@ class Lambda(Term):
s = self.out.to_str(vars=vars)
del vars[char]
return "λ" + char + "." + ecsl(s)
return "λ" + char + "." + (f"({s})" if " " in s else s)
L1 = lambda f : Lambda(lambda x : f(x))
L2 = lambda f : Lambda(lambda x : L1(lambda y : f(x, y)))
@ -457,13 +398,10 @@ if __name__ == "__main__":
# x
print(Const("x"))
# λx.x
print(Lambda(lambda a : a))
# λx.(f x)
print(Lambda(lambda a : App(f=Const("f"), x=a)))
# λx.λy.(x y)
# λx.(λy.(x y))
print(Lambda(lambda b : Lambda(lambda c : App(f=b, x=c))))
# Nat.Succ (Nat.Succ Nat.Zero)
@ -526,12 +464,12 @@ if __name__ == "__main__":
print("\nSHORTHAND NOTATION")
print(30 * "=")
# λx.λy.λz.(x y z)
# λx.(λy.(λz.(x y z))
e = L3(lambda a, b, c : App(f=App(f=a, x=b), x=c))
print(e)
# λx.λy.λz.(x y z)
# λx.(λy.(λz.(x y z))
f = L3(lambda a, b, c : A3(L3(lambda a, b, c : A2(a, b, c)), a, b, c))
print(f)
print(f.normalize())

63
proof_checker.py
View File

@ -1,7 +1,6 @@
from checker import lib, proof, props
from checker.terms import A1, A2, App, Const
from checker.terms import A2, App, Const
from checker.lib.basic import kernel_from_int
from checker.props import Eq
# Prove : true == not false
p = proof.reflexivity(
@ -10,7 +9,7 @@ p = proof.reflexivity(
y=App(f=Const("Bool.not"), x=Const("Bool.False"))
)
)
p.check(to_stdout=True)
p.check()
# Prove : false == not true
p = proof.reflexivity(
@ -19,7 +18,7 @@ p = proof.reflexivity(
y=App(f=Const("Bool.not"), x=Const("Bool.True"))
)
)
p.check(to_stdout=True)
p.check()
# Prove : 4 + 1 == 2 + 3
p = proof.reflexivity(
@ -28,59 +27,3 @@ p = proof.reflexivity(
y=A2(Const("Nat.add"), kernel_from_int(2), kernel_from_int(3)),
)
)
p.check(to_stdout=True)
# Prove : 0 + x = x
p = proof.reflexivity(
props.Eq(
x=A2(Const("Nat.add"), kernel_from_int(0), Const("x")),
y=Const("x"),
)
)
p.check(to_stdout=True)
# Prove : x + 0 = x
# # SHOULD RAISE EXCEPTION
# p = proof.reflexivity(
# props.Eq(
# x=A2(Const("Nat.add"), Const("x"), kernel_from_int(0)),
# y=Const("x"),
# )
# )
# p.check(to_stdout=True)
case_1 = proof.eq_l(
proof=proof.reflexivity(
Eq(
x = A2(Const("Nat.add"), Const("Nat.Zero"), Const("Nat.Zero")),
y = Const("Nat.Zero")
)
),
eq=Eq(x=Const("x"), y=Const("Nat.Zero")),
statement=Eq(
x=A2(Const("Nat.add"), Const("x"), Const("Nat.Zero")),
y=Const("x")
),
)
case_1.check(is_lemma=True, to_stdout=True)
case_2 = proof.eq_l(
proof=proof.eq_l(
proof=proof.reflexivity(Eq(
x=A1(Const("Nat.Succ"), Const("n")),
y=A1(Const("Nat.Succ"), Const("n")),
)),
eq=Eq(x=A2(Const("Nat.add"), Const("n"), Const("Nat.Zero")), y=Const("n")),
statement=Eq(
x=A2(Const("Nat.add"), A1(Const("Nat.Succ"), Const("n")), Const("Nat.Zero")),
y=A1(Const("Nat.Succ"), Const("n")),
),
),
eq=Eq(x=Const("x"), y=A1(Const("Nat.Succ"), Const("n"))),
statement=Eq(
x=A2(Const("Nat.add"), Const("x"), Const("Nat.Zero")),
y=Const("x"),
),
)
case_2.check(is_lemma=True, to_stdout=True)