chore: bump to v4.8.0

.gitignore

@@ -1,2 +1 @@
-/.vscode
 /.lake

Smt/Reconstruct.lean

@@ -204,7 +204,7 @@ def solve (query : String) (timeout : Option Nat) : MetaM (Except Error cvc5.Pro
       let ps ← Solver.getProof
       if h : 0 < ps.size then
         return ps[0]
-    throw (self := instMonadExcept _ _) (Error.user_error "something went wrong")
+    throw (self := instMonadExceptOfMonadExceptOf _ _) (Error.user_error "something went wrong")
 
 syntax (name := reconstruct) "reconstruct" str : tactic
 

Smt/Reconstruct/Arith.lean

@@ -28,12 +28,12 @@ open Qq
   | _             => 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)⟩
+  | false => ⟨q(Real), q(Real.instLinearOrderedRing)⟩
+  | true  => ⟨q(Int), q(Int.instLinearOrderedCommRing.toLinearOrderedRing)⟩
 
 def getTypeAndInst' (s : cvc5.Sort) : Σ (α : Q(Type)) (_ : Q(LinearOrderedRing $α)), Q(FloorRing $α) := match s.isInteger with
-  | false => ⟨q(Real), q(Real.instLinearOrderedRingReal), q(Real.instFloorRingRealInstLinearOrderedRingReal)⟩
-  | true  => ⟨q(Int), q(Int.linearOrderedCommRing.toLinearOrderedRing), q(instFloorRingIntToLinearOrderedRingLinearOrderedCommRing)⟩
+  | false => ⟨q(Real), q(Real.instLinearOrderedRing), q(Real.instFloorRing)⟩
+  | true  => ⟨q(Int), q(Int.instLinearOrderedCommRing.toLinearOrderedRing), q(instFloorRingInt)⟩
 
 @[smt_term_reconstruct] def reconstructArith : TermReconstructor := fun t => do match t.getKind with
   | .SKOLEM => match t.getSkolemId with
@@ -130,7 +130,7 @@ where
     | 1     => q(1 : Real)
     | _ + 2 =>
       let h : Q(Nat.AtLeastTwo $n) := h ▸ q(instNatAtLeastTwo)
-      let h := mkApp3 q(@instOfNatAtLeastTwo Real) (mkRawNatLit n) q(Real.natCast) h
+      let h := mkApp3 q(@instOfNatAtLeastTwo Real) (mkRawNatLit n) q(Real.instNatCast) h
       mkApp2 q(@OfNat.ofNat Real) (mkRawNatLit n) h
   leftAssocOp (op : Expr) (t : cvc5.Term) : ReconstructM Expr := do
     let mut curr ← reconstructTerm t[0]!

Smt/Reconstruct/Arith/ArithMulSign/Lemmas.lean

@@ -5,8 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Tomaz Gomes Mascarenhas
 -/
 
-import Mathlib.Algebra.Parity
-import Mathlib.Data.Nat.Parity
+import Mathlib.Algebra.Order.Ring.Defs
+-- import Mathlib.Algebra.Order.Ring.Nat
+-- import Mathlib.Data.Nat.Parity
 import Mathlib.Data.Real.Basic
 
 import Smt.Reconstruct.Arith.MulPosNeg.Lemmas
@@ -95,18 +96,18 @@ theorem combineSigns₄ : a < 0 → b < 0 → b * a > 0 := by
   simp at h
   exact h
 
-theorem castPos : ∀ (a : Int), a > 0 → Real.intCast.intCast a > 0 := by
+theorem castPos : ∀ (a : Int), a > 0 → ↑a > 0 := by
   intros a h
   simp [h]
 
-theorem castNeg : ∀ (a : Int), a < 0 → Real.intCast.intCast a < 0 := by
+theorem castNeg : ∀ (a : Int), a < 0 → ↑a < 0 := by
   intros a h
   simp [h]
 
 instance : HMul ℤ ℝ ℝ where
-  hMul z r := Real.intCast.intCast z * r
+  hMul z r := ↑z * r
 
 instance : HMul ℝ ℤ ℝ where
-  hMul r z := r * Real.intCast.intCast z
+  hMul r z := r * ↑z
 
 end Smt.Reconstruct.Arith

Smt/Reconstruct/Arith/ArithMulSign/Tactic.lean

@@ -7,7 +7,7 @@ Authors: Tomaz Gomes Mascarenhas
 
 import Lean
 
-import Mathlib.Data.Nat.Parity
+import Mathlib.Algebra.Order.Ring.Nat
 import Mathlib.Data.Real.Basic
 
 import Smt.Reconstruct.Arith.ArithMulSign.Lemmas
