https://github.com/ufmg-smite/lean-smt Skip to content Navigation Menu Toggle navigation Sign in * Product + GitHub Copilot Write better code with AI + Security Find and fix vulnerabilities + Actions Automate any workflow + Codespaces Instant dev environments + Issues Plan and track work + Code Review Manage code changes + Discussions Collaborate outside of code + Code Search Find more, search less Explore + All features + Documentation + GitHub Skills + Blog * Solutions By company size + Enterprises + Small and medium teams + Startups By use case + DevSecOps + DevOps + CI/CD + View all use cases By industry + Healthcare + Financial services + Manufacturing + Government + View all industries View all solutions * Resources Topics + AI + DevOps + Security + Software Development + View all Explore + Learning Pathways + White papers, Ebooks, Webinars + Customer Stories + Partners * Open Source + GitHub Sponsors Fund open source developers + The ReadME Project GitHub community articles Repositories + Topics + Trending + Collections * Enterprise + Enterprise platform AI-powered developer platform Available add-ons + Advanced Security Enterprise-grade security features + GitHub Copilot Enterprise-grade AI features + Premium Support Enterprise-grade 24/7 support * Pricing Search or jump to... Search code, repositories, users, issues, pull requests... Search [ ] Clear Search syntax tips Provide feedback We read every piece of feedback, and take your input very seriously. [ ] [ ] Include my email address so I can be contacted Cancel Submit feedback Saved searches Use saved searches to filter your results more quickly Name [ ] Query [ ] To see all available qualifiers, see our documentation. Cancel Create saved search Sign in Sign up Reseting focus You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session. You switched accounts on another tab or window. Reload to refresh your session. Dismiss alert {{ message }} ufmg-smite / lean-smt Public * Notifications You must be signed in to change notification settings * Fork 19 * Star 139 Tactics for discharging Lean goals into SMT solvers. License Apache-2.0 license 139 stars 19 forks Branches Tags Activity Star Notifications You must be signed in to change notification settings * Code * Issues 8 * Pull requests 3 * Actions * Projects 0 * Security * Insights Additional navigation options * Code * Issues * Pull requests * Actions * Projects * Security * Insights ufmg-smite/lean-smt main BranchesTags [ ] Go to file Code Folders and files Name Name Last commit Last commit message date Latest commit History 130 Commits .github/workflows .github/workflows Smt Smt Test Test .gitignore .gitignore AUTHORS AUTHORS LICENSE LICENSE README.md README.md Smt.lean Smt.lean lake-manifest.json lake-manifest.json lakefile.lean lakefile.lean lean-toolchain lean-toolchain View all files Repository files navigation * README * Apache-2.0 license SMT Lean This project is inspired by SMTCoq and aims to provide Lean tactics that discharge goals into SMT solvers. It is under active development and is currently in a beta phase. While it is ready for use, 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 currently required for Arithmetic. Support for the theory of Bitvectors is at an experimental stage. We are working on adding support for other theories as well. Requirements lean-smt depends on lean-cvc5 FFI, which currently only supports Linux (x86_64) and macOS (AArch64 and x86_64). Usage To use 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" def libcpp : String := if System.Platform.isWindows then "libstdc++-6.dll" else if System.Platform.isOSX then "libc++.dylib" else "libstdc++.so.6" package foo where moreLeanArgs := #[s!"--load-dynlib={libcpp}"] moreGlobalServerArgs := #[s!"--load-dynlib={libcpp}"] 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 sometimes contain holes, which are sent back to the user as Lean goals. The user can then fill in these holes manually or by using other tactics. Example To use the smt tactic, you just need to import the Smt library: import Smt example {U : Type} [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] About Tactics for discharging Lean goals into SMT solvers. Topics smt lean4 Resources Readme License Apache-2.0 license Activity Custom properties Stars 139 stars Watchers 9 watching Forks 19 forks Report repository Releases No releases published Packages 0 No packages published Contributors 9 * @abdoo8080 * @Vtec234 * @tomaz1502 * @mhk119 * @HanielB * @eric-wieser * @AdrienChampion * @Paul-Lez * @joewatt95 Languages * Lean 100.0% Footer (c) 2024 GitHub, Inc. Footer navigation * Terms * Privacy * Security * Status * Docs * Contact * Manage cookies * Do not share my personal information You can't perform that action at this time.