Using Lean like an External SMT Solver from Python
It seems that the only thing I don’t want to use Lean for is it’s main purpose. That tracks.
Anyhoo, I’m a big fan of SMT solvers https://en.wikipedia.org/wiki/Satisfiability_modulo_theories . They are the workhouse behind 90% of automated software verification tooling. Three popular solvers probably account for a majority of usage, Z3, CVC5, and Bitwuzla.
One can use them by writing an SMTLib file and calling a subprocess of the solver.
Lean can be used in the same way now thanks to the grind tactic. I think this is an interesting angle. Not everyone is going to switch whole hog into using Lean. But by writing a short lean file analogous to an SMTLib one, you can kind of dip your toe in while staying in your language of choice (python, C++, scala, haskell, whatever). Lean offers more extensibility compared to an SMTLib and a huge library of functionality. You can also have the backstop of going interactive if you truly must. This is kind of using Lean as a Why3 https://www.why3.org/ in that regard.
Brief SMT Spiel
On initial introduction, SMT solvers are usually presented as puzzle / constraint solvers. Things like Sudoku or package versioning or n-queens can be encoded into the solver and you seek a solution (the solver returns SAT) to the given problem.
from z3 import *
# We know each queen must be in a different row.
# So, we represent each queen by a single integer: the column position
Q = [ Int(f"Q_{row + 1}") for row in range(8) ]
# Each queen is in a column {1, ... 8 }
val_c = [ And(1 <= Q[row], Q[row] <= 8) for row in range(8) ]
# At most one queen per column
col_c = [ Distinct(Q) ]
# Diagonal constraint
diag_c = [ If(i == j,
True,
And(Q[i] - Q[j] != i - j, Q[i] - Q[j] != j - i))
for i in range(8) for j in range(i) ]
s = Solver()
s.add(val_c + col_c + diag_c)
print(s.check())
s.model()
sat
[Q_3 = 8, Q_1 = 4, Q_7 = 5, Q_8 = 7, Q_5 = 1, Q_4 = 6, Q_2 = 2, Q_6 = 3]
When you want to do verification or theorem proving, you are seeking counterexamples. You do this by asserting the negation of the theorem in question. The theorem being proven is getting back unsat from the solver, saying that there are no counterexamples.
s = Solver()
p,q = Bools("p q")
s.add(Not(Implies(And(p,q), p)))
print(s.check())
unsat
In addition to the bindings, you can also use a textual format, SMTLIB https://smt-lib.org/ . Making files like this can be useful for inspecting the problems and is easier than developing bindings for a new language.
%%file /tmp/test.smt2
(declare-const p Bool)
(declare-const q Bool)
(assert (not (=> (and p q) p)))
(check-sat)
Writing /tmp/test.smt2
! z3 /tmp/test.smt2
unsat
We can also dump files out of the solver using the bindings. I have found this useful because I have used systems enmeshed with z3, but want to try another solver, or want to fiddle with my encoding to see if I can make it work better without changing the code of the generator.
s = Solver()
p,q = Bools("p q")
s.add(Not(Implies(And(p,q), p)))
print(s.sexpr())
(declare-fun p () Bool)
(declare-fun q () Bool)
(assert (not (=> (and p q) p)))
Using Lean
But we can also spit out lean files.
The advent of the grind tactic https://lean-lang.org/doc/reference/4.22.0-rc2//The--grind--tactic/#grind makes this more compelling. By and large, the most powerful automation of interactive theorems provers has been made by using external solvers. It is a bit unclear if the runaround of emitting the language of the ITP is worth doing compared to just emitting the solver language (smtlib or tptp).
grind however is a native general purpose lean tactic written by Leo de Moura, one of the authors of Z3. My impression is that it is kind of like an SMT solver without the SAT part, a communicating pile of theories communicating through the fabric of an e-graph /congruence closure.
I also suspect it will deal less well than existing SMT solvers with reams of garbage like software verifiers produce. https://lean-lang.org/doc/reference/4.22.0-rc2//The--grind--tactic/What--grind--is--not-___/ But for smaller queries or more nuanced quantifier queries, maybe the different emphasis wins out. I’ve been using SMT solvers in a somewhat unusual way in my project knuckledragger and I suspect they are similarly used in projects like F* or Dafny where really they are pretty small queries with more equational content than the bulk bit blasting like queries that come out of something like a model checker.
Lean also recently gained bv_decide which is powered by the SAT solver cadical. It is actually still kind of intriguing because Lean offers modelling features that honestly would have been kind of gosh darn nice. SMTLib is both extremely rich in that it is basically a full Higher order logic, but also pretty impoverished in terms of syntactic niceties.
The BitVec type does enable you to do arbitrary size bitvector reasoning, a desired feature by compiler verifiers. I would assume this cannot be bit blasted by bv_decide however. How would you?
%%file /tmp/test.lean
theorem mytheorem (p q : Prop) : p ∧ q → p := by grind
#check mytheorem
Overwriting /tmp/test.lean
You can see this passes in a human readable form
! lean /tmp/test.lean
mytheorem (p q : Prop) : p ∧ q → p
Or you can use json output to make something more easily consumable by another tool.
! lean /tmp/test.lean --json
{"severity":"information","pos":{"line":3,"column":0},"kind":"[anonymous]","keepFullRange":false,"isSilent":false,"fileName":"/tmp/test.lean","endPos":{"line":3,"column":6},"data":"mytheorem (p q : Prop) : p ∧ q → p","caption":""}
This is what it looks like to try and prove a false theorem
%%file /tmp/test2.lean
theorem mytheorem (p q : Prop) : p \/ q -> p := by grind
#check mytheorem
Overwriting /tmp/test2.lean
! lean /tmp/test2.lean
/tmp/test2.lean:2:51: error: `grind` failed
case grind
p q : Prop
h : p ∨ q
h_1 : ¬p
⊢ False
[grind] Goal diagnostics
[facts] Asserted facts
[prop] p ∨ q
[prop] ¬p
[eqc] True propositions
[prop] q
[prop] p ∨ q
[eqc] False propositions
[prop] p
mytheorem (p q : Prop) : p ∨ q → p
! lean /tmp/test2.lean --json
{"severity":"error","pos":{"line":2,"column":51},"kind":"[anonymous]","keepFullRange":false,"isSilent":false,"fileName":"/tmp/test2.lean","endPos":{"line":2,"column":56},"data":"`grind` failed\ncase grind\np q : Prop\nh : p ∨ q\nh_1 : ¬p\n⊢ False\n[grind] Goal diagnostics\n [facts] Asserted facts\n [prop] p ∨ q\n [prop] ¬p\n [eqc] True propositions\n [prop] q\n [prop] p ∨ q\n [eqc] False propositions\n [prop] p","caption":""}
{"severity":"information","pos":{"line":3,"column":0},"kind":"[anonymous]","keepFullRange":false,"isSilent":false,"fileName":"/tmp/test2.lean","endPos":{"line":3,"column":6},"data":"mytheorem (p q : Prop) : p ∨ q → p","caption":""}
We can wrap this up into a Solver object if you’re willing to just inject strings into the thing. Here I’m using it in the refutational style as I did with Z3. When check is called, it just prints the negation of all of the theorems you have added.
from dataclasses import dataclass, field
import subprocess
import json
@dataclass
class LeanSolver():
imports : list[str] = field(default_factory=list)
asserts : list[str] = field(default_factory=list)
tactic : str = "grind"
def add(self, expr: str):
self.asserts.append(expr)
def check(self):
with open('/tmp/test.lean', 'w') as f:
for imp in self.imports:
f.write(f'import {imp}\n')
f.write("theorem mythm : Not (True ")
for expr in self.asserts:
f.write(' /\\ \n')
f.write(expr)
f.write(f') := by {self.tactic}\n')
f.write('#check mythm\n')
f.flush()
result = subprocess.run(['lean', '--json', '/tmp/test.lean'], capture_output=True, text=True)
if result.returncode != 0:
return "unknown"
#raise ValueError(result.stderr)
else:
result = json.loads(result.stdout)
# just a little sanity checking.
assert result["severity"] == "information"
assert "mythm" in result["data"]
return "unsat"
s = LeanSolver()
s.add("Not (forall x y : Nat, x + y = y + x)")
s.check()
'unsat'
! cat /tmp/test.lean
theorem mythm : Not (True /\
Not (forall x y : Nat, x + y = y + x)) := by grind
#check mythm
Printing Lean out of the Z3Py AST
But really I want a drop in replacement for Z3. A interesting emergent design principle of Knuckledragger was to just use the Z3 term and formulas as my terms and formulas. To use other solvers, I just make a new pretty printer out of the Z3 AST. I’ve done this previously to emit TPTP so I can try using Vampire and E-prover and others https://github.com/philzook58/knuckledragger/blob/main/kdrag/solvers/__init__.py so I could reuse functionality from there (BaseSolver etc). By and large my conclusion thus far has been the delta in solving power compared to z3 combined with the remaining jankiness of the translation is just not worth it.
One small translational hiccup is that SMTLib represents propositions as Bool, whereas Lean uses Prop. It is a bit confusing to even navigate the conceptual differences represented by this choice. The things in Bool are true and false. The things in Prop are the propositions themselves, which in turn hold proof objects.
Some other things that are goofy in the translation
- We need our uninterpreted sorts to have decidable equality and be inhabited
- Accessors and recognizers are part of the theory of datatypes. Lean will not be happy about this style. I at least tried generating accessors that return a
defaultvalue if you’re in the wrong constructor.
There are some ways to translate between the two in Init.Classical https://leanprover-community.github.io/mathlib4_docs/Init/Classical.html in particular propDecidable and decide (thanks to Cody Roux for the tips). The main place I think I need these is in forall and exists as I’m not sure what the computable version of them would be for infinite domains like Nat. Lean is also auto coercing between Prop and Bool for me sometimes.
The translation from smt code is at the end of the post and here https://github.com/philzook58/knuckledragger/blob/main/kdrag/printers/lean.py
from kdrag.all import *
import kdrag.printers.lean as lean
from kdrag.solvers import BaseSolver, collect_sorts, collect_decls, predefined_names
from dataclasses import dataclass, field
import subprocess
import json
class LeanSolver(BaseSolver):
def __init__(self):
self.imports = []
self.tactic = "grind" # can replace by bv_decide or even tactic script. The string is just spliced in.
super().__init__()
def check(self):
with open('/tmp/test.lean', 'w') as f:
for imp in self.imports:
f.write(f'import {imp}\n')
f.write("set_option linter.unusedVariables false\n") # To remove an warning
predefined = set()
# make inductive datatype definitions
for sort in collect_sorts(
self.adds + [thm for thm, name in self.assert_tracks]
):
if isinstance(sort, smt.DatatypeSortRef):
f.write(lean.of_datatype(sort))
f.write("open " + sort.name() + "\n")
for n in range(sort.num_constructors()):
cons = sort.constructor(n)
predefined.add(cons)
for i in range(cons.arity()):
f.write(lean.accessor_def(sort, n, i))
predefined.add(sort.accessor(n,i))
elif sort.name() not in self.predefined_sorts:
f.write(lean.sort_axiom(sort))
# state axioms for all non predefined declarations
for decl in collect_decls(self.adds + [thm for thm, name in self.assert_tracks]):
if decl not in predefined and decl.name() not in predefined_names:
f.write(lean.decl_axiom(decl))
# Make the actual goal
f.write("theorem mythm : Not (True ")
for expr in self.adds + [thm for thm, name in self.assert_tracks]:
f.write(' /\\ \n')
f.write(lean.of_expr(expr))
f.write(f') := by {self.tactic}\n')
f.write('#check mythm\n')
f.flush()
result = subprocess.run(['lean', '--json', '/tmp/test.lean'], capture_output=True, text=True)
if result.returncode != 0:
return smt.unknown
else:
result = json.loads(result.stdout)
assert result["severity"] == "information"
assert "mythm" in result["data"]
return smt.unsat
Here’s a simple commutativity problem
x,y,z = smt.Ints("x y z")
s = LeanSolver()
s.add(smt.Not(smt.ForAll([x,y], x + y == y + x)))
assert s.check() == smt.unsat
This is what it generates. Somewhat ugly lean.
! cat /tmp/test.lean
set_option linter.unusedVariables false
theorem mythm : Not (True /\
(not (Classical.propDecidable (∀ (x : Int) (y : Int), (((x : Int) + (y : Int)) = ((y : Int) + (x : Int))))).decide)) := by grind
#check mythm
But the output cleans it up a little of you want to see it.
! lean /tmp/test.lean
mythm : ¬(True ∧ (!decide (∀ (x y : Int), x + y = y + x)) = true)
Here’s a pile of little queries just to sanity check the thing. I haven’t used it at much scale and there are definitely remaining problems.
s = LeanSolver()
x,y,z = smt.Bools("x y z")
s.add(smt.Not(smt.ForAll([x], x == x)))
assert s.check() == smt.unsat
x,y,z = smt.Ints("x y z")
s = LeanSolver()
s.add(smt.Not(smt.ForAll([x,y], x + y == y + x)))
assert s.check() == smt.unsat
s = LeanSolver()
s.add(smt.Not(smt.ForAll([x,y], x + 1 >= x)))
s.check()
s = LeanSolver()
x,y,z = smt.Bools("x y z")
s.add(smt.Not(smt.Implies(smt.And(x, y), x)))
s.check()
s = LeanSolver()
x,y,z = smt.Bools("x y z")
s.add(smt.Not(smt.Implies(smt.Or(x, y), x)))
assert s.check() != smt.unsat
s = LeanSolver()
x,y,z = smt.Bools("x y z")
s.add(smt.Not(smt.Implies(x, smt.Or(x, y, z))))
assert s.check() == smt.unsat
def testit(expr):
s = LeanSolver()
s.add(expr)
res = s.check()
assert res == smt.unsat, f"Expected unsat, got {res} for {expr}"
testit(smt.Not(smt.ForAll([x,y], x + y == y + x)))
x,y,z = smt.BitVecs("x y z", 8)
testit(smt.Not(smt.ForAll([x,y], x + y == y + x)))
testit(smt.Not(smt.ForAll([x,y], x | x == x)))
# uninterpreted functions
x,y,z = smt.Ints("x y z")
f = smt.Function("f", smt.IntSort(), smt.IntSort())
s = LeanSolver()
s.add(smt.ForAll([x], f(x) == x))
s.add(smt.Not(f(f(y)) == y))
assert s.check() == smt.unsat
# Uninterpreted sorts
S = smt.DeclareSort("S")
n = smt.Const("n", S)
f = smt.Function("f", S, S)
s = LeanSolver()
s.add(f(n) == n)
s.add(f(f(n)) != n)
assert s.check() == smt.unsat
# Inductive Datatypes
#from kdrag.theories.nat import Nat
MyNat = smt.Datatype("MyNat")
MyNat.declare("Z")
MyNat.declare("S", ("pred", MyNat))
MyNat = MyNat.create()
n = smt.Const("n", MyNat)
s = LeanSolver()
s.add(smt.Not(smt.ForAll([n], MyNat.S(n).pred == n)))
assert s.check() == smt.unsat
It’s not all rosy. You can put your foot into potholes pretty fast. Maybe there is a way to fix it. It seems like this existential goal trips it up. Maybe a little fiddling would fix it.
s = LeanSolver()
s.add(smt.Not(smt.Exists([n], n.pred == MyNat.Z))) # can't do this one?
s.check()
unknown
! cat /tmp/test.lean
set_option linter.unusedVariables false
inductive MyNat : Type where
| Z : MyNat
| S : MyNat -> MyNat
deriving BEq, Inhabited, Repr, DecidableEq, Inhabited
open MyNat
@[grind]
def pred : MyNat -> MyNat
| .S x => x
| _ => default
theorem mythm : Not (True /\
(not (Classical.propDecidable (∃ (n : MyNat), ((pred (n : MyNat)) = (Z : MyNat)))).decide)) := by grind
#check mythm
! lean /tmp/test.lean
/tmp/test.lean:14:98: error: `grind` failed
case grind
h : ∀ (x : MyNat), ¬pred x = Z
⊢ False
[grind] Goal diagnostics
[facts] Asserted facts
[prop] ∀ (x : MyNat), ¬pred x = Z
[eqc] True propositions
[prop] ∀ (x : MyNat), ¬pred x = Z
[ematch] E-matching patterns
[thm] h: [pred #0]
[thm] h: [pred #0]
mythm : ¬(True ∧ (!decide (∃ n, pred n = Z)) = true)
Bits and Bobbles
Isabelle can be used a similar way, see below.
Maybe a less antisocial thing for me to do would be to add a Lean backend to PySMT. https://github.com/pysmt/pysmt . PySMT does not bring me joy, sorry.
Some smt resources
- https://colab.research.google.com/github/philzook58/z3_tutorial/blob/master/Z3%20Tutorial.ipynb
- https://microsoft.github.io/z3guide/docs/logic/intro/
- https://cvc5.github.io/tutorials/beginners/
- https://smt.st/
Lean-smt https://github.com/ufmg-smite/lean-smt https://arxiv.org/abs/2505.15796 must have already spanned the smt-lean gap in multiple ways. I’m trying to really go the other direction, the dual of lean-smt. I wonder if I can leverage that? Libraries are problematic in Lean and for my purposes
Lean as an smt solver.
SMT -> lean printer Wrap in solver object lemma.ipynb might have stuff
If you’re like me, maybe this is a way to dip your toe into that Lean hotness.
Maybe my story is “deep math in lean” “shallow math in knuckeldragger”
lean is a fun and natural extraction target also for knuckeldragger. I can dynlink into it to get fast execution of knuckledragger. A truly perverse architecture.
Not sure what to do about Reals. mathlib has em. Lean Std don’t. Does grind even recognize anything special?
Lean might also be useful as a well packaged termination checker, something I’ve punted on for a while. I included aprove, but never did much with it. It isn’t clear how to use aprove without exposing all definitions. Maybe that’s the thing to do.
It is nice when grind isn’t working to flip into interactive lean to try to figure out why. Sometimes it doesn’t have enough, sometimes the thing you said is wrong. I hope knuckeldragger might be useful in a similar way for SMTLIB. I needed to build by backward tactic system to understand where the solver go stumped (in addition to figuring out the write induction hypotheses and stuff) or get convinced how I stated the wrong goal.
%%file /tmp/test.lean
theorem mythm (x y : Nat) : x + y = y + x := by grind
#check mythm
Overwriting /tmp/test.lean
! lean --json /tmp/test.lean
{"severity":"information","pos":{"line":3,"column":0},"kind":"[anonymous]","keepFullRange":false,"isSilent":false,"fileName":"/tmp/test.lean","endPos":{"line":3,"column":6},"data":"mythm (x y : Nat) : x + y = y + x","caption":""}
%%file /tmp/test.lean
#eval 1 + 1
Overwriting /tmp/test.lean
It’s pretty slow. It’s dominated by lean boot time I think at least for trivial queries. Haven’t dug into depth. pypantograph or something that keeps a live lean session would be faster.
%%timeit
result = subprocess.run(['lean', '--json', '/tmp/test.lean'], capture_output=True, text=True)
196 ms ± 6.31 ms per loop (mean ± std. dev. of 7 runs, 10 loops each)
%%file /tmp/test.lean
def mytheorem (x y : Nat) : x + y = y + x := by grind
Overwriting /tmp/test.lean
%%timeit
result = subprocess.run(['lean', '--json', '/tmp/test.lean'], capture_output=True, text=True)
195 ms ± 10.9 ms per loop (mean ± std. dev. of 7 runs, 1 loop each)
%%timeit
result = subprocess.run(['echo', 'hello world'], capture_output=True, text=True)
1.1 ms ± 14.4 μs per loop (mean ± std. dev. of 7 runs, 1,000 loops each)
CompletedProcess(args=['echo', 'hello world'], returncode=0, stdout='hello world\n', stderr='')
try out some of my z3 tutorial stuff.
---------------------------------------------------------------------------
AssertionError Traceback (most recent call last)
Cell In[2], line 74
72 testit(smt.Not(smt.ForAll([x,y], x + y == y + x)))
73 testit(smt.Not(smt.ForAll([x,y], x | x == x)))
---> 74 testit(smt.Not(smt.ForAll([x,y], x + 1 >= x)))
Cell In[2], line 42, in testit(expr)
40 s.add(expr)
41 res = s.check()
---> 42 assert res == smt.unsat, f"Expected unsat, got {res} for {expr}"
AssertionError: Expected unsat, got unknown for Not(ForAll([x, y], x + 1 >= x))
! cat /tmp/test.lean
set_option linter.unusedVariables false
theorem mythm : Not (True /\
(not (Classical.propDecidable (∀ (x : (BitVec 8)) (y : (BitVec 8)), ((bvadd (x : (BitVec 8)) (y : (BitVec 8))) = (bvadd (y : (BitVec 8)) (x : (BitVec 8)))))).decide)) := by grind
#check mythm
Py pantograph
Pantograph is a more complete lean binding that can take in strings. This might be a better for faster thing than opening up new processes, but otherwise for my purposes feels about the same?
https://github.com/stanford-centaur/PyPantograph
https://arxiv.org/abs/2410.16429
import nest_asyncio
nest_asyncio.apply() # some funkiness about async using in a jupyuter notebook.
from pantograph.server import Server
server = Server()#imports=['Init'])
state0 = server.goal_start("forall (p q: Prop), Or p q -> Or q p")
state1 = server.goal_tactic(state0, goal_id=0, tactic="intro")
print(state1)
p✝ : Prop
⊢ ∀ (q : Prop), p✝ ∨ q → q ∨ p✝
from pantograph.server import Server
server = Server()#imports=['Init'])
state0 = server.goal_start("forall (p q: Prop), Or p q -> Or q p")
print(state0.goals)
state1 = server.goal_tactic(state0, goal_id=0, tactic="grind")
state1.goals
server = Server()#imports=['Init'])
state0 = server.goal_start("forall (p q: Prop), Or q p -> p")
print(state0.goals)
state1 = server.goal_tactic(state0, goal_id=0, tactic="grind")
state1.goals
from kdrag.all import *
class LeanSolver():
def __init__(self):
self.server = Server()
self.goals
def add(self, goal):
self.goals.append(goal)
def check(self):
state0 = self.server.goal_start(smt.Not(smt.And(self.goals)))
try:
state1 = self.server.goal_tactic(state0, goal_id=0, tactic="grind")
if len(state1.goals) == 0:
return smt.unsat
else:
return smt.unknown
except Exception as e:
return smt.unknown
A different direction to go is import of Lean theorems. Somehow convert them to smtlib
https://arxiv.org/pdf/2505.15796
Isabelle
I tried a while back top use Isabelle in a similar wya. I’m just not as familiar with it. Isabelle does have a reputation of being some of the best automation available for an ITP
isabelle process -T
! ~/Downloads/Isabelle2025_linux/Isabelle2025/bin/isabelle tptp_sledgehammer
Usage: isabelle tptp_sledgehammer TIMEOUT FILES
Runs Sledgehammer on TPTP problems.
Each problem is allocated at most TIMEOUT seconds.
%%file /tmp/Test.thy
theory Test
imports Main
begin
theorem mytheorem: " 1 + 1 = 2" by auto
theorem mytheorem2: " 1 + 1 = 2"
sledgehammer
by auto
end
Overwriting /tmp/Test.thy
The bootup time for Isabelle seems a bit slow (3s). Would probably want it being kept online, which complicates things.
! cd /tmp && ~/Downloads/Isabelle2025_linux/Isabelle2025/bin/isabelle process -T Test
Loading theory "Draft.Test"
Sledgehammering...
### theory "Draft.Test"
### 0.064s elapsed time, 0.100s cpu time, 0.000s GC time
*** Outer syntax error (line 12 of "/tmp/Test.thy"): command expected,
*** but symbolic identifier # (line 12 of "/tmp/Test.thy") was found
*** At command "<malformed>" (line 11 of "/tmp/Test.thy")
Exception- TOPLEVEL_ERROR raised
from kdrag.solvers import BaseSolver
class IsabelleSolver(BaseSolver):
def __init__(self):
super().__init__()
def check(self):
self.write_tptp("/tmp/isabelle.p")
cmd = [
"/home/philip/Downloads/Isabelle2025_linux/Isabelle2025/bin/isabelle", "tptp_sledgehammer",
"/tmp/isabelle.p",
]
#if "timeout" in self.options:
# cmd.extend(["-t", str(self.options["timeout"] // 100) + "d"])
self.res = subprocess.run(cmd, stdout=subprocess.PIPE, stderr=subprocess.PIPE)
return self.check_tptp_status(self.res.stdout)
s = IsabelleSolver()
#x,y = smt.Ints("x y")
#s.add(smt.Not(smt.ForAll([x,y], x + y == y + x)))
p,q = smt.Bools("p q")
s.add(smt.Implies(smt.Or(p, q), smt.Or(q, p)))
s.check()
---------------------------------------------------------------------------
Exception Traceback (most recent call last)
Cell In[6], line 22
20 p,q = smt.Bools("p q")
21 s.add(smt.Implies(smt.Or(p, q), smt.Or(q, p)))
---> 22 s.check()
Cell In[6], line 15, in IsabelleSolver.check(self)
12 #if "timeout" in self.options:
13 # cmd.extend(["-t", str(self.options["timeout"] // 100) + "d"])
14 self.res = subprocess.run(cmd, stdout=subprocess.PIPE, stderr=subprocess.PIPE)
---> 15 return self.check_tptp_status(self.res.stdout)
File ~/Documents/python/knuckledragger/kdrag/solvers/__init__.py:433, in BaseSolver.check_tptp_status(self, res)
431 return smt.unknown
432 else:
--> 433 raise Exception("Unexpected return from solver", res)
Exception: ('Unexpected return from solver', b'')
from kdrag.all import *
f = smt.Function("f", smt.IntSort(), smt.IntSort(), smt.BoolSort())
f.domain(0)
Int
from kdrag.theories.nat import Nat
dir(Nat)
Nat.accessor(1,0)
pred
A Copy of the lean printing code
This version will continue to evolve if this proves to be useful https://github.com/philzook58/knuckledragger/blob/main/kdrag/printers/lean.py
import kdrag.smt as smt
import kdrag as kd
import subprocess
def decl_sig(f: smt.FuncDeclRef) -> str:
"""
Convert a function declaration to a Lean signature.
>>> f = smt.Function("f", smt.IntSort(), smt.IntSort(), smt.BoolSort())
>>> decl_sig(f)
'f : Int -> Int -> Bool'
"""
typs = [f.domain(n) for n in range(f.arity())] + [f.range()]
typ = " -> ".join(map(of_sort, typs))
return f"{f.name()} : {typ}"
def decl_axiom(f: smt.FuncDeclRef) -> str:
"""
Convert a function declaration to a Lean axiom definition.
>>> f = smt.Function("f", smt.IntSort(), smt.IntSort(), smt.BoolSort())
>>> decl_axiom(f)
'axiom f : Int -> Int -> Bool\\n'
"""
return f"axiom {decl_sig(f)}\n"
def sort_axiom(s: smt.SortRef) -> str:
"""
Convert uninterpreted sort to a Lean axiom definition.
"""
name = s.name()
assert name not in ["Bool", "Int"]
return f"""
axiom {name} : Type
axiom {name}_Inhabited : Inhabited {name}
axiom {name}_BEq : BEq {name}
axiom {name}_DecidableEq : DecidableEq {name}
"""
def of_sort(s: smt.SortRef) -> str:
"""
Convert a sort to a Lean type.
>>> of_sort(smt.BoolSort())
'Bool'
>>> of_sort(smt.BitVecSort(8))
'(BitVec 8)'
>>> of_sort(smt.ArraySort(smt.BitVecSort(8), smt.BitVecSort(16)))
'((BitVec 8) -> (BitVec 16))'
"""
if s == smt.BoolSort():
return "Bool"
elif isinstance(s, smt.BitVecSortRef):
return f"(BitVec {s.size()})"
elif s == smt.IntSort():
return "Int"
elif s == smt.StringSort():
return "String"
elif isinstance(s, smt.SeqSortRef):
return f"(Array {of_sort(s.basis())})"
elif isinstance(s, smt.ArraySortRef):
# TODO: multi arity
return f"({of_sort(s.domain())} -> {of_sort(s.range())})"
else:
return s.name()
# raise NotImplementedError(f"Cannot convert {s} to Lean type")
def of_datatype(dt: smt.DatatypeSortRef) -> str:
"""
Convert a datatype to a Lean inductive type definition.
>>> Nat = smt.Datatype("Nat")
>>> Nat.declare("Zero")
>>> Nat.declare("Succ", ("pred", Nat))
>>> Nat = Nat.create()
>>> of_datatype(Nat)
'inductive Nat : Type where\\n| Zero : Nat\\n| Succ : Nat -> Nat\\nderiving BEq, Inhabited, Repr, DecidableEq\\n'
"""
name = dt.name()
output = [f"inductive {name} : Type where"]
for n in range(dt.num_constructors()):
cons = dt.constructor(n)
output.append(f"| {decl_sig(cons)}")
output.append("deriving BEq, Inhabited, Repr, DecidableEq, Inhabited\n")
return "\n".join(output)
def accessor_def(dt: smt.DatatypeSortRef, n, i) -> str:
"""
Make a lean definition that matches accessor, otherwise returns default.
This might not be a perfect translation of accessor behavior in SMTLIB
"""
cons = dt.constructor(n)
acc = dt.accessor(n, i)
pargs = " ".join(["_" if j != i else "x" for j in range(cons.arity())])
return f"""
@[grind]
def {decl_sig(acc)}
| .{dt.constructor(n).name()} {pargs} => x
| _ => default
"""
def of_expr(e: smt.ExprRef):
"""
>>> x,y,z = smt.Ints("x y z")
>>> of_expr(x)
'(x : Int)'
>>> of_expr(x + y + z)
'(((x : Int) + (y : Int)) + (z : Int))'
>>> of_expr(smt.If(x == x, y, z))
'(if ((x : Int) = (x : Int)) then (y : Int) else (z : Int))'
"""
if isinstance(e, smt.QuantifierRef):
vs, body = kd.utils.open_binder_unhygienic(e)
vs = " ".join([f"({v.decl().name()} : {of_sort(v.sort())})" for v in vs])
body = of_expr(body)
if e.is_forall():
return f"(Classical.propDecidable (∀ {vs}, {body})).decide"
elif e.is_exists():
return f"(Classical.propDecidable (∃ {vs}, {body})).decide"
elif e.is_lambda():
return f"(λ {vs}, {body})"
else:
raise NotImplementedError(
"Cannot convert unknown quantifier to Lean expression."
)
if isinstance(e, smt.IntNumRef):
return str(e.as_long())
elif isinstance(e, smt.BitVecNumRef):
return f"{e.as_long()}#{e.size()}"
elif smt.is_app(e):
decl = e.decl()
name = decl.name()
args = [of_expr(arg) for arg in e.children()]
if smt.is_select(e):
assert len(args) == 2
return f"({args[0]} {args[1]})"
# special case store? fun k -> if k = v then d else a k
elif smt.is_if(e):
return f"(if {args[0]} then {args[1]} else {args[2]})"
elif len(args) == 0:
return f"({name} : {of_sort(e.sort())})"
elif name == "distinct":
assert len(args) == 2
return f"(Not ({args[0]} = {args[1]}))"
elif name == "=>":
assert len(args) == 2
return f"(not {args[0]} || {args[1]})"
elif name == "or":
return f"({' || '.join(args)})"
elif name == "and":
return f"({' && '.join(args)})"
elif name == "bvand":
return f"({' &&& '.join(args)})"
elif name == "bvor":
return f"({' ||| '.join(args)})"
elif name == "bvadd":
return f"({' + '.join(args)})"
elif name == "bvsub":
return f"({' - '.join(args)})"
elif name == "bvmul":
return f"({' * '.join(args)})"
elif not name[0].isalpha() and len(args) == 2:
return f"({args[0]} {name} {args[1]})"
else:
return f"({decl.name()} {' '.join(args)})"
else:
raise NotImplementedError(f"Cannot convert {e} to Lean expression. ", e)
def run_lean(filename: str):
return subprocess.run(["lean", filename], check=True, capture_output=True)