Update Lean toolchain to v4.26.0.

Author: abdoo8080

Smt/Preprocess/Embedding/Nat.lean

@@ -49,15 +49,15 @@ theorem Int.toNat_eq_toNat_of_nonneg {x y : Int} (hx : x ≥ 0) (hy : y ≥ 0) :
   | .negSucc n, _ => contradiction
   | _, .negSucc m => contradiction
   | .ofNat n, .ofNat m =>
-    simp only [Int.ofNat_eq_coe, Int.toNat_natCast, Int.natCast_inj]
+    simp only [Int.ofNat_eq_natCast, Int.toNat_natCast, Int.natCast_inj]
 
 @[embedding ↓]
 theorem Int.toNat_ne_toNat_of_nonneg {x y : Int} (hx : x ≥ 0) (hy : y ≥ 0) : (x.toNat ≠ y.toNat) ↔ (x ≠ y) := by
   match x, y with
   | .negSucc n, _ => contradiction
   | _, .negSucc m => contradiction
   | .ofNat n, .ofNat m =>
-    simp only [Int.ofNat_eq_coe, Int.toNat_natCast, ne_eq, Int.natCast_inj]
+    simp only [Int.ofNat_eq_natCast, Int.toNat_natCast, ne_eq, Int.natCast_inj]
 
 namespace Smt.Preprocess.Embedding
 

Smt/Reconstruct/Rat/Core.lean

@@ -182,7 +182,7 @@ protected theorem sub_nonneg {a b : Rat} : 0 ≤ a - b ↔ b ≤ a := by
 
 theorem divInt_pos_iff_of_pos_right {a b : Int} (hb : 0 < b) : 0 < a /. b ↔ 0 < a := by
   cases hab : a /. b with | mk' n d hd hnd =>
