adaptations required for nightly-2024-02-18

Auto/Embedding/Lift.lean

@@ -1,4 +1,3 @@
-import Std.Data.Int.Basic
 import Std.Data.BitVec.Basic
 import Auto.Lib.IsomType
 import Auto.Lib.StringExtra

Auto/Lib/HList.lean

@@ -12,7 +12,7 @@ theorem HList.nil_IsomType : IsomType (HList β .nil) PUnit :=
    fun x => match x with | .nil => rfl, fun _ => rfl⟩
 
 theorem HList.cons_IsomType : IsomType (HList β (a :: as)) (β a × HList β as) :=
-  ⟨fun xs => match xs with | .cons x xs => (x, xs), fun (x, xs) => .cons x xs, 
+  ⟨fun xs => match xs with | .cons x xs => (x, xs), fun (x, xs) => .cons x xs,
    fun xs => match xs with | .cons _ _ => rfl,
    fun (_, _) => rfl⟩
 
@@ -72,7 +72,7 @@ theorem HList.append_assoc (xs : HList β as) (ys : HList β bs) (zs : HList β
       case Hβ => rw [List.append_assoc]
       case h₁ =>
         apply congr_hd_heq <;> try apply HEq.rfl;
-        rw [List.append_assoc]; apply HEq.rfl
+        rw [List.append_assoc]
       case h₂ => apply HEq.rfl
     case h₂ => exact IH
 
@@ -176,4 +176,4 @@ theorem HList.reverse_cons {x : β a} {xs : HList β as} :
   HEq ((HList.cons x xs).reverse) (xs.reverse.append (.cons x .nil)) :=
   reverseAux_eq_append (xs:=xs) (ys:=.cons x .nil)
 
-end Auto
+end Auto

Auto/Lib/NatExtra.lean

@@ -203,7 +203,7 @@ theorem Nat.le_pow (h : b ≥ 2) : a < b ^ a := by
     rw [Nat.testBit_to_div_mod, decide_eq_true_iff]; apply Iff.intro <;> intro h
     case mp =>
       have ⟨k, hk⟩ := Nat.mod_par h; clear h
-      have ⟨r, ⟨er, lr⟩⟩ := Nat.div_par hk (Nat.pow_two_pos _); clear hk; cases er
+      have ⟨r, ⟨er, lr⟩⟩ := Nat.div_par hk (Nat.two_pow_pos _); clear hk; cases er
       have eqi : 2 ^ i * (2 * k + 1) + r = 2 ^ (i + 1) * k + (2 ^ i + r) := by
         rw [Nat.mul_add _ _ 1, ← Nat.mul_assoc, Nat.pow_add, Nat.add_assoc]; simp
       rw [eqi, Nat.mul_add_mod]
@@ -213,13 +213,13 @@ theorem Nat.le_pow (h : b ≥ 2) : a < b ^ a := by
       rw [Nat.mod_eq_of_lt elt]; apply Nat.le_add_right
     case mpr =>
       generalize ek : a % 2 ^ (i + 1) = k at h
-      have lk : k < 2 ^ (i + 1) := by cases ek; apply Nat.mod_lt; apply Nat.pow_two_pos
+      have lk : k < 2 ^ (i + 1) := by cases ek; apply Nat.mod_lt; apply Nat.two_pow_pos
       have ⟨l, hl⟩ := Nat.mod_par ek; clear ek; cases hl
       have eqi : 2 ^ (i + 1) * l + k = 2 ^ i * (2 * l) + k := by
         rw [Nat.pow_add, Nat.mul_assoc]; simp
-      rw [eqi, Nat.mul_add_div (Nat.pow_two_pos _), Nat.mul_add_mod]
-      have kdge : k / (2 ^ i) > 0 := (Nat.le_div_iff_mul_le (Nat.pow_two_pos _)).mpr (by simp [h])
-      have kdle : k / (2 ^ i) < 2 := (Nat.div_lt_iff_lt_mul (Nat.pow_two_pos _)).mpr (by rw [Nat.pow_add, Nat.mul_comm] at lk; apply lk)
+      rw [eqi, Nat.mul_add_div (Nat.two_pow_pos _), Nat.mul_add_mod]
+      have kdge : k / (2 ^ i) > 0 := (Nat.le_div_iff_mul_le (Nat.two_pow_pos _)).mpr (by simp [h])
+      have kdle : k / (2 ^ i) < 2 := (Nat.div_lt_iff_lt_mul (Nat.two_pow_pos _)).mpr (by rw [Nat.pow_add, Nat.mul_comm] at lk; apply lk)
       have kone : k / (2 ^ i) = 1 := Nat.eq_iff_le_and_ge.mpr (And.intro (Nat.le_of_succ_le_succ kdle) kdge)
       rw [kone]; rfl
 
@@ -230,17 +230,17 @@ theorem Nat.le_pow (h : b ≥ 2) : a < b ^ a := by
     rw [Nat.testBit_true_iff]; have ⟨k, ek⟩ := Nat.lt_par h; clear h; cases ek
     have eqi : 2 ^ (i + 1 + k) - 1 = 2 ^ (i + 1) * (2 ^ k - 1) + (2 ^ (i + 1) - 1) := calc
       _ = 2 ^ (i + 1) * 2 ^ k - 1 := by rw [Nat.pow_add]
-      _ = 2 ^ (i + 1) * (2 ^ k - 1 + 1) - 1 := by rw [Nat.sub_add_cancel]; apply Nat.pow_two_pos
+      _ = 2 ^ (i + 1) * (2 ^ k - 1 + 1) - 1 := by rw [Nat.sub_add_cancel]; apply Nat.two_pow_pos
       _ = _ := by
-        have hle : 1 ≤ 2 ^ (i + 1) * 1 := by rw [Nat.mul_one]; apply Nat.pow_two_pos
+        have hle : 1 ≤ 2 ^ (i + 1) * 1 := by rw [Nat.mul_one]; apply Nat.two_pow_pos
         rw [Nat.mul_add]; rw [Nat.add_sub_assoc hle]; simp
-    rw [eqi, Nat.mul_add_mod, Nat.mod_eq_of_lt (Nat.sub_lt (Nat.pow_two_pos _) .refl)]
+    rw [eqi, Nat.mul_add_mod, Nat.mod_eq_of_lt (Nat.sub_lt (Nat.two_pow_pos _) .refl)]
     rw [Nat.pow_add, show (2 ^ 1 = 2) by rfl, Nat.mul_two, show (Nat.succ 0 = 1) by rfl]
-    rw [Nat.add_sub_assoc (Nat.pow_two_pos _)]; apply Nat.le_add_right
+    rw [Nat.add_sub_assoc (Nat.two_pow_pos _)]; apply Nat.le_add_right
 
   theorem Nat.ones_testBit_false_of_ge (n i : Nat) (h : i ≥ n) : (2 ^ n - 1).testBit i = false := by
     have hl : 2 ^ n - 1 < 2 ^ i := by
-      rw [Nat.lt_eq_succ_le, Nat.succ_eq_add_one, Nat.sub_add_cancel (Nat.pow_two_pos _)]
+      rw [Nat.lt_eq_succ_le, Nat.succ_eq_add_one, Nat.sub_add_cancel (Nat.two_pow_pos _)]
       apply Nat.pow_le_pow_of_le_right (Nat.le_step .refl) h
     have hls : 2 ^ i ≤ 2 ^ (i + 1) := Nat.pow_le_pow_of_le_right (Nat.le_step .refl) (Nat.le_add_right _ _)
     rw [Nat.testBit_false_iff]; rw [Nat.mod_eq_of_lt (Nat.le_trans hl hls)]; apply hl
@@ -274,15 +274,15 @@ theorem Nat.le_pow (h : b ≥ 2) : a < b ^ a := by
       rw [Nat.ones_testBit_true_of_lt _ _ hl]
       rw [show (∀ b, (true != b) = !b) by (intro b; simp)]
       generalize hk : a % 2 ^ (i + 1) = k
-      have kl : k < 2 ^ (i + 1) := by rw [← hk]; apply Nat.mod_lt; apply Nat.pow_two_pos
+      have kl : k < 2 ^ (i + 1) := by rw [← hk]; apply Nat.mod_lt; apply Nat.two_pow_pos
       have tr : (2 ^ n - 1 - a) % 2 ^ (i + 1) = 2 ^ (i + 1) - (k + 1) := by
-        rw [Nat.sub_mod _ _ _ (show a ≤ 2 ^ n - 1 by exact (Nat.le_sub_iff_add_le (Nat.pow_two_pos _)).mpr h)]
+        rw [Nat.sub_mod _ _ _ (show a ≤ 2 ^ n - 1 by exact (Nat.le_sub_iff_add_le (Nat.two_pow_pos _)).mpr h)]
         rw [hk]; have ⟨dn, hdn⟩ := Nat.lt_par hl; cases hdn
-        rw [Nat.pow_add _ _ dn, show (2 ^ dn = 2 ^ dn - 1 + 1) by rw[Nat.sub_add_cancel (Nat.pow_two_pos _)]]
+        rw [Nat.pow_add _ _ dn, show (2 ^ dn = 2 ^ dn - 1 + 1) by rw[Nat.sub_add_cancel (Nat.two_pow_pos _)]]
         rw [Nat.mul_add, Nat.mul_one, ← Nat.sub_add_eq]
         rw [Nat.add_sub_assoc (by rw [Nat.add_comm]; exact kl)]
         rw [Nat.mul_add_mod, Nat.mod_eq_of_lt, Nat.add_comm 1 k]
-        apply Nat.sub_lt (Nat.pow_two_pos _)
+        apply Nat.sub_lt (Nat.two_pow_pos _)
         rw [Nat.add_comm]; apply Nat.zero_lt_succ
       cases hai : Nat.testBit a i
       case false =>

lake-manifest.json

@@ -4,10 +4,10 @@
  [{"url": "https://github.com/leanprover/std4.git",
    "type": "git",
    "subDir": null,
-   "rev": "f697bda1b4764a571042fed030690220c66ac4b2",
+   "rev": "bfa9e0827f3011b17d6d849546105ec8c64a265c",
    "name": "std",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "nightly-testing-2024-02-18",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "auto",

lakefile.lean

@@ -7,7 +7,7 @@ package «auto» {
 }
 
 require std from git
-  "https://github.com/leanprover/std4.git"@"main"
+  "https://github.com/leanprover/std4.git"@"nightly-testing-2024-02-18"
 
 @[default_target]
 lean_lib «Auto» {

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.6.0-rc1
+leanprover/lean4:nightly-2024-02-18