KO | EN

GitLite

Minimalist Open Source Repository Search Engine

gitlite — search

#dsh #dsh-plugin #ai-agents #developer-tools #codex #claude-code #mcp #rust #deepseek-harness #typescript #ai-agent #cli

lean-smt

★ 306 Open GitHub ↗

Tactics for discharging Lean goals into SMT solvers.

// repository documentation

Was this content helpful?

★ 0 (0 ratings)

# 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`:
```toml
[[require]]
name = "smt"
scope = "ufmg-smite"
rev = "main"
```
If your build configuration is in `lakefile.lean`, add the following line to
your dependencies:
```lean
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:
```lean
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`:
```lean
import Smt
import Smt.Real

example (ε : Real) (h1 : ε > 0) : ε / 2 + ε / 3 + ε / 7 < ε := by
  smt [h1]
```
`lean-smt` utilizes
[`lean-auto`](https://github.com/leanprover-community/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`:
```lean
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]
```

lean-smt

Explore Similar Repositories

Was this content helpful?

Recent Feedback

Download README