Lean-SMT

This project provides Lean tactics to discharge goals into SMT solvers. It is under active development and is currently in a beta phase. While it is usable, it is important to note that there are still some rough edges and ongoing improvements being made.

Supported Theories

lean-smt currently supports the theories of Uninterpreted Functions and Linear Integer/Real Arithmetic with quantifiers. Mathlib is required for Real Arithmetic. Support for the theory of Bitvectors is at an experimental stage. Support for additional theories is in progress.

Setup

To use lean-smt in your project, add the following lines to your list of dependencies in lakefile.toml:

[[require]]
name = "smt"
scope = "ufmg-smite"
rev = "main"

If your build configuration is in lakefile.lean, add the following line to your dependencies:

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

Alternatively, lean-smt has an experimental no_mathlib branch which can be accessed by replacing main with no_mathlib in your lakefile.toml or lakefile.lean file.

Usage

lean-smt comes with one main tactic, smt, that translates the current goal into an SMT query, sends the query to cvc5, and (if the solver returns unsat) replays cvc5's proof in Lean. cvc5's proofs may contain holes, returned as Lean goals. You can fill these holes manually or with other tactics. To use the smt tactic, you just need to import the Smt library:

import Smt

example [Nonempty U] {f : U → U → U} {a b c d : U}
  (h0 : a = b) (h1 : c = d) (h2 : p1 ∧ True) (h3 : (¬ p1) ∨ (p2 ∧ p3))
  (h4 : (¬ p3) ∨ (¬ (f a c = f b d))) : False := by
  smt [h0, h1, h2, h3, h4]

To use the smt tactic on Real arithmetic goals, import Smt.Real:

import Smt
import Smt.Real

example (ε : Real) (h1 : ε > 0) : ε / 2 + ε / 3 + ε / 7 < ε := by
  smt [h1]

lean-smt utilizes lean-auto to monomorphize goals in dependent type theory and higher-order logic into first-order logic. Enable auto's monomorphization procedure via smt +mono:

import Smt

variable [Group G]

theorem inverse : ∀ (a : G), a * a⁻¹ = 1 := by
  smt +mono [mul_assoc, one_mul, inv_mul_cancel]

theorem identity : ∀ (a : G), a * 1 = a := by
  smt +mono [mul_assoc, one_mul, inv_mul_cancel, inverse]

theorem unique_identity : ∀ (e : G), (∀ a, e * a = a) ↔ e = 1 := by
  smt +mono [mul_assoc, one_mul, inv_mul_cancel]