@@ -24,9 +24,9 @@ inductive Pol where
  deriving BEq
 
 def intLOR := mkApp2 (.const ``LinearOrderedCommRing.toLinearOrderedRing [.zero])
-                     (.const ``Int []) (.const ``Int.linearOrderedCommRing [])
+                     (.const ``Int []) (.const ``Int.instLinearOrderedCommRing [])
 
-def RealLOR := Expr.const ``Real.instLinearOrderedRingReal []
+def RealLOR := Expr.const ``Real.instLinearOrderedRing []
 
 
 def traceMulSign (r : Except Exception Unit) : MetaM MessageData :=
@@ -181,7 +181,7 @@ where
         | _ => throwError "[arithMulSign]: unexpected type for expression"
       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]
+      let zeroR ← mkAppOptM ``OfNat.ofNat #[mkConst ``Real, (mkNatLit 0), none]
       -- zero with the same type as the current argument
       let currZero := if exprIsInt then zeroI else zeroR
       let bindedType: Expr ←

Smt/Reconstruct/Arith/MulPosNeg/Lemmas.lean

@@ -15,7 +15,7 @@ variable [LinearOrderedRing α]
 
 variable {a b c : α}
 
-@[simp] def zToR : Int → Real := Real.intCast.intCast
+@[simp] def zToR (i : Int) : Real := ↑i
 
 def uncurry {p₁ p₂ p₃ : Prop} : (p₁ → p₂ → p₃) → (p₁ ∧ p₂) → p₃ := by
   intros h₁ h₂

Smt/Reconstruct/Arith/MulPosNeg/Tactic.lean

