An Intuitionistic Micro Proof Assistant
I’ve been tinkering on a solver-oriented interactive proof assistant as a library called Knuckledragger https://github.com/philzook58/knuckledragger .
I wanted a version for intuitionistic logic to play with Bell’s infinitesimal analysis https://en.wikipedia.org/wiki/Smooth_infinitesimal_analysis . Z3 doesn’t help for this problem since it is too classical, so I started from scratch and am using Jens Otten’s nanocopi https://leancop.de/ihat/ , a prolog based prover for intuitionistic first order logic
I’m a fan of “micro” implementations like microkanren. They are more adaptable and easier to explain.
Formulas
A basic term datatype might look like this
from dataclasses import dataclass
@dataclass
class Term:
f : str
args : tuple["Term", ...]
It is nice however to enrich f to be more than a string. f are the symbols of the theory. It may be useful to associate arity, types/bounds and contracts to them. So instead we’ll use a richer type Decl
from dataclasses import dataclass
from typing import Optional, Callable
@dataclass(frozen=True, slots=True)
class Decl:
name : str
arity : int
is_var : bool = False
def __call__(self, *args : 'Term') -> 'Term':
assert len(args) == self.arity, f"Expected {self.arity} arguments, got {len(args)}"
return Term(self, args)
And0 = Decl('and', 2)
Or = Decl('or', 2)
Implies = Decl('imp', 2)
Not = Decl('not', 1)
Iff = Decl('iff', 2)
Eq = Decl('eq', 2)
NEq = Decl('neq', 2)
Add = Decl('add', 2)
Sub = Decl('sub', 2)
Mul = Decl('mul', 2)
Neg = Decl('neg', 1)
LT = Decl('lt', 2)
LE = Decl('le', 2)
Quantifiers are currently an inelegant hack. What I’m doing here doesn’t make any sense. Perhaps if I didn’t make them multi variable and added binding data to Decl this could be more principled
ForAll0 = Decl('forall', 2)
Exists0 = Decl('exists', 2)
The term datatype is long but almost only because it is so useful to have overloads. == overload is a pain. I love how it looks, but python really doesn’t want __eq__ to return anything except a bool. Shrug.
Kind of the meat is in the printer to TPTP FOF. https://tptp.org/UserDocs/TPTPWorldTutorial/LogicFOF.html . This is the format that nanocopi and many other provers accept
@dataclass(frozen=True, slots=True)
class Term:
decl : Decl
args : tuple['Term', ...]
def eq(self, other : 'Term') -> bool:
assert self.decl.name not in ["exists", "forall"] # Todo
return self.decl == other.decl and all(s.eq(o) for s, o in zip(self.args, other.args))
def __add__(self, other : 'Term') -> 'Term':
return Add(self, other)
def __sub__(self, other : 'Term') -> 'Term':
return Sub(self, other)
def __mul__(self, other : 'Term') -> 'Term':
return Mul(self, other)
def __eq__(self, other : 'Term') -> "Term":
return Eq(self, other)
def __ne__(self, other : 'Term') -> "Term":
return NEq(self, other)
def __lt__(self, other : 'Term') -> "Term":
return LT(self, other)
def __neg__(self) -> "Term":
return Neg(self)
def __str__(self) -> str:
match self.decl.name:
case 'and':
return f"({self.args[0]} & {self.args[1]})"
case 'or':
return f"({self.args[0]} | {self.args[1]})"
case 'imp':
return f"({self.args[0]} => {self.args[1]})"
case 'not':
return f"~{self.args[0]}"
case 'iff':
return f"({self.args[0]} <=> {self.args[1]})"
case "eq":
return f"({self.args[0]} = {self.args[1]})"
case "neq":
return f"({self.args[0]} != {self.args[1]})"
case "forall":
return f"![{', '.join(str(arg) for arg in self.args[0])}]: {self.args[1]}"
case "exists":
return f"?[{', '.join(str(arg) for arg in self.args[0])}]: {self.args[1]}"
if self.decl.arity == 0:
return self.decl.name
else:
return f"{self.decl.name}({', '.join(str(arg) for arg in self.args)})"
def fvs(self) -> set["Term"]:
# free variables in the expression
if self.decl.name == 'forall' or self.decl.name == 'exists':
return self.args[1].fvs() - set(self.args[0])
elif self.decl.is_var:
return {self}
else:
return set().union(*(arg.fvs() for arg in self.args))
Proof and LCF
Perhaps the most intellectually interesting piece is Proof. It is important to somehow distinguish between things to be proven and things that have been proven. A datatype with smart constructors is one such way. The is the “LCF” style. I like Harrison’s Handbook Chapter 6 as further explanation of LCF https://www.cambridge.org/core/books/abs/handbook-of-practical-logic-and-automated-reasoning/interactive-theorem-proving/E9E7F39333A72B7BF865B53724CF40C4
@dataclass(frozen=True, slots=True)
class Proof:
thm : Term
reasons : list[object]
def __repr__(self) -> str:
return "|- " + str(self.thm)
def __call__(self, *args : 'Term') -> 'Proof':
# instantiate a universally quantified theorem with specific terms
assert self.thm.decl.name == 'forall', f"Expected forall, got {self.thm.decl.name}"
assert len(args) == len(self.thm.args[0]), f"Expected {len(self.thm.args[0])} arguments, got {len(args)}"
subst = dict(zip(self.thm.args[0], args))
new_thm = substitute(self.thm.args[1], subst)
return Proof(new_thm, self.reasons + [args])
def axiom(p : Term) -> Proof:
# Ya need axioms. What can I say
assert len(p.fvs()) == 0, f"Expected closed term, got {p}, free variables: {p.fvs()}"
return Proof(p, reasons=["axiom"])
The idea of Knuckledragger is that I want the main inference rule to just be “please call trusted theorem prover”. I am not always all that interested in the low level mud of logical manipulation.
|- by1 |- by2 .... implies(and(by1,by2,...), p) nanocopi
-------------------------------------------------------------------- prove
|- p
Here I write the problem to a file, make a SWI prolog subprocess, and initiate the nanocopi main routine. I have had weird problems using a persistent prolog process (?) maybe because nanocopi isn’t meant to be rerun without tearing it down. With pipelining of the startup time, I can get around 8ms per prove. Not great, not terrible.
import subprocess
def prove(p : Term, by=[]) -> Proof:
assert isinstance(p, Term), f"Expected Term, got {p}"
assert len(p.fvs()) == 0, f"Expected closed term, got {p}, free variables: {[str(v) for v in p.fvs()]}"
with open("/tmp/prob.p", "w") as f:
for i, b in enumerate(by):
assert isinstance(b, Proof), f"Expected Proof, got {b}"
f.write(f"fof(ax{i}, axiom, {b.thm}).\n")
f.write(f"fof(goal, conjecture, {p}).\n")
# replace the path with wherever you put nanocopi
# If you aren't doing intuitionistic logic, use vampire.
res = subprocess.run(["swipl", "-O", "-g",
"assert(prolog(swi)),assert(proof(none)), asserta(logic(intu)), ['/home/philip/Downloads/nanoCoP-i-HT/nanocopi_main.pl'], call_with_time_limit(1,nanocopi_main('/tmp/prob.p',[cut,comp(6)],_)), halt"],
capture_output=True, text=True, timeout=2) # without timeout memory was leaking badly?
if "is a intu Theorem" in res.stdout:
return Proof(p, by)
else:
raise ValueError(f"Failed to prove {p} with {by}, result: {res.stdout}")
Helpers
Some helpful term constructors. I find allowed ForAll to take many arguments which go in an implication to be extremely useful
def And(*args) -> 'Term':
if len(args) == 0:
return true
elif len(args) == 1:
return args[0]
else:
return Term(And0, (args[0], And(*args[1:])))
def ForAll(vars : list['Term'], *hyp_conc) -> 'Term':
assert len(hyp_conc) >= 1
if len(hyp_conc) == 1:
return Term(ForAll0, (tuple(vars), hyp_conc[0]))
elif len(hyp_conc) == 2:
return Term(ForAll0, (tuple(vars), Implies(hyp_conc[0], hyp_conc[1])))
else:
return Term(ForAll0, (tuple(vars), Implies(And(*hyp_conc[:-1]), hyp_conc[-1])))
Here’s some helpers to match z3py naming conventions
def Const(name : str) -> Term:
return Term(Decl(name, 0), ())
def Consts(names : str) -> list[Term]:
return [Const(name) for name in names.split()]
def Function(name : str, arity : int) -> Decl:
return Decl(name, arity)
true = Const('$true')
false = Const('$false')
def Vars(names : str) -> list[Term]:
assert all(name.isupper() for name in names.split()), f"Expected uppercase variable names, got {names}"
return [Term(Decl(name, 0, is_var=True), ()) for name in names.split()]
Using It
Hey check it out, excluded middle fails! How exciting!
p = Const("p")
prove(Or(p, Not(p)))
---------------------------------------------------------------------------
ValueError Traceback (most recent call last)
Cell In[14], line 2
1 p = Const("p")
----> 2 prove(Or(p, Not(p)))
Cell In[9], line 18, in prove(p, by)
16 return Proof(p, by)
17 else:
---> 18 raise ValueError(f"Failed to prove {p} with {by}, result: {res.stdout}")
ValueError: Failed to prove (p | ~p) with [], result:
/tmp/prob.p is a intu Non-Theorem
But p => p succeeds
prove(Implies(p,p))
|- (p => p)
The beginning of Bell’s book https://www.cambridge.org/core/books/primer-of-infinitesimal-analysis/B0EF33F73CAF97C180897D2FD0AD1B6E has an axiomatization of an ordered field and some exercises.
zero, one = Consts('zero one')
a,b,c = Vars('A B C')
add_zero = axiom(ForAll([a], zero + a == a))
add_neg = axiom(ForAll([a], a + (Neg(a)) == zero))
add_comm = axiom(ForAll([a,b], a + b == b + a))
add_assoc = axiom(ForAll([a,b,c], (a + b) + c == a + (b + c)))
inv = Function("inv", 1)
mul_zero = axiom(ForAll([a], zero * a == zero))
mul_one = axiom(ForAll([a], one * a == a))
mul_comm = axiom(ForAll([a,b], a * b == b * a))
mul_assoc = axiom(ForAll([a,b,c], (a * b) * c == a * (b * c)))
mul_add = axiom(ForAll([a,b,c], a * (b + c) == (a * b) + (a * c)))
mul_inv = axiom(ForAll([a], a != zero, a * inv(a) == one))
mul_inv
# pg 19
lt_trans = axiom(ForAll([a,b,c], a < b, b < c, a < c))
lt_irrefl = axiom(ForAll([a], Not(a < a)))
add_lt_mono = axiom(ForAll([a,b,c], a < b, a + c < b + c))
mul_lt_mono = axiom(ForAll([a,b,c], a < b, zero < c, a * c < b * c))
lt_dich = axiom(ForAll([a], Or(zero < a, a < one))) # yea I dunno what to call this principle.
distinct_lt = axiom(ForAll([a,b], a != b, Or(a < b, b < a)))
le_defn = axiom(ForAll([a,b], Iff(LE(a,b), Not(b < a))))
sub_defn = axiom(ForAll([a,b], a - b == a + Neg(b)))
And now actually proving some stuff
a,b,c = Vars('A B C')
add_lt_mono_left = prove(ForAll([a,b,c], a < b, c + a < c + b), by=[add_lt_mono, add_comm])
add_zero_right = prove(ForAll([a], a + zero == a), by=[add_zero, add_comm])
#lt_zero_one = prove(ForAll([a], zero < one), by=[l])
neq_zero_one = prove(zero != one, by=[lt_dich, lt_irrefl])
lt_zero_one = prove(zero < one, by=[lt_dich, lt_irrefl])
lt_one_two = prove(one < one + one, by=[lt_zero_one, add_lt_mono, add_zero])
lt_zero_two = prove(zero < one + one, by=[lt_zero_one, lt_one_two, lt_trans])
What’s Next
Ok, so the above is just a core. A proof assistant it hardly make. There is a butt ton of infrastructure needed on top of any kernel.
Bounds and Types
Basically you do end up needing something that is a relative of a type system, even if you’re using untyped first order logic.
One trick I’ve liked is to associate bounds with variables. This auto inserts predicates forall x, bound(x) -> P and forall x, bound(x) & P using smart constructors for ForAll and Exists, something like the following.
from dataclasses import dataclass
from typing import Optional, Callable
@dataclass(frozen=True, slots=True)
class Decl:
name : str
arity : int
is_var : bool = False
bound : Callable[[Term], Term] = lambda v: true
def SmartForAll(v, body):
return ForAll(v, Implies(v.bound(v)), body)
You can also associate theorems to constants and make a tactic that traverse the term to grab all the “default” theorems associated with constants. I call these “contracts”. You can use this to use the solver as a “type checker” and maybe even a type inferrer. You can do some things that look a bit like dependent/refinement types.
https://www.philipzucker.com/refinement_kdrag1/
contracts : dict[Decl, Proof] = {}
def collect_contracts(t : Term) -> set[Proof]:
cs = set()
todo = [t]
while todo:
t = todo.pop()
if t.decl in contracts:
cs.add(contracts[t.decl])
todo.extend(t.args)
https://www.cs.ru.nl/~freek/mizar/miztype.pdf mizar soft typing https://lawrencecpaulson.github.io/2026/05/07/Mizar.html
Further Rules and Axiom Schema
To start doing more interesting stuff, you need to probably move into second order arithmetic (you can create comprehensions to turn predicates over nats into sets of the nat) and/or set theory looking (more careful schema let you comprehend over everything) things. These require comprehension schema.
Some easy other proof rules that can be useful. Avoiding the solver will be faster
def modus(ab : Proof, a : Proof) -> Proof:
assert isinstance(ab, Proof), f"Expected Proof, got {ab}"
assert isinstance(a, Proof), f"Expected Proof, got {a}"
assert ab.thm.decl.name == 'imp', f"Expected imp, got {ab.thm.decl.name}"
assert a.thm.eq(ab.thm.args[0]), f"Expected {ab.thm.args[0]}, got {a.thm}"
return Proof(ab.thm.args[1], reasons=["modus", ab, a])
def and_intro(a : Proof, b : Proof) -> Proof:
assert isinstance(a, Proof), f"Expected Proof, got {a}"
assert isinstance(b, Proof), f"Expected Proof, got {b}"
return Proof(And(a.thm, b.thm), reasons=["and_intro", a, b])
def fst(a : Proof) -> Proof:
assert isinstance(a, Proof), f"Expected Proof, got {a}"
assert a.thm.decl.name == 'and', f"Expected and, got {a.thm.decl.name}"
return Proof(a.thm.args[0], reasons=["fst", a])
def snd(a : Proof) -> Proof:
assert isinstance(a, Proof), f"Expected Proof, got {a}"
assert a.thm.decl.name == 'and', f"Expected and, got {a.thm.decl.name}"
return Proof(a.thm.args[1], reasons=["snd", a])
ptrue = prove(true)
def PAnd(*ps : Proof):
return functools.reduce(and_intro, ps, ptrue)
It is also very nice to be able to explicitly instantiate universal formula. Finding instantiations of universals is a hard problem that the solver needs to infer.
@dataclass(frozen=True, slots=True)
class Proof:
thm : Term
reasons : list[object]
def __repr__(self) -> str:
return "|- " + str(self.thm)
def __call__(self, *args : 'Term') -> 'Proof':
assert self.thm.decl.name == 'forall', f"Expected forall, got {self.thm.decl.name}"
assert len(args) == len(self.thm.args[0]), f"Expected {len(self.thm.args[0])} arguments, got {len(args)}"
subst = dict(zip(self.thm.args[0], args))
new_thm = substitute(self.thm.args[1], subst)
return Proof(new_thm, self.reasons + [args])
Axiom schema take the form of python functions that take in data and produce calls to axiom. They are outside the purview of the solver, which is a bummer.
Backwards Proof State
Making tactics can make more readable proofs or help you debug why a proof isn’t going through.
A mutable proof state object can hold the current obligations and collect up the proven sublemmas to be supplied to a final qed call that actually proves the topgoal.
Even just a have tactic + proofstate is nice way to organize lemmas.
@dataclass
class Theorem:
topgoal : Term
lemmas : list[Term] = field(default_factory=list)
def qed(self):
return prove(self.topgoal, by=self.lemmas)
def have(self, thm, by=[])
self.lemmas.append(prove(thm, by=by + self.lemmas))
return self
Implicits and Keyword Args
It might be important to allow implicits to be part of decls. One way is to associate a function that fills in other args when called with the Decl. Or one could add a meta_variable system and infer the implicits via a traversal.
Better Printing
I have hard to read, over parenthesized printing. It starts to matter a lot. You want to enable interesting syntax sometimes.
Better Parsing
It may make sense to make a lark based or other parser rather than constructing terms using python functions directly. This allows for more readable input formulas
Overloading
Yikes.
Bits and Bobbles
More narrowly speaking LCF uses abstract types to protect it’s proof objects, not mere convention of smart constructors. Python has bad protection mechanisms. But I’m interested in playing and making logic meanginful. Being a hardo about de bruijn criterion or soundness is a different (and also valid) game to play.
Full proof certificate production might be nice to avoid solver usage.
I like the library style because you have whichever familiar programming language you like (Python in this case) at your fingertips. Programming languages are very rich in features that it is fun to explore how they can be used to make proving more ergonomic.
I also kind of like making a very clear distinction between the metaprogramming language and the logic language. This is not novel, HOL Light etc are quite obviously manipulated in OCaml.
While big implementations are more useful if you are literally going to use them, micro implementations are nice if you want to modify them to custom needs. There is a constant difficult decision, something like “build or buy”, “DRY or WET”. Is it better to make a common abstraction with many hooks? Is it better to make a general purpose system really really fast so weird offlabel usages of it can be fast enough or is it better to make a simple bespoke thing that because of it’s bespokeness beats the general purpose super engineered thing? I do both, but I enjoy the simple bespoke thing because it often involves more generalizable understanding / concepts than thrashing against non generalizable irrelevancies.
t has also been nice to make the language of the solver and the language of the ITP close or identical out the outset. It reduces the amount of code needed and complexity, properties that perhaps are even more valuable in the AI age where you can get something big and complex (unnecessarily so?) at the push of a button. It is also surprisingly hard to translate between fairly minor differences in systems.
While the main Knuckledragger system was shallowly built on z3, I’m pretty curious what it looks like to swap out an SMT solver for a resolution/tableau/superposition style solver. An SMT solver’s typical strength is reams of combinatorics and not funky quantifier usage, while I have encountered more of the latter in trying to write down any unsupported abstract theory. The low latency of z3 and it’s wide spread of features and availability and packaging on numerous platforms still make it a great thing to try first. It is also killer if the goal is software verification. The theory of arrays + bitvectors is pretty OP for those purposes.
Intuitionistic logic is kind of neat and still a bit mysterious a decade in. I’ve been trying to read Bell’s Primer of Infinitesimal Analysis https://www.cambridge.org/core/books/primer-of-infinitesimal-analysis/B0EF33F73CAF97C180897D2FD0AD1B6E . It is apparently consistent to have $\eps^2 = 0$ but you have to be careful which logical principles you allow in. It is distinct from the hyperreals https://en.wikipedia.org/wiki/Hyperreal_number , which are another approach to rigorous infinitesimals and would also be fun to do.
Jens Otten https://jens-otten.de/tutorial_tableaux19/ https://leancop.de/ihat/ has been tinkering on compact Prolog based theorem provers for a while. I am not aware of a readily available intuitionistic theorem provers other than maybe to just use Rocq, Agda, Lean, Isabelle etc + their tactic systems. Somehow this approach is aesthetically displeasing to me. Maybe because the whole endeavor becomes extra insane. You’re doing lacroscopic surgery via python over into Rocq? Why exactly?
While ITPs have automation, they aren’t automated solvers. They don’t optimize for small, self contained binaries or simplicity or start up time.
One thing that is kind of disappointing about using nanocopi is that the proof objects it emits are inscrutable to me. One of the pleasures of intuitionsitc logic is that the proof objects are often kind of interesting to interpret as programs or constructions.
Alternative Formula Types
An algebraic datatype style If we want to include variables as a separate entity a typical thing might look like this
from dataclasses import dataclass
class Term:
pass
@dataclass
class App(Term):
f : str
args : tuple[Term, ...]
@dataclass
class Var(Term):
name : str
Are the free variables part of the term.
Gamma |- t just as much as they are part of the sequent etc. This is not the same as having an fvs function becasue this allows explicit weakening (redundant variables in the context that do not appear in the term itself).
@dataclass
class App(Term):
f : str
fvs : set[str]
args : tuple[Term, ...]
Arena style
It is tempting to spell out all the builtin operators as special cases. This blows up the amount of code I have to write though. It is easy on the eyes. Should Prop be made distinct from Term at the python datatype level? Not so sure. It feels like any effort to tie the host type systems to the object type system is more complication than its worth. It’s a sinkhole.
class Prop:
pass
@dataclass
class And(Prop):
left : Prop
right : Prop
# etc
@dataclass(frozen=True, slots=True)
class Decl:
name : str
arity : int | None
is_var : bool = False
infix : bool = False
from dataclasses import dataclass
from typing import Optional, Callable
@dataclass(frozen=True, slots=True)
class Decl:
name : str
arity : int | None
defn : Optional["Proof"] = None
is_var : bool = False
bound : Optional["Term"] = None # auto insert bounds in quantifiers. Not hashable? Just Term? contract?
contract : Optional["Proof"] = None
# kwargs : dict[str, object] = field(default_factory=dict)
#sort : Proof
# implicit : None | Callable[[Term], Term] = None # function to derive some args from others. I guess you could subclass it?
# is_meta : bool = False # is meta variable. Worth Distinguishing from other vars?
def __call__(self, *args : 'Term') -> 'Term':
if self.arity is not None:
assert len(args) == self.arity, f"Expected {self.arity} arguments, got {len(args)}"
return Term(self, args)
And0 = Decl('and', 2)
Or = Decl('or', 2)
Implies = Decl('imp', 2)
Not = Decl('not', 1)
Iff = Decl('iff', 2)
Eq = Decl('eq', 2)
NEq = Decl('neq', 2)
ForAll0 = Decl('forall', 2)
Exists0 = Decl('exists', 2)
Add = Decl('add', 2)
Sub = Decl('sub', 2)
Mul = Decl('mul', 2)
Neg = Decl('neg', 1)
LT = Decl('lt', 2)
# def FreshConst
# def FreshVar
# def FreshFunction
# Use a prefix users aren't allowed to use
def And(*args) -> 'Term':
if len(args) == 0:
return true
elif len(args) == 1:
return args[0]
else:
return Term(And0, (args[0], And(*args[1:])))
def ForAll(vars : list['Term'], *hyp_conc) -> 'Term':
assert len(hyp_conc) >= 1
hyp_conc = list(hyp_conc)
for v in reversed(vars):
assert v.decl.is_var, f"Expected variable, got {v}"
if v.decl.bound is not None:
hyp_conc = [v.decl.bound] + hyp_conc
if len(hyp_conc) == 1:
return Term(ForAll0, (tuple(vars), hyp_conc[0]))
elif len(hyp_conc) == 2:
return Term(ForAll0, (tuple(vars), Implies(hyp_conc[0], hyp_conc[1])))
else:
return Term(ForAll0, (tuple(vars), Implies(And(*hyp_conc[:-1]), hyp_conc[-1])))
@dataclass(frozen=True, slots=True)
class Term:
decl : Decl
args : tuple['Term', ...]
def __add__(self, other : 'Term') -> 'Term':
return Add(self, other)
def __sub__(self, other : 'Term') -> 'Term':
return Sub(self, other)
def __mul__(self, other : 'Term') -> 'Term':
return Mul(self, other)
def __eq__(self, other : 'Term') -> "Term":
return Eq(self, other)
def __ne__(self, other : 'Term') -> "Term":
return NEq(self, other)
def __lt__(self, other : 'Term') -> "Term":
return LT(self, other)
def __neg__(self) -> "Term":
return Neg(self)
def __str__(self) -> str:
match self.decl.name:
case 'and':
return f"({self.args[0]} & {self.args[1]})"
case 'or':
return f"({self.args[0]} | {self.args[1]})"
case 'imp':
return f"({self.args[0]} => {self.args[1]})"
case 'not':
return f"~{self.args[0]}"
case 'iff':
return f"({self.args[0]} <=> {self.args[1]})"
case "eq":
return f"({self.args[0]} = {self.args[1]})"
case "neq":
return f"({self.args[0]} != {self.args[1]})"
case "forall":
return f"![{', '.join(str(arg) for arg in self.args[0])}]: {self.args[1]}"
case "exists":
return f"?[{', '.join(str(arg) for arg in self.args[0])}]: {self.args[1]}"
if self.decl.arity == 0:
return self.decl.name
else:
return f"{self.decl.name}({', '.join(str(arg) for arg in self.args)})"
def fvs(self) -> set["Term"]:
if self.decl.name == 'forall' or self.decl.name == 'exists':
return self.args[1].fvs() - set(self.args[0])
elif self.decl.is_var:
return {self}
else:
return set().union(*(arg.fvs() for arg in self.args))
def substitute(term : Term, subst : dict[Term, Term]) -> Term:
if term.decl.name == 'forall' or term.decl.name == 'exists':
subst = {k: v for k, v in subst.items() if k not in term.args[0]} # helps a little, but this is still janky and wrong
if term in subst:
return subst[term]
else:
return Term(term.decl, tuple(substitute(arg, subst) for arg in term.args))
def Const(name : str) -> Term:
return Term(Decl(name, 0), ())
def Const(name : str, bound=None) -> Term:
if bound is not None:
d0 = Decl(name, 0)
bound = bound(d0())
return Term(Decl(name, 0, bound=bound), ())
return Term(Decl(name, 0, bound=bound), ())
def Consts(names : str, bound=None) -> list[Term]:
return [Const(name, bound=bound) for name in names.split()]
def Function(name : str, arity : int) -> Decl:
return Decl(name, arity)
true = Const('$true')
false = Const('$false')
def Vars(names : str, bound=None) -> list[Term]:
assert all(name.isupper() for name in names.split()), f"Expected uppercase variable names, got {names}"
vs1 = [Term(Decl(name, 0, is_var=True), ()) for name in names.split()]
if bound is None:
return vs1
else:
return [Term(Decl(name, 0, is_var=True, bound=bound(v)), ()) for v,name in zip(vs1, names.split())]
A,B,C,X,Y,Z = Vars("A B C X Y Z")
@dataclass(frozen=True, slots=True)
class Proof:
thm : Term
reasons : list[object]
def __repr__(self) -> str:
return "|- " + str(self.thm)
def __call__(self, *args : 'Term') -> 'Proof':
assert self.thm.decl.name == 'forall', f"Expected forall, got {self.thm.decl.name}"
assert len(args) == len(self.thm.args[0]), f"Expected {len(self.thm.args[0])} arguments, got {len(args)}"
subst = dict(zip(self.thm.args[0], args))
new_thm = substitute(self.thm.args[1], subst)
return Proof(new_thm, self.reasons + [args])
def axiom(p : Term) -> Proof:
assert len(p.fvs()) == 0, f"Expected closed term, got {p}, free variables: {p.fvs()}"
return Proof(p, reasons=["axiom"])
p,q,r = Consts("p q r")
def prove(p : Term, by=[]) -> Proof:
assert isinstance(p, Term), f"Expected Term, got {p}"
assert len(p.fvs()) == 0, f"Expected closed term, got {p}, free variables: {[str(v) for v in p.fvs()]}"
with open("/tmp/prob.p", "w") as f:
for i, b in enumerate(by):
assert isinstance(b, Proof), f"Expected Proof, got {b}"
f.write(f"fof(ax, axiom, {b.thm}).\n")
f.write(f"fof(goal, conjecture, {p}).\n")
res = subprocess.run(["swipl", "-O", "-g",
"assert(prolog(swi)),assert(proof(none)), asserta(logic(intu)), ['/home/philip/Downloads/nanoCoP-i-HT/nanocopi_main.pl'], call_with_time_limit(1,nanocopi_main('/tmp/prob.p',[cut,comp(6)],_)), halt"],
capture_output=True, text=True, timeout=2) # without timeout memory was leaking badly?
if "is a intu Theorem" in res.stdout:
return Proof(p, by)
else:
raise ValueError(f"Failed to prove {p} with {by}, result: {res.stdout}")
import subprocess
def cprove(p : Term, by=[]) -> Proof:
assert isinstance(p, Term), f"Expected Term, got {p}"
with open("/tmp/prob.p", "w") as f:
for i, b in enumerate(by):
assert isinstance(b, Proof), f"Expected Proof, got {b}"
f.write(f"fof(ax, axiom, {b.thm}).\n")
f.write(f"fof(goal, conjecture, {p}).\n")
return subprocess.run(["vampire", "/tmp/prob.p"], capture_output=True, text=True).stdout
_defined = set()
def declare(name):
assert name not in _defined, f"{name} already defined"
_defined.add(name)
def define(name : str, args, body):
decl = Decl(name, len(args))
defn = Proof(ForAll(args, Eq(decl(*args), body)), ["define"])
return Decl(name, len(args), defn=defn)
Neither bound nor contract make any sense.
Annot = Decl(“annot”, 2) contract makes no sense how it can traverse into scopes. Substituwting terms with vars is impossible
def contracts(self):
Weak A -> A by typing rules wprove weak A modus ponens
let inferred stuff float up to nearest quantifier
def type_weaken(p : Term, polarity) -> Term:
preds = []
@functools.cache
def worker(p, polarity):
if is_quantifier(p):
return Term(p.decl, (p.args[0], type_weaken(p.args[1])))
if p.decl.name == "imp":
return Implies(worker(p.args[0], not polarity), worker(p.args[1], polarity))
elif p.decl.name == "not":
return Not(worker(p.args[0], not polarity))
else:
if p.decl.constract is not None:
preds.append(p.decl.contract.thm(*p.args))
preds.append()
return Term(p.decl, tuple(map(worker, p.args)))
p1 = worker(p, polarity)
if polarity:
Implies(preds, p1)
else:
And(preds, p1)
def modus(ab : Proof, a : Proof) -> Proof:
assert isinstance(ab, Proof), f"Expected Proof, got {ab}"
assert isinstance(a, Proof), f"Expected Proof, got {a}"
assert ab.thm.decl.name == 'imp', f"Expected imp, got {ab.thm.decl.name}"
assert a.thm == ab.thm.args[0], f"Expected {ab.thm.args[0]}, got {a.thm}"
return Proof(ab.thm.args[1], reasons=["modus", ab, a])
def and_intro(a : Proof, b : Proof) -> Proof:
assert isinstance(a, Proof), f"Expected Proof, got {a}"
assert isinstance(b, Proof), f"Expected Proof, got {b}"
return Proof(And(a.thm, b.thm), reasons=["and_intro", a, b])
def fst(a : Proof) -> Proof:
assert isinstance(a, Proof), f"Expected Proof, got {a}"
assert a.thm.decl.name == 'and', f"Expected and, got {a.thm.decl.name}"
return Proof(a.thm.args[0], reasons=["fst", a])
def snd(a : Proof) -> Proof:
assert isinstance(a, Proof), f"Expected Proof, got {a}"
assert a.thm.decl.name == 'and', f"Expected and, got {a.thm.decl.name}"
return Proof(a.thm.args[1], reasons=["snd", a])
ptrue = prove(true)
def PAnd(*ps : Proof):
return functools.reduce(and_intro, ps, ptrue)
class Term:
vs : set(vs)
decl : Decl
args : tuple[Term, ...]
def weaken(term : Term):
# add vs
class Proof:
term : Term
def prove(term, by=[]):
for b in by:
assert isinstance(b, Proof)
assert b.term.fvs() <= term.fvs(), f"Proof {b} has free variables not in term {term}" # Or do I accumlate them?
ForAll(term.fvs(), *[by], term)
return Proof(term, by=by)
Real = Decl('real', 1)
a,b,c = Vars('A B C', Real)
zero = Const('zero')
axiom(Real(zero))
one = Const("one")
axiom(Real(one))
str(ForAll([a], zero + a == a))
'![A]: (real(A) => (add(zero, A) = A))'
Sorting. Order sorting - Obj / maude. https://belle.sourceforge.net/doc/lf91.pdf order sorted polymorphism https://lawrencecpaulson.github.io/2022/03/02/Type_classes.html https://doi.org/10.1145/158511.158698 type checking type classes nat(x) <= real(x) and so on contract telescopes
def Lambda(vs, body):
f = FreshConst
f.contract = axiom(ForAll(vs], apply(f, vs) == body))
return f
Real = Decl('real', 1)
zero, one = Consts('zero one', Real)
a,b,c = Vars('A B C', Real)
add_zero = axiom(ForAll([a], zero + a == a))
add_neg = axiom(ForAll([a], a + (Neg(a)) == zero))
add_comm = axiom(ForAll([a,b], a + b == b + a))
add_assoc = axiom(ForAll([a,b,c], (a + b) + c == a + (b + c)))
inv = Function("inv", 1)
mul_zero = axiom(ForAll([a], zero * a == zero))
mul_one = axiom(ForAll([a], one * a == a))
mul_comm = axiom(ForAll([a,b], a * b == b * a))
mul_assoc = axiom(ForAll([a,b,c], (a * b) * c == a * (b * c)))
mul_add = axiom(ForAll([a,b,c], a * (b + c) == (a * b) + (a * c)))
mul_inv = axiom(ForAll([a], a != zero, a * inv(a) == one))
mul_inv
# pg 19
lt_trans = axiom(ForAll([a,b,c], a < b, b < c, a < c))
lt_irrefl = axiom(ForAll([a], Not(a < a)))
add_lt_mono = axiom(ForAll([a,b,c], a < b, a + c < b + c))
mul_lt_mono = axiom(ForAll([a,b,c], a < b, zero < c, a * c < b * c))
lt_dich = axiom(ForAll([a], Or(zero < a, a < one)))
distinct_lt = axiom(ForAll([a,b], a != b, Or(a < b, b < a)))
le = define("le", [a,b], Not(b < a))
le
#neg_defn = axiom(ForAll([a], Neg(a) == zero - a))
sub_defn = axiom(ForAll([a,b], a - b == a + Neg(b)))
print(prove(ForAll([a], zero < a, zero != a), by=[lt_irrefl]))
real_zero = axiom(Real(zero))
real_one = axiom(Real(one))
real_add = axiom(ForAll([a,b], Real(a + b)))
add_lt_mono_left = prove(ForAll([a,b,c], a < b, c + a < c + b), by=[add_lt_mono, add_comm])
add_zero_right = prove(ForAll([a], a + zero == a), by=[add_zero, add_comm,real_zero ])
#lt_zero_one = prove(ForAll([a], zero < one), by=[l])
neq_zero_one = prove(ForAll([a], zero != one), by=[lt_dich(zero), lt_irrefl, real_zero, real_one])
lt_zero_one = prove(ForAll([a], zero < one), by=[lt_dich(zero), lt_irrefl, real_zero, real_one])
lt_one_two = prove(ForAll([a], one < one + one), by=[lt_zero_one, add_lt_mono, add_zero, real_zero,real_one])
lt_zero_two = prove(ForAll([a], zero < one + one), by=[lt_zero_one, lt_one_two, lt_trans, real_zero, real_one, real_add])
![A]: (real(A) => (add(zero, A) = A))
(real(A) => (add(zero, A) = A))
real(A)
A
(add(zero, A) = A)
add(zero, A)
zero
A
A
![A]: (real(A) => (add(zero, A) = A))
(real(A) => (add(zero, A) = A))
real(A)
A
(add(zero, A) = A)
add(zero, A)
zero
A
A
---------------------------------------------------------------------------
AssertionError Traceback (most recent call last)
Cell In[9], line 5
2 zero, one = Consts('zero one', Real)
4 a,b,c = Vars('A B C', Real)
----> 5 add_zero = axiom(ForAll([a], zero + a == a))
6 add_neg = axiom(ForAll([a], a + (Neg(a)) == zero))
7 add_comm = axiom(ForAll([a,b], a + b == b + a))
Cell In[8], line 167, in axiom(p)
166 def axiom(p : Term) -> Proof:
--> 167 assert len(p.fvs()) == 0, f"Expected closed term, got {p}, free variables: {p.fvs()}"
168 return Proof(p, reasons=["axiom"])
AssertionError: Expected closed term, got ![A]: (real(A) => (add(zero, A) = A)), free variables: {Term(decl=Decl(name='A', arity=0, defn=None, is_var=True, bound=None, contract=None), args=())}
zero, one = Consts('zero one')
a,b,c = Vars('A B C')
add_zero = axiom(ForAll([a], zero + a == a))
add_neg = axiom(ForAll([a], a + (Neg(a)) == zero))
add_comm = axiom(ForAll([a,b], a + b == b + a))
add_assoc = axiom(ForAll([a,b,c], (a + b) + c == a + (b + c)))
inv = Function("inv", 1)
mul_zero = axiom(ForAll([a], zero * a == zero))
mul_one = axiom(ForAll([a], one * a == a))
mul_comm = axiom(ForAll([a,b], a * b == b * a))
mul_assoc = axiom(ForAll([a,b,c], (a * b) * c == a * (b * c)))
mul_add = axiom(ForAll([a,b,c], a * (b + c) == (a * b) + (a * c)))
mul_inv = axiom(ForAll([a], a != zero, a * inv(a) == one))
mul_inv
# pg 19
lt_trans = axiom(ForAll([a,b,c], a < b, b < c, a < c))
lt_irrefl = axiom(ForAll([a], Not(a < a)))
add_lt_mono = axiom(ForAll([a,b,c], a < b, a + c < b + c))
mul_lt_mono = axiom(ForAll([a,b,c], a < b, zero < c, a * c < b * c))
lt_dich = axiom(ForAll([a], Or(zero < a, a < one)))
distinct_lt = axiom(ForAll([a,b], a != b, Or(a < b, b < a)))
le = define("le", [a,b], Not(b < a))
le
#neg_defn = axiom(ForAll([a], Neg(a) == zero - a))
sub_defn = axiom(ForAll([a,b], a - b == a + Neg(b)))
print(prove(ForAll([a], zero < a, zero != a), by=[lt_irrefl]))
![A]: (add(zero, A) = A)
(add(zero, A) = A)
add(zero, A)
zero
A
A
![A]: (add(A, neg(A)) = zero)
(add(A, neg(A)) = zero)
add(A, neg(A))
A
neg(A)
A
|- ![A]: (lt(zero, A) => (zero != A))
316ms -> 50ms by getting rid of startup time. That seems pretty dece. N=6 seems to be enough to cover. 50ms/6 = 8.3ms per call
50/6
8.333333333333334
%%prun
a,b,c = Vars('A B C')
add_lt_mono_left = prove(ForAll([a,b,c], a < b, c + a < c + b), by=[add_lt_mono, add_comm])
add_zero_right = prove(ForAll([a], a + zero == a), by=[add_zero, add_comm])
#lt_zero_one = prove(ForAll([a], zero < one), by=[l])
neq_zero_one = prove(ForAll([a], zero != one), by=[lt_dich(zero), lt_irrefl])
lt_zero_one = prove(ForAll([a], zero < one), by=[lt_dich(zero), lt_irrefl])
lt_one_two = prove(ForAll([a], one < one + one), by=[lt_zero_one, add_lt_mono, add_zero])
lt_zero_two = prove(ForAll([a], zero < one + one), by=[lt_zero_one, lt_one_two, lt_trans])
![A, B, C]: (lt(A, B) => lt(add(C, A), add(C, B)))
(lt(A, B) => lt(add(C, A), add(C, B)))
lt(A, B)
A
B
lt(add(C, A), add(C, B))
add(C, A)
C
A
add(C, B)
C
B
![A]: (add(A, zero) = A)
(add(A, zero) = A)
add(A, zero)
A
zero
A
![A]: (zero != one)
(zero != one)
zero
one
![A]: lt(zero, one)
lt(zero, one)
zero
one
![A]: lt(one, add(one, one))
lt(one, add(one, one))
one
add(one, one)
one
one
![A]: lt(zero, add(one, one))
lt(zero, add(one, one))
zero
add(one, one)
one
one
8324 function calls (7809 primitive calls) in 0.389 seconds
Ordered by: internal time
ncalls tottime percall cumtime percall filename:lineno(function)
12 0.367 0.031 0.367 0.031 {method 'poll' of 'select.poll' objects}
5/0 0.006 0.001 0.000 {method 'poll' of 'select.epoll' objects}
6 0.004 0.001 0.004 0.001 {built-in method _posixsubprocess.fork_exec}
18 0.001 0.000 0.001 0.000 {built-in method _io.open}
6 0.001 0.000 0.001 0.000 {method '__exit__' of '_io._IOBase' objects}
76 0.000 0.000 0.001 0.000 iostream.py:655(write)
276 0.000 0.000 0.001 0.000 <frozen posixpath>:71(join)
6 0.000 0.000 0.369 0.061 subprocess.py:2062(_communicate)
76 0.000 0.000 0.001 0.000 interactiveshell.py:3051(write)
6 0.000 0.000 0.009 0.001 base_events.py:1910(_run_once)
12 0.000 0.000 0.367 0.031 selectors.py:402(select)
6 0.000 0.000 0.007 0.001 subprocess.py:1791(_execute_child)
290/58 0.000 0.000 0.000 0.000 787023132.py:82(__str__)
24 0.000 0.000 0.000 0.000 {method 'close' of '_io.TextIOWrapper' objects}
2 0.000 0.000 0.000 0.000 {method '__exit__' of 'sqlite3.Connection' objects}
24 0.000 0.000 0.000 0.000 socket.py:623(send)
6 0.000 0.000 0.007 0.001 subprocess.py:807(__init__)
5 0.000 0.000 0.001 0.000 zmqstream.py:546(_run_callback)
5/0 0.000 0.000 0.000
Prop = Decl('prop', 1)
Real = Decl('real', 1)
sort_add = axiom(ForAll([a,b], Real(a), Real(b), Real(a + b)))
sort_mul = axiom(ForAll([a,b], Real(a), Real(b), Real(a * b)))
sort_lt = axiom(ForAll([a,b], Real(a), Real(b), Prop(a < b)))
prove(ForAll([a,b], Real(a), Real(b), Real(a + b + a + a)), by=[sort_add])
|- ![A, B]: ((real(A) & real(B)) => real(add(add(add(A, B), A), A)))
BitVec
curried apply or apply apply
Nat = Function('nat', 1)
BitVec = Function('bitvec', 2) # takes integer
#concat = Function('concat', 2)
n,m = Vars('N M', Nat)
a,b,c = Vars('A B C', lambda x: BitVec(n,x))
b = Vars('B', lambda x: BitVec(m,x))
bitvec_true = axiom(BitVec(one, true))
bitvec_false = axiom(BitVec(one, false))
add_assoc
# add_comm. Not true
bitvec_add = axiom(ForAll([n,a,b], BitVec(n + m, a + b)))
#concat(
Sorts
from dataclasses import dataclass
from typing import Optional
@dataclass(frozen=True, slots=True)
class Decl:
name : str
arity : int | None
is_var : bool = False
defn : Optional["Proof"] = None
sort : Optional["Proof"] = None
def __call__(self, *args : 'Term') -> 'Term':
if self.arity is not None:
assert len(args) == self.arity, f"Expected {self.arity} arguments, got {len(args)}"
return Term(self, args)
# Or a wrapper for later? Thee is a torublesome mutualness or circuliaty here.
@dataclass(frozen=True, slots=True)
class SDecl:
decl : Decl
sort : Proof
Prop = Decl('prop', 1)
Real = Decl('real', 1)
And0 = Decl('and', 2)
Or = Decl('or', 2)
Implies = Decl('imp', 2)
Not = Decl('not', 1)
Iff = Decl('iff', 2)
Eq = Decl('eq', 2)
NEq = Decl('neq', 2)
ForAll0 = Decl('forall', 2)
Exists0 = Decl('exists', 2)
Add = Decl('add', 2)
Sub = Decl('sub', 2)
Mul = Decl('mul', 2)
Neg = Decl('neg', 1)
LT = Decl('lt', 2)
sort_and = axiom(ForAll([a,b], Prop(a), Prop(b), Prop(a & b)))
sort_or = axiom(ForAll([a,b], Prop(a), Prop(b), Prop(a | b)))
def Function(name : str, *sorts) -> Decl:
args = [Term(Decl(f"{name}_arg{i}", 0, is_var=True), ()) for i in range(len(sorts))]
sort_proof = axiom(ForAll(args, [for sort in sorts]))
def Var(name : str, sort : Callable[[Term], Term]) -> Term:
v = Term(Decl(name, 0, is_var=True), ())
sort = prove(ForAll([v], sort(v), sort(v))) # Or even just allow it.
v = Term(Decl(name, 0, is_var=True, sort=sort), ())
#sort_axiom = axiom(ForAll([v], sort(v)))
return v
def And(*args) -> 'Term':
if len(args) == 0:
return true
elif len(args) == 1:
return args[0]
else:
return Term(And0, (args[0], And(*args[1:])))
def ForAll(vars : list['Term'], *hyp_conc) -> 'Term':
assert len(hyp_conc) >= 1
if len(hyp_conc) == 1:
return Term(ForAll0, (tuple(vars), hyp_conc[0]))
elif len(hyp_conc) == 2:
return Term(ForAll0, (tuple(vars), Implies(hyp_conc[0], hyp_conc[1])))
else:
return Term(ForAll0, (tuple(vars), Implies(And(*hyp_conc[:-1]), hyp_conc[-1])))
@dataclass(frozen=True, slots=True)
class Term:
decl : Decl
args : tuple['Term', ...]
def __add__(self, other : 'Term') -> 'Term':
return Add(self, other)
def __sub__(self, other : 'Term') -> 'Term':
return Sub(self, other)
def __mul__(self, other : 'Term') -> 'Term':
return Mul(self, other)
def __eq__(self, other : 'Term') -> "Term":
return Eq(self, other)
def __ne__(self, other : 'Term') -> "Term":
return NEq(self, other)
def __lt__(self, other : 'Term') -> "Term":
return LT(self, other)
def __neg__(self) -> "Term":
return Neg(self)
def __str__(self) -> str:
match self.decl.name:
case 'and':
return f"({self.args[0]} & {self.args[1]})"
case 'or':
return f"({self.args[0]} | {self.args[1]})"
case 'imp':
return f"({self.args[0]} => {self.args[1]})"
case 'not':
return f"~{self.args[0]}"
case 'iff':
return f"({self.args[0]} <=> {self.args[1]})"
case "eq":
return f"({self.args[0]} = {self.args[1]})"
case "neq":
return f"({self.args[0]} != {self.args[1]})"
case "forall":
return f"![{', '.join(str(arg) for arg in self.args[0])}]: {self.args[1]}"
case "exists":
return f"?[{', '.join(str(arg) for arg in self.args[0])}]: {self.args[1]}"
if self.decl.arity == 0:
return self.decl.name
else:
return f"{self.decl.name}({', '.join(str(arg) for arg in self.args)})"
def fvs(self) -> set["Term"]:
if self.decl.name == 'forall' or self.decl.name == 'exists':
return self.args[1].fvs() - set(self.args[0])
elif self.decl.is_var:
return {self}
else:
return set().union(*(arg.fvs() for arg in self.args))
def substitute(term : Term, subst : dict[Term, Term]) -> Term:
if term.decl.name == 'forall' or term.decl.name == 'exists':
subst = {k: v for k, v in subst.items() if k not in term.args[0]} # helps a little, but this is still janky and wrong
if term in subst:
return subst[term]
else:
return Term(term.decl, tuple(substitute(arg, subst) for arg in term.args))
def Const(name : str) -> Term:
return Term(Decl(name, 0), ())
def Const(name : str) -> Term:
return Term(Decl(name, 0), ())
def Consts(names : str) -> list[Term]:
return [Const(name) for name in names.split()]
def Function(name : str, arity : int) -> Decl:
return Decl(name, arity)
true = Const('$true')
false = Const('$false')
def Vars(names : str) -> list[Term]:
assert all(name.isupper() for name in names.split()), f"Expected uppercase variable names, got {names}"
return [Term(Decl(name, 0, is_var=True), ()) for name in names.split()]
A,B,C,X,Y,Z = Vars("A B C X Y Z")
@dataclass(frozen=True, slots=True)
class Proof:
thm : Term
reasons : list[object]
def __repr__(self) -> str:
return "|- " + str(self.thm)
def __call__(self, *args : 'Term') -> 'Proof':
assert self.thm.decl.name == 'forall', f"Expected forall, got {self.thm.decl.name}"
assert len(args) == len(self.thm.args[0]), f"Expected {len(self.thm.args[0])} arguments, got {len(args)}"
subst = dict(zip(self.thm.args[0], args))
new_thm = substitute(self.thm.args[1], subst)
return Proof(new_thm, self.reasons + [args])
def axiom(p : Term) -> Proof:
assert len(p.fvs()) == 0, f"Expected closed term, got {p}, free variables: {p.fvs()}"
return Proof(p, reasons=["axiom"])
p,q,r = Consts("p q r")
import subprocess
_procs = []
Warm Start
import subprocess
import threading
class NanoCopi():
def _make_proc(self):
return subprocess.Popen(
[
"swipl",
"-O",
"-g",
"""assert(prolog(swi)),assert(proof(none)),
asserta(logic(intu)), ['/home/philip/Downloads/nanoCoP-i-HT/nanocopi_main.pl']."""
],
stdout=subprocess.PIPE,
stdin=subprocess.PIPE,
)
def __init__(self, N=2):
self.index = 0
self.procs = [self._make_proc() for _ in range(N)]
self.lock = threading.Lock()
def get_proc(self):
with self.lock:
proc = self.procs[self.index]
self.procs[self.index] = self._make_proc()
self.index = (self.index + 1 ) % len(self.procs)
return proc
def prove(self, p : Term, by=[]) -> Proof:
assert isinstance(p, Term), f"Expected Term, got {p}"
assert len(p.fvs()) == 0, f"Expected closed term, got {p}, free variables: {[str(v) for v in p.fvs()]}"
try:
proc = self.get_proc()
with open("/tmp/prob.p", "w") as f: # TODO: if we want to supporting threading map, we should make this a tempfile
for i, b in enumerate(by):
assert isinstance(b, Proof), f"Expected Proof, got {b}"
f.write(f"fof(ax, axiom, {b.thm}).\n")
f.write(f"fof(goal, conjecture, {p}).\n")
res = proc.communicate(b"""call_with_time_limit(1,nanocopi_main('/tmp/prob.p',[cut,comp(6)],_)), halt.""", timeout=2)
if "is a intu Theorem" in res[0].decode():
return Proof(p, by)
else:
raise ValueError(f"Failed to prove {p} with {by}, result: {res[0].decode()}")
finally:
proc.kill()
def __del__(self):
for proc in self.procs:
proc.kill()
def multiprove(self, pfs):
from concurrent.futures import ThreadPoolExecutor
# Use max_workers to set the number of threads
with ThreadPoolExecutor(max_workers=3) as executor:
results = executor.map(lambda *args: self.prove, pfs)
return results
nc = NanoCopi(N=6)
def prove(p : Term, by=[]) -> Proof:
return nc.prove(p, by)
try:
proc = subprocess.Popen(
[
"swipl",
"-O",
"-g",
"""assert(prolog(swi)),assert(proof(none)),
asserta(logic(intu)), ['/home/philip/Downloads/nanoCoP-i-HT/nanocopi_main.pl']."""
],
stdout=subprocess.PIPE,
stdin=subprocess.PIPE,
)
#res = proc.communicate("""
#assert(prolog(swi)),assert(proof(none)),
#asserta(logic(intu)), ['/home/philip/Downloads/nanoCoP-i-HT/nanocopi_main.pl'].""", timeout=2)
res = proc.communicate(b"""call_with_time_limit(1,nanocopi_main('/tmp/prob.p',[cut,comp(6)],_)), halt.""", timeout=2)
#res = proc.communicate("halt.", timeout=2)
finally:
proc.kill()
res
What about a Theory in the non arena style
@dataclass
class Theory:
decls : list[Decl]
# terms ?
axioms: list[Proof]
pfs : list[Proof]
def Function(self, name, arity):
def axiom(self, term):
ax = axiom()
@dataclass
class Proof:
theory : Theory
f
prove(A == B) # should fail. nanocopi unfortnautely treats unbound vars as constants or something. Or existentials?
---------------------------------------------------------------------------
AssertionError Traceback (most recent call last)
Cell In[99], line 1
----> 1 prove(A == B) # should fail. nanocopi unfortnautely treats unbound vars as constants or something. Or existentials?
Cell In[98], line 148, in prove(p, by)
146 def prove(p : Term, by=[]) -> Proof:
147 assert isinstance(p, Term), f"Expected Term, got {p}"
--> 148 assert len(p.fvs()) == 0, f"Expected closed term, got {p}, free variables: {[str(v) for v in p.fvs()]}"
149 with open("/tmp/prob.p", "w") as f:
150 for i, b in enumerate(by):
AssertionError: Expected closed term, got (A = B), free variables: ['A', 'B']
prove(ForAll([A,B], A == B, ForAll([A], A == B))) # Ok, does fail.
---------------------------------------------------------------------------
ValueError Traceback (most recent call last)
Cell In[94], line 1
----> 1 prove(ForAll([A,B], A == B, ForAll([A], A == B)))
Cell In[89], line 160, in prove(p, by)
158 return Proof(p, by)
159 else:
--> 160 raise ValueError(f"Failed to prove {p} with {by}, result: {res.stdout}")
ValueError: Failed to prove ![A, B]: ((A = B) => ![A]: (A = B)) with [], result:
prove(ForAll([A,B], A == B, ForAll([C], A == B)))
|- ![A, B]: ((A = B) => ![C]: (A = B))
%%prun
prove(ForAll([a], zero < a, zero != a), by=[lt_irrefl])
---------------------------------------------------------------------------
AttributeError Traceback (most recent call last)
Cell In[82], line 1
----> 1 get_ipython().run_cell_magic('prun', '', 'prove(ForAll([a], zero < a, zero != a), by=[lt_irrefl])\n')
File ~/philzook58.github.io/.venv/lib/python3.12/site-packages/IPython/core/interactiveshell.py:2572, in InteractiveShell.run_cell_magic(self, magic_name, line, cell)
2570 with self.builtin_trap:
2571 args = (magic_arg_s, cell)
-> 2572 result = fn(*args, **kwargs)
2574 # The code below prevents the output from being displayed
2575 # when using magics with decorator @output_can_be_silenced
2576 # when the last Python token in the expression is a ';'.
2577 if getattr(fn, magic.MAGIC_OUTPUT_CAN_BE_SILENCED, False):
File ~/philzook58.github.io/.venv/lib/python3.12/site-packages/IPython/core/magics/execution.py:326, in ExecutionMagics.prun(self, parameter_s, cell)
324 arg_str += '\n' + cell
325 arg_str = self.shell.transform_cell(arg_str)
--> 326 return self._run_with_profiler(arg_str, opts, self.shell.user_ns)
File ~/philzook58.github.io/.venv/lib/python3.12/site-packages/IPython/core/magics/execution.py:348, in ExecutionMagics._run_with_profiler(self, code, opts, namespace)
346 prof = profile.Profile()
347 try:
--> 348 prof = prof.runctx(code, namespace, namespace)
349 sys_exit = ''
350 except SystemExit:
File /usr/lib/python3.12/cProfile.py:102, in Profile.runctx(self, cmd, globals, locals)
100 self.enable()
101 try:
--> 102 exec(cmd, globals, locals)
103 finally:
104 self.disable()
File <string>:1
Cell In[81], line 147, in prove(p, by)
145 def prove(p : Term, by=[]) -> Proof:
146 assert isinstance(p, Term), f"Expected Term, got {p}"
--> 147 assert len(p.fvs() == 0), f"Expected closed term, got {p}, free variables: {p.fvs()}"
148 with open("/tmp/prob.p", "w") as f:
149 for i, b in enumerate(by):
Cell In[81], line 91, in Term.fvs(self)
89 def fvs(self) -> set[Decl]:
90 if self.decl.name == 'forall' or self.decl.name == 'exists':
---> 91 return self.args[1].fvs() - set(self.args[0])
92 elif self.decl.is_var:
93 return {self}
Cell In[81], line 95, in Term.fvs(self)
93 return {self}
94 else:
---> 95 return set().union(*(arg.fvs() for arg in self.args))
Cell In[81], line 95, in <genexpr>(.0)
93 return {self}
94 else:
---> 95 return set().union(*(arg.fvs() for arg in self.args))
Cell In[81], line 95, in Term.fvs(self)
93 return {self}
94 else:
---> 95 return set().union(*(arg.fvs() for arg in self.args))
Cell In[81], line 95, in <genexpr>(.0)
93 return {self}
94 else:
---> 95 return set().union(*(arg.fvs() for arg in self.args))
AttributeError: 'Term' object has no attribute 'fvs'
%%timeit
prove(Or(p, Not(p)), by=[])
---------------------------------------------------------------------------
ValueError Traceback (most recent call last)
Cell In[27], line 1
----> 1 get_ipython().run_cell_magic('timeit', '', 'prove(Or(p, Not(p)), by=[])\n')
File ~/philzook58.github.io/.venv/lib/python3.12/site-packages/IPython/core/interactiveshell.py:2572, in InteractiveShell.run_cell_magic(self, magic_name, line, cell)
2570 with self.builtin_trap:
2571 args = (magic_arg_s, cell)
-> 2572 result = fn(*args, **kwargs)
2574 # The code below prevents the output from being displayed
2575 # when using magics with decorator @output_can_be_silenced
2576 # when the last Python token in the expression is a ';'.
2577 if getattr(fn, magic.MAGIC_OUTPUT_CAN_BE_SILENCED, False):
File ~/philzook58.github.io/.venv/lib/python3.12/site-packages/IPython/core/magics/execution.py:1222, in ExecutionMagics.timeit(self, line, cell, local_ns)
1220 for index in range(0, 10):
1221 number = 10 ** index
-> 1222 time_number = timer.timeit(number)
1223 if time_number >= 0.2:
1224 break
File ~/philzook58.github.io/.venv/lib/python3.12/site-packages/IPython/core/magics/execution.py:184, in Timer.timeit(self, number)
182 gc.disable()
183 try:
--> 184 timing = self.inner(it, self.timer)
185 finally:
186 if gcold:
File <magic-timeit>:1, in inner(_it, _timer)
Cell In[14], line 142, in prove(p, by)
140 return Proof(p, by)
141 else:
--> 142 raise ValueError(f"Failed to prove {p} with {by}, result: {res.stdout}")
ValueError: Failed to prove (p | ~p) with [], result:
/tmp/prob.p is a intu Non-Theorem
def seqprove(vs,hyps,conc,by=[]):
# This is almost certainly too cute to not be fucked (fucked = unsound).
assert all(isinstance(by, Proof) for by in by), f"Expected list of Proof, got {by}"
prove(ForAll(vs, *hyps, *[b.thm for b in by], conc))
return Proof(ForAll(vs, *hyps, conc), ["seqprove", by])
@dataclass
class Sequent:
vs : list[Term]
hyps : list[Term]
conc : Term
def __repr__(self) -> str:
return f"{', '.join(str(v) for v in self.vs)} |- {', '.join(str(h) for h in self.hyps)} =>? {self.conc}"
def term(self) -> Term:
if len(self.vs) == 0:
if len(self.hyps) == 0:
return self.conc
else:
return Implies(And(*self.hyps), self.conc)
else:
if len(self.hyps) == 0:
return ForAll(self.vs, self.conc)
else:
return ForAll(self.vs, Implies(And(*self.hyps), self.conc))
def prove(self, by=[]):
return seqprove(self.vs, self.hyps, self.conc, by=by)
from dataclasses import dataclass, field, replace
@dataclass
class ProofState:
topgoal : Sequent
todo : list[Sequent]
lemmas : list[Proof]
def __init__(self, topgoal : Sequent | Term):
if isinstance(topgoal, Term):
topgoal = Sequent([], [], topgoal)
else:
self.topgoal = topgoal
self.todo = [topgoal]
self.lemmas = []
def intro(self):
g = self.todo.pop()
name = g.conc.decl.name
if name == 'forall':
self.todo.append(replace(g, vs=g.vs + list(g.conc.args[0]), conc=g.conc.args[1]))
elif name == 'imp':
self.todo.append(replace(g, hyps=g.hyps + [g.conc.args[0]], conc=g.conc.args[1]))
elif name == "not":
self.todo.append(replace(g, hyps=g.hyps + [g.conc.args[0]], conc=false))
elif name == "neq":
self.todo.append(replace(g, hyps=g.hyps + [Eq(g.conc.args[0], g.conc.args[1])], conc=false))
elif name == "eq" or name == "iff":
self.todo.append(replace(g, hyps=g.hyps + [g.conc.args[1]], conc=g.conc.args[0]))
self.todo.append(replace(g, hyps=g.hyps + [g.conc.args[0]], conc=g.conc.args[1]))
else:
raise ValueError(f"Cannot intro on goal {g}")
return self
def have(self, p : Term, by=None):
seq = self.todo.pop()
self.todo.append(replace(seq, hyps=seq.hyps + [p]))
newgoal = replace(seq, conc=p)
if by is None:
self.todo.append(newgoal)
else:
self.lemmas.append(newgoal.prove(by=by))
return self
def auto(self, by=[]):
self.lemmas.append(self.todo.pop().prove(by=by))
return self
def __repr__(self) -> str:
if len(self.todo) == 0:
return "Done!"
return repr(self.todo[-1])
def qed(self):
return prove(self.topgoal.term(), by=self.lemmas)
#ProofState(Sequent([a], [a < one], zero < a))
p = ProofState(Sequent([], [], ForAll([a], zero < a, zero != a)))
p.intro().intro().intro().auto(by=[lt_irrefl(a)]).qed()
ProofState(ForAll([a], Iff(zero < a, -a < zero))).intro().intro().have(-a == zero - a, by=[neg_defn]).auto(by=[add_lt_mono
A |- lt(zero, A), (neg(A) = sub(zero, A)) =>? lt(neg(A), zero)
See this is worrisome:
|- (A = B)
@dataclass
class ProofZipper:
goal : Sequent
trail = field(default_factory=list)
lemmas = field(default_factory=list)
def intros(self):
if self.goal.decl.name == 'forall':
self.trail.append(self.)
nanocopi isn’t designed to clean itself up. Also maybe some Janus bug? Memory was shooting through the roof and crashing my computer.
import janus_swi as janus
def setup_nanocopi():
janus.query_once(
"set_prolog_flag(optimise,true),"
"assert(prolog(swi)),assert(proof(none))"
)
janus.consult("/home/philip/Downloads/nanoCoP-i-HT/nanocopi_main.pl")
janus.query_once("retractall(logic(_)),asserta(logic(intu))")
setup_nanocopi()
def prove(p : Term, by=[]) -> Proof:
assert isinstance(p, Term), f"Expected Term, got {p}"
with open("/tmp/prob.p", "w") as f:
for i, b in enumerate(by):
assert isinstance(b, Proof), f"Expected Proof, got {b}"
f.write(f"fof(ax, axiom, {b.thm}).\n")
f.write(f"fof(goal, conjecture, {p}).\n")
result = janus.query_once(
"with_output_to(string(_),"
"call_with_time_limit(1,"
"nanocopi_main(File,[cut,comp(6)],Result)))",
{"File": "/tmp/prob.p"},
)
janus.query_once("""
retractall(lit(_,_,_,_)),
retractall(pathlim)
""")
if result.get("Result") == "Theorem":
return Proof(p, by)
else:
raise ValueError(f"Failed to prove {p} with {by}, result: {result}")
Isthere a nice way to make proof terms as programs
def and_index(a,n):
while n > 0:
assert a.decl == "and":
a = a.args[1]
n -= 1
return a
class Sequent
vs : list[Term]
hyps : list[Term]
conc : Term
pf : Proof # |- Forall vs, implies(and(hyps), conc)
# just keep it in preparsed form
class Proof:
vs :
hyps :
conc :
def subst(self, subst):
assert subst.keys() in vs
def weaken(self, fm, n):
def
class Rule:
name :
left : list[Term | Proof]
right : list[Term | Proof]
def left():
def right():
def plug()
class ProofZipper:
trail : list[Rule]
goal :
def up
def refl():
def auto():
def intros(self):
def split(self):
def exists(self, *ts):
def prove(vs, hyps, conc, by=[]):
ForAll(vs, hyps, conc, by)
class Proof:
def __get_item__(self, idx):
return Proof(and_index(idx), ["proj", self, idx])
def Theorem(thm):
def res(pf):
Theorem(ForAll)
def mul_comm(xs, ps):
! swipl -O -g "assert(prolog(swi)),assert(proof(none)), asserta(logic(intu)), ['/home/philip/Downloads/nanoCoP-i-HT/nanocopi_main.pl'], call_with_time_limit(1,nanocopi_main('/tmp/prob.p',[cut,comp(6)],_)), halt"
/tmp/prob.p is a intu Theorem
import subprocess
res = subprocess.run(["swipl", "-O", "-g", "assert(prolog(swi)),assert(proof(none)), asserta(logic(intu)), ['/home/philip/Downloads/nanoCoP-i-HT/nanocopi_main.pl'], call_with_time_limit(1,nanocopi_main('/tmp/prob.p',[cut,comp(6)],_)), halt"], capture_output=True, text=True)
"is a intu Theorem" in res.stdout
True
prove(Implies(p,p))
#prove(Or(p, Not(p)))
#prove(Implies(And(Eq(p,q), Eq(q,r)), Eq(r,p)))
#prove(Eq(q, p))
pf1 = prove(ForAll([X], Implies(Eq(X, p), Eq(p, X))))
#p(q)
print(cprove(Implies(p,p)))
% Running in auto input_syntax mode. Trying TPTP
% Refutation found. Thanks to Tanya!
% SZS status Theorem for prob
% SZS output start Proof for prob
1. p => p [input(conjecture)]
2. ~(p => p) [negated conjecture 1]
3. ~p & p [ennf transformation 2]
4. p [cnf transformation 3]
5. ~p [cnf transformation 3]
6. $false [forward subsumption resolution 5,4]
% SZS output end Proof for prob
% ------------------------------
% Version: Vampire 5.0.1 (Release build, commit 1b13eaf on 2026-01-18 12:14:50 +0000)
% Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 NOTFOUND
% CaDiCaL version: 2.1.3
% Termination reason: Refutation
% Time elapsed: 0.0000 s
% Peak memory usage: 85 MB
% ------------------------------
% ------------------------------
|- ![A]: (lt(zero, A) => (zero != A))
The Kernel crashed while executing code in the current cell or a previous cell.
Please review the code in the cell(s) to identify a possible cause of the failure.
Click <a href='https://aka.ms/vscodeJupyterKernelCrash'>here</a> for more info.
View Jupyter <a href='command:jupyter.viewOutput'>log</a> for further details.
%%time
prove(Implies(And(Eq(p,q), Eq(q,r)), Eq(r,p)))
CPU times: user 150 ms, sys: 9.15 ms, total: 159 ms
Wall time: 154 ms
|- (((p = q) & (q = r)) => (r = p))
LJT
https://ceur-ws.org/Vol-2271/paper1.pdf https://www.cs.cmu.edu/~fp/courses/15317-f08/cmuonly/dyckhoff92.pdf
from dataclasses import dataclass
@dataclass(frozen=True, slots=True)
class Decl:
name : str
arity : int
is_var : bool = False
def __call__(self, *args : 'Term') -> 'Term':
assert len(args) == self.arity, f"Expected {self.arity} arguments, got {len(args)}"
return Term(self, args)
@dataclass(frozen=True, slots=True)
class Term:
decl : Decl
args : tuple['Term', ...]
def __str__(self) -> str:
if self.decl.arity == 0:
return self.decl.name
else:
return f"{self.decl.name}({', '.join(str(arg) for arg in self.args)})"
And = Decl('and', 2)
Or = Decl('or', 2)
Implies = Decl('imp', 2)
def Vars(names : str) -> list[Decl]:
return [Decl(name, 0, is_var=True)() for name in names.split()]
def Consts(names : str) -> list[Decl]:
return [Decl(name, 0)() for name in names.split()]
x,y,z = Vars("x y z")
p,q,r = Consts("p q r")
str(And(p,q))
def ljt(p : Term) -> bool:
def right(ctx, goal : Term) -> bool:
match goal.decl:
case Decl("and"):
return right(ctx, goal.args[0]) and right(ctx, goal.args[1])
case Decl("or"):
return right(ctx, goal.args[0]) or right(ctx, goal.args[1])
case Decl("imp"):
return right(ctx + [goal.args[0]], goal.args[1])
case _:
return left(ctx, goal)
'and(p, q)'
Arena style
Arena vs Not
Theory vs Not
Using
FuncDecl can be variable?
Many different dataclass vs 1 mondo dataclass
Getting variables where they need to go.
def pforall(vs, body, by=[]):
prove(body, by=by)
return Proof(ForAll(vs, body), by=by)
from dataclasses import dataclass, field
@dataclass(frozen=True, slots=True)
class Decl:
name : str
arity : int
is_var : bool = False
@dataclass(frozen=True, slots=True)
class DeclRef:
theory : Theory
idx : int
def __call__(self, *args : 'Term') -> 'Term':
decl = self.theory.decls.get(self.idx)
assert len(args) == decl.arity, f"Expected {decl.arity} arguments, got {len(args)}"
return Term(decl, args)
@dataclass(frozen=True, slots=True)
class Node:
declid : int
args : tuple[int, ...]
@dataclass(frozen=True, slots=True)
class TermRef:
theory : Theory
idx : int
def __str__(self) -> str:
term = self.theory.terms.get(self.idx)
decl = self.theory.decls.get(term.declid)
if decl.arity == 0:
return decl.name
else:
return f"{decl.name}({', '.join(str(self.theory.terms.get(arg)) for arg in term.args)})"
@dataclass
class Theory:
vs : list[int] = field(default_factory=list) # named variables
decls : list[Decl] #: HashCons(Decl) = field(default_factory=HashCons)
terms : list[Node] #: HashCons(Term) = field(default_factory=HashCons)
fvs : list[int] # free variable anaysis
def Function(self, name : str, arity : int) -> DeclRef:
return DeclRef(self, self.decls.add(Decl(name, arity)))
def Var(self, name : str, arity=0) -> DeclRef:
# add
return DeclRef(self, self.decls.add(Decl(name, arity, is_var=True)))
def add_term(self, decl : Decl, args : tuple['Term', ...]) -> TermRef:
self.terms.append(Term(decl, args))
self.fvs.append(self.compute_fvs(decl, args))
import kdrag as kd
import kdrag.solvers as solvers
import subprocess
from dataclasses import dataclass, field
from enum import Enum
import functools
from typing import Protocol
type FID = int
type EID = int
class Kind(Enum):
VAR = 1
APP = 2
QUANT = 3
type KID = tuple[Kind, int]
@dataclass(frozen=True)
class FuncDecl:
name: str
arity: int
infix: bool = False
# domain: tuple
# range: str
# def arity(self):
# return len(self.domain)
@dataclass
class FuncDeclRef:
th: "Theory"
idx: FID
def arity(self):
return self.th.decls[self.idx].arity
def eq(self, other: "FuncDeclRef") -> bool:
assert self.th is other.th, "Cannot compare FuncDeclRef from different theories"
return self.idx == other.idx
def __call__(self, *args: "ExprRef") -> "AppRef":
return self.th.apply(self, *args)
@dataclass(frozen=True)
class VarDecl:
name: str
sort: EID
class ExprRef(Protocol):
th: "Theory"
def __add__(self, other: "ExprRef") -> "ExprRef":
assert self.th is other.th, "Cannot add ExprRef from different theories"
f = self.th.Function("add", 2)
return f(self, other)
def __eq__(self, other: "ExprRef") -> "ExprRef":
assert self.th is other.th, "Cannot compare ExprRef from different theories"
f = self.th.Function("=", 2, infix=True)
return f(self, other)
def kid(self) -> tuple[Kind, int]:
raise NotImplementedError("kid() must be implemented by subclasses")
@dataclass(eq=False)
class VarRef(ExprRef):
th: "Theory"
idx: int
def kid(self):
return (Kind.VAR, self.idx)
@dataclass(frozen=True)
class Expr:
decl: int
args: tuple[tuple[Kind, int], ...]
@dataclass(eq=False)
class AppRef(ExprRef):
th: "Theory"
idx: int
def __repr__(self):
return self.th.tptp(self.idx)
def kid(self):
return (Kind.APP, self.idx)
@dataclass(frozen=True)
class Proof:
th: "Theory"
prop: int
by: tuple[int, ...]
axiom: bool
@dataclass
class ProofRef:
th: "Theory"
idx: int
@dataclass
class HashCons[T]:
items: list[T] = field(default_factory=list)
memo: dict[T, int] = field(default_factory=dict)
def add(self, item: T) -> int:
if item in self.memo:
return self.memo[item]
else:
idx = len(self.items)
self.items.append(item)
self.memo[item] = idx
return idx
def get(self, idx: int) -> T:
return self.items[idx]
@dataclass
class Theory:
"""
>>> th = Theory()
>>> a = th.Const("a")
>>> f = th.Function("f", 1)
>>> f(a)
f(a)
>>> a == a
(a = a)
>>> b = th.Var("B")
>>> b + a
"""
"""
Increasing the decl is a theory extension
"""
vs: list[VarDecl] = field(default_factory=list)
decls: list[FuncDecl] = field(default_factory=list)
decl_memo: dict[FuncDecl, int] = field(default_factory=dict)
terms: list[Expr] = field(default_factory=list)
term_memo: dict[Expr, int] = field(default_factory=dict)
proven: list[bool] = field(default_factory=list) # list[PID | None]
fvs: list[int] = field(default_factory=list)
theorems: list[Proof] = field(default_factory=list)
_warm_vampire: subprocess.Popen | None = None
def __post_init__(self):
self._warmup()
def Function(self, name, arity: int, infix=False, fail=True) -> FuncDeclRef:
decl = FuncDecl(name, arity, infix=infix)
if decl in self.decl_memo:
if fail:
raise ValueError(f"Function {name} with arity {arity} already exists")
else:
return FuncDeclRef(self, self.decl_memo[decl])
else:
self.decls.append(decl)
idx = len(self.decls) - 1
self.decl_memo[decl] = idx
return FuncDeclRef(self, idx)
def Const(self, name) -> AppRef:
return self.Function(name, 0)()
def Var(self, name) -> VarRef:
assert name.isupper(), "Variable names must be uppercase"
self.vs.append(name)
idx = len(self.vs) - 1
return VarRef(self, idx)
def from_kid(self, kid: KID) -> ExprRef:
kind, idx = kid
if kind == Kind.VAR:
return VarRef(self, idx)
elif kind == Kind.APP:
return AppRef(self, idx)
else:
raise ValueError(f"Unknown kind: {kind}")
def apply(self, func: FuncDeclRef, *args: ExprRef) -> AppRef:
assert all(self is arg.th for arg in args), (
"Cannot apply FuncDeclRef to ExprRef from different theories"
)
assert all(func.arity() == len(args) for arg in args), (
f"Function {func.th.decls[func.idx].name} expects {func.arity()} arguments, got {len(args)}"
)
# assert all(isinstance(arg, ExprRef) for arg in args), (
# "All arguments must be ExprRef"
# )
expr = Expr(func.idx, tuple(arg.kid() for arg in args))
if expr in self.term_memo:
return AppRef(self, self.term_memo[expr])
else:
self.terms.append(expr)
idx = len(self.terms) - 1
self.term_memo[expr] = idx
self.proven.append(False)
self.fvs.append(
functools.reduce(
lambda x, y: x | y, (self.fvs[arg.idx] for arg in args), 0
)
)
return AppRef(self, idx)
def add(self, idx1: int, idx2: int) -> ExprRef:
raise NotImplementedError("Addition of ExprRef is not implemented yet")
def axiom(self, expr: ExprRef):
self.theorems.append(Proof(self, expr.idx, (), True))
return ProofRef(self, len(self.theorems) - 1)
def _warmup(self):
if self._warm_vampire is None:
self._warm_vampire = subprocess.Popen(
[
solvers.binpath("vampire"),
"input_language",
"tptp",
"--time_limit",
"1",
"--proof",
"off",
],
)
"""
def prove(self, expr: ExprRef, by=[]) -> ProofRef:
proc = self._warm_vampire
assert proc is not None, "Vampire process is not running"
self._warm_vampire = None
self._warmup()
for p in by:
assert isinstance(p, ProofRef) and p.th is self, "ProofRef must belong to the same theory"
proc.stdin.write(f"fof(proof_{p.idx}, axiom, {self.tptp(self.proofs[p.idx].)}).\n".encode())
proc.stdin.write(f"fof(goal, conjecture, {self.tptp(expr.idx)}).\n".encode())
proc.stdin.close()
proc.wait()
if proc.returncode == 0:
else:
raise RuntimeError(f"Vampire failed with return code {proc.returncode}, {proc.stderr.read().decode()}")
"""
def tptp(self, kid: KID) -> str:
kind, idx = kid
match kind:
case Kind.VAR:
return self.vs[idx].name
case Kind.APP:
expr = self.terms[idx]
decl = self.decls[expr.decl]
if decl.infix and len(expr.args) == 2:
left = self.tptp(expr.args[0])
right = self.tptp(expr.args[1])
return f"({left} {decl.name} {right})"
if len(expr.args) != 0:
args = [self.tptp(arg) for arg in expr.args]
return f"{decl.name}({', '.join(args)})"
else:
return decl.name
case _:
raise ValueError(f"Unknown kind: {kind}")
Constraint typing. Semantics of G |- A |X C
Could use vampire to solve constraints. Query answering mode? Or Even that there exists a solution might be sufficient. Exists([], …)
aexpr bexpr
Ohad mcbride descriptions
vampire tla
box
temporal and or ite
always(and(A,B)) = (always(A) & always(B)) valid (?)
Hmm.
apply(T,X) ext
eval(x, T) x + y == y + x X + succ(Y) == succ(X + Y)
X <= Y
x in 1..2 == x = 1 \/ x = 2
But that \/ is on signals
| eval(x in 1..2, T) == eval(eq(x,1), T) | eval(eq(x,2), T) == (eval(x,T) = eval(1, T) | eval(x,T) = eval(2,T)) |
eq(x,2) is boolStream x = 2 is prop
always(eq(x,2)) = (x = 2)
https://en.wikipedia.org/wiki/Standard_translation
== in tla is tptp =
= in tla is eq
Mizar soft typing
from dataclasses import dataclass
counter = 0
def fresh_num():
global counter
counter += 1
return counter
@dataclass(frozen=True)
class MySet():
name : str
def __iter__(self):
def res():
yield Var(self, fresh_num())
return res()
@dataclass(frozen=True)
class Var():
s : MySet
name : int
@dataclass
class Comp:
it : Var
def __init__(self, it):
...
class Fun:
#C(y for x in MySet("A") for y in MySet("A"))
{x : x for x in MySet("A")}
{Var(s=MySet(name='A'), name=1): Var(s=MySet(name='A'), name=1)}
A theory is a set of sentences. So pfs is an under approximation of that. Kind of fun
@dataclass
class Theory:
sig : list[_FuncDecl]
pfs : list[_Prop]
@dataclass
class FuncDeclRef():
th: Theory
idx : int
@dataclass
class Theory:
sig : list[FuncDecl]
pfs : list[Prop]
import subprocess
from dataclasses import dataclass, field
class Prop:
ctx :
class Term:
ctx : list[Var]
@dataclass(frozen=True)
class FuncDecl:
name : str
arity : int
def __call__(self, *args):
if len(args) != self.arity:
raise ValueError(f"Function {self.name} expects {self.arity} arguments, got {len(args)}")
return App(self.name, list(args))
@dataclass(frozen=True, eq=False)
class App(Term):
decl: FuncDecl
args: list[Term]
def __repr__(self):
if self.args:
return f"{self.name}({','.join(map(repr, self.args))})"
else:
return self.name
FuncDecl("add", 2)
FuncDecl("ite", 3)
nat = Relation("nat",1)
bool = Relation("bool",1)
def
import subprocess
from dataclasses import dataclass, field
class Prop:
def __and__(self, other):
return And([self, other])
def __or__(self, other):
return Or([self, other])
def __invert__(self):
return Not(self)
def __eq__(self, other):
return Iff(self, other)
class Term:
def __eq__(self, other):
return Eq(self, other)
def __ne__(self, other):
return Not(Eq(self, other))
def __add__(self, other):
return App("add", [self, other])
@dataclass(frozen=True, eq=False)
class App(Term):
name: str
args: list[Term]
def __repr__(self):
if self.args:
return f"{self.name}({','.join(map(repr, self.args))})"
else:
return self.name
@dataclass(frozen=True)
class FuncDecl:
name : str
arity : int
def __call__(self, *args):
if len(args) != self.arity:
raise ValueError(f"Function {self.name} expects {self.arity} arguments, got {len(args)}")
return App(self.name, list(args))
@dataclass(frozen=True, eq=False)
class Var(Term):
name: str
prop : Prop | None = None
def __post_init__(self):
if not self.name.isupper():
raise ValueError("Variable names must be uppercase", self.name)
def __repr__(self):
return self.name
@dataclass(frozen=True, eq=False)
class PApp(Prop):
name: str
args: list[Term]
def __repr__(self):
if self.args:
return f"{self.name}({','.join(map(repr, self.args))})"
else:
return self.name
@dataclass(frozen=True, eq=False)
class Eq(Prop):
left: Term
right: Term
def __repr__(self):
return f"({self.left} = {self.right})"
@dataclass(frozen=True, eq=False)
class And(Prop):
children: list[Term]
def __repr__(self):
return f"({' & '.join(map(str, self.children))})"
@dataclass(frozen=True, eq=False)
class Or(Prop):
children: list[Term]
def __repr__(self):
return f"({' | '.join(map(str, self.children))})"
@dataclass(frozen=True, eq=False)
class Not(Prop):
child: Term
def __repr__(self):
return f"~({repr(self.child)})"
@dataclass(frozen=True, eq=False)
class Implies(Prop):
hyp: Term
conc: Term
def __repr__(self):
return f"({self.hyp} => {self.conc})"
@dataclass(frozen=True, eq=False)
class Iff(Prop):
left: Term
right: Term
def __repr__(self):
return f"({self.left} <=> {self.right})"
@dataclass(frozen=True, eq=False)
class ForAll(Prop):
vars: list[Var]
body: object
def __repr__(self):
return f"![{",".join(map(repr, self.vars))}]: ({self.body})"
# Could make ForAll just have these?
def QForAll(vars: list[Var], *body):
if len(body) == 1:
return ForAll(vars, body[0])
elif len(body) == 2:
return ForAll(vars, Implies(body[0], body[1]))
else:
return ForAll(vars, Implies(And(list(body[:-1])), body[-1]))
@dataclass(frozen=True, eq=False)
class Exists(Prop):
vars: list[Var]
body: object
def __repr__(self):
return f"?[{",".join(map(repr, self.vars))}]: ({self.body})"
true = App("true", [])
false = App("false", [])
@dataclass(frozen=True)
class Proof:
# ctx
# hyps
goal: Prop
by: list[object] = field(default_factory=list)
def __repr__(self):
return f"|- {self.goal}"
def __and__(self, other): # and intro
assert isinstance(other, Proof), f"Expected Proof, got {other}"
return Proof(And([self.goal, other.goal]), self.by + other.by)
def __or__(self, other): # or intro 1
assert isinstance(other, Prop)
return Proof(Or([self.goal, other]), self.by + other.by)
def __call__(self, *args): # forall and implies elim
if isinstance(self.goal, ForAll):
...
elif isinstance(self.goal, Implies):
assert isinstance(args[0], Proof), f"Expected Proof, got {args[0]}"
assert args[0].goal == self.goal.hyp, f"Expected proof of {self.goal.hyp}, got {args[0].goal}"
return Proof(self.goal.conc)(*args[1:])
def axiom(p : Prop) -> Proof:
return Proof(p, ["axiom"])
def prove(p : Prop, by=[]) -> Proof:
with open("/tmp/prob.p", "w") as f:
for i, b in enumerate(by):
assert isinstance(b, Proof), f"Expected Proof, got {b}"
f.write(f"fof(ax, axiom, {b.goal}).\n")
f.write(f"fof(goal, conjecture, {p}).\n")
res = subprocess.run(["./nanocopi-ht.sh /tmp/prob.p 1"], shell=True, cwd="/home/philip/Downloads/nanoCoP-i-HT/", capture_output=True, text=True).stdout
if "is a intu Theorem" in res:
return Proof(p, by)
else:
raise ValueError(f"Failed to prove {p} with {by}. Result: {res}")
import janus_swi as janus
class NanoCoP:
def __init__(self):
janus.query_once(
"set_prolog_flag(optimise,true),"
"assert(prolog(swi)),assert(proof(none))"
)
janus.consult("/home/philip/Downloads/nanoCoP-i-HT/nanocopi_main.pl")
janus.query_once("retractall(logic(_)),asserta(logic(intu))")
def prove_file(self, path: str) -> bool:
result = janus.query_once(
"with_output_to(string(_),"
"call_with_time_limit(1,"
"nanocopi_main(File,[cut,comp(6)],Result)))",
{"File": path},
)
return result.get("Result") == "Theorem"
_nanocop = NanoCoP()
def prove(p : Prop, by=[]) -> Proof:
with open("/tmp/prob.p", "w") as f:
for i, b in enumerate(by):
assert isinstance(b, Proof), f"Expected Proof, got {b}"
f.write(f"fof(ax, axiom, {b.goal}).\n")
f.write(f"fof(goal, conjecture, {p}).\n")
if _nanocop.prove_file("/tmp/prob.p"):
return Proof(p, by)
else:
raise ValueError(f"Failed to prove {p} with {by}")
def Consts(names: str) -> list[App]:
return [App(name, []) for name in names.split()]
def Vars(names: str) -> list[Var]:
return [Var(name) for name in names.split()]
def Function(name, arity):
def res(*args):
if len(args) != arity:
raise ValueError(f"Function {name} expects {arity} arguments, got {len(args)}")
return App(name, list(args))
return res
def Relation(name, arity):
def res(*args):
if len(args) != arity:
raise ValueError(f"Relation {name} expects {arity} arguments, got {len(args)}")
return PApp(name, list(args))
return res
def Props(names: str) -> list[PApp]:
return [PApp(name, []) for name in names.split()]
p,q,r = Props("p q r")
prove(Implies(p,p))
#prove(p | ~p)
elem = Relation("elem", 2)
emp = App("emp", [])
X,Y,Z = Vars("X Y Z")
ext = axiom(ForAll([X,Y], ForAll([Z], elem(Z, X) == elem(Z, Y)) == (X==Y)))
elem_emp = axiom(ForAll([X], ~(elem(X, emp))))
prove(~elem(emp, emp), by=[elem_emp])
upair = Function("upair", 2)
elem_upair = axiom(QForAll([X,Y,Z], elem(X, upair(Y,Z)) ==
((X==Y) | (X==Z))))
#_1 = prove(ForAll([X,Y], (elem() == (upair(X,Y) == upair(Y,X)) ), by=[ext, elem_upair])
prove(ForAll([X,Y], upair(X,Y) == upair(Y,X)), by=[ext, elem_upair])
defined = set()
def define(name, args, body):
#assert name not in defined, f"{name} already defined"
# Check for occurrence in body
if isinstance(body, Prop):
f = Relation(name, len(args))
elif isinstance(body, Term):
f = Function(name, len(args))
return f, axiom(ForAll(args, f(*args) == body))
#upair(X,Y) == upair(X,Y)
sing, sing_defn = define("sing", [X], upair(X,X))
#elem_upair
elem_sing = prove(QForAll([X, Y], elem(X, sing(Y)) == (X==Y)), by=[ext, elem_upair, sing_defn])
elem_sing
pair = define("pair", [X,Y], upair(sing(X), upair(X,Y)))
def vprove(p : Prop, by = []) -> Proof:
with open("/tmp/prob.p", "w") as f:
for i, b in enumerate(by):
assert isinstance(b, Proof), f"Expected Proof, got {b}"
f.write(f"fof(ax, axiom, {b.goal}).\n")
f.write(f"fof(goal, conjecture, {p}).\n")
res = subprocess.run(["vampire",
"--time_limit", "1",
#"--mode", "casc" ,
"--input_syntax",
"tptp" ,
"/tmp/prob.p"], capture_output=True, )
if b"SZS status Theorem" in res.stdout:
return Proof(p, ["vampire", by])
else:
raise ValueError("no proof", res.stdout.decode())
vprove(p | ~p)
|- (p | ~(p))
%%timeit
vprove(p | ~p)
9.32 ms ± 312 μs per loop (mean ± std. dev. of 7 runs, 100 loops each)
%%timeit
prove(Implies(p,p))
248 μs ± 71.3 μs per loop (mean ± std. dev. of 7 runs, 1,000 loops each)
---------------------------------------------------------------------------
ValueError Traceback (most recent call last)
Cell In[4], line 1
----> 1 get_ipython().run_cell_magic('timeit', '', 'prove(p | ~p)\n')
File ~/philzook58.github.io/.venv/lib/python3.12/site-packages/IPython/core/interactiveshell.py:2572, in InteractiveShell.run_cell_magic(self, magic_name, line, cell)
2570 with self.builtin_trap:
2571 args = (magic_arg_s, cell)
-> 2572 result = fn(*args, **kwargs)
2574 # The code below prevents the output from being displayed
2575 # when using magics with decorator @output_can_be_silenced
2576 # when the last Python token in the expression is a ';'.
2577 if getattr(fn, magic.MAGIC_OUTPUT_CAN_BE_SILENCED, False):
File ~/philzook58.github.io/.venv/lib/python3.12/site-packages/IPython/core/magics/execution.py:1222, in ExecutionMagics.timeit(self, line, cell, local_ns)
1220 for index in range(0, 10):
1221 number = 10 ** index
-> 1222 time_number = timer.timeit(number)
1223 if time_number >= 0.2:
1224 break
File ~/philzook58.github.io/.venv/lib/python3.12/site-packages/IPython/core/magics/execution.py:184, in Timer.timeit(self, number)
182 gc.disable()
183 try:
--> 184 timing = self.inner(it, self.timer)
185 finally:
186 if gcold:
File <magic-timeit>:1, in inner(_it, _timer)
Cell In[1], line 200, in prove(p, by)
198 return Proof(p, by)
199 else:
--> 200 raise ValueError(f"Failed to prove {p} with {by}")
ValueError: Failed to prove (p | ~(p)) with []
def prove(p : Prop, by=[]) -> Proof:
with open("/tmp/prob.p", "w") as f:
for i, b in enumerate(by):
assert isinstance(b, Proof), f"Expected Proof, got {b}"
f.write(f"fof(ax, axiom, {b.goal}).\n")
f.write(f"fof(goal, conjecture, {p}).\n")
janus.query_once(
"set_prolog_flag(optimise,true),"
"assert(prolog(swi)),assert(proof(none))"
)
janus.query_once("retractall(logic(_)),asserta(logic(intu))")
result = janus.query_once(
"with_output_to(string(_),"
"call_with_time_limit(1,"
"nanocopi_main(File,[cut,comp(6)],Result)))",
{"File": "/tmp/prob.p"},
)
if result.get("Result") == "Theorem":
return Proof(p, by)
else:
raise ValueError(f"Failed to prove {p} with {by}")
prove(Implies(p,p))
---------------------------------------------------------------------------
NameError Traceback (most recent call last)
Cell In[1], line 1
----> 1 def prove(p : Prop, by=[]) -> Proof:
2 with open("/tmp/prob.p", "w") as f:
3 for i, b in enumerate(by):
NameError: name 'Prop' is not defined
---------------------------------------------------------------------------
NameError Traceback (most recent call last)
Cell In[1], line 24
18 return result.get("Result") == "Theorem"
21 _nanocop = NanoCoP()
---> 24 def prove(p : Prop, by=[]) -> Proof:
25 with open("/tmp/prob.p", "w") as f:
26 for i, b in enumerate(by):
NameError: name 'Prop' is not defined
prove(Implies(p,p))
|- (p => p)
Peano
Ring Kock Lawvere
https://pi.math.cornell.edu/~oconnor/sia.pdf
x,y,z = Vars("X Y Z")
zero, one = Consts("zero one")
add_comm = axiom(ForAll([x,y], x + y == y + x))
add_assoc = axiom(ForAll([x,y,z], (x + y) + z == x + (y + z)))
add_zero = axiom(ForAll([x], x + zero == x))
zero_add = prove(ForAll([x], zero + x == x), by=[add_comm, add_zero])
mul_comm = axiom(ForAll([x,y], x * y == y * x))
mul_assoc = axiom(ForAll([x,y,z], (x * y) * z == x * (y * z)))
one_mul = axiom(ForAll([x], x * one == x))
mul_one = prove(ForAll([x], one * x == x), by=[mul_comm, one_mul])
#eps, = Consts("eps")
inf = Relation("inf", 1)
inf_defn = axiom(ForAll([x], inf(x) == (x * x == 0)))
def inf(x):
return x*x == 0
---------------------------------------------------------------------------
TypeError Traceback (most recent call last)
Cell In[76], line 11
7 add_zero = axiom(ForAll([x], x + zero == x))
9 zero_add = prove(ForAll([x], zero + x == x), by=[add_comm, add_zero])
---> 11 mul_comm = axiom(ForAll([x,y], x * y == y * x))
12 mul_assoc = axiom(ForAll([x,y,z], (x * y) * z == x * (y * z)))
13 one_mul = axiom(ForAll([x], x * one == x))
TypeError: unsupported operand type(s) for *: 'Var' and 'Var'
def kock(f):
d,a = Vars("d a")
return axiom(ForAll([d], d*d == 0, Exists([a], f(d) == f(0) + a*d)))
apply = Function("apply", 2)
def comp(f): # functional comprehension. Lambda lifting?
F,x = Vars("F X")
axiom(Exists[F], ForAll([x], apply(F,x) == f(x)))
fun = Relation("fun", 1)
def define2(name, args, body):
F = Const(name)
return axiom(And(fun(F), ForAll([args], apply(F, *args) == body)))
def ext
@dataclass(frozen=True, eq=False)
class App(Term):
name: str
args: list[Term]
def __repr__(self):
if self.args:
return f"{self.name}({','.join(map(repr, self.args))})"
else:
return self.name
@classmethod
def Var(cls, name):
@classmethod
def Const(cl, name):
return cls(name, [])
@classmethod
class Set(App):
class Real(App):
def __add__(self, other):
return Real("add", [self, other])
Real.Var("foo")
class Term:
f : str
args : list[Term] | None
infix = False
def is_var(self):
return self.args is None
@classmethod
def Var(cls, name):
return cls(name, None)
@classmethod
def Const(cls, name):
return cls(name, [])
@classmethod
def App(cls, name, args):
return cls(name, args)
class FuncDecl:
name : str
args : list[type]
range : type
def __call__(self, *args):
if len(args) != len(self.args):
raise ValueError(f"Function {self.name} expects {len(self.args)} arguments, got {len(args)}")
for i, (arg, arg_type) in enumerate(zip(args, self.args)):
if not isinstance(arg, arg_type):
raise ValueError(f"Argument {i} of function {self.name} expects type {arg_type}, got {type(arg)}")
return self.range.App(self.name, list(args))
class Prop(Term): ...
class Set(Term): ...
class Real(Term):
def __add__(self, other):
return Real("add", [self, other])
Partial logic. Carrying extra props in tags
def qprove(vs, goal, by=[]): ...
class ProofZipper:
vs : list[Var]
hyps : list[Var]
trail : list[ProofCtx]
goal : Prop
@dataclass
class Intro:
vs : list[Var]
@dataclass
class Exists:
...
class AVar(): ...
class EVar(): ...
type Ctx = list[AVar | EVar]
class App:
f : str
args : list[App]
infix = False
class Prop:
f : str
args : list[App | Prop]
infix = False
precedence = 0
def tptp(self): ...
class ForAll: ...
class Exists: ...
prove(ForAll([X,Y], upair(X,Y) == upair(X,Y)))
---------------------------------------------------------------------------
ValueError Traceback (most recent call last)
Cell In[61], line 1
----> 1 prove(ForAll([X,Y], upair(X,Y) == upair(X,Y)))
Cell In[59], line 136, in prove(p, by)
134 return Proof(p, by)
135 else:
--> 136 raise ValueError(f"Failed to prove {p} with {by}. Result: {res}")
ValueError: Failed to prove ![X,Y]: (True) with []. Result: Timeout
Proof in context makes more sense if you have Term/Prop in ctx also.
CZF IZF
Synthetic Differentials
Category stuff
Arith goals Congruence closure
Locale internal language of topoi computable functions? apply(F, X)
Temporal modal?
class Poly:
f : str
terms : dict[tuple[object, int], float]
lift : list[bool]
def __add__(self, other):
if not isinstance(other, Poly):
raise ValueError(f"Cannot add {other} to Poly")
res = Poly()
res.terms = self.terms.copy()
for k,v in other.terms.items():
if k in res.terms:
res.terms[k] += v
else:
res.terms[k] = v
return res