Update Lean toolchain to v4.29.0.

Author: abdoo8080

Smt/Reconstruct.lean

@@ -321,7 +321,7 @@ def solve (query : String) (timeout : Option Nat) (prove : Bool := true) (option
       where each entry is the Lean reconstruction of either a declared sort (paired with a
       `Fin n` standing for its finite domain) or a declared function/constant (paired with the
       value cvc5 assigned to it).
-    * `unsat hp mvs usedHints` — the query is unsatisfiable.
+    * `unsat hp mvs uc` — the query is unsatisfiable.
         - `hp` is the reconstructed proof term, or `none` when proof reconstruction was disabled
           (i.e. the call was made with `prove := false`). See `solveAndReconstructProof` for the
           shape of its type.
@@ -332,13 +332,13 @@ def solve (query : String) (timeout : Option Nat) (prove : Bool := true) (option
           the caller to discharge. These should be **rare in practice and worth flagging** when
           they appear: a non-empty `mvs` means part of the cvc5 proof was trusted rather than
           checked.
-        - `usedHints` is the unsat core returned by cvc5, with each assertion reconstructed as a
+        - `uc` is the unsat core returned by cvc5, with each assertion reconstructed as a
           Lean `Expr`.
     * `unknown reason` — cvc5 returned `unknown`; `reason` is the stringified
       `cvc5.UnknownExplanation`. -/
 inductive SolveReconstructResult where
   | sat (model : Array (Expr × Expr))
-  | unsat (hp : Option Expr) (mvs : List MVarId) (usedHints : Array Expr)
+  | unsat (hp : Option Expr) (mvs : List MVarId) (uc : Array Expr)
   | unknown (reason : String)
 
 open Qq in
@@ -393,7 +393,7 @@ open Qq in
     degenerates to `True → ¬ andN as`; with a single assertion the conclusion is `¬ a₁`; with no
     assertions at all it is `¬ True`. -/
 def solveAndReconstructProof (query : String)
-  (timeout : Option Nat) (prove : Bool := true)
+  (timeout : Option Nat := none) (prove : Bool := true)
   (options : List (String × String) := defaultSolverOptions ++ (if prove then [("produce-proofs", "true")] else []))
   (userNames : Std.HashMap String Expr := {}) (native : Bool := false) : MetaM SolveReconstructResult :=
   profileitM Exception "smt" {} do
@@ -438,7 +438,7 @@ open Lean.Elab Tactic in
 @[tactic reconstruct] def evalReconstruct : Tactic := fun stx =>
   withMainContext do
     let some query := stx[1].isStrLit? | throwError "expected string"
-    let r ← solveAndReconstructProof query none true (defaultSolverOptions) (← getUserNames)
+    let r ← solveAndReconstructProof query (userNames := ← getUserNames)
     match r with
     | .unknown reason =>
       throwError m!"solver returned unknown: {reason}"
@@ -455,7 +455,6 @@ open Lean.Elab Tactic in
       for (v, t) in model do
         md := md ++ m!"\n  {v} = {t}"
       logInfo md
-
 where
   getUserNames : MetaM (Std.HashMap String Expr) := do
     let lCtx ← getLCtx

Smt/Reconstruct/Builtin.lean

@@ -266,17 +266,13 @@ where
   decide (p : Q(Prop)) (hp : Q(Decidable $p)) : MetaM Q($p) := do
     return .app q(@of_decide_eq_true $p $hp) q(Eq.refl true)
   nativeDecide (p : Q(Prop)) (hp : Q(Decidable $p)) : MetaM Q($p) := do
-    let auxDeclName ← mkNativeAuxDecl `_nativePolynorm q(Bool) q(decide $p)
-    let b : Q(Bool) := .const auxDeclName []
-    return .app q(@of_decide_eq_true $p $hp) (.app q(Lean.ofReduceBool $b true) q(Eq.refl true))
-  mkNativeAuxDecl (baseName : Name) (type value : Expr) : MetaM Name := do
-    let auxName ← Lean.mkAuxDeclName baseName
-    let decl := Declaration.defnDecl {
-      name := auxName, levelParams := [], type, value
-      hints := .abbrev
-      safety := .safe
-    }
-    addAndCompile decl
-    pure auxName
+    match ← Meta.nativeEqTrue `Smt.eval q(decide $p) with
+    | .notTrue =>
+      throwError m!"[smt_eval] evaluated that the proposition
+        {indentExpr q(decide $p)}\n\
+        is false"
+    | .success hdp =>
+      -- get instance from `d`
+      return .app q(@of_decide_eq_true $p $hp) hdp
 
 end Smt.Reconstruct.Builtin

Smt/Reconstruct/Builtin/Tactic.lean

@@ -64,18 +64,14 @@ def nativeAbsorb (mv : MVarId) (zero op : Expr) : MetaM Unit := do
 where
   nativeDecide (p : Q(Prop)) : MetaM Q($p) := do
     let hp : Q(Decidable $p) ← Meta.synthInstance q(Decidable $p)
-    let auxDeclName ← mkNativeAuxDecl `_nativePolynorm q(Bool) q(decide $p)
-    let b : Q(Bool) := .const auxDeclName []
-    return .app q(@of_decide_eq_true $p $hp) (.app q(Lean.ofReduceBool $b true) q(Eq.refl true))
-  mkNativeAuxDecl (baseName : Name) (type value : Expr) : MetaM Name := do
-    let auxName ← Lean.mkAuxDeclName baseName
-    let decl := Declaration.defnDecl {
-      name := auxName, levelParams := [], type, value
-      hints := .abbrev
-      safety := .safe
-    }
-    addAndCompile decl
-    pure auxName
+    match ← Meta.nativeEqTrue `Smt.absorb q(decide $p) with
+    | .notTrue =>
+      throwError m!"[poly_norm] evaluated that the proposition
+        {indentExpr q(decide $p)}\n\
+        is false"
+    | .success hdp =>
+      -- get instance from `d`
+      return .app q(@of_decide_eq_true $p $hp) hdp
 
 namespace Tactic
 

Smt/Reconstruct/Int/Polynorm.lean

@@ -366,18 +366,14 @@ where
     logInfo m!"poly := {PolyNorm.Polynomial.toExpr p.toPolynomial ppCtx}"
   nativeDecide (p : Q(Prop)) : MetaM Q($p) := do
     let hp : Q(Decidable $p) ← Meta.synthInstance q(Decidable $p)
-    let auxDeclName ← mkNativeAuxDecl `_nativePolynorm q(Bool) q(decide $p)
-    let b : Q(Bool) := .const auxDeclName []
-    return .app q(@of_decide_eq_true $p $hp) (.app q(Lean.ofReduceBool $b true) q(Eq.refl true))
-  mkNativeAuxDecl (baseName : Name) (type value : Expr) : MetaM Name := do
-    let auxName ← Lean.mkAuxDeclName baseName
-    let decl := Declaration.defnDecl {
-      name := auxName, levelParams := [], type, value
-      hints := .abbrev
-      safety := .safe
-    }
-    addAndCompile decl
-    pure auxName
+    match ← Meta.nativeEqTrue `Smt.polynorm q(decide $p) with
+    | .notTrue =>
+      throwError m!"[poly_norm] evaluated that the proposition
+        {indentExpr q(decide $p)}\n\
+        is false"
+    | .success hdp =>
+      -- get instance from `d`
+      return .app q(@of_decide_eq_true $p $hp) hdp
 
 namespace Tactic
 

Smt/Reconstruct/Rat/Core.lean

@@ -11,8 +11,6 @@ namespace Rat
 
 variable (x y a b c q : Rat)
 
-protected def abs (x : Rat) := if x < 0 then -x else x
-
 instance : NatPow Rat where
   pow := Rat.pow
 
@@ -58,14 +56,6 @@ theorem mk'_zero (d) (h : d ≠ 0) (w) : mk' 0 d h w = 0 := by
   congr
   apply Nat.coprime_zero_left d |>.mp w
 
-theorem eq_iff_mul_eq_mul {p q : Rat} : p = q ↔ p.num * q.den = q.num * p.den := by
-  conv =>
-    lhs
-    rw [← num_divInt_den p, ← num_divInt_den q]
-  apply Rat.divInt_eq_divInt_iff <;>
-    · rw [← Int.natCast_zero, Ne, Int.ofNat_inj]
-      apply den_nz
-
 protected theorem lt_iff_blt {x y : Rat} : x < y ↔ x.blt y := by
   simp only [LT.lt]
 
@@ -103,11 +93,6 @@ protected theorem mul_eq_zero_iff : a * b = 0 ↔ a = 0 ∨ b = 0 := by
 protected theorem mul_ne_zero_iff : a * b ≠ 0 ↔ a ≠ 0 ∧ b ≠ 0 := by
   simp only [not_congr (Rat.mul_eq_zero_iff a b), not_or, ne_eq]
 
-@[simp]
-theorem neg_neg : - -q = q := by
-  rewrite [← Rat.mkRat_self q, Rat.neg_mkRat, Rat.neg_mkRat]
-  simp
-
 theorem num_ne_zero : q.num ≠ 0 ↔ q ≠ 0 := not_congr num_eq_zero
 
 theorem nonneg_iff_sub_nonpos : 0 ≤ q ↔ -q ≤ 0 := by
@@ -158,14 +143,8 @@ theorem num_neg : q.num < 0 ↔ q < 0 := by
 theorem num_neg_eq_neg_num (q : Rat) : (-q).num = -q.num :=
   rfl
 
-@[simp]
-protected theorem sub_self : x - x = 0 :=
-  numDenCasesOn' x fun nx dx h_dx => by
-    rw [Rat.divInt_sub_divInt _ _ (Int.natCast_ne_zero.mpr h_dx) (Int.natCast_ne_zero.mpr h_dx)]
-    simp
-
 protected theorem add_neg_self : x + -x = 0 :=
-  Rat.sub_eq_add_neg x x ▸ Rat.sub_self x
+  Rat.sub_eq_add_neg x x ▸ Rat.sub_self
 
 protected theorem eq_neg_of_add_eq_zero_left : x + y = 0 → x = - y :=
   numDenCasesOn'' x fun nx dx h_dx h_dx_red =>
@@ -205,7 +184,7 @@ protected theorem divInt_le_divInt
 
 theorem cast_lt1 {a b : Int} : Rat.ofInt a < Rat.ofInt b -> a < b := by
   intro h
-  simp [Rat.instLT, Rat.ofInt] at h
+  simp [Rat.lt_iff_blt, Rat.ofInt] at h
   simp [Rat.blt] at h
   cases h with
   | inl h =>
@@ -220,7 +199,7 @@ theorem cast_lt1 {a b : Int} : Rat.ofInt a < Rat.ofInt b -> a < b := by
 
 theorem cast_lt2 {a b : Int} : a < b → Rat.ofInt a < Rat.ofInt b := by
   intro h
-  simp only [instLT, ofInt, mk_den_one]
+  simp only [Rat.lt_iff_blt, ofInt, mk_den_one]
   simp [Rat.blt]
   cases Classical.em (a = 0) with
   | inl ha => simp [ha]; rw [ha] at h; exact h
@@ -236,7 +215,7 @@ theorem cast_lt' {a b : Int} : a < b ↔ Rat.ofInt a < Rat.ofInt b :=
 
 theorem cast_le1 {a b : Int} : Rat.ofInt a ≤ Rat.ofInt b -> a ≤ b := by
   intro h
-  simp only [instLE, ofInt, mk_den_one] at h
+  simp only [Rat.le_iff_blt, ofInt, mk_den_one] at h
   simp [Rat.blt] at h
   cases Classical.em (b = 0) with
   | inl hb =>
@@ -260,7 +239,7 @@ theorem cast_le1 {a b : Int} : Rat.ofInt a ≤ Rat.ofInt b -> a ≤ b := by
 
 theorem cast_le2 {a b : Int} : a ≤ b → Rat.ofInt a ≤ Rat.ofInt b := by
   intro h
-  simp [Rat.instLE, Rat.ofInt]
+  simp [Rat.le_iff_blt, Rat.ofInt]
   simp [Rat.blt]
   cases Classical.em (b = 0) with
   | inl hb =>
@@ -303,13 +282,6 @@ theorem le_floor {z : Int} : ∀ {r : Rat}, z ≤ Rat.floor r ↔ (z : Rat) ≤
       rw [Rat.intCast_eq_divInt, Rat.divInt_le_divInt Int.zero_lt_one h', Int.mul_one]
     exact Int.le_ediv_iff_mul_le h'
 
-@[simp]
-protected theorem neg_zero : -(0:Rat) = 0 := rfl
-
-protected theorem neg_add (a b : Rat) : -(a + b) = -a + -b := by
-  rw [←Rat.sub_eq_add_neg, ←Rat.neg_neg b, ←Rat.sub_eq_add_neg, Rat.neg_sub]
-  simp [Rat.sub_eq_add_neg, Rat.add_comm, Rat.neg_neg]
-
 theorem neg_eq_neg_one_mul (a : Rat) : -a = -1 * a :=
   numDenCasesOn a fun n d h h1 => by
     simp [Rat.neg_mkRat, Rat.mul_def, Rat.normalize_eq_mkRat]