lean-smt
lean-smt copied to clipboard
ufmg-smite
Tactics for discharging Lean goals into SMT solvers.
With a context that looks like this: ```Lean import Smt set_option trace.smt.translate.query true theorem extracted {round : Type} [round_dec : DecidableEq round] (st_one_a : round → Bool) (st'_one_a : round...
We currently translate `Nat`-based expressions in the `smt` tactic as `Int`s greater than zero. However this translation is not proof-producing, and it will cause issues for proof reconstruction when the...
With #32, the `smt` tactic is becoming robust enough that I can translate some fairly complex expressions (e.g. exponentiation by squaring in $GF(2^8)$ with internals `declare`d). Unfortunately, the current preprocessing...
@abdoo8080 and I discussed recently when terms should be encoded with their definition, and when just declared. Here is a proposal for how the tactic could behave. It is almost...
The following file: ```Lean import Smt theorem funextEq {α β : Type} (f g : α → β) : (f = g) = ∀ x, f x = g x...
more `Int` and `Rat` lemmas - most `Int` lemmas are only useful for proofs over `Rat`-s
Metadata
Owner
Metadata
Tactics for discharging Lean goals into SMT solvers.