Add initial support for skolems. (#78)

Smt/Reconstruct/Prop.lean

@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Abdalrhman Mohamed
 -/
 
+import Smt.Reconstruct.Prop.Core
 import Smt.Reconstruct.Prop.Factor
 import Smt.Reconstruct.Prop.Lemmas
 import Smt.Reconstruct.Prop.LiftOrNToImp

Smt/Reconstruct/Prop/Core.lean

@@ -19,7 +19,9 @@ theorem XOr.elim {p q r : Prop} (h : XOr p q) (h₁ : p → ¬q → r) (h₂ : 
 
 theorem XOr.symm (h : XOr p q) : XOr q p := h.elim (flip inr) (flip inl)
 
-@[macro_inline] instance [dp : Decidable p] [dq : Decidable q] : Decidable (XOr p q) :=
+namespace XOr
+
+@[macro_inline] scoped instance [dp : Decidable p] [dq : Decidable q] : Decidable (XOr p q) :=
   match dp with
   | isTrue   hp =>
     match dq with
@@ -30,6 +32,8 @@ theorem XOr.symm (h : XOr p q) : XOr q p := h.elim (flip inr) (flip inl)
     | isTrue   hq => isTrue (.inr hnp hq)
     | isFalse hnq => isFalse (·.elim (fun hp _ => hnp hp) (fun _ hq => hnq hq))
 
+end XOr
+
 namespace Smt.Reconstruct.Prop
 
 theorem and_assoc_eq : ((a ∧ b) ∧ c) = (a ∧ (b ∧ c)) := by simp [and_assoc]

Smt/Reconstruct/Quant/Lemmas.lean

@@ -5,6 +5,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Tomaz Gomes Mascarenhas
 -/
 
+import Std.Logic
+
+namespace Classical
+
+theorem epsilon_spec_aux' {α : Sort u} (h : Nonempty α) (p : α → Prop) : (¬∀ y, p y) → ¬p (@epsilon α h (fun x => ¬p x)) :=
+  propext not_forall ▸ epsilon_spec_aux h (fun x => ¬p x)
+
+end Classical
+
 open Classical
 
 namespace Smt.Reconstruct.Quant

Smt/Reconstruct/UF/Congruence.lean

@@ -11,14 +11,14 @@ open Lean Elab Tactic Meta
 
 namespace Smt.Reconstruct.UF
 
-def rewriteHyp (hyp : Expr) (mv : MVarId) : MetaM MVarId :=
+def rewriteHyp (mv : MVarId) (hyp : Expr) : MetaM MVarId :=
   mv.withContext do
     let type ← mv.getType
-    let r ← mv.rewrite type hyp
+    let r ← mv.rewrite type hyp false { occs := .pos [1] }
     mv.replaceTargetEq r.eNew r.eqProof
 
 def smtCongr (mv : MVarId) (hyps : Array Expr) : MetaM Unit := do
-  let mv ← hyps.foldrM rewriteHyp mv
+  let mv ← hyps.foldlM rewriteHyp mv
   mv.refl
 
 namespace Tactic

Test/Examples/Demo.expected

@@ -1,27 +0,0 @@
-goal: ∀ (a : G), op a (inv a) = e
-
-query:
-(declare-sort G 0)
-(declare-fun op (G G) G)
-(declare-const e G)
-(assert (forall ((a G)) (= (op e a) a)))
-(declare-fun inv (G) G)
-(assert (forall ((a G)) (= (op (inv a) a) e)))
-(assert (forall ((a G)) (forall ((b G)) (forall ((c G)) (= (op a (op b c)) (op (op a b) c))))))
-(assert (not (forall ((a G)) (= (op a (inv a)) e))))
-(check-sat)
-Test/Examples/Demo.lean:9:8: warning: declaration uses 'sorry'
-goal: ∀ (a : G), op a e = a
-
-query:
-(declare-sort G 0)
-(declare-const e G)
-(declare-fun op (G G) G)
-(declare-fun inv (G) G)
-(assert (forall ((a G)) (= (op a (inv a)) e)))
-(assert (forall ((a G)) (= (op e a) a)))
-(assert (forall ((a G)) (= (op (inv a) a) e)))
-(assert (forall ((a G)) (forall ((b G)) (forall ((c G)) (= (op a (op b c)) (op (op a b) c))))))
-(assert (not (forall ((a G)) (= (op a e) a))))
-(check-sat)
-Test/Examples/Demo.lean:14:8: warning: declaration uses 'sorry'

Test/Examples/Demo.lean

@@ -7,14 +7,13 @@ axiom inverse : ∀ a, op (inv a) a = e
 axiom ident   : ∀ a, op e a = a
 
 theorem inverse' : ∀ a, op a (inv a) = e := by
-   -- TODO: too slow. Replace `smt_show` with `smt` once performance is improved.
-  smt_show [assoc op, inverse op inv e, ident op e]
-  sorry
+  smt [assoc op, inverse op inv e, ident op e]
+  all_goals simp [eq_comm, Classical.not_not]
 
 theorem identity' : ∀ a, op a e = a := by
-  smt_show [assoc op, inverse op inv e, ident op e, inverse' op inv e]
-  sorry
+  smt [assoc op, inverse op inv e, ident op e, inverse' op inv e]
+  all_goals simp [eq_comm, Classical.not_not]
 
 theorem unique_identity e' : (∀ z, op e' z = z) → e' = e := by
   smt [assoc op, inverse op inv e, ident op e]
-  all_goals simp
+  all_goals simp [eq_comm]

Test/Nat/Sum'.expected

@@ -6,9 +6,9 @@ query:
 (declare-const n Nat)
 (assert (>= n 0))
 (define-fun Nat.sub ((x Nat) (y Nat)) Nat (ite (< x y) 0 (- x y)))
-(assert (forall ((_uniq.11686 Nat)) (=> (>= _uniq.11686 0) (forall ((_uniq.11687 Nat)) (=> (>= _uniq.11687 0) (>= (Nat.sub _uniq.11686 _uniq.11687) 0))))))
+(assert (forall ((_uniq.11646 Nat)) (=> (>= _uniq.11646 0) (forall ((_uniq.11647 Nat)) (=> (>= _uniq.11647 0) (>= (Nat.sub _uniq.11646 _uniq.11647) 0))))))
 (define-fun-rec sum ((n Nat)) Nat (ite (= n 0) 0 (+ n (sum (Nat.sub n 1)))))
-(assert (forall ((_uniq.11688 Nat)) (=> (>= _uniq.11688 0) (>= (sum _uniq.11688) 0))))
+(assert (forall ((_uniq.11648 Nat)) (=> (>= _uniq.11648 0) (>= (sum _uniq.11648) 0))))
 (assert (= (sum n) (div (* n (+ n 1)) 2)))
 (assert (not (= (sum (+ n 1)) (div (* (+ n 1) (+ (+ n 1) 1)) 2))))
 (check-sat)

Test/Nat/ZeroSub'.expected

@@ -1,4 +1,11 @@
-Test/Nat/ZeroSub'.lean:6:12: error: unknown free variable '«Nat.sub»'
-cvc5.Kind.INTERNAL_KIND : @PURIFY_4
+Test/Nat/ZeroSub'.lean:6:12: error: tactic 'rewrite' failed, motive is not type correct
+a.0 : «Nat.sub» = fun x y => if x < y then 0 else x - y
+a.1 :
+  ∀ («_uniq.189» : Int),
+    «_uniq.189» ≥ 0 → ∀ («_uniq.190» : Int), «_uniq.190» ≥ 0 → «Nat.sub» «_uniq.189» «_uniq.190» ≥ 0
+a.2 : ¬«Nat.sub» 0 0 = 0
+s.3 : 0 = 0
+s.4 : «Nat.sub» 0 0 = (fun x y => if x < y then 0 else x - y) 0 0
+⊢ («Nat.sub» 0 0 = 0) = ((fun x y => if x < y then 0 else x - y) 0 0 = 0)
 Test/Nat/ZeroSub'.lean:7:17: error: failed to synthesize
   Decidable (x ≥ 0)

Test/Prop/Cong.expected

@@ -1,12 +0,0 @@
-goal: p = q → f p = f q
-
-query:
-(declare-fun f (Bool) Bool)
-(declare-const p Bool)
-(declare-const q Bool)
-(assert (not (=> (= p q) (= (f p) (f q)))))
-(check-sat)
-Test/Prop/Cong.lean:3:67: error: unsolved goals
-p q : Prop
-f : Prop → Prop
-⊢ p = q → f p = f q

Test/Prop/Cong.lean

@@ -1,4 +1,4 @@
 import Smt
 
-theorem cong (p q : Prop) (f : Prop → Prop) : p = q → f p = f q := by
-  smt_show
+example (p q : Prop) (f : Prop → Prop) : p = q → f p = f q := by
+  smt

lake-manifest.json

@@ -13,7 +13,7 @@
   {"url": "https://github.com/abdoo8080/lean-cvc5.git",
    "type": "git",
    "subDir": null,
-   "rev": "6a5abce73167591e4b6a065034b11319cdad4474",
+   "rev": "d8376743562e89acedf30a4004b30c25763037a2",
    "name": "cvc5",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",