From 3e89fccbb335677e56dcef825a7b0c5dd22234d8 Mon Sep 17 00:00:00 2001 From: Abdalrhman M Mohamed Date: Thu, 25 Jan 2024 11:27:56 -0800 Subject: [PATCH] Utilize FFI to reconstruct cvc5 proofs in Lean. --- Smt/Reconstruct.lean | 3 +- Smt/Reconstruct/Builtin/Rewrites.lean | 6 +- Smt/Reconstruct/Prop/Core.lean | 39 + Smt/Reconstruct/Prop/Lemmas.lean | 179 +-- Smt/Reconstruct/Prop/Resolution.lean | 3 - Smt/Reconstruct/Prop/Rewrites.lean | 56 +- Smt/Reconstruct/Reconstruct.lean | 1059 +++++++++++++++++ Smt/Reconstruct/UF/Rewrites.lean | 4 +- Smt/Tactic/Smt.lean | 96 +- Smt/Translate/BitVec.lean | 18 +- Test/BitVec/Shift.expected | 28 +- Test/BitVec/Shift.lean | 11 +- Test/BitVec/XorComm.expected | 14 +- Test/BitVec/XorComm.lean | 7 +- Test/Bool/Addition.expected | 8 - Test/Bool/Addition.lean | 2 +- Test/Bool/Assoc.expected | 16 +- Test/Bool/Assoc.lean | 2 +- Test/Bool/Comm.expected | 13 +- Test/Bool/Comm.lean | 2 +- Test/Bool/Cong.expected | 9 - Test/Bool/Cong.lean | 2 +- Test/Bool/Conjunction.expected | 8 - Test/Bool/Conjunction.lean | 2 +- Test/Bool/DisjunctiveSyllogism.expected | 8 - Test/Bool/DisjunctiveSyllogism.lean | 2 +- Test/Bool/Exists'.expected | 7 - Test/Bool/Exists'.lean | 2 +- Test/Bool/Falsum.expected | 7 - Test/Bool/Falsum.lean | 2 +- Test/Bool/HypotheticalSyllogism.expected | 3 - Test/Bool/HypotheticalSyllogism.lean | 2 +- Test/Bool/ModusPonens'.expected | 10 - Test/Bool/ModusPonens'.lean | 2 +- Test/Bool/ModusPonens.expected | 8 - Test/Bool/ModusPonens.lean | 2 +- Test/Bool/ModusTollens.expected | 8 - Test/Bool/ModusTollens.lean | 2 +- Test/Bool/PropExt.expected | 16 +- Test/Bool/PropExt.lean | 2 +- Test/Bool/Refl.expected | 8 - Test/Bool/Refl.lean | 2 +- Test/Bool/Resolution.expected | 8 - Test/Bool/Resolution.lean | 2 +- Test/Bool/Simplification.expected | 8 - Test/Bool/Simplification.lean | 2 +- Test/Bool/Symm.expected | 10 +- Test/Bool/Symm.lean | 2 +- Test/Bool/Trans.expected | 10 +- Test/Bool/Trans.lean | 2 +- Test/Bool/Triv''.expected | 8 - Test/Bool/Triv''.lean | 2 +- Test/Bool/Triv'.expected | 7 - Test/Bool/Triv'.lean | 2 +- Test/Bool/Triv.expected | 8 - Test/Bool/Triv.lean | 2 +- Test/Bool/Verum.expected | 7 - Test/Bool/Verum.lean | 2 +- Test/EUF/Example.expected | 16 - Test/EUF/Example.lean | 8 +- Test/Examples/Demo.expected | 36 +- Test/Examples/Demo.lean | 20 +- Test/Int/Arith.expected | 27 +- Test/Int/Arith.lean | 6 +- Test/Int/Binders.expected | 36 - Test/Int/Binders.lean | 8 +- Test/Int/Cong.expected | 3 - Test/Int/Cong.lean | 2 +- Test/Int/DefineSort.expected | 9 - Test/Int/DefineSort.lean | 2 +- Test/Int/Dvd.expected | 46 +- Test/Int/Dvd.lean | 6 +- Test/Int/DvdTimeout.expected | 15 +- Test/Int/DvdTimeout.lean | 2 +- Test/Int/ForallExists.expected | 9 +- Test/Int/ForallExists.lean | 2 +- Test/Int/Let.expected | 32 +- Test/Int/Let.lean | 10 +- Test/Int/Neg.expected | 3 +- Test/Int/Neg.lean | 2 +- Test/Nat/Cong.expected | 5 +- Test/Nat/Cong.lean | 2 +- Test/Nat/Exists''.expected | 7 - Test/Nat/Exists''.lean | 2 +- Test/Nat/Exists'.expected | 7 - Test/Nat/Exists'.lean | 2 +- Test/Nat/Forall'.expected | 9 +- Test/Nat/Forall'.lean | 2 +- Test/Nat/Max.expected | 14 +- Test/Nat/Max.lean | 4 +- Test/Nat/NeqZero.expected | 18 +- Test/Nat/NeqZero.lean | 4 +- Test/Nat/Sum'.expected | 32 +- Test/Nat/Sum'.lean | 2 +- Test/Nat/Triv'.expected | 7 - Test/Nat/Triv'.lean | 2 +- Test/Nat/Triv.expected | 7 - Test/Nat/Triv.lean | 2 +- Test/Nat/ZeroSub'.expected | 41 +- Test/Nat/ZeroSub.expected | 11 +- Test/Nat/ZeroSub.lean | 2 +- Test/Prop/Addition.expected | 9 - Test/Prop/Assoc.expected | 19 - Test/Prop/Comm.expected | 17 - Test/Prop/Cong.expected | 6 +- Test/Prop/Cong.lean | 2 +- Test/Prop/Conjunction.expected | 9 - Test/Prop/DisjunctiveSyllogism.expected | 9 - Test/Prop/Exists'.expected | 7 - Test/Prop/Exists'.lean | 10 +- Test/Prop/Falsum.expected | 7 - Test/Prop/HypotheticalSyllogism.expected | 14 - Test/Prop/ModusPonens'.expected | 11 - Test/Prop/ModusPonens.expected | 9 - Test/Prop/ModusTollens.expected | 9 - Test/Prop/PropExt.expected | 9 - Test/Prop/Refl.expected | 8 - Test/Prop/Resolution.expected | 10 - Test/Prop/Simplification.expected | 9 - Test/Prop/Symm.expected | 9 - Test/Prop/Trans.expected | 10 - Test/Prop/Triv'''.expected | 0 Test/Prop/Triv''.expected | 8 - Test/Prop/Triv'.expected | 7 - Test/Prop/Triv'.lean | 10 +- Test/Prop/Triv.expected | 8 - Test/Prop/Verum.expected | 7 - Test/Rat/Density.expected | 3 - Test/Rat/Density.lean | 2 +- Test/Rat/Inverse.expected | 6 +- Test/Rat/Inverse.lean | 2 +- .../Arith/ArithMulSign.expected | 19 + Test/Reconstruction/Arith/ArithMulSign.lean | 4 +- Test/Reconstruction/Arith/MulPosNeg.expected | 8 + Test/Reconstruction/Arith/MulPosNeg.lean | 4 +- Test/Reconstruction/Arith/SumBounds.lean | 4 +- Test/Reconstruction/Arith/TightBounds.lean | 4 +- Test/Reconstruction/Arith/Trichotomy.lean | 4 +- Test/Reconstruction/LiftOrNToNeg.lean | 1 - Test/Solver/Error.lean | 4 +- Test/Solver/Interactive.lean | 6 +- Test/Solver/Model.lean | 6 +- Test/Solver/Proof.expected | 4 +- Test/Solver/Proof.lean | 6 +- Test/Solver/Triv.lean | 6 +- Test/String/Append.expected | 3 - Test/String/Append.lean | 2 +- Test/String/Contains.expected | 11 - Test/String/Contains.lean | 2 +- Test/String/Empty.expected | 3 - Test/String/Empty.lean | 2 +- Test/String/GetOp.expected | 11 - Test/String/GetOp.lean | 2 +- Test/String/Length.expected | 3 - Test/String/Length.lean | 2 +- Test/String/Lt.expected | 3 - Test/String/Lt.lean | 2 +- Test/String/Replace.expected | 3 - Test/String/Replace.lean | 2 +- lake-manifest.json | 9 + lakefile.lean | 11 +- 161 files changed, 1495 insertions(+), 1146 deletions(-) create mode 100644 Smt/Reconstruct/Prop/Core.lean create mode 100644 Smt/Reconstruct/Reconstruct.lean delete mode 100644 Test/Prop/Triv'''.expected diff --git a/Smt/Reconstruct.lean b/Smt/Reconstruct.lean index 27752653..1f2ffee9 100644 --- a/Smt/Reconstruct.lean +++ b/Smt/Reconstruct.lean @@ -5,11 +5,12 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Abdalrhman Mohamed -/ -import Smt.Reconstruct.Arith +-- import Smt.Reconstruct.Arith import Smt.Reconstruct.Builtin import Smt.Reconstruct.Options import Smt.Reconstruct.Prop import Smt.Reconstruct.Quant +import Smt.Reconstruct.Reconstruct import Smt.Reconstruct.Rewrite import Smt.Reconstruct.Timed import Smt.Reconstruct.UF diff --git a/Smt/Reconstruct/Builtin/Rewrites.lean b/Smt/Reconstruct/Builtin/Rewrites.lean index 2ebeea17..ca57b867 100644 --- a/Smt/Reconstruct/Builtin/Rewrites.lean +++ b/Smt/Reconstruct/Builtin/Rewrites.lean @@ -13,7 +13,7 @@ namespace Smt.Reconstruct.Builtin theorem ite_true_cond : ite True x y = x := rfl theorem ite_false_cond : ite False x y = y := rfl -theorem ite_not_cond [h : Decidable c] : ite (Not c) x y = ite c y x := +theorem ite_not_cond [h : Decidable c] : ite (¬c) x y = ite c y x := h.byCases (fun hc => if_pos hc ▸ if_neg (not_not_intro hc) ▸ rfl) (fun hnc => if_pos hnc ▸ if_neg hnc ▸ rfl) theorem ite_eq_branch [h : Decidable c] : ite c x x = x := @@ -25,10 +25,10 @@ theorem ite_then_lookahead [h : Decidable c] : ite c (ite c x y) z = ite c x z : theorem ite_else_lookahead [h : Decidable c] : ite c x (ite c y z) = ite c x z := h.byCases (fun hc => if_pos hc ▸ if_pos hc ▸ rfl) (fun hc => if_neg hc ▸ if_neg hc ▸ if_neg hc ▸ rfl) -theorem ite_then_neg_lookahead [h : Decidable c] : ite c (ite (Not c) x y) z = ite c y z := +theorem ite_then_neg_lookahead [h : Decidable c] : ite c (ite (¬c) x y) z = ite c y z := h.byCases (fun hc => if_pos hc ▸ if_pos hc ▸ ite_not_cond (c := c) ▸ if_pos hc ▸ rfl) (fun hc => if_neg hc ▸ if_neg hc ▸ rfl) -theorem ite_else_neg_lookahead [h : Decidable c] : ite c x (ite (Not c) y z) = ite c x y := +theorem ite_else_neg_lookahead [h : Decidable c] : ite c x (ite (¬c) y z) = ite c x y := h.byCases (fun hc => if_pos hc ▸ if_pos hc ▸ rfl) (fun hc => if_neg hc ▸ if_neg hc ▸ ite_not_cond (c := c) ▸ if_neg hc ▸ rfl) diff --git a/Smt/Reconstruct/Prop/Core.lean b/Smt/Reconstruct/Prop/Core.lean new file mode 100644 index 00000000..5abbb13a --- /dev/null +++ b/Smt/Reconstruct/Prop/Core.lean @@ -0,0 +1,39 @@ +/- +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 Std.Logic + +/- abbrev Implies (p q : Prop) := p → q -/ + +inductive XOr (p q : Prop) : Prop where + | inl : p → ¬q → XOr p q + | inr : ¬p → q → XOr p q + +theorem XOr.elim {p q r : Prop} (h : XOr p q) (h₁ : p → ¬q → r) (h₂ : ¬p → q → r) : r := match h with + | inl hp hnq => h₁ hp hnq + | inr hnp hq => h₂ hnp hq + +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) := + match dp with + | isTrue hp => + match dq with + | isTrue hq => isFalse (·.elim (fun _ hnq => hnq hq) (fun hnp _ => hnp hp)) + | isFalse hnq => isTrue (.inl hp hnq) + | isFalse hnp => + match dq with + | isTrue hq => isTrue (.inr hnp hq) + | isFalse hnq => isFalse (·.elim (fun hp _ => hnp hp) (fun _ hq => hnq hq)) + +namespace Smt.Reconstruct.Prop + +theorem and_assoc_eq : ((a ∧ b) ∧ c) = (a ∧ (b ∧ c)) := by simp [and_assoc] + +theorem or_assoc_eq : ((a ∨ b) ∨ c) = (a ∨ (b ∨ c)) := by simp [or_assoc] + +end Smt.Reconstruct.Prop diff --git a/Smt/Reconstruct/Prop/Lemmas.lean b/Smt/Reconstruct/Prop/Lemmas.lean index 8644e96a..ec447a3d 100644 --- a/Smt/Reconstruct/Prop/Lemmas.lean +++ b/Smt/Reconstruct/Prop/Lemmas.lean @@ -8,6 +8,7 @@ Authors: Tomaz Gomes Mascarenhas import Lean import Std +import Smt.Reconstruct.Prop.Core import Smt.Reconstruct.Options import Smt.Reconstruct.Util @@ -16,8 +17,6 @@ namespace Smt.Reconstruct.Prop open Lean Elab.Tactic Meta Expr Syntax open Nat List Classical -/- abbrev Implies (p q : Prop) := p → q -/ - theorem notImplies1 : ∀ {P Q : Prop}, ¬ (P → Q) → P := by intros P Q h cases Classical.em P with @@ -63,37 +62,53 @@ theorem notEquivElim2 : ∀ {P Q : Prop}, ¬ (Eq P Q) → ¬ P ∨ ¬ Q := by | Or.inl p, Or.inl q => absurd (propext (Iff.intro (λ _ => q) (λ _ => p))) h -theorem iteElim1 : ∀ {c a b : Prop}, ite c a b → ¬ c ∨ a := by - intros c a b h - cases Classical.em c with - | inl hc => have r: ite c a b = a := if_pos hc - rewrite [r] at h - exact Or.inr h - | inr hnc => exact Or.inl hnc - -theorem iteElim2 : ∀ {c a b : Prop}, ite c a b → c ∨ b := by - intros c a b h - cases Classical.em c with - | inl hc => exact Or.inl hc - | inr hnc => have r: ite c a b = b := if_neg hnc - rewrite [r] at h - exact Or.inr h - -theorem notIteElim1 : ∀ {c a b : Prop}, ¬ ite c a b → ¬ c ∨ ¬ a := by - intros c a b h - cases Classical.em c with - | inl hc => have r : ite c a b = a := if_pos hc - rewrite [r] at h - exact Or.inr h - | inr hnc => exact Or.inl hnc - -theorem notIteElim2 : ∀ {c a b : Prop}, ¬ ite c a b → c ∨ ¬ b := by - intros c a b h - cases Classical.em c with - | inl hc => exact Or.inl hc - | inr hnc => have r : ite c a b = b := if_neg hnc - rewrite [r] at h - exact Or.inr h +theorem xorElim1 (h : XOr p q) : p ∨ q := + match h with + | .inl hp _ => Or.inl hp + | .inr _ hq => Or.inr hq + +theorem xorElim2 (h : XOr p q) : ¬p ∨ ¬q := + match h with + | .inl _ hnq => Or.inr hnq + | .inr hnp _ => Or.inl hnp + +theorem notXorElim1 (h : ¬XOr p q) : p ∨ ¬q := + match Classical.em p, Classical.em q with + | Or.inl hp, _ => Or.inl hp + | _, Or.inr hnq => Or.inr hnq + | Or.inr hnp, Or.inl hq => + absurd (.inr hnp hq) h + +theorem notXorElim2 (h : ¬XOr p q) : ¬p ∨ q := + match Classical.em p, Classical.em q with + | Or.inr hnp, _ => Or.inl hnp + | _, Or.inl hq => Or.inr hq + | Or.inl hp, Or.inr hnq => + absurd (.inl hp hnq) h + +theorem iteElim1 [hc : Decidable c] : ite c a b → ¬ c ∨ a := by + intros h + cases hc with + | isTrue hc => exact Or.inr h + | isFalse hnc => exact Or.inl hnc + +theorem iteElim2 [hc : Decidable c] : ite c a b → c ∨ b := by + intros h + cases hc with + | isTrue hc => exact Or.inl hc + | isFalse hnc => exact Or.inr h + +theorem notIteElim1 [hc : Decidable c] : ¬ ite c a b → ¬ c ∨ ¬ a := by + intros h + cases hc with + | isTrue hc => exact Or.inr h + | isFalse hnc => exact Or.inl hnc + +theorem notIteElim2 [hc : Decidable c] : ¬ ite c a b → c ∨ ¬ b := by + intros h + cases hc with + | isTrue hc => exact Or.inl hc + | isFalse hnc => exact Or.inr h theorem contradiction : ∀ {P : Prop}, P → ¬ P → False := λ p np => np p @@ -314,102 +329,92 @@ theorem cnfImpliesNeg2 : ∀ {p q : Prop}, (p → q) ∨ ¬ q := by intros hnnq _ exact notNotElim hnnq -theorem cnfEquivPos1 : ∀ {p q : Prop}, ¬ (Eq p q) ∨ ¬ p ∨ q := by +theorem cnfEquivPos1 : ∀ {p q : Prop}, p ≠ q ∨ ¬ p ∨ q := by intros _ _ apply orImplies exact equivElim1 ∘ notNotElim -theorem cnfEquivPos2 : ∀ {p q : Prop}, ¬ (Eq p q) ∨ p ∨ ¬ q := by +theorem cnfEquivPos2 : ∀ {p q : Prop}, p ≠ q ∨ p ∨ ¬ q := by intros _ _ apply orImplies exact equivElim2 ∘ notNotElim -theorem cnfEquivNeg1 : ∀ {p q : Prop}, Eq p q ∨ p ∨ q := by +theorem cnfEquivNeg1 : ∀ {p q : Prop}, p = q ∨ p ∨ q := by intros _ _ apply orImplies exact notEquivElim1 -theorem cnfEquivNeg2 : ∀ {p q : Prop}, Eq p q ∨ ¬ p ∨ ¬ q := by +theorem cnfEquivNeg2 : ∀ {p q : Prop}, p = q ∨ ¬ p ∨ ¬ q := by intros _ _ apply orImplies exact notEquivElim2 -theorem cnfItePos1 : ∀ {c a b : Prop}, ¬ (ite c a b) ∨ ¬ c ∨ a := by - intros c a b +theorem cnfXorPos1 : ¬(XOr p q) ∨ p ∨ q := + orImplies (xorElim1 ∘ notNotElim) + +theorem cnfXorPos2 : ¬(XOr p q) ∨ ¬p ∨ ¬q := + orImplies (xorElim2 ∘ notNotElim) + +theorem cnfXorNeg1 : (XOr p q) ∨ ¬p ∨ q := + orImplies notXorElim2 + +theorem cnfXorNeg2 : (XOr p q) ∨ p ∨ ¬q := + orImplies notXorElim1 + +theorem cnfItePos1 [h : Decidable c] : ¬ (ite c a b) ∨ ¬ c ∨ a := by apply orImplies intro hite have hite' := notNotElim hite - match Classical.em c with - | Or.inl hc => have r: (if c then a else b) = a := if_pos hc - rewrite [r] at hite' - exact Or.inr hite' - | Or.inr hnc => exact Or.inl hnc + match h with + | isTrue _ => exact Or.inr hite' + | isFalse hnc => exact Or.inl hnc -theorem cnfItePos2 : ∀ {c a b : Prop}, ¬ (ite c a b) ∨ c ∨ b := by - intros c a b +theorem cnfItePos2 [h : Decidable c] : ¬ (ite c a b) ∨ c ∨ b := by apply orImplies intro hite have hite' := notNotElim hite - match Classical.em c with - | Or.inr hnc => have r: (if c then a else b) = b := if_neg hnc - rewrite [r] at hite' - exact Or.inr hite' - | Or.inl hc => exact Or.inl hc + match h with + | isFalse _ => exact Or.inr hite' + | isTrue hc => exact Or.inl hc -theorem cnfItePos3 : ∀ {c a b : Prop}, ¬ (ite c a b) ∨ a ∨ b := by - intros c a b +theorem cnfItePos3 [h : Decidable c] : ¬ (ite c a b) ∨ a ∨ b := by apply orImplies intro hite have hite' := notNotElim hite - match Classical.em c with - | Or.inr hnc => have r: (if c then a else b) = b := if_neg hnc - rewrite [r] at hite' - exact Or.inr hite' - | Or.inl hc => have r: (if c then a else b) = a := if_pos hc - rewrite [r] at hite' - exact Or.inl hite' - -theorem cnfIteNeg1 : ∀ {c a b : Prop}, (ite c a b) ∨ ¬ c ∨ ¬ a := by - intros c a b + match h with + | isFalse _ => exact Or.inr hite' + | isTrue _ => exact Or.inl hite' + +theorem cnfIteNeg1 [h : Decidable c] : (ite c a b) ∨ ¬ c ∨ ¬ a := by apply orImplies intro hnite - match Classical.em c with - | Or.inl hc => have r: (if c then a else b) = a := if_pos hc - rewrite [r] at hnite - exact Or.inr hnite - | Or.inr hnc => exact Or.inl hnc + match h with + | isTrue _ => exact Or.inr hnite + | isFalse hnc => exact Or.inl hnc -theorem cnfIteNeg2 : ∀ {c a b : Prop}, (ite c a b) ∨ c ∨ ¬ b := by - intros c a b +theorem cnfIteNeg2 [h : Decidable c] : (ite c a b) ∨ c ∨ ¬ b := by apply orImplies intro hnite - match Classical.em c with - | Or.inr hnc => have r: (if c then a else b) = b := if_neg hnc - rewrite [r] at hnite - exact Or.inr hnite - | Or.inl hc => exact Or.inl hc + match h with + | isFalse _ => exact Or.inr hnite + | isTrue hc => exact Or.inl hc -theorem cnfIteNeg3 : ∀ {c a b : Prop}, (ite c a b) ∨ ¬ a ∨ ¬ b := by - intros c a b +theorem cnfIteNeg3 [h : Decidable c] : (ite c a b) ∨ ¬ a ∨ ¬ b := by apply orImplies intro hnite - match Classical.em c with - | Or.inr hnc => have r: (if c then a else b) = b := if_neg hnc - rewrite [r] at hnite - exact Or.inr hnite - | Or.inl hc => have r: (if c then a else b) = a := if_pos hc - rewrite [r] at hnite - exact Or.inl hnite + match h with + | isFalse _ => exact Or.inr hnite + | isTrue _ => exact Or.inl hnite theorem iteIntro {α : Type u} {c : Prop} {t e : α} : ite c ((ite c t e) = t) ((ite c t e) = e) := by match Classical.em c with | Or.inl hc => rw [if_pos hc, if_pos hc] | Or.inr hnc => rw [if_neg hnc, if_neg hnc] -theorem congrIte {α : Type u} : ∀ {c₁ c₂ : Prop} {t₁ t₂ e₁ e₂ : α} , +theorem congrIte [Decidable c₁] [Decidable c₂] {t₁ t₂ e₁ e₂ : α} : c₁ = c₂ → t₁ = t₂ → e₁ = e₂ → ite c₁ t₁ e₁ = ite c₂ t₂ e₂ := by - intros c₁ c₂ t₁ t₂ e₁ e₂ h₁ h₂ h₃ - rw [h₁, h₂, h₃] + intros h₁ h₂ h₃ + simp only [h₁, h₂, h₃] theorem congrHAdd {α β γ : Type} [HAdd α β γ] : ∀ {a₁ a₂ : α} {b₁ b₂ : β}, a₁ = a₂ → b₁ = b₂ → a₁ + b₁ = a₂ + b₂ := by diff --git a/Smt/Reconstruct/Prop/Resolution.lean b/Smt/Reconstruct/Prop/Resolution.lean index 61444a73..a2c67972 100644 --- a/Smt/Reconstruct/Prop/Resolution.lean +++ b/Smt/Reconstruct/Prop/Resolution.lean @@ -73,15 +73,12 @@ def resolutionCoreMeta (val₁ val₂ pivot : Expr) (sufIdx₁' sufIdx₂' : Opt let len₂ := sufIdx₂ + 1 let lenGoal := len₁ + len₂ - 2 let prefixLength := len₁ - 2 - if flipped then let tmp := pivot pivot := notPivot notPivot := tmp - let pulled₁ ← pullCore pivot val₁ type₁ sufIdx₁' let pulled₂ ← pullCore notPivot val₂ type₂ sufIdx₂' - let props₁ ← collectPropsInOrChain' sufIdx₁ type₁ let props₁ := props₁.erase pivot let props₂ ← collectPropsInOrChain' sufIdx₂ type₂ diff --git a/Smt/Reconstruct/Prop/Rewrites.lean b/Smt/Reconstruct/Prop/Rewrites.lean index e4a43383..60d3ee32 100644 --- a/Smt/Reconstruct/Prop/Rewrites.lean +++ b/Smt/Reconstruct/Prop/Rewrites.lean @@ -5,26 +5,20 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Abdalrhman Mohamed -/ -import Std.Logic +import Smt.Reconstruct.Prop.Core namespace Smt.Reconstruct.Prop --- prelude - -theorem and_assoc_eq : ((a ∧ b) ∧ c) = (a ∧ (b ∧ c)) := by simp [and_assoc] - -theorem or_assoc_eq : ((a ∨ b) ∨ c) = (a ∨ (b ∨ c)) := by simp [or_assoc] - -- https://github.com/cvc5/cvc5/blob/proof-new/src/theory/booleans/rewrites open Function -theorem bool_double_not_elim [Decidable t] : (¬¬t) = t := - propext ⟨Decidable.of_not_not, not_not_intro⟩ +theorem bool_double_not_elim : (¬¬t) = t := + propext Classical.not_not theorem bool_eq_true : (t = True) = t := propext ⟨of_eq_true, eq_true⟩ -theorem bool_eq_false : (t = False) = (Not t) := +theorem bool_eq_false : (t = False) = ¬t := propext ⟨(· ▸ not_false), eq_false⟩ theorem bool_eq_nrefl : (t = ¬t) = False := propext ⟨(have H : t ↔ ¬t := · ▸ ⟨id, id⟩; have f h := H.mp h h; f (H.mpr f)), False.elim⟩ @@ -33,12 +27,12 @@ theorem bool_impl_false1 : (t → False) = ¬t := propext ⟨(·), (·)⟩ theorem bool_impl_false2 : (False → t) = True := propext ⟨const _ trivial, const _ False.elim⟩ -theorem bool_impl_true1 : (t → True) = True := +theorem bool_impl_true1 {t : Prop} : (t → True) = True := propext ⟨const _ trivial, const _ (const _ trivial)⟩ theorem bool_impl_true2 {t : Prop} : (True → t) = t := propext ⟨(· trivial), const _⟩ -theorem bool_impl_elim [h : Decidable t] : (t → s) = (¬t ∨ s) := - propext ⟨fun hts => h.byCases (Or.inr $ hts ·) Or.inl, (fun ht => ·.elim (absurd ht) id)⟩ +theorem bool_impl_elim : (t → s) = (¬t ∨ s) := + propext ⟨fun hts => (Classical.em t).elim (Or.inr $ hts ·) Or.inl, (fun ht => ·.elim (absurd ht) id)⟩ theorem bool_or_true : (xs ∨ True ∨ ys) = True := (true_or _).symm ▸ or_true _ @@ -62,23 +56,27 @@ theorem bool_and_dup : (xs ∧ b ∧ ys ∧ b ∧ zs) = (xs ∧ b ∧ ys ∧ zs) theorem bool_and_conf : (xs ∧ w ∧ ys ∧ ¬w ∧ zs) = False := propext ⟨fun ⟨_, hw, _, hnw, _⟩ => absurd hw hnw, False.elim⟩ -theorem bool_or_taut [h : Decidable w] : (xs ∨ w ∨ ys ∨ ¬w ∨ zs) = True := propext $ .intro +theorem bool_or_taut : (xs ∨ w ∨ ys ∨ ¬w ∨ zs) = True := propext $ .intro (const _ trivial) - (eq_true h.em ▸ (·.elim (Or.inr ∘ Or.inl) (Or.inr ∘ Or.inr ∘ Or.inr ∘ Or.inl))) - -theorem bool_xor_refl : (x ≠ x) = False := - propext ⟨(nomatch ·), False.elim⟩ -theorem bool_xor_nrefl : (x ≠ ¬x) = True := - propext ⟨const _ trivial, const _ (show x = ¬x → False from bool_eq_nrefl ▸ id)⟩ -theorem bool_xor_false [h : Decidable x] : (x ≠ False) = x := - propext ⟨(h.of_not_not $ @bool_eq_false x ▸ ·), flip (· ▸ ·)⟩ -theorem bool_xor_true : (x ≠ True) = ¬x := - propext ⟨(· $ propext ⟨const _ trivial, const _ ·⟩), ne_true_of_not⟩ -theorem bool_xor_comm : (x ≠ y) = (y ≠ x) := - propext ⟨Ne.symm, Ne.symm⟩ -theorem bool_xor_elim : (x ≠ y) = ¬(x = y) := rfl - -theorem ite_neg_branch [h : Decidable c] [Decidable y] : x = ¬y → ite c x y = (c = x) := + (eq_true (Classical.em w) ▸ (·.elim (Or.inr ∘ Or.inl) (Or.inr ∘ Or.inr ∘ Or.inr ∘ Or.inl))) + +theorem bool_xor_refl : XOr x x = False := + propext ⟨(·.elim absurd (flip absurd)), False.elim⟩ +theorem bool_xor_nrefl : (XOr x ¬x) = True := + propext ⟨const _ trivial, + const _ ((Classical.em x).elim (fun hx => .inl hx (· hx)) (fun hnx => .inr hnx hnx))⟩ +theorem bool_xor_false : XOr x False = x := + propext ⟨(·.elim (flip (const _ id)) (const _ False.elim)), (.inl · not_false)⟩ +theorem bool_xor_true : XOr x True = ¬x := + propext ⟨(·.elim (const _ (False.elim $ not_true.mp ·)) (flip (const _ id))), (.inr · trivial)⟩ +theorem bool_xor_comm : XOr x y = XOr y x := + propext ⟨XOr.symm, XOr.symm⟩ +theorem bool_xor_elim : XOr x y = ¬(x = y) := + propext ⟨(·.elim (fun h => absurd · $ h ▸ ·) (fun h => (flip absurd) · $ h ▸ ·)), fun hnxy => + (Classical.em x).elim ((Classical.em y).elim (False.elim $ hnxy $ propext ⟨const _ ·, const _ ·⟩) (flip .inl)) + ((Classical.em y).elim (flip .inr) (fun hny hnx => False.elim $ hnxy $ propext ⟨(False.elim $ hnx ·), (False.elim $ hny ·)⟩))⟩ + +theorem ite_neg_branch [h : Decidable c] : x = ¬y → ite c x y = (c = x) := fun hxny => hxny ▸ h.byCases (fun hc => if_pos hc ▸ propext ⟨(propext ⟨const _ ·, const _ hc⟩), (· ▸ hc)⟩) (fun hnc => if_neg hnc ▸ propext diff --git a/Smt/Reconstruct/Reconstruct.lean b/Smt/Reconstruct/Reconstruct.lean new file mode 100644 index 00000000..6733bb1b --- /dev/null +++ b/Smt/Reconstruct/Reconstruct.lean @@ -0,0 +1,1059 @@ +import cvc5 +import Lean +import Qq + +import Smt.Reconstruct.Builtin +import Smt.Reconstruct.Options +import Smt.Reconstruct.Prop +import Smt.Reconstruct.Quant +import Smt.Reconstruct.Rewrite +import Smt.Reconstruct.Timed +import Smt.Reconstruct.UF +import Smt.Reconstruct.Util + +/-- Takes an array `xs` of free variables or metavariables and a term `e` that may contain those variables, and abstracts and binds them as existential quantifiers. + +- if `usedOnly = true` then only variables that the expression body depends on will appear. +- if `usedLetOnly = true` same as `usedOnly` except for let-bound variables. (That is, local constants which have been assigned a value.) + -/ +def Lean.Meta.mkExistsFVars (xs : Array Expr) (e : Expr) (usedOnly : Bool := false) (usedLetOnly : Bool := true) (binderInfoForMVars := BinderInfo.implicit) : MetaM Expr := do + let e ← if xs.isEmpty then return e else liftMkBindingM <| MetavarContext.mkLambda xs e usedOnly usedLetOnly binderInfoForMVars + addExists e xs.size +where + addExists : Expr → Nat → MetaM Expr + | .lam n t b i, m + 1 => do + let b ← addExists b m + mkAppM ``Exists #[.lam n t b i] + | e, _ => pure e + +namespace Smt.Reconstruct + +open Lean hiding Rat mkRat +open Qq cvc5 +open Smt.Reconstruct.Prop + +def findFVarId (n : Name) : MetaM FVarId := do + return match (← getLCtx).findFromUserName? n with + | some d => d.fvarId + | none => ⟨n⟩ + +def rconsSort (s : cvc5.Sort) : MetaM Expr := do match s.getKind with + | .BOOLEAN_SORT => return q(Prop) + | .INTERNAL_SORT_KIND + | .UNINTERPRETED_SORT => return .fvar (← findFVarId s.getSymbol) + | .BITVECTOR_SORT => + let w : Q(Nat) := mkNatLit s.getBitVectorSize.val + return q(Std.BitVec $w) + | .INTEGER_SORT => return q(Int) + | .REAL_SORT => return q(Rat) + | _ => return .const `sorry [] + +partial def rconsTerm (t : cvc5.Term) : MetaM Expr := do match t.getKind with + | .VARIABLE => return .fvar (← findFVarId t.getSymbol) + | .CONSTANT => return .fvar (← findFVarId t.getSymbol) + | .CONST_BOOLEAN => return if t.getBooleanValue then q(True) else q(False) + | .NOT => + let b : Q(Prop) ← rconsTerm t[0]! + return q(¬$b) + | .IMPLIES => + let mut curr : Q(Prop) ← rconsTerm t[t.getNumChildren - 1]! + for i in [1:t.getNumChildren] do + let p : Q(Prop) ← rconsTerm t[t.getNumChildren - i - 1]! + curr := q($p → $curr) + return curr + | .AND => rightAssocOp q(And) t + | .OR => rightAssocOp q(Or) t + | .XOR => rightAssocOp q(XOr) t + | .EQUAL => + let α : Q(Type) ← rconsSort t[0]!.getSort + let x : Q($α) ← rconsTerm t[0]! + let y : Q($α) ← rconsTerm t[1]! + return q($x = $y) + | .DISTINCT => + let α : Q(Type) ← rconsSort t[0]!.getSort + let x : Q($α) ← rconsTerm t[0]! + let y : Q($α) ← rconsTerm t[1]! + return q($x ≠ $y) + | .ITE => + let α : Q(Type) ← rconsSort t.getSort + let c : Q(Prop) ← rconsTerm t[0]! + let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c) + let x : Q($α) ← rconsTerm t[1]! + let y : Q($α) ← rconsTerm t[2]! + return q(@ite $α $c $h $x $y) + | .FORALL => + let mut xs : Array (Name × (Array Expr → MetaM Expr)) := #[] + for x in t[0]! do + xs := xs.push (x.getSymbol, fun _ => rconsSort x.getSort) + Meta.withLocalDeclsD xs fun xs => do + let b ← rconsTerm t[1]! + Meta.mkForallFVars xs b + | .EXISTS => + let mut xs : Array (Name × (Array Expr → MetaM Expr)) := #[] + for x in t[0]! do + xs := xs.push (x.getSymbol, fun _ => rconsSort x.getSort) + Meta.withLocalDeclsD xs fun xs => do + let b ← rconsTerm t[1]! + Meta.mkExistsFVars xs b + | .LAMBDA => + let mut xs : Array (Name × (Array Expr → MetaM Expr)) := #[] + for x in t[0]! do + xs := xs.push (x.getSymbol, fun _ => rconsSort x.getSort) + Meta.withLocalDeclsD xs fun xs => do + let b ← rconsTerm t[1]! + Meta.mkLambdaFVars xs b + | .HO_APPLY => + return .app (← rconsTerm t[0]!) (← rconsTerm t[1]!) + | .APPLY_UF => + let mut curr ← rconsTerm t[0]! + for i in [1:t.getNumChildren] do + curr := .app curr (← rconsTerm t[i]!) + return curr + | .CONST_BITVECTOR => + let w : Nat := t.getSort.getBitVectorSize.val + let v : Nat := (t.getBitVectorValue 10).toNat! + return q(Std.BitVec.ofNat $w $v) + | .BITVECTOR_ADD => + let w : Nat := t.getSort.getBitVectorSize.val + let x : Q(Std.BitVec $w) ← rconsTerm t[0]! + let y : Q(Std.BitVec $w) ← rconsTerm t[1]! + return q($x + $y) + | .CONST_INTEGER => + let x : Int := t.getIntegerValue + let x' : Q(Nat) := mkRawNatLit x.natAbs + if x ≥ 0 then + return q(OfNat.ofNat $x' : Int) + else + return q(-(OfNat.ofNat $x' : Int)) + | .CONST_RATIONAL => + let x : Rat := t.getRationalValue + let num : Int := x.num + let den : Nat := x.den + return q(mkRat $num $den) + | .NEG => + if t.getSort.isInteger then + let x : Q(Int) ← rconsTerm t[0]! + return q(-$x) + else + let x : Q(Rat) ← rconsTerm t[0]! + return q(-$x) + | .SUB => + if t.getSort.isInteger then + let x : Q(Int) ← rconsTerm t[0]! + let y : Q(Int) ← rconsTerm t[1]! + return q($x - $y) + else + let x : Q(Rat) ← rconsTerm t[0]! + let y : Q(Rat) ← rconsTerm t[1]! + return q($x - $y) + | .ADD => + if t.getSort.isInteger then + let x : Q(Int) ← rconsTerm t[0]! + let y : Q(Int) ← rconsTerm t[1]! + return q($x + $y) + else + let x : Q(Rat) ← rconsTerm t[0]! + let y : Q(Rat) ← rconsTerm t[1]! + return q($x + $y) + | .MULT => + if t.getSort.isInteger then + let x : Q(Int) ← rconsTerm t[0]! + let y : Q(Int) ← rconsTerm t[1]! + return q($x * $y) + else + let x : Q(Rat) ← rconsTerm t[0]! + let y : Q(Rat) ← rconsTerm t[1]! + return q($x * $y) + | .INTS_DIVISION => + let x : Q(Int) ← rconsTerm t[0]! + let y : Q(Int) ← rconsTerm t[1]! + return q($x / $y) + | .INTS_MODULUS => + let x : Q(Int) ← rconsTerm t[0]! + let y : Q(Int) ← rconsTerm t[1]! + return q($x % $y) + | .DIVISION => + let x : Q(Rat) ← rconsTerm t[0]! + let y : Q(Rat) ← rconsTerm t[1]! + return q($x / $y) + | .ABS => + let x : Q(Int) ← rconsTerm t[0]! + return q(Int.natAbs $x : Int) + | .LEQ => + if t[0]!.getSort.isInteger then + let x : Q(Int) ← rconsTerm t[0]! + let y : Q(Int) ← rconsTerm t[1]! + return q($x ≤ $y) + else + let x : Q(Rat) ← rconsTerm t[0]! + let y : Q(Rat) ← rconsTerm t[1]! + return q($x ≤ $y) + | .LT => + if t[0]!.getSort.isInteger then + let x : Q(Int) ← rconsTerm t[0]! + let y : Q(Int) ← rconsTerm t[1]! + return q($x < $y) + else + let x : Q(Rat) ← rconsTerm t[0]! + let y : Q(Rat) ← rconsTerm t[1]! + return q($x < $y) + | .GEQ => + if t[0]!.getSort.isInteger then + let x : Q(Int) ← rconsTerm t[0]! + let y : Q(Int) ← rconsTerm t[1]! + return q($x ≥ $y) + else + let x : Q(Rat) ← rconsTerm t[0]! + let y : Q(Rat) ← rconsTerm t[1]! + return q($x ≥ $y) + | .GT => + if t[0]!.getSort.isInteger then + let x : Q(Int) ← rconsTerm t[0]! + let y : Q(Int) ← rconsTerm t[1]! + return q($x > $y) + else + let x : Q(Rat) ← rconsTerm t[0]! + let y : Q(Rat) ← rconsTerm t[1]! + return q($x > $y) + | .TO_REAL => + let x : Q(Int) ← rconsTerm t[0]! + return q($x : Rat) + | .TO_INTEGER => + let x : Q(Rat) ← rconsTerm t[0]! + return q(Rat.floor $x) + | .IS_INTEGER => + let x : Q(Rat) ← rconsTerm t[0]! + return q(Rat.isInt $x) + | _ => + logInfo m!"{repr t.getKind} : {t}" + return .const `sorry [] +where + rightAssocOp (op : Expr) (t : cvc5.Term) : MetaM Expr := do + let mut curr ← rconsTerm t[t.getNumChildren - 1]! + for i in [1:t.getNumChildren] do + curr := mkApp2 op (← rconsTerm t[t.getNumChildren - i - 1]!) curr + return curr + +structure RconsState where + termMap : HashMap cvc5.Term Name + proofMap : HashMap cvc5.Proof Name + count : Nat + trusts : Array cvc5.Proof + mainGoal : MVarId + currGoal : MVarId + currAssums : Array Expr + skipedGoals : Array MVarId + +abbrev RconsM := StateT RconsState MetaM + +namespace Rcons + +def incCount : RconsM Nat := + modifyGet fun state => (state.count, { state with count := state.count + 1 }) + +def cacheTerm (t : cvc5.Term) (n : Name) : RconsM Unit := + modify fun state => { state with termMap := state.termMap.insert t n } + +def getTermExpr (t : cvc5.Term) : RconsM Expr := + return .fvar ⟨(← get).termMap.find! t⟩ + +def cacheProof (p : cvc5.Proof) (n : Name) : RconsM Unit := + modify fun state => { state with proofMap := state.proofMap.insert p n } + +def isReconstructed (p : cvc5.Proof) : RconsM Bool := + return (← get).proofMap.contains p + +def getProofExpr (p : cvc5.Proof) : RconsM Expr := + return .fvar ⟨(← get).proofMap.find! p⟩ + +def withAssums (as : Array Expr) (k : RconsM α) : RconsM α := do + modify fun state => { state with currAssums := state.currAssums ++ as } + let r ← k + modify fun state => { state with currAssums := state.currAssums.shrink (state.currAssums.size - as.size) } + return r + +def skipStep (mv : MVarId) : RconsM Unit := mv.withContext do + let state ← get + let t ← Meta.mkForallFVars state.currAssums (← mv.getType) + let mv' ← state.mainGoal.withContext (Meta.mkFreshExprMVar t) + let e := mkAppN mv' state.currAssums + set { state with skipedGoals := state.skipedGoals.push mv'.mvarId! } + mv.assignIfDefeq e + +inductive Tac where + | rewrite : Expr → Expr → Expr → Array (Array Expr) → Tac + | r0 : Expr → Expr → Expr → Option Nat → Option Nat → Tac + | r1 : Expr → Expr → Expr → Option Nat → Option Nat → Tac + | factor : Expr → Option Nat → Tac + | reorder : Expr → Array Nat → Option Nat → Tac + | andElim : Expr → Nat → Tac + | notOrElim : Expr → Nat → Tac + | cong : Array Expr → Tac + | sumUB : Array Expr → Tac + | polyNorm : Tac + | mulSign : Array (Expr × Fin 3 × Nat) → Tac +deriving Repr + +instance : ToMessageData Tac where + toMessageData : Tac → MessageData + | .rewrite assoc null rule args => m!"rewrite {assoc} {null} {rule} {args}" + | .r0 v₁ v₂ p i₁ i₂ => m!"r0 {v₁} {v₂} ({p}) {i₁} {i₂}" + | .r1 v₁ v₂ p i₁ i₂ => m!"r1 {v₁} {v₂} ({p}) {i₁} {i₂}" + | .factor v i => m!"factor {v} {i}" + | .reorder n is i => m!"reorder {n} {is} {i}" + | .andElim n i => m!"andElim {n} {i}" + | .notOrElim n i => m!"notOrElim {n} {i}" + | .cong ns => m!"cong {ns}" + | .sumUB ns => m!"sumUB {ns}" + | .polyNorm => m!"polyNorm" + | .mulSign fs => m!"mulSign {fs}" + +def runTac (mv : MVarId) (tac : Tac) : RconsM Unit := mv.withContext do + match tac with + | .rewrite assoc null rule args => Tactic.smtRw mv assoc null rule args + | .r0 v₁ v₂ p i₁ i₂ => r₀ mv v₁ v₂ p i₁ i₂ + | .r1 v₁ v₂ p i₁ i₂ => r₁ mv v₁ v₂ p i₁ i₂ + | .factor v i => factor mv v i + | .reorder e is i => reorder mv e is i + | .andElim e i => andElim mv e i + | .notOrElim e i => notOrElim mv e i + | .cong es => UF.smtCongr mv es + | .sumUB _ => skipStep mv + | .polyNorm => skipStep mv + | .mulSign _ => skipStep mv + +def getCurrGoal : RconsM MVarId := + get >>= (pure ·.currGoal) + +def setCurrGoal (mv : MVarId) : RconsM Unit := + modify fun state => { state with currGoal := mv } + +def addThm (type : Expr) (val : Expr) : RconsM Expr := do + let mv ← getCurrGoal + mv.withContext do + let name := Name.num `s (← incCount) + let (fv, mv) ← (← mv.assert name type val).intro1P + trace[smt.debug.reconstruct] "have {name} : {type} := {val}" + setCurrGoal mv + return .fvar fv + +def addTac (type : Expr) (tac : Tac) : RconsM Expr := do + let mv ← getCurrGoal + mv.withContext do + let name := Name.num `s (← incCount) + let mv' ← Meta.mkFreshExprMVar type + runTac mv'.mvarId! tac + let (fv, mv) ← (← mv.assert name type mv').intro1P + trace[smt.debug.reconstruct] "have {name} : {type} := by {tac}" + setCurrGoal mv + return .fvar fv + +def addTrust (type : Expr) (pf : cvc5.Proof) : RconsM Expr := do + let mv ← getCurrGoal + mv.withContext do + let name := Name.num `s (← incCount) + let mv' ← Meta.mkFreshExprMVar type + skipStep mv'.mvarId! + let (fv, mv) ← (← mv.assert name type mv').intro1P + trace[smt.debug.reconstruct] m!"have {name} : {type} := sorry" + trace[smt.debug.reconstruct] + m!"rule : {repr pf.getRule}\npremises : {pf.getChildren.map (·.getResult)}\nargs : {pf.getArguments}\nconclusion : {pf.getResult}" + modify fun state => { state with trusts := state.trusts.push pf } + setCurrGoal mv + return .fvar fv + +def rconsRewrite (pf : cvc5.Proof) (cpfs : Array Expr) : RconsM Expr := do + match cvc5.RewriteRule.fromNat! pf.getArguments[0]!.getIntegerValue.toNat with + | .BOOL_DOUBLE_NOT_ELIM => + let p : Q(Prop) ← rconsTerm pf.getArguments[1]! + addThm q((¬¬$p) = $p) q(@Prop.bool_double_not_elim $p) + | .BOOL_EQ_TRUE => + let p : Q(Prop) ← rconsTerm pf.getArguments[1]! + addThm q(($p = True) = $p) q(@Prop.bool_eq_true $p) + | .BOOL_EQ_FALSE => + let p : Q(Prop) ← rconsTerm pf.getArguments[1]! + addThm q(($p = False) = ¬$p) q(@Prop.bool_eq_false $p) + | .BOOL_EQ_NREFL => + let p : Q(Prop) ← rconsTerm pf.getArguments[1]! + addThm q(($p = ¬$p) = False) q(@Prop.bool_eq_nrefl $p) + | .BOOL_IMPL_FALSE1 => + let p : Q(Prop) ← rconsTerm pf.getArguments[1]! + addThm q(($p → False) = ¬$p) q(@Prop.bool_impl_false1 $p) + | .BOOL_IMPL_FALSE2 => + let p : Q(Prop) ← rconsTerm pf.getArguments[1]! + addThm q((False → $p) = True) q(@Prop.bool_impl_false2 $p) + | .BOOL_IMPL_TRUE1 => + let p : Q(Prop) ← rconsTerm pf.getArguments[1]! + addThm q(($p → True) = True) q(@Prop.bool_impl_true1 $p) + | .BOOL_IMPL_TRUE2 => + let p : Q(Prop) ← rconsTerm pf.getArguments[1]! + addThm q((True → $p) = $p) q(@Prop.bool_impl_true2 $p) + | .BOOL_OR_TRUE => + let args ← rconsArgs pf.getArguments + addTac (← rconsTerm pf.getResult) (.rewrite q(@Prop.or_assoc_eq) q(or_true) q(@Prop.bool_or_true) args) + | .BOOL_OR_FALSE => + let args ← rconsArgs pf.getArguments + addTac (← rconsTerm pf.getResult) (.rewrite q(@Prop.or_assoc_eq) q(or_true) q(@Prop.bool_or_false) args) + | .BOOL_OR_FLATTEN => + let args ← rconsArgs pf.getArguments + addTac (← rconsTerm pf.getResult) (.rewrite q(@Prop.or_assoc_eq) q(or_true) q(@Prop.bool_or_flatten) args) + | .BOOL_OR_DUP => + let args ← rconsArgs pf.getArguments + addTac (← rconsTerm pf.getResult) (.rewrite q(@Prop.or_assoc_eq) q(or_true) q(@Prop.bool_or_dup) args) + | .BOOL_AND_TRUE => + let args ← rconsArgs pf.getArguments + addTac (← rconsTerm pf.getResult) (.rewrite q(@Prop.and_assoc_eq) q(and_true) q(@Prop.bool_and_true) args) + | .BOOL_AND_FALSE => + let args ← rconsArgs pf.getArguments + addTac (← rconsTerm pf.getResult) (.rewrite q(@Prop.and_assoc_eq) q(and_true) q(@Prop.bool_and_false) args) + | .BOOL_AND_FLATTEN => + let args ← rconsArgs pf.getArguments + addTac (← rconsTerm pf.getResult) (.rewrite q(@Prop.and_assoc_eq) q(and_true) q(@Prop.bool_and_flatten) args) + | .BOOL_AND_DUP => + let args ← rconsArgs pf.getArguments + addTac (← rconsTerm pf.getResult) (.rewrite q(@Prop.and_assoc_eq) q(and_true) q(@Prop.bool_and_dup) args) + | .BOOL_AND_CONF => + let args ← rconsArgs pf.getArguments + addTac (← rconsTerm pf.getResult) (.rewrite q(@Prop.and_assoc_eq) q(and_true) q(@Prop.bool_and_conf) args) + | .BOOL_OR_TAUT => + let args ← rconsArgs pf.getArguments + addTac (← rconsTerm pf.getResult) (.rewrite q(@Prop.or_assoc_eq) q(or_true) q(@Prop.bool_or_taut) args) + | .BOOL_XOR_REFL => + let p : Q(Prop) ← rconsTerm pf.getArguments[1]! + addThm q(XOr $p $p = False) q(@Prop.bool_xor_refl $p) + | .BOOL_XOR_NREFL => + let p : Q(Prop) ← rconsTerm pf.getArguments[1]! + addThm q((XOr $p ¬$p) = True) q(@Prop.bool_xor_nrefl $p) + | .BOOL_XOR_FALSE => + let p : Q(Prop) ← rconsTerm pf.getArguments[1]! + addThm q(XOr $p False = $p) q(@Prop.bool_xor_false $p) + | .BOOL_XOR_TRUE => + let p : Q(Prop) ← rconsTerm pf.getArguments[1]! + addThm q(XOr $p True = ¬$p) q(@Prop.bool_xor_true $p) + | .BOOL_XOR_COMM => + let p : Q(Prop) ← rconsTerm pf.getArguments[1]! + let q : Q(Prop) ← rconsTerm pf.getArguments[2]! + addThm q(XOr $p $q = XOr $q $p) q(@Prop.bool_xor_comm $p $q) + | .BOOL_XOR_ELIM => + let p : Q(Prop) ← rconsTerm pf.getArguments[1]! + let q : Q(Prop) ← rconsTerm pf.getArguments[2]! + addThm q(XOr $p $q = ¬($p = $q)) q(@Prop.bool_xor_elim $p $q) + | .ITE_NEG_BRANCH => + let c : Q(Prop) ← rconsTerm pf.getArguments[1]! + let p : Q(Prop) ← rconsTerm pf.getArguments[2]! + let q : Q(Prop) ← rconsTerm pf.getArguments[3]! + let hc : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c) + let h : Q($p = ¬$q) := cpfs[0]! + addThm q(ite $c $p $q = ($c = $p)) q(@Prop.ite_neg_branch $c $p $q $hc $h) + | .ITE_THEN_TRUE => + let c : Q(Prop) ← rconsTerm pf.getArguments[1]! + let p : Q(Prop) ← rconsTerm pf.getArguments[2]! + let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c) + addThm q(ite $c True $p = ($c ∨ $p)) q(@Prop.ite_then_true $c $p $h) + | .ITE_ELSE_FALSE => + let c : Q(Prop) ← rconsTerm pf.getArguments[1]! + let p : Q(Prop) ← rconsTerm pf.getArguments[2]! + let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c) + addThm q(ite $c $p False = ($c ∧ $p)) q(@Prop.ite_else_false $c $p $h) + | .ITE_THEN_FALSE => + let c : Q(Prop) ← rconsTerm pf.getArguments[1]! + let p : Q(Prop) ← rconsTerm pf.getArguments[2]! + let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c) + addThm q(ite $c False $p = (¬$c ∧ $p)) q(@Prop.ite_then_false $c $p $h) + | .ITE_ELSE_TRUE => + let c : Q(Prop) ← rconsTerm pf.getArguments[1]! + let p : Q(Prop) ← rconsTerm pf.getArguments[2]! + let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c) + addThm q(ite $c $p True = (¬$c ∨ $p)) q(@Prop.ite_else_true $c $p $h) + | .ITE_THEN_LOOKAHEAD_SELF => + let c : Q(Prop) ← rconsTerm pf.getArguments[1]! + let p : Q(Prop) ← rconsTerm pf.getArguments[2]! + let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c) + addThm q(ite $c $c $p = ite $c True $p) q(@Prop.ite_then_lookahead_self $c $p $h) + | .ITE_ELSE_LOOKAHEAD_SELF => + let c : Q(Prop) ← rconsTerm pf.getArguments[1]! + let p : Q(Prop) ← rconsTerm pf.getArguments[2]! + let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c) + addThm q(ite $c $p $c = ite $c $p False) q(@Prop.ite_else_lookahead_self $c $p $h) + | .ITE_TRUE_COND => + let α : Q(Type) ← rconsSort pf.getArguments[1]!.getSort + let x : Q($α) ← rconsTerm pf.getArguments[1]! + let y : Q($α) ← rconsTerm pf.getArguments[2]! + addThm q(ite True $x $y = $x) q(@Builtin.ite_true_cond $α $x $y) + | .ITE_FALSE_COND => + let α : Q(Type) ← rconsSort pf.getArguments[1]!.getSort + let x : Q($α) ← rconsTerm pf.getArguments[1]! + let y : Q($α) ← rconsTerm pf.getArguments[2]! + addThm q(ite False $x $y = $y) q(@Builtin.ite_false_cond $α $x $y) + | .ITE_NOT_COND => + let c : Q(Prop) ← rconsTerm pf.getArguments[1]! + let α : Q(Type) ← rconsSort pf.getArguments[2]!.getSort + let x : Q($α) ← rconsTerm pf.getArguments[2]! + let y : Q($α) ← rconsTerm pf.getArguments[3]! + let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c) + addThm q(ite (¬$c) $x $y = ite $c $y $x) q(@Builtin.ite_not_cond $c $α $x $y $h) + | .ITE_EQ_BRANCH => + let c : Q(Prop) ← rconsTerm pf.getArguments[1]! + let α : Q(Type) ← rconsSort pf.getArguments[2]!.getSort + let x : Q($α) ← rconsTerm pf.getArguments[2]! + let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c) + addThm q(ite $c $x $x = $x) q(@Builtin.ite_eq_branch $c $α $x $h) + | .ITE_THEN_LOOKAHEAD => + let c : Q(Prop) ← rconsTerm pf.getArguments[1]! + let α : Q(Type) ← rconsSort pf.getArguments[2]!.getSort + let x : Q($α) ← rconsTerm pf.getArguments[2]! + let y : Q($α) ← rconsTerm pf.getArguments[3]! + let z : Q($α) ← rconsTerm pf.getArguments[4]! + let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c) + addThm q(ite $c (ite $c $x $y) $z = ite $c $x $z) q(@Builtin.ite_then_lookahead $c $α $x $y $z $h) + | .ITE_ELSE_LOOKAHEAD => + let c : Q(Prop) ← rconsTerm pf.getArguments[1]! + let α : Q(Type) ← rconsSort pf.getArguments[2]!.getSort + let x : Q($α) ← rconsTerm pf.getArguments[2]! + let y : Q($α) ← rconsTerm pf.getArguments[3]! + let z : Q($α) ← rconsTerm pf.getArguments[4]! + let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c) + addThm q(ite $c $x (ite $c $y $z) = ite $c $x $z) q(@Builtin.ite_else_lookahead $c $α $x $y $z $h) + | .ITE_THEN_NEG_LOOKAHEAD => + let c : Q(Prop) ← rconsTerm pf.getArguments[1]! + let α : Q(Type) ← rconsSort pf.getArguments[2]!.getSort + let x : Q($α) ← rconsTerm pf.getArguments[2]! + let y : Q($α) ← rconsTerm pf.getArguments[3]! + let z : Q($α) ← rconsTerm pf.getArguments[4]! + let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c) + addThm q(ite $c (ite (¬$c) $x $y) $z = ite $c $y $z) q(@Builtin.ite_then_neg_lookahead $c $α $x $y $z $h) + | .ITE_ELSE_NEG_LOOKAHEAD => + let c : Q(Prop) ← rconsTerm pf.getArguments[1]! + let α : Q(Type) ← rconsSort pf.getArguments[2]!.getSort + let x : Q($α) ← rconsTerm pf.getArguments[2]! + let y : Q($α) ← rconsTerm pf.getArguments[3]! + let z : Q($α) ← rconsTerm pf.getArguments[4]! + let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c) + addThm q(ite $c $x (ite (¬$c) $y $z) = ite $c $x $y) q(@Builtin.ite_else_neg_lookahead $c $α $x $y $z $h) + | .EQ_REFL => + let α : Q(Type) ← rconsSort pf.getArguments[1]!.getSort + let t : Q($α) ← rconsTerm pf.getArguments[1]! + addThm q(($t = $t) = True) q(@UF.eq_refl $α $t) + | .EQ_SYMM => + let α : Q(Type) ← rconsSort pf.getArguments[1]!.getSort + let t : Q($α) ← rconsTerm pf.getArguments[1]! + let s : Q($α) ← rconsTerm pf.getArguments[2]! + addThm q(($t = $s) = ($s = $t)) q(@UF.eq_symm $α $t $s) + | .DISTINCT_BINARY_ELIM => + let α : Q(Type) ← rconsSort pf.getArguments[1]!.getSort + let t : Q($α) ← rconsTerm pf.getArguments[1]! + let s : Q($α) ← rconsTerm pf.getArguments[2]! + addThm q(($t ≠ $s) = ¬($t = $s)) q(@UF.distinct_binary_elim $α $t $s) + | _ => + let type ← rconsTerm pf.getResult + addTrust type pf +where + rconsArgs (args : Array cvc5.Term) : MetaM (Array (Array Expr)) := do + let mut args' := #[] + for arg in args do + let mut arg' := #[] + for subarg in arg do + arg' := arg'.push (← rconsTerm subarg) + args' := args'.push arg' + return args' + +def rconsChainResolution (cs as : Array cvc5.Term) (ps : Array Expr) : RconsM Expr := do + let mut cc := clausify cs[0]! + let mut cp := ps[0]! + for i in [1:cs.size] do + let pol := as[2 * i - 2]! + let l := as[2 * i - 1]! + cp ← rconsResolution cc (clausify cs[i]!) pol l cp ps[i]! + cc := getResolutionResult cc (clausify cs[i]!) pol l + return cp +where + clausify (c : cvc5.Term) : Array cvc5.Term := Id.run do + if c.getKind != .OR then + return #[c] + let mut cs := #[] + for cc in c do + cs := cs.push cc + return cs + rconsResolution (c₁ c₂ : Array cvc5.Term) (pol l : cvc5.Term) (p₁ p₂ : Expr) : RconsM Expr := do + let f := if pol.getBooleanValue == true then Tac.r0 else Tac.r1 + addTac (← rightAssocOp q(Or) (getResolutionResult c₁ c₂ pol l)) (f p₁ p₂ (← rconsTerm l) (some (c₁.size - 1)) (some (c₂.size - 1))) + getResolutionResult (c₁ c₂ : Array cvc5.Term) (pol l : cvc5.Term) : Array cvc5.Term := Id.run do + let l₁ := if pol.getBooleanValue then l else l.not + let l₂ := if pol.getBooleanValue then l.not else l + let mut ls := #[] + for li in c₁ do + if li != l₁ then + ls := ls.push li + for li in c₂ do + if li != l₂ then + ls := ls.push li + return ls + rightAssocOp (op : Expr) (ts : Array cvc5.Term) : MetaM Expr := do + if ts.isEmpty then + return q(False) + let mut curr ← rconsTerm ts[ts.size - 1]! + for i in [1:ts.size] do + curr := mkApp2 op (← rconsTerm ts[ts.size - i - 1]!) curr + return curr + +def rconsScope (pf : cvc5.Proof) (rconsProof : cvc5.Proof → RconsM Expr) : RconsM Expr := do + let mv ← getCurrGoal + mv.withContext do + let f := fun arg ps => do + let p : Q(Prop) ← rconsTerm arg + return q($p :: $ps) + let ps : Q(List Prop) ← pf.getArguments.foldrM f q([]) + let as ← pf.getArguments.mapM (fun _ => return Name.num `a (← incCount)) + let q : Q(Prop) ← rconsTerm pf.getChildren[0]!.getResult + let h₁ : Q(impliesN $ps $q) ← Meta.mkFreshExprMVar q(impliesN $ps $q) + let (fvs, mv') ← h₁.mvarId!.introN pf.getArguments.size as.toList + setCurrGoal mv' + mv'.withContext do + let h₂ : Q($q) ← withAssums (fvs.map Expr.fvar) (rconsProof pf.getChildren[0]!) + let mv'' ← getCurrGoal + mv''.withContext (mv''.assignIfDefeq h₂) + setCurrGoal mv + addThm q(andN $ps → $q) q(Prop.scopes $h₁) + +def rconsForallCong (pf : cvc5.Proof) (rconsProof : cvc5.Proof → RconsM Expr) : RconsM Expr := do + let mv ← getCurrGoal + mv.withContext do + let n := Name.str Name.anonymous pf.getResult[0]![0]![0]!.getSymbol + let α : Q(Type) ← rconsSort pf.getResult[0]![0]![0]!.getSort + let mkLam n α t := Meta.withLocalDeclD n α (rconsTerm t >>= Meta.mkLambdaFVars #[·]) + let p : Q($α → Prop) ← mkLam n α pf.getResult[0]![1]! + let q : Q($α → Prop) ← mkLam n α pf.getResult[1]![1]! + let h : Q(∀ a, $p a = $q a) ← Meta.mkFreshExprMVar q(∀ a, $p a = $q a) + let (fv, mv') ← h.mvarId!.intro n + let a : Q($α) ← (return .fvar fv) + setCurrGoal mv' + let h' : Q($p $a = $q $a) ← mv'.withContext (withAssums #[a] (rconsProof pf.getChildren[1]!)) + let mv' ← getCurrGoal + mv'.withContext (mv'.assignIfDefeq h') + setCurrGoal mv + addThm q((∀ a, $p a) = (∀ a, $q a)) q(forall_congr $h) + +partial def rconsProof (pf : cvc5.Proof) : RconsM Expr := do + if (← isReconstructed pf) && (← Meta.findLocalDeclWithType? (← rconsTerm pf.getResult)).isSome then + return ← getProofExpr pf + let e ← do match pf.getRule with + | .ASSUME => + let p : Q(Prop) ← rconsTerm pf.getArguments[0]! + match (← Meta.findLocalDeclWithType? p) with + | none => throwError "no assumption of type\n\t{p}\nfound in local context" + | some fv => return .fvar fv + | .SCOPE => + rconsScope pf rconsProof + | .EVALUATE => + let α : Q(Type) ← rconsSort pf.getResult[0]!.getSort + -- TODO: handle case where a Prop is inside an expression + if α.isProp then + let p : Q(Prop) ← rconsTerm pf.getResult[0]! + let p' : Q(Prop) ← rconsTerm pf.getResult[1]! + addThm q($p = $p') (← Meta.mkAppOptM ``of_decide_eq_true #[q($p = $p'), none, q(Eq.refl true)]) + else + let t : Q($α) ← rconsTerm pf.getResult[0]! + let t' : Q($α) ← rconsTerm pf.getResult[1]! + addThm q($t = $t') q(Eq.refl $t) + | .DSL_REWRITE => + rconsRewrite pf (← pf.getChildren.mapM rconsProof) + | .RESOLUTION + | .CHAIN_RESOLUTION => + let cs := pf.getChildren.map (·.getResult) + let as := pf.getArguments + let ps ← pf.getChildren.mapM rconsProof + rconsChainResolution cs as ps + | .FACTORING => + -- as an argument we pass whether the suffix of the factoring clause is a + -- singleton *repeated* literal. This is marked by a number as in + -- resolution. + let children := pf.getChildren + let lastPremiseLit := children[0]!.getResult[children[0]!.getResult.getNumChildren - 1]! + let resOriginal := pf.getResult + -- For the last premise literal to be a singleton repeated literal, either + -- it is equal to the result (in which case the premise was just n + -- occurrences of it), or the end of the original clause is different from + -- the end of the resulting one. In principle we'd need to add the + -- singleton information only for OR nodes, so we could avoid this test if + -- the result is not an OR node. However given the presence of + -- purification boolean variables which can stand for OR nodes (and could + -- thus be ambiguous in the final step, with the purification remove), we + -- do the general test. + let singleton := if lastPremiseLit == resOriginal || (resOriginal.getKind == .OR && lastPremiseLit != resOriginal[resOriginal.getNumChildren - 1]!) + then some (children[0]!.getResult.getNumChildren - 1) else none; + addTac (← rconsTerm pf.getResult) (.factor (← rconsProof children[0]!) singleton) + | .REORDERING => + let children := pf.getChildren + let size := pf.getResult.getNumChildren + let lastPremiseLit := children[0]!.getResult[size - 1]! + -- none if tail of the clause is not an OR (i.e., it cannot be a singleton) + let singleton := if lastPremiseLit.getKind == .OR then some (size - 1) else none + -- for each literal in the resulting clause, get its position in the premise + let mut pos := #[] + for resLit in pf.getResult do + for i in [:size] do + if children[0]!.getResult[i]! == resLit then + pos := pos.push i + -- turn conclusion into clause + addTac (← rconsTerm pf.getResult) (.reorder (← rconsProof children[0]!) pos singleton) + | .SPLIT => + let q : Q(Prop) ← rconsTerm pf.getArguments[0]! + addThm q($q ∨ ¬$q) q(Classical.em $q) + | .EQ_RESOLVE => + let p : Q(Prop) ← rconsTerm pf.getChildren[0]!.getResult + let q : Q(Prop) ← rconsTerm pf.getResult + let hp : Q($p) ← rconsProof pf.getChildren[0]! + let hpq : Q($p = $q) ← rconsProof pf.getChildren[1]! + addThm q($q) q(Prop.eqResolve $hp $hpq) + | .MODUS_PONENS => + let p : Q(Prop) ← rconsTerm pf.getChildren[0]!.getResult + let q : Q(Prop) ← rconsTerm pf.getResult + let hp : Q($p) ← rconsProof pf.getChildren[0]! + let hpq : Q($p → $q) ← rconsProof pf.getChildren[1]! + addThm q($q) q(Prop.modusPonens $hp $hpq) + | .NOT_NOT_ELIM => + let p : Q(Prop) ← rconsTerm pf.getResult + let hnnp : Q(¬¬$p) ← rconsProof pf.getChildren[0]! + addThm q($p) q(Prop.notNotElim $hnnp) + | .CONTRA => + let p : Q(Prop) ← rconsTerm pf.getChildren[0]!.getResult + let hp : Q($p) ← rconsProof pf.getChildren[0]! + let hnp : Q(¬$p) ← rconsProof pf.getChildren[0]! + addThm q(False) q(Prop.contradiction $hp $hnp) + | .AND_ELIM => + addTac (← rconsTerm pf.getResult) (.andElim (← rconsProof pf.getChildren[0]!) pf.getArguments[0]!.getIntegerValue.toNat) + | .AND_INTRO => + let cpfs := pf.getChildren + let q : Q(Prop) ← rconsTerm cpfs.back.getResult + let hq : Q($q) ← rconsProof cpfs.back + let f := fun pf ⟨q, hq⟩ => do + let p : Q(Prop) ← rconsTerm pf.getResult + let hp : Q($p) ← rconsProof pf + let hq ← addThm q($p ∧ $q) q(And.intro $hp $hq) + let q := q($p ∧ $q) + return ⟨q, hq⟩ + let ⟨_, hq⟩ ← cpfs.pop.foldrM f (⟨q, hq⟩ : Σ q : Q(Prop), Q($q)) + return hq + | .NOT_OR_ELIM => + addTac (← rconsTerm pf.getResult) (.notOrElim (← rconsProof pf.getChildren[0]!) pf.getArguments[0]!.getIntegerValue.toNat) + | .IMPLIES_ELIM => + let p : Q(Prop) ← rconsTerm pf.getChildren[0]!.getResult[0]! + let q : Q(Prop) ← rconsTerm pf.getChildren[0]!.getResult[1]! + let hpq : Q($p → $q) ← rconsProof pf.getChildren[0]! + addThm q(¬$p ∨ $q) q(Prop.impliesElim $hpq) + | .NOT_IMPLIES_ELIM1 => + let p : Q(Prop) ← rconsTerm pf.getResult + let q : Q(Prop) ← rconsTerm pf.getChildren[0]!.getResult[0]![1]! + let hnpq : Q(¬($p → $q)) ← rconsProof pf.getChildren[0]! + addThm q($p) q(Prop.notImplies1 $hnpq) + | .NOT_IMPLIES_ELIM2 => + let p : Q(Prop) ← rconsTerm pf.getChildren[0]!.getResult[0]![0]! + let q : Q(Prop) ← rconsTerm pf.getResult[0]! + let hnpq : Q(¬($p → $q)) ← rconsProof pf.getChildren[0]! + addThm q(¬$q) q(Prop.notImplies2 $hnpq) + | .EQUIV_ELIM1 => + let p : Q(Prop) ← rconsTerm pf.getResult[0]![0]! + let q : Q(Prop) ← rconsTerm pf.getResult[1]! + let hpq : Q($p = $q) ← rconsProof pf.getChildren[0]! + addThm q(¬$p ∨ $q) q(Prop.equivElim1 $hpq) + | .EQUIV_ELIM2 => + let p : Q(Prop) ← rconsTerm pf.getResult[0]! + let q : Q(Prop) ← rconsTerm pf.getResult[1]![0]! + let hpq : Q($p = $q) ← rconsProof pf.getChildren[0]! + addThm q($p ∨ ¬$q) q(Prop.equivElim2 $hpq) + | .NOT_EQUIV_ELIM1 => + let p : Q(Prop) ← rconsTerm pf.getResult[0]! + let q : Q(Prop) ← rconsTerm pf.getResult[1]! + let hnpq : Q($p ≠ $q) ← rconsProof pf.getChildren[0]! + addThm q($p ∨ $q) q(Prop.notEquivElim1 $hnpq) + | .NOT_EQUIV_ELIM2 => + let p : Q(Prop) ← rconsTerm pf.getResult[0]![0]! + let q : Q(Prop) ← rconsTerm pf.getResult[1]![0]! + let hnpq : Q($p ≠ $q) ← rconsProof pf.getChildren[0]! + addThm q(¬$p ∨ ¬$q) q(Prop.notEquivElim2 $hnpq) + | .XOR_ELIM1 => + let p : Q(Prop) ← rconsTerm pf.getResult[0]! + let q : Q(Prop) ← rconsTerm pf.getResult[1]! + let hpq : Q(XOr $p $q) ← rconsProof pf.getChildren[0]! + addThm q($p ∨ $q) q(Prop.xorElim1 $hpq) + | .XOR_ELIM2 => + let p : Q(Prop) ← rconsTerm pf.getResult[0]![0]! + let q : Q(Prop) ← rconsTerm pf.getResult[1]![0]! + let hpq : Q(XOr $p $q) ← rconsProof pf.getChildren[0]! + addThm q(¬$p ∨ ¬$q) q(Prop.xorElim2 $hpq) + | .NOT_XOR_ELIM1 => + let p : Q(Prop) ← rconsTerm pf.getResult[0]! + let q : Q(Prop) ← rconsTerm pf.getResult[1]![0]! + let hnpq : Q(¬XOr $p $q) ← rconsProof pf.getChildren[0]! + addThm q($p ∨ ¬$q) q(Prop.notXorElim1 $hnpq) + | .NOT_XOR_ELIM2 => + let p : Q(Prop) ← rconsTerm pf.getResult[0]![0]! + let q : Q(Prop) ← rconsTerm pf.getResult[1]! + let hnpq : Q(¬XOr $p $q) ← rconsProof pf.getChildren[0]! + addThm q(¬$p ∨ $q) q(Prop.notXorElim2 $hnpq) + | .ITE_ELIM1 => + let c : Q(Prop) ← rconsTerm pf.getChildren[0]!.getResult[0]! + let hc : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c) + let p : Q(Prop) ← rconsTerm pf.getChildren[0]!.getResult[1]! + let q : Q(Prop) ← rconsTerm pf.getChildren[0]!.getResult[2]! + let h : Q(@ite Prop $c $hc $p $q) ← rconsProof pf.getChildren[0]! + addThm q(¬$c ∨ $p) q(Prop.iteElim1 $h) + | .ITE_ELIM2 => + let c : Q(Prop) ← rconsTerm pf.getChildren[0]!.getResult[0]! + let hc : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c) + let p : Q(Prop) ← rconsTerm pf.getChildren[0]!.getResult[1]! + let q : Q(Prop) ← rconsTerm pf.getChildren[0]!.getResult[2]! + let h : Q(@ite Prop $c $hc $p $q) ← rconsProof pf.getChildren[0]! + addThm q($c ∨ $q) q(Prop.iteElim2 $h) + | .NOT_ITE_ELIM1 => + let c : Q(Prop) ← rconsTerm pf.getChildren[0]!.getResult[0]![0]! + let hc : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c) + let p : Q(Prop) ← rconsTerm pf.getChildren[0]!.getResult[0]![1]! + let q : Q(Prop) ← rconsTerm pf.getChildren[0]!.getResult[0]![2]! + let hn : Q(¬@ite Prop $c $hc $p $q) ← rconsProof pf.getChildren[0]! + addThm q(¬$c ∨ ¬$p) q(Prop.notIteElim1 $hn) + | .NOT_ITE_ELIM2 => + let c : Q(Prop) ← rconsTerm pf.getChildren[0]!.getResult[0]![0]! + let hc : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c) + let p : Q(Prop) ← rconsTerm pf.getChildren[0]!.getResult[0]![1]! + let q : Q(Prop) ← rconsTerm pf.getChildren[0]!.getResult[0]![2]! + let hn : Q(¬@ite Prop $c $hc $p $q) ← rconsProof pf.getChildren[0]! + addThm q($c ∨ ¬$q) q(Prop.notIteElim2 $hn) + | .NOT_AND => + let fs := pf.getChildren[0]!.getResult[0]! + let mut ps : Q(List Prop) := q([]) + let n := fs.getNumChildren + for i in [:n] do + let p : Q(Prop) ← rconsTerm fs[n - i - 1]! + ps := q($p :: $ps) + let hnps : Q(¬andN $ps) ← rconsProof pf.getChildren[0]! + addThm (← rconsTerm pf.getResult) (.app q(Prop.notAnd $ps) hnps) + | .CNF_AND_POS => + let cnf := pf.getArguments[0]! + let i : Q(Nat) := mkNatLit pf.getArguments[1]!.getIntegerValue.toNat + let mut ps : Q(List Prop) := q([]) + let n := cnf.getNumChildren + for i in [:n] do + let p : Q(Prop) ← rconsTerm cnf[n - i - 1]! + ps := q($p :: $ps) + addThm (← rconsTerm pf.getResult) q(Prop.cnfAndPos $ps $i) + | .CNF_AND_NEG => + let cnf := pf.getArguments[0]! + let mut ps : Q(List Prop) := q([]) + let n := cnf.getNumChildren + for i in [:n] do + let p : Q(Prop) ← rconsTerm cnf[n - i - 1]! + ps := q($p :: $ps) + addThm (← rconsTerm pf.getResult) q(Prop.cnfAndNeg $ps) + | .CNF_OR_POS => + let cnf := pf.getArguments[0]! + let mut ps : Q(List Prop) := q([]) + let n := cnf.getNumChildren + for i in [:n] do + let p : Q(Prop) ← rconsTerm cnf[n - i - 1]! + ps := q($p :: $ps) + addThm (← rconsTerm pf.getResult) q(Prop.cnfOrPos $ps) + | .CNF_OR_NEG => + let cnf := pf.getArguments[0]! + let i : Q(Nat) := mkNatLit pf.getArguments[1]!.getIntegerValue.toNat + let mut ps : Q(List Prop) := q([]) + let n := cnf.getNumChildren + for i in [:n] do + let p : Q(Prop) ← rconsTerm cnf[n - i - 1]! + ps := q($p :: $ps) + addThm (← rconsTerm pf.getResult) q(Prop.cnfOrNeg $ps $i) + | .CNF_IMPLIES_POS => + let p : Q(Prop) ← rconsTerm pf.getArguments[0]![0]! + let q : Q(Prop) ← rconsTerm pf.getArguments[0]![1]! + addThm q(¬($p → $q) ∨ ¬$p ∨ $q) q(@Prop.cnfImpliesPos $p $q) + | .CNF_IMPLIES_NEG1 => + let p : Q(Prop) ← rconsTerm pf.getArguments[0]![0]! + let q : Q(Prop) ← rconsTerm pf.getArguments[0]![1]! + addThm q(($p → $q) ∨ $p) q(@Prop.cnfImpliesNeg1 $p $q) + | .CNF_IMPLIES_NEG2 => + let p : Q(Prop) ← rconsTerm pf.getArguments[0]![0]! + let q : Q(Prop) ← rconsTerm pf.getArguments[0]![1]! + addThm q(($p → $q) ∨ ¬$q) q(@Prop.cnfImpliesNeg2 $p $q) + | .CNF_EQUIV_POS1 => + let p : Q(Prop) ← rconsTerm pf.getArguments[0]![0]! + let q : Q(Prop) ← rconsTerm pf.getArguments[0]![1]! + addThm q($p ≠ $q ∨ ¬$p ∨ $q) q(@Prop.cnfEquivPos1 $p $q) + | .CNF_EQUIV_POS2 => + let p : Q(Prop) ← rconsTerm pf.getArguments[0]![0]! + let q : Q(Prop) ← rconsTerm pf.getArguments[0]![1]! + addThm q($p ≠ $q ∨ $p ∨ ¬$q) q(@Prop.cnfEquivPos2 $p $q) + | .CNF_EQUIV_NEG1 => + let p : Q(Prop) ← rconsTerm pf.getArguments[0]![0]! + let q : Q(Prop) ← rconsTerm pf.getArguments[0]![1]! + addThm q($p = $q ∨ $p ∨ $q) q(@Prop.cnfEquivNeg1 $p $q) + | .CNF_EQUIV_NEG2 => + let p : Q(Prop) ← rconsTerm pf.getArguments[0]![0]! + let q : Q(Prop) ← rconsTerm pf.getArguments[0]![1]! + addThm q($p = $q ∨ ¬$p ∨ ¬$q) q(@Prop.cnfEquivNeg2 $p $q) + | .CNF_XOR_POS1 => + let p : Q(Prop) ← rconsTerm pf.getArguments[0]![0]! + let q : Q(Prop) ← rconsTerm pf.getArguments[0]![1]! + addThm q(¬XOr $p $q ∨ $p ∨ $q) q(@Prop.cnfXorPos1 $p $q) + | .CNF_XOR_POS2 => + let p : Q(Prop) ← rconsTerm pf.getArguments[0]![0]! + let q : Q(Prop) ← rconsTerm pf.getArguments[0]![1]! + addThm q(¬XOr $p $q ∨ ¬$p ∨ ¬$q) q(@Prop.cnfXorPos2 $p $q) + | .CNF_XOR_NEG1 => + let p : Q(Prop) ← rconsTerm pf.getArguments[0]![0]! + let q : Q(Prop) ← rconsTerm pf.getArguments[0]![1]! + addThm q(XOr $p $q ∨ ¬$p ∨ $q) q(@Prop.cnfXorNeg1 $p $q) + | .CNF_XOR_NEG2 => + let p : Q(Prop) ← rconsTerm pf.getArguments[0]![0]! + let q : Q(Prop) ← rconsTerm pf.getArguments[0]![1]! + addThm q(XOr $p $q ∨ $p ∨ ¬$q) q(@Prop.cnfXorNeg2 $p $q) + | .CNF_ITE_POS1 => + let c : Q(Prop) ← rconsTerm pf.getArguments[0]![0]! + let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c) + let p : Q(Prop) ← rconsTerm pf.getArguments[0]![1]! + let q : Q(Prop) ← rconsTerm pf.getArguments[0]![2]! + addThm q(¬(ite $c $p $q) ∨ ¬$c ∨ $p) q(@Prop.cnfItePos1 $c $p $q $h) + | .CNF_ITE_POS2 => + let c : Q(Prop) ← rconsTerm pf.getArguments[0]![0]! + let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c) + let p : Q(Prop) ← rconsTerm pf.getArguments[0]![1]! + let q : Q(Prop) ← rconsTerm pf.getArguments[0]![2]! + addThm q(¬(ite $c $p $q) ∨ $c ∨ $q) q(@Prop.cnfItePos2 $c $p $q $h) + | .CNF_ITE_POS3 => + let c : Q(Prop) ← rconsTerm pf.getArguments[0]![0]! + let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c) + let p : Q(Prop) ← rconsTerm pf.getArguments[0]![1]! + let q : Q(Prop) ← rconsTerm pf.getArguments[0]![2]! + addThm q(¬(ite $c $p $q) ∨ $p ∨ $q) q(@Prop.cnfItePos3 $c $p $q $h) + | .CNF_ITE_NEG1 => + let c : Q(Prop) ← rconsTerm pf.getArguments[0]![0]! + let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c) + let p : Q(Prop) ← rconsTerm pf.getArguments[0]![1]! + let q : Q(Prop) ← rconsTerm pf.getArguments[0]![2]! + addThm q(ite $c $p $q ∨ ¬$c ∨ ¬$p) q(@Prop.cnfIteNeg1 $c $p $q $h) + | .CNF_ITE_NEG2 => + let c : Q(Prop) ← rconsTerm pf.getArguments[0]![0]! + let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c) + let p : Q(Prop) ← rconsTerm pf.getArguments[0]![1]! + let q : Q(Prop) ← rconsTerm pf.getArguments[0]![2]! + addThm q(ite $c $p $q ∨ $c ∨ ¬$q) q(@Prop.cnfIteNeg2 $c $p $q $h) + | .CNF_ITE_NEG3 => + let c : Q(Prop) ← rconsTerm pf.getArguments[0]![0]! + let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c) + let p : Q(Prop) ← rconsTerm pf.getArguments[0]![1]! + let q : Q(Prop) ← rconsTerm pf.getArguments[0]![2]! + addThm q(ite $c $p $q ∨ ¬$p ∨ ¬$q) q(@Prop.cnfIteNeg3 $c $p $q $h) + | .REFL => + let α : Q(Type) ← rconsSort pf.getArguments[0]!.getSort + let a : Q($α) ← rconsTerm pf.getArguments[0]! + addThm q($a = $a) q(Eq.refl $a) + | .SYMM => + let α : Q(Type) ← rconsSort pf.getResult[0]!.getSort + let a : Q($α) ← rconsTerm pf.getResult[1]! + let b : Q($α) ← rconsTerm pf.getResult[0]! + if pf.getResult.getKind == .EQUAL then + let h : Q($a = $b) ← rconsProof pf.getChildren[0]! + addThm q($b = $a) q(Eq.symm $h) + else + let h : Q($a ≠ $b) ← rconsProof pf.getChildren[0]! + addThm q($b ≠ $a) q(Ne.symm $h) + | .TRANS => + let cpfs := pf.getChildren + let α : Q(Type) ← rconsSort cpfs[0]!.getResult[0]!.getSort + let a : Q($α) ← rconsTerm cpfs[0]!.getResult[0]! + let mut curr ← rconsProof cpfs[0]! + for i in [1:cpfs.size] do + let b : Q($α) ← rconsTerm cpfs[i]!.getResult[0]! + let c : Q($α) ← rconsTerm cpfs[i]!.getResult[1]! + let hab : Q($a = $b) := curr + let hbc : Q($b = $c) ← rconsProof cpfs[i]! + curr ← addThm q($a = $c) q(Eq.trans $hab $hbc) + return curr + | .CONG => + let k := pf.getResult[0]!.getKind + -- This rule is messed up for closures! + if k == .FORALL then + rconsForallCong pf rconsProof + else if k == .EXISTS || k == .WITNESS || k == .LAMBDA || k == .SET_COMPREHENSION then + let type ← rconsTerm pf.getResult + addTrust type pf + else + let mut assums ← pf.getChildren.mapM rconsProof + addTac (← rconsTerm pf.getResult) (.cong assums) + | .TRUE_INTRO => + let p : Q(Prop) ← rconsTerm pf.getResult[0]! + let hp : Q($p) ← rconsProof pf.getChildren[0]! + addThm q($p = True) q(Prop.trueIntro $hp) + | .TRUE_ELIM => + let p : Q(Prop) ← rconsTerm pf.getResult[0]! + let hp : Q($p = True) ← rconsProof pf.getChildren[0]! + addThm q($p) q(Prop.trueElim $hp) + | .FALSE_INTRO => + let p : Q(Prop) ← rconsTerm pf.getResult[0]! + let hnp : Q(¬$p) ← rconsProof pf.getChildren[0]! + addThm q($p = False) q(Prop.falseIntro $hnp) + | .FALSE_ELIM => + let p : Q(Prop) ← rconsTerm pf.getResult[0]! + let hnp : Q($p = False) ← rconsProof pf.getChildren[0]! + addThm q(¬$p) q(Prop.falseElim $hnp) + | .BETA_REDUCE => + let α : Q(Type) ← rconsSort pf.getResult[0]!.getSort + let t : Q($α) ← rconsTerm pf.getResult[0]! + let t' : Q($α) ← rconsTerm pf.getResult[1]! + addThm q($t = $t') q(Eq.refl $t) + | .INSTANTIATE => + let xsF : Q(Prop) ← rconsProof pf.getChildren[0]! + let es ← (pf.getArguments.extract 0 pf.getChildren[0]!.getResult[0]!.getNumChildren).mapM (rconsTerm ·) + addThm (← rconsTerm pf.getResult) (mkAppN xsF es) + | .ALPHA_EQUIV => + let α : Q(Type) ← rconsSort pf.getResult[0]!.getSort + let t : Q($α) ← rconsTerm pf.getResult[0]! + let t' : Q($α) ← rconsTerm pf.getResult[1]! + addThm q($t = $t') q(Eq.refl $t) + | _ => + _ ← pf.getChildren.mapM rconsProof + let type ← rconsTerm pf.getResult + addTrust type pf + cacheProof pf e.fvarId!.name + return e + +end Rcons + +partial def rconsProof (mv : MVarId) (pf : cvc5.Proof) : MetaM (FVarId × MVarId × List MVarId) := do + let p : Q(Prop) ← rconsTerm (pf.getResult) + let Prod.mk (h : Q(True → $p)) (.mk _ _ _ _ _ mv _ mvs) ← StateT.run (Rcons.rconsProof pf) ⟨{}, {}, 0, #[], mv, mv, #[], #[]⟩ + let ⟨fv, mv, _⟩ ← mv.replace h.fvarId! q($h trivial) q($p) + return (fv, mv, mvs.toList) + +syntax (name := reconstruct) "reconstruct" str : tactic + +open cvc5 in +def prove (query : String) (timeout : Option Nat) : Lean.MetaM (Except SolverError cvc5.Proof) := Solver.run do + if let .some timeout := timeout then + Solver.setOption "tlimit" (toString (1000*timeout)) + Solver.setOption "dag-thresh" "0" + Solver.setOption "simplification" "none" + Solver.setOption "produce-models" "true" + Solver.setOption "produce-proofs" "true" + Solver.setOption "proof-granularity" "dsl-rewrite" + Solver.setOption "enum-inst" "true" + Solver.parse query + let r ← Solver.checkSat + if r.isUnsat then + let ps ← Solver.getProof + if h : 0 < ps.size then + trace[smt.debug.reconstruct] (← Solver.proofToString ps[0]) + return ps[0] + throw (self := instMonadExcept _ _) (SolverError.user_error "something went wrong") + +open Lean.Elab Tactic in +@[tactic reconstruct] def evalReconstruct : Tactic := fun stx => + withMainContext do + let some query := stx[1].isStrLit? | throwError "expected string" + let r ← prove query none + match r with + | .error e => logInfo (repr e) + | .ok pf => + let (_, mv, mvs) ← rconsProof (← getMainGoal) pf + replaceMainGoal (mv :: mvs) + +end Smt.Reconstruct diff --git a/Smt/Reconstruct/UF/Rewrites.lean b/Smt/Reconstruct/UF/Rewrites.lean index 6b0ea1af..330aa158 100644 --- a/Smt/Reconstruct/UF/Rewrites.lean +++ b/Smt/Reconstruct/UF/Rewrites.lean @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Abdalrhman Mohamed -/ -namespace Smt.Reconstruct.Rewrites.UF +namespace Smt.Reconstruct.UF -- https://github.com/cvc5/cvc5/blob/proof-new/src/theory/uf/rewrites @@ -16,4 +16,4 @@ theorem eq_symm : (t = s) = (s = t) := propext ⟨(· ▸ rfl), (· ▸ rfl)⟩ theorem distinct_binary_elim : (t ≠ s) = ¬(t = s) := rfl -end Smt.Reconstruct.Rewrites.UF +end Smt.Reconstruct.UF diff --git a/Smt/Tactic/Smt.lean b/Smt/Tactic/Smt.lean index 3059edf2..416cf303 100644 --- a/Smt/Tactic/Smt.lean +++ b/Smt/Tactic/Smt.lean @@ -21,7 +21,6 @@ open Smt Reconstruct Translate Query Solver initialize registerTraceClass `smt.debug registerTraceClass `smt.debug.attr - registerTraceClass `smt.debug.reconstruct registerTraceClass `smt.debug.translate.query registerTraceClass `smt.debug.translate.expr @@ -96,7 +95,7 @@ def prepareSmtQuery (hs : List Expr) : TacticM (List Command) := do def elabProof (text : String) : TacticM Name := do let name ← mkFreshId - let name := Name.str name.getPrefix ("th0" ++ name.getString) + let name := Name.str name.getPrefix ("th0" ++ name.toString) let text := text.replace "th0" s!"{name}" let (env, log) ← process text (← getEnv) .empty "" _ ← modifyEnv (fun _ => env) @@ -130,90 +129,49 @@ private def addDeclToUnfoldOrTheorem (thms : Meta.SimpTheorems) (e : Expr) : Met else thms.add (.fvar e.fvarId!) #[] e -open Reconstruction.Certifying in -def rconsProof (name : Name) (hints : List Expr) : TacticM Unit := do - let mvar' ← Smt.Util.rewriteIffMeta (← Tactic.getMainGoal) - replaceMainGoal [mvar'] - let mut gs ← (← Tactic.getMainGoal).apply (mkApp (mkConst ``notNotElim) (← Tactic.getMainTarget)) - Tactic.replaceMainGoal gs - let th ← Meta.mkConstWithFreshMVarLevels name - trace[smt.debug.reconstruct] "theorem {name} : {← Meta.inferType th}" - gs ← (← Tactic.getMainGoal).apply th - Tactic.replaceMainGoal gs - for h in hints do - evalAnyGoals do - let gs ← (← Tactic.getMainGoal).apply h - Tactic.replaceMainGoal gs - let mut some thms ← (← Meta.getSimpExtension? `smt_simp).mapM (·.getTheorems) - | throwError "smt tactic failed, 'smt_simp' simpset is not available" - -- TODO: replace with our abbreviation of `Implies` - thms ← thms.addDeclToUnfold ``Implies - for h in hints do - thms ← addDeclToUnfoldOrTheorem thms h - evalAnyGoals do - let (result?, _) ← Meta.simpGoal (← Tactic.getMainGoal) { - config := { { : Lean.Meta.Simp.Config } with failIfUnchanged := false } - simpTheorems := #[thms], - congrTheorems := (← Meta.getSimpCongrTheorems) - } - match result? with - | none => replaceMainGoal [] - | some (_, mvarId) => replaceMainGoal [mvarId] - @[tactic smt] def evalSmt : Tactic := fun stx => withMainContext do - let goalType ← Tactic.getMainTarget + let mv ← Util.rewriteIffMeta (← Tactic.getMainGoal) + Tactic.replaceMainGoal [mv] + let goalType : Q(Prop) ← mv.getType -- 1. Get the hints passed to the tactic. let mut hs ← parseHints ⟨stx[1]⟩ hs := hs.eraseDups withProcessedHints hs fun hs => do -- 2. Generate the SMT query. let cmds ← prepareSmtQuery hs - let query := setOption "produce-models" "true" - *> emitCommands cmds.reverse - *> checkSat - logInfo m!"goal: {goalType}" - logInfo m!"\nquery:\n{Command.cmdsAsQuery (.checkSat :: cmds)}" + let cmds := .setLogic "ALL" :: cmds + trace[smt.debug] m!"goal: {goalType}" + trace[smt.debug] m!"\nquery:\n{Command.cmdsAsQuery (cmds ++ [.checkSat])}" -- 3. Run the solver. - let kind := smt.solver.kind.get (← getOptions) - let path := smt.solver.path.get? (← getOptions) let timeout ← parseTimeout ⟨stx[2]⟩ - let ss ← createFromKind kind path timeout - let (res, ss) ← (StateT.run query ss : MetaM _) + let res ← prove (Command.cmdsAsQuery cmds) timeout -- 4. Print the result. - logInfo m!"\nresult: {res}" - if res = .sat then - -- 4a. Print model. - let (model, _) ← StateT.run getModel ss - logInfo m!"\ncounter-model:\n{model}\n" + -- logInfo m!"\nresult: {res.toString}" + match res with + | .error e => + -- 4a. Print error reason. + trace[smt.debug] m!"\nerror reason:\n{repr e}\n" throwError "unable to prove goal, either it is false or you need to define more symbols with `smt [foo, bar]`" - if res = .unknown then - throwError "unable to prove goal" - try - -- 4b. Reconstruct proof. - let (.expr [.atom "proof", .atom nnp], _) ← StateT.run getProof ss - | throwError "encountered error parsing cvc5 proof" - let nnp := skipImports (unquote nnp) - trace[smt.debug.reconstruct] "proof:\n{nnp}" - let name ← elabProof nnp - rconsProof name hs - catch e => - logInfo m!"failed to reconstruct proof: {e.toMessageData}" -where - unquote s := s.extract ⟨1⟩ (s.endPos - ⟨1⟩) - skipImports (s : String) := Id.run do - let mut s := s - while s.startsWith "import" do - s := s.dropWhile (· != '\n') - s := s.drop 1 - return s + | .ok pf => + let (fv, mv, mvs) ← rconsProof (← Tactic.getMainGoal) pf + mv.withContext do + let ts ← hs.mapM (fun h => Meta.inferType h) + let mut gs ← mv.apply (← Meta.mkAppOptM ``Prop.implies_of_not_and #[listExpr ts q(Prop), goalType]) + Tactic.replaceMainGoal (gs ++ mvs) + let hs := (.fvar fv) :: hs + for h in hs do + evalAnyGoals do + let gs ← (← Tactic.getMainGoal).apply h + Tactic.replaceMainGoal gs @[tactic smtShow] def evalSmtShow : Tactic := fun stx => withMainContext do - let goalType ← Tactic.getMainTarget + let mv ← Util.rewriteIffMeta (← Tactic.getMainGoal) + let goalType ← mv.getType let mut hs ← parseHints ⟨stx[1]⟩ hs := hs.eraseDups withProcessedHints hs fun hs => do let cmds ← prepareSmtQuery hs - let cmds := .checkSat :: cmds + let cmds := cmds ++ [.checkSat] logInfo m!"goal: {goalType}\n\nquery:\n{Command.cmdsAsQuery cmds}" end Smt diff --git a/Smt/Translate/BitVec.lean b/Smt/Translate/BitVec.lean index 42a0e8fc..4ccd4873 100644 --- a/Smt/Translate/BitVec.lean +++ b/Smt/Translate/BitVec.lean @@ -85,12 +85,18 @@ def mkLit (w : Nat) (n : Nat) : Term := | e@(app (app (const ``BitVec.replicate _) _) i) => do let i ← reduceLit i e return mkApp2 (symbolT "_") (symbolT "repeat") (literalT (toString i)) - | e@(app (app (const ``BitVec.zeroExtend _) _) i) => do - let i ← reduceLit i e - return mkApp2 (symbolT "_") (symbolT "zero_extend") (literalT (toString i)) - | e@(app (app (const ``BitVec.signExtend _) _) i) => do - let i ← reduceLit i e - return mkApp2 (symbolT "_") (symbolT "sign_extend") (literalT (toString i)) + | e@(app (app (const ``BitVec.zeroExtend _) w) v) => do + let w ← reduceWidth w e + let v ← reduceLit v e + if v ≤ w then + throwError "{v} is not greater than bitvector width {w} in{indentD e}" + return mkApp2 (symbolT "_") (symbolT "zero_extend") (literalT (toString (v - w))) + | e@(app (app (const ``BitVec.signExtend _) w) v) => do + let w ← reduceWidth w e + let v ← reduceLit v e + if v ≤ w then + throwError "{v} is not greater than bitvector width {w} in{indentD e}" + return mkApp2 (symbolT "_") (symbolT "sign_extend") (literalT (toString (v - w))) | _ => return none where reduceWidth (w : Expr) (e : Expr) : TranslationM Nat := do diff --git a/Test/BitVec/Shift.expected b/Test/BitVec/Shift.expected index 3cf18699..b3aa8954 100644 --- a/Test/BitVec/Shift.expected +++ b/Test/BitVec/Shift.expected @@ -1,34 +1,16 @@ -goal: x ++ y = BitVec.zeroExtend 2 x <<< 2 ||| BitVec.zeroExtend 2 y +goal: x ++ y = BitVec.zeroExtend 4 x <<< 2 ||| BitVec.zeroExtend 4 y query: (declare-const x (_ BitVec 2)) (declare-const y (_ BitVec 2)) (assert (not (= (concat x y) (bvor (bvshl ((_ zero_extend 2) x) #b0010) ((_ zero_extend 2) y))))) (check-sat) - -result: unsat -failed to reconstruct proof: could not parse solver output: incomplete input: expected a token, got none -solver stdout: - -solver stderr: -Fatal failure within cvc5::internal::Node cvc5::internal::proof::LeanNodeConverter::convert(cvc5::internal::Node) at /home/hbarbosa/cvc/wt-leanPrinter/src/proof/lean/lean_node_converter.cpp:549 -Unreachable code reached Kind concat is not supported - -Test/BitVec/Shift.lean:4:8: warning: declaration uses 'sorry' -goal: x ++ y = BitVec.zeroExtend 3 x <<< 3 ||| BitVec.zeroExtend 3 y +Test/BitVec/Shift.lean:5:8: warning: declaration uses 'sorry' +goal: x ++ y = BitVec.zeroExtend 6 x <<< 3 ||| BitVec.zeroExtend 6 y query: -(declare-const y (_ BitVec 3)) (declare-const x (_ BitVec 3)) +(declare-const y (_ BitVec 3)) (assert (not (= (concat x y) (bvor (bvshl ((_ zero_extend 3) x) #b000011) ((_ zero_extend 3) y))))) (check-sat) - -result: unsat -failed to reconstruct proof: could not parse solver output: incomplete input: expected a token, got none -solver stdout: - -solver stderr: -Fatal failure within cvc5::internal::Node cvc5::internal::proof::LeanNodeConverter::convert(cvc5::internal::Node) at /home/hbarbosa/cvc/wt-leanPrinter/src/proof/lean/lean_node_converter.cpp:549 -Unreachable code reached Kind concat is not supported - -Test/BitVec/Shift.lean:9:8: warning: declaration uses 'sorry' +Test/BitVec/Shift.lean:10:8: warning: declaration uses 'sorry' diff --git a/Test/BitVec/Shift.lean b/Test/BitVec/Shift.lean index d0a20cb5..dcef9b51 100644 --- a/Test/BitVec/Shift.lean +++ b/Test/BitVec/Shift.lean @@ -1,12 +1,13 @@ import Smt -import Smt.Data.BitVec + +open Std theorem append_eq_shl_or_2 (x y : BitVec 2) - : x ++ y = (x.zeroExtend 2 <<< 2) ||| y.zeroExtend 2 := by - smt + : x ++ y = (x.zeroExtend 4 <<< 2) ||| y.zeroExtend 4 := by + smt_show sorry theorem append_eq_shl_or_3 (x y : BitVec 3) - : x ++ y = (x.zeroExtend 3 <<< 3) ||| y.zeroExtend 3 := by - smt + : x ++ y = (x.zeroExtend 6 <<< 3) ||| y.zeroExtend 6 := by + smt_show sorry diff --git a/Test/BitVec/XorComm.expected b/Test/BitVec/XorComm.expected index b3d69020..6a0334eb 100644 --- a/Test/BitVec/XorComm.expected +++ b/Test/BitVec/XorComm.expected @@ -1,22 +1,16 @@ goal: x ^^^ y = y ^^^ x query: -(declare-const x (_ BitVec 2)) (declare-const y (_ BitVec 2)) +(declare-const x (_ BitVec 2)) (assert (not (= (bvxor x y) (bvxor y x)))) (check-sat) - -result: unsat -failed to reconstruct proof: encountered errors elaborating cvc5 proof -Test/BitVec/XorComm.lean:4:8: warning: declaration uses 'sorry' +Test/BitVec/XorComm.lean:5:8: warning: declaration uses 'sorry' goal: x ^^^ y = y ^^^ x query: -(declare-const y (_ BitVec 8)) (declare-const x (_ BitVec 8)) +(declare-const y (_ BitVec 8)) (assert (not (= (bvxor x y) (bvxor y x)))) (check-sat) - -result: unsat -failed to reconstruct proof: encountered errors elaborating cvc5 proof -Test/BitVec/XorComm.lean:8:8: warning: declaration uses 'sorry' +Test/BitVec/XorComm.lean:9:8: warning: declaration uses 'sorry' diff --git a/Test/BitVec/XorComm.lean b/Test/BitVec/XorComm.lean index 19436aaa..b6ca3cc0 100644 --- a/Test/BitVec/XorComm.lean +++ b/Test/BitVec/XorComm.lean @@ -1,10 +1,11 @@ import Smt -import Smt.Data.BitVec + +open Std theorem xor_comm_2 (x y : BitVec 2) : x ^^^ y = y ^^^ x := by - smt + smt_show sorry theorem xor_comm_4p4 (x y : BitVec (4+4)) : x ^^^ y = y ^^^ x := by - smt + smt_show sorry diff --git a/Test/Bool/Addition.expected b/Test/Bool/Addition.expected index 3fdcaabb..ce1ccff1 100644 --- a/Test/Bool/Addition.expected +++ b/Test/Bool/Addition.expected @@ -5,11 +5,3 @@ query: (declare-const p Bool) (assert (not (=> (= p true) (= (or p q) true)))) (check-sat) - -result: unsat -failed to reconstruct proof: tactic 'apply' failed, failed to unify - ¬Implies (?p = True) ((?p ∨ ?q) = True) → False -with - ¬¬(p = true → (p || q) = true) -p q : Bool -⊢ ¬¬(p = true → (p || q) = true) diff --git a/Test/Bool/Addition.lean b/Test/Bool/Addition.lean index 7200396d..dca371af 100644 --- a/Test/Bool/Addition.lean +++ b/Test/Bool/Addition.lean @@ -1,5 +1,5 @@ import Smt theorem addition (p q : Bool) : p → p || q := by - smt + smt_show simp_all diff --git a/Test/Bool/Assoc.expected b/Test/Bool/Assoc.expected index dc9b331a..c4f6c58a 100644 --- a/Test/Bool/Assoc.expected +++ b/Test/Bool/Assoc.expected @@ -1,20 +1,10 @@ goal: (f p (f q r) == f (f p q) r) = true query: +(declare-fun f (Bool Bool) Bool) (declare-const p Bool) -(declare-const q Bool) (declare-const r Bool) -(declare-fun f (Bool Bool) Bool) +(declare-const q Bool) (assert (not (= (= (f p (f q r)) (f (f p q) r)) true))) (check-sat) - -result: sat - -counter-model: -( -(define-fun p () Bool true) -(define-fun q () Bool false) -(define-fun r () Bool false) -(define-fun f ((_arg_1 Bool) (_arg_2 Bool)) Bool (ite _arg_1 (not _arg_2) (and (not _arg_1) (not _arg_2)))) -) -Test/Bool/Assoc.lean:5:2: error: unable to prove goal, either it is false or you need to define more symbols with `smt [foo, bar]` +Test/Bool/Assoc.lean:3:8: warning: declaration uses 'sorry' diff --git a/Test/Bool/Assoc.lean b/Test/Bool/Assoc.lean index 8a34ad1b..f17345e1 100644 --- a/Test/Bool/Assoc.lean +++ b/Test/Bool/Assoc.lean @@ -2,5 +2,5 @@ import Smt theorem assoc (f : Bool → Bool → Bool) (p q r : Bool) : f p (f q r) == f (f p q) r := by - smt + smt_show admit diff --git a/Test/Bool/Comm.expected b/Test/Bool/Comm.expected index b5bea551..89cfc8c8 100644 --- a/Test/Bool/Comm.expected +++ b/Test/Bool/Comm.expected @@ -1,18 +1,9 @@ goal: (f p q == f q p) = true query: +(declare-const q Bool) (declare-fun f (Bool Bool) Bool) (declare-const p Bool) -(declare-const q Bool) (assert (not (= (= (f p q) (f q p)) true))) (check-sat) - -result: sat - -counter-model: -( -(define-fun f ((_arg_1 Bool) (_arg_2 Bool)) Bool (and _arg_1 (not _arg_2))) -(define-fun p () Bool false) -(define-fun q () Bool true) -) -Test/Bool/Comm.lean:4:2: error: unable to prove goal, either it is false or you need to define more symbols with `smt [foo, bar]` +Test/Bool/Comm.lean:3:0: warning: declaration uses 'sorry' diff --git a/Test/Bool/Comm.lean b/Test/Bool/Comm.lean index 33aa3d85..cdd02ae4 100644 --- a/Test/Bool/Comm.lean +++ b/Test/Bool/Comm.lean @@ -1,5 +1,5 @@ import Smt example (f : Bool → Bool → Bool) (p q : Bool) : f p q == f q p := by - smt + smt_show admit diff --git a/Test/Bool/Cong.expected b/Test/Bool/Cong.expected index e7e14d9a..f97fc612 100644 --- a/Test/Bool/Cong.expected +++ b/Test/Bool/Cong.expected @@ -6,12 +6,3 @@ query: (declare-const q Bool) (assert (not (=> (= (= p q) true) (= (= (f p) (f q)) true)))) (check-sat) - -result: unsat -failed to reconstruct proof: tactic 'apply' failed, failed to unify - ¬Implies ((?p = ?q) = True) ((?f ?p = ?f ?q) = True) → False -with - ¬¬((p == q) = true → (f p == f q) = true) -p q : Bool -f : Bool → Bool -⊢ ¬¬((p == q) = true → (f p == f q) = true) diff --git a/Test/Bool/Cong.lean b/Test/Bool/Cong.lean index 0dde58e3..3f757fe4 100644 --- a/Test/Bool/Cong.lean +++ b/Test/Bool/Cong.lean @@ -1,5 +1,5 @@ import Smt theorem cong (p q : Bool) (f : Bool → Bool) : p == q → f p == f q := by - smt + smt_show cases p <;> cases q <;> cases f true <;> cases f false <;> simp_all diff --git a/Test/Bool/Conjunction.expected b/Test/Bool/Conjunction.expected index 900afca7..319cf0e0 100644 --- a/Test/Bool/Conjunction.expected +++ b/Test/Bool/Conjunction.expected @@ -5,11 +5,3 @@ query: (declare-const q Bool) (assert (not (=> (= p true) (=> (= q true) (= (and p q) true))))) (check-sat) - -result: unsat -failed to reconstruct proof: tactic 'apply' failed, failed to unify - ¬Implies (?p = True) (Implies (?q = True) ((?p ∧ ?q) = True)) → False -with - ¬¬(p = true → q = true → (p && q) = true) -p q : Bool -⊢ ¬¬(p = true → q = true → (p && q) = true) diff --git a/Test/Bool/Conjunction.lean b/Test/Bool/Conjunction.lean index c18a7797..0a018dc3 100644 --- a/Test/Bool/Conjunction.lean +++ b/Test/Bool/Conjunction.lean @@ -1,5 +1,5 @@ import Smt theorem conjunction (p q : Bool) : p → q → p && q := by - smt + smt_show simp_all diff --git a/Test/Bool/DisjunctiveSyllogism.expected b/Test/Bool/DisjunctiveSyllogism.expected index 0cf9b998..7044302b 100644 --- a/Test/Bool/DisjunctiveSyllogism.expected +++ b/Test/Bool/DisjunctiveSyllogism.expected @@ -5,11 +5,3 @@ query: (declare-const q Bool) (assert (not (=> (= (or p q) true) (=> (= (not p) true) (= q true))))) (check-sat) - -result: unsat -failed to reconstruct proof: tactic 'apply' failed, failed to unify - ¬Implies ((?p ∨ ?q) = True) (Implies ((¬?p) = True) (?q = True)) → False -with - ¬¬((p || q) = true → (!p) = true → q = true) -p q : Bool -⊢ ¬¬((p || q) = true → (!p) = true → q = true) diff --git a/Test/Bool/DisjunctiveSyllogism.lean b/Test/Bool/DisjunctiveSyllogism.lean index fd84bd00..9070b715 100644 --- a/Test/Bool/DisjunctiveSyllogism.lean +++ b/Test/Bool/DisjunctiveSyllogism.lean @@ -1,6 +1,6 @@ import Smt theorem disjunctive_syllogism (p q : Bool) : p || q → !p → q := by - smt + smt_show intro hpq hnp cases p <;> simp_all diff --git a/Test/Bool/Exists'.expected b/Test/Bool/Exists'.expected index 17918ff7..4d2adca3 100644 --- a/Test/Bool/Exists'.expected +++ b/Test/Bool/Exists'.expected @@ -3,10 +3,3 @@ goal: ∃ p, p = true query: (assert (not (exists ((p Bool)) (= p true)))) (check-sat) - -result: unsat -failed to reconstruct proof: tactic 'apply' failed, failed to unify - (¬∃ p, p = True) → False -with - ¬¬∃ p, p = true -⊢ ¬¬∃ p, p = true diff --git a/Test/Bool/Exists'.lean b/Test/Bool/Exists'.lean index db11979a..6252497b 100644 --- a/Test/Bool/Exists'.lean +++ b/Test/Bool/Exists'.lean @@ -1,5 +1,5 @@ import Smt theorem exists' : ∃ p : Bool, p := by - smt + smt_show exact Exists.intro true rfl diff --git a/Test/Bool/Falsum.expected b/Test/Bool/Falsum.expected index da920083..9fb456d6 100644 --- a/Test/Bool/Falsum.expected +++ b/Test/Bool/Falsum.expected @@ -3,10 +3,3 @@ goal: (!false) = true query: (assert (not (= (not false) true))) (check-sat) - -result: unsat -failed to reconstruct proof: tactic 'apply' failed, failed to unify - ¬(¬False) = True → False -with - ¬¬(!false) = true -⊢ ¬¬(!false) = true diff --git a/Test/Bool/Falsum.lean b/Test/Bool/Falsum.lean index 5664f6e1..ecc0402e 100644 --- a/Test/Bool/Falsum.lean +++ b/Test/Bool/Falsum.lean @@ -1,5 +1,5 @@ import Smt theorem falsum : !false := by - smt + smt_show simp_all diff --git a/Test/Bool/HypotheticalSyllogism.expected b/Test/Bool/HypotheticalSyllogism.expected index 2aa9da8b..01b899e6 100644 --- a/Test/Bool/HypotheticalSyllogism.expected +++ b/Test/Bool/HypotheticalSyllogism.expected @@ -6,6 +6,3 @@ query: (declare-const q Bool) (assert (not (=> (=> (= p true) (= q true)) (=> (=> (= q true) (= r true)) (=> (= p true) (= r true)))))) (check-sat) - -result: unsat -failed to reconstruct proof: encountered errors elaborating cvc5 proof diff --git a/Test/Bool/HypotheticalSyllogism.lean b/Test/Bool/HypotheticalSyllogism.lean index adad4b20..0c6355c5 100644 --- a/Test/Bool/HypotheticalSyllogism.lean +++ b/Test/Bool/HypotheticalSyllogism.lean @@ -1,5 +1,5 @@ import Smt theorem hypothetical_syllogism (p q r : Bool) : (p → q) → (q → r) → p → r := by - smt + smt_show simp_all diff --git a/Test/Bool/ModusPonens'.expected b/Test/Bool/ModusPonens'.expected index 76306d24..5fd7c28b 100644 --- a/Test/Bool/ModusPonens'.expected +++ b/Test/Bool/ModusPonens'.expected @@ -7,13 +7,3 @@ query: (assert (= p true)) (assert (not (= q true))) (check-sat) - -result: unsat -failed to reconstruct proof: tactic 'apply' failed, failed to unify - ¬?q = True → False -with - ¬¬q = true -p q : Bool -hp : p = true -hpq : p = true → q = true -⊢ ¬¬q = true diff --git a/Test/Bool/ModusPonens'.lean b/Test/Bool/ModusPonens'.lean index 0e836b74..78f50869 100644 --- a/Test/Bool/ModusPonens'.lean +++ b/Test/Bool/ModusPonens'.lean @@ -1,5 +1,5 @@ import Smt theorem modus_ponens' (p q : Bool) (hp : p) (hpq : p → q) : q := by - smt [hp, hpq] + smt_show [hp, hpq] simp_all diff --git a/Test/Bool/ModusPonens.expected b/Test/Bool/ModusPonens.expected index 93056d69..5a811051 100644 --- a/Test/Bool/ModusPonens.expected +++ b/Test/Bool/ModusPonens.expected @@ -5,11 +5,3 @@ query: (declare-const q Bool) (assert (not (=> (= p true) (=> (=> (= p true) (= q true)) (= q true))))) (check-sat) - -result: unsat -failed to reconstruct proof: tactic 'apply' failed, failed to unify - ¬Implies (?p = True) (Implies (Implies (?p = True) (?q = True)) (?q = True)) → False -with - ¬¬(p = true → (p = true → q = true) → q = true) -p q : Bool -⊢ ¬¬(p = true → (p = true → q = true) → q = true) diff --git a/Test/Bool/ModusPonens.lean b/Test/Bool/ModusPonens.lean index f6f0bb48..e782646b 100644 --- a/Test/Bool/ModusPonens.lean +++ b/Test/Bool/ModusPonens.lean @@ -1,5 +1,5 @@ import Smt theorem modus_ponens (p q : Bool) : p → (p → q) → q := by - smt + smt_show simp_all diff --git a/Test/Bool/ModusTollens.expected b/Test/Bool/ModusTollens.expected index 941fe3ff..4949c3f9 100644 --- a/Test/Bool/ModusTollens.expected +++ b/Test/Bool/ModusTollens.expected @@ -5,11 +5,3 @@ query: (declare-const q Bool) (assert (not (=> (= (not q) true) (=> (=> (= p true) (= q true)) (= (not p) true))))) (check-sat) - -result: unsat -failed to reconstruct proof: tactic 'apply' failed, failed to unify - ¬Implies ((¬?q) = True) (Implies (Implies (?p = True) (?q = True)) ((¬?p) = True)) → False -with - ¬¬((!q) = true → (p = true → q = true) → (!p) = true) -p q : Bool -⊢ ¬¬((!q) = true → (p = true → q = true) → (!p) = true) diff --git a/Test/Bool/ModusTollens.lean b/Test/Bool/ModusTollens.lean index 641a20c7..2ecfd7cf 100644 --- a/Test/Bool/ModusTollens.lean +++ b/Test/Bool/ModusTollens.lean @@ -1,6 +1,6 @@ import Smt theorem modus_tollens (p q : Bool) : !q → (p → q) → !p := by - smt + smt_show intro hnq hpq cases p <;> simp_all diff --git a/Test/Bool/PropExt.expected b/Test/Bool/PropExt.expected index fa341362..58929b81 100644 --- a/Test/Bool/PropExt.expected +++ b/Test/Bool/PropExt.expected @@ -1,15 +1 @@ -goal: (p = true ↔ q = true) → (p == q) = true - -query: -(declare-const p Bool) -(declare-const q Bool) -(assert (not (=> (= (= p true) (= q true)) (= (= p q) true)))) -(check-sat) - -result: unsat -failed to reconstruct proof: tactic 'apply' failed, failed to unify - ¬Implies ((?p = True) = (?q = True)) ((?p = ?q) = True) → False -with - ¬¬((p = true) = (q = true) → (p == q) = true) -p q : Bool -⊢ ¬¬((p = true) = (q = true) → (p == q) = true) +Test/Bool/PropExt.lean:4:2: error: no goals to be solved diff --git a/Test/Bool/PropExt.lean b/Test/Bool/PropExt.lean index 4e62c0e3..8ffdfffc 100644 --- a/Test/Bool/PropExt.lean +++ b/Test/Bool/PropExt.lean @@ -1,6 +1,6 @@ import Smt theorem prop_ext (p q : Bool) : (p ↔ q) → p == q := by - smt + smt_show intro ⟨hpq, hqp⟩ cases p <;> cases q <;> simp_all diff --git a/Test/Bool/Refl.expected b/Test/Bool/Refl.expected index 6f79dbd0..2d02ce49 100644 --- a/Test/Bool/Refl.expected +++ b/Test/Bool/Refl.expected @@ -4,11 +4,3 @@ query: (declare-const p Bool) (assert (not (= (= p p) true))) (check-sat) - -result: unsat -failed to reconstruct proof: tactic 'apply' failed, failed to unify - ¬(?p = ?p) = True → False -with - ¬¬(p == p) = true -p : Bool -⊢ ¬¬(p == p) = true diff --git a/Test/Bool/Refl.lean b/Test/Bool/Refl.lean index 18bd2ef2..e8ad1070 100644 --- a/Test/Bool/Refl.lean +++ b/Test/Bool/Refl.lean @@ -1,5 +1,5 @@ import Smt example (p : Bool) : p == p := by - smt + smt_show cases p <;> simp_all diff --git a/Test/Bool/Resolution.expected b/Test/Bool/Resolution.expected index 06bd3918..9efcedae 100644 --- a/Test/Bool/Resolution.expected +++ b/Test/Bool/Resolution.expected @@ -6,11 +6,3 @@ query: (declare-const r Bool) (assert (not (=> (= (or p q) true) (=> (= (or (not p) r) true) (= (or q r) true))))) (check-sat) - -result: unsat -failed to reconstruct proof: tactic 'apply' failed, failed to unify - ¬Implies ((?p ∨ ?q) = True) (Implies ((¬?p ∨ ?r) = True) ((?q ∨ ?r) = True)) → False -with - ¬¬((p || q) = true → (!p || r) = true → (q || r) = true) -p q r : Bool -⊢ ¬¬((p || q) = true → (!p || r) = true → (q || r) = true) diff --git a/Test/Bool/Resolution.lean b/Test/Bool/Resolution.lean index 8a7d0110..2b34a59b 100644 --- a/Test/Bool/Resolution.lean +++ b/Test/Bool/Resolution.lean @@ -1,7 +1,7 @@ import Smt theorem resolution (p q r : Bool) : p || q → !p || r → q || r := by - smt + smt_show intro hpq intro hnpr cases p <;> cases r <;> simp_all diff --git a/Test/Bool/Simplification.expected b/Test/Bool/Simplification.expected index 6e8922d6..7f598051 100644 --- a/Test/Bool/Simplification.expected +++ b/Test/Bool/Simplification.expected @@ -5,11 +5,3 @@ query: (declare-const p Bool) (assert (not (=> (= (and p q) true) (= p true)))) (check-sat) - -result: unsat -failed to reconstruct proof: tactic 'apply' failed, failed to unify - ¬Implies ((?p ∧ ?q) = True) (?p = True) → False -with - ¬¬((p && q) = true → p = true) -p q : Bool -⊢ ¬¬((p && q) = true → p = true) diff --git a/Test/Bool/Simplification.lean b/Test/Bool/Simplification.lean index bf6551ac..d0bedb1a 100644 --- a/Test/Bool/Simplification.lean +++ b/Test/Bool/Simplification.lean @@ -1,5 +1,5 @@ import Smt theorem simplification (p q : Bool) : p && q → p := by - smt + smt_show cases p <;> simp_all diff --git a/Test/Bool/Symm.expected b/Test/Bool/Symm.expected index 2c242af9..63cedce5 100644 --- a/Test/Bool/Symm.expected +++ b/Test/Bool/Symm.expected @@ -1,15 +1,7 @@ goal: (p == q) = true → (q == p) = true query: -(declare-const q Bool) (declare-const p Bool) +(declare-const q Bool) (assert (not (=> (= (= p q) true) (= (= q p) true)))) (check-sat) - -result: unsat -failed to reconstruct proof: tactic 'apply' failed, failed to unify - ¬Implies ((?p = ?q) = True) ((?q = ?p) = True) → False -with - ¬¬((p == q) = true → (q == p) = true) -p q : Bool -⊢ ¬¬((p == q) = true → (q == p) = true) diff --git a/Test/Bool/Symm.lean b/Test/Bool/Symm.lean index 05b12845..6837b1a4 100644 --- a/Test/Bool/Symm.lean +++ b/Test/Bool/Symm.lean @@ -1,5 +1,5 @@ import Smt example (p q : Bool) : p == q → q == p := by - smt + smt_show cases p <;> cases q <;> simp_all diff --git a/Test/Bool/Trans.expected b/Test/Bool/Trans.expected index e2469d4e..e329b3cb 100644 --- a/Test/Bool/Trans.expected +++ b/Test/Bool/Trans.expected @@ -1,16 +1,8 @@ goal: (p == q) = true → (q == r) = true → (p == r) = true query: -(declare-const p Bool) (declare-const r Bool) +(declare-const p Bool) (declare-const q Bool) (assert (not (=> (= (= p q) true) (=> (= (= q r) true) (= (= p r) true))))) (check-sat) - -result: unsat -failed to reconstruct proof: tactic 'apply' failed, failed to unify - ¬Implies ((?p = ?q) = True) (Implies ((?q = ?r) = True) ((?p = ?r) = True)) → False -with - ¬¬((p == q) = true → (q == r) = true → (p == r) = true) -p q r : Bool -⊢ ¬¬((p == q) = true → (q == r) = true → (p == r) = true) diff --git a/Test/Bool/Trans.lean b/Test/Bool/Trans.lean index 92f40ba3..96b4c07e 100644 --- a/Test/Bool/Trans.lean +++ b/Test/Bool/Trans.lean @@ -1,5 +1,5 @@ import Smt example (p q r : Bool) : p == q → q == r → p == r := by - smt + smt_show cases p <;> cases q <;> cases r <;> simp_all diff --git a/Test/Bool/Triv''.expected b/Test/Bool/Triv''.expected index 74b63e7b..67c7c9b3 100644 --- a/Test/Bool/Triv''.expected +++ b/Test/Bool/Triv''.expected @@ -4,11 +4,3 @@ query: (declare-const p Bool) (assert (not (=> (= (not p) true) (= (not p) true)))) (check-sat) - -result: unsat -failed to reconstruct proof: tactic 'apply' failed, failed to unify - ¬Implies ((¬?p) = True) ((¬?p) = True) → False -with - ¬¬((!p) = true → (!p) = true) -p : Bool -⊢ ¬¬((!p) = true → (!p) = true) diff --git a/Test/Bool/Triv''.lean b/Test/Bool/Triv''.lean index 4ad90fa0..cc7ea96c 100644 --- a/Test/Bool/Triv''.lean +++ b/Test/Bool/Triv''.lean @@ -1,5 +1,5 @@ import Smt theorem triv'' (p : Bool) : !p → !p := by - smt + smt_show simp_all diff --git a/Test/Bool/Triv'.expected b/Test/Bool/Triv'.expected index e47357fd..c44e574a 100644 --- a/Test/Bool/Triv'.expected +++ b/Test/Bool/Triv'.expected @@ -3,10 +3,3 @@ goal: ∀ (p : Bool), p = true → p = true query: (assert (not (forall ((p Bool)) (=> (= p true) (= p true))))) (check-sat) - -result: unsat -failed to reconstruct proof: tactic 'apply' failed, failed to unify - (¬∀ (p : Prop), Implies (p = True) (p = True)) → False -with - ¬¬∀ (p : Bool), p = true → p = true -⊢ ¬¬∀ (p : Bool), p = true → p = true diff --git a/Test/Bool/Triv'.lean b/Test/Bool/Triv'.lean index a6a8a39d..3b2bafea 100644 --- a/Test/Bool/Triv'.lean +++ b/Test/Bool/Triv'.lean @@ -1,6 +1,6 @@ import Smt theorem triv': ∀ p : Bool, ∀ _ : p, p := by - smt + smt_show intro p simp_all diff --git a/Test/Bool/Triv.expected b/Test/Bool/Triv.expected index d1863aa7..29bd2483 100644 --- a/Test/Bool/Triv.expected +++ b/Test/Bool/Triv.expected @@ -4,11 +4,3 @@ query: (declare-const p Bool) (assert (not (=> (= p true) (= p true)))) (check-sat) - -result: unsat -failed to reconstruct proof: tactic 'apply' failed, failed to unify - ¬Implies (?p = True) (?p = True) → False -with - ¬¬(p = true → p = true) -p : Bool -⊢ ¬¬(p = true → p = true) diff --git a/Test/Bool/Triv.lean b/Test/Bool/Triv.lean index e6e0e34b..35691664 100644 --- a/Test/Bool/Triv.lean +++ b/Test/Bool/Triv.lean @@ -1,5 +1,5 @@ import Smt theorem triv (p : Bool) : p → p := by - smt + smt_show simp_all diff --git a/Test/Bool/Verum.expected b/Test/Bool/Verum.expected index a200bb22..3b290a70 100644 --- a/Test/Bool/Verum.expected +++ b/Test/Bool/Verum.expected @@ -3,10 +3,3 @@ goal: true = true query: (assert (not (= true true))) (check-sat) - -result: unsat -failed to reconstruct proof: tactic 'apply' failed, failed to unify - ¬True = True → False -with - ¬¬true = true -⊢ ¬¬true = true diff --git a/Test/Bool/Verum.lean b/Test/Bool/Verum.lean index 4ed5b601..2cc14759 100644 --- a/Test/Bool/Verum.lean +++ b/Test/Bool/Verum.lean @@ -1,5 +1,5 @@ import Smt theorem verum : true := by - smt + smt_show simp_all diff --git a/Test/EUF/Example.expected b/Test/EUF/Example.expected index 14848a4d..e69de29b 100644 --- a/Test/EUF/Example.expected +++ b/Test/EUF/Example.expected @@ -1,16 +0,0 @@ -goal: a = b → c = d → p1 ∧ True → ¬p1 ∨ p2 ∧ p3 → ¬p3 ∨ ¬f a c = f b d → False - -query: -(declare-sort U 0) -(declare-const c U) -(declare-const p3 Bool) -(declare-const a U) -(declare-const d U) -(declare-const p1 Bool) -(declare-const b U) -(declare-const p2 Bool) -(declare-fun f (U U) U) -(assert (not (=> (= a b) (=> (= c d) (=> (and p1 true) (=> (or (not p1) (and p2 p3)) (=> (or (not p3) (not (= (f a c) (f b d)))) false))))))) -(check-sat) - -result: unsat diff --git a/Test/EUF/Example.lean b/Test/EUF/Example.lean index 5ae762af..18cf81d9 100644 --- a/Test/EUF/Example.lean +++ b/Test/EUF/Example.lean @@ -1,6 +1,8 @@ import Smt -theorem euf {U : Type} [Nonempty U] {f : U → U → U} {a b c d : U} : (a = b) → (c = d) → p1 ∧ True → (¬ p1) ∨ (p2 ∧ p3) → (¬ p3) ∨ (¬ (f a c = f b d)) → False := by +example {U : Type} [Nonempty U] {f : U → U → U} {a b c d : U} : (a = b) → (c = d) → p1 ∧ True → (¬ p1) ∨ (p2 ∧ p3) → (¬ p3) ∨ (¬ (f a c = f b d)) → False := by smt - · exact propext ⟨Or.inl, (Or.elim · id False.elim)⟩ - · exact (and_true p1).symm + +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] diff --git a/Test/Examples/Demo.expected b/Test/Examples/Demo.expected index 29b824e5..38739db8 100644 --- a/Test/Examples/Demo.expected +++ b/Test/Examples/Demo.expected @@ -1,55 +1,27 @@ -Test/Examples/Demo.lean:3:4: warning: declaration uses 'sorry' -Test/Examples/Demo.lean:3:4: warning: declaration uses 'sorry' -Test/Examples/Demo.lean:16:14: warning: declaration uses 'sorry' -Test/Examples/Demo.lean:16:14: warning: declaration uses 'sorry' -goal: sum (Int.ofNat Nat.zero) = Int.ofNat Nat.zero * (Int.ofNat Nat.zero + 1) / 2 - -query: -(define-fun-rec sum ((n Int)) Int (ite (< n 0) 0 (+ n (sum (- n 1))))) -(assert (not (= (sum 0) (div (* 0 (+ 0 1)) 2)))) -(check-sat) - -result: unsat -failed to reconstruct proof: encountered errors elaborating cvc5 proof -Test/Examples/Demo.lean:17:19: error: incorrect number of universe levels GE.ge goal: ∀ (a : G), op a (inv a) = e query: (declare-sort G 0) -(declare-const e G) (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:25:8: warning: declaration uses 'sorry' +Test/Examples/Demo.lean:9:8: warning: declaration uses 'sorry' goal: ∀ (a : G), op a e = a query: (declare-sort G 0) -(declare-fun inv (G) G) (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:30:8: warning: declaration uses 'sorry' -goal: (∀ (z : G), op e' z = z) → e' = 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)))))) -(declare-const |e'| G) -(assert (not (=> (forall ((z G)) (= (op |e'| z) z)) (= |e'| e)))) -(check-sat) -Test/Examples/Demo.lean:34:8: warning: declaration uses 'sorry' +Test/Examples/Demo.lean:14:8: warning: declaration uses 'sorry' diff --git a/Test/Examples/Demo.lean b/Test/Examples/Demo.lean index 2f66b33f..42d63db9 100644 --- a/Test/Examples/Demo.lean +++ b/Test/Examples/Demo.lean @@ -1,21 +1,5 @@ import Smt -def sum (n : Int) : Int := - if h : n < 0 then - 0 - else - have : sizeOf (n - 1) < sizeOf n := sorry - n + sum (n - 1) -termination_by _ => n - -theorem sum_formula : n ≥ 0 → sum n = n * (n + 1) / 2 := by - intro h - induction n with - | negSucc _ => contradiction - | ofNat n => induction n with - | zero => smt [sum]; sorry - | succ n ih => smt [sum, ih]; sorry - variable {G : Type} [Nonempty G] (op : G → G → G) (inv : G → G) (e : G) axiom assoc : ∀ a b c, op a (op b c) = op (op a b) c @@ -32,5 +16,5 @@ theorem identity' : ∀ a, op a e = a := by sorry theorem unique_identity e' : (∀ z, op e' z = z) → e' = e := by - 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 diff --git a/Test/Int/Arith.expected b/Test/Int/Arith.expected index aab0c91e..d9a2cee1 100644 --- a/Test/Int/Arith.expected +++ b/Test/Int/Arith.expected @@ -6,47 +6,26 @@ query: (declare-const n Int) (assert (not (< (mod n m) m))) (check-sat) - -result: unsat -failed to reconstruct proof: could not parse solver output: incomplete input: expected a token, got none -solver stdout: - -solver stderr: -Fatal failure within cvc5::internal::Node cvc5::internal::proof::LeanNodeConverter::convert(cvc5::internal::Node) at /home/hbarbosa/cvc/wt-leanPrinter/src/proof/lean/lean_node_converter.cpp:549 -Unreachable code reached Kind * is not supported - Test/Int/Arith.lean:3:0: warning: declaration uses 'sorry' goal: (n - m) * k + l = n * k - m * k + l query: -(declare-const k Int) +(declare-const l Int) (declare-const n Int) (declare-const m Int) -(declare-const l Int) +(declare-const k Int) (assert (not (= (+ (* (- n m) k) l) (+ (- (* n k) (* m k)) l)))) (check-sat) - -result: unsat -failed to reconstruct proof: could not parse solver output: incomplete input: expected a token, got none -solver stdout: - -solver stderr: -Fatal failure within cvc5::internal::Node cvc5::internal::proof::LeanNodeConverter::convert(cvc5::internal::Node) at /home/hbarbosa/cvc/wt-leanPrinter/src/proof/lean/lean_node_converter.cpp:549 -Unreachable code reached Kind * is not supported - Test/Int/Arith.lean:7:0: warning: declaration uses 'sorry' goal: n + k ≤ m + l query: -(declare-const l Int) (declare-const k Int) +(declare-const l Int) (assert (<= k l)) (declare-const n Int) (declare-const m Int) (assert (<= n m)) (assert (not (<= (+ n k) (+ m l)))) (check-sat) - -result: unsat -failed to reconstruct proof: encountered errors elaborating cvc5 proof Test/Int/Arith.lean:11:0: warning: declaration uses 'sorry' diff --git a/Test/Int/Arith.lean b/Test/Int/Arith.lean index 32109cb7..670627e6 100644 --- a/Test/Int/Arith.lean +++ b/Test/Int/Arith.lean @@ -1,13 +1,13 @@ import Smt example (n m : Int) (h : 0 < m) : n % m < m := by - smt [h] + smt_show [h] sorry example (n m k l : Int) : (n - m) * k + l = n*k - m*k + l := by - smt + smt_show sorry example (n m k l : Int) (hN : n ≤ m) (hK : k ≤ l) : n + k ≤ m + l := by - smt [hN, hK] + smt_show [hN, hK] sorry diff --git a/Test/Int/Binders.expected b/Test/Int/Binders.expected index 09ec0ad1..02404191 100644 --- a/Test/Int/Binders.expected +++ b/Test/Int/Binders.expected @@ -6,15 +6,6 @@ query: (declare-const b Int) (assert (not (= (curryAdd a b) (curryAdd b a)))) (check-sat) - -result: unsat -failed to reconstruct proof: could not parse solver output: incomplete input: expected a token, got none -solver stdout: - -solver stderr: -Fatal failure within virtual bool cvc5::internal::proof::LeanProofPostprocessCallback::update(cvc5::internal::Node, cvc5::internal::PfRule, const std::vector >&, const std::vector >&, cvc5::internal::CDProof*, bool&) at /home/hbarbosa/cvc/wt-leanPrinter/src/proof/lean/lean_post_processor.cpp:785 -Unreachable code reached Higher-order congruence not supported yet - Test/Int/Binders.lean:5:0: warning: declaration uses 'sorry' goal: partCurryAdd a b = partCurryAdd b a @@ -24,15 +15,6 @@ query: (declare-const b Int) (assert (not (= (partCurryAdd a b) (partCurryAdd b a)))) (check-sat) - -result: unsat -failed to reconstruct proof: could not parse solver output: incomplete input: expected a token, got none -solver stdout: - -solver stderr: -Fatal failure within virtual bool cvc5::internal::proof::LeanProofPostprocessCallback::update(cvc5::internal::Node, cvc5::internal::PfRule, const std::vector >&, const std::vector >&, cvc5::internal::CDProof*, bool&) at /home/hbarbosa/cvc/wt-leanPrinter/src/proof/lean/lean_post_processor.cpp:785 -Unreachable code reached Higher-order congruence not supported yet - Test/Int/Binders.lean:11:0: warning: declaration uses 'sorry' goal: partCurryAdd' a b = partCurryAdd' b a @@ -42,15 +24,6 @@ query: (declare-const a Int) (assert (not (= (|partCurryAdd'| a b) (|partCurryAdd'| b a)))) (check-sat) - -result: unsat -failed to reconstruct proof: could not parse solver output: incomplete input: expected a token, got none -solver stdout: - -solver stderr: -Fatal failure within virtual bool cvc5::internal::proof::LeanProofPostprocessCallback::update(cvc5::internal::Node, cvc5::internal::PfRule, const std::vector >&, const std::vector >&, cvc5::internal::CDProof*, bool&) at /home/hbarbosa/cvc/wt-leanPrinter/src/proof/lean/lean_post_processor.cpp:785 -Unreachable code reached Higher-order congruence not supported yet - Test/Int/Binders.lean:15:0: warning: declaration uses 'sorry' goal: mismatchNamesAdd a b = mismatchNamesAdd b a @@ -60,13 +33,4 @@ query: (declare-const a Int) (assert (not (= (mismatchNamesAdd a b) (mismatchNamesAdd b a)))) (check-sat) - -result: unsat -failed to reconstruct proof: could not parse solver output: incomplete input: expected a token, got none -solver stdout: - -solver stderr: -Fatal failure within virtual bool cvc5::internal::proof::LeanProofPostprocessCallback::update(cvc5::internal::Node, cvc5::internal::PfRule, const std::vector >&, const std::vector >&, cvc5::internal::CDProof*, bool&) at /home/hbarbosa/cvc/wt-leanPrinter/src/proof/lean/lean_post_processor.cpp:785 -Unreachable code reached Higher-order congruence not supported yet - Test/Int/Binders.lean:25:0: warning: declaration uses 'sorry' diff --git a/Test/Int/Binders.lean b/Test/Int/Binders.lean index 6ce8a083..7c0624bb 100644 --- a/Test/Int/Binders.lean +++ b/Test/Int/Binders.lean @@ -3,25 +3,25 @@ import Smt def curryAdd : Int → Int → Int := Int.add example (a b : Int) : curryAdd a b = curryAdd b a := by - smt [curryAdd] + smt_show [curryAdd] sorry def partCurryAdd (a : Int) : Int → Int := Int.add a example (a b : Int) : partCurryAdd a b = partCurryAdd b a := by - smt [partCurryAdd] + smt_show [partCurryAdd] sorry example (a b : Int) : let partCurryAdd' := fun a => Int.add a; partCurryAdd' a b = partCurryAdd' b a := by intro partCurryAdd' - smt [partCurryAdd'] + smt_show [partCurryAdd'] sorry set_option linter.unusedVariables false in def mismatchNamesAdd : ∀ (a b : Int), Int := fun c d => c + d example (a b : Int) : mismatchNamesAdd a b = mismatchNamesAdd b a := by - smt [mismatchNamesAdd] + smt_show [mismatchNamesAdd] sorry diff --git a/Test/Int/Cong.expected b/Test/Int/Cong.expected index d6149d1d..e472e520 100644 --- a/Test/Int/Cong.expected +++ b/Test/Int/Cong.expected @@ -6,6 +6,3 @@ query: (declare-const y Int) (assert (not (=> (= x y) (= (f x) (f y))))) (check-sat) - -result: unsat -Test/Int/Cong.lean:5:2: error: no goals to be solved diff --git a/Test/Int/Cong.lean b/Test/Int/Cong.lean index efbb67f7..6c7108c7 100644 --- a/Test/Int/Cong.lean +++ b/Test/Int/Cong.lean @@ -1,5 +1,5 @@ import Smt theorem cong (x y : Int) (f : Int → Int) : x = y → f x = f y := by - smt + smt_show simp_all diff --git a/Test/Int/DefineSort.expected b/Test/Int/DefineSort.expected index 44bb1bd2..87ff65d3 100644 --- a/Test/Int/DefineSort.expected +++ b/Test/Int/DefineSort.expected @@ -7,13 +7,4 @@ query: (declare-const a MyInt) (assert (not (= (MyInt.add a b) (MyInt.add b a)))) (check-sat) - -result: unsat -failed to reconstruct proof: could not parse solver output: incomplete input: expected a token, got none -solver stdout: - -solver stderr: -Fatal failure within virtual bool cvc5::internal::proof::LeanProofPostprocessCallback::update(cvc5::internal::Node, cvc5::internal::PfRule, const std::vector >&, const std::vector >&, cvc5::internal::CDProof*, bool&) at /home/hbarbosa/cvc/wt-leanPrinter/src/proof/lean/lean_post_processor.cpp:785 -Unreachable code reached Higher-order congruence not supported yet - Test/Int/DefineSort.lean:6:0: warning: declaration uses 'sorry' diff --git a/Test/Int/DefineSort.lean b/Test/Int/DefineSort.lean index 4d160488..5ecd7e8b 100644 --- a/Test/Int/DefineSort.lean +++ b/Test/Int/DefineSort.lean @@ -4,5 +4,5 @@ def MyInt := Int def MyInt.add (a b : MyInt) : MyInt := Int.add a b example (a b : MyInt) : a.add b = b.add a := by - smt [MyInt, MyInt.add] + smt_show [MyInt, MyInt.add] sorry diff --git a/Test/Int/Dvd.expected b/Test/Int/Dvd.expected index 08720425..fb0f8637 100644 --- a/Test/Int/Dvd.expected +++ b/Test/Int/Dvd.expected @@ -3,26 +3,13 @@ goal: dvd a c = true query: (declare-fun dvd (Int Int) Bool) (assert (forall ((x Int)) (forall ((y Int)) (forall ((z Int)) (=> (= (dvd x y) true) (=> (= (dvd y z) true) (= (dvd x z) true))))))) -(declare-const b Int) (declare-const c Int) +(declare-const b Int) (assert (= (dvd b c) true)) (declare-const a Int) (assert (= (dvd a b) true)) (assert (not (= (dvd a c) true))) (check-sat) - -result: unsat -failed to reconstruct proof: tactic 'apply' failed, failed to unify - ¬?dvd ?a ?c = True → False -with - ¬¬dvd a c = true -a b c d e : ℤ -dvdax : ∀ (x y z : ℤ), dvd x y = true → dvd y z = true → dvd x z = true -h1 : dvd a b = true -h2 : dvd b c = true -h3 : dvd c d = true -h4 : dvd d e = true -⊢ ¬¬dvd a c = true goal: dvd c e = true query: @@ -35,44 +22,15 @@ query: (assert (= (dvd c d) true)) (assert (not (= (dvd c e) true))) (check-sat) - -result: unsat -failed to reconstruct proof: tactic 'apply' failed, failed to unify - ¬?dvd ?c ?e = True → False -with - ¬¬dvd c e = true -a b c d e : ℤ -dvdax : ∀ (x y z : ℤ), dvd x y = true → dvd y z = true → dvd x z = true -h1 : dvd a b = true -h2 : dvd b c = true -h3 : dvd c d = true -h4 : dvd d e = true -h5 : dvd a c = true -⊢ ¬¬dvd c e = true goal: dvd a e = true query: (declare-fun dvd (Int Int) Bool) (assert (forall ((x Int)) (forall ((y Int)) (forall ((z Int)) (=> (= (dvd x y) true) (=> (= (dvd y z) true) (= (dvd x z) true))))))) -(declare-const c Int) (declare-const e Int) +(declare-const c Int) (assert (= (dvd c e) true)) (declare-const a Int) (assert (= (dvd a c) true)) (assert (not (= (dvd a e) true))) (check-sat) - -result: unsat -failed to reconstruct proof: tactic 'apply' failed, failed to unify - ¬?dvd ?a ?e = True → False -with - ¬¬dvd a e = true -a b c d e : ℤ -dvdax : ∀ (x y z : ℤ), dvd x y = true → dvd y z = true → dvd x z = true -h1 : dvd a b = true -h2 : dvd b c = true -h3 : dvd c d = true -h4 : dvd d e = true -h5 : dvd a c = true -h6 : dvd c e = true -⊢ ¬¬dvd a e = true diff --git a/Test/Int/Dvd.lean b/Test/Int/Dvd.lean index 3978bd5f..b3aa4689 100644 --- a/Test/Int/Dvd.lean +++ b/Test/Int/Dvd.lean @@ -11,10 +11,10 @@ example (h4 : dvd d e) : dvd a e := by have h5 : dvd a c := by - smt [h1, h2, dvdax] + smt_show [h1, h2, dvdax] exact dvdax _ _ _ h1 h2 have h6 : dvd c e := by - smt [h3, h4, dvdax] + smt_show [h3, h4, dvdax] exact dvdax _ _ _ h3 h4 - smt [h5, h6, dvdax] + smt_show [h5, h6, dvdax] exact dvdax _ _ _ h5 h6 diff --git a/Test/Int/DvdTimeout.expected b/Test/Int/DvdTimeout.expected index 7f58f2a8..96cb9ac8 100644 --- a/Test/Int/DvdTimeout.expected +++ b/Test/Int/DvdTimeout.expected @@ -1,9 +1,9 @@ goal: dvd a (b + c + d) = true query: -(declare-fun dvd (Int Int) Bool) (declare-const a Int) (declare-const d Int) +(declare-fun dvd (Int Int) Bool) (assert (= (dvd a d) true)) (declare-const c Int) (assert (= (dvd a c) true)) @@ -12,8 +12,11 @@ query: (assert (forall ((x Int)) (forall ((y Int)) (forall ((z Int)) (=> (= (dvd x y) true) (=> (= (dvd x z) true) (= (dvd x (+ y z)) true))))))) (assert (not (= (dvd a (+ (+ b c) d)) true))) (check-sat) -Test/Int/DvdTimeout.lean:13:4: error: could not parse solver output: incomplete input: expected a token, got none -solver stdout: - -solver stderr: -cvc5 interrupted by timeout. +Test/Int/DvdTimeout.lean:12:25: error: unsolved goals +a b c d : Int +dvdax : ∀ (x y z : Int), dvd x y = true → dvd x z = true → dvd x (y + z) = true +h1 : dvd a b = true +h2 : dvd a c = true +h3 : dvd a d = true +⊢ dvd a (b + c + d) = true +Test/Int/DvdTimeout.lean:13:33: error: unexpected token '(timeout :='; expected command diff --git a/Test/Int/DvdTimeout.lean b/Test/Int/DvdTimeout.lean index ba80ab14..33a02954 100644 --- a/Test/Int/DvdTimeout.lean +++ b/Test/Int/DvdTimeout.lean @@ -10,4 +10,4 @@ example (h2 : dvd a c) (h3 : dvd a d) : dvd a (b + c + d) := by - smt [dvdax, h1, h2, h3] (timeout := 1) + smt_show [dvdax, h1, h2, h3] (timeout := 1) diff --git a/Test/Int/ForallExists.expected b/Test/Int/ForallExists.expected index 63935d1c..a70ed2fb 100644 --- a/Test/Int/ForallExists.expected +++ b/Test/Int/ForallExists.expected @@ -1,12 +1,5 @@ -goal: ∀ (x : ℕ), ∃ y, ↑x ≤ y +goal: ∀ (x : Nat), ∃ y, ↑x ≤ y query: (assert (not (forall ((x Int)) (=> (>= x 0) (exists ((y Int)) (<= x y)))))) (check-sat) - -result: unsat -failed to reconstruct proof: tactic 'apply' failed, failed to unify - (¬∀ (x : ℤ), Implies (x ≥ 0) (∃ y, x ≤ y)) → False -with - ¬¬∀ (x : ℕ), ∃ y, ↑x ≤ y -⊢ ¬¬∀ (x : ℕ), ∃ y, ↑x ≤ y diff --git a/Test/Int/ForallExists.lean b/Test/Int/ForallExists.lean index 82b166e8..fd0ce094 100644 --- a/Test/Int/ForallExists.lean +++ b/Test/Int/ForallExists.lean @@ -1,7 +1,7 @@ import Smt theorem forallExists : ∀ x : Nat, ∃ y : Int, x ≤ y := by - smt + smt_show intro x apply Exists.intro case w => exact Int.ofNat x diff --git a/Test/Int/Let.expected b/Test/Int/Let.expected index f3712678..6bd26a16 100644 --- a/Test/Int/Let.expected +++ b/Test/Int/Let.expected @@ -6,8 +6,11 @@ query: (assert (= (f 10) 10)) (assert (not (let ((y 10)) (= (f y) 10)))) (check-sat) - -result: unsat +Test/Int/Let.lean:5:51: error: unsolved goals +f : Int → Int +h : f 10 = 10 +⊢ let y := 10; + f y = 10 goal: f 10 = 10 query: @@ -15,8 +18,12 @@ query: (assert (let ((y 10)) (= (f y) 10))) (assert (not (= (f 10) 10))) (check-sat) - -result: unsat +Test/Int/Let.lean:8:51: error: unsolved goals +f : Int → Int +h : + let y := 10; + f y = 10 +⊢ f 10 = 10 goal: f z = z query: @@ -25,10 +32,6 @@ query: (assert (= (f 10) 10)) (assert (not (= (f z) z))) (check-sat) - -result: unsat -failed to reconstruct proof: invalid 'simp', proposition expected - ℤ goal: f y = y query: @@ -38,10 +41,6 @@ query: (assert (= (f 10) 10)) (assert (not (= (f y) y))) (check-sat) - -result: unsat -failed to reconstruct proof: invalid 'simp', proposition expected - ℤ goal: z 3 = 10 query: @@ -50,12 +49,3 @@ query: (assert (= (f 10) 10)) (assert (not (= (z 3) 10))) (check-sat) - -result: unsat -failed to reconstruct proof: could not parse solver output: incomplete input: expected a token, got none -solver stdout: - -solver stderr: -Fatal failure within virtual bool cvc5::internal::proof::LeanProofPostprocessCallback::update(cvc5::internal::Node, cvc5::internal::PfRule, const std::vector >&, const std::vector >&, cvc5::internal::CDProof*, bool&) at /home/hbarbosa/cvc/wt-leanPrinter/src/proof/lean/lean_post_processor.cpp:785 -Unreachable code reached Higher-order congruence not supported yet - diff --git a/Test/Int/Let.lean b/Test/Int/Let.lean index 906ef717..ffc32dda 100644 --- a/Test/Int/Let.lean +++ b/Test/Int/Let.lean @@ -3,16 +3,16 @@ import Smt variable (f : Int → Int) example (h : f 10 = 10) : let y := 10; f y = 10 := by - smt [h] + smt_show [h] example (h : let y := 10; f y = 10) : f 10 = 10 := by - smt [h] + smt_show [h] example (h : f 10 = 10) : f 10 = 10 := by let z : Int := 10 have : 10 = z := rfl rw [this] - smt [h, z] + smt_show [h, z] exact h example (h : f 10 = 10) : f 10 = 10 := by @@ -20,12 +20,12 @@ example (h : f 10 = 10) : f 10 = 10 := by let y : Int := z have : 10 = y := rfl rw [this] - smt [h, y, z] + smt_show [h, y, z] exact h example (h : f 10 = 10) : f 10 = 10 := by let z (_ : Int) : Int := f 10 have : f 10 = z 3 := rfl rw [this] - smt [h, z] + smt_show [h, z] exact h diff --git a/Test/Int/Neg.expected b/Test/Int/Neg.expected index 259f6fb8..028bee62 100644 --- a/Test/Int/Neg.expected +++ b/Test/Int/Neg.expected @@ -4,6 +4,5 @@ query: (declare-const x Int) (assert (not (= (- (- x)) x))) (check-sat) - -result: unsat Test/Int/Neg.lean:3:8: warning: declaration uses 'sorry' +Test/Int/Neg.lean:4:11: warning: Used `tac1 <;> tac2` where `(tac1; tac2)` would suffice [linter.unnecessarySeqFocus] diff --git a/Test/Int/Neg.lean b/Test/Int/Neg.lean index cb847997..26a0429a 100644 --- a/Test/Int/Neg.lean +++ b/Test/Int/Neg.lean @@ -1,4 +1,4 @@ import Smt theorem neg (x : Int) : - -x = x := by - smt <;> sorry + smt_show <;> sorry diff --git a/Test/Nat/Cong.expected b/Test/Nat/Cong.expected index 9ac6c73e..3761ce02 100644 --- a/Test/Nat/Cong.expected +++ b/Test/Nat/Cong.expected @@ -3,13 +3,10 @@ goal: x = y → f x = f y query: (define-sort Nat () Int) (declare-fun f (Nat) Nat) -(assert (forall ((_uniq.30 Nat)) (=> (>= _uniq.30 0) (>= (f _uniq.30) 0)))) +(assert (forall ((_uniq.40 Nat)) (=> (>= _uniq.40 0) (>= (f _uniq.40) 0)))) (declare-const x Nat) (assert (>= x 0)) (declare-const y Nat) (assert (>= y 0)) (assert (not (=> (= x y) (= (f x) (f y))))) (check-sat) - -result: unsat -failed to reconstruct proof: encountered errors elaborating cvc5 proof diff --git a/Test/Nat/Cong.lean b/Test/Nat/Cong.lean index 2713d097..3b53b406 100644 --- a/Test/Nat/Cong.lean +++ b/Test/Nat/Cong.lean @@ -1,5 +1,5 @@ import Smt theorem cong (x y : Nat) (f : Nat → Nat) : x = y → f x = f y := by - smt + smt_show simp_all diff --git a/Test/Nat/Exists''.expected b/Test/Nat/Exists''.expected index b833978a..d741f3f6 100644 --- a/Test/Nat/Exists''.expected +++ b/Test/Nat/Exists''.expected @@ -4,10 +4,3 @@ query: (define-sort Nat () Int) (assert (not (exists ((x Nat)) (>= x 0)))) (check-sat) - -result: unsat -failed to reconstruct proof: tactic 'apply' failed, failed to unify - (¬∃ x, x ≥ 0) → False -with - ¬¬∃ x, x ≥ 0 -⊢ ¬¬∃ x, x ≥ 0 diff --git a/Test/Nat/Exists''.lean b/Test/Nat/Exists''.lean index b3fbdf4d..f40d51e7 100644 --- a/Test/Nat/Exists''.lean +++ b/Test/Nat/Exists''.lean @@ -1,5 +1,5 @@ import Smt theorem exists'' : ∃ x : Nat, x ≥ 0 := by - smt + smt_show exact ⟨0, by decide⟩ diff --git a/Test/Nat/Exists'.expected b/Test/Nat/Exists'.expected index c1d40ac5..3e66ff5d 100644 --- a/Test/Nat/Exists'.expected +++ b/Test/Nat/Exists'.expected @@ -4,10 +4,3 @@ query: (define-sort Nat () Int) (assert (not (exists ((x Nat)) (= x 1)))) (check-sat) - -result: unsat -failed to reconstruct proof: tactic 'apply' failed, failed to unify - (¬∃ x, x = 1) → False -with - ¬¬∃ x, x = 1 -⊢ ¬¬∃ x, x = 1 diff --git a/Test/Nat/Exists'.lean b/Test/Nat/Exists'.lean index 53ebbfbe..45d2957d 100644 --- a/Test/Nat/Exists'.lean +++ b/Test/Nat/Exists'.lean @@ -1,5 +1,5 @@ import Smt theorem exists' : ∃ x : Nat, x = 1 := by - smt + smt_show exact ⟨1, rfl⟩ diff --git a/Test/Nat/Forall'.expected b/Test/Nat/Forall'.expected index 49286407..0c93adb5 100644 --- a/Test/Nat/Forall'.expected +++ b/Test/Nat/Forall'.expected @@ -1,12 +1,5 @@ -goal: ∀ (x : ℕ), x ≥ 0 +goal: ∀ (x : Nat), x ≥ 0 query: (assert (not (forall ((x Int)) (=> (>= x 0) (>= x 0))))) (check-sat) - -result: unsat -failed to reconstruct proof: tactic 'apply' failed, failed to unify - (¬∀ (x : ℤ), Implies (x ≥ 0) (x ≥ 0)) → False -with - ¬¬∀ (x : ℕ), x ≥ 0 -⊢ ¬¬∀ (x : ℕ), x ≥ 0 diff --git a/Test/Nat/Forall'.lean b/Test/Nat/Forall'.lean index 71b95030..acad0699 100644 --- a/Test/Nat/Forall'.lean +++ b/Test/Nat/Forall'.lean @@ -1,5 +1,5 @@ import Smt theorem forall' : ∀ x : Nat, x ≥ 0 := by - smt + smt_show simp [Nat.zero_le] diff --git a/Test/Nat/Max.expected b/Test/Nat/Max.expected index 9c2cd32e..b54b4ece 100644 --- a/Test/Nat/Max.expected +++ b/Test/Nat/Max.expected @@ -2,29 +2,23 @@ goal: x ≤ max' x y ∧ y ≤ max' x y query: (define-sort Nat () Int) +(declare-const x Nat) +(assert (>= x 0)) (declare-fun |Nat.max'| (Nat Nat) Nat) -(assert (forall ((_uniq.217 Nat)) (=> (>= _uniq.217 0) (forall ((_uniq.218 Nat)) (=> (>= _uniq.218 0) (>= (|Nat.max'| _uniq.217 _uniq.218) 0)))))) +(assert (forall ((_uniq.221 Nat)) (=> (>= _uniq.221 0) (forall ((_uniq.222 Nat)) (=> (>= _uniq.222 0) (>= (|Nat.max'| _uniq.221 _uniq.222) 0)))))) (declare-const y Nat) (assert (>= y 0)) -(declare-const x Nat) -(assert (>= x 0)) (assert (not (and (<= x (|Nat.max'| x y)) (<= y (|Nat.max'| x y))))) (check-sat) - -result: unknown -Test/Nat/Max.lean:12:2: error: unable to prove goal goal: x ≤ max' x y ∧ y ≤ max' x y query: (define-sort Nat () Int) (define-fun |Nat.max'| ((x Nat) (y Nat)) Nat (ite (<= x y) y x)) -(assert (forall ((_uniq.257 Nat)) (=> (>= _uniq.257 0) (forall ((_uniq.258 Nat)) (=> (>= _uniq.258 0) (>= (|Nat.max'| _uniq.257 _uniq.258) 0)))))) +(assert (forall ((_uniq.506 Nat)) (=> (>= _uniq.506 0) (forall ((_uniq.507 Nat)) (=> (>= _uniq.507 0) (>= (|Nat.max'| _uniq.506 _uniq.507) 0)))))) (declare-const x Nat) (assert (>= x 0)) (declare-const y Nat) (assert (>= y 0)) (assert (not (and (<= x (|Nat.max'| x y)) (<= y (|Nat.max'| x y))))) (check-sat) - -result: unsat -failed to reconstruct proof: operator does not have function type diff --git a/Test/Nat/Max.lean b/Test/Nat/Max.lean index f0d66f60..31695ef7 100644 --- a/Test/Nat/Max.lean +++ b/Test/Nat/Max.lean @@ -9,12 +9,12 @@ theorem Nat.not_le_of_reverse_le {m n : Nat} : ¬ m ≤ n → n ≤ m := fun hn theorem Nat.max'_ge : ∀ x y : Nat, x ≤ max' x y ∧ y ≤ max' x y := by intro x y - smt + smt_show by_cases h : x ≤ y <;> simp [max', h] apply not_le_of_reverse_le h theorem Nat.max'_ge' : ∀ x y : Nat, x ≤ max' x y ∧ y ≤ max' x y := by intro x y - smt [max'] + smt_show [max'] by_cases h : x ≤ y <;> simp [max', h] apply not_le_of_reverse_le h diff --git a/Test/Nat/NeqZero.expected b/Test/Nat/NeqZero.expected index d89779a5..7b40c2ff 100644 --- a/Test/Nat/NeqZero.expected +++ b/Test/Nat/NeqZero.expected @@ -1,24 +1,12 @@ -goal: ∀ (x : ℕ), x ≠ 0 +goal: ∀ (x : Nat), x ≠ 0 query: (assert (not (forall ((x Int)) (=> (>= x 0) (distinct x 0))))) (check-sat) - -result: sat - -counter-model: -() -Test/Nat/NeqZero.lean:4:2: error: unable to prove goal, either it is false or you need to define more symbols with `smt [foo, bar]` -goal: ∀ (x : ℕ), x + 1 ≠ 0 +Test/Nat/NeqZero.lean:3:8: warning: declaration uses 'sorry' +goal: ∀ (x : Nat), x + 1 ≠ 0 query: (assert (not (forall ((x Int)) (=> (>= x 0) (distinct (+ x 1) 0))))) (check-sat) - -result: unsat -failed to reconstruct proof: tactic 'apply' failed, failed to unify - (¬∀ (x : ℤ), Implies (x ≥ 0) (x + 1 ≠ 0)) → False -with - ¬¬∀ (x : ℕ), x + 1 ≠ 0 -⊢ ¬¬∀ (x : ℕ), x + 1 ≠ 0 Test/Nat/NeqZero.lean:7:8: warning: declaration uses 'sorry' diff --git a/Test/Nat/NeqZero.lean b/Test/Nat/NeqZero.lean index 23bcfa80..92b0b017 100644 --- a/Test/Nat/NeqZero.lean +++ b/Test/Nat/NeqZero.lean @@ -1,9 +1,9 @@ import Smt theorem neq_zero : ∀ (x : Nat), x ≠ 0 := by - smt + smt_show admit theorem succ_neq_zero : ∀ (x : Nat), x + 1 ≠ 0 := by - smt + smt_show admit diff --git a/Test/Nat/Sum'.expected b/Test/Nat/Sum'.expected index 600a90b5..da3d9198 100644 --- a/Test/Nat/Sum'.expected +++ b/Test/Nat/Sum'.expected @@ -1,36 +1,14 @@ -goal: sum Nat.zero = Nat.zero * (Nat.zero + 1) / 2 - -query: -(define-sort Nat () Int) -(define-fun Nat.sub ((x Nat) (y Nat)) Nat (ite (< x y) 0 (- x y))) -(assert (forall ((_uniq.12533 Nat)) (=> (>= _uniq.12533 0) (forall ((_uniq.12534 Nat)) (=> (>= _uniq.12534 0) (>= (Nat.sub _uniq.12533 _uniq.12534) 0)))))) -(define-fun-rec sum ((n Nat)) Nat (ite (= n 0) 0 (+ n (sum (Nat.sub n 1))))) -(assert (forall ((_uniq.12535 Nat)) (=> (>= _uniq.12535 0) (>= (sum _uniq.12535) 0)))) -(assert (not (= (sum 0) (div (* 0 (+ 0 1)) 2)))) -(check-sat) - -result: unsat -failed to reconstruct proof: operator does not have function type +Test/Nat/Sum'.lean:7:12: error: unknown free variable 'sum' goal: sum (Nat.succ n) = Nat.succ n * (Nat.succ n + 1) / 2 query: (define-sort Nat () Int) -(define-fun Nat.sub ((x Nat) (y Nat)) Nat (ite (< x y) 0 (- x y))) -(assert (forall ((_uniq.12553 Nat)) (=> (>= _uniq.12553 0) (forall ((_uniq.12554 Nat)) (=> (>= _uniq.12554 0) (>= (Nat.sub _uniq.12553 _uniq.12554) 0)))))) -(define-fun-rec sum ((n Nat)) Nat (ite (= n 0) 0 (+ n (sum (Nat.sub n 1))))) -(assert (forall ((_uniq.12555 Nat)) (=> (>= _uniq.12555 0) (>= (sum _uniq.12555) 0)))) (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)))))) +(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 (= (sum n) (div (* n (+ n 1)) 2))) (assert (not (= (sum (+ n 1)) (div (* (+ n 1) (+ (+ n 1) 1)) 2)))) (check-sat) - -result: unsat -failed to reconstruct proof: could not parse solver output: incomplete input: expected a token, got none -solver stdout: - -solver stderr: -Fatal failure within cvc5::internal::Node cvc5::internal::proof::LeanNodeConverter::convert(cvc5::internal::Node) at /home/hbarbosa/cvc/wt-leanPrinter/src/proof/lean/lean_node_converter.cpp:549 -Unreachable code reached Kind * is not supported - -Test/Nat/Sum'.lean:5:8: warning: declaration uses 'sorry' diff --git a/Test/Nat/Sum'.lean b/Test/Nat/Sum'.lean index 743b85f4..445094a2 100644 --- a/Test/Nat/Sum'.lean +++ b/Test/Nat/Sum'.lean @@ -6,5 +6,5 @@ theorem sum_formula : sum n = n * (n + 1) / 2 := by induction n with | zero => smt [sum]; rfl | succ n ih => - smt [sum, ih] + smt_show [sum, ih] sorry diff --git a/Test/Nat/Triv'.expected b/Test/Nat/Triv'.expected index a08ec457..7abc888b 100644 --- a/Test/Nat/Triv'.expected +++ b/Test/Nat/Triv'.expected @@ -3,10 +3,3 @@ goal: 0 + 1 = 1 query: (assert (not (= (+ 0 1) 1))) (check-sat) - -result: unsat -failed to reconstruct proof: tactic 'apply' failed, failed to unify - ¬Int.ofNat 0 + 1 = 1 → False -with - ¬¬0 + 1 = 1 -⊢ ¬¬0 + 1 = 1 diff --git a/Test/Nat/Triv'.lean b/Test/Nat/Triv'.lean index 1eaf0cc5..fbd2ca89 100644 --- a/Test/Nat/Triv'.lean +++ b/Test/Nat/Triv'.lean @@ -1,5 +1,5 @@ import Smt theorem triv' : 0 + 1 = 1 := by - smt + smt_show simp_all diff --git a/Test/Nat/Triv.expected b/Test/Nat/Triv.expected index 9e4d08ad..e7e4a8ea 100644 --- a/Test/Nat/Triv.expected +++ b/Test/Nat/Triv.expected @@ -3,10 +3,3 @@ goal: Nat.zero + Nat.succ Nat.zero = Nat.succ Nat.zero query: (assert (not (= (+ 0 (+ 0 1)) (+ 0 1)))) (check-sat) - -result: unsat -failed to reconstruct proof: tactic 'apply' failed, failed to unify - ¬0 + (Int.ofNat 0 + 1) = Int.ofNat 0 + 1 → False -with - ¬¬Nat.zero + Nat.succ Nat.zero = Nat.succ Nat.zero -⊢ ¬¬Nat.zero + Nat.succ Nat.zero = Nat.succ Nat.zero diff --git a/Test/Nat/Triv.lean b/Test/Nat/Triv.lean index 5d794e8e..9e19e9e4 100644 --- a/Test/Nat/Triv.lean +++ b/Test/Nat/Triv.lean @@ -1,5 +1,5 @@ import Smt theorem triv : Nat.zero + Nat.succ Nat.zero = Nat.succ Nat.zero := by - smt + smt_show simp_all diff --git a/Test/Nat/ZeroSub'.expected b/Test/Nat/ZeroSub'.expected index 26a2fe01..026c4dda 100644 --- a/Test/Nat/ZeroSub'.expected +++ b/Test/Nat/ZeroSub'.expected @@ -1,37 +1,4 @@ -goal: 0 - Nat.zero = 0 - -query: -(define-sort Nat () Int) -(define-fun Nat.sub ((x Nat) (y Nat)) Nat (ite (< x y) 0 (- x y))) -(assert (forall ((_uniq.229 Nat)) (=> (>= _uniq.229 0) (forall ((_uniq.230 Nat)) (=> (>= _uniq.230 0) (>= (Nat.sub _uniq.229 _uniq.230) 0)))))) -(assert (not (= (Nat.sub 0 0) 0))) -(check-sat) - -result: unsat -failed to reconstruct proof: could not parse solver output: incomplete input: expected a token, got none -solver stdout: - -solver stderr: -Fatal failure within virtual bool cvc5::internal::proof::LeanProofPostprocessCallback::update(cvc5::internal::Node, cvc5::internal::PfRule, const std::vector >&, const std::vector >&, cvc5::internal::CDProof*, bool&) at /home/hbarbosa/cvc/wt-leanPrinter/src/proof/lean/lean_post_processor.cpp:785 -Unreachable code reached Higher-order congruence not supported yet - -goal: 0 - Nat.succ x = 0 - -query: -(define-sort Nat () Int) -(define-fun Nat.sub ((x Nat) (y Nat)) Nat (ite (< x y) 0 (- x y))) -(assert (forall ((_uniq.244 Nat)) (=> (>= _uniq.244 0) (forall ((_uniq.245 Nat)) (=> (>= _uniq.245 0) (>= (Nat.sub _uniq.244 _uniq.245) 0)))))) -(declare-const x Nat) -(assert (>= x 0)) -(assert (= (Nat.sub 0 x) 0)) -(assert (not (= (Nat.sub 0 (+ x 1)) 0))) -(check-sat) - -result: unsat -failed to reconstruct proof: could not parse solver output: incomplete input: expected a token, got none -solver stdout: - -solver stderr: -Fatal failure within virtual bool cvc5::internal::proof::LeanProofPostprocessCallback::update(cvc5::internal::Node, cvc5::internal::PfRule, const std::vector >&, const std::vector >&, cvc5::internal::CDProof*, bool&) at /home/hbarbosa/cvc/wt-leanPrinter/src/proof/lean/lean_post_processor.cpp:785 -Unreachable code reached Higher-order congruence not supported yet - +Test/Nat/ZeroSub'.lean:6:12: error: unknown free variable '«Nat.sub»' +cvc5.Kind.INTERNAL_KIND : @PURIFY_4 +Test/Nat/ZeroSub'.lean:7:17: error: failed to synthesize + Decidable (x ≥ 0) diff --git a/Test/Nat/ZeroSub.expected b/Test/Nat/ZeroSub.expected index 465b3646..575d61dc 100644 --- a/Test/Nat/ZeroSub.expected +++ b/Test/Nat/ZeroSub.expected @@ -3,17 +3,8 @@ goal: 0 - x = 0 query: (define-sort Nat () Int) (define-fun Nat.sub ((x Nat) (y Nat)) Nat (ite (< x y) 0 (- x y))) -(assert (forall ((_uniq.190 Nat)) (=> (>= _uniq.190 0) (forall ((_uniq.191 Nat)) (=> (>= _uniq.191 0) (>= (Nat.sub _uniq.190 _uniq.191) 0)))))) +(assert (forall ((_uniq.150 Nat)) (=> (>= _uniq.150 0) (forall ((_uniq.151 Nat)) (=> (>= _uniq.151 0) (>= (Nat.sub _uniq.150 _uniq.151) 0)))))) (declare-const x Nat) (assert (>= x 0)) (assert (not (= (Nat.sub 0 x) 0))) (check-sat) - -result: unsat -failed to reconstruct proof: could not parse solver output: incomplete input: expected a token, got none -solver stdout: - -solver stderr: -Fatal failure within virtual bool cvc5::internal::proof::LeanProofPostprocessCallback::update(cvc5::internal::Node, cvc5::internal::PfRule, const std::vector >&, const std::vector >&, cvc5::internal::CDProof*, bool&) at /home/hbarbosa/cvc/wt-leanPrinter/src/proof/lean/lean_post_processor.cpp:785 -Unreachable code reached Higher-order congruence not supported yet - diff --git a/Test/Nat/ZeroSub.lean b/Test/Nat/ZeroSub.lean index 455849f5..e28a5cfe 100644 --- a/Test/Nat/ZeroSub.lean +++ b/Test/Nat/ZeroSub.lean @@ -1,5 +1,5 @@ import Smt example : 0 - x = 0 := by - smt + smt_show induction x <;> simp_all [Nat.sub_succ] diff --git a/Test/Prop/Addition.expected b/Test/Prop/Addition.expected index 233d7000..e69de29b 100644 --- a/Test/Prop/Addition.expected +++ b/Test/Prop/Addition.expected @@ -1,9 +0,0 @@ -goal: p → p ∨ q - -query: -(declare-const q Bool) -(declare-const p Bool) -(assert (not (=> p (or p q)))) -(check-sat) - -result: unsat diff --git a/Test/Prop/Assoc.expected b/Test/Prop/Assoc.expected index c10b1426..3056d2be 100644 --- a/Test/Prop/Assoc.expected +++ b/Test/Prop/Assoc.expected @@ -1,20 +1 @@ -goal: f p (f q r) = f (f p q) r - -query: -(declare-const q Bool) -(declare-fun f (Bool Bool) Bool) -(declare-const r Bool) -(declare-const p Bool) -(assert (not (= (f p (f q r)) (f (f p q) r)))) -(check-sat) - -result: sat - -counter-model: -( -(define-fun q () Bool false) -(define-fun f ((_arg_1 Bool) (_arg_2 Bool)) Bool (ite _arg_1 (not _arg_2) (and (not _arg_1) (not _arg_2)))) -(define-fun r () Bool false) -(define-fun p () Bool true) -) Test/Prop/Assoc.lean:5:2: error: unable to prove goal, either it is false or you need to define more symbols with `smt [foo, bar]` diff --git a/Test/Prop/Comm.expected b/Test/Prop/Comm.expected index 5085c744..1c521a20 100644 --- a/Test/Prop/Comm.expected +++ b/Test/Prop/Comm.expected @@ -1,18 +1 @@ -goal: f p q = f q p - -query: -(declare-const q Bool) -(declare-fun f (Bool Bool) Bool) -(declare-const p Bool) -(assert (not (= (f p q) (f q p)))) -(check-sat) - -result: sat - -counter-model: -( -(define-fun q () Bool true) -(define-fun f ((_arg_1 Bool) (_arg_2 Bool)) Bool (and _arg_1 (not _arg_2))) -(define-fun p () Bool false) -) Test/Prop/Comm.lean:4:2: error: unable to prove goal, either it is false or you need to define more symbols with `smt [foo, bar]` diff --git a/Test/Prop/Cong.expected b/Test/Prop/Cong.expected index 954da559..d3408654 100644 --- a/Test/Prop/Cong.expected +++ b/Test/Prop/Cong.expected @@ -6,5 +6,7 @@ query: (declare-const q Bool) (assert (not (=> (= p q) (= (f p) (f q))))) (check-sat) - -result: unsat +Test/Prop/Cong.lean:3:67: error: unsolved goals +p q : Prop +f : Prop → Prop +⊢ p = q → f p = f q diff --git a/Test/Prop/Cong.lean b/Test/Prop/Cong.lean index fbfbd6f1..c52c6bf6 100644 --- a/Test/Prop/Cong.lean +++ b/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 + smt_show diff --git a/Test/Prop/Conjunction.expected b/Test/Prop/Conjunction.expected index b80f67fb..e69de29b 100644 --- a/Test/Prop/Conjunction.expected +++ b/Test/Prop/Conjunction.expected @@ -1,9 +0,0 @@ -goal: p → q → p ∧ q - -query: -(declare-const p Bool) -(declare-const q Bool) -(assert (not (=> p (=> q (and p q))))) -(check-sat) - -result: unsat diff --git a/Test/Prop/DisjunctiveSyllogism.expected b/Test/Prop/DisjunctiveSyllogism.expected index d99e795b..e69de29b 100644 --- a/Test/Prop/DisjunctiveSyllogism.expected +++ b/Test/Prop/DisjunctiveSyllogism.expected @@ -1,9 +0,0 @@ -goal: p ∨ q → ¬p → q - -query: -(declare-const p Bool) -(declare-const q Bool) -(assert (not (=> (or p q) (=> (not p) q)))) -(check-sat) - -result: unsat diff --git a/Test/Prop/Exists'.expected b/Test/Prop/Exists'.expected index 027c4735..e69de29b 100644 --- a/Test/Prop/Exists'.expected +++ b/Test/Prop/Exists'.expected @@ -1,7 +0,0 @@ -goal: ∃ p, p - -query: -(assert (not (exists ((p Bool)) p))) -(check-sat) - -result: unsat diff --git a/Test/Prop/Exists'.lean b/Test/Prop/Exists'.lean index d508fa03..13ce8f89 100644 --- a/Test/Prop/Exists'.lean +++ b/Test/Prop/Exists'.lean @@ -2,15 +2,13 @@ import Smt theorem exists' : ∃ p : Prop, p := by smt - · apply propext - apply Iff.intro + · intro; apply propext; apply Iff.intro · intro ⟨p, hp⟩ hnp exact hnp p hp · intro exact ⟨True, True.intro⟩ - · apply propext - apply Iff.intro + · intro; apply propext; apply Iff.intro + · intro hnp + exact hnp True · intro hf contradiction - · intro hnp - exact hnp True True.intro diff --git a/Test/Prop/Falsum.expected b/Test/Prop/Falsum.expected index b808dd1c..e69de29b 100644 --- a/Test/Prop/Falsum.expected +++ b/Test/Prop/Falsum.expected @@ -1,7 +0,0 @@ -goal: ¬False - -query: -(assert (not (not false))) -(check-sat) - -result: unsat diff --git a/Test/Prop/HypotheticalSyllogism.expected b/Test/Prop/HypotheticalSyllogism.expected index cbcd0542..e69de29b 100644 --- a/Test/Prop/HypotheticalSyllogism.expected +++ b/Test/Prop/HypotheticalSyllogism.expected @@ -1,14 +0,0 @@ -goal: (p → q) → (q → r) → p → r - -query: -(declare-const r Bool) -(declare-const p Bool) -(declare-const q Bool) -(assert (not (=> (=> p q) (=> (=> q r) (=> p r))))) -(check-sat) - -result: unsat -failed to reconstruct proof: encountered errors elaborating cvc5 proof -Test/Prop/HypotheticalSyllogism.lean:3:77: error: unsolved goals -p q r : Prop -⊢ (p → q) → (q → r) → p → r diff --git a/Test/Prop/ModusPonens'.expected b/Test/Prop/ModusPonens'.expected index 1530e634..e69de29b 100644 --- a/Test/Prop/ModusPonens'.expected +++ b/Test/Prop/ModusPonens'.expected @@ -1,11 +0,0 @@ -goal: q - -query: -(declare-const q Bool) -(declare-const p Bool) -(assert (=> p q)) -(assert p) -(assert (not q)) -(check-sat) - -result: unsat diff --git a/Test/Prop/ModusPonens.expected b/Test/Prop/ModusPonens.expected index 5f2c8d81..e69de29b 100644 --- a/Test/Prop/ModusPonens.expected +++ b/Test/Prop/ModusPonens.expected @@ -1,9 +0,0 @@ -goal: p → (p → q) → q - -query: -(declare-const q Bool) -(declare-const p Bool) -(assert (not (=> p (=> (=> p q) q)))) -(check-sat) - -result: unsat diff --git a/Test/Prop/ModusTollens.expected b/Test/Prop/ModusTollens.expected index 900c7fe5..e69de29b 100644 --- a/Test/Prop/ModusTollens.expected +++ b/Test/Prop/ModusTollens.expected @@ -1,9 +0,0 @@ -goal: ¬q → (p → q) → ¬p - -query: -(declare-const p Bool) -(declare-const q Bool) -(assert (not (=> (not q) (=> (=> p q) (not p))))) -(check-sat) - -result: unsat diff --git a/Test/Prop/PropExt.expected b/Test/Prop/PropExt.expected index 1368e9b2..e69de29b 100644 --- a/Test/Prop/PropExt.expected +++ b/Test/Prop/PropExt.expected @@ -1,9 +0,0 @@ -goal: (p ↔ q) → p = q - -query: -(declare-const p Bool) -(declare-const q Bool) -(assert (not (=> (= p q) (= p q)))) -(check-sat) - -result: unsat diff --git a/Test/Prop/Refl.expected b/Test/Prop/Refl.expected index ddf3c519..e69de29b 100644 --- a/Test/Prop/Refl.expected +++ b/Test/Prop/Refl.expected @@ -1,8 +0,0 @@ -goal: p = p - -query: -(declare-const p Bool) -(assert (not (= p p))) -(check-sat) - -result: unsat diff --git a/Test/Prop/Resolution.expected b/Test/Prop/Resolution.expected index 3a072611..e69de29b 100644 --- a/Test/Prop/Resolution.expected +++ b/Test/Prop/Resolution.expected @@ -1,10 +0,0 @@ -goal: p ∨ q → ¬p ∨ r → q ∨ r - -query: -(declare-const q Bool) -(declare-const r Bool) -(declare-const p Bool) -(assert (not (=> (or p q) (=> (or (not p) r) (or q r))))) -(check-sat) - -result: unsat diff --git a/Test/Prop/Simplification.expected b/Test/Prop/Simplification.expected index a6448ac3..e69de29b 100644 --- a/Test/Prop/Simplification.expected +++ b/Test/Prop/Simplification.expected @@ -1,9 +0,0 @@ -goal: p ∧ q → p - -query: -(declare-const q Bool) -(declare-const p Bool) -(assert (not (=> (and p q) p))) -(check-sat) - -result: unsat diff --git a/Test/Prop/Symm.expected b/Test/Prop/Symm.expected index 0968e6f1..e69de29b 100644 --- a/Test/Prop/Symm.expected +++ b/Test/Prop/Symm.expected @@ -1,9 +0,0 @@ -goal: p = q → q = p - -query: -(declare-const q Bool) -(declare-const p Bool) -(assert (not (=> (= p q) (= q p)))) -(check-sat) - -result: unsat diff --git a/Test/Prop/Trans.expected b/Test/Prop/Trans.expected index 01d037c7..e69de29b 100644 --- a/Test/Prop/Trans.expected +++ b/Test/Prop/Trans.expected @@ -1,10 +0,0 @@ -goal: p = q → q = r → p = r - -query: -(declare-const r Bool) -(declare-const p Bool) -(declare-const q Bool) -(assert (not (=> (= p q) (=> (= q r) (= p r))))) -(check-sat) - -result: unsat diff --git a/Test/Prop/Triv'''.expected b/Test/Prop/Triv'''.expected deleted file mode 100644 index e69de29b..00000000 diff --git a/Test/Prop/Triv''.expected b/Test/Prop/Triv''.expected index 1f8a5b49..e69de29b 100644 --- a/Test/Prop/Triv''.expected +++ b/Test/Prop/Triv''.expected @@ -1,8 +0,0 @@ -goal: ¬p → ¬p - -query: -(declare-const p Bool) -(assert (not (=> (not p) (not p)))) -(check-sat) - -result: unsat diff --git a/Test/Prop/Triv'.expected b/Test/Prop/Triv'.expected index 0e9e467b..e69de29b 100644 --- a/Test/Prop/Triv'.expected +++ b/Test/Prop/Triv'.expected @@ -1,7 +0,0 @@ -goal: ∀ (p : Prop), p → p - -query: -(assert (not (forall ((p Bool)) (=> p p)))) -(check-sat) - -result: unsat diff --git a/Test/Prop/Triv'.lean b/Test/Prop/Triv'.lean index 3b55ce30..aa3c6e84 100644 --- a/Test/Prop/Triv'.lean +++ b/Test/Prop/Triv'.lean @@ -1,8 +1,8 @@ import Smt -theorem triv': ∀ p : Prop, p → p := by +example : ∀ p : Prop, p → p := by smt - apply propext - apply Iff.intro - · exact λ _ _ => (Classical.em _).symm - · exact λ _ => True.intro + all_goals + intros; apply propext; apply Iff.intro + · intros; trivial + · intros; trivial diff --git a/Test/Prop/Triv.expected b/Test/Prop/Triv.expected index 4153c341..e69de29b 100644 --- a/Test/Prop/Triv.expected +++ b/Test/Prop/Triv.expected @@ -1,8 +0,0 @@ -goal: p → p - -query: -(declare-const p Bool) -(assert (not (=> p p))) -(check-sat) - -result: unsat diff --git a/Test/Prop/Verum.expected b/Test/Prop/Verum.expected index e1b919e8..e69de29b 100644 --- a/Test/Prop/Verum.expected +++ b/Test/Prop/Verum.expected @@ -1,7 +0,0 @@ -goal: True - -query: -(assert (not true)) -(check-sat) - -result: unsat diff --git a/Test/Rat/Density.expected b/Test/Rat/Density.expected index d5d9f372..3b24009b 100644 --- a/Test/Rat/Density.expected +++ b/Test/Rat/Density.expected @@ -5,7 +5,4 @@ query: (declare-const z Real) (assert (not (=> (= (< x z) true) (exists ((y Real)) (and (= (< x y) true) (= (< y z) true)))))) (check-sat) - -result: unsat -failed to reconstruct proof: encountered errors elaborating cvc5 proof Test/Rat/Density.lean:3:8: warning: declaration uses 'sorry' diff --git a/Test/Rat/Density.lean b/Test/Rat/Density.lean index 4824d5ae..79513e35 100644 --- a/Test/Rat/Density.lean +++ b/Test/Rat/Density.lean @@ -1,5 +1,5 @@ import Smt theorem density (x z : Rat) : x < z → ∃ y, x < y ∧ y < z := by - smt + smt_show sorry diff --git a/Test/Rat/Inverse.expected b/Test/Rat/Inverse.expected index 1c884c5f..e47bc5f3 100644 --- a/Test/Rat/Inverse.expected +++ b/Test/Rat/Inverse.expected @@ -4,8 +4,4 @@ query: (declare-const x Real) (assert (not (=> (distinct x 0) (exists ((y Real)) (= (* x y) 1))))) (check-sat) -Test/Rat/Inverse.lean:4:2: error: could not parse solver output: incomplete input: expected a token, got none -solver stdout: - -solver stderr: -cvc5 interrupted by timeout. +Test/Rat/Inverse.lean:3:8: warning: declaration uses 'sorry' diff --git a/Test/Rat/Inverse.lean b/Test/Rat/Inverse.lean index 057518c7..5e230024 100644 --- a/Test/Rat/Inverse.lean +++ b/Test/Rat/Inverse.lean @@ -1,5 +1,5 @@ import Smt theorem inverse (x : Rat) : x ≠ 0 → ∃ y, x * y = 1 := by - smt + smt_show sorry diff --git a/Test/Reconstruction/Arith/ArithMulSign.expected b/Test/Reconstruction/Arith/ArithMulSign.expected index e69de29b..a72f18f9 100644 --- a/Test/Reconstruction/Arith/ArithMulSign.expected +++ b/Test/Reconstruction/Arith/ArithMulSign.expected @@ -0,0 +1,19 @@ +Test/Reconstruction/Arith/ArithMulSign.lean:24:2: error: type mismatch + _uniq.6012 +has type + a < Int.ofNat 0 → b < Rat.ofInt (Int.ofNat 0) → Rat.ofInt (Pow.pow a 3) * Pow.pow b 3 > 0 : Prop +but is expected to have type + a < 0 → b < 0 → ↑a ^ 3 * b ^ 3 > 0 : Prop +Test/Reconstruction/Arith/ArithMulSign.lean:33:2: error: type mismatch + _uniq.10504 +has type + a < Int.ofNat 0 → + b > Rat.ofInt (Int.ofNat 0) → + c < Rat.ofInt (Int.ofNat 0) → + d > Rat.ofInt (Int.ofNat 0) → + e < Int.ofNat 0 → + Mul.mul (Mul.mul (Mul.mul (Rat.ofInt a) (Pow.pow b 2)) (Pow.pow c 2)) (Pow.pow d 4) * + Rat.ofInt (Pow.pow e 5) > + 0 : Prop +but is expected to have type + a < 0 → b > 0 → c < 0 → d > 0 → e < 0 → ↑a * b ^ 2 * c ^ 2 * d ^ 4 * ↑e ^ 5 > 0 : Prop diff --git a/Test/Reconstruction/Arith/ArithMulSign.lean b/Test/Reconstruction/Arith/ArithMulSign.lean index 83ff41f1..4a4b28c0 100644 --- a/Test/Reconstruction/Arith/ArithMulSign.lean +++ b/Test/Reconstruction/Arith/ArithMulSign.lean @@ -1,6 +1,6 @@ -import Smt +import Smt.Reconstruct.Arith -open Smt.Reconstruct +open Smt.Reconstruct.Arith example (a : Int) : (a + 3) > 0 → (a + 3) ^ 2 > 0 := by arithMulSign [(a + 3)], [1], [2] diff --git a/Test/Reconstruction/Arith/MulPosNeg.expected b/Test/Reconstruction/Arith/MulPosNeg.expected index e69de29b..e982f007 100644 --- a/Test/Reconstruction/Arith/MulPosNeg.expected +++ b/Test/Reconstruction/Arith/MulPosNeg.expected @@ -0,0 +1,8 @@ +Test/Reconstruction/Arith/MulPosNeg.lean:15:2: error: application type mismatch + 2 > Rat.ofInt (Int.ofNat 0) +argument + Rat.ofInt (Int.ofNat 0) +has type + ℚ : Type +but is expected to have type + ℕ : Type diff --git a/Test/Reconstruction/Arith/MulPosNeg.lean b/Test/Reconstruction/Arith/MulPosNeg.lean index f1e55996..cb29e9c3 100644 --- a/Test/Reconstruction/Arith/MulPosNeg.lean +++ b/Test/Reconstruction/Arith/MulPosNeg.lean @@ -1,6 +1,6 @@ -import Smt +import Smt.Reconstruct.Arith -open Smt.Reconstruct +open Smt.Reconstruct.Arith example {a b c : Int} : c > 0 ∧ a < b → c * a < c * b := by arithMulPos [a,b,c], 0 diff --git a/Test/Reconstruction/Arith/SumBounds.lean b/Test/Reconstruction/Arith/SumBounds.lean index 78c85444..69994d98 100644 --- a/Test/Reconstruction/Arith/SumBounds.lean +++ b/Test/Reconstruction/Arith/SumBounds.lean @@ -1,6 +1,6 @@ -import Smt +import Smt.Reconstruct.Arith -open Smt.Reconstruct +open Smt.Reconstruct.Arith example {a b c d e f : Nat} : a < d → b < e → c < f → a + (b + c) < d + (e + f) := by intros h₁ h₂ h₃ diff --git a/Test/Reconstruction/Arith/TightBounds.lean b/Test/Reconstruction/Arith/TightBounds.lean index a0a1f554..a51ea4e6 100644 --- a/Test/Reconstruction/Arith/TightBounds.lean +++ b/Test/Reconstruction/Arith/TightBounds.lean @@ -1,6 +1,6 @@ -import Smt +import Smt.Reconstruct.Arith -open Smt.Reconstruct +open Smt.Reconstruct.Arith example {a b : Int} : a < b → (a : Int) ≤ Int.ceil (Rat.ofInt b) - 1 := by intro h diff --git a/Test/Reconstruction/Arith/Trichotomy.lean b/Test/Reconstruction/Arith/Trichotomy.lean index b6f3dce8..2f10bc68 100644 --- a/Test/Reconstruction/Arith/Trichotomy.lean +++ b/Test/Reconstruction/Arith/Trichotomy.lean @@ -1,6 +1,6 @@ -import Smt +import Smt.Reconstruct.Arith -open Smt.Reconstruct +open Smt.Reconstruct.Arith example {a b : Nat} : a ≥ b → ¬ a = b → a > b := by intros h₁ h₂ diff --git a/Test/Reconstruction/LiftOrNToNeg.lean b/Test/Reconstruction/LiftOrNToNeg.lean index e6456a22..561c3176 100644 --- a/Test/Reconstruction/LiftOrNToNeg.lean +++ b/Test/Reconstruction/LiftOrNToNeg.lean @@ -5,7 +5,6 @@ open Smt.Reconstruct example : ¬ A ∨ B ∨ ¬ C ∨ False → ¬ A ∨ B ∨ ¬ C := by intro h removeFalse h, h₁ - exact h₁ example : ¬ A ∨ ¬ B ∨ ¬ C ∨ ¬ D ∨ False → ¬ (A ∧ B ∧ C ∧ D) := by intro h diff --git a/Test/Solver/Error.lean b/Test/Solver/Error.lean index 712cd091..0a26c755 100644 --- a/Test/Solver/Error.lean +++ b/Test/Solver/Error.lean @@ -1,6 +1,6 @@ -import Smt.Solver +import Smt.Translate.Solver -open Smt Solver +open Smt Translate Solver def query : SolverM Result := do setLogic "LIA" diff --git a/Test/Solver/Interactive.lean b/Test/Solver/Interactive.lean index e626da9e..ace7d9ad 100644 --- a/Test/Solver/Interactive.lean +++ b/Test/Solver/Interactive.lean @@ -1,6 +1,6 @@ -import Smt.Solver +import Smt.Translate.Solver -open Smt Solver +open Smt Translate Solver open Term in def query : SolverM Result := do @@ -20,6 +20,6 @@ def main : IO Unit := do let ss ← createFromKind .cvc5 "cvc5" none let (res, ss) ← StateT.run query ss _ ← StateT.run exit ss - println! "query:\n{Command.cmdsAsQuery ss.commands}\n\nres: {res}" + println! "query:\n{Command.cmdsAsQuery ss.commands.reverse}\n\nres: {res}" #eval main diff --git a/Test/Solver/Model.lean b/Test/Solver/Model.lean index b61a2a41..9ca726f3 100644 --- a/Test/Solver/Model.lean +++ b/Test/Solver/Model.lean @@ -1,6 +1,6 @@ -import Smt.Solver +import Smt.Translate.Solver -open Smt Solver +open Smt Translate Solver def query : SolverM (Result × Sexp) := do setLogic "LIA" @@ -12,6 +12,6 @@ def main : IO Unit := do let ss ← createFromKind .cvc5 "cvc5" none let ((res, model), ss) ← StateT.run query ss _ ← StateT.run exit ss - println! "query:\n{Command.cmdsAsQuery ss.commands}\n\nres: {res}\n\nmodel:\n{model}" + println! "query:\n{Command.cmdsAsQuery ss.commands.reverse}\n\nres: {res}\n\nmodel:\n{model}" #eval main diff --git a/Test/Solver/Proof.expected b/Test/Solver/Proof.expected index 92b4a686..bd46ce9a 100644 --- a/Test/Solver/Proof.expected +++ b/Test/Solver/Proof.expected @@ -7,10 +7,10 @@ query: res: unsat proof: -import Smt.Reconstruct +import Smt.Reconstruction.Certifying open Classical -open Smt.Reconstruct +open Smt.Reconstruction.Certifying diff --git a/Test/Solver/Proof.lean b/Test/Solver/Proof.lean index e6fbdf71..da63f8f3 100644 --- a/Test/Solver/Proof.lean +++ b/Test/Solver/Proof.lean @@ -1,6 +1,6 @@ -import Smt.Solver +import Smt.Translate.Solver -open Smt Solver +open Smt Translate Solver def query : SolverM Sexp := do setLogic "QF_UF" @@ -12,7 +12,7 @@ def main : IO Unit := do let ss ← createFromKind .cvc5 "cvc5" none let (res, ss) ← StateT.run query ss _ ← StateT.run exit ss - println! "query:\n{Command.cmdsAsQuery ss.commands}\n\nres: unsat\n\nproof:\n{unquote (toString res)}" + println! "query:\n{Command.cmdsAsQuery ss.commands.reverse}\n\nres: unsat\n\nproof:\n{unquote (toString res)}" where unquote s := s.extract ⟨8⟩ (s.endPos - ⟨2⟩) diff --git a/Test/Solver/Triv.lean b/Test/Solver/Triv.lean index 4447dcb8..90c9cedc 100644 --- a/Test/Solver/Triv.lean +++ b/Test/Solver/Triv.lean @@ -1,6 +1,6 @@ -import Smt.Solver +import Smt.Translate.Solver -open Smt Solver +open Smt Translate Solver def query : SolverM Result := checkSat @@ -8,6 +8,6 @@ def main : IO Unit := do let ss ← createFromKind .cvc5 "cvc5" none let (res, ss) ← StateT.run query ss _ ← StateT.run exit ss - println! "query:\n{Command.cmdsAsQuery ss.commands}\n\nres: {res}" + println! "query:\n{Command.cmdsAsQuery ss.commands.reverse}\n\nres: {res}" #eval main diff --git a/Test/String/Append.expected b/Test/String/Append.expected index c1cb085c..d7962cad 100644 --- a/Test/String/Append.expected +++ b/Test/String/Append.expected @@ -3,6 +3,3 @@ goal: "a" ++ "b" = "ab" query: (assert (not (= (str.++ "a" "b") "ab"))) (check-sat) - -result: unsat -failed to reconstruct proof: encountered error parsing cvc5 proof diff --git a/Test/String/Append.lean b/Test/String/Append.lean index 50f6fb27..eee2e6c7 100644 --- a/Test/String/Append.lean +++ b/Test/String/Append.lean @@ -1,5 +1,5 @@ import Smt theorem append : "a" ++ "b" = "ab" := by - smt + smt_show rfl diff --git a/Test/String/Contains.expected b/Test/String/Contains.expected index d29bcf13..2bd7b0d2 100644 --- a/Test/String/Contains.expected +++ b/Test/String/Contains.expected @@ -3,15 +3,4 @@ goal: String.contains "a" (Char.ofNat 97) = true query: (assert (not (= (str.contains "a" (str.from_code 97)) true))) (check-sat) - -result: unsat -failed to reconstruct proof: could not parse solver output: incomplete input: expected a token, got none -solver stdout: - -solver stderr: -Fatal failure within cvc5::internal::Node cvc5::internal::proof::LeanNodeConverter::convert(cvc5::internal::Node) at /home/hbarbosa/cvc/wt-leanPrinter/src/proof/lean/lean_node_converter.cpp:236 -Check failure - - !it->second.isNull() - Test/String/Contains.lean:3:8: warning: declaration uses 'sorry' diff --git a/Test/String/Contains.lean b/Test/String/Contains.lean index eb22c14b..3e3eff11 100644 --- a/Test/String/Contains.lean +++ b/Test/String/Contains.lean @@ -1,5 +1,5 @@ import Smt theorem contains : "a".contains 'a' := by - smt + smt_show sorry diff --git a/Test/String/Empty.expected b/Test/String/Empty.expected index 772256cf..3726de30 100644 --- a/Test/String/Empty.expected +++ b/Test/String/Empty.expected @@ -3,6 +3,3 @@ goal: "" = "" query: (assert (not (= "" ""))) (check-sat) - -result: unsat -failed to reconstruct proof: encountered error parsing cvc5 proof diff --git a/Test/String/Empty.lean b/Test/String/Empty.lean index 44ca5406..222a1163 100644 --- a/Test/String/Empty.lean +++ b/Test/String/Empty.lean @@ -1,5 +1,5 @@ import Smt theorem empty : "" = "" := by - smt + smt_show rfl diff --git a/Test/String/GetOp.expected b/Test/String/GetOp.expected index 593049a4..d63b7e91 100644 --- a/Test/String/GetOp.expected +++ b/Test/String/GetOp.expected @@ -3,14 +3,3 @@ goal: String.get "a" 0 = Char.ofNat 97 query: (assert (not (= (str.to_code (str.at "a" 0)) 97))) (check-sat) - -result: unsat -failed to reconstruct proof: could not parse solver output: incomplete input: expected a token, got none -solver stdout: - -solver stderr: -Fatal failure within cvc5::internal::Node cvc5::internal::proof::LeanNodeConverter::convert(cvc5::internal::Node) at /home/hbarbosa/cvc/wt-leanPrinter/src/proof/lean/lean_node_converter.cpp:236 -Check failure - - !it->second.isNull() - diff --git a/Test/String/GetOp.lean b/Test/String/GetOp.lean index 2e179b33..3f863f6d 100644 --- a/Test/String/GetOp.lean +++ b/Test/String/GetOp.lean @@ -1,5 +1,5 @@ import Smt theorem index : "a".get 0 = 'a' := by - smt + smt_show rfl diff --git a/Test/String/Length.expected b/Test/String/Length.expected index ad751807..f9cc4c20 100644 --- a/Test/String/Length.expected +++ b/Test/String/Length.expected @@ -3,6 +3,3 @@ goal: String.length "a" = 1 query: (assert (not (= (str.len "a") 1))) (check-sat) - -result: unsat -failed to reconstruct proof: encountered error parsing cvc5 proof diff --git a/Test/String/Length.lean b/Test/String/Length.lean index 3ffdbc51..7d492e49 100644 --- a/Test/String/Length.lean +++ b/Test/String/Length.lean @@ -1,5 +1,5 @@ import Smt theorem length : "a".length = 1 := by - smt + smt_show rfl diff --git a/Test/String/Lt.expected b/Test/String/Lt.expected index ea6444c4..b6d90c14 100644 --- a/Test/String/Lt.expected +++ b/Test/String/Lt.expected @@ -3,6 +3,3 @@ goal: "a" < "b" query: (assert (not (str.< "a" "b"))) (check-sat) - -result: unsat -failed to reconstruct proof: encountered error parsing cvc5 proof diff --git a/Test/String/Lt.lean b/Test/String/Lt.lean index c04bebc2..5fe304c6 100644 --- a/Test/String/Lt.lean +++ b/Test/String/Lt.lean @@ -1,5 +1,5 @@ import Smt theorem lt : "a" < "b" := by - smt + smt_show decide diff --git a/Test/String/Replace.expected b/Test/String/Replace.expected index d5486c8c..8024e65a 100644 --- a/Test/String/Replace.expected +++ b/Test/String/Replace.expected @@ -3,7 +3,4 @@ goal: String.replace "a" "a" "b" = "b" query: (assert (not (= (str.replace_all "a" "a" "b") "b"))) (check-sat) - -result: unsat -failed to reconstruct proof: encountered error parsing cvc5 proof Test/String/Replace.lean:3:8: warning: declaration uses 'sorry' diff --git a/Test/String/Replace.lean b/Test/String/Replace.lean index 6ec9e8cb..4446e15e 100644 --- a/Test/String/Replace.lean +++ b/Test/String/Replace.lean @@ -1,5 +1,5 @@ import Smt theorem replace : "a".replace "a" "b" = "b" := by - smt + smt_show admit diff --git a/lake-manifest.json b/lake-manifest.json index b70b399a..8f80a921 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -10,6 +10,15 @@ "inputRev": "v4.4.0", "inherited": true, "configFile": "lakefile.lean"}, + {"url": "https://github.com/abdoo8080/lean-cvc5.git", + "type": "git", + "subDir": null, + "rev": "6a5abce73167591e4b6a065034b11319cdad4474", + "name": "cvc5", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": false, + "configFile": "lakefile.lean"}, {"url": "https://github.com/leanprover-community/quote4", "type": "git", "subDir": null, diff --git a/lakefile.lean b/lakefile.lean index 7e32f97e..be74286b 100644 --- a/lakefile.lean +++ b/lakefile.lean @@ -2,12 +2,17 @@ import Lake open Lake DSL -package smt where - precompileModules := true +require cvc5 from git + "https://github.com/abdoo8080/lean-cvc5.git" @ "main" require mathlib from git "https://github.com/leanprover-community/mathlib4.git" @ "v4.4.0" +package smt where + precompileModules := true + moreLeanArgs := #[s!"--load-dynlib={nameToSharedLib "c++"}.1"] + moreGlobalServerArgs := #[s!"--load-dynlib={nameToSharedLib "c++"}.1"] + @[default_target] lean_lib Smt @@ -112,7 +117,7 @@ where | do IO.println s!"Error: Could not find `libSmt.so`"; return 2 let out ← IO.Process.output { cmd := (← getLean).toString - args := #[s!"--load-dynlib={dynlib}", test.toString] + args := #[s!"--load-dynlib={nameToSharedLib "c++"}.1", s!"--load-dynlib={dynlib}", test.toString] env := ← getAugmentedEnv } IO.FS.writeFile expected out.stdout