Update to v4.26.0-rc2

Author: JOSHCLUNE

Auto/Embedding/LCtx.lean

@@ -495,7 +495,7 @@ section push
     pushLCtxs (x :: xs) lctx = pushLCtx x (pushLCtxs xs lctx) := by
     apply funext; intros n; cases n
     case h.zero =>
-      dsimp [pushLCtxs, pushLCtx, Nat.blt, Nat.ble]; rw [Nat.zero_ble]
+      dsimp [pushLCtxs, pushLCtx, Nat.blt, Nat.ble]
     case h.succ n =>
       dsimp [pushLCtxs, pushLCtx, Nat.blt, Nat.ble]; rw [Nat.succ_sub_succ]
 
@@ -515,7 +515,7 @@ section push
 
   theorem pushLCtxs_cons_zero (xs : List α) (lctx : Nat → α) :
     pushLCtxs (x :: xs) lctx 0 = x := by
-    dsimp [pushLCtxs, Nat.blt, Nat.ble]; rw [Nat.zero_ble]
+    dsimp [pushLCtxs, Nat.blt, Nat.ble]
 
   theorem pushLCtxs_cons_succ (xs : List α) (lctx : Nat → α) (n : Nat) :
     pushLCtxs (x :: xs) lctx (.succ n) = pushLCtxs xs lctx n := by
@@ -612,8 +612,7 @@ section push
     apply HEq.funext; intros n; cases n
     case zero =>
       dsimp [pushLCtxs, pushLCtx, Nat.blt, Nat.ble]
-      rw [Nat.ble_eq_true_of_le]; rfl
-      apply Nat.zero_le
+      rfl
     case succ n =>
       dsimp [pushLCtxs, pushLCtx, Nat.blt, Nat.ble]
       rw [Nat.succ_sub_succ]; rfl
@@ -623,8 +622,7 @@ section push
     (xs : HList lctxty tys) {rty : Nat → α} (lctx : ∀ n, lctxty (rty n)) :
     HEq (pushLCtxsDep (.cons x xs) lctx 0) x := by
     dsimp [pushLCtxs, Nat.blt, Nat.ble];
-    rw [Nat.ble_eq_true_of_le]; rfl
-    apply Nat.zero_le
+    rfl
 
   theorem pushLCtxsDep_cons_succ
     {lctxty : α → Sort u} {ty : α} (x : lctxty ty) {tys : List α}
@@ -771,9 +769,7 @@ section push
       dsimp at heq; rw [← heq]
       rw [HList.ofFun_succ];
       congr
-      case e_3.h => dsimp; rw [pushLCtxs_cons_zero]
       case e_4.h => dsimp; rw [pushLCtxs_cons_succ_Fn]; apply List.ofFun_ofPushLCtx; rfl
-      case e_5 => apply pushLCtxsDep_cons_zero
       case e_6 =>
         apply HEq.trans _ (ofFun_ofPushLCtxDep rfl xs lctx)
         congr

Auto/Embedding/LamBase.lean

@@ -2569,7 +2569,7 @@ theorem LamTerm.maxLooseBVarSucc.spec (m : Nat) :
     let IH' := Nat.pred_le_pred (IH.mp h)
     rw [Nat.pred_succ] at IH'; exact IH'
   case mpr =>
-    apply IH.mpr; apply Nat.lt_pred_iff_succ_lt.mp; exact h
+    apply IH.mpr; apply Nat.lt_pred_iff.mp; exact h
 | .app _ t₁ t₂ => by
   dsimp [hasLooseBVarGe, maxLooseBVarSucc];
   rw [Bool.or_eq_true]; rw [spec m t₁]; rw [spec m t₂];

Auto/Embedding/LamBitVec.lean