@@ -63,7 +63,8 @@ def arithMulMeta (va vb vc : Expr) (pos : Bool) (compId : Nat) (thms : List Name
     else throwError "[arithMul]: index too large"
 
   let zeroI := mkApp (mkConst ``Int.ofNat) (mkNatLit 0)
-  let zeroR ← mkAppOptM' (.const ``OfNat.ofNat [.zero]) #[mkConst ``Real, (mkNatLit 0), none]
+  let zeroR ←
+    mkAppOptM ``OfNat.ofNat #[mkConst ``Real, (mkNatLit 0), none]
   let zeroC := if typeC == mkConst ``Int then zeroI else zeroR
   let premiseLeft ←
     if pos then mkAppM ``LT.lt #[zeroC, vc]

Smt/Reconstruct/Arith/SumBounds/Tactic.lean

@@ -17,7 +17,7 @@ namespace Smt.Reconstruct.Arith
 open Lean
 open Meta Elab.Tactic Expr
 
-theorem castEQ : ∀ {a b : Int}, a = b → Real.intCast.intCast a = Real.intCast.intCast b := by
+theorem castEQ : ∀ {a b : Int}, a = b → (↑a : Real) = (↑b : Real) := by
   intros a b h
   rw [h]
 

Smt/Reconstruct/Arith/TransFns/ArithTransPi.lean

@@ -25,16 +25,20 @@ open Elab Tactic Meta
 open Real
 
 def expr_3141592 : Expr :=
-  mkApp5 (Expr.const ``OfScientific.ofScientific [Level.zero]) (mkConst ``Rat) (Lean.Expr.const `Rat.instOfScientificRat []) (.lit (.natVal 3141592)) (mkConst ``Bool.true) (.lit (.natVal 6))
+  mkApp5 (Expr.const ``OfScientific.ofScientific [Level.zero])
+    (mkConst ``Rat) (Lean.Expr.const `Rat.instOfScientific [])
+    (.lit (.natVal 3141592)) (mkConst ``Bool.true) (.lit (.natVal 6))
 
 def expr_3141593 : Expr :=
-  mkApp5 (Expr.const ``OfScientific.ofScientific [Level.zero]) (mkConst ``Rat) (Lean.Expr.const `Rat.instOfScientificRat []) (.lit (.natVal 3141593)) (mkConst ``Bool.true) (.lit (.natVal 6))
+  mkApp5 (Expr.const ``OfScientific.ofScientific [Level.zero])
+    (mkConst ``Rat) (Lean.Expr.const `Rat.instOfScientific [])
+    (.lit (.natVal 3141593)) (mkConst ``Bool.true) (.lit (.natVal 6))
 
 def ratCast_lt_mpr {x y : ℚ} : x < y → (x : ℝ) < (y : ℝ) := ratCast_lt.mpr
 
 def ratOfFloat : Expr → Expr
   | .app (.app (.app (.app (.app a _) _) d) e) f =>
-      .app (.app (.app (.app (.app a (mkConst ``Rat)) (mkConst ``Rat.instOfScientificRat)) d) e) f
+      .app (.app (.app (.app (.app a (mkConst ``Rat)) (mkConst ``Rat.instOfScientific)) d) e) f
   | e => e
 
 def isOfNatNatLit : Expr → Bool

Smt/Reconstruct/BitVec.lean

@@ -34,14 +34,14 @@ partial def synthDecidableInst (t : cvc5.Term) : ReconstructM Expr := do match t
       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
+    | .XOR => rightAssocOpDecidableInst q(XOr) q(@XOr.instDecidable) 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))
+        return q(@instDecidableEqOfIff $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(@instDecidableEqBitVec $w)
@@ -275,7 +275,7 @@ def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
       let mv ← Bool.boolify h.mvarId!
       let ds := [``BitVec.beq, ``BitVec.beq.go]
       let ts := [``BitVec.getLsb_cons, ``Nat.succ.injEq]
-      let ps := [``Nat.reduceAdd, ``Nat.reduceSub, ``Nat.reduceEq, ``reduceIte]
+      let ps := [``Nat.reduceAdd, ``Nat.reduceSub, ``Nat.reduceEqDiff, ``reduceIte]
       let simpTheorems ← ds.foldrM (fun n a => a.addDeclToUnfold n) {}
       let simpTheorems ← ts.foldrM (fun n a => a.addConst n) simpTheorems
       let simpProcs ← ps.foldrM (fun n a => a.add n false) {}

Smt/Reconstruct/Builtin.lean

@@ -38,7 +38,7 @@ def getFVarOrConstExpr! (n : Name) : MetaM Expr := do
 
 @[smt_term_reconstruct] def reconstructBuiltin : TermReconstructor := fun t => do match t.getKind with
   | .VARIABLE => getFVarExpr! (getVariableName t)
-  | .CONSTANT => getFVarOrConstExpr! t.getSymbol
+  | .CONSTANT => getFVarOrConstExpr! (Name.mkSimple t.getSymbol)
   | .EQUAL =>
     let α : Q(Type) ← reconstructSort t[0]!.getSort
     let x : Q($α) ← reconstructTerm t[0]!
@@ -65,7 +65,7 @@ def getFVarOrConstExpr! (n : Name) : MetaM Expr := do
   | _ => return none
 where
   getVariableName (t : cvc5.Term) : Name :=
-    if t.hasSymbol then t.getSymbol else Name.num `x t.getId
+    if t.hasSymbol then Name.mkSimple t.getSymbol else Name.num `x t.getId
 
 def reconstructRewrite (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
   match pf.getRewriteRule with

Smt/Reconstruct/Prop/Lemmas.lean

@@ -182,47 +182,56 @@ theorem notNotElim : ∀ {p : Prop}, ¬ ¬ p → p :=
 
 theorem notNotIntro : ∀ {p : Prop}, p → ¬ ¬ p := λ p np => np p
 
-theorem deMorgan : ∀ {l : List Prop}, ¬ orN (notList l) → andN l :=
-  by intros l h
-     exact match l with
-     | []   => True.intro
-     | [t]  => by simp only [andN]
-                  simp only [notList, orN, map] at h
-                  cases Classical.em t with
-                  | inl tt  => exact tt
-                  | inr ntt => exact False.elim (h ntt)
-     | h₁::h₂::t => by simp [orN, notList, map] at h
-                       have ⟨ t₁, t₂ ⟩ := deMorganSmall h
-                       have ih := @deMorgan (h₂::t) t₂
-                       simp [andN]
-                       have t₁' := notNotElim t₁
-                       exact ⟨ t₁', ih ⟩
-
-theorem deMorgan₂ : ∀ {l : List Prop}, andN l → ¬ orN (notList l) :=
-  by intros l h
-     exact match l with
-     | [] => by simp [orN, notList]
-     | [t] => by simp only [orN, notList]; simp [andN] at h; exact notNotIntro h
-     | h₁::h₂::t => by simp [orN, notList, map]
-                       simp [andN] at h
-                       apply deMorganSmall₂
-                       have nnh₁ := notNotIntro (And.left h)
-                       have ih := @deMorgan₂ (h₂::t) (And.right h)
-                       exact ⟨nnh₁, ih⟩
-
-theorem deMorgan₃ : ∀ {l : List Prop}, ¬ orN l → andN (notList l) :=
-  by intros l h
-     exact match l with
-     | [] => True.intro
-     | [t] => by simp [andN, notList, map]
-                 simp [orN, Not] at h
-                 exact h
-     | h₁::h₂::t => by simp [orN, Not] at h
-                       have ⟨t₁, t₂⟩ := deMorganSmall h
-                       simp [orN, Not] at t₂
-                       simp [andN, notList, map]
-                       have ih := @deMorgan₃ (h₂::t) t₂
-                       exact ⟨t₁, ih⟩
+theorem deMorgan : ∀ {l : List Prop}, ¬ orN (notList l) → andN l := by
+  intros l h
+  exact match l with
+  | []   => True.intro
+  | [t]  => by
+    simp only [andN]
+    simp only [notList, orN, map] at h
+    cases Classical.em t with
+    | inl tt  => exact tt
+    | inr ntt => exact False.elim (h ntt)
+  | h₁::h₂::t => by
+    simp only [orN, notList, map] at h
+    have ⟨ t₁, t₂ ⟩ := deMorganSmall h
+    have ih := @deMorgan (h₂::t) t₂
+    simp [andN]
+    have t₁' := notNotElim t₁
+    exact ⟨ t₁', ih ⟩
+
+theorem deMorgan₂ : ∀ {l : List Prop}, andN l → ¬ orN (notList l) := by
+  intros l h
+  exact match l with
+  | [] => by
+    simp [orN, notList]
+  | [t] => by
+    simp only [orN, notList]
+    simp [andN] at h
+    exact notNotIntro h
+  | h₁::h₂::t => by
+    simp only [orN, notList, map]
+    simp [andN] at h
+    apply deMorganSmall₂
+    have nnh₁ := notNotIntro (And.left h)
+    have ih := @deMorgan₂ (h₂::t) (And.right h)
+    exact ⟨nnh₁, ih⟩
+
+theorem deMorgan₃ : ∀ {l : List Prop}, ¬ orN l → andN (notList l) := by
+  intros l h
+  exact match l with
+  | [] => True.intro
+  | [t] => by
+    simp only [andN, notList, map]
+    simp only [orN, Not] at h
+    exact h
+  | h₁::h₂::t => by
+    simp only [orN, Not] at h
+    have ⟨t₁, t₂⟩ := deMorganSmall h
+    simp only [orN, Not] at t₂
+    simp [andN, notList, map]
+    have ih := @deMorgan₃ (h₂::t) t₂
+    exact ⟨t₁, ih⟩
 
 theorem cnfAndNeg' : ∀ (l : List Prop), andN l ∨ orN (notList l) :=
   by intro l
@@ -652,7 +661,7 @@ theorem length_eraseIdx (h : i < l.length) : (eraseIdx l i).length = l.length -1
     | succ i =>
       simp
       rw [length_cons, succ_lt_succ_iff] at hi
-      rw [ih hi, Nat.succ_eq_add_one, Nat.sub_add_cancel (zero_lt_of_lt hi)]
+      rw [ih hi, Nat.sub_add_cancel (zero_lt_of_lt hi)]
 
 theorem take_append (a b : List α) : take a.length (a ++ b) = a := by
   have H3:= take_append_drop a.length (a ++ b)

Smt/Reconstruct/Quant.lean

@@ -28,7 +28,7 @@ namespace Smt.Reconstruct.Quant
 open Lean Qq
 
 def getVariableName (t : cvc5.Term) : Name :=
-  if t.hasSymbol then t.getSymbol else Name.num `x t.getId
+  if t.hasSymbol then Name.mkSimple t.getSymbol else Name.num `x t.getId
 
 @[smt_term_reconstruct] def reconstructQuant : TermReconstructor := fun t => do match t.getKind with
   | .FORALL =>

Smt/Reconstruct/UF.lean

@@ -22,8 +22,8 @@ def getFVarOrConstExpr! (n : Name) : MetaM Expr := do
 
 @[smt_sort_reconstruct] def reconstructUS : SortReconstructor := fun s => do match s.getKind with
   | .INTERNAL_SORT_KIND
-  | .UNINTERPRETED_SORT => getFVarOrConstExpr! s.getSymbol
-  | _             => return none
+  | .UNINTERPRETED_SORT => getFVarOrConstExpr! (Name.mkSimple s.getSymbol)
+  | _ => return none
 
 @[smt_term_reconstruct] def reconstructUF : TermReconstructor := fun t => do match t.getKind with
   | .APPLY_UF =>

Smt/Tactic/Concretize.lean

@@ -77,7 +77,10 @@ def Location.simpRwAt (loc : Location) (pf : Expr) : TacticM Unit := do
   }
   _ ← Tactic.simpLocation ctx #[] (loc := loc.toTacticLocation)
   let { ctx, .. } ← mkSimpContext Syntax.missing (eraseLocal := false) (kind := .dsimp)
-  Tactic.dsimpLocation { ctx with config := { ctx.config with failIfUnchanged := false } } (loc := loc.toTacticLocation)
+  Tactic.dsimpLocation
+    { ctx with config := { ctx.config with failIfUnchanged := false } }
+    (loc := loc.toTacticLocation)
+    (simprocs := #[])
 
 end Lean.Meta
 
@@ -209,7 +212,7 @@ def concretizeApp (e : Expr) : ConcretizeM TransformStep := do
     for (pi, a) in info.paramInfo.zip args do
       let argTp ← inferType a
       -- TODO: This has good results but might be expensive.
-      let a' := if !pi.isInstImplicit then ← whnf a else a
+      let a' ← if !pi.isInstImplicit then whnf a else pure a
       let isConcretizable :=
         !a'.hasLooseBVars ∧ !a'.hasFVar ∧ (argTp.isType ∨ pi.hasFwdDeps ∨ pi.isInstImplicit)
       if isConcretizable then
@@ -347,7 +350,7 @@ The Coq variant is in `snipe`:
 - https://github.com/smtcoq/sniper/blob/af7b0d22f496f8e7a0ee6ca495314d80ea2aa881/theories/elimination_polymorphism.v
 -/
 elab "concretize" "[" nms:ident,* "]" : tactic => do
-  let nms ← (nms : Array Syntax).mapM resolveGlobalConstNoOverloadWithInfo
+  let nms ← (nms : Array Syntax).mapM (liftM $ Elab.realizeGlobalConstNoOverloadWithInfo ·)
   let concretizeSet := nms.foldl (init := .empty) (NameSet.insert · ·)
   evalConcretize
     |>.run' { visitSet := #[.goal] }

Smt/Tactic/EqnDef.lean

@@ -109,7 +109,7 @@ def addEqnDefWithBody (nm : Name) (e : Expr) : TacticM (FVarId × FVarId) := do
     -- in the equational definition.
     let (fvVar, mvarId) ← (← mvarId.define nm tp e).intro1P
     return (fvVar, [mvarId])
-  
+
   let (eqn, pf) ← withMainContext <| lambdaTelescope e fun args body => do
     let lhs ← mkAppOptM' (mkFVar fvVar) (args.map some)
     let eqn ← mkEq lhs body
@@ -127,7 +127,7 @@ def addEqnDefWithBody (nm : Name) (e : Expr) : TacticM (FVarId × FVarId) := do
 open Lean Meta Elab Tactic in
 /-- Place an equational definition for a constant in the local context. -/
 elab "extract_def" i:ident : tactic => do
-  let nm ← resolveGlobalConstNoOverloadWithInfo i
+  let nm ← Elab.realizeGlobalConstNoOverloadWithInfo i
   let _ ← addEqnDefForConst nm
 
 /-- Specialize an equational definition via partial evaluation. See `specialize_def`. -/

Smt/Tactic/WHNFConfigurable.lean

@@ -980,7 +980,7 @@ def reduceProjOf? (e : Expr) (p : Name → Bool) : MetaM (Option Expr) := do
     | _ => pure none
 
 private instance [MonadAlwaysExcept ε m] [STWorld ω m] [BEq α] [Hashable α] : MonadAlwaysExcept ε (MonadCacheT α β m) :=
-  instMonadAlwaysExceptStateRefT' ε
+  instMonadAlwaysExceptStateRefT'
 
 partial def reduce (e : Expr) (explicitOnly skipTypes skipProofs := true) : ReductionM Expr :=
   let rec visit (e : Expr) : MonadCacheT Expr Expr ReductionM Expr :=
@@ -1007,7 +1007,7 @@ partial def reduce (e : Expr) (explicitOnly skipTypes skipProofs := true) : Redu
             else
               args ← args.modifyM i visit
           if f.isConstOf ``Nat.succ && args.size == 1 && args[0]!.isRawNatLit then
-            pure <| mkRawNatLit (args[0]!.natLit?.get! + 1)
+            pure <| mkRawNatLit (args[0]!.rawNatLit?.get! + 1)
           else
             pure <| mkAppN f args
         -- `let`-bindings are normally substituted by WHNF, but they are left alone when `zeta` is off,