-  rw [mk'_eq_divInt, divInt_eq_divInt_iff (Int.ne_of_lt hb).symm (mod_cast hd)] at hab
+  rw [mk_eq_divInt, divInt_eq_divInt_iff (Int.ne_of_lt hb).symm (mod_cast hd)] at hab
   rw [ ← Rat.num_pos, <- Int.mul_pos_iff_of_pos_right hb, <- hab,
        Int.mul_pos_iff_of_pos_right (mod_cast Nat.pos_of_ne_zero hd)]
 
@@ -291,12 +291,12 @@ theorem floor_def' (a : Rat) : a.floor = a.num / a.den := by
   · next h => simp [h]
   · next => rfl
 
-theorem intCast_eq_divInt (z : Int) : (z : Rat) = z /. 1 := mk'_eq_divInt
+theorem intCast_eq_divInt (z : Int) : (z : Rat) = z /. 1 := mk_eq_divInt
 
 theorem le_floor {z : Int} : ∀ {r : Rat}, z ≤ Rat.floor r ↔ (z : Rat) ≤ r
   | ⟨n, d, h, c⟩ => by
     simp only [Rat.floor_def']
-    rw [mk'_eq_divInt]
+    rw [mk_eq_divInt]
     have h' := Int.ofNat_lt.2 (Nat.pos_of_ne_zero h)
     conv =>
       rhs

Smt/Reconstruct/Rat/Lemmas.lean

@@ -144,10 +144,10 @@ theorem add_nonneg : 0 ≤ a → 0 ≤ b → 0 ≤ a + b :=
     apply Int.add_nonneg
     · apply Int.mul_nonneg
       · exact (Rat.divInt_nonneg_iff_of_pos_right d₁0).mp n₁0
-      · exact Int.ofNat_zero_le d₂
+      · exact Int.natCast_nonneg d₂
     · apply Int.mul_nonneg
       · exact (Rat.divInt_nonneg_iff_of_pos_right d₂0).mp n₂0
-      · exact Int.ofNat_zero_le d₁
+      · exact Int.natCast_nonneg d₁
 
 theorem le_trans (hab : a ≤ b) (hbc : b ≤ c) : a ≤ c := by
   rw [Rat.le_iff_sub_nonneg] at hab hbc

Smt/Reconstruct/Real/Lemmas.lean

@@ -17,41 +17,40 @@ namespace Smt.Reconstruct.Real
 variable {a b c d x₁ x₂ y₁ y₂ : Real}
 
 theorem sum_ub₁ (h₁ : a < b) (h₂ : c < d) : a + c < b + d := by
-  have r₁ : a + c < a + d := add_lt_add_left h₂ a
-  have r₂ : a + d < b + d := add_lt_add_right h₁ d
+  have r₁ : a + c < a + d := add_lt_add_right h₂ a
+  have r₂ : a + d < b + d := add_lt_add_left h₁ d
   exact lt_trans r₁ r₂
 
 theorem sum_ub₂ (h₁ : a < b) (h₂ : c ≤ d) : a + c < b + d := by
-  have r₁ : a + c ≤ a + d := add_le_add_left h₂ a
-  have r₂ : a + d < b + d := add_lt_add_right h₁ d
+  have r₁ : a + c ≤ a + d := add_le_add_right h₂ a
+  have r₂ : a + d < b + d := add_lt_add_left h₁ d
   exact lt_of_le_of_lt r₁ r₂
 
 theorem sum_ub₃ (h₁ : a < b) (h₂ : c = d) : a + c < b + d := by
   rewrite [h₂]
-  exact add_lt_add_right h₁ d
+  exact add_lt_add_left h₁ d
 
 theorem sum_ub₄ (h₁ : a ≤ b) (h₂ : c < d) : a + c < b + d := by
-  have r₁ : a + c < a + d := add_lt_add_left h₂ a
-  have r₂ : a + d ≤ b + d := add_le_add_right h₁ d
+  have r₁ : a + c < a + d := add_lt_add_right h₂ a
+  have r₂ : a + d ≤ b + d := add_le_add_left h₁ d
   exact lt_of_lt_of_le r₁ r₂
 
 theorem sum_ub₅ (h₁ : a ≤ b) (h₂ : c ≤ d) : a + c ≤ b + d := by
-  have r₁ : a + c ≤ a + d := add_le_add_left h₂ a
-  have r₂ : a + d ≤ b + d := add_le_add_right h₁ d
+  have r₁ : a + c ≤ a + d := add_le_add_right h₂ a
+  have r₂ : a + d ≤ b + d := add_le_add_left h₁ d
   exact le_trans r₁ r₂
 
 theorem sum_ub₆ (h₁ : a ≤ b) (h₂ : c = d) : a + c ≤ b + d := by
   rewrite [h₂]
-  exact add_le_add_right h₁ d
+  exact add_le_add_left h₁ d
 
 theorem sum_ub₇ (h₁ : a = b) (h₂ : c < d) : a + c < b + d := by
   rewrite [h₁]
-  exact add_lt_add_left h₂ b
+  exact add_lt_add_right h₂ b
 
 theorem sum_ub₈ (h₁ : a = b) (h₂ : c ≤ d) : a + c ≤ b + d := by
   rewrite [h₁]
-  exact add_le_add_left h₂ b
-
+  exact add_le_add_right h₂ b
 theorem sum_ub₉ (h₁ : a = b) (h₂ : c = d) : a + c = b + d := by
   rw [h₁, h₂]
 

Smt/Reconstruct/Real/TransFns/ArithTransSineShift.lean

@@ -87,7 +87,7 @@ theorem arithTransSineShift₀ : ∀ x , ∃ s y , shift_prop x s y := fun x =>
         have := Int.ceil_le_floor_add_one ((x - Real.pi) / (2 * Real.pi))
         apply le_trans (Int.cast_le.mpr this)
         have : Int.floor ((x - Real.pi) / (2 * Real.pi)) + 1 ≤ (x - Real.pi) / (2 * Real.pi) + 1 :=
-          add_le_add_right (Int.floor_le _) 1
+          add_le_add_left (Int.floor_le _) 1
         simp only [Int.cast_add, Int.cast_one, ge_iff_le]
         apply le_trans this
         rw [← div_add_same two_pi_ne_zero, tau]

Smt/Reconstruct/UF.lean

@@ -35,7 +35,7 @@ def getFVarOrConstExpr! (n : String) : ReconstructM Expr := do
   | .UNINTERPRETED_SORT_VALUE =>
     let some n := (← read).sortCard[t.getSort]? | throwError "unknown sort {t.getSort}"
     let s := t.toString
-    let endPos := (s.endPos - t.getSort.toString).decreaseBy 2
+    let endPos := (s.rawEndPos - t.getSort.toString).decreaseBy 2
     let endPos := if endPos.dec.get? s == some '|' then endPos.dec else endPos
     let startPos := (s.revFindAux (· != '_') endPos).get!
     let i : Nat := (String.Pos.Raw.extract s startPos endPos).toNat!

Smt/Translate/String.lean

@@ -29,8 +29,9 @@ private def mkString : Expr :=
 @[smt_translate] def translateString : Translator := fun e => do
   if let .lit (.strVal s) := e then
     return literalT s!"\"{s}\""
-  else if let some (z, x, y) := e.app3? ``String.replace then
-    return mkApp3 (symbolT "str.replace_all") (← applyTranslators! z) (← applyTranslators! x) (← applyTranslators! y)
+  else if e.isAppOfArity ``String.replace 11 then
+    let #[_, _, _, _, _, _, _, _, x, y, z] := e.getAppArgsN 11 | return none
+    return mkApp3 (symbolT "str.replace_all") (← applyTranslators! x) (← applyTranslators! y) (← applyTranslators! z)
   else if let some (x, y) := e.hAppendOf? mkString mkString then
     return mkApp2 (symbolT "str.++") (← applyTranslators! x) (← applyTranslators! y)
   else

Test/BitVec/Shift.expected

@@ -2,17 +2,17 @@ goal: x ++ y = zeroExtend 4 x <<< 2#2 ||| zeroExtend 4 y
 
 query:
 (set-logic ALL)
-(declare-const y (_ BitVec 2))
 (declare-const x (_ BitVec 2))
+(declare-const y (_ BitVec 2))
 (assert (not (= (concat x y) (bvor (bvshl ((_ zero_extend 2) x) #b10) ((_ zero_extend 2) y)))))
 (check-sat)
 Test/BitVec/Shift.lean:5:8: warning: declaration uses 'sorry'
 goal: x ++ y = zeroExtend 6 x <<< 3#2 ||| zeroExtend 6 y
 
 query:
 (set-logic ALL)
-(declare-const x (_ BitVec 3))
 (declare-const y (_ BitVec 3))
+(declare-const x (_ BitVec 3))
 (assert (not (= (concat x y) (bvor (bvshl ((_ zero_extend 3) x) #b11) ((_ zero_extend 3) y)))))
 (check-sat)
 Test/BitVec/Shift.lean:10:8: warning: declaration uses 'sorry'

Test/BitVec/XorComm.expected

@@ -2,17 +2,17 @@ goal: x ^^^ y = y ^^^ x
 
 query:
 (set-logic ALL)
-(declare-const x (_ BitVec 2))
 (declare-const y (_ BitVec 2))
+(declare-const x (_ BitVec 2))
 (assert (not (= (bvxor x y) (bvxor y x))))
 (check-sat)
 Test/BitVec/XorComm.lean:3:8: warning: declaration uses 'sorry'
 goal: x ^^^ y = y ^^^ x
 
 query:
 (set-logic ALL)
-(declare-const y (_ BitVec 8))
 (declare-const x (_ BitVec 8))
+(declare-const y (_ BitVec 8))
 (assert (not (= (bvxor x y) (bvxor y x))))
 (check-sat)
 Test/BitVec/XorComm.lean:7:8: warning: declaration uses 'sorry'

Test/Bool/Assoc.expected

@@ -2,5 +2,5 @@ Test/Bool/Assoc.lean:5:2: error: unable to prove goal, either it is false or you
 
   f = fun _arg_1 _arg_2 => if _arg_1 then ¬_arg_2 else ¬_arg_1 ∧ ¬_arg_2
   r = False
-  p = True
   q = False
+  p = True