@@ -66,7 +66,7 @@ namespace BVLems
       have hle := of_decide_eq_true hdec
       rw [Bool.dite_eq_true (proof:=hle), toNat_zeroExtend']
       rw [Nat.mod_eq_of_lt]; rcases a with ⟨⟨a, isLt⟩⟩;
-      apply Nat.le_trans isLt; apply Nat.pow_le_pow_right (Nat.le_step .refl) hle
+      apply Nat.le_trans isLt; apply Nat.pow_le_pow_right (Nat.le_succ_of_le .refl) hle
 
   theorem toNat_sub (a b : BitVec n) : (a - b).toNat = (2 ^ n - b.toNat + a.toNat) % (2 ^ n) := rfl
 
@@ -93,12 +93,12 @@ namespace BVLems
   theorem ushiftRight_ge_length_eq_zero (a : BitVec n) (i : Nat) : i ≥ n → a >>> i = 0#n := by
     intro h; apply eq_of_val_eq; rw [toNat_ushiftRight, toNat_ofNat]
     apply (Nat.le_iff_div_eq_zero (Nat.two_pow_pos _)).mpr
-    apply Nat.le_trans (toNat_le _) (Nat.pow_le_pow_right (.step .refl) h)
+    apply Nat.le_trans (toNat_le _) (Nat.pow_le_pow_right (Nat.lt_succ_of_lt .refl) h)
 
   theorem ushiftRight_ge_length_eq_zero' (a : BitVec n) (i : Nat) : i ≥ n → BitVec.ofNat n (a.toNat >>> i) = 0#n := by
     intro h; apply congrArg (@BitVec.ofNat n)
     rw [Nat.shiftRight_eq_div_pow, Nat.le_iff_div_eq_zero (Nat.two_pow_pos _)]
-    apply Nat.le_trans (toNat_le _) (Nat.pow_le_pow_right (.step .refl) h)
+    apply Nat.le_trans (toNat_le _) (Nat.pow_le_pow_right (Nat.lt_succ_of_lt .refl) h)
 
   theorem msb_equiv_lt (a : BitVec n) : !a.msb ↔ a.toNat < 2 ^ (n - 1) := by
     dsimp [BitVec.msb, BitVec.getMsbD, BitVec.getLsbD]
@@ -116,32 +116,37 @@ namespace BVLems
     case succ n =>
       rw [Nat.succ_sub_one, Nat.pow_succ, Nat.mul_comm (m:=2)]
       apply Iff.symm; apply Nat.mul_lt_mul_left
-      exact .step .refl
+      exact Nat.lt_succ_of_lt .refl
 
   theorem sshiftRight_ge_length_eq_msb (a : BitVec n) (i : Nat) : i ≥ n → a.sshiftRight i =
     if a.msb then (1#n).neg else 0#n := by
     intro h; simp only [sshiftRight, BitVec.toInt, ← msb_equiv_lt']
-    cases hmsb : a.msb <;> simp only [Int.shiftRight_def] <;> dsimp
+    cases hmsb : a.msb <;> simp only [Int.shiftRight_def]
     case false =>
+      dsimp only [Bool.not_false, ↓dreduceIte, Int.ofNat_eq_natCast, Int.natCast_shiftRight, Bool.false_eq_true]
       rw [BitVec.ofNat]
       apply ushiftRight_ge_length_eq_zero'; exact h
     case true =>
       rw [← Int.subNatNat_eq_coe, Int.subNatNat_of_lt (toNat_le _)]
-      simp only [BitVec.ofInt]; dsimp
+      simp only [BitVec.ofInt]
+      dsimp only [Bool.not_true, Bool.false_eq_true, ↓dreduceIte,
+        Nat.pred_eq_sub_one, Int.ofNat_eq_natCast, Int.natCast_shiftRight, Int.natCast_pow,
+        Int.cast_ofNat_Int, neg_eq]
       have hzero : (2 ^ n - BitVec.toNat a - 1) >>> i = 0 := by
         rw [Nat.shiftRight_eq_div_pow]; apply (Nat.le_iff_div_eq_zero (Nat.two_pow_pos _)).mpr
         rw [Nat.sub_one, Nat.pred_lt_iff_le (Nat.two_pow_pos _)]
-        apply Nat.le_trans (Nat.sub_le _ _) (Nat.pow_le_pow_right (.step .refl) h)
+        apply Nat.le_trans (Nat.sub_le _ _) (Nat.pow_le_pow_right (Nat.lt_succ_of_lt .refl) h)
       apply eq_of_val_eq; rw [toNat_ofNatLt, hzero]
       rw [toNat_neg, Int.mod_def', Int.emod]
-      rw [Nat.zero_mod, Int.natAbs_natCast, Nat.succ_eq_add_one, Nat.zero_add]
-      rw [Int.subNatNat_of_sub_eq_zero ((Nat.sub_eq_zero_iff_le).mpr (Nat.two_pow_pos _))]
+      rw [Nat.zero_mod, Nat.succ_eq_add_one, Nat.zero_add]
+      rw [Int.subNatNat_of_sub_eq_zero (by grind)]
       rw [Int.toNat_natCast, BitVec.toNat_ofNat]
       cases n <;> try rfl
       case succ n =>
-        have hlt : 2 ≤ 2 ^ Nat.succ n := @Nat.pow_le_pow_right 2 (.step .refl) 1 (.succ n) (Nat.succ_le_succ (Nat.zero_le _))
+        have hlt : 2 ≤ 2 ^ Nat.succ n := @Nat.pow_le_pow_right 2 (Nat.lt_succ_of_lt .refl) 1 (.succ n) (Nat.succ_le_succ (Nat.zero_le _))
         rw [Nat.mod_eq_of_lt (a:=1) hlt]
-        rw [Nat.mod_eq_of_lt]; apply Nat.sub_lt (Nat.le_trans (.step .refl) hlt) .refl
+        rw [Nat.mod_eq_of_lt (by grind)]
+        grind
 
   theorem shiftRight_eq_zero_iff (a : BitVec n) (b : Nat) : a >>> b = 0#n ↔ a.toNat < 2 ^ b := by
     rw [ushiftRight_def]; rcases a with ⟨⟨a, isLt⟩⟩;
@@ -201,7 +206,7 @@ namespace BVLems
 
   theorem shl_toNat_equiv_short (a : BitVec n) (b : BitVec m) (h : m ≤ n) : a <<< b.toNat = a <<< (zeroExtend n b) := by
     apply eq_of_val_eq; rw [toNat_shiftLeft, smtshiftLeft_def, toNat_shiftLeft, toNat_zeroExtend, Nat.mod_eq_of_lt (a:=BitVec.toNat b)]
-    apply Nat.le_trans (toNat_le _) (Nat.pow_le_pow_right (.step .refl) h)
+    apply Nat.le_trans (toNat_le _) (Nat.pow_le_pow_right (Nat.lt_succ_of_lt .refl) h)
 
   theorem shl_toNat_equiv_long (a : BitVec n) (b : BitVec m) (h : m > n) : a <<< b.toNat =
     if (b >>> (BitVec.ofNat m n)) = 0#m then a <<< (zeroExtend n b) else 0 := by
@@ -244,7 +249,7 @@ namespace BVLems
 
   theorem lshr_toNat_equiv_short (a : BitVec n) (b : BitVec m) (h : m ≤ n) : a >>> b.toNat = a >>> (zeroExtend n b) := by
     apply eq_of_val_eq; rw [toNat_ushiftRight, smtushiftRight_def, toNat_ushiftRight, toNat_zeroExtend, Nat.mod_eq_of_lt]
-    apply Nat.le_trans (toNat_le _) (Nat.pow_le_pow_right (.step .refl) h)
+    apply Nat.le_trans (toNat_le _) (Nat.pow_le_pow_right (Nat.lt_succ_of_lt .refl) h)
 
   theorem lshr_toNat_equiv_long (a : BitVec n) (b : BitVec m) (h : m > n) : a >>> b.toNat =
     if (b >>> (BitVec.ofNat m n)) = 0#m then a >>> (zeroExtend n b) else 0 := by
@@ -289,7 +294,7 @@ namespace BVLems
 
   theorem ashr_toNat_equiv_short (a : BitVec n) (b : BitVec m) (h : m ≤ n) : a.sshiftRight b.toNat = a.sshiftRight (zeroExtend n b).toNat := by
     apply eq_of_val_eq; rw [toNat_zeroExtend, Nat.mod_eq_of_lt]
-    apply Nat.le_trans (toNat_le _) (Nat.pow_le_pow_right (.step .refl) h)
+    apply Nat.le_trans (toNat_le _) (Nat.pow_le_pow_right (Nat.lt_succ_of_lt .refl) h)
 
   theorem ashr_toNat_equiv_long (a : BitVec n) (b : BitVec m) (h : m > n) : a.sshiftRight b.toNat =
     if (b >>> (BitVec.ofNat m n)) = 0#m then a.sshiftRight (zeroExtend n b).toNat else (if a.msb then (1#n).neg else 0#n) := by

Auto/Embedding/LamChecker.lean

@@ -1664,7 +1664,7 @@ theorem EtomStep.eval_correct
           rw [Nat.beq_eq_false_of_ne (Nat.ne_of_lt hlt)]
         case right =>
           rw [LamTerm.maxEVarSucc_mkEq]; dsimp [LamTerm.maxEVarSucc]
-          rw [Nat.max_le]; apply And.intro (Nat.le_refl _) (Nat.le_step h₂')
+          rw [Nat.max_le]; apply And.intro (Nat.le_refl _) (Nat.le_succ_of_le h₂')
     | false => exact True.intro
   | .none => exact True.intro
 

Auto/Embedding/LamConv.lean

@@ -962,7 +962,6 @@ theorem LamWF.interp_instantiate1.{u}
   case eqBody => rw [pushLCtxAt_zero]
   case eqLarge =>
     apply eq_of_heq; apply LamWF.interp_heq <;> try rfl
-    case h.HLCtxTyEq => rw [pushLCtxAt_zero]
     case h.HLCtxTermEq =>
       apply HEq.trans (HEq.symm (pushLCtxAtDep_zero _ _)) _
       apply pushLCtxAtDep_heq <;> try rfl

Auto/EvaluateAuto/NameArr.lean

@@ -36,11 +36,11 @@ def Name.uniqRepr (n : Name) : String :=
 -/
 def Name.parseUniqRepr (n : String) : Name :=
   let compParse (s : String) : String ⊕ Nat := Id.run <| do
-    let s := s.data
+    let s := s.toList
     if s[0]? == '\\' then
       if let .some c := s[1]? then
         if c.isDigit then
-          return .inr ((String.toNat? (String.mk (s.drop 1))).getD 0)
+          return .inr ((String.toNat? (String.ofList (s.drop 1))).getD 0)
     let mut ret := ""
     let mut escape := false
     for c in s do

Auto/EvaluateAuto/OS.lean

@@ -12,14 +12,14 @@ def EvalProc.create (path : String) (args : Array String) : IO EvalProc :=
   IO.Process.spawn {stdin := .piped, stdout := .null, stderr := .null, cmd := path, args := args}
 
 def bashRepr (s : String) :=
-  "\"" ++ String.join (s.data.map go) ++ "\""
+  "\"" ++ String.join (s.toList.map go) ++ "\""
 where
   go : Char → String
   | '$' => "\\$"
   | '`' => "\\`"
   | '\"' => "\\\""
   | '\\' => "\\\\"
-  | c => String.mk [c]
+  | c => String.ofList [c]
 
 def runLeanFileUsingNewLeanProcess
   (leanFile : String) (memoryLimitKb : Nat) (timeLimitS : Nat) :

Auto/IR/SMT.lean

@@ -99,7 +99,7 @@ def SpecConst.toString : SpecConst → String
 | .binary bs => bs.foldl (fun acc b => acc.push (if b then '1' else '0')) "#b"
 | .num n     => ToString.toString (repr n)
 where specCharRepr (c : Char) : String :=
-  "\\u{" ++ String.mk (Nat.toDigits 16 c.toNat) ++ "}"
+  "\\u{" ++ String.ofList (Nat.toDigits 16 c.toNat) ++ "}"
 
 mutual
 

Auto/IR/TPTP_TH0.lean

@@ -60,7 +60,7 @@ def transNatConst (nc : NatConst) : String := "t_" ++ nc.reprAux.replace " " "_"
 def transIntConst (ic : IntConst) : String := "t_" ++ ic.reprAux
 
 def transString (s : String) : String :=
-  String.join (s.data.map (fun c => s!"d{c.toNat}"))
+  String.join (s.toList.map (fun c => s!"d{c.toNat}"))
 
 def transStringConst : StringConst → String
 | .strVal s  => "t_strVal_" ++ transString s

Auto/Lib/BinTree.lean

@@ -315,7 +315,7 @@ theorem insert'.correct₁ (bt : BinTree β) (n : Nat) (x : β) : n ≠ 0 → ge
   case ind =>
     intros n IH bt _
     have hne' : (n + 2) / 2 ≠ 0 := by
-      rw [Nat.add_div_right _ (.step .refl)]; intro h; cases h
+      rw [Nat.add_div_right _ (Nat.lt_succ_of_lt .refl)]; intro h; cases h
     let IH' := fun bt => IH bt hne'
     rw [get?'_succSucc, insert'.succSucc, left!.eq_def, right!.eq_def]
     cases (n + 2) % 2 <;> cases bt <;> dsimp <;> rw [IH']
@@ -349,7 +349,7 @@ theorem insert'.correct₂ (bt : BinTree β) (n₁ n₂ : Nat) (x : β) : n₁ 
         rw [heq, h]
       have hmod : ∀ {n n'}, (n % 2) = .succ n' → n % 2 = 1 := by
         intros n n' H;
-        have hle : (n % 2) < 2 := Nat.mod_lt _ (.step .refl)
+        have hle : (n % 2) < 2 := Nat.mod_lt _ (Nat.lt_succ_of_lt .refl)
         revert H hle; cases (n % 2)
         case zero => intro contra; cases contra
         case succ a =>