Provide a solver backend for lean-auto. (#150)

* Provide a solver backend for lean-auto.

* Add lean-auto lake configs.

* Reorder dependencies.

.github/workflows/ci.yml

@@ -21,5 +21,5 @@ jobs:
     - name: Build and Test lean-smt
       uses: leanprover/lean-action@v1
       with:
-        build-args: "Smt Smt.Rat Smt.Real"
+        build-args: "Smt Smt.Auto Smt.Rat Smt.Real"
         use-github-cache: false

Smt/Auto.lean

@@ -0,0 +1,36 @@
+/-
+Copyright (c) 2021-2024 by the authors listed in the file AUTHORS and their
+institutional affiliations. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Abdalrhman Mohamed
+-/
+
+import Auto.Tactic
+import Smt.Tactic.Smt
+
+open Lean in
+def smtSolverFunc (ls : Array Auto.Lemma) (is : Array Auto.Lemma) : MetaM Expr := do
+  let fi l := do
+    let userName ← mkFreshUserName `inst
+    let type ← Meta.mkAppM ``Inhabited #[l.type]
+    let value ← Meta.mkAppOptM ``Inhabited.mk #[l.type, l.proof]
+    return { userName, type, value }
+  let is ← is.mapM fi
+  let fl l := do
+    let userName ← mkFreshUserName `h
+    let type ← Auto.Lam2D.approxSimpNF l.type
+    let value := l.proof
+    return { userName, type, value }
+  let ls ← ls.mapM fl
+  let h ← Meta.mkFreshExprMVar (Expr.const ``False [])
+  let (_, mv) ← h.mvarId!.assertHypotheses is
+  let (fvs, mv) ← mv.assertHypotheses ls
+  mv.withContext do
+    let hs := fvs.map (.fvar ·)
+    _ ← Smt.smt mv hs.toList
+    -- Note: auto should allow solvers to export new goals to users
+    -- for mv in mvs do
+    --   logInfo m!"new : {mv}"
+    instantiateMVars h
+
+attribute [rebind Auto.Native.solverFunc] smtSolverFunc

Test/Auto.lean

@@ -0,0 +1,48 @@
+import Mathlib.Algebra.Group.Defs
+import Mathlib.Data.Set.Function
+
+import Smt
+import Smt.Auto
+
+set_option auto.native true
+
+example {α : Type} (x : α) : List.head? [x] = .some x := by
+  have h₂ : ∀ (x : α) (ys : _), List.head? (x :: ys) = .some x := fun _ _ => rfl
+  auto
+
+example {α : Type} (x y : α) : [x] ++ [y] = [x, y] := by
+  -- Invoke definition unfolding
+  have h : ∀ (x y : List α), x ++ y = x.append y := fun _ _ => rfl
+  auto [h] d[List.append]
+
+variable {G : Type} [Group G]
+
+theorem inverse' : ∀ (a : G), a * a⁻¹ = 1 := by
+  auto [mul_assoc, one_mul, inv_mul_cancel]
+
+theorem identity' : ∀ (a : G), a * 1 = a := by
+  auto [mul_assoc, one_mul, inv_mul_cancel, inverse']
+
+theorem unique_identity (e : G) : (∀ z, e * z = z) → e = 1 := by
+  auto [mul_assoc, one_mul, inv_mul_cancel]
+
+-- TODO: pre-process Nat away
+-- example {α : Type} (x y : α) : List.get? [x, y] 1 = .some y := by
+  -- auto d[List.get?]
+
+set_option auto.mono.mode "fol"
+
+variable {α β : Type} [Nonempty α] [Nonempty β] {f : α → β} {s : Set α} {v u : Set β}
+
+example : f '' s ⊆ v ↔ s ⊆ f ⁻¹' v := by
+  auto [Set.subset_def, Set.mem_image, Set.mem_preimage]
+
+example (h : Function.Injective f) : f ⁻¹' (f '' s) ⊆ s := by
+  auto [Set.subset_def, Set.mem_preimage, Function.Injective.mem_set_image, h]
+
+example : f '' (f ⁻¹' u) ⊆ u := by
+  auto [Set.subset_def, Set.mem_image, Set.mem_preimage]
+
+example (h : Function.Surjective f) : u ⊆ f '' (f ⁻¹' u) := by
+  unfold Function.Surjective at h
+  auto [Set.subset_def, Set.mem_image, Set.mem_preimage, h]

lake-manifest.json

@@ -1,7 +1,17 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/abdoo8080/lean-cvc5.git",
+ [{"url": "https://github.com/leanprover-community/lean-auto.git",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "5367bcd32133a50ee5c4c39fb6cfa345893387bf",
+   "name": "auto",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "5367bcd32133a50ee5c4c39fb6cfa345893387bf",
+   "inherited": false,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/abdoo8080/lean-cvc5.git",
    "type": "git",
    "subDir": null,
    "scope": "",

lakefile.lean

@@ -2,6 +2,9 @@ import Lake
 
 open Lake DSL
 
+require auto from
+  git "https://github.com/leanprover-community/lean-auto.git" @ "5367bcd32133a50ee5c4c39fb6cfa345893387bf"
+
 require cvc5 from
   git "https://github.com/abdoo8080/lean-cvc5.git" @ "b7a6933c50aea5bb294eeff9ed2555640bc9c435"