diff --git a/Smt/Attribute.lean b/Smt/Attribute.lean index 7b25e7d6..beaa40a4 100644 --- a/Smt/Attribute.lean +++ b/Smt/Attribute.lean @@ -15,12 +15,12 @@ open Std /-- An extension to Lean's runtime environment to support SMT attributes. Maintains a set of function declarations for the `smt` tactic to utilize while generating the SMT query. -/ -abbrev SmtExtension := SimpleScopedEnvExtension Name (HashSet Name) +abbrev SmtExtension := SimpleScopedEnvExtension (Name × Name) (HashMap Name (HashSet Name)) /-- Adds a declaration to the set of function declarations maintained by the SMT environment extension. -/ -def addSmtEntry (d : HashSet Name) (e : Name) : HashSet Name := - d.insert e +def addSmtEntry (d : HashMap Name (HashSet Name)) (e : (Name × Name)) := + d.insert e.fst ((d.findD e.fst {}).insert e.snd) initialize smtExt : SmtExtension ← registerSimpleScopedEnvExtension { name := `SmtExt @@ -33,18 +33,17 @@ def throwUnexpectedType (t : Name) (n : Name) : AttrM Unit := throwError s!"unexpected type at '{n}', `{t}` expected" /-- Validates the tagged declaration. -/ -def validate (n : Name) : AttrM Unit := do +def validate (n : Name) (t : Name) : AttrM Unit := do match (← getEnv).find? n with | none => throwError s!"unknown constant '{n}'" | some info => match info.type with - | Expr.const c .. => - if c != `Smt.Translator then throwUnexpectedType `Smt.Translator n - | _ => throwUnexpectedType `Smt.Translator n + | Expr.const c .. => if c != t then throwUnexpectedType t n + | _ => throwUnexpectedType t n /-- Registers an SMT attribute with the provided name and description and links it against `ext`. -/ -def registerSmtAttr (attrName : Name) (attrDescr : String) +def registerSmtAttr (attrName : Name) (typeName : Name) (attrDescr : String) : IO Unit := registerBuiltinAttribute { name := attrName @@ -54,17 +53,24 @@ def registerSmtAttr (attrName : Name) (attrDescr : String) trace[smt.debug.attr] s!"attrName: {attrName}, attrDescr: {attrDescr}" trace[smt.debug.attr] s!"decl: {decl}, stx: {stx}, attrKind: {attrKind}" Attribute.Builtin.ensureNoArgs stx - validate decl - setEnv (smtExt.addEntry (← getEnv) decl) - trace[smt.debug.attr] - s!"translators: {(smtExt.getState (← getEnv)).toList}" + validate decl typeName + setEnv (smtExt.addEntry (← getEnv) (typeName, decl)) erase := fun declName => do let s := smtExt.getState (← getEnv) let s := s.erase declName modifyEnv fun env => smtExt.modifyState env fun _ => s } -initialize registerSmtAttr `smt_translate +initialize registerSmtAttr `smt_translate `Smt.Translator "Utilize this function to translate Lean expressions to SMT terms." +initialize registerSmtAttr `smt_sort_reconstruct `Smt.SortReconstructor + "Utilize this function to translate cvc5 sorts to Lean expressions." + +initialize registerSmtAttr `smt_term_reconstruct `Smt.TermReconstructor + "Utilize this function to translate cvc5 terms to Lean expressions." + +initialize registerSmtAttr `smt_proof_reconstruct `Smt.ProofReconstructor + "Utilize this function to translate cvc5 proofs to Lean expressions." + end Smt.Attribute diff --git a/Smt/Reconstruct.lean b/Smt/Reconstruct.lean index 1f2ffee9..b746d724 100644 --- a/Smt/Reconstruct.lean +++ b/Smt/Reconstruct.lean @@ -5,13 +5,10 @@ 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.BitVec 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 -import Smt.Reconstruct.Util diff --git a/Smt/Reconstruct/Arith.lean b/Smt/Reconstruct/Arith.lean index 49b5f348..f1c507ba 100644 --- a/Smt/Reconstruct/Arith.lean +++ b/Smt/Reconstruct/Arith.lean @@ -5,13 +5,4 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Tomaz Gomes Mascarenhas -/ -import Smt.Reconstruct.Arith.ArithMulSign -import Smt.Reconstruct.Arith.MulPosNeg -import Smt.Reconstruct.Arith.Rewrites -import Smt.Reconstruct.Arith.SumBounds -import Smt.Reconstruct.Arith.TangentPlane -import Smt.Reconstruct.Arith.TightBounds -import Smt.Reconstruct.Arith.Trichotomy - --- Non-linear arithmetic is increasing compilation time too much --- import Smt.Reconstruct.Arith.TransFns +import Smt.Reconstruct.Arith.Reconstruct diff --git a/Smt/Reconstruct/Arith/ArithMulSign/Tactic.lean b/Smt/Reconstruct/Arith/ArithMulSign/Tactic.lean index d5f595f5..6ca0a739 100644 --- a/Smt/Reconstruct/Arith/ArithMulSign/Tactic.lean +++ b/Smt/Reconstruct/Arith/ArithMulSign/Tactic.lean @@ -11,7 +11,6 @@ import Mathlib.Data.Nat.Parity import Mathlib.Data.Real.Basic import Smt.Reconstruct.Arith.ArithMulSign.Lemmas -import Smt.Reconstruct.Arith.MulPosNeg.Instances import Smt.Reconstruct.Util namespace Smt.Reconstruct.Arith @@ -24,6 +23,11 @@ inductive Pol where | Pos : Pol -- 2 deriving BEq +def intLOR := mkApp2 (.const ``LinearOrderedCommRing.toLinearOrderedRing [.zero]) + (.const ``Int []) (.const ``Int.linearOrderedCommRing []) + +def RealLOR := Expr.const ``Real.instLinearOrderedRingReal [] + def mulSign (mv : MVarId) (xs : Array (Expr × Fin 3 × Nat)) : MetaM Unit := do mv.assignIfDefeq (← go true xs.toList (mkConst `empty) (mkConst `empty)) where @@ -37,8 +41,7 @@ where | .const `Rat .. => pure false | .const `Int .. => pure true | _ => throwError "[arithMulSign]: unexpected type for expression" - let lorInst := mkConst $ - if exprIsInt then ``lorInt else ``lorReal + let lorInst := if exprIsInt then intLOR else RealLOR let zeroI := mkApp (mkConst ``Int.ofNat) (mkNatLit 0) let zeroR := mkApp (mkConst ``Rat.ofInt) zeroI -- zero with the same type as the current argument @@ -170,8 +173,7 @@ where | .const `Real .. => pure false | .const `Int .. => pure true | _ => throwError "[arithMulSign]: unexpected type for expression" - let lorInst := mkConst $ - if exprIsInt then ``lorInt else ``lorReal + let lorInst := if exprIsInt then intLOR else RealLOR let zeroI := mkApp (mkConst ``Int.ofNat) (mkNatLit 0) let zeroR ← mkAppOptM' (.const ``OfNat.ofNat [.zero]) #[mkConst ``Real, (mkNatLit 0), none] -- zero with the same type as the current argument diff --git a/Smt/Reconstruct/Arith/MulPosNeg.lean b/Smt/Reconstruct/Arith/MulPosNeg.lean index 87ea729e..d3452cbf 100644 --- a/Smt/Reconstruct/Arith/MulPosNeg.lean +++ b/Smt/Reconstruct/Arith/MulPosNeg.lean @@ -10,6 +10,5 @@ Authors: Tomaz Gomes Mascarenhas -- and -- https://cvc5.github.io/docs/cvc5-1.0.2/proofs/proof_rules.html#_CPPv4N4cvc58internal6PfRule14ARITH_MULT_NEGE -import Smt.Reconstruct.Arith.MulPosNeg.Instances import Smt.Reconstruct.Arith.MulPosNeg.Lemmas import Smt.Reconstruct.Arith.MulPosNeg.Tactic diff --git a/Smt/Reconstruct/Arith/MulPosNeg/Lemmas.lean b/Smt/Reconstruct/Arith/MulPosNeg/Lemmas.lean index ef4af79d..497dbfde 100644 --- a/Smt/Reconstruct/Arith/MulPosNeg/Lemmas.lean +++ b/Smt/Reconstruct/Arith/MulPosNeg/Lemmas.lean @@ -9,8 +9,6 @@ import Mathlib.Data.Real.Basic namespace Smt.Reconstruct.Arith -noncomputable instance : LinearOrderedRing Real := inferInstance - variable {α : Type} variable [LinearOrderedRing α] diff --git a/Smt/Reconstruct/Arith/MulPosNeg/Tactic.lean b/Smt/Reconstruct/Arith/MulPosNeg/Tactic.lean index bdce9cc1..a6af2153 100644 --- a/Smt/Reconstruct/Arith/MulPosNeg/Tactic.lean +++ b/Smt/Reconstruct/Arith/MulPosNeg/Tactic.lean @@ -14,8 +14,6 @@ import Smt.Reconstruct.Util namespace Smt.Reconstruct.Arith -noncomputable instance : LinearOrderedRing Real := inferInstance - open Lean open Elab Tactic Expr Meta diff --git a/Smt/Reconstruct/Arith/Reconstruct.lean b/Smt/Reconstruct/Arith/Reconstruct.lean new file mode 100644 index 00000000..0c98c14e --- /dev/null +++ b/Smt/Reconstruct/Arith/Reconstruct.lean @@ -0,0 +1,140 @@ +/- +Copyright (c) 2021-2023 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 Smt.Reconstruct.Arith.ArithMulSign +import Smt.Reconstruct.Arith.MulPosNeg +import Smt.Reconstruct.Arith.Rewrites +import Smt.Reconstruct.Arith.SumBounds +import Smt.Reconstruct.Arith.Rewrites +import Smt.Reconstruct.Arith.TangentPlane +import Smt.Reconstruct.Arith.TightBounds +import Smt.Reconstruct.Arith.Trichotomy +import Smt.Reconstruct.Reconstruct + +namespace Smt.Reconstruct.Arith + +open Lean hiding Rat +open Qq + +@[smt_sort_reconstruct] def reconstructArithSort : SortReconstructor := fun s => do match s.getKind with + | .INTEGER_SORT => return q(Int) + | .REAL_SORT => return q(Real) + | _ => return none + +def getTypeAndInst (s : cvc5.Sort) : Σ α : Q(Type), Q(LinearOrderedRing $α) := match s.isInteger with + | false => ⟨q(Real), q(Real.instLinearOrderedRingReal)⟩ + | true => ⟨q(Int), q(Int.linearOrderedCommRing.toLinearOrderedRing)⟩ + +@[smt_term_reconstruct] def reconstructUF : TermReconstructor := fun t => do match t.getKind with + | .SKOLEM_FUN => match t.getSkolemId with + | .DIV_BY_ZERO => return q(fun (x : Real) => x / 0) + | .INT_DIV_BY_ZERO => return q(fun (x : Int) => x / 0) + | .MOD_BY_ZERO => return q(fun (x : Int) => x % 0) + | _ => return none + | .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 : Q(Real) := mkRealLit x.num.natAbs + if x.den == 1 then + if x.num ≥ 0 then + return q($num) + else + return q(-$num) + else + let den : Q(Real) := mkRealLit x.den + if x.num ≥ 0 then + return q($num / $den) + else + return q(-$num / $den) + | .NEG => + let ⟨α, _⟩ := getTypeAndInst t.getSort + let x : Q($α) ← reconstructTerm t[0]! + return q(-$x) + | .SUB => + let ⟨α, _⟩ := getTypeAndInst t.getSort + let x : Q($α) ← reconstructTerm t[0]! + let y : Q($α) ← reconstructTerm t[1]! + return q($x - $y) + | .ADD => + let ⟨α, _⟩ := getTypeAndInst t.getSort + let x : Q($α) ← reconstructTerm t[0]! + let y : Q($α) ← reconstructTerm t[1]! + return q($x + $y) + | .MULT => + let ⟨α, _⟩ := getTypeAndInst t.getSort + let x : Q($α) ← reconstructTerm t[0]! + let y : Q($α) ← reconstructTerm t[1]! + return q($x * $y) + | .INTS_DIVISION => + let x : Q(Int) ← reconstructTerm t[0]! + let y : Q(Int) ← reconstructTerm t[1]! + return q($x / $y) + | .INTS_MODULUS => + let x : Q(Int) ← reconstructTerm t[0]! + let y : Q(Int) ← reconstructTerm t[1]! + return q($x % $y) + | .DIVISION => + let x : Q(Real) ← reconstructTerm t[0]! + let y : Q(Real) ← reconstructTerm t[1]! + return q($x / $y) + | .ABS => + let x : Q(Int) ← reconstructTerm t[0]! + return q(Int.natAbs $x : Int) + | .LEQ => + let ⟨α, _⟩ := getTypeAndInst t[0]!.getSort + let x : Q($α) ← reconstructTerm t[0]! + let y : Q($α) ← reconstructTerm t[1]! + return q($x ≤ $y) + | .LT => + let ⟨α, _⟩ := getTypeAndInst t[0]!.getSort + let x : Q($α) ← reconstructTerm t[0]! + let y : Q($α) ← reconstructTerm t[1]! + return q($x < $y) + | .GEQ => + let ⟨α, _⟩ := getTypeAndInst t[0]!.getSort + let x : Q($α) ← reconstructTerm t[0]! + let y : Q($α) ← reconstructTerm t[1]! + return q($x ≥ $y) + | .GT => + let ⟨α, _⟩ := getTypeAndInst t[0]!.getSort + let x : Q($α) ← reconstructTerm t[0]! + let y : Q($α) ← reconstructTerm t[1]! + return q($x > $y) + | .TO_REAL => + let x : Q(Int) ← reconstructTerm t[0]! + return q($x : Real) + | .TO_INTEGER => + let x : Q(Real) ← reconstructTerm t[0]! + return q(⌊$x⌋) + | .IS_INTEGER => + let x : Q(Real) ← reconstructTerm t[0]! + return q($x = ⌊$x⌋) + | _ => return none +where + mkRealLit (n : Nat) : Q(Real) := match h : n with + | 0 => q(0 : Real) + | 1 => q(1 : Real) + | _ + 2 => + let h : Q(Nat.AtLeastTwo $n) := h ▸ q(instNatAtLeastTwo) + let h := mkApp3 q(@instOfNat Real) (mkRawNatLit n) q(Real.natCast) h + mkApp2 q(@OfNat.ofNat Real) (mkRawNatLit n) h + +def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do + match cvc5.RewriteRule.fromNat! pf.getArguments[0]!.getIntegerValue.toNat with + | _ => return none + +@[smt_proof_reconstruct] def reconstructArithProof : ProofReconstructor := fun pf => do match pf.getRule with + | .DSL_REWRITE => reconstructRewrite pf + | _ => return none + +end Smt.Reconstruct.Arith diff --git a/Smt/Reconstruct/Arith/Rewrites.lean b/Smt/Reconstruct/Arith/Rewrites.lean index 73447299..78c6f9f3 100644 --- a/Smt/Reconstruct/Arith/Rewrites.lean +++ b/Smt/Reconstruct/Arith/Rewrites.lean @@ -13,16 +13,16 @@ namespace Smt.Reconstruct.Arith open Function -variable {α : Type} [LinearOrderedRing α] +variable {α : Type} [h : LinearOrderedRing α] -variable {xs w ys zs t x s r : α} +variable {t ts x xs : α} -theorem arith_plus_zero : t + 0 + s = t + s := - (add_zero t).symm ▸ rfl -theorem arith_mul_one : t * 1 * s = t * s := - (mul_one t).symm ▸ rfl -theorem arith_mul_zero : t * 0 * s = 0 := - (mul_zero t).symm ▸ (zero_mul s).symm ▸ rfl +theorem arith_plus_zero : ts + 0 + ss = ts + ss := + (add_zero ts).symm ▸ rfl +theorem arith_mul_one : ts * 1 * ss = ts * ss := + (mul_one ts).symm ▸ rfl +theorem arith_mul_zero : ts * 0 * ss = 0 := + (mul_zero ts).symm ▸ (zero_mul ss).symm ▸ rfl theorem arith_int_div_one {t : Int} : t / 1 = t := Int.ediv_one t @@ -43,7 +43,7 @@ theorem arith_elim_lt : (t < s) = ¬(t ≥ s) := theorem arith_elim_leq : (t ≤ s) = (s ≥ t) := propext ge_iff_le -theorem arith_leq_norm {t s : Int}: (t ≤ s) = ¬(t ≥ s + 1) := +theorem arith_leq_norm {t s : Int} : (t ≤ s) = ¬(t ≥ s + 1) := propext ⟨(propext Int.not_le ▸ Int.lt_add_one_of_le ·), (Int.le_of_lt_add_one $ propext Int.not_le ▸ · )⟩ @@ -68,15 +68,15 @@ theorem arith_plus_flatten : xs + (w + ys) + zs = xs + w + ys + zs := theorem arith_mult_flatten : xs * (w * ys) * zs = xs * w * ys * zs := mul_assoc xs w ys ▸ rfl -theorem arith_mult_dist : x * (y + z + w) = x * y + x * (z + w) := - add_assoc y z w ▸ mul_add x y (z + w) ▸ rfl +theorem arith_mult_dist : x * (y + z + ws) = x * y + x * (z + ws) := + add_assoc y z ws ▸ mul_add x y (z + ws) ▸ rfl -theorem arith_plus_cancel1 : t + x + s + (-1 * x) + r = t + s + r := - neg_eq_neg_one_mul x ▸ add_assoc t x s ▸ add_assoc t (x + s) (-x) ▸ - add_comm x s ▸ (add_neg_cancel_right s x).symm ▸ rfl +theorem arith_plus_cancel1 : ts + x + ss + (-1 * x) + rs = ts + ss + rs := + neg_eq_neg_one_mul x ▸ add_assoc ts x ss ▸ add_assoc ts (x + ss) (-x) ▸ + add_comm x ss ▸ (add_neg_cancel_right ss x).symm ▸ rfl -theorem arith_plus_cancel2 : t + (-1 * x) + s + x + r = t + s + r := - neg_eq_neg_one_mul x ▸ add_assoc t (-x) s ▸ add_assoc t (-x + s) x ▸ - add_comm (-x) s ▸ (neg_add_cancel_right s x).symm ▸ rfl +theorem arith_plus_cancel2 : ts + (-1 * x) + ss + x + rs = ts + ss + rs := + neg_eq_neg_one_mul x ▸ add_assoc ts (-x) ss ▸ add_assoc ts (-x + ss) x ▸ + add_comm (-x) ss ▸ (neg_add_cancel_right ss x).symm ▸ rfl end Smt.Reconstruct.Arith diff --git a/Smt/Reconstruct/Arith/SumBounds.lean b/Smt/Reconstruct/Arith/SumBounds.lean index d66e2cd5..ff878d3d 100644 --- a/Smt/Reconstruct/Arith/SumBounds.lean +++ b/Smt/Reconstruct/Arith/SumBounds.lean @@ -5,6 +5,5 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Tomaz Gomes Mascarenhas -/ -import Smt.Reconstruct.Arith.SumBounds.Instances import Smt.Reconstruct.Arith.SumBounds.Lemmas import Smt.Reconstruct.Arith.SumBounds.Tactic diff --git a/Smt/Reconstruct/Arith/SumBounds/Lemmas.lean b/Smt/Reconstruct/Arith/SumBounds/Lemmas.lean index 4e0bb2b1..00a0be1f 100644 --- a/Smt/Reconstruct/Arith/SumBounds/Lemmas.lean +++ b/Smt/Reconstruct/Arith/SumBounds/Lemmas.lean @@ -5,21 +5,13 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Tomaz Gomes Mascarenhas -/ -import Mathlib.Algebra.Order.Monoid.Lemmas -- add_lt_add -import Mathlib.Init.Function -- swap +import Mathlib.Algebra.Order.Ring.Defs namespace Smt.Reconstruct.Arith open Function -variable {α : Type} - -variable [Preorder α] -variable [Add α] -variable [CovariantClass α α (· + ·) (· < ·)] -variable [CovariantClass α α (· + ·) (· ≤ ·)] -variable [CovariantClass α α (swap (· + ·)) (· < ·)] -variable [CovariantClass α α (swap (· + ·)) (· ≤ ·)] +variable {α : Type} [LinearOrderedRing α] variable {a b c d : α} diff --git a/Smt/Reconstruct/Arith/TightBounds/Lemmas.lean b/Smt/Reconstruct/Arith/TightBounds/Lemmas.lean index 38afe1f3..e2cdde02 100644 --- a/Smt/Reconstruct/Arith/TightBounds/Lemmas.lean +++ b/Smt/Reconstruct/Arith/TightBounds/Lemmas.lean @@ -11,29 +11,33 @@ import Smt.Reconstruct.Arith.MulPosNeg.Lemmas namespace Smt.Reconstruct.Arith -theorem Real.neg_lt_neg {a b : ℝ} (h : a < b) : -a > -b := by +variable {α : Type} [LinearOrderedRing α] [FloorRing α] + +theorem Real.neg_lt_neg {a b : α} (h : a < b) : -a > -b := by simp exact h -theorem Real.neg_le_neg {a b : ℝ} (h : a ≤ b) : -a ≥ -b := by +theorem Real.neg_le_neg {a b : α} (h : a ≤ b) : -a ≥ -b := by simp exact h -theorem intTightLb' : ∀ {i : Int} {c : ℝ}, i > c → i ≥ ⌊c⌋ + 1 := by +theorem castLE' : ∀ {a b : Int}, a ≤ b → (a : α) ≤ b := by simp + +theorem intTightLb' : ∀ {i : Int} {c : α}, i > c → i ≥ ⌊c⌋ + 1 := by intros i c h cases lt_trichotomy i (⌊c⌋ + 1) with | inl iltc => have ilec := (Int.lt_iff_add_one_le i (⌊c⌋ + 1)).mp iltc simp at ilec have c_le_floor := Int.floor_le c - have cast_ilec := le_trans (castLE ilec) c_le_floor + have cast_ilec := le_trans (castLE' ilec) c_le_floor have abs := lt_of_le_of_lt cast_ilec h simp at abs | inr h' => cases h' with | inl ieqc => exact le_of_eq (Eq.symm ieqc) | inr igtc => exact le_of_lt igtc -theorem intTightUb' : ∀ {i : Int} {c : ℝ}, i < c → i ≤ ⌈c⌉ - 1 := by +theorem intTightUb' : ∀ {i : Int} {c : α}, i < c → i ≤ ⌈c⌉ - 1 := by intros i c h have neg_c_lt_neg_i := Real.neg_lt_neg h have i_le_floor_neg_c: -i ≥ ⌊-c⌋ + 1 := by diff --git a/Smt/Reconstruct/BitVec.lean b/Smt/Reconstruct/BitVec.lean new file mode 100644 index 00000000..b047c96c --- /dev/null +++ b/Smt/Reconstruct/BitVec.lean @@ -0,0 +1,8 @@ +/- +Copyright (c) 2021-2023 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 Smt.Reconstruct.BitVec.Reconstruct diff --git a/Smt/Reconstruct/BitVec/Reconstruct.lean b/Smt/Reconstruct/BitVec/Reconstruct.lean new file mode 100644 index 00000000..0f1d116f --- /dev/null +++ b/Smt/Reconstruct/BitVec/Reconstruct.lean @@ -0,0 +1,103 @@ +/- +Copyright (c) 2021-2023 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 Smt.Reconstruct.Prop.Core +import Smt.Reconstruct.Reconstruct + +namespace Smt.Reconstruct.BitVec + +open Lean Qq + +@[smt_sort_reconstruct] def reconstructBitVecSort : SortReconstructor := fun s => do match s.getKind with + | .BITVECTOR_SORT => + let w : Nat := s.getBitVectorSize.val + return q(Std.BitVec $w) + | _ => return none + +@[smt_term_reconstruct] partial def reconstructBitVec : TermReconstructor := fun t => do match t.getKind with + | .CONST_BITVECTOR => + let w : Nat := t.getSort.getBitVectorSize.val + let v : Nat := (t.getBitVectorValue 10).toNat! + return q(Std.BitVec.ofNat $w $v) + | .BITVECTOR_BITOF => + let w : Nat := t[0]!.getSort.getBitVectorSize.val + let x : Q(Std.BitVec $w) ← reconstructTerm t[0]! + let i : Nat := t.getOp[0]!.getIntegerValue.toNat + return q(«$x».getLsb $i = true) + | .BITVECTOR_BB_TERM => + let w : Nat := t.getNumChildren + let bs : Q(Std.BitVec 0) := q(.nil) + let f (bs : Expr) (i : Nat) : ReconstructM Expr := do + let p : Q(Prop) ← reconstructTerm t[i]! + let bs : Q(Std.BitVec $i) := bs + let hp : Q(Decidable $p) ← synthDecidableInst t[i]! + return q(@Std.BitVec.cons $i (@decide $p $hp) $bs) + let bs : Q(Std.BitVec $w) ← (List.range w).foldlM f bs + return q($bs) + | .BITVECTOR_ADD => + let w : Nat := t.getSort.getBitVectorSize.val + let x : Q(Std.BitVec $w) ← reconstructTerm t[0]! + let y : Q(Std.BitVec $w) ← reconstructTerm t[1]! + return q($x + $y) + | _ => return none +where + rightAssocOpDecidableInst (op : Expr) (inst : Expr) (t : cvc5.Term) : ReconstructM Expr := do + let mut curr ← reconstructTerm t[t.getNumChildren - 1]! + let mut currInst ← synthDecidableInst t[t.getNumChildren - 1]! + for i in [1:t.getNumChildren] do + let ct := t[t.getNumChildren - i - 1]! + currInst := mkApp4 inst (← reconstructTerm ct) curr (← synthDecidableInst ct) currInst + curr := mkApp2 op (← reconstructTerm ct) curr + return currInst + synthDecidableInst (t : cvc5.Term) : ReconstructM Expr := do match t.getKind with + | .CONST_BOOLEAN => return if t.getBooleanValue then q(instDecidableTrue) else q(instDecidableFalse) + | .NOT => + let p : Q(Prop) ← reconstructTerm t[0]! + let hp : Q(Decidable $p) ← synthDecidableInst t[0]! + return q(@instDecidableNot $p $hp) + | .AND => rightAssocOpDecidableInst q(And) q(@instDecidableAnd) t + | .OR => rightAssocOpDecidableInst q(Or) q(@instDecidableOr) t + | .XOR => rightAssocOpDecidableInst q(XOr) q(@XOr.instDecidableXOr) t + | .EQUAL => + if t[0]!.getSort.getKind == .BOOLEAN_SORT then + let p : Q(Prop) ← reconstructTerm t[0]! + let q : Q(Prop) ← reconstructTerm t[1]! + let hp : Q(Decidable $p) ← synthDecidableInst t[0]! + let hq : Q(Decidable $q) ← synthDecidableInst t[1]! + return q(@instDecidableEqProp $p $q (@instDecidableIff $p $q $hp $hq)) + if t[0]!.getSort.getKind == .BITVECTOR_SORT then + let w : Nat := t[0]!.getSort.getBitVectorSize.val + return q(@Std.instDecidableEqBitVec $w) + let p : Q(Prop) ← reconstructTerm t + Meta.synthInstance q(Decidable $p) + | .BITVECTOR_BITOF => + let w : Nat := t[0]!.getSort.getBitVectorSize.val + let x : Q(Std.BitVec $w) ← reconstructTerm t[0]! + let i : Nat := t.getOp[0]!.getIntegerValue.toNat + return q(instDecidableEqBool («$x».getLsb $i) true) + | _ => + let p : Q(Prop) ← reconstructTerm t + Meta.synthInstance q(Decidable $p) + +def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do + match cvc5.RewriteRule.fromNat! pf.getArguments[0]!.getIntegerValue.toNat with + | _ => return none + +@[smt_proof_reconstruct] def reconstructBitVecProof : ProofReconstructor := fun pf => do match pf.getRule with + | .DSL_REWRITE => reconstructRewrite pf + | .BV_BITBLAST_STEP => + let t := pf.getArguments[0]![0]! + match t.getKind with + | .CONST_BITVECTOR => + let w : Nat := t.getSort.getBitVectorSize.toNat + let t : Q(Std.BitVec $w) ← reconstructTerm pf.getResult[0]! + let t' : Q(Std.BitVec $w) ← reconstructTerm pf.getResult[1]! + addThm q($t = $t') q(Eq.refl $t) + | _ => return none + | _ => return none + +end Smt.Reconstruct.BitVec diff --git a/Smt/Reconstruct/Builtin.lean b/Smt/Reconstruct/Builtin.lean index da1d8b45..44d7ef1b 100644 --- a/Smt/Reconstruct/Builtin.lean +++ b/Smt/Reconstruct/Builtin.lean @@ -5,4 +5,4 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Abdalrhman Mohamed -/ -import Smt.Reconstruct.Builtin.Rewrites +import Smt.Reconstruct.Builtin.Reconstruct diff --git a/Smt/Reconstruct/Builtin/Lemmas.lean b/Smt/Reconstruct/Builtin/Lemmas.lean new file mode 100644 index 00000000..59455584 --- /dev/null +++ b/Smt/Reconstruct/Builtin/Lemmas.lean @@ -0,0 +1,108 @@ +/- +Copyright (c) 2021-2023 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 Smt.Reconstruct.Util + +namespace Smt.Reconstruct.Builtin + +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 orImplies : ∀ {p q : Prop}, (¬ p → q) → p ∨ q := + by intros p q h + exact match Classical.em p with + | Or.inl pp => Or.inl pp + | Or.inr npp => match Classical.em q with + | Or.inl pq => Or.inr pq + | Or.inr npq => False.elim (npq (h npp)) + +theorem notNotElim : ∀ {p : Prop}, ¬ ¬ p → p := + by intros p h + exact match Classical.em p with + | Or.inl pp => pp + | Or.inr np => False.elim (h (λ p => np p)) + +theorem cnfItePos1 [h : Decidable c] : ¬ (ite c a b) ∨ ¬ c ∨ a := by + apply orImplies + intro hite + have hite' := notNotElim hite + match h with + | isTrue _ => exact Or.inr hite' + | isFalse hnc => exact Or.inl hnc + +theorem cnfItePos2 [h : Decidable c] : ¬ (ite c a b) ∨ c ∨ b := by + apply orImplies + intro hite + have hite' := notNotElim hite + match h with + | isFalse _ => exact Or.inr hite' + | isTrue hc => exact Or.inl hc + +theorem cnfItePos3 [h : Decidable c] : ¬ (ite c a b) ∨ a ∨ b := by + apply orImplies + intro hite + have hite' := notNotElim hite + 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 h with + | isTrue _ => exact Or.inr hnite + | isFalse hnc => exact Or.inl hnc + +theorem cnfIteNeg2 [h : Decidable c] : (ite c a b) ∨ c ∨ ¬ b := by + apply orImplies + intro hnite + match h with + | isFalse _ => exact Or.inr hnite + | isTrue hc => exact Or.inl hc + +theorem cnfIteNeg3 [h : Decidable c] : (ite c a b) ∨ ¬ a ∨ ¬ b := by + apply orImplies + intro hnite + match h with + | isFalse _ => exact Or.inr hnite + | isTrue _ => exact Or.inl hnite + +theorem scopes : ∀ {ps : List Prop} {q : Prop}, impliesN ps q → andN ps → q := + by intros ps q h + match ps with + | [] => intro; exact h + | [p] => unfold andN + unfold impliesN at h + exact h + | p₁::p₂::ps => unfold andN + unfold impliesN at h + intro ⟨hp₁, hps⟩ + revert hps + exact scopes (h hp₁) + +end Smt.Reconstruct.Builtin diff --git a/Smt/Reconstruct/Builtin/Reconstruct.lean b/Smt/Reconstruct/Builtin/Reconstruct.lean new file mode 100644 index 00000000..01b282d4 --- /dev/null +++ b/Smt/Reconstruct/Builtin/Reconstruct.lean @@ -0,0 +1,215 @@ +/- +Copyright (c) 2021-2023 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 Smt.Reconstruct.Builtin.Lemmas +import Smt.Reconstruct.Builtin.Rewrites +import Smt.Reconstruct.Reconstruct + +namespace Smt.Reconstruct.Builtin + +open Lean Qq + +def getFVarExpr! (n : Name) : MetaM Expr := do + match (← getLCtx).findFromUserName? n with + | some d => return d.toExpr + | none => throwError "unknown free variable '{n}'" + +def getFVarOrConstExpr! (n : Name) : MetaM Expr := do + match (← getLCtx).findFromUserName? n with + | some d => return d.toExpr + | none => + let c ← getConstInfo n + return .const c.name (c.numLevelParams.repeat (.zero :: ·) []) + +@[smt_term_reconstruct] def reconstructBuiltin : TermReconstructor := fun t => do match t.getKind with + | .VARIABLE => getFVarExpr! (getVariableName t) + | .CONSTANT => getFVarOrConstExpr! t.getSymbol + | .ITE => + let α : Q(Type) ← reconstructSort t.getSort + let c : Q(Prop) ← reconstructTerm t[0]! + let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c) + let x : Q($α) ← reconstructTerm t[1]! + let y : Q($α) ← reconstructTerm t[2]! + return q(@ite $α $c $h $x $y) + | .SKOLEM_FUN => match t.getSkolemId with + | .PURIFY => reconstructTerm t.getSkolemArguments[0]! + | _ => return none + | _ => return none +where + getVariableName (t : cvc5.Term) : Name := + if t.hasSymbol then t.getSymbol else Name.num `x t.getId + +def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do + match cvc5.RewriteRule.fromNat! pf.getArguments[0]!.getIntegerValue.toNat with + | .ITE_TRUE_COND => + let α : Q(Type) ← reconstructSort pf.getArguments[1]!.getSort + let x : Q($α) ← reconstructTerm pf.getArguments[1]! + let y : Q($α) ← reconstructTerm pf.getArguments[2]! + addThm q(ite True $x $y = $x) q(@Builtin.ite_true_cond $α $x $y) + | .ITE_FALSE_COND => + let α : Q(Type) ← reconstructSort pf.getArguments[1]!.getSort + let x : Q($α) ← reconstructTerm pf.getArguments[1]! + let y : Q($α) ← reconstructTerm pf.getArguments[2]! + addThm q(ite False $x $y = $y) q(@Builtin.ite_false_cond $α $x $y) + | .ITE_NOT_COND => + let c : Q(Prop) ← reconstructTerm pf.getArguments[1]! + let α : Q(Type) ← reconstructSort pf.getArguments[2]!.getSort + let x : Q($α) ← reconstructTerm pf.getArguments[2]! + let y : Q($α) ← reconstructTerm 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) ← reconstructTerm pf.getArguments[1]! + let α : Q(Type) ← reconstructSort pf.getArguments[2]!.getSort + let x : Q($α) ← reconstructTerm 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) ← reconstructTerm pf.getArguments[1]! + let α : Q(Type) ← reconstructSort pf.getArguments[2]!.getSort + let x : Q($α) ← reconstructTerm pf.getArguments[2]! + let y : Q($α) ← reconstructTerm pf.getArguments[3]! + let z : Q($α) ← reconstructTerm 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) ← reconstructTerm pf.getArguments[1]! + let α : Q(Type) ← reconstructSort pf.getArguments[2]!.getSort + let x : Q($α) ← reconstructTerm pf.getArguments[2]! + let y : Q($α) ← reconstructTerm pf.getArguments[3]! + let z : Q($α) ← reconstructTerm 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) ← reconstructTerm pf.getArguments[1]! + let α : Q(Type) ← reconstructSort pf.getArguments[2]!.getSort + let x : Q($α) ← reconstructTerm pf.getArguments[2]! + let y : Q($α) ← reconstructTerm pf.getArguments[3]! + let z : Q($α) ← reconstructTerm 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) ← reconstructTerm pf.getArguments[1]! + let α : Q(Type) ← reconstructSort pf.getArguments[2]!.getSort + let x : Q($α) ← reconstructTerm pf.getArguments[2]! + let y : Q($α) ← reconstructTerm pf.getArguments[3]! + let z : Q($α) ← reconstructTerm 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) + | _ => return none + +@[smt_proof_reconstruct] def reconstructBuiltinProof : ProofReconstructor := fun pf => do match pf.getRule with + | .ASSUME => + let p : Q(Prop) ← reconstructTerm pf.getArguments[0]! + match (← Meta.findLocalDeclWithType? p) with + | none => throwError "no assumption of type\n\t{p}\nfound in local context" + | some fv => return Expr.fvar fv + | .SCOPE => + let mv ← getCurrGoal + mv.withContext do + let f := fun arg ps => do + let p : Q(Prop) ← reconstructTerm 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) ← reconstructTerm 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) (reconstructProof pf.getChildren[0]!) + let mv'' ← getCurrGoal + mv''.withContext (mv''.assignIfDefeq h₂) + setCurrGoal mv + addThm q(andN $ps → $q) q(Builtin.scopes $h₁) + | .EVALUATE => + let α : Q(Type) ← reconstructSort pf.getResult[0]!.getSort + if (← reconstructTerm pf.getResult).getUsedConstants.any (isNoncomputable (← getEnv)) then + return none + -- TODO: handle case where a Prop is inside an expression + if α.isProp then + let p : Q(Prop) ← reconstructTerm pf.getResult[0]! + let p' : Q(Prop) ← reconstructTerm pf.getResult[1]! + let h : Q(Decidable ($p = $p')) ← Meta.synthInstance q(Decidable ($p = $p')) + addThm q($p = $p') (.app q(@of_decide_eq_true ($p = $p') $h) q(Eq.refl true)) + else + let t : Q($α) ← reconstructTerm pf.getResult[0]! + let t' : Q($α) ← reconstructTerm pf.getResult[1]! + addThm q($t = $t') q(Eq.refl $t) + | .DSL_REWRITE => reconstructRewrite pf + | .ITE_ELIM1 => + let c : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult[0]! + let hc : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c) + let p : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult[1]! + let q : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult[2]! + let h : Q(@ite Prop $c $hc $p $q) ← reconstructProof pf.getChildren[0]! + addThm q(¬$c ∨ $p) q(Builtin.iteElim1 $h) + | .ITE_ELIM2 => + let c : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult[0]! + let hc : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c) + let p : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult[1]! + let q : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult[2]! + let h : Q(@ite Prop $c $hc $p $q) ← reconstructProof pf.getChildren[0]! + addThm q($c ∨ $q) q(Builtin.iteElim2 $h) + | .NOT_ITE_ELIM1 => + let c : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult[0]![0]! + let hc : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c) + let p : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult[0]![1]! + let q : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult[0]![2]! + let hn : Q(¬@ite Prop $c $hc $p $q) ← reconstructProof pf.getChildren[0]! + addThm q(¬$c ∨ ¬$p) q(Builtin.notIteElim1 $hn) + | .NOT_ITE_ELIM2 => + let c : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult[0]![0]! + let hc : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c) + let p : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult[0]![1]! + let q : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult[0]![2]! + let hn : Q(¬@ite Prop $c $hc $p $q) ← reconstructProof pf.getChildren[0]! + addThm q($c ∨ ¬$q) q(Builtin.notIteElim2 $hn) + | .CNF_ITE_POS1 => + let c : Q(Prop) ← reconstructTerm pf.getArguments[0]![0]! + let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c) + let p : Q(Prop) ← reconstructTerm pf.getArguments[0]![1]! + let q : Q(Prop) ← reconstructTerm pf.getArguments[0]![2]! + addThm q(¬(ite $c $p $q) ∨ ¬$c ∨ $p) q(@Builtin.cnfItePos1 $c $p $q $h) + | .CNF_ITE_POS2 => + let c : Q(Prop) ← reconstructTerm pf.getArguments[0]![0]! + let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c) + let p : Q(Prop) ← reconstructTerm pf.getArguments[0]![1]! + let q : Q(Prop) ← reconstructTerm pf.getArguments[0]![2]! + addThm q(¬(ite $c $p $q) ∨ $c ∨ $q) q(@Builtin.cnfItePos2 $c $p $q $h) + | .CNF_ITE_POS3 => + let c : Q(Prop) ← reconstructTerm pf.getArguments[0]![0]! + let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c) + let p : Q(Prop) ← reconstructTerm pf.getArguments[0]![1]! + let q : Q(Prop) ← reconstructTerm pf.getArguments[0]![2]! + addThm q(¬(ite $c $p $q) ∨ $p ∨ $q) q(@Builtin.cnfItePos3 $c $p $q $h) + | .CNF_ITE_NEG1 => + let c : Q(Prop) ← reconstructTerm pf.getArguments[0]![0]! + let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c) + let p : Q(Prop) ← reconstructTerm pf.getArguments[0]![1]! + let q : Q(Prop) ← reconstructTerm pf.getArguments[0]![2]! + addThm q(ite $c $p $q ∨ ¬$c ∨ ¬$p) q(@Builtin.cnfIteNeg1 $c $p $q $h) + | .CNF_ITE_NEG2 => + let c : Q(Prop) ← reconstructTerm pf.getArguments[0]![0]! + let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c) + let p : Q(Prop) ← reconstructTerm pf.getArguments[0]![1]! + let q : Q(Prop) ← reconstructTerm pf.getArguments[0]![2]! + addThm q(ite $c $p $q ∨ $c ∨ ¬$q) q(@Builtin.cnfIteNeg2 $c $p $q $h) + | .CNF_ITE_NEG3 => + let c : Q(Prop) ← reconstructTerm pf.getArguments[0]![0]! + let h : Q(Decidable $c) ← Meta.synthInstance q(Decidable $c) + let p : Q(Prop) ← reconstructTerm pf.getArguments[0]![1]! + let q : Q(Prop) ← reconstructTerm pf.getArguments[0]![2]! + addThm q(ite $c $p $q ∨ ¬$p ∨ ¬$q) q(@Builtin.cnfIteNeg3 $c $p $q $h) + | .SKOLEM_INTRO => + let α : Q(Type) ← reconstructSort pf.getResult[0]!.getSort + let k : Q($α) ← reconstructTerm pf.getResult[0]! + let t : Q($α) ← reconstructTerm pf.getResult[1]! + addThm q($k = $t) q(Eq.refl $t) + | _ => return none + +end Smt.Reconstruct.Builtin diff --git a/Smt/Reconstruct/Options.lean b/Smt/Reconstruct/Options.lean index 5a56ce9d..f20e7138 100644 --- a/Smt/Reconstruct/Options.lean +++ b/Smt/Reconstruct/Options.lean @@ -13,6 +13,9 @@ open Lean initialize registerTraceClass `smt.profile.reconstruct + registerTraceClass `smt.debug.reconstruct.sort + registerTraceClass `smt.debug.reconstruct.term + registerTraceClass `smt.debug.reconstruct.proof registerTraceClass `smt.debug.reconstruct end Smt.Reconstruct diff --git a/Smt/Reconstruct/Prop.lean b/Smt/Reconstruct/Prop.lean index 1c0f8757..c3245456 100644 --- a/Smt/Reconstruct/Prop.lean +++ b/Smt/Reconstruct/Prop.lean @@ -5,12 +5,4 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Abdalrhman Mohamed -/ -import Smt.Reconstruct.Prop.Core -import Smt.Reconstruct.Prop.Factor -import Smt.Reconstruct.Prop.Lemmas -import Smt.Reconstruct.Prop.LiftOrNToImp -import Smt.Reconstruct.Prop.LiftOrNToNeg -import Smt.Reconstruct.Prop.PermutateOr -import Smt.Reconstruct.Prop.Pull -import Smt.Reconstruct.Prop.Resolution -import Smt.Reconstruct.Prop.Rewrites +import Smt.Reconstruct.Prop.Reconstruct diff --git a/Smt/Reconstruct/Prop/Lemmas.lean b/Smt/Reconstruct/Prop/Lemmas.lean index ec447a3d..6ef7d989 100644 --- a/Smt/Reconstruct/Prop/Lemmas.lean +++ b/Smt/Reconstruct/Prop/Lemmas.lean @@ -86,30 +86,6 @@ theorem notXorElim2 (h : ¬XOr p q) : ¬p ∨ q := | 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 theorem orComm : ∀ {P Q : Prop}, P ∨ Q → Q ∨ P := by @@ -165,19 +141,6 @@ theorem orImplies₃ : ∀ {p q : Prop}, p ∨ q → ¬ p → q := by | inl p => exact False.elim (np p) | inr q => exact q -theorem scopes : ∀ {ps : List Prop} {q : Prop}, impliesN ps q → andN ps → q := - by intros ps q h - match ps with - | [] => intro; exact h - | [p] => unfold andN - unfold impliesN at h - exact h - | p₁::p₂::ps => unfold andN - unfold impliesN at h - intro ⟨hp₁, hps⟩ - revert hps - exact scopes (h hp₁) - def impliesElim : ∀ {p q : Prop}, (p → q) → ¬ p ∨ q := by intros p q h exact match Classical.em p with @@ -361,51 +324,6 @@ theorem cnfXorNeg1 : (XOr p q) ∨ ¬p ∨ q := 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 h with - | isTrue _ => exact Or.inr hite' - | isFalse hnc => exact Or.inl hnc - -theorem cnfItePos2 [h : Decidable c] : ¬ (ite c a b) ∨ c ∨ b := by - apply orImplies - intro hite - have hite' := notNotElim hite - match h with - | isFalse _ => exact Or.inr hite' - | isTrue hc => exact Or.inl hc - -theorem cnfItePos3 [h : Decidable c] : ¬ (ite c a b) ∨ a ∨ b := by - apply orImplies - intro hite - have hite' := notNotElim hite - 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 h with - | isTrue _ => exact Or.inr hnite - | isFalse hnc => exact Or.inl hnc - -theorem cnfIteNeg2 [h : Decidable c] : (ite c a b) ∨ c ∨ ¬ b := by - apply orImplies - intro hnite - match h with - | isFalse _ => exact Or.inr hnite - | isTrue hc => exact Or.inl hc - -theorem cnfIteNeg3 [h : Decidable c] : (ite c a b) ∨ ¬ a ∨ ¬ b := by - apply orImplies - intro 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] diff --git a/Smt/Reconstruct/Prop/Reconstruct.lean b/Smt/Reconstruct/Prop/Reconstruct.lean new file mode 100644 index 00000000..838c93ea --- /dev/null +++ b/Smt/Reconstruct/Prop/Reconstruct.lean @@ -0,0 +1,462 @@ +/- +Copyright (c) 2021-2023 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 Smt.Reconstruct.Prop.Core +import Smt.Reconstruct.Prop.Factor +import Smt.Reconstruct.Prop.Lemmas +import Smt.Reconstruct.Prop.LiftOrNToImp +import Smt.Reconstruct.Prop.LiftOrNToNeg +import Smt.Reconstruct.Prop.PermutateOr +import Smt.Reconstruct.Prop.Pull +import Smt.Reconstruct.Prop.Resolution +import Smt.Reconstruct.Prop.Rewrites +import Smt.Reconstruct.Reconstruct +import Smt.Reconstruct.Rewrite + +namespace Smt.Reconstruct.Prop + +open Lean Qq + +@[smt_sort_reconstruct] def reconstructSort : SortReconstructor := fun s => do match s.getKind with + | .BOOLEAN_SORT => return q(Prop) + | _ => return none + +@[smt_term_reconstruct] def reconstructProp : TermReconstructor := fun t => do match t.getKind with + | .CONST_BOOLEAN => return if t.getBooleanValue then q(True) else q(False) + | .NOT => + let b : Q(Prop) ← reconstructTerm t[0]! + return q(¬$b) + | .IMPLIES => + let mut curr : Q(Prop) ← reconstructTerm t[t.getNumChildren - 1]! + for i in [1:t.getNumChildren] do + let p : Q(Prop) ← reconstructTerm 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 + | _ => return none +where + rightAssocOp (op : Expr) (t : cvc5.Term) : ReconstructM Expr := do + let mut curr ← reconstructTerm t[t.getNumChildren - 1]! + for i in [1:t.getNumChildren] do + curr := mkApp2 op (← reconstructTerm t[t.getNumChildren - i - 1]!) curr + return curr + +def reconstructRewrite (pf : cvc5.Proof) (cpfs : Array Expr) : ReconstructM (Option Expr) := do + match cvc5.RewriteRule.fromNat! pf.getArguments[0]!.getIntegerValue.toNat with + | .BOOL_DOUBLE_NOT_ELIM => + let p : Q(Prop) ← reconstructTerm pf.getArguments[1]! + addThm q((¬¬$p) = $p) q(@Prop.bool_double_not_elim $p) + | .BOOL_EQ_TRUE => + let p : Q(Prop) ← reconstructTerm pf.getArguments[1]! + addThm q(($p = True) = $p) q(@Prop.bool_eq_true $p) + | .BOOL_EQ_FALSE => + let p : Q(Prop) ← reconstructTerm pf.getArguments[1]! + addThm q(($p = False) = ¬$p) q(@Prop.bool_eq_false $p) + | .BOOL_EQ_NREFL => + let p : Q(Prop) ← reconstructTerm pf.getArguments[1]! + addThm q(($p = ¬$p) = False) q(@Prop.bool_eq_nrefl $p) + | .BOOL_IMPL_FALSE1 => + let p : Q(Prop) ← reconstructTerm pf.getArguments[1]! + addThm q(($p → False) = ¬$p) q(@Prop.bool_impl_false1 $p) + | .BOOL_IMPL_FALSE2 => + let p : Q(Prop) ← reconstructTerm pf.getArguments[1]! + addThm q((False → $p) = True) q(@Prop.bool_impl_false2 $p) + | .BOOL_IMPL_TRUE1 => + let p : Q(Prop) ← reconstructTerm pf.getArguments[1]! + addThm q(($p → True) = True) q(@Prop.bool_impl_true1 $p) + | .BOOL_IMPL_TRUE2 => + let p : Q(Prop) ← reconstructTerm pf.getArguments[1]! + addThm q((True → $p) = $p) q(@Prop.bool_impl_true2 $p) + -- | .BOOL_OR_TRUE => + -- let args ← reconstructArgs pf.getArguments + -- addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@Prop.or_assoc_eq) q(or_false) q(@Prop.bool_or_true) args) + | .BOOL_OR_FALSE => + let args ← reconstructArgs pf.getArguments[1:] + addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@Prop.or_assoc_eq) q(or_false) q(@Prop.bool_or_false) args) + | .BOOL_OR_FLATTEN => + let args ← reconstructArgs pf.getArguments[1:] + addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@Prop.or_assoc_eq) q(or_false) q(@Prop.bool_or_flatten) args) + | .BOOL_OR_DUP => + let args ← reconstructArgs pf.getArguments[1:] + addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@Prop.or_assoc_eq) q(or_false) q(@Prop.bool_or_dup) args) + | .BOOL_AND_TRUE => + let args ← reconstructArgs pf.getArguments[1:] + addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@Prop.and_assoc_eq) q(and_true) q(@Prop.bool_and_true) args) + -- | .BOOL_AND_FALSE => + -- let args ← reconstructArgs pf.getArguments[1:] + -- addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@Prop.and_assoc_eq) q(and_true) q(@Prop.bool_and_false) args) + | .BOOL_AND_FLATTEN => + let args ← reconstructArgs pf.getArguments[1:] + addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@Prop.and_assoc_eq) q(and_true) q(@Prop.bool_and_flatten) args) + | .BOOL_AND_DUP => + let args ← reconstructArgs pf.getArguments[1:] + addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@Prop.and_assoc_eq) q(and_true) q(@Prop.bool_and_dup) args) + | .BOOL_AND_CONF => + let args ← reconstructArgs pf.getArguments[1:] + addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@Prop.and_assoc_eq) q(and_true) q(@Prop.bool_and_conf) args) + | .BOOL_OR_TAUT => + let args ← reconstructArgs pf.getArguments[1:] + addTac (← reconstructTerm pf.getResult) (Tactic.smtRw · q(@Prop.or_assoc_eq) q(or_false) q(@Prop.bool_or_taut) args) + | .BOOL_XOR_REFL => + let p : Q(Prop) ← reconstructTerm pf.getArguments[1]! + addThm q(XOr $p $p = False) q(@Prop.bool_xor_refl $p) + | .BOOL_XOR_NREFL => + let p : Q(Prop) ← reconstructTerm pf.getArguments[1]! + addThm q((XOr $p ¬$p) = True) q(@Prop.bool_xor_nrefl $p) + | .BOOL_XOR_FALSE => + let p : Q(Prop) ← reconstructTerm pf.getArguments[1]! + addThm q(XOr $p False = $p) q(@Prop.bool_xor_false $p) + | .BOOL_XOR_TRUE => + let p : Q(Prop) ← reconstructTerm pf.getArguments[1]! + addThm q(XOr $p True = ¬$p) q(@Prop.bool_xor_true $p) + | .BOOL_XOR_COMM => + let p : Q(Prop) ← reconstructTerm pf.getArguments[1]! + let q : Q(Prop) ← reconstructTerm 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) ← reconstructTerm pf.getArguments[1]! + let q : Q(Prop) ← reconstructTerm pf.getArguments[2]! + addThm q(XOr $p $q = ¬($p = $q)) q(@Prop.bool_xor_elim $p $q) + | .ITE_NEG_BRANCH => + let c : Q(Prop) ← reconstructTerm pf.getArguments[1]! + let p : Q(Prop) ← reconstructTerm pf.getArguments[2]! + let q : Q(Prop) ← reconstructTerm 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) ← reconstructTerm pf.getArguments[1]! + let p : Q(Prop) ← reconstructTerm 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) ← reconstructTerm pf.getArguments[1]! + let p : Q(Prop) ← reconstructTerm 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) ← reconstructTerm pf.getArguments[1]! + let p : Q(Prop) ← reconstructTerm 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) ← reconstructTerm pf.getArguments[1]! + let p : Q(Prop) ← reconstructTerm 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) ← reconstructTerm pf.getArguments[1]! + let p : Q(Prop) ← reconstructTerm 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) ← reconstructTerm pf.getArguments[1]! + let p : Q(Prop) ← reconstructTerm 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) + | _ => return none +where + reconstructArgs (args : Array cvc5.Term) : ReconstructM (Array (Array Expr)) := do + let mut args' := #[] + for arg in args do + let mut arg' := #[] + for subarg in arg do + arg' := arg'.push (← reconstructTerm subarg) + args' := args'.push arg' + return args' + +def 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 + +def reconstructResolution (c₁ c₂ : Array cvc5.Term) (pol l : cvc5.Term) (p₁ p₂ : Expr) : ReconstructM Expr := do + let f := if pol.getBooleanValue == true then r₀ else r₁ + addTac (← rightAssocOp q(Or) (getResolutionResult c₁ c₂ pol l)) (f · p₁ p₂ (← reconstructTerm l) (some (c₁.size - 1)) (some (c₂.size - 1))) +where + rightAssocOp (op : Expr) (ts : Array cvc5.Term) : ReconstructM Expr := do + if ts.isEmpty then + return q(False) + let mut curr ← reconstructTerm ts[ts.size - 1]! + for i in [1:ts.size] do + curr := mkApp2 op (← reconstructTerm ts[ts.size - i - 1]!) curr + return curr + +def 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 + +def reconstructChainResolution (cs as : Array cvc5.Term) (ps : Array Expr) : ReconstructM Expr := do + let mut cc := clausify cs[0]! + let mut cp := ps[0]! + for i in [1:cs.size] do + let pol := as[0]![i - 1]! + let l := as[1]![i - 1]! + cp ← reconstructResolution cc (clausify cs[i]!) pol l cp ps[i]! + cc := getResolutionResult cc (clausify cs[i]!) pol l + return cp + +@[smt_proof_reconstruct] def reconstructPropProof : ProofReconstructor := fun pf => do match pf.getRule with + | .DSL_REWRITE => reconstructRewrite pf (← pf.getChildren.mapM reconstructProof) + | .RESOLUTION => + let c₁ := clausify pf.getChildren[0]!.getResult + let c₂ := clausify pf.getChildren[1]!.getResult + let p₁ ← reconstructProof pf.getChildren[0]! + let p₂ ← reconstructProof pf.getChildren[1]! + reconstructResolution c₁ c₂ pf.getArguments[0]! pf.getArguments[1]! p₁ p₂ + | .CHAIN_RESOLUTION => + let cs := pf.getChildren.map (·.getResult) + let as := pf.getArguments + let ps ← pf.getChildren.mapM reconstructProof + reconstructChainResolution 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 (← reconstructTerm pf.getResult) (factor · (← reconstructProof 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 (← reconstructTerm pf.getResult) (reorder · (← reconstructProof children[0]!) pos singleton) + | .SPLIT => + let q : Q(Prop) ← reconstructTerm pf.getArguments[0]! + addThm q($q ∨ ¬$q) q(Classical.em $q) + | .EQ_RESOLVE => + let p : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult + let q : Q(Prop) ← reconstructTerm pf.getResult + let hp : Q($p) ← reconstructProof pf.getChildren[0]! + let hpq : Q($p = $q) ← reconstructProof pf.getChildren[1]! + addThm q($q) q(Prop.eqResolve $hp $hpq) + | .MODUS_PONENS => + let p : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult + let q : Q(Prop) ← reconstructTerm pf.getResult + let hp : Q($p) ← reconstructProof pf.getChildren[0]! + let hpq : Q($p → $q) ← reconstructProof pf.getChildren[1]! + addThm q($q) q(Prop.modusPonens $hp $hpq) + | .NOT_NOT_ELIM => + let p : Q(Prop) ← reconstructTerm pf.getResult + let hnnp : Q(¬¬$p) ← reconstructProof pf.getChildren[0]! + addThm q($p) q(Prop.notNotElim $hnnp) + | .CONTRA => + let p : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult + let hp : Q($p) ← reconstructProof pf.getChildren[0]! + let hnp : Q(¬$p) ← reconstructProof pf.getChildren[0]! + addThm q(False) q(Prop.contradiction $hp $hnp) + | .AND_ELIM => + addTac (← reconstructTerm pf.getResult) (andElim · (← reconstructProof pf.getChildren[0]!) pf.getArguments[0]!.getIntegerValue.toNat) + | .AND_INTRO => + let cpfs := pf.getChildren + let q : Q(Prop) ← reconstructTerm cpfs.back.getResult + let hq : Q($q) ← reconstructProof cpfs.back + let f := fun pf ⟨q, hq⟩ => do + let p : Q(Prop) ← reconstructTerm pf.getResult + let hp : Q($p) ← reconstructProof 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 (← reconstructTerm pf.getResult) (notOrElim · (← reconstructProof pf.getChildren[0]!) pf.getArguments[0]!.getIntegerValue.toNat) + | .IMPLIES_ELIM => + let p : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult[0]! + let q : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult[1]! + let hpq : Q($p → $q) ← reconstructProof pf.getChildren[0]! + addThm q(¬$p ∨ $q) q(Prop.impliesElim $hpq) + | .NOT_IMPLIES_ELIM1 => + let p : Q(Prop) ← reconstructTerm pf.getResult + let q : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult[0]![1]! + let hnpq : Q(¬($p → $q)) ← reconstructProof pf.getChildren[0]! + addThm q($p) q(Prop.notImplies1 $hnpq) + | .NOT_IMPLIES_ELIM2 => + let p : Q(Prop) ← reconstructTerm pf.getChildren[0]!.getResult[0]![0]! + let q : Q(Prop) ← reconstructTerm pf.getResult[0]! + let hnpq : Q(¬($p → $q)) ← reconstructProof pf.getChildren[0]! + addThm q(¬$q) q(Prop.notImplies2 $hnpq) + | .EQUIV_ELIM1 => + let p : Q(Prop) ← reconstructTerm pf.getResult[0]![0]! + let q : Q(Prop) ← reconstructTerm pf.getResult[1]! + let hpq : Q($p = $q) ← reconstructProof pf.getChildren[0]! + addThm q(¬$p ∨ $q) q(Prop.equivElim1 $hpq) + | .EQUIV_ELIM2 => + let p : Q(Prop) ← reconstructTerm pf.getResult[0]! + let q : Q(Prop) ← reconstructTerm pf.getResult[1]![0]! + let hpq : Q($p = $q) ← reconstructProof pf.getChildren[0]! + addThm q($p ∨ ¬$q) q(Prop.equivElim2 $hpq) + | .NOT_EQUIV_ELIM1 => + let p : Q(Prop) ← reconstructTerm pf.getResult[0]! + let q : Q(Prop) ← reconstructTerm pf.getResult[1]! + let hnpq : Q($p ≠ $q) ← reconstructProof pf.getChildren[0]! + addThm q($p ∨ $q) q(Prop.notEquivElim1 $hnpq) + | .NOT_EQUIV_ELIM2 => + let p : Q(Prop) ← reconstructTerm pf.getResult[0]![0]! + let q : Q(Prop) ← reconstructTerm pf.getResult[1]![0]! + let hnpq : Q($p ≠ $q) ← reconstructProof pf.getChildren[0]! + addThm q(¬$p ∨ ¬$q) q(Prop.notEquivElim2 $hnpq) + | .XOR_ELIM1 => + let p : Q(Prop) ← reconstructTerm pf.getResult[0]! + let q : Q(Prop) ← reconstructTerm pf.getResult[1]! + let hpq : Q(XOr $p $q) ← reconstructProof pf.getChildren[0]! + addThm q($p ∨ $q) q(Prop.xorElim1 $hpq) + | .XOR_ELIM2 => + let p : Q(Prop) ← reconstructTerm pf.getResult[0]![0]! + let q : Q(Prop) ← reconstructTerm pf.getResult[1]![0]! + let hpq : Q(XOr $p $q) ← reconstructProof pf.getChildren[0]! + addThm q(¬$p ∨ ¬$q) q(Prop.xorElim2 $hpq) + | .NOT_XOR_ELIM1 => + let p : Q(Prop) ← reconstructTerm pf.getResult[0]! + let q : Q(Prop) ← reconstructTerm pf.getResult[1]![0]! + let hnpq : Q(¬XOr $p $q) ← reconstructProof pf.getChildren[0]! + addThm q($p ∨ ¬$q) q(Prop.notXorElim1 $hnpq) + | .NOT_XOR_ELIM2 => + let p : Q(Prop) ← reconstructTerm pf.getResult[0]![0]! + let q : Q(Prop) ← reconstructTerm pf.getResult[1]! + let hnpq : Q(¬XOr $p $q) ← reconstructProof pf.getChildren[0]! + addThm q(¬$p ∨ $q) q(Prop.notXorElim2 $hnpq) + | .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) ← reconstructTerm fs[n - i - 1]! + ps := q($p :: $ps) + let hnps : Q(¬andN $ps) ← reconstructProof pf.getChildren[0]! + addThm (← reconstructTerm pf.getResult) (.app q(Prop.notAnd $ps) hnps) + | .CNF_AND_POS => + let cnf := pf.getArguments[0]! + let i : Nat := 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) ← reconstructTerm cnf[n - i - 1]! + ps := q($p :: $ps) + addThm (← reconstructTerm 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) ← reconstructTerm cnf[n - i - 1]! + ps := q($p :: $ps) + addThm (← reconstructTerm 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) ← reconstructTerm cnf[n - i - 1]! + ps := q($p :: $ps) + addThm (← reconstructTerm pf.getResult) q(Prop.cnfOrPos $ps) + | .CNF_OR_NEG => + let cnf := pf.getArguments[0]! + let i : Nat := 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) ← reconstructTerm cnf[n - i - 1]! + ps := q($p :: $ps) + addThm (← reconstructTerm pf.getResult) q(Prop.cnfOrNeg $ps $i) + | .CNF_IMPLIES_POS => + let p : Q(Prop) ← reconstructTerm pf.getArguments[0]![0]! + let q : Q(Prop) ← reconstructTerm pf.getArguments[0]![1]! + addThm q(¬($p → $q) ∨ ¬$p ∨ $q) q(@Prop.cnfImpliesPos $p $q) + | .CNF_IMPLIES_NEG1 => + let p : Q(Prop) ← reconstructTerm pf.getArguments[0]![0]! + let q : Q(Prop) ← reconstructTerm pf.getArguments[0]![1]! + addThm q(($p → $q) ∨ $p) q(@Prop.cnfImpliesNeg1 $p $q) + | .CNF_IMPLIES_NEG2 => + let p : Q(Prop) ← reconstructTerm pf.getArguments[0]![0]! + let q : Q(Prop) ← reconstructTerm pf.getArguments[0]![1]! + addThm q(($p → $q) ∨ ¬$q) q(@Prop.cnfImpliesNeg2 $p $q) + | .CNF_EQUIV_POS1 => + let p : Q(Prop) ← reconstructTerm pf.getArguments[0]![0]! + let q : Q(Prop) ← reconstructTerm pf.getArguments[0]![1]! + addThm q($p ≠ $q ∨ ¬$p ∨ $q) q(@Prop.cnfEquivPos1 $p $q) + | .CNF_EQUIV_POS2 => + let p : Q(Prop) ← reconstructTerm pf.getArguments[0]![0]! + let q : Q(Prop) ← reconstructTerm pf.getArguments[0]![1]! + addThm q($p ≠ $q ∨ $p ∨ ¬$q) q(@Prop.cnfEquivPos2 $p $q) + | .CNF_EQUIV_NEG1 => + let p : Q(Prop) ← reconstructTerm pf.getArguments[0]![0]! + let q : Q(Prop) ← reconstructTerm pf.getArguments[0]![1]! + addThm q($p = $q ∨ $p ∨ $q) q(@Prop.cnfEquivNeg1 $p $q) + | .CNF_EQUIV_NEG2 => + let p : Q(Prop) ← reconstructTerm pf.getArguments[0]![0]! + let q : Q(Prop) ← reconstructTerm pf.getArguments[0]![1]! + addThm q($p = $q ∨ ¬$p ∨ ¬$q) q(@Prop.cnfEquivNeg2 $p $q) + | .CNF_XOR_POS1 => + let p : Q(Prop) ← reconstructTerm pf.getArguments[0]![0]! + let q : Q(Prop) ← reconstructTerm pf.getArguments[0]![1]! + addThm q(¬XOr $p $q ∨ $p ∨ $q) q(@Prop.cnfXorPos1 $p $q) + | .CNF_XOR_POS2 => + let p : Q(Prop) ← reconstructTerm pf.getArguments[0]![0]! + let q : Q(Prop) ← reconstructTerm pf.getArguments[0]![1]! + addThm q(¬XOr $p $q ∨ ¬$p ∨ ¬$q) q(@Prop.cnfXorPos2 $p $q) + | .CNF_XOR_NEG1 => + let p : Q(Prop) ← reconstructTerm pf.getArguments[0]![0]! + let q : Q(Prop) ← reconstructTerm pf.getArguments[0]![1]! + addThm q(XOr $p $q ∨ ¬$p ∨ $q) q(@Prop.cnfXorNeg1 $p $q) + | .CNF_XOR_NEG2 => + let p : Q(Prop) ← reconstructTerm pf.getArguments[0]![0]! + let q : Q(Prop) ← reconstructTerm pf.getArguments[0]![1]! + addThm q(XOr $p $q ∨ $p ∨ ¬$q) q(@Prop.cnfXorNeg2 $p $q) + | .TRUE_INTRO => + let p : Q(Prop) ← reconstructTerm pf.getResult[0]! + let hp : Q($p) ← reconstructProof pf.getChildren[0]! + addThm q($p = True) q(Prop.trueIntro $hp) + | .TRUE_ELIM => + let p : Q(Prop) ← reconstructTerm pf.getResult + let hp : Q($p = True) ← reconstructProof pf.getChildren[0]! + addThm q($p) q(Prop.trueElim $hp) + | .FALSE_INTRO => + let p : Q(Prop) ← reconstructTerm pf.getResult[0]! + let hnp : Q(¬$p) ← reconstructProof pf.getChildren[0]! + addThm q($p = False) q(Prop.falseIntro $hnp) + | .FALSE_ELIM => + let p : Q(Prop) ← reconstructTerm pf.getResult[0]! + let hnp : Q($p = False) ← reconstructProof pf.getChildren[0]! + addThm q(¬$p) q(Prop.falseElim $hnp) + | _ => return none + +end Smt.Reconstruct.Prop diff --git a/Smt/Reconstruct/Quant.lean b/Smt/Reconstruct/Quant.lean index a72474ef..03526f31 100644 --- a/Smt/Reconstruct/Quant.lean +++ b/Smt/Reconstruct/Quant.lean @@ -5,4 +5,4 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Abdalrhman Mohamed -/ -import Smt.Reconstruct.Quant.Lemmas +import Smt.Reconstruct.Quant.Reconstruct diff --git a/Smt/Reconstruct/Quant/Reconstruct.lean b/Smt/Reconstruct/Quant/Reconstruct.lean new file mode 100644 index 00000000..8693d7ac --- /dev/null +++ b/Smt/Reconstruct/Quant/Reconstruct.lean @@ -0,0 +1,173 @@ +/- +Copyright (c) 2021-2023 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 Smt.Reconstruct.Quant.Lemmas +import Smt.Reconstruct.Reconstruct + +/-- 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.Quant + +open Lean Qq + +@[smt_term_reconstruct] def reconstructQuant : TermReconstructor := fun t => do match t.getKind with + | .FORALL => + let mut xs : Array (Name × (Array Expr → ReconstructM Expr)) := #[] + for x in t[0]! do + xs := xs.push (getVariableName x, fun _ => reconstructSort x.getSort) + withNewTermCache $ Meta.withLocalDeclsD xs fun xs => do + let b ← reconstructTerm t[1]! + Meta.mkForallFVars xs b + | .EXISTS => + let mut xs : Array (Name × (Array Expr → ReconstructM Expr)) := #[] + for x in t[0]! do + xs := xs.push (getVariableName x, fun _ => reconstructSort x.getSort) + withNewTermCache $ Meta.withLocalDeclsD xs fun xs => do + let b ← reconstructTerm t[1]! + Meta.mkExistsFVars xs b + | .LAMBDA => + let mut xs : Array (Name × (Array Expr → ReconstructM Expr)) := #[] + for x in t[0]! do + xs := xs.push (getVariableName x, fun _ => reconstructSort x.getSort) + withNewTermCache $ Meta.withLocalDeclsD xs fun xs => do + let b ← reconstructTerm t[1]! + Meta.mkLambdaFVars xs b + | .HO_APPLY => + return (← reconstructTerm t[0]!).app (← reconstructTerm t[1]!) + | .SKOLEM_FUN => match t.getSkolemId with + | .QUANTIFIERS_SKOLEMIZE => + let q := t.getSkolemArguments[0]! + let n := t.getSkolemArguments[1]!.getIntegerValue.toNat + let es ← if q.getKind == .EXISTS then reconstructExistsSkolems q n else reconstructForallSkolems q n + return es[n]! + | _ => return none + | _ => return none +where + reconstructForallSkolems (q : cvc5.Term) (n : Nat) : ReconstructM (Array Expr) := do + let mut xs : Array (Name × (Array Expr → ReconstructM Expr)) := #[] + let mut es := #[] + for x in q[0]![0]! do + xs := xs.push (getVariableName x, fun _ => reconstructSort x.getSort) + let F := q[0]![1]! + for i in [0:n + 1] do + let α : Q(Type) ← reconstructSort q[0]![0]![i]!.getSort + let h : Q(Nonempty $α) ← Meta.synthInstance q(Nonempty $α) + let e ← withNewTermCache $ Meta.withLocalDeclsD xs fun xs => do + let F ← reconstructTerm F + let F' := F.replaceFVars xs[0:i] es + let ysF' ← Meta.mkExistsFVars xs[i + 1:n + 1] F' + let xysF' : Q($α → Prop) ← Meta.mkLambdaFVars #[xs[i]!] (.app q(Not) ysF') + return q(@Classical.epsilon $α $h $xysF') + es := es.push e + return es + reconstructExistsSkolems (q : cvc5.Term) (n : Nat) : ReconstructM (Array Expr) := do + let mut xs : Array (Name × (Array Expr → ReconstructM Expr)) := #[] + let mut es := #[] + for x in q[0]! do + xs := xs.push (getVariableName x, fun _ => reconstructSort x.getSort) + let F := q[1]! + for i in [0:n + 1] do + let α : Q(Type) ← reconstructSort q[0]![i]!.getSort + let h : Q(Nonempty $α) ← Meta.synthInstance q(Nonempty $α) + let e ← withNewTermCache $ Meta.withLocalDeclsD xs fun xs => do + let F ← reconstructTerm F + let F' := F.replaceFVars xs[0:i] es + let ysF' ← Meta.mkExistsFVars xs[i + 1:n + 1] F' + let xysF' : Q($α → Prop) ← Meta.mkLambdaFVars #[xs[i]!] ysF' + return q(@Classical.epsilon $α $h $xysF') + es := es.push e + return es + getVariableName (t : cvc5.Term) : Name := + if t.hasSymbol then t.getSymbol else Name.num `x t.getId + withNewTermCache {α} (k : ReconstructM α) : ReconstructM α := do + let state ← get + let r ← k + set { ← get with termCache := state.termCache } + return r + +@[smt_proof_reconstruct] def reconstructQuantProof : ProofReconstructor := fun pf => do match pf.getRule with + | .CONG => + let k := pf.getResult[0]!.getKind + -- This rule needs more care for closures. + if k == .FORALL then + reconstructForallCong pf + else + return none + | .BETA_REDUCE => + let α : Q(Type) ← reconstructSort pf.getResult[0]!.getSort + let t : Q($α) ← reconstructTerm pf.getResult[0]! + let t' : Q($α) ← reconstructTerm pf.getResult[1]! + addThm q($t = $t') q(Eq.refl $t) + | .SKOLEMIZE => reconstructSkolemize pf + | .INSTANTIATE => + let xsF : Q(Prop) ← reconstructProof pf.getChildren[0]! + let mut es := #[] + for t in pf.getArguments[0]! do + es := es.push (← reconstructTerm t) + addThm (← reconstructTerm pf.getResult) (mkAppN xsF es) + | .ALPHA_EQUIV => + let α : Q(Type) ← reconstructSort pf.getResult[0]!.getSort + let t : Q($α) ← reconstructTerm pf.getResult[0]! + let t' : Q($α) ← reconstructTerm pf.getResult[1]! + addThm q($t = $t') q(Eq.refl $t) + | _ => return none +where + reconstructForallCong (pf : cvc5.Proof) : ReconstructM Expr := do + let mv ← getCurrGoal + mv.withContext do + let n := reconstructQuant.getVariableName pf.getArguments[1]![0]! + let α : Q(Type) ← reconstructSort pf.getArguments[1]![0]!.getSort + let mkLam n α t := Meta.withLocalDeclD n α (reconstructTerm t >>= liftM ∘ 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] (reconstructProof pf.getChildren[0]!)) + let mv' ← getCurrGoal + mv'.withContext (mv'.assignIfDefeq h') + setCurrGoal mv + addThm q((∀ a, $p a) = (∀ a, $q a)) q(forall_congr $h) + reconstructSkolemize (pf : cvc5.Proof) : ReconstructM Expr := do + let res := pf.getChildren[0]!.getResult + if res.getKind == .EXISTS then + let es ← reconstructQuant.reconstructExistsSkolems res (res[0]![0]!.getNumChildren - 1) + let f := fun h e => do + let α : Q(Type) ← pure (e.getArg! 0) + let hα : Q(Nonempty $α) ← Meta.synthInstance q(Nonempty $α) + let p : Q($α → Prop) ← pure (e.getArg! 2) + let h : Q(∃ x, $p x) ← pure h + return q(@Classical.epsilon_spec_aux $α $hα $p $h) + let h : Expr ← es.foldlM f (← reconstructProof pf.getChildren[0]!) + addThm (← reconstructTerm pf.getResult) h + else + let es ← reconstructQuant.reconstructForallSkolems res (res[0]![0]!.getNumChildren - 1) + let f := fun h e => do + let α : Q(Type) ← pure (e.getArg! 0) + let hα : Q(Nonempty $α) ← Meta.synthInstance q(Nonempty $α) + let .lam n _ (.app _ b) bi := e.getArg! 2 | throwError "[skolemize]: expected a predicate with a negated body: {e}" + let p : Q($α → Prop) ← pure (.lam n α b bi) + let h : Q(¬∀ x, $p x) ← pure h + return q(@Classical.epsilon_spec_aux' $α $hα $p $h) + let h : Expr ← es.foldlM f (← reconstructProof pf.getChildren[0]!) + addThm (← reconstructTerm pf.getResult) h + +end Smt.Reconstruct.Quant diff --git a/Smt/Reconstruct/Reconstruct.lean b/Smt/Reconstruct/Reconstruct.lean index 41176830..348da56b 100644 --- a/Smt/Reconstruct/Reconstruct.lean +++ b/Smt/Reconstruct/Reconstruct.lean @@ -1,368 +1,17 @@ import cvc5 -import Lean import Qq +import Std -import Mathlib.Data.Real.Archimedean +import Smt.Attribute -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 +namespace Smt -/-- 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. +open Lean +open Attribute -- 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 getFVarExpr! (n : Name) : MetaM Expr := do - match (← getLCtx).findFromUserName? n with - | some d => return d.toExpr - | none => throwError "unknown free variable '{n}'" - -def getFVarOrConstExpr! (n : Name) : MetaM Expr := do - match (← getLCtx).findFromUserName? n with - | some d => return d.toExpr - | none => - let c ← getConstInfo n - return .const c.name (c.numLevelParams.iterate (.zero :: ·) []) - -def rconsSort (s : cvc5.Sort) : MetaM Expr := do match s.getKind with - | .BOOLEAN_SORT => return q(Prop) - | .INTERNAL_SORT_KIND - | .UNINTERPRETED_SORT => getFVarOrConstExpr! s.getSymbol - | .BITVECTOR_SORT => - let w : Nat := s.getBitVectorSize.val - return q(Std.BitVec $w) - | .INTEGER_SORT => return q(Int) - | .REAL_SORT => return q(Real) - | _ => return .const `sorry [] - -partial def rconsTerm (t : cvc5.Term) : MetaM Expr := do match t.getKind with - | .VARIABLE => getFVarExpr! (getVariableName t) - | .CONSTANT => getFVarOrConstExpr! 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 (getVariableName x, 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 (getVariableName x, 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 (getVariableName x, 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 - | .SKOLEM_FUN => - rconsSkolem t - | .CONST_BITVECTOR => - let w : Nat := t.getSort.getBitVectorSize.val - let v : Nat := (t.getBitVectorValue 10).toNat! - return q(Std.BitVec.ofNat $w $v) - | .BITVECTOR_BITOF => - let w : Nat := t[0]!.getSort.getBitVectorSize.val - let x : Q(Std.BitVec $w) ← rconsTerm t[0]! - let i : Nat := t.getOp[0]!.getIntegerValue.toNat - return q(«$x».getLsb $i = true) - | .BITVECTOR_BB_TERM => - let w : Nat := t.getNumChildren - let bs : Q(Std.BitVec 0) := q(.nil) - let f (bs : Expr) (i : Nat) : MetaM Expr := do - let p : Q(Prop) ← rconsTerm t[i]! - let bs : Q(Std.BitVec $i) := bs - let hp : Q(Decidable $p) ← synthDecidableInst t[i]! - return q(@Std.BitVec.cons $i (@decide $p $hp) $bs) - let bs : Q(Std.BitVec $w) ← (List.range w).foldlM f bs - return q($bs) - | .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 : Q(Real) := mkRealLit x.num.natAbs - if x.den == 1 then - if x.num ≥ 0 then - return q($num) - else - return q(-$num) - else - let den : Q(Real) := mkRealLit x.den - if x.num ≥ 0 then - return q($num / $den) - else - return q(-$num / $den) - | .NEG => - if t.getSort.isInteger then - let x : Q(Int) ← rconsTerm t[0]! - return q(-$x) - else - let x : Q(Real) ← 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(Real) ← rconsTerm t[0]! - let y : Q(Real) ← 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(Real) ← rconsTerm t[0]! - let y : Q(Real) ← 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(Real) ← rconsTerm t[0]! - let y : Q(Real) ← 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(Real) ← rconsTerm t[0]! - let y : Q(Real) ← 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(Real) ← rconsTerm t[0]! - let y : Q(Real) ← 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(Real) ← rconsTerm t[0]! - let y : Q(Real) ← 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(Real) ← rconsTerm t[0]! - let y : Q(Real) ← 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(Real) ← rconsTerm t[0]! - let y : Q(Real) ← rconsTerm t[1]! - return q($x > $y) - | .TO_REAL => - let x : Q(Int) ← rconsTerm t[0]! - return q($x : Real) - | .TO_INTEGER => - let x : Q(Real) ← rconsTerm t[0]! - return q(⌊$x⌋) - | .IS_INTEGER => - let x : Q(Real) ← rconsTerm t[0]! - return q($x = ⌊$x⌋) - | _ => - throwError "Unsupported kind: {repr t.getKind} : {t}" -where - mkRealLit (n : Nat) : Q(Real) := match h : n with - | 0 => q(0 : Real) - | 1 => q(1 : Real) - | _ + 2 => - let h : Q(Nat.AtLeastTwo $n) := h ▸ q(instNatAtLeastTwo) - let h := mkApp3 q(@instOfNat Real) (mkRawNatLit n) q(Real.natCast) h - mkApp2 q(@OfNat.ofNat Real) (mkRawNatLit n) h - rconsForallSkolems (q : cvc5.Term) (n : Nat) : MetaM (Array Expr) := do - let mut xs : Array (Name × (Array Expr → MetaM Expr)) := #[] - let mut es := #[] - for x in q[0]![0]! do - xs := xs.push (getVariableName x, fun _ => rconsSort x.getSort) - let F := q[0]![1]! - for i in [0:n + 1] do - let α : Q(Type) ← rconsSort q[0]![0]![i]!.getSort - let h : Q(Nonempty $α) ← Meta.synthInstance q(Nonempty $α) - let e ← Meta.withLocalDeclsD xs fun xs => do - let F ← rconsTerm F - let F' := F.replaceFVars xs[0:i] es - let ysF' ← Meta.mkExistsFVars xs[i + 1:n] F' - let xysF' : Q($α → Prop) ← Meta.mkLambdaFVars #[xs[i]!] (.app q(Not) ysF') - return q(@Classical.epsilon $α $h $xysF') - es := es.push e - return es - rconsExistsSkolems (q : cvc5.Term) (n : Nat) : MetaM (Array Expr) := do - let mut xs : Array (Name × (Array Expr → MetaM Expr)) := #[] - let mut es := #[] - for x in q[0]! do - xs := xs.push (getVariableName x, fun _ => rconsSort x.getSort) - let F := q[1]! - for i in [0:n + 1] do - let α : Q(Type) ← rconsSort q[0]![i]!.getSort - let h : Q(Nonempty $α) ← Meta.synthInstance q(Nonempty $α) - let e ← Meta.withLocalDeclsD xs fun xs => do - let F ← rconsTerm F - let F' := F.replaceFVars xs[0:i] es - let ysF' ← Meta.mkExistsFVars xs[i + 1:n] F' - let xysF' : Q($α → Prop) ← Meta.mkLambdaFVars #[xs[i]!] ysF' - return q(@Classical.epsilon $α $h $xysF') - es := es.push e - return es - rconsSkolem (t : cvc5.Term) : MetaM Expr := do match t.getSkolemId with - | .PURIFY => rconsTerm t.getSkolemArguments[0]! - | .DIV_BY_ZERO => return q(fun (x : Real) => x / 0) - | .INT_DIV_BY_ZERO => return q(fun (x : Int) => x / 0) - | .MOD_BY_ZERO => return q(fun (x : Int) => x % 0) - | .QUANTIFIERS_SKOLEMIZE => - let q := t.getSkolemArguments[0]! - let n := t.getSkolemArguments[1]!.getIntegerValue.toNat - let es ← if q.getKind == .EXISTS then rconsExistsSkolems q n else rconsForallSkolems q n - return es[n]! - | _ => - throwError "Unsupported skolem ID: {repr t.getSkolemId} : {t.getSkolemArguments}" - getVariableName (t : cvc5.Term) : Name := - if t.hasSymbol then t.getSymbol else Name.num `x t.getId - 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 - rightAssocOpDecidableInst (op : Expr) (inst : Expr) (t : cvc5.Term) : MetaM Expr := do - let mut curr ← rconsTerm t[t.getNumChildren - 1]! - let mut currInst ← synthDecidableInst t[t.getNumChildren - 1]! - for i in [1:t.getNumChildren] do - let ct := t[t.getNumChildren - i - 1]! - currInst := mkApp4 inst (← rconsTerm ct) curr (← synthDecidableInst ct) currInst - curr := mkApp2 op (← rconsTerm ct) curr - return currInst - synthDecidableInst (t : cvc5.Term) : MetaM Expr := do match t.getKind with - | .CONST_BOOLEAN => return if t.getBooleanValue then q(instDecidableTrue) else q(instDecidableFalse) - | .NOT => - let p : Q(Prop) ← rconsTerm t[0]! - let hp : Q(Decidable $p) ← synthDecidableInst t[0]! - return q(@instDecidableNot $p $hp) - | .AND => rightAssocOpDecidableInst q(And) q(@instDecidableAnd) t - | .OR => rightAssocOpDecidableInst q(Or) q(@instDecidableOr) t - | .XOR => rightAssocOpDecidableInst q(XOr) q(@XOr.instDecidableXOr) t - | .EQUAL => - if t[0]!.getSort.getKind == .BOOLEAN_SORT then - let p : Q(Prop) ← rconsTerm t[0]! - let q : Q(Prop) ← rconsTerm t[1]! - let hp : Q(Decidable $p) ← synthDecidableInst t[0]! - let hq : Q(Decidable $q) ← synthDecidableInst t[1]! - return q(@instDecidableEqProp $p $q (@instDecidableIff $p $q $hp $hq)) - if t[0]!.getSort.getKind == .BITVECTOR_SORT then - let w : Nat := t[0]!.getSort.getBitVectorSize.val - return q(@Std.instDecidableEqBitVec $w) - let p : Q(Prop) ← rconsTerm t - Meta.synthInstance q(Decidable $p) - | .BITVECTOR_BITOF => - let w : Nat := t[0]!.getSort.getBitVectorSize.val - let x : Q(Std.BitVec $w) ← rconsTerm t[0]! - let i : Nat := t.getOp[0]!.getIntegerValue.toNat - return q(instDecidableEqBool («$x».getLsb $i) true) - | _ => - let p : Q(Prop) ← rconsTerm t - Meta.synthInstance q(Decidable $p) - -structure RconsState where - termMap : HashMap cvc5.Term Name - proofMap : HashMap cvc5.Proof Name +structure Reconstruct.state where + termCache : HashMap cvc5.Term Expr + proofCache : HashMap cvc5.Proof Expr count : Nat trusts : Array cvc5.Proof mainGoal : MVarId @@ -370,40 +19,87 @@ structure RconsState where currAssums : Array Expr skipedGoals : Array MVarId -abbrev RconsM := StateT RconsState MetaM +abbrev ReconstructM := StateT Reconstruct.state MetaM -namespace Rcons +abbrev SortReconstructor := cvc5.Sort → ReconstructM (Option Expr) -def incCount : RconsM Nat := - modifyGet fun state => (state.count, { state with count := state.count + 1 }) +abbrev TermReconstructor := cvc5.Term → ReconstructM (Option Expr) -def cacheTerm (t : cvc5.Term) (n : Name) : RconsM Unit := - modify fun state => { state with termMap := state.termMap.insert t n } +abbrev ProofReconstructor := cvc5.Proof → ReconstructM (Option Expr) -def getTermExpr (t : cvc5.Term) : RconsM Expr := - return .fvar ⟨(← get).termMap.find! t⟩ +namespace Reconstruct -def cacheProof (pf : cvc5.Proof) (n : Name) : RconsM Unit := - modify fun state => { state with proofMap := state.proofMap.insert pf n } +private unsafe def getReconstructorsUnsafe (n : Name) (rcons : Type) : MetaM (List (rcons × Name)) := do + let env ← getEnv + let names := ((smtExt.getState env).findD n {}).toList + let mut reconstructors := [] + for name in names do + let fn ← IO.ofExcept <| Id.run <| ExceptT.run <| + env.evalConst rcons Options.empty name + reconstructors := (fn, name) :: reconstructors + return reconstructors -def isReconstructed (pf : cvc5.Proof) : RconsM Bool := do - let state ← get - if !state.proofMap.contains pf then - return false - state.currGoal.withContext do - let ctx ← getLCtx - return if ctx.contains ⟨state.proofMap.find! pf⟩ then true else false +@[implemented_by getReconstructorsUnsafe] +opaque getReconstructors (n : Name) (rcons : Type) : MetaM (List (rcons × Name)) -def getProofExpr (pf : cvc5.Proof) : RconsM Expr := - return .fvar ⟨(← get).proofMap.find! pf⟩ +def reconstructSort (s : cvc5.Sort) : ReconstructM Expr := do + let rs ← getReconstructors ``SortReconstructor SortReconstructor + go rs s +where + go (rs : List (SortReconstructor × Name)) (s : cvc5.Sort) : ReconstructM Expr := do + for (r, n) in rs do + if let some e ← r s then + trace[smt.debug.reconstruct.sort] "{s} =({n})=> {e}" + return e + throwError "Failed to reconstruct sort {s} with kind {repr s.getKind}" + +def traceReconstructTerm (t : cvc5.Term) (r : Except Exception Expr) : ReconstructM MessageData := + return m!"{t} ↦ " ++ match r with + | .ok e => m!"{e}" + | .error _ => m!"{bombEmoji}" + +def reconstructTerm : cvc5.Term → ReconstructM Expr := withTermCache fun t => + withTraceNode `smt.debug.reconstruct (traceReconstructTerm t) do + let rs ← getReconstructors ``TermReconstructor TermReconstructor + go rs t +where + withTermCache (r : cvc5.Term → ReconstructM Expr) (t : cvc5.Term) : ReconstructM Expr := do + match (← get).termCache.find? t with + -- TODO: cvc5's global bound variables mess up the cache. Find a fix. + | some e => if e.hasFVar then reconstruct r t else return e + | none => reconstruct r t + reconstruct r t := do + let e ← r t + modify fun state => { state with termCache := state.termCache.insert t e } + return e + go (rs : List (TermReconstructor × Name)) (t : cvc5.Term) : ReconstructM Expr := do + for (r, n) in rs do + if let some e ← r t then + trace[smt.debug.reconstruct.term] "{t} =({n})=> {e}" + return e + throwError "Failed to reconstruct term {t} with kind {repr t.getKind}" + +def withProofCache (r : cvc5.Proof → ReconstructM Expr) (p : cvc5.Proof) : ReconstructM Expr := do + match (← get).proofCache.find? p with + | some e => (← get).currGoal.withContext do + if (← getLCtx).containsFVar e then return e else reconstruct r p + | none => reconstruct r p +where + reconstruct r p := do + let e ← r p + modify fun state => { state with proofCache := state.proofCache.insert p e } + return e -def withAssums (as : Array Expr) (k : RconsM α) : RconsM α := do +def incCount : ReconstructM Nat := + modifyGet fun state => (state.count, { state with count := state.count + 1 }) + +def withAssums (as : Array Expr) (k : ReconstructM α) : ReconstructM α := 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 +def skipStep (mv : MVarId) : ReconstructM Unit := mv.withContext do let state ← get let t ← Meta.mkForallFVars state.currAssums (← mv.getType) let mv' ← state.mainGoal.withContext (Meta.mkFreshExprMVar t) @@ -411,826 +107,99 @@ def skipStep (mv : MVarId) : RconsM Unit := mv.withContext do 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 := +def getCurrGoal : ReconstructM MVarId := get >>= (pure ·.currGoal) -def setCurrGoal (mv : MVarId) : RconsM Unit := +def setCurrGoal (mv : MVarId) : ReconstructM Unit := modify fun state => { state with currGoal := mv } -def addThm (type : Expr) (val : Expr) : RconsM Expr := do +def addThm (type : Expr) (val : Expr) : ReconstructM 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}" + trace[smt.debug.reconstruct.proof] "have {name} : {type} := {val}" setCurrGoal mv return .fvar fv -def addTac (type : Expr) (tac : Tac) : RconsM Expr := do +def addTac (type : Expr) (tac : MVarId → MetaM Unit) : ReconstructM Expr := do let mv ← getCurrGoal mv.withContext do let name := Name.num `s (← incCount) let mv' ← Meta.mkFreshExprMVar type - runTac mv'.mvarId! tac + tac mv'.mvarId! let (fv, mv) ← (← mv.assert name type mv').intro1P - trace[smt.debug.reconstruct] "have {name} : {type} := by {tac}" + trace[smt.debug.reconstruct.proof] "have {name} : {type} := by {mv'}" setCurrGoal mv return .fvar fv -def addTrust (type : Expr) (pf : cvc5.Proof) : RconsM Expr := do +def addTrust (type : Expr) (pf : cvc5.Proof) : ReconstructM 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] + trace[smt.debug.reconstruct.proof] m!"have {name} : {type} := sorry" + trace[smt.debug.reconstruct.proof] 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_false) 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_false) 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_false) 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_false) 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_false) 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 +partial def reconstructProof : cvc5.Proof → ReconstructM Expr := withProofCache fun pf => do + let rs ← getReconstructors ``ProofReconstructor ProofReconstructor + go rs 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 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 - -def 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))) -where - 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 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 - -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[0]![i - 1]! - let l := as[1]![i - 1]! - cp ← rconsResolution cc (clausify cs[i]!) pol l cp ps[i]! - cc := getResolutionResult cc (clausify cs[i]!) pol l - return cp - -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 := rconsTerm.getVariableName pf.getArguments[1]![0]! - let α : Q(Type) ← rconsSort pf.getArguments[1]![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[0]!)) - let mv' ← getCurrGoal - mv'.withContext (mv'.assignIfDefeq h') - setCurrGoal mv - addThm q((∀ a, $p a) = (∀ a, $q a)) q(forall_congr $h) - -def rconsBB (pf : cvc5.Proof) : RconsM Expr := do - let t := pf.getArguments[0]![0]! - match t.getKind with - | .CONST_BITVECTOR => - let w : Nat := t.getSort.getBitVectorSize.toNat - let t : Q(Std.BitVec $w) ← rconsTerm pf.getResult[0]! - let t' : Q(Std.BitVec $w) ← rconsTerm pf.getResult[1]! - addThm q($t = $t') q(Eq.refl $t) - | _ => - let type ← rconsTerm pf.getResult + go (rs : List (ProofReconstructor × Name)) (pf : cvc5.Proof) : ReconstructM Expr := do + for (r, _) in rs do + if let some e ← r pf then + return e + _ ← pf.getChildren.mapM reconstructProof + let type ← reconstructTerm pf.getResult addTrust type pf -def rconsSkolemize (pf : cvc5.Proof) (rconsProof : cvc5.Proof → RconsM Expr) : RconsM Expr := do - if pf.getChildren[0]!.getResult.getKind == .EXISTS then - let es ← rconsTerm.rconsExistsSkolems pf.getChildren[0]!.getResult (pf.getChildren[0]!.getResult[0]![0]!.getNumChildren - 1) - let f := fun h e => do - let α : Q(Type) ← pure (e.getArg! 0) - let hα : Q(Nonempty $α) ← Meta.synthInstance q(Nonempty $α) - let p : Q($α → Prop) ← pure (e.getArg! 2) - let h : Q(∃ x, $p x) ← pure h - return q(@Classical.epsilon_spec_aux $α $hα $p $h) - let h : Expr ← es.foldlM f (← rconsProof pf.getChildren[0]!) - addThm (← rconsTerm pf.getResult) h - else - let es ← rconsTerm.rconsForallSkolems pf.getChildren[0]!.getResult (pf.getChildren[0]!.getResult[0]![0]!.getNumChildren - 1) - let f := fun h e => do - let α : Q(Type) ← pure (e.getArg! 0) - let hα : Q(Nonempty $α) ← Meta.synthInstance q(Nonempty $α) - let .lam n _ (.app _ b) bi := e.getArg! 2 | throwError "[skolemize]: expected a predicate with a negated body: {e}" - let p : Q($α → Prop) ← pure (.lam n α b bi) - let h : Q(¬∀ x, $p x) ← pure h - return q(@Classical.epsilon_spec_aux' $α $hα $p $h) - let h : Expr ← es.foldlM f (← rconsProof pf.getChildren[0]!) - addThm (← rconsTerm pf.getResult) h +end Reconstruct -partial def rconsProof (pf : cvc5.Proof) : RconsM Expr := do - if ← isReconstructed pf 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 => - let c₁ := clausify pf.getChildren[0]!.getResult - let c₂ := clausify pf.getChildren[1]!.getResult - let p₁ ← rconsProof pf.getChildren[0]! - let p₂ ← rconsProof pf.getChildren[1]! - rconsResolution c₁ c₂ pf.getArguments[0]! pf.getArguments[1]! p₁ p₂ - | .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 : Nat := 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 : Nat := 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 needs more care 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) - | .NARY_CONG => - 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 - 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) - | .BV_BITBLAST_STEP => - rconsBB pf - | .SKOLEM_INTRO => - let α : Q(Type) ← rconsSort pf.getResult[0]!.getSort - let k : Q($α) ← rconsTerm pf.getResult[0]! - let t : Q($α) ← rconsTerm pf.getResult[1]! - addThm q($k = $t) q(Eq.refl $t) - | .SKOLEMIZE => - rconsSkolemize pf rconsProof - | .INSTANTIATE => - let xsF : Q(Prop) ← rconsProof pf.getChildren[0]! - let mut es := #[] - for t in pf.getArguments[0]! do - es := es.push (← rconsTerm t) - 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 +def traceReconstructProof (r : Except Exception (FVarId × MVarId × List MVarId)) : MetaM MessageData := + return match r with + | .ok _ => m!"{checkEmoji}" + | _ => m!"{bombEmoji}" -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, #[], #[]⟩ +open Qq in +partial def reconstructProof (mv : MVarId) (pf : cvc5.Proof) : MetaM (FVarId × MVarId × List MVarId) := + withTraceNode `smt.debug.reconstruct traceReconstructProof do + let Prod.mk (p : Q(Prop)) state ← (Reconstruct.reconstructTerm (pf.getResult)).run ⟨{}, {}, 0, #[], mv, mv, #[], #[]⟩ + let Prod.mk (h : Q(True → $p)) (.mk _ _ _ _ _ mv _ mvs) ← (Reconstruct.reconstructProof pf).run state let ⟨fv, mv, _⟩ ← mv.replace h.fvarId! q($h trivial) q($p) return (fv, mv, mvs.toList) 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 "enum-inst" "true" - Solver.setOption "produce-models" "true" - Solver.setOption "produce-proofs" "true" - Solver.setOption "proof-elim-subtypes" "true" - Solver.setOption "proof-granularity" "dsl-rewrite" - 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") +def traceProve (r : Except Exception (Except SolverError Proof)) : MetaM MessageData := + return match r with + | .ok (.ok _) => m!"{checkEmoji}" + | _ => m!"{bombEmoji}" + +open cvc5 in +def prove (query : String) (timeout : Option Nat) : MetaM (Except SolverError cvc5.Proof) := + withTraceNode `smt.debug.prove traceProve do 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 "enum-inst" "true" + Solver.setOption "produce-models" "true" + Solver.setOption "produce-proofs" "true" + Solver.setOption "proof-elim-subtypes" "true" + Solver.setOption "proof-granularity" "dsl-rewrite" + 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") syntax (name := reconstruct) "reconstruct" str : tactic @@ -1242,7 +211,7 @@ open Lean.Elab Tactic in match r with | .error e => logInfo (repr e) | .ok pf => - let (_, mv, mvs) ← rconsProof (← getMainGoal) pf + let (_, mv, mvs) ← reconstructProof (← getMainGoal) pf replaceMainGoal (mv :: mvs) -end Smt.Reconstruct +end Smt diff --git a/Smt/Reconstruct/UF.lean b/Smt/Reconstruct/UF.lean index dfab13c3..03781b3f 100644 --- a/Smt/Reconstruct/UF.lean +++ b/Smt/Reconstruct/UF.lean @@ -5,5 +5,4 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Abdalrhman Mohamed -/ -import Smt.Reconstruct.UF.Congruence -import Smt.Reconstruct.UF.Rewrites +import Smt.Reconstruct.UF.Reconstruct diff --git a/Smt/Reconstruct/UF/Reconstruct.lean b/Smt/Reconstruct/UF/Reconstruct.lean new file mode 100644 index 00000000..9832f575 --- /dev/null +++ b/Smt/Reconstruct/UF/Reconstruct.lean @@ -0,0 +1,103 @@ +/- +Copyright (c) 2021-2023 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 Smt.Reconstruct.Reconstruct +import Smt.Reconstruct.UF.Congruence +import Smt.Reconstruct.UF.Rewrites + +namespace Smt.Reconstruct.UF + +open Lean Qq + +def getFVarOrConstExpr! (n : Name) : MetaM Expr := do + match (← getLCtx).findFromUserName? n with + | some d => return d.toExpr + | none => + let c ← getConstInfo n + return .const c.name (c.numLevelParams.repeat (.zero :: ·) []) + +@[smt_sort_reconstruct] def reconstructUS : SortReconstructor := fun s => do match s.getKind with + | .INTERNAL_SORT_KIND + | .UNINTERPRETED_SORT => getFVarOrConstExpr! s.getSymbol + | _ => return none + +@[smt_term_reconstruct] def reconstructUF : TermReconstructor := fun t => do match t.getKind with + | .EQUAL => + let α : Q(Type) ← reconstructSort t[0]!.getSort + let x : Q($α) ← reconstructTerm t[0]! + let y : Q($α) ← reconstructTerm t[1]! + return q($x = $y) + | .DISTINCT => + let α : Q(Type) ← reconstructSort t[0]!.getSort + let x : Q($α) ← reconstructTerm t[0]! + let y : Q($α) ← reconstructTerm t[1]! + return q($x ≠ $y) + | .APPLY_UF => + let mut curr ← reconstructTerm t[0]! + for i in [1:t.getNumChildren] do + curr := .app curr (← reconstructTerm t[i]!) + return curr + | _ => return none + +def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do + match cvc5.RewriteRule.fromNat! pf.getArguments[0]!.getIntegerValue.toNat with + | .EQ_REFL => + let α : Q(Type) ← reconstructSort pf.getArguments[1]!.getSort + let t : Q($α) ← reconstructTerm pf.getArguments[1]! + addThm q(($t = $t) = True) q(@UF.eq_refl $α $t) + | .EQ_SYMM => + let α : Q(Type) ← reconstructSort pf.getArguments[1]!.getSort + let t : Q($α) ← reconstructTerm pf.getArguments[1]! + let s : Q($α) ← reconstructTerm pf.getArguments[2]! + addThm q(($t = $s) = ($s = $t)) q(@UF.eq_symm $α $t $s) + | .DISTINCT_BINARY_ELIM => + let α : Q(Type) ← reconstructSort pf.getArguments[1]!.getSort + let t : Q($α) ← reconstructTerm pf.getArguments[1]! + let s : Q($α) ← reconstructTerm pf.getArguments[2]! + addThm q(($t ≠ $s) = ¬($t = $s)) q(@UF.distinct_binary_elim $α $t $s) + | _ => return none + +@[smt_proof_reconstruct] def reconstructUFProof : ProofReconstructor := fun pf => do match pf.getRule with + | .DSL_REWRITE => reconstructRewrite pf + | .REFL => + let α : Q(Type) ← reconstructSort pf.getArguments[0]!.getSort + let a : Q($α) ← reconstructTerm pf.getArguments[0]! + addThm q($a = $a) q(Eq.refl $a) + | .SYMM => + let α : Q(Type) ← reconstructSort pf.getResult[0]!.getSort + let a : Q($α) ← reconstructTerm pf.getResult[1]! + let b : Q($α) ← reconstructTerm pf.getResult[0]! + if pf.getResult.getKind == .EQUAL then + let h : Q($a = $b) ← reconstructProof pf.getChildren[0]! + addThm q($b = $a) q(Eq.symm $h) + else + let h : Q($a ≠ $b) ← reconstructProof pf.getChildren[0]! + addThm q($b ≠ $a) q(Ne.symm $h) + | .TRANS => + let cpfs := pf.getChildren + let α : Q(Type) ← reconstructSort cpfs[0]!.getResult[0]!.getSort + let a : Q($α) ← reconstructTerm cpfs[0]!.getResult[0]! + let mut curr ← reconstructProof cpfs[0]! + for i in [1:cpfs.size] do + let b : Q($α) ← reconstructTerm cpfs[i]!.getResult[0]! + let c : Q($α) ← reconstructTerm cpfs[i]!.getResult[1]! + let hab : Q($a = $b) := curr + let hbc : Q($b = $c) ← reconstructProof cpfs[i]! + curr ← addThm q($a = $c) q(Eq.trans $hab $hbc) + return curr + | .CONG => + let k := pf.getResult[0]!.getKind + if k == .FORALL || k == .EXISTS || k == .WITNESS || k == .LAMBDA || k == .SET_COMPREHENSION then + return none + let mut assums ← pf.getChildren.mapM reconstructProof + addTac (← reconstructTerm pf.getResult) (smtCongr · assums) + | .NARY_CONG => + let mut assums ← pf.getChildren.mapM reconstructProof + addTac (← reconstructTerm pf.getResult) (smtCongr · assums) + | _ => return none + +end Smt.Reconstruct.UF diff --git a/Smt/Tactic/Smt.lean b/Smt/Tactic/Smt.lean index 416cf303..bf098d22 100644 --- a/Smt/Tactic/Smt.lean +++ b/Smt/Tactic/Smt.lean @@ -8,15 +8,16 @@ Authors: Abdalrhman Mohamed import Lean import Smt.Dsl.Sexp -import Smt.Reconstruct -import Smt.Translate +import Smt.Reconstruct.Prop.Lemmas +import Smt.Reconstruct.Reconstruct +import Smt.Translate.Query import Smt.Util namespace Smt open Lean hiding Command open Elab Tactic Qq -open Smt Reconstruct Translate Query Solver +open Smt Reconstruct Translate Query initialize registerTraceClass `smt.debug @@ -153,7 +154,7 @@ private def addDeclToUnfoldOrTheorem (thms : Meta.SimpTheorems) (e : Expr) : Met 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]`" | .ok pf => - let (fv, mv, mvs) ← rconsProof (← Tactic.getMainGoal) pf + let (fv, mv, mvs) ← reconstructProof (← 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]) diff --git a/Smt/Translate/Translator.lean b/Smt/Translate/Translator.lean index 9082e50e..c14e0441 100644 --- a/Smt/Translate/Translator.lean +++ b/Smt/Translate/Translator.lean @@ -38,7 +38,7 @@ namespace Translator private unsafe def getTranslatorsUnsafe : MetaM (List (Translator × Name)) := do let env ← getEnv - let names := (smtExt.getState env).toList + let names := ((smtExt.getState env).findD ``Translator {}).toList -- trace[smt.debug.attr] "Translators: {names}" let mut translators := [] for name in names do diff --git a/Test/Reconstruction/Arith/ArithMulSign.expected b/Test/Reconstruction/Arith/ArithMulSign.expected index 3fe3f183..b80d024c 100644 --- a/Test/Reconstruction/Arith/ArithMulSign.expected +++ b/Test/Reconstruction/Arith/ArithMulSign.expected @@ -1,8 +1,18 @@ -Test/Reconstruction/Arith/ArithMulSign.lean:1:0: error: object file './.lake/build/lib/Smt/Reconstruct/Arith.olean' of module Smt.Reconstruct.Arith does not exist -Test/Reconstruction/Arith/ArithMulSign.lean:3:5: error: unknown namespace 'Smt.Reconstruct.Arith' -Test/Reconstruction/Arith/ArithMulSign.lean:5:22: error: unexpected token '+'; expected ')', ',' or ':' -Test/Reconstruction/Arith/ArithMulSign.lean:8:22: error: expected token -Test/Reconstruction/Arith/ArithMulSign.lean:11:22: error: expected token -Test/Reconstruction/Arith/ArithMulSign.lean:15:4: error: expected token -Test/Reconstruction/Arith/ArithMulSign.lean:23:30: error: expected token -Test/Reconstruction/Arith/ArithMulSign.lean:27:4: error: expected token +Test/Reconstruction/Arith/ArithMulSign.lean:24:2: error: type mismatch + _uniq.7790 +has type + a < Int.ofNat 0 → b < OfNat.ofNat 0 → zToR (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.13465 +has type + a < Int.ofNat 0 → + b > OfNat.ofNat 0 → + c < OfNat.ofNat 0 → + d > OfNat.ofNat 0 → + e < Int.ofNat 0 → + Mul.mul (Mul.mul (Mul.mul (zToR a) (Pow.pow b 2)) (Pow.pow c 2)) (Pow.pow d 4) * zToR (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/MulPosNeg.expected b/Test/Reconstruction/Arith/MulPosNeg.expected index 6e84c6aa..e69de29b 100644 --- a/Test/Reconstruction/Arith/MulPosNeg.expected +++ b/Test/Reconstruction/Arith/MulPosNeg.expected @@ -1,17 +0,0 @@ -Test/Reconstruction/Arith/MulPosNeg.lean:1:0: error: object file './.lake/build/lib/Smt/Reconstruct/Arith.olean' of module Smt.Reconstruct.Arith does not exist -Test/Reconstruction/Arith/MulPosNeg.lean:3:5: error: unknown namespace 'Smt.Reconstruct.Arith' -Test/Reconstruction/Arith/MulPosNeg.lean:5:26: error: expected token -Test/Reconstruction/Arith/MulPosNeg.lean:8:24: error: expected token -Test/Reconstruction/Arith/MulPosNeg.lean:11:26: error: expected token -Test/Reconstruction/Arith/MulPosNeg.lean:14:24: error: expected token -Test/Reconstruction/Arith/MulPosNeg.lean:17:26: error: expected token -Test/Reconstruction/Arith/MulPosNeg.lean:20:26: error: expected token -Test/Reconstruction/Arith/MulPosNeg.lean:23:27: error: expected token -Test/Reconstruction/Arith/MulPosNeg.lean:26:35: error: expected token -Test/Reconstruction/Arith/MulPosNeg.lean:29:35: error: expected token -Test/Reconstruction/Arith/MulPosNeg.lean:32:35: error: expected token -Test/Reconstruction/Arith/MulPosNeg.lean:35:35: error: expected token -Test/Reconstruction/Arith/MulPosNeg.lean:38:35: error: expected token -Test/Reconstruction/Arith/MulPosNeg.lean:41:35: error: expected token -Test/Reconstruction/Arith/MulPosNeg.lean:44:35: error: expected token -Test/Reconstruction/Arith/MulPosNeg.lean:47:27: error: expected token diff --git a/Test/Reconstruction/Arith/SumBounds.expected b/Test/Reconstruction/Arith/SumBounds.expected index 82d092d7..9a18ef1c 100644 --- a/Test/Reconstruction/Arith/SumBounds.expected +++ b/Test/Reconstruction/Arith/SumBounds.expected @@ -1,6 +1,16 @@ -Test/Reconstruction/Arith/SumBounds.lean:1:0: error: object file './.lake/build/lib/Smt/Reconstruct/Arith.olean' of module Smt.Reconstruct.Arith does not exist -Test/Reconstruction/Arith/SumBounds.lean:3:5: error: unknown namespace 'Smt.Reconstruct.Arith' -Test/Reconstruction/Arith/SumBounds.lean:5:32: error: expected token -Test/Reconstruction/Arith/SumBounds.lean:10:4: error: expected token -Test/Reconstruction/Arith/SumBounds.lean:14:30: error: expected token -Test/Reconstruction/Arith/SumBounds.lean:18:32: error: expected token +Test/Reconstruction/Arith/SumBounds.lean:7:2: error: application type mismatch + sumBounds₁ h₂ +argument + h₂ +has type + @LT.lt ℕ instLTNat b e : Prop +but is expected to have type + @LT.lt ℕ Preorder.toLT b e : Prop +Test/Reconstruction/Arith/SumBounds.lean:20:2: error: application type mismatch + sumBounds₁ h₂ +argument + h₂ +has type + @LT.lt ℕ instLTNat b e : Prop +but is expected to have type + @LT.lt ℕ Preorder.toLT b e : Prop diff --git a/Test/Reconstruction/Arith/TightBounds.expected b/Test/Reconstruction/Arith/TightBounds.expected index c6d5465b..e69de29b 100644 --- a/Test/Reconstruction/Arith/TightBounds.expected +++ b/Test/Reconstruction/Arith/TightBounds.expected @@ -1,5 +0,0 @@ -Test/Reconstruction/Arith/TightBounds.lean:1:0: error: object file './.lake/build/lib/Smt/Reconstruct/Arith.olean' of module Smt.Reconstruct.Arith does not exist -Test/Reconstruction/Arith/TightBounds.lean:3:5: error: unknown namespace 'Smt.Reconstruct.Arith' -Test/Reconstruction/Arith/TightBounds.lean:5:24: error: expected token -Test/Reconstruction/Arith/TightBounds.lean:9:32: error: expected token -Test/Reconstruction/Arith/TightBounds.lean:13:24: error: expected token diff --git a/Test/Reconstruction/Arith/Trichotomy.expected b/Test/Reconstruction/Arith/Trichotomy.expected index 8c45a67e..e69de29b 100644 --- a/Test/Reconstruction/Arith/Trichotomy.expected +++ b/Test/Reconstruction/Arith/Trichotomy.expected @@ -1,3 +0,0 @@ -Test/Reconstruction/Arith/Trichotomy.lean:1:0: error: object file './.lake/build/lib/Smt/Reconstruct/Arith.olean' of module Smt.Reconstruct.Arith does not exist -Test/Reconstruction/Arith/Trichotomy.lean:3:5: error: unknown namespace 'Smt.Reconstruct.Arith' -Test/Reconstruction/Arith/Trichotomy.lean:5:24: error: expected token