Breakdown proof reconstruction file.

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

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

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

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

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

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 α]

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
 

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

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

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

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 : α}