Bump Lean version to v4.24.0.

Author: abdoo8080

Smt/Dsl/Sexp.lean

@@ -21,7 +21,7 @@ def generalIdent : Parser :=
     fn := fun c s =>
       let startPos := s.pos
       let s := takeWhile1Fn (fun c => !("(){}[].".contains c) ∧ !c.isWhitespace) "expected generalized identifier" c s
-      mkNodeToken `generalIdent startPos c s }
+      mkNodeToken `generalIdent startPos true c s }
 
 def Lean.TSyntax.getGeneralId : TSyntax `generalIdent → String
   | ⟨.node _ `generalIdent args⟩ => args[0]!.getAtomVal

Smt/Preprocess/BoolAsProp.lean

@@ -13,7 +13,7 @@ theorem Bool.eq_eq_true (x y : Bool) : (x = y : Bool) = ((x : Prop) = (y : Prop)
   simp only [decide_eq_true_eq, _root_.eq_iff_iff, coe_iff_coe]
 
 theorem Bool.eq_self (x : Bool): (x = x) = (True : Prop) := by
-  simp only [eq_self]
+  simp only
 
 theorem Prop.eq_true (x : Prop) : (x = True : Prop) = (x : Prop) := by
   simp only [eq_iff_iff, iff_true]

Smt/Preprocess/Embedding.lean

@@ -1,13 +1,11 @@
 import Lean
-import Smt
-import Smt.Real
-import Lean.Meta.Tactic.Congr
 
+import Smt.Preprocess.Basic
 import Smt.Preprocess.BoolAsProp
 import Smt.Preprocess.NatAsInt
 import Smt.Preprocess.RatAsReal
 
-namespace Smt.Preprocess.SmtTranslate
+namespace Smt.Preprocess
 
 open Lean Meta
 
@@ -334,7 +332,7 @@ def addNonNegToHypotheses (mv : MVarId) (sortedNatDomainVars : Array Expr) : Met
     `Int.toNat_of_nonneg` normalization, generalize away Bool/Rat/Nat locals,
     then re-introduce hypotheses and clear the original variables.
 -/
-def smt_translate (mv' : MVarId) : MetaM MVarId := withTraceNode `smt.reconstruct.smt_translate traceSmtTranslate do
+def smtTranslateCore (mv' : MVarId) : MetaM MVarId := withTraceNode `smt.reconstruct.smtTranslate traceSmtTranslate do
   trace[debug] m!"initial goal: {mv'}"
 
   let mut mv := mv'
@@ -397,7 +395,7 @@ def smt_translate (mv' : MVarId) : MetaM MVarId := withTraceNode `smt.reconstruc
   -- For each `x : Rat`, assert a witness equation `x = a / b` with `a b : Int`
   for ratVar in sortedRatVars do
     let varName ← ratVar.fvarId!.getUserName
-    let divProof ← mkAppOptM ``Rat.cast_eq_div_int #[ratVar]
+    let divProof ← mkAppOptM `Rat.cast_eq_div_int #[ratVar]
     let divType ← inferType divProof
     mv ← mv.assert (varName.appendAfter "_rat") divType divProof
     let (fVarId, mv') ← mv.intro (varName.appendAfter "_rat")
@@ -669,7 +667,7 @@ def smt_translate (mv' : MVarId) : MetaM MVarId := withTraceNode `smt.reconstruc
   let ns := [
     ``Bool.and_eq_true, ``Bool.or_eq_true, ``Bool.not_eq_true2, ``Bool.iff_eq_true, ``Bool.xor_eq_true, ``Bool.eq_eq_true, ``Bool.eq_self, ``Bool.true_eq_false, ``Bool.false_eq_true, ``Prop.eq_true, ``Prop.eq_false,
 
-    ``Int.natCast_add, ``Int.natCast_sub2, ``Int.natCast_mul, ``Int.natCast_ediv, ``Int.natCast_emod, ``Int.ofNat_eq, ``Int.ofNat_le2, ``Int.ofNat_lt2, ``Int.ofNat_ge, ``Int.ofNat_gt, ``Int.ofNat_ne, ``Nat.cast_zero, ``Nat.cast_one, ``Nat.cast_ofNat, ``Int.natSub.eq_1, ``Int.toNat_of_nonneg, ``Int.ofNat_eq_coe,
+    ``Int.natCast_add, ``Int.natCast_sub2, ``Int.natCast_mul, ``Int.natCast_ediv, ``Int.natCast_emod, ``Int.ofNat_eq, ``Int.ofNat_le2, ``Int.ofNat_lt2, ``Int.ofNat_ge, ``Int.ofNat_gt, ``Int.ofNat_ne, ``Int.natSub.eq_1, ``Int.toNat_of_nonneg, ``Int.ofNat_eq_coe, ``Int.cast_ofNat_Int,
 
     ``Rat.cast_add, ``Rat.cast_sub, ``Rat.cast_mul, ``Rat.cast_div, ``Rat.cast_neg, ``Rat.cast_inv, ``Rat.cast_eq, ``Rat.cast_le, ``Rat.cast_lt, ``Rat.cast_ge, ``Rat.cast_gt, ``Rat.cast_ne, ``Rat.cast_zero, ``Rat.cast_one, ``Rat.cast_ofNat,
   ]
@@ -729,7 +727,7 @@ def smt_translate (mv' : MVarId) : MetaM MVarId := withTraceNode `smt.reconstruc
 
   for ratVar in sortedRatVars do
     let varName ← ratVar.fvarId!.getUserName
-    let castExpr ← mkAppOptM ``Rat.cast #[mkConst ``Real, none, ratVar]
+    let castExpr ← mkAppOptM `Rat.cast #[mkConst `Real, none, ratVar]
     (_, mv) ← mv.generalize #[{ expr := castExpr, xName? := varName }]
 
   for natVar in sortedNatVars do
@@ -751,14 +749,10 @@ def smt_translate (mv' : MVarId) : MetaM MVarId := withTraceNode `smt.reconstruc
 
   return mv
 
-namespace Tactic
+def smtTranslate (mv : MVarId) : MetaM Result := do
+  let mv ← smtTranslateCore mv
+  trace[smt.preprocess] m!"final translated goal: {mv}"
+  let hs ← mv.withContext (return (← getPropHyps).map Expr.fvar)
+  return { map := {}, hs, mv }
 
-syntax (name := smt_translate) "smt_translate" : tactic
-
-open Lean.Elab Tactic in
-@[tactic smt_translate] def evalSmtTranslate : Tactic := fun _ => withMainContext do
-  let mv ← Tactic.getMainGoal
-  let mv ← SmtTranslate.smt_translate mv
-  replaceMainGoal [mv]
-
-end Tactic
+end Smt.Preprocess

Smt/Preprocess/NatAsInt.lean

@@ -1,5 +1,3 @@
-import Mathlib.Data.Nat.Cast.Order.Basic
-
 theorem Nat.forall_as_int (P : Nat → Prop) : (∀ x : Nat, P x) ↔ (∀ x : Int, x ≥ 0 → P x.toNat) := by
   constructor
   · intro h x x_nonneg
@@ -17,15 +15,15 @@ theorem Nat.exists_as_int (P : Nat → Prop) : (∃ x : Nat, P x) ↔ (∃ x : I
   constructor
   · intro h
     obtain ⟨x, hx⟩ := h
-    use x
+    exists x
     exact if_false_right.mp fun a => hx
   · intro h
     obtain ⟨x, hx⟩ := h
     let x_nat : Nat := x.toNat
     have h_nat : x = x_nat := by
       refine Int.eq_natCast_toNat.mpr ?_
       exact hx.1
-    use x_nat
+    exists x_nat
     unfold x_nat
     have : x ≥ 0 := hx.1
     exact hx.2 this
@@ -35,10 +33,10 @@ def Int.natSub (x y : Int) :=
 
 theorem Int.natCast_sub2 (x y : Nat) : (x - y : Nat) = Int.natSub x y := by
   rw [Int.natSub]
-  split_ifs with h
+  split <;> rename_i h
   · rw [Int.natCast_sub]
     exact Int.ofNat_le.mp h
-  · rw [Nat.sub_eq_zero_of_le (Nat.le_of_succ_le (Int.ofNat_lt.mp (not_le.mp h))), Int.natCast_zero]
+  · rw [Nat.sub_eq_zero_of_le (Nat.le_of_succ_le (Int.ofNat_lt.mp (Int.not_le.mp h))), Int.natCast_zero]
 
 theorem Int.ofNat_eq (x y : Nat) : (x = y) = ((x : Int) = (y : Int)) := by
   simp only [Int.ofNat_inj]
@@ -56,8 +54,8 @@ theorem Int.ofNat_gt (x y : Nat) : (x > y) = ((x : Int) > (y : Int)) := by
   simp only [gt_iff_lt, Int.ofNat_lt]
 
 theorem Int.ofNat_ne (x y : Nat) : x ≠ y ↔ ((x : Int) ≠ (y : Int)) := by
-  rw [← not_iff_not]
-  rw [not_not, not_not]
+  rw [← Decidable.not_iff_not]
+  rw [Decidable.not_not, Decidable.not_not]
   rw [Int.ofNat_inj]
 
 theorem doubleCast (p : Nat → Prop) (w : Nat) : p w = p (w : Int).toNat := by

Smt/Preprocess/RatAsReal.lean

@@ -1,7 +1,4 @@
 import Mathlib.Data.Real.Basic
-import Batteries.Data.Rat.Basic
-import Batteries.Classes.RatCast
-import Mathlib.Data.Rat.Cast.CharZero
 import Mathlib.Data.Rat.Cast.Order
 
 open Real

Smt/Reconstruct.lean

@@ -262,27 +262,29 @@ def defaultSolverOptions : List (String × String) := [
 open cvc5 in
 def solve (query : String) (timeout : Option Nat) (options : List (String × String)) : MetaM (Except cvc5.Error cvc5Result) :=
   profileitM Exception "smt" {} do
-  withTraceNode `smt.solve traceSolve do Solver.run (← TermManager.new) do
+  withTraceNode `smt.solve traceSolve do cvc5.run do
+    let tm ← TermManager.new
+    let slv ← Solver.new tm
     if let .some timeout := timeout then
       -- NOTE: `tlimit` wouldn't have any effect here, since we're not running in
       -- the binary, and because we only have a single `checkSat`, we can use
       -- `tlimit-per` instead to achieve the same effect.
-      Solver.setOption "tlimit-per" (toString (1000*timeout))
+      slv.setOption "tlimit-per" (toString (1000*timeout))
     for (opt, val) in options do
-      Solver.setOption opt val
-    let (uss, ufs) ← Solver.parseCommands query
-    let res ← Solver.checkSat
+      slv.setOption opt val
+    let (uss, ufs) ← slv.parseCommands query
+    let res ← slv.checkSat
     trace[smt.solve] m!"result: {res}"
     if res.isSat then
-      let iss ← uss.mapM fun us => return (us, ← Solver.getModelDomainElements us)
-      let ifs ← ufs.mapM fun uf => return (uf, ← Solver.getValue uf)
+      let iss ← uss.mapM fun us => return (us, ← slv.getModelDomainElements us)
+      let ifs ← ufs.mapM fun uf => return (uf, ← slv.getValue uf)
       trace[smt.solve] "model:\n{iss}\n{ifs}"
       return .sat { iss, ifs }
     else if res.isUnsat then
-      let ps ← Solver.getProof
-      let uc ← Solver.getUnsatCore
+      let ps ← slv.getProof
+      let uc ← slv.getUnsatCore
       if h : 0 < ps.size then
-        trace[smt.solve] "proof:\n{← Solver.proofToString ps[0]}"
+        trace[smt.solve] "proof:\n{← slv.proofToString ps[0]}"
         trace[smt.solve] "unsat-core:\n{uc}"
         return .unsat ps[0] uc
     else if res.isUnknown then

Smt/Reconstruct/Prop.lean

@@ -242,17 +242,13 @@ def reclausify (c : Array cvc5.Term) (l : cvc5.Term) : Array cvc5.Term :=
 def clausify (c l : cvc5.Term) : Array cvc5.Term :=
   reclausify (nary .OR c) l
 
+private def isNotOf (t₁ t₂ : cvc5.Term) : Bool :=
+  t₁.getKind == .NOT && t₁[0]! == t₂
+
 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
+  let l₁ := if pol.getBooleanValue! then (· == l) else (isNotOf · l)
+  let l₂ := if pol.getBooleanValue! then (isNotOf · l) else (· == l)
+  return c₁.eraseP l₁ ++ c₂.eraseP l₂
 
 def reconstructResolution (c₁ c₂ : Array cvc5.Term) (pol l : cvc5.Term) (hps hqs : Expr) : ReconstructM Expr := do
   let f t ps := do
@@ -262,7 +258,9 @@ def reconstructResolution (c₁ c₂ : Array cvc5.Term) (pol l : cvc5.Term) (hps
   let qs : Q(List Prop) ← c₂.foldrM f q([])
   let hps : Q(orN $ps) ← pure hps
   let hqs : Q(orN $qs) ← pure hqs
-  let (i?, j?) := if pol.getBooleanValue! then (c₁.finIdxOf? l, c₂.finIdxOf? l.not!) else (c₁.finIdxOf? l.not!, c₂.finIdxOf? l)
+  let (i?, j?) := if pol.getBooleanValue!
+    then (c₁.finIdxOf? l, c₂.findFinIdx? (isNotOf · l))
+    else (c₁.findFinIdx? (isNotOf · l), c₂.finIdxOf? l)
   if let (some ⟨i, _⟩, some ⟨j, _⟩) := (i?, j?) then
     let hi : Q($i < «$ps».length) := .app q(@of_decide_eq_true ($i < «$ps».length) _) q(Eq.refl true)
     let hj : Q($j < «$qs».length) := .app q(@of_decide_eq_true ($j < «$qs».length) _) q(Eq.refl true)

Smt/Reconstruct/Rat.lean

@@ -25,7 +25,7 @@ open Lean Qq
     | .DIV_BY_ZERO => return q(fun (x : Rat) => x / 0)
     | _ => return none
   | .CONST_RATIONAL =>
-    let c : Std.Internal.Rat := t.getRationalValue!
+    let c : Rat := t.getRationalValue!
     let num : Q(Rat) := mkRatLit c.num.natAbs
     if c.den == 1 then
       if c.num ≥ 0 then
@@ -342,7 +342,7 @@ where
       return ha
 
 def reconstructArithPolyNormRel (pf : cvc5.Proof) : ReconstructM (Option Expr) := do
-  let lcx : Std.Internal.Rat := pf.getChildren[0]!.getResult[0]![0]!.getRationalValue!
+  let lcx : Rat := pf.getChildren[0]!.getResult[0]![0]!.getRationalValue!
   let cx : Q(Rat) ← reconstructTerm pf.getChildren[0]!.getResult[0]![0]!
   let cy : Q(Rat) ← reconstructTerm pf.getChildren[0]!.getResult[1]![0]!
   let x₁ : Q(Rat) ← reconstructTerm pf.getResult[0]![0]!