chore: update to nightly-2024-10-14 (#700)

SSA/Projects/InstCombine/ForLean.lean

@@ -517,63 +517,6 @@ theorem shiftLeft_and_distrib' {x y : BitVec w} {n m : Nat} :
 theorem zero_sub {x : BitVec w} : 0#w - x = - x := by
     simp [bv_toNat]
 
-theorem getMsbD_sshiftRight {x : BitVec w} {i n : Nat} :
-    getMsbD (x.sshiftRight n) i = (decide (i < w) && if i < n then x.msb else getMsbD x (i - n)) := by
-  simp only [getMsbD]
-  rw [BitVec.getLsbD_sshiftRight]
-  by_cases h : i < w
-  <;> by_cases h₁ : w ≤ w - 1 - i
-  <;> by_cases h₂ : ¬(i < n)
-  <;> by_cases h₃ : n + (w - 1 - i) < w
-  <;> by_cases h₄ : i - n < w
-  all_goals (simp [h, h₁, h₂, h₃, h₄]; try congr; try omega)
-  simp_all
-
-theorem getLsbD_sshiftRight' (x y: BitVec w) {i : Nat} :
-    getLsbD (x.sshiftRight' y) i =
-      (!decide (w ≤ i) && if y.toNat + i < w then x.getLsbD (y.toNat + i) else x.msb) := by
-  simp only [BitVec.sshiftRight', BitVec.getLsbD_sshiftRight]
-
-theorem getMsbD_sshiftRight' {x y: BitVec w} {i : Nat} :
-    getMsbD (x.sshiftRight' y) i = (decide (i < w) && if i < y.toNat then x.msb else getMsbD x (i - y.toNat)) := by
-  simp only [BitVec.sshiftRight', getMsbD, BitVec.getLsbD_sshiftRight]
-  by_cases h : i < w
-  <;> by_cases h₁ : w ≤ w - 1 - i
-  <;> by_cases h₂ : i < y.toNat
-  <;> by_cases h₃ : y.toNat + (w - 1 - i) < w
-  <;> by_cases h₄ : (y.toNat + (w - 1 - i)) = (w - 1 - (i - y.toNat))
-  all_goals (simp [h, h₁, h₂, h₃, h₄]; try omega)
-  simp_all
-  omega
-
-theorem getMsbD_ushiftRight {x : BitVec w} {i n : Nat} :
-    getMsbD (x.ushiftRight n) i = (decide (i < w) && if i < n then false else getMsbD x (i - n)) := by
-  simp only [getMsbD, Bool.if_false_left]
-  by_cases h : i < w
-  <;> by_cases h₁ : i < n
-  <;> by_cases h₂ : i - n < w
-  all_goals (simp [h, h₁, h₂]; try congr; try omega)
-  rw [BitVec.getLsbD_ge]
-  omega
-
-theorem msb_shiftLeft {x : BitVec w} {n : Nat} :
-    (x <<< n).msb = x.getMsbD n := by
-  simp [BitVec.msb]
-
-theorem msb_ushiftRight {x : BitVec w} {n : Nat} :
-    (x.ushiftRight n).msb = if n > 0 then false else x.msb := by
-  induction n
-  case zero =>
-    simp
-  case succ n ih =>
-    simp [ih, ← BitVec.ushiftRight_eq, getMsbD_ushiftRight, BitVec.msb]
-
--- msb_sshiftRight exists already under the name : sshiftRight_msb_eq_msb
-
-theorem msb_sshiftRight' {x y: BitVec w} :
-    (x.sshiftRight' y).msb = x.msb := by
-  simp [BitVec.sshiftRight', BitVec.sshiftRight_msb_eq_msb]
-
 theorem getLsbD_sub {i : Nat} {i_lt : i < w} {x y : BitVec w} :
     (x - y).getLsbD i =
       (x.getLsbD i ^^ ((~~~y + 1).getLsbD i ^^ carry i x (~~~y + 1) false)) := by

SSA/Projects/InstCombine/ForMathlib.lean

@@ -10,45 +10,12 @@ import Mathlib.Data.ZMod.Defs
 namespace BitVec
 open Nat
 
-theorem ofInt_negSucc (w n : Nat ) :
-    BitVec.ofInt w (Int.negSucc n) = ~~~.ofNat w n := by
-  simp [BitVec.ofInt]
-  rw [BitVec.toNat_eq]
-  simp only [Int.toNat, toNat_ofNatLt, toNat_not, toNat_ofNat]
-  split
-  · rename_i a b c
-    simp only [Int.ofNat_eq_coe] at c
-    rw [Int.negSucc_emod] at c
-    symm
-    rw [← Int.natCast_inj]
-    rw [Nat.cast_sub]
-    rw [Nat.cast_sub]
-    have _ : 0 < 2 ^ w := by simp
-    simp_all only [gt_iff_lt, Nat.ofNat_pos, pow_pos, Nat.cast_pow,
-      Nat.cast_ofNat, Nat.cast_one, Int.ofNat_emod]
-    have h : 0 < 2 ^ w := by simp
-    · omega
-    · omega
-    · omega
-  · have nonneg : Int.negSucc n % 2 ^ w ≥ 0 := by
-      simp only [ge_iff_le, ne_eq, pow_eq_zero_iff', OfNat.ofNat_ne_zero, false_and,
-        not_false_eq_true, Int.emod_nonneg (Int.negSucc n) _]
-    simp_all only [Nat.ofNat_pos, gt_iff_lt, pow_pos, ne_eq, pow_eq_zero_iff',
-      OfNat.ofNat_ne_zero, false_and, not_false_eq_true, ge_iff_le, Int.negSucc_not_nonneg]
-
 @[simp] lemma ofFin_neg : ofFin (-x) = -(ofFin x) := by
   ext; rw [neg_eq_zero_sub]; simp; rfl
 
-@[simp] lemma ofFin_ofNat (n : ℕ) :
-    ofFin (no_index (OfNat.ofNat n : Fin (2^w))) = OfNat.ofNat n := by
-  simp only [OfNat.ofNat, Fin.ofNat', BitVec.ofNat, Nat.and_pow_two_sub_one_eq_mod]
-
 theorem toFin_injective {n : Nat} : Function.Injective (toFin : BitVec n → _)
   | ⟨_, _⟩, ⟨_, _⟩, rfl => rfl
 
-theorem toFin_inj {x y : BitVec w} : x.toFin = y.toFin ↔ x = y :=
-  toFin_injective.eq_iff
-
 @[simp] lemma ofFin_natCast (n : ℕ) : ofFin (n : Fin (2^w)) = n := by
   simp only [Nat.cast, NatCast.natCast, OfNat.ofNat, BitVec.ofNat, Nat.and_pow_two_sub_one_eq_mod]
   rfl
@@ -65,18 +32,14 @@ theorem ofFin_intCast (z : ℤ) : ofFin (z : Fin (2^w)) = Int.cast z := by
     unfold Int.castDef
     cases' z with z z
     · rfl
-    · rw [ofInt_negSucc]
+    · rw [ofInt_negSucc_eq_not_ofNat]
       simp only [Nat.cast_add, Nat.cast_one, neg_add_rev]
       rw [← add_ofFin, ofFin_neg, ofFin_ofNat, ofNat_eq_ofNat, ofFin_neg, ofFin_natCast,
         natCast_eq_ofNat, negOne_eq_allOnes, ← sub_toAdd, allOnes_sub_eq_not]
 
 theorem toFin_intCast (z : ℤ) : toFin (z : BitVec w) = z := by
   apply toFin_inj.mpr <| (ofFin_intCast z).symm
 
-lemma toFin_zero : toFin (0 : BitVec w) = 0 := rfl
-lemma toFin_one  : toFin (1 : BitVec w) = 1 := by
-  rw [toFin_inj]; simp only [ofNat_eq_ofNat, ofFin_ofNat]
-
 instance : SMul ℕ (BitVec w) := ⟨fun x y => ofFin <| x • y.toFin⟩
 instance : SMul ℤ (BitVec w) := ⟨fun x y => ofFin <| x • y.toFin⟩
 instance : Pow (BitVec w) ℕ  := ⟨fun x n => ofFin <| x.toFin ^ n⟩

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "daf1ed91789811cf6bbb7bf2f4dad6b3bad8fbf4",
+   "rev": "5f963d5d06cc3c2d3abd0806891133137a59d7eb",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -75,10 +75,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "6125cddcb7541bb61d58f6f316cdd43b9c962e17",
+   "rev": "663637410a7edbee9fc0737ff0fdd01edd35a4b4",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "nightly-testing-2024-10-13",
+   "inputRev": "nightly-testing-2024-10-14",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/acmepjz/md4lean",

lakefile.toml

@@ -4,7 +4,7 @@ defaultTargets = ["SSA"]
 [[require]]
 name = "mathlib"
 git = "https://github.com/leanprover-community/mathlib4"
-rev = "nightly-testing-2024-10-13"
+rev = "nightly-testing-2024-10-14"
 
 [[require]]
 name = "Cli"

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2024-10-13
+leanprover/lean4:nightly-2024-10-14