Skip to content

Tactics for discharging Lean goals into SMT solvers.

License

Notifications You must be signed in to change notification settings

mhk119/lean-smt

 
 

Repository files navigation

SMT Lean

This project is inspired by SMTCoq and aims to provide Lean tactics that discharge goals into SMT solvers. This project is in its early design/development phase and is not recommended for use.

Requirements

lean-smt communicates with SMT solvers via the SMT-LIB textual interface. Therefore, it requires a supported SMT solver to be installed. Currently, lean-smt supports two SMT solvers:

Usage

To use the lean-smt in your project. Add the following line to your list of dependencies in lakefile.lean:

require smt from git "https://github.com/ufmg-smite/lean-smt.git"@"main"

lean-smt comes with one main tactic, smt, that translates the current goal into an SMT query, sends the query to an SMT solver, and prints the result returned by the SMT solver. The tactic DOES NOT currently generate a proof term to discharge the goal.

Example

To use the smt tactic, you just need to import the Smt library:

import Smt

theorem modus_ponens (p q : Prop) : p → (p → q) → q := by
  smt
  simp_all

For the theorem above, smt prints

goal: p → (p → q) → q

query:
(declare-const p Bool)
(declare-const q Bool)
(assert (not (=> p (=> (=> p q) q))))
(check-sat)

result: unsat

You can specify the SMT solver to use like so:

set_option smt.solver.kind "z3"

lean-smt assumes the specified SMT solver to be in the path. If that's not the case, you can specify the path to the SMT solver like so:

set_option smt.solver.path "path/to/z3"

About

Tactics for discharging Lean goals into SMT solvers.

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages

  • Lean 99.9%
  • SMT 0.1%