chore: alignment of Array and List lemmas

CODEOWNERS

@@ -4,7 +4,7 @@
 # Listed persons will automatically be asked by GitHub to review a PR touching these paths.
 # If multiple names are listed, a review by any of them is considered sufficient by default.
 
-/.github/ @kim-em
+/.github/ @Kha @kim-em
 /RELEASES.md @kim-em
 /src/kernel/ @leodemoura
 /src/lake/ @tydeu
@@ -14,7 +14,9 @@
 /src/Lean/Elab/Tactic/ @kim-em
 /src/Lean/Language/ @Kha
 /src/Lean/Meta/Tactic/ @leodemoura
-/src/Lean/PrettyPrinter/ @kmill
+/src/Lean/Parser/ @Kha
+/src/Lean/PrettyPrinter/ @Kha
+/src/Lean/PrettyPrinter/Delaborator/ @kmill
 /src/Lean/Server/ @mhuisi
 /src/Lean/Widget/ @Vtec234
 /src/Init/Data/ @kim-em

src/Init/Data.lean

@@ -21,7 +21,6 @@ import Init.Data.Fin
 import Init.Data.UInt
 import Init.Data.SInt
 import Init.Data.Float
-import Init.Data.Float32
 import Init.Data.Option
 import Init.Data.Ord
 import Init.Data.Random

src/Init/Data/Array/Basic.lean

@@ -663,7 +663,7 @@ def all (as : Array α) (p : α → Bool) (start := 0) (stop := as.size) : Bool
   Id.run <| as.allM p start stop
 
 def contains [BEq α] (as : Array α) (a : α) : Bool :=
-  as.any (a == ·)
+  as.any (· == a)
 
 def elem [BEq α] (a : α) (as : Array α) : Bool :=
   as.contains a

src/Init/Data/Array/Lemmas.lean

@@ -19,6 +19,8 @@ import Init.Data.List.ToArray
 ## Theorems about `Array`.
 -/
 
+
+
 namespace Array
 
 /-! ## Preliminaries -/
@@ -182,14 +184,6 @@ theorem getElem_eq_getElem?_get (a : Array α) (i : Nat) (h : i < a.size) :
     a[i] = a[i]?.get (by simp [getElem?_eq_getElem, h]) := by
   simp [getElem_eq_iff]
 
-theorem getD_getElem? (a : Array α) (i : Nat) (d : α) :
-    a[i]?.getD d = if p : i < a.size then a[i]'p else d := by
-  if h : i < a.size then
-    simp [h, getElem?_def]
-  else
-    have p : i ≥ a.size := Nat.le_of_not_gt h
-    simp [getElem?_eq_none p, h]
-
 @[simp] theorem getElem?_empty {n : Nat} : (#[] : Array α)[n]? = none := rfl
 
 theorem getElem_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
@@ -363,517 +357,6 @@ theorem forall_getElem {l : Array α} {p : α → Prop} :
     (∀ (n : Nat) h, p (l[n]'h)) ↔ ∀ a, a ∈ l → p a := by
   cases l; simp [List.forall_getElem]
 
-/-! ### isEmpty-/
-
-@[simp] theorem isEmpty_toList {l : Array α} : l.toList.isEmpty = l.isEmpty := by
-  rcases l with ⟨_ | _⟩ <;> simp
-
-theorem isEmpty_iff {l : Array α} : l.isEmpty ↔ l = #[] := by
-  cases l <;> simp
-
-theorem isEmpty_eq_false_iff_exists_mem {xs : Array α} :
-    xs.isEmpty = false ↔ ∃ x, x ∈ xs := by
-  cases xs
-  simpa using List.isEmpty_eq_false_iff_exists_mem
-
-theorem isEmpty_iff_size_eq_zero {l : Array α} : l.isEmpty ↔ l.size = 0 := by
-  rw [isEmpty_iff, size_eq_zero]
-
-@[simp] theorem isEmpty_eq_true {l : Array α} : l.isEmpty ↔ l = #[] := by
-  cases l <;> simp
-
-@[simp] theorem isEmpty_eq_false {l : Array α} : l.isEmpty = false ↔ l ≠ #[] := by
-  cases l <;> simp
-
-/-! ### Decidability of bounded quantifiers -/
-
-instance {xs : Array α} {p : α → Prop} [DecidablePred p] :
-    Decidable (∀ x, x ∈ xs → p x) :=
-  decidable_of_iff (∀ (i : Nat) h, p (xs[i]'h)) (by
-    simp only [mem_iff_getElem, forall_exists_index]
-    exact
-      ⟨by rintro w _ i h rfl; exact w i h, fun w i h => w _ i h rfl⟩)
-
-instance {xs : Array α} {p : α → Prop} [DecidablePred p] :
-    Decidable (∃ x, x ∈ xs ∧ p x) :=
-  decidable_of_iff (∃ (i : Nat), ∃ (h : i < xs.size), p (xs[i]'h)) (by
-    simp [mem_iff_getElem]
-    exact
-      ⟨by rintro ⟨i, h, w⟩; exact ⟨_, ⟨i, h, rfl⟩, w⟩, fun ⟨_, ⟨i, h, rfl⟩, w⟩ => ⟨i, h, w⟩⟩)
-
-/-! ### any / all -/
-
-theorem anyM_eq_anyM_loop [Monad m] (p : α → m Bool) (as : Array α) (start stop) :
-    anyM p as start stop = anyM.loop p as (min stop as.size) (Nat.min_le_right ..) start := by
-  simp only [anyM, Nat.min_def]; split <;> rfl
-
-theorem anyM_stop_le_start [Monad m] (p : α → m Bool) (as : Array α) (start stop)
-    (h : min stop as.size ≤ start) : anyM p as start stop = pure false := by
-  rw [anyM_eq_anyM_loop, anyM.loop, dif_neg (Nat.not_lt.2 h)]
-
-theorem anyM_loop_cons [Monad m] (p : α → m Bool) (a : α) (as : List α) (stop start : Nat)
-    (h : stop + 1 ≤ (a :: as).length) :
-    anyM.loop p ⟨a :: as⟩ (stop + 1) h (start + 1) =
-      anyM.loop p ⟨as⟩ stop (by simpa using h) start := by
-  rw [anyM.loop]
-  conv => rhs; rw [anyM.loop]
-  split <;> rename_i h'
-  · simp only [Nat.add_lt_add_iff_right] at h'
-    rw [dif_pos h', anyM_loop_cons]
-    simp
-  · rw [dif_neg]
-    omega
-
-@[simp] theorem anyM_toList [Monad m] (p : α → m Bool) (as : Array α) :
-    as.toList.anyM p = as.anyM p :=
-  match as with
-  | ⟨[]⟩  => rfl
-  | ⟨a :: as⟩ => by
-    simp only [List.anyM, anyM, size_toArray, List.length_cons, Nat.le_refl, ↓reduceDIte]
-    rw [anyM.loop, dif_pos (by omega)]
-    congr 1
-    funext b
-    split
-    · simp
-    · simp only [Bool.false_eq_true, ↓reduceIte]
-      rw [anyM_loop_cons]
-      simpa [anyM] using anyM_toList p ⟨as⟩
-
--- Auxiliary for `any_iff_exists`.
-theorem anyM_loop_iff_exists {p : α → Bool} {as : Array α} {start stop} (h : stop ≤ as.size) :
-    anyM.loop (m := Id) p as stop h start = true ↔
-      ∃ (i : Nat) (_ : i < as.size), start ≤ i ∧ i < stop ∧ p as[i] = true := by
-  unfold anyM.loop
-  split <;> rename_i h₁
-  · dsimp
-    split <;> rename_i h₂
-    · simp only [true_iff]
-      refine ⟨start, by omega, by omega, by omega, h₂⟩
-    · rw [anyM_loop_iff_exists]
-      constructor
-      · rintro ⟨i, hi, ge, lt, h⟩
-        have : start ≠ i := by rintro rfl; omega
-        exact ⟨i, by omega, by omega, lt, h⟩
-      · rintro ⟨i, hi, ge, lt, h⟩
-        have : start ≠ i := by rintro rfl; erw [h] at h₂; simp_all
-        exact ⟨i, by omega, by omega, lt, h⟩
-  · simp
-    omega
-termination_by stop - start
-
--- This could also be proved from `SatisfiesM_anyM_iff_exists` in `Batteries.Data.Array.Init.Monadic`
-theorem any_iff_exists {p : α → Bool} {as : Array α} {start stop} :
-    as.any p start stop ↔ ∃ (i : Nat) (_ : i < as.size), start ≤ i ∧ i < stop ∧ p as[i] := by
-  dsimp [any, anyM, Id.run]
-  split
-  · rw [anyM_loop_iff_exists]
-  · rw [anyM_loop_iff_exists]
-    constructor
-    · rintro ⟨i, hi, ge, _, h⟩
-      exact ⟨i, by omega, by omega, by omega, h⟩
-    · rintro ⟨i, hi, ge, _, h⟩
-      exact ⟨i, by omega, by omega, by omega, h⟩
-
-@[simp] theorem any_eq_true {p : α → Bool} {as : Array α} :
-    as.any p = true ↔ ∃ (i : Nat) (_ : i < as.size), p as[i] := by
-  simp [any_iff_exists]
-
-@[simp] theorem any_eq_false {p : α → Bool} {as : Array α} :
-    as.any p = false ↔ ∀ (i : Nat) (_ : i < as.size), ¬p as[i] := by
-  rw [Bool.eq_false_iff, Ne, any_eq_true]
-  simp
-
-theorem any_toList {p : α → Bool} (as : Array α) : as.toList.any p = as.any p := by
-  rw [Bool.eq_iff_iff, any_eq_true, List.any_eq_true]
-  simp only [List.mem_iff_getElem, getElem_toList]
-  exact ⟨fun ⟨_, ⟨i, w, rfl⟩, h⟩ => ⟨i, w, h⟩, fun ⟨i, w, h⟩ => ⟨_, ⟨i, w, rfl⟩, h⟩⟩
-
-theorem allM_eq_not_anyM_not [Monad m] [LawfulMonad m] (p : α → m Bool) (as : Array α) :
-    allM p as = (! ·) <$> anyM ((! ·) <$> p ·) as := by
-  dsimp [allM, anyM]
-  simp
-
-@[simp] theorem allM_toList [Monad m] [LawfulMonad m] (p : α → m Bool) (as : Array α) :
-    as.toList.allM p = as.allM p := by
-  rw [allM_eq_not_anyM_not]
-  rw [← anyM_toList]
-  rw [List.allM_eq_not_anyM_not]
-
-theorem all_eq_not_any_not (p : α → Bool) (as : Array α) (start stop) :
-    as.all p start stop = !(as.any (!p ·) start stop) := by
-  dsimp [all, allM]
-  rfl
-
-theorem all_iff_forall {p : α → Bool} {as : Array α} {start stop} :
-    as.all p start stop ↔ ∀ (i : Nat) (_ : i < as.size), start ≤ i ∧ i < stop → p as[i] := by
-  rw [all_eq_not_any_not]
-  suffices ¬(as.any (!p ·) start stop = true) ↔
-      ∀ (i : Nat) (_ : i < as.size), start ≤ i ∧ i < stop → p as[i] by
-    simp_all
-  simp only [any_iff_exists, Bool.not_eq_eq_eq_not, Bool.not_true, not_exists, not_and,
-    Bool.not_eq_false, and_imp]
-
-@[simp] theorem all_eq_true {p : α → Bool} {as : Array α} :
-    as.all p = true ↔ ∀ (i : Nat) (_ : i < as.size), p as[i] := by
-  simp [all_iff_forall]
-
-@[simp] theorem all_eq_false {p : α → Bool} {as : Array α} :
-    as.all p = false ↔ ∃ (i : Nat) (_ : i < as.size), ¬p as[i] := by
-  rw [Bool.eq_false_iff, Ne, all_eq_true]
-  simp
-
-theorem all_toList {p : α → Bool} (as : Array α) : as.toList.all p = as.all p := by
-  rw [Bool.eq_iff_iff, all_eq_true, List.all_eq_true]
-  simp only [List.mem_iff_getElem, getElem_toList]
-  constructor
-  · intro w i h
-    exact w as[i] ⟨i, h, getElem_toList h⟩
-  · rintro w x ⟨i, h, rfl⟩
-    exact w i h
-
-theorem all_eq_true_iff_forall_mem {l : Array α} : l.all p ↔ ∀ x, x ∈ l → p x := by
-  simp only [← all_toList, List.all_eq_true, mem_def]
-
-theorem _root_.List.anyM_toArray [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α) :
-    l.toArray.anyM p = l.anyM p := by
-  rw [← anyM_toList]
-
-theorem _root_.List.any_toArray (p : α → Bool) (l : List α) : l.toArray.any p = l.any p := by
-  rw [any_toList]
-
-theorem _root_.List.allM_toArray [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α) :
-    l.toArray.allM p = l.allM p := by
-  rw [← allM_toList]
-
-theorem _root_.List.all_toArray (p : α → Bool) (l : List α) : l.toArray.all p = l.all p := by
-  rw [all_toList]
-
-/-- Variant of `anyM_toArray` with a side condition on `stop`. -/
-@[simp] theorem _root_.List.anyM_toArray' [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α)
-    (h : stop = l.toArray.size) :
-    l.toArray.anyM p 0 stop = l.anyM p := by
-  subst h
-  rw [← anyM_toList]
-
-/-- Variant of `any_toArray` with a side condition on `stop`. -/
-@[simp] theorem _root_.List.any_toArray' (p : α → Bool) (l : List α) (h : stop = l.toArray.size) :
-    l.toArray.any p 0 stop = l.any p := by
-  subst h
-  rw [any_toList]
-
-/-- Variant of `allM_toArray` with a side condition on `stop`. -/
-@[simp] theorem _root_.List.allM_toArray' [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α)
-    (h : stop = l.toArray.size) :
-    l.toArray.allM p 0 stop = l.allM p := by
-  subst h
-  rw [← allM_toList]
-
-/-- Variant of `all_toArray` with a side condition on `stop`. -/
-@[simp] theorem _root_.List.all_toArray' (p : α → Bool) (l : List α) (h : stop = l.toArray.size) :
-    l.toArray.all p 0 stop = l.all p := by
-  subst h
-  rw [all_toList]
-
-/-- Variant of `any_eq_true` in terms of membership rather than an array index. -/
-theorem any_eq_true' {p : α → Bool} {as : Array α} :
-    as.any p = true ↔ (∃ x, x ∈ as ∧ p x) := by
-  cases as
-  simp
-
-/-- Variant of `any_eq_false` in terms of membership rather than an array index. -/
-theorem any_eq_false' {p : α → Bool} {as : Array α} :
-    as.any p = false ↔ ∀ x, x ∈ as → ¬p x := by
-  rw [Bool.eq_false_iff, Ne, any_eq_true']
-  simp
-
-/-- Variant of `all_eq_true` in terms of membership rather than an array index. -/
-theorem all_eq_true' {p : α → Bool} {as : Array α} :
-    as.all p = true ↔ (∀ x, x ∈ as → p x) := by
-  cases as
-  simp
-
-/-- Variant of `all_eq_false` in terms of membership rather than an array index. -/
-theorem all_eq_false' {p : α → Bool} {as : Array α} :
-    as.all p = false ↔ ∃ x, x ∈ as ∧ ¬p x := by
-  rw [Bool.eq_false_iff, Ne, all_eq_true']
-  simp
-
-theorem any_eq {xs : Array α} {p : α → Bool} : xs.any p = decide (∃ i : Nat, ∃ h, p (xs[i]'h)) := by
-  by_cases h : xs.any p
-  · simp_all [any_eq_true]
-  · simp_all [any_eq_false]
-
-/-- Variant of `any_eq` in terms of membership rather than an array index. -/
-theorem any_eq' {xs : Array α} {p : α → Bool} : xs.any p = decide (∃ x, x ∈ xs ∧ p x) := by
-  by_cases h : xs.any p
-  · simp_all [any_eq_true', -any_eq_true]
-  · simp only [Bool.not_eq_true] at h
-    simp only [h]
-    simp only [any_eq_false'] at h
-    simpa using h
-
-theorem all_eq {xs : Array α} {p : α → Bool} : xs.all p = decide (∀ i, (_ : i < xs.size) → p xs[i]) := by
-  by_cases h : xs.all p
-  · simp_all [all_eq_true]
-  · simp only [Bool.not_eq_true] at h
-    simp only [h]
-    simp only [all_eq_false] at h
-    simpa using h
-
-/-- Variant of `all_eq` in terms of membership rather than an array index. -/
-theorem all_eq' {xs : Array α} {p : α → Bool} : xs.all p = decide (∀ x, x ∈ xs → p x) := by
-  by_cases h : xs.all p
-  · simp_all [all_eq_true', -all_eq_true]
-  · simp only [Bool.not_eq_true] at h
-    simp only [h]
-    simp only [all_eq_false'] at h
-    simpa using h
-
-theorem decide_exists_mem {xs : Array α} {p : α → Prop} [DecidablePred p] :
-    decide (∃ x, x ∈ xs ∧ p x) = xs.any p := by
-  simp [any_eq']
-
-theorem decide_forall_mem {xs : Array α} {p : α → Prop} [DecidablePred p] :
-    decide (∀ x, x ∈ xs → p x) = xs.all p := by
-  simp [all_eq']
-
-@[simp] theorem _root_.List.contains_toArray [BEq α] {l : List α} {a : α} :
-    l.toArray.contains a = l.contains a := by
-  simp [Array.contains, List.any_beq]
-
-@[simp] theorem _root_.List.elem_toArray [BEq α] {l : List α} {a : α} :
-    Array.elem a l.toArray = List.elem a l := by
-  simp [Array.elem]
-
-theorem any_beq [BEq α] {xs : Array α} {a : α} : (xs.any fun x => a == x) = xs.contains a := by
-  cases xs
-  simp [List.any_beq]
-
-/-- Variant of `any_beq` with `==` reversed. -/
-theorem any_beq' [BEq α] [PartialEquivBEq α] {xs : Array α} :
-    (xs.any fun x => x == a) = xs.contains a := by
-  simp only [BEq.comm, any_beq]
-
-theorem all_bne [BEq α] {xs : Array α} : (xs.all fun x => a != x) = !xs.contains a := by
-  cases xs
-  simp [List.all_bne]
-
-/-- Variant of `all_bne` with `!=` reversed. -/
-theorem all_bne' [BEq α] [PartialEquivBEq α] {xs : Array α} :
-    (xs.all fun x => x != a) = !xs.contains a := by
-  simp only [bne_comm, all_bne]
-
-theorem mem_of_elem_eq_true [BEq α] [LawfulBEq α] {a : α} {as : Array α} : elem a as = true → a ∈ as := by
-  cases as
-  simp
-
-theorem elem_eq_true_of_mem [BEq α] [LawfulBEq α] {a : α} {as : Array α} (h : a ∈ as) : elem a as = true := by
-  cases as
-  simpa using h
-
-instance [BEq α] [LawfulBEq α] (a : α) (as : Array α) : Decidable (a ∈ as) :=
-  decidable_of_decidable_of_iff (Iff.intro mem_of_elem_eq_true elem_eq_true_of_mem)
-
-@[simp] theorem elem_eq_contains [BEq α] {a : α} {l : Array α} :
-    elem a l = l.contains a := by
-  simp [elem]
-
-theorem elem_iff [BEq α] [LawfulBEq α] {a : α} {as : Array α} :
-    elem a as = true ↔ a ∈ as := ⟨mem_of_elem_eq_true, elem_eq_true_of_mem⟩
-
-theorem contains_iff [BEq α] [LawfulBEq α] {a : α} {as : Array α} :
-    as.contains a = true ↔ a ∈ as := ⟨mem_of_elem_eq_true, elem_eq_true_of_mem⟩
-
-theorem elem_eq_mem [BEq α] [LawfulBEq α] (a : α) (as : Array α) :
-    elem a as = decide (a ∈ as) := by rw [Bool.eq_iff_iff, elem_iff, decide_eq_true_iff]
-
-@[simp] theorem contains_eq_mem [BEq α] [LawfulBEq α] (a : α) (as : Array α) :
-    as.contains a = decide (a ∈ as) := by rw [← elem_eq_contains, elem_eq_mem]
-
-/-- Variant of `any_push` with a side condition on `stop`. -/
-@[simp] theorem any_push' [BEq α] {as : Array α} {a : α} {p : α → Bool} (h : stop = as.size + 1) :
-    (as.push a).any p 0 stop = (as.any p || p a) := by
-  cases as
-  rw [List.push_toArray]
-  simp [h]
-
-theorem any_push [BEq α] {as : Array α} {a : α} {p : α → Bool} :
-    (as.push a).any p = (as.any p || p a) :=
-  any_push' (by simp)
-
-/-- Variant of `all_push` with a side condition on `stop`. -/
-@[simp] theorem all_push' [BEq α] {as : Array α} {a : α} {p : α → Bool} (h : stop = as.size + 1) :
-    (as.push a).all p 0 stop = (as.all p && p a) := by
-  cases as
-  rw [List.push_toArray]
-  simp [h]
-
-theorem all_push [BEq α] {as : Array α} {a : α} {p : α → Bool} :
-    (as.push a).all p = (as.all p && p a) :=
-  all_push' (by simp)
-
-@[simp] theorem contains_push [BEq α] {l : Array α} {a : α} {b : α} :
-    (l.push a).contains b = (l.contains b || b == a) := by
-  simp [contains]
-
-/-! ### set -/
-
-
-/-! # set -/
-
-@[simp] theorem getElem_set_self (a : Array α) (i : Nat) (h : i < a.size) (v : α) {j : Nat}
-      (eq : i = j) (p : j < (a.set i v).size) :
-    (a.set i v)[j]'p = v := by
-  cases a
-  simp
-  simp [set, ← getElem_toList, ←eq]
-
-@[deprecated getElem_set_self (since := "2024-12-11")]
-abbrev getElem_set_eq := @getElem_set_self
-
-@[simp] theorem getElem?_set_self (a : Array α) (i : Nat) (h : i < a.size) (v : α) :
-    (a.set i v)[i]? = v := by simp [getElem?_eq_getElem, h]
-
-@[deprecated getElem?_set_self (since := "2024-12-11")]
-abbrev getElem?_set_eq := @getElem?_set_self
-
-@[simp] theorem getElem_set_ne (a : Array α) (i : Nat) (h' : i < a.size) (v : α) {j : Nat}
-    (pj : j < (a.set i v).size) (h : i ≠ j) :
-    (a.set i v)[j]'pj = a[j]'(size_set a i v _ ▸ pj) := by
-  simp only [set, ← getElem_toList, List.getElem_set_ne h]
-
-@[simp] theorem getElem?_set_ne (a : Array α) (i : Nat) (h : i < a.size) {j : Nat} (v : α)
-    (ne : i ≠ j) : (a.set i v)[j]? = a[j]? := by
-  by_cases h : j < a.size <;> simp [getElem?_eq_getElem, getElem?_eq_none, Nat.ge_of_not_lt, ne, h]
-
-theorem getElem_set (a : Array α) (i : Nat) (h' : i < a.size) (v : α) (j : Nat)
-    (h : j < (a.set i v).size) :
-    (a.set i v)[j]'h = if i = j then v else a[j]'(size_set a i v _ ▸ h) := by
-  by_cases p : i = j <;> simp [p]
-
-theorem getElem?_set (a : Array α) (i : Nat) (h : i < a.size) (v : α) (j : Nat) :
-    (a.set i v)[j]? = if i = j then some v else a[j]? := by
-  split <;> simp_all
-
-@[simp] theorem set_getElem_self {as : Array α} {i : Nat} (h : i < as.size) :
-    as.set i as[i] = as := by
-  cases as
-  simp
-
-@[simp] theorem set_eq_empty_iff {as : Array α} (n : Nat) (a : α) (h) :
-     as.set n a = #[] ↔ as = #[] := by
-  cases as <;> cases n <;> simp [set]
-
-theorem set_comm (a b : α)
-    {n m : Nat} (as : Array α) {hn : n < as.size} {hm : m < (as.set n a).size} (h : n ≠ m) :
-    (as.set n a).set m b = (as.set m b (by simpa using hm)).set n a (by simpa using hn) := by
-  cases as
-  simp [List.set_comm _ _ _ h]
-
-@[simp]
-theorem set_set (a b : α) (as : Array α) (n : Nat) (h : n < as.size) :
-    (as.set n a).set n b (by simpa using h) = as.set n b := by
-  cases as
-  simp
-
-theorem mem_set (as : Array α) (n : Nat) (h : n < as.size) (a : α) :
-    a ∈ as.set n a := by
-  simp [mem_iff_getElem]
-  exact ⟨n, (by simpa using h), by simp⟩
-
-theorem mem_or_eq_of_mem_set
-    {as : Array α} {n : Nat} {a b : α} {w : n < as.size} (h : a ∈ as.set n b) : a ∈ as ∨ a = b := by
-  cases as
-  simpa using List.mem_or_eq_of_mem_set (by simpa using h)
-
-/-! # setIfInBounds -/
-
-@[simp] theorem set!_is_setIfInBounds : @set! = @setIfInBounds := rfl
-
-@[simp] theorem size_setIfInBounds (as : Array α) (index : Nat) (val : α) :
-    (as.setIfInBounds index val).size = as.size := by
-  if h : index < as.size  then
-    simp [setIfInBounds, h]
-  else
-    simp [setIfInBounds, h]
-
-theorem getElem_setIfInBounds (as : Array α) (i : Nat) (v : α) (j : Nat)
-    (hj : j < (as.setIfInBounds i v).size) :
-    (as.setIfInBounds i v)[j]'hj = if i = j then v else as[j]'(by simpa using hj) := by
-  simp only [setIfInBounds]
-  split
-  · simp [getElem_set]
-  · simp only [size_setIfInBounds] at hj
-    rw [if_neg]
-    omega
-
-@[simp] theorem getElem_setIfInBounds_self (as : Array α) {i : Nat} (v : α) (h : _) :
-    (as.setIfInBounds i v)[i]'h = v := by
-  simp at h
-  simp only [setIfInBounds, h, ↓reduceDIte, getElem_set_self]
-
-@[deprecated getElem_setIfInBounds_self (since := "2024-12-11")]
-abbrev getElem_setIfInBounds_eq := @getElem_setIfInBounds_self
-
-@[simp] theorem getElem_setIfInBounds_ne (as : Array α) {i : Nat} (v : α) {j : Nat}
-    (hj : j < (as.setIfInBounds i v).size) (h : i ≠ j) :
-    (as.setIfInBounds i v)[j]'hj = as[j]'(by simpa using hj) := by
-  simp [getElem_setIfInBounds, h]
-
-@[simp]
-theorem getElem?_setIfInBounds_self (as : Array α) {i : Nat} (p : i < as.size) (v : α) :
-    (as.setIfInBounds i v)[i]? = some v := by
-  simp [getElem?_eq_getElem, p]
-
-@[deprecated getElem?_setIfInBounds_self (since := "2024-12-11")]
-abbrev getElem?_setIfInBounds_eq := @getElem?_setIfInBounds_self
-
-theorem getElem?_setIfInBounds {as : Array α} {i j : Nat} {a : α}  :
-    (as.setIfInBounds i a)[j]? = if i = j then if i < as.size then some a else none else as[j]? := by
-  cases as
-  simp [List.getElem?_set]
-
-@[simp] theorem getElem?_setIfInBounds_ne {as : Array α} {i j : Nat} (h : i ≠ j) {a : α}  :
-    (as.setIfInBounds i a)[j]? = as[j]? := by
-  simp [getElem?_setIfInBounds, h]
-
-theorem setIfInBounds_eq_of_size_le {l : Array α} {n : Nat} (h : l.size ≤ n) {a : α} :
-    l.setIfInBounds n a = l := by
-  cases l
-  simp [List.set_eq_of_length_le (by simpa using h)]
-
-@[simp] theorem setIfInBounds_eq_empty_iff {as : Array α} (n : Nat) (a : α) :
-     as.setIfInBounds n a = #[] ↔ as = #[] := by
-  cases as <;> cases n <;> simp
-
-theorem setIfInBounds_comm (a b : α)
-    {n m : Nat} (as : Array α) (h : n ≠ m) :
-    (as.setIfInBounds n a).setIfInBounds m b = (as.setIfInBounds m b).setIfInBounds n a := by
-  cases as
-  simp [List.set_comm _ _ _ h]
-
-@[simp]
-theorem setIfInBounds_setIfInBounds (a b : α) (as : Array α) (n : Nat) :
-    (as.setIfInBounds n a).setIfInBounds n b = as.setIfInBounds n b := by
-  cases as
-  simp
-
-theorem mem_setIfInBounds (as : Array α) (n : Nat) (h : n < as.size) (a : α) :
-    a ∈ as.setIfInBounds n a := by
-  simp [mem_iff_getElem]
-  exact ⟨n, (by simpa using h), by simp⟩
-
-theorem mem_or_eq_of_mem_setIfInBounds
-    {as : Array α} {n : Nat} {a b : α} (h : a ∈ as.setIfInBounds n b) : a ∈ as ∨ a = b := by
-  cases as
-  simpa using List.mem_or_eq_of_mem_set (by simpa using h)
-
-/-- Simplifies a normal form from `get!` -/
-@[simp] theorem getD_get?_setIfInBounds (a : Array α) (i : Nat) (v d : α) :
-    (setIfInBounds a i v)[i]?.getD d = if i < a.size then v else d := by
-  by_cases h : i < a.size <;>
-    simp [setIfInBounds, Nat.not_lt_of_le, h,  getD_getElem?]
-
 theorem singleton_inj : #[a] = #[b] ↔ a = b := by
   simp
 
@@ -892,6 +375,8 @@ theorem singleton_eq_toArray_singleton (a : α) : #[a] = [a].toArray := rfl
 
 @[simp] theorem size_mk (as : List α) : (Array.mk as).size = as.length := by simp [size]
 
+@[simp] theorem isEmpty_toList {l : Array α} : l.toList.isEmpty = l.isEmpty := by
+  rcases l with ⟨_ | _⟩ <;> simp
 
 theorem foldrM_push [Monad m] (f : α → β → m β) (init : β) (arr : Array α) (a : α) :
     (arr.push a).foldrM f init = f a init >>= arr.foldrM f := by
@@ -975,6 +460,13 @@ theorem foldl_toList_eq_map (l : List α) (acc : Array β) (G : α → β) :
     (l.foldl (fun acc a => acc.push (G a)) acc).toList = acc.toList ++ l.map G := by
   induction l generalizing acc <;> simp [*]
 
+theorem anyM_eq_anyM_loop [Monad m] (p : α → m Bool) (as : Array α) (start stop) :
+    anyM p as start stop = anyM.loop p as (min stop as.size) (Nat.min_le_right ..) start := by
+  simp only [anyM, Nat.min_def]; split <;> rfl
+
+theorem anyM_stop_le_start [Monad m] (p : α → m Bool) (as : Array α) (start stop)
+    (h : min stop as.size ≤ start) : anyM p as start stop = pure false := by
+  rw [anyM_eq_anyM_loop, anyM.loop, dif_neg (Nat.not_lt.2 h)]
 
 /-! # uset -/
 
@@ -984,31 +476,102 @@ theorem size_uset (a : Array α) (v i h) : (uset a i v h).size = a.size := by si
 
 /-! # get -/
 
-@[deprecated getElem?_eq_getElem (since := "2024-12-11")]
 theorem getElem?_lt
     (a : Array α) {i : Nat} (h : i < a.size) : a[i]? = some a[i] := dif_pos h
 
-@[deprecated getElem?_eq_none (since := "2024-12-11")]
 theorem getElem?_ge
     (a : Array α) {i : Nat} (h : i ≥ a.size) : a[i]? = none := dif_neg (Nat.not_lt_of_le h)
 
 @[simp] theorem get?_eq_getElem? (a : Array α) (i : Nat) : a.get? i = a[i]? := rfl
 
-@[deprecated getElem?_eq_none (since := "2024-12-11")]
 theorem getElem?_len_le (a : Array α) {i : Nat} (h : a.size ≤ i) : a[i]? = none := by
-  simp [getElem?_eq_none, h]
+  simp [getElem?_ge, h]
 
-@[deprecated getD_getElem? (since := "2024-12-11")] abbrev getD_get? := @getD_getElem?
+theorem getD_get? (a : Array α) (i : Nat) (d : α) :
+  Option.getD a[i]? d = if p : i < a.size then a[i]'p else d := by
+  if h : i < a.size then
+    simp [setIfInBounds, h, getElem?_def]
+  else
+    have p : i ≥ a.size := Nat.le_of_not_gt h
+    simp [setIfInBounds, getElem?_len_le _ p, h]
 
 @[simp] theorem getD_eq_get? (a : Array α) (n d) : a.getD n d = (a[n]?).getD d := by
-  simp only [getD, get_eq_getElem, get?_eq_getElem?]; split <;> simp [getD_getElem?, *]
+  simp only [getD, get_eq_getElem, get?_eq_getElem?]; split <;> simp [getD_get?, *]
 
 theorem get!_eq_getD [Inhabited α] (a : Array α) : a.get! n = a.getD n default := rfl
 
 @[simp] theorem get!_eq_getElem? [Inhabited α] (a : Array α) (i : Nat) :
     a.get! i = (a.get? i).getD default := by
   by_cases p : i < a.size <;>
-  simp only [get!_eq_getD, getD_eq_get?, getD_getElem?, p, get?_eq_getElem?]
+  simp only [get!_eq_getD, getD_eq_get?, getD_get?, p, get?_eq_getElem?]
+
+/-! # set -/
+
+@[simp] theorem getElem_set_eq (a : Array α) (i : Nat) (h : i < a.size) (v : α) {j : Nat}
+      (eq : i = j) (p : j < (a.set i v).size) :
+    (a.set i v)[j]'p = v := by
+  cases a
+  simp
+  simp [set, ← getElem_toList, ←eq]
+
+@[simp] theorem getElem_set_ne (a : Array α) (i : Nat) (h' : i < a.size) (v : α) {j : Nat}
+    (pj : j < (a.set i v).size) (h : i ≠ j) :
+    (a.set i v)[j]'pj = a[j]'(size_set a i v _ ▸ pj) := by
+  simp only [set, ← getElem_toList, List.getElem_set_ne h]
+
+theorem getElem_set (a : Array α) (i : Nat) (h' : i < a.size) (v : α) (j : Nat)
+    (h : j < (a.set i v).size) :
+    (a.set i v)[j]'h = if i = j then v else a[j]'(size_set a i v _ ▸ h) := by
+  by_cases p : i = j <;> simp [p]
+
+@[simp] theorem getElem?_set_eq (a : Array α) (i : Nat) (h : i < a.size) (v : α) :
+    (a.set i v)[i]? = v := by simp [getElem?_lt, h]
+
+@[simp] theorem getElem?_set_ne (a : Array α) (i : Nat) (h : i < a.size) {j : Nat} (v : α)
+    (ne : i ≠ j) : (a.set i v)[j]? = a[j]? := by
+  by_cases h : j < a.size <;> simp [getElem?_lt, getElem?_ge, Nat.ge_of_not_lt, ne, h]
+
+/-! # setIfInBounds -/
+
+@[simp] theorem set!_is_setIfInBounds : @set! = @setIfInBounds := rfl
+
+@[simp] theorem size_setIfInBounds (a : Array α) (index : Nat) (val : α) :
+    (Array.setIfInBounds a index val).size = a.size := by
+  if h : index < a.size  then
+    simp [setIfInBounds, h]
+  else
+    simp [setIfInBounds, h]
+
+theorem getElem_setIfInBounds (a : Array α) (i : Nat) (v : α) (j : Nat)
+    (hj : j < (setIfInBounds a i v).size) :
+  (setIfInBounds a i v)[j]'hj = if i = j then v else a[j]'(by simpa using hj) := by
+  simp only [setIfInBounds]
+  split
+  · simp [getElem_set]
+  · simp only [size_setIfInBounds] at hj
+    rw [if_neg]
+    omega
+
+@[simp] theorem getElem_setIfInBounds_eq (a : Array α) {i : Nat} (v : α) (h : _) :
+    (setIfInBounds a i v)[i]'h = v := by
+  simp at h
+  simp only [setIfInBounds, h, ↓reduceDIte, getElem_set_eq]
+
+@[simp] theorem getElem_setIfInBounds_ne (a : Array α) {i : Nat} (v : α) {j : Nat}
+    (hj : j < (setIfInBounds a i v).size) (h : i ≠ j) :
+    (setIfInBounds a i v)[j]'hj = a[j]'(by simpa using hj) := by
+  simp [getElem_setIfInBounds, h]
+
+@[simp]
+theorem getElem?_setIfInBounds_eq (a : Array α) {i : Nat} (p : i < a.size) (v : α) :
+    (a.setIfInBounds i v)[i]? = some v := by
+  simp [getElem?_lt, p]
+
+/-- Simplifies a normal form from `get!` -/
+@[simp] theorem getD_get?_setIfInBounds (a : Array α) (i : Nat) (v d : α) :
+    Option.getD (setIfInBounds a i v)[i]? d = if i < a.size then v else d := by
+  by_cases h : i < a.size <;>
+    simp [setIfInBounds, Nat.not_lt_of_le, h,  getD_get?]
 
 /-! # ofFn -/
 
@@ -1185,6 +748,9 @@ theorem get_set (a : Array α) (i : Nat) (hi : i < a.size) (j : Nat) (hj : j < a
     (h : i ≠ j) : (a.set i v)[j]'(by simp [*]) = a[j] := by
   simp only [set, ← getElem_toList, List.getElem_set_ne h]
 
+theorem set_set (a : Array α) (i : Nat) (h) (v v' : α) :
+    (a.set i v h).set i v' (by simp [h]) = a.set i v' := by simp [set, List.set_set]
+
 private theorem fin_cast_val (e : n = n') (i : Fin n) : e ▸ i = ⟨i.1, e ▸ i.2⟩ := by cases e; rfl
 
 theorem swap_def (a : Array α) (i j : Nat) (hi hj) :
@@ -1926,6 +1492,119 @@ theorem extract_empty_of_size_le_start (as : Array α) {start stop : Nat} (h : a
 @[simp] theorem extract_empty (start stop : Nat) : (#[] : Array α).extract start stop = #[] :=
   extract_empty_of_size_le_start _ (Nat.zero_le _)
 
+/-! ### any -/
+
+theorem anyM_loop_cons [Monad m] (p : α → m Bool) (a : α) (as : List α) (stop start : Nat) (h : stop + 1 ≤ (a :: as).length) :
+    anyM.loop p ⟨a :: as⟩ (stop + 1) h (start + 1) = anyM.loop p ⟨as⟩ stop (by simpa using h) start := by
+  rw [anyM.loop]
+  conv => rhs; rw [anyM.loop]
+  split <;> rename_i h'
+  · simp only [Nat.add_lt_add_iff_right] at h'
+    rw [dif_pos h']
+    rw [anyM_loop_cons]
+    simp
+  · rw [dif_neg]
+    omega
+
+@[simp] theorem anyM_toList [Monad m] (p : α → m Bool) (as : Array α) :
+    as.toList.anyM p = as.anyM p :=
+  match as with
+  | ⟨[]⟩  => rfl
+  | ⟨a :: as⟩ => by
+    simp only [List.anyM, anyM, size_toArray, List.length_cons, Nat.le_refl, ↓reduceDIte]
+    rw [anyM.loop, dif_pos (by omega)]
+    congr 1
+    funext b
+    split
+    · simp
+    · simp only [Bool.false_eq_true, ↓reduceIte]
+      rw [anyM_loop_cons]
+      simpa [anyM] using anyM_toList p ⟨as⟩
+
+-- Auxiliary for `any_iff_exists`.
+theorem anyM_loop_iff_exists {p : α → Bool} {as : Array α} {start stop} (h : stop ≤ as.size) :
+    anyM.loop (m := Id) p as stop h start = true ↔
+      ∃ i : Fin as.size, start ≤ ↑i ∧ ↑i < stop ∧ p as[i] = true := by
+  unfold anyM.loop
+  split <;> rename_i h₁
+  · dsimp
+    split <;> rename_i h₂
+    · simp only [true_iff]
+      refine ⟨⟨start, by omega⟩, by dsimp; omega, by dsimp; omega, h₂⟩
+    · rw [anyM_loop_iff_exists]
+      constructor
+      · rintro ⟨i, ge, lt, h⟩
+        have : start ≠ i := by rintro rfl; omega
+        exact ⟨i, by omega, lt, h⟩
+      · rintro ⟨i, ge, lt, h⟩
+        have : start ≠ i := by rintro rfl; erw [h] at h₂; simp_all
+        exact ⟨i, by omega, lt, h⟩
+  · simp
+    omega
+termination_by stop - start
+
+-- This could also be proved from `SatisfiesM_anyM_iff_exists` in `Batteries.Data.Array.Init.Monadic`
+theorem any_iff_exists {p : α → Bool} {as : Array α} {start stop} :
+    as.any p start stop ↔ ∃ i : Fin as.size, start ≤ i.1 ∧ i.1 < stop ∧ p as[i] := by
+  dsimp [any, anyM, Id.run]
+  split
+  · rw [anyM_loop_iff_exists]; rfl
+  · rw [anyM_loop_iff_exists]
+    constructor
+    · rintro ⟨i, ge, _, h⟩
+      exact ⟨i, by omega, by omega, h⟩
+    · rintro ⟨i, ge, _, h⟩
+      exact ⟨i, by omega, by omega, h⟩
+
+theorem any_eq_true {p : α → Bool} {as : Array α} :
+    as.any p ↔ ∃ i : Fin as.size, p as[i] := by simp [any_iff_exists, Fin.isLt]
+
+theorem any_toList {p : α → Bool} (as : Array α) : as.toList.any p = as.any p := by
+  rw [Bool.eq_iff_iff, any_eq_true, List.any_eq_true]; simp only [List.mem_iff_get]
+  exact ⟨fun ⟨_, ⟨i, rfl⟩, h⟩ => ⟨i, h⟩, fun ⟨i, h⟩ => ⟨_, ⟨i, rfl⟩, h⟩⟩
+
+/-! ### all -/
+
+theorem allM_eq_not_anyM_not [Monad m] [LawfulMonad m] (p : α → m Bool) (as : Array α) :
+    allM p as = (! ·) <$> anyM ((! ·) <$> p ·) as := by
+  dsimp [allM, anyM]
+  simp
+
+@[simp] theorem allM_toList [Monad m] [LawfulMonad m] (p : α → m Bool) (as : Array α) :
+    as.toList.allM p = as.allM p := by
+  rw [allM_eq_not_anyM_not]
+  rw [← anyM_toList]
+  rw [List.allM_eq_not_anyM_not]
+
+theorem all_eq_not_any_not (p : α → Bool) (as : Array α) (start stop) :
+    as.all p start stop = !(as.any (!p ·) start stop) := by
+  dsimp [all, allM]
+  rfl
+
+theorem all_iff_forall {p : α → Bool} {as : Array α} {start stop} :
+    as.all p start stop ↔ ∀ i : Fin as.size, start ≤ i.1 ∧ i.1 < stop → p as[i] := by
+  rw [all_eq_not_any_not]
+  suffices ¬(as.any (!p ·) start stop = true) ↔
+      ∀ i : Fin as.size, start ≤ i.1 ∧ i.1 < stop → p as[i] by
+    simp_all
+  rw [any_iff_exists]
+  simp
+
+theorem all_eq_true {p : α → Bool} {as : Array α} : as.all p ↔ ∀ i : Fin as.size, p as[i] := by
+  simp [all_iff_forall, Fin.isLt]
+
+theorem all_toList {p : α → Bool} (as : Array α) : as.toList.all p = as.all p := by
+  rw [Bool.eq_iff_iff, all_eq_true, List.all_eq_true]; simp only [List.mem_iff_getElem]
+  constructor
+  · intro w i
+    exact w as[i] ⟨i, i.2, getElem_toList i.2⟩
+  · rintro w x ⟨r, h, rfl⟩
+    rw [getElem_toList]
+    exact w ⟨r, h⟩
+
+theorem all_eq_true_iff_forall_mem {l : Array α} : l.all p ↔ ∀ x, x ∈ l → p x := by
+  simp only [← all_toList, List.all_eq_true, mem_def]
+
 /-! ### contains -/
 
 theorem contains_def [DecidableEq α] {a : α} {as : Array α} : as.contains a ↔ a ∈ as := by
@@ -2088,6 +1767,54 @@ Our goal is to have `simp` "pull `List.toArray` outwards" as much as possible.
   apply ext'
   simp
 
+@[simp] theorem setIfInBounds_toArray (l : List α) (i : Nat) (a : α) :
+    l.toArray.setIfInBounds i a  = (l.set i a).toArray := by
+  apply ext'
+  simp only [setIfInBounds]
+  split
+  · simp
+  · simp_all [List.set_eq_of_length_le]
+
+theorem anyM_toArray [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α) :
+    l.toArray.anyM p = l.anyM p := by
+  rw [← anyM_toList]
+
+theorem any_toArray (p : α → Bool) (l : List α) : l.toArray.any p = l.any p := by
+  rw [any_toList]
+
+theorem allM_toArray [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α) :
+    l.toArray.allM p = l.allM p := by
+  rw [← allM_toList]
+
+theorem all_toArray (p : α → Bool) (l : List α) : l.toArray.all p = l.all p := by
+  rw [all_toList]
+
+/-- Variant of `anyM_toArray` with a side condition on `stop`. -/
+@[simp] theorem anyM_toArray' [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α)
+    (h : stop = l.toArray.size) :
+    l.toArray.anyM p 0 stop = l.anyM p := by
+  subst h
+  rw [← anyM_toList]
+
+/-- Variant of `any_toArray` with a side condition on `stop`. -/
+@[simp] theorem any_toArray' (p : α → Bool) (l : List α) (h : stop = l.toArray.size) :
+    l.toArray.any p 0 stop = l.any p := by
+  subst h
+  rw [any_toList]
+
+/-- Variant of `allM_toArray` with a side condition on `stop`. -/
+@[simp] theorem allM_toArray' [Monad m] [LawfulMonad m] (p : α → m Bool) (l : List α)
+    (h : stop = l.toArray.size) :
+    l.toArray.allM p 0 stop = l.allM p := by
+  subst h
+  rw [← allM_toList]
+
+/-- Variant of `all_toArray` with a side condition on `stop`. -/
+@[simp] theorem all_toArray' (p : α → Bool) (l : List α) (h : stop = l.toArray.size) :
+    l.toArray.all p 0 stop = l.all p := by
+  subst h
+  rw [all_toList]
+
 @[simp] theorem swap_toArray (l : List α) (i j : Nat) {hi hj}:
     l.toArray.swap i j hi hj = ((l.set i l[j]).set j l[i]).toArray := by
   apply ext'
@@ -2406,8 +2133,8 @@ abbrev eq_push_pop_back_of_size_ne_zero := @eq_push_pop_back!_of_size_ne_zero
 
 @[deprecated set!_is_setIfInBounds (since := "2024-11-24")] abbrev set_is_setIfInBounds := @set!_is_setIfInBounds
 @[deprecated size_setIfInBounds (since := "2024-11-24")] abbrev size_setD := @size_setIfInBounds
-@[deprecated getElem_setIfInBounds_eq (since := "2024-11-24")] abbrev getElem_setD_eq := @getElem_setIfInBounds_self
-@[deprecated getElem?_setIfInBounds_eq (since := "2024-11-24")] abbrev get?_setD_eq := @getElem?_setIfInBounds_self
+@[deprecated getElem_setIfInBounds_eq (since := "2024-11-24")] abbrev getElem_setD_eq := @getElem_setIfInBounds_eq
+@[deprecated getElem?_setIfInBounds_eq (since := "2024-11-24")] abbrev get?_setD_eq := @getElem?_setIfInBounds_eq
 @[deprecated getD_get?_setIfInBounds (since := "2024-11-24")] abbrev getD_setD := @getD_get?_setIfInBounds
 @[deprecated getElem_setIfInBounds (since := "2024-11-24")] abbrev getElem_setD := @getElem_setIfInBounds
 

src/Init/Data/BEq.lean

@@ -40,9 +40,6 @@ theorem BEq.symm [BEq α] [PartialEquivBEq α] {a b : α} : a == b → b == a :=
 theorem BEq.comm [BEq α] [PartialEquivBEq α] {a b : α} : (a == b) = (b == a) :=
   Bool.eq_iff_iff.2 ⟨BEq.symm, BEq.symm⟩
 
-theorem bne_comm [BEq α] [PartialEquivBEq α] {a b : α} : (a != b) = (b != a) := by
-  rw [bne, BEq.comm, bne]
-
 theorem BEq.symm_false [BEq α] [PartialEquivBEq α] {a b : α} : (a == b) = false → (b == a) = false :=
   BEq.comm (α := α) ▸ id
 

src/Init/Data/BitVec/Bitblast.lean

@@ -462,7 +462,7 @@ theorem msb_neg {w : Nat} {x : BitVec w} :
       case true =>
         apply hmin
         apply eq_of_getMsbD_eq
-        intro i hi
+        rintro ⟨i, hi⟩
         simp only [getMsbD_intMin, w_pos, decide_true, Bool.true_and]
         cases i
         case zero => exact hmsb
@@ -470,7 +470,7 @@ theorem msb_neg {w : Nat} {x : BitVec w} :
       case false =>
         apply hzero
         apply eq_of_getMsbD_eq
-        intro i hi
+        rintro ⟨i, hi⟩
         simp only [getMsbD_zero]
         cases i
         case zero => exact hmsb
@@ -573,11 +573,11 @@ theorem setWidth_setWidth_succ_eq_setWidth_setWidth_add_twoPow (x : BitVec w) (i
     setWidth w (x.setWidth (i + 1)) =
       setWidth w (x.setWidth i) + (x &&& twoPow w i) := by
   rw [add_eq_or_of_and_eq_zero]
-  · ext k h
-    simp only [getLsbD_setWidth, h, decide_true, Bool.true_and, getLsbD_or, getLsbD_and]
+  · ext k
+    simp only [getLsbD_setWidth, Fin.is_lt, decide_true, Bool.true_and, getLsbD_or, getLsbD_and]
     by_cases hik : i = k
     · subst hik
-      simp [h]
+      simp
     · simp only [getLsbD_twoPow, hik, decide_false, Bool.and_false, Bool.or_false]
       by_cases hik' : k < (i + 1)
       · have hik'' : k < i := by omega

src/Init/Data/BitVec/Lemmas.lean

@@ -173,21 +173,21 @@ theorem getMsbD_eq_getMsb?_getD (x : BitVec w) (i : Nat) :
 -- We choose `eq_of_getLsbD_eq` as the `@[ext]` theorem for `BitVec`
 -- somewhat arbitrarily over `eq_of_getMsbD_eq`.
 @[ext] theorem eq_of_getLsbD_eq {x y : BitVec w}
-    (pred : ∀ i, i < w → x.getLsbD i = y.getLsbD i) : x = y := by
+    (pred : ∀(i : Fin w), x.getLsbD i.val = y.getLsbD i.val) : x = y := by
   apply eq_of_toNat_eq
   apply Nat.eq_of_testBit_eq
   intro i
   if i_lt : i < w then
-    exact pred i i_lt
+    exact pred ⟨i, i_lt⟩
   else
     have p : i ≥ w := Nat.le_of_not_gt i_lt
     simp [testBit_toNat, getLsbD_ge _ _ p]
 
 theorem eq_of_getMsbD_eq {x y : BitVec w}
-    (pred : ∀ i, i < w → x.getMsbD i = y.getMsbD i) : x = y := by
+    (pred : ∀(i : Fin w), x.getMsbD i.val = y.getMsbD i.val) : x = y := by
   simp only [getMsbD] at pred
   apply eq_of_getLsbD_eq
-  intro i i_lt
+  intro ⟨i, i_lt⟩
   if w_zero : w = 0 then
     simp [w_zero]
   else
@@ -199,7 +199,7 @@ theorem eq_of_getMsbD_eq {x y : BitVec w}
       simp only [Nat.sub_sub]
       apply Nat.sub_lt w_pos
       simp [Nat.succ_add]
-    have q := pred (w - 1 - i) q_lt
+    have q := pred ⟨w - 1 - i, q_lt⟩
     simpa [q_lt, Nat.sub_sub_self, r] using q
 
 -- This cannot be a `@[simp]` lemma, as it would be tried at every term.
@@ -241,11 +241,8 @@ theorem toFin_one  : toFin (1 : BitVec w) = 1 := by
 @[simp] theorem toNat_ofBool (b : Bool) : (ofBool b).toNat = b.toNat := by
   cases b <;> rfl
 
-@[simp] theorem toInt_ofBool (b : Bool) : (ofBool b).toInt = -b.toInt := by
-  cases b <;> rfl
-
-@[simp] theorem toFin_ofBool (b : Bool) : (ofBool b).toFin = Fin.ofNat' 2 (b.toNat) := by
-  cases b <;> rfl
+@[simp] theorem msb_ofBool (b : Bool) : (ofBool b).msb = b := by
+  cases b <;> simp [BitVec.msb, getMsbD, getLsbD]
 
 theorem ofNat_one (n : Nat) : BitVec.ofNat 1 n = BitVec.ofBool (n % 2 = 1) :=  by
   rcases (Nat.mod_two_eq_zero_or_one n) with h | h <;> simp [h, BitVec.ofNat, Fin.ofNat']
@@ -369,12 +366,6 @@ theorem getElem_ofBool {b : Bool} {i : Nat} : (ofBool b)[0] = b := by
   · simp only [ofBool]
     by_cases hi : i = 0 <;> simp [hi] <;> omega
 
-@[simp] theorem getMsbD_ofBool (b : Bool) : (ofBool b).getMsbD i = (decide (i = 0) && b) := by
-  cases b <;> simp [getMsbD]
-
-@[simp] theorem msb_ofBool (b : Bool) : (ofBool b).msb = b := by
-  cases b <;> simp [BitVec.msb]
-
 /-! ### msb -/
 
 @[simp] theorem msb_zero : (0#w).msb = false := by simp [BitVec.msb, getMsbD]
@@ -507,9 +498,6 @@ theorem toInt_ofNat {n : Nat} (x : Nat) :
 @[simp] theorem ofInt_ofNat (w n : Nat) :
   BitVec.ofInt w (no_index (OfNat.ofNat n)) = BitVec.ofNat w (OfNat.ofNat n) := rfl
 
-@[simp] theorem ofInt_toInt {x : BitVec w} : BitVec.ofInt w x.toInt = x := by
-  by_cases h : 2 * x.toNat < 2^w <;> ext <;> simp [getLsbD, h, BitVec.toInt]
-
 theorem toInt_neg_iff {w : Nat} {x : BitVec w} :
     BitVec.toInt x < 0 ↔ 2 ^ w ≤ 2 * x.toNat := by
   simp [toInt_eq_toNat_cond]; omega
@@ -581,10 +569,6 @@ theorem zeroExtend_eq_setWidth {v : Nat} {x : BitVec w} :
     (x.setWidth v).toInt = Int.bmod x.toNat (2^v) := by
   simp [toInt_eq_toNat_bmod, toNat_setWidth, Int.emod_bmod]
 
-@[simp] theorem toFin_setWidth {x : BitVec w} :
-    (x.setWidth v).toFin = Fin.ofNat' (2^v) x.toNat := by
-  ext; simp
-
 theorem setWidth'_eq {x : BitVec w} (h : w ≤ v) : x.setWidth' h = x.setWidth v := by
   apply eq_of_toNat_eq
   rw [toNat_setWidth, toNat_setWidth']
@@ -661,20 +645,6 @@ theorem getElem?_setWidth (m : Nat) (x : BitVec n) (i : Nat) :
     getLsbD (setWidth m x) i = (decide (i < m) && getLsbD x i) := by
   simp [getLsbD, toNat_setWidth, Nat.testBit_mod_two_pow]
 
-theorem getMsbD_setWidth {m : Nat} {x : BitVec n} {i : Nat} :
-    getMsbD (setWidth m x) i = (decide (m - n ≤ i) && getMsbD x (i + n - m)) := by
-  unfold setWidth
-  by_cases h : n ≤ m <;> simp only [h]
-  · by_cases h' : m - n ≤ i
-    <;> simp [h', show i - (m - n) = i + n - m by omega]
-  · simp only [show m - n = 0 by omega, getMsbD, getLsbD_setWidth]
-    by_cases h' : i < m
-    · simp [show m - 1 - i < m by omega, show i + n - m < n by omega,
-        show n - 1 - (i + n - m) = m - 1 - i by omega]
-      omega
-    · simp [h']
-      omega
-
 @[simp] theorem getMsbD_setWidth_add {x : BitVec w} (h : k ≤ i) :
     (x.setWidth (w + k)).getMsbD i = x.getMsbD (i - k) := by
   by_cases h : w = 0
@@ -719,15 +689,14 @@ theorem msb_setWidth'' (x : BitVec w) : (x.setWidth (k + 1)).msb = x.getLsbD k :
 /-- zero extending a bitvector to width 1 equals the boolean of the lsb. -/
 theorem setWidth_one_eq_ofBool_getLsb_zero (x : BitVec w) :
     x.setWidth 1 = BitVec.ofBool (x.getLsbD 0) := by
-  ext i h
-  simp at h
-  simp [getLsbD_setWidth, h]
+  ext i
+  simp [getLsbD_setWidth, Fin.fin_one_eq_zero i]
 
 /-- Zero extending `1#v` to `1#w` equals `1#w` when `v > 0`. -/
 theorem setWidth_ofNat_one_eq_ofNat_one_of_lt {v w : Nat} (hv : 0 < v) :
     (BitVec.ofNat v 1).setWidth w = BitVec.ofNat w 1 := by
-  ext i h
-  simp only [getLsbD_setWidth, h, decide_true, getLsbD_ofNat, Bool.true_and,
+  ext ⟨i, hilt⟩
+  simp only [getLsbD_setWidth, hilt, decide_true, getLsbD_ofNat, Bool.true_and,
     Bool.and_iff_right_iff_imp, decide_eq_true_eq]
   intros hi₁
   have hv := Nat.testBit_one_eq_true_iff_self_eq_zero.mp hi₁
@@ -754,7 +723,8 @@ protected theorem extractLsb_ofFin {n} (x : Fin (2^n)) (hi lo : Nat) :
 @[simp]
 protected theorem extractLsb_ofNat (x n : Nat) (hi lo : Nat) :
   extractLsb hi lo (BitVec.ofNat n x) = .ofNat (hi - lo + 1) ((x % 2^n) >>> lo) := by
-  ext i
+  apply eq_of_getLsbD_eq
+  intro ⟨i, _lt⟩
   simp [BitVec.ofNat]
 
 @[simp] theorem extractLsb'_toNat (s m : Nat) (x : BitVec n) :
@@ -841,8 +811,8 @@ theorem extractLsb'_eq_extractLsb {w : Nat} (x : BitVec w) (start len : Nat) (h
 
 @[simp] theorem setWidth_or {x y : BitVec w} :
     (x ||| y).setWidth k = x.setWidth k ||| y.setWidth k := by
-  ext i h
-  simp [h]
+  ext
+  simp
 
 theorem or_assoc (x y z : BitVec w) :
     x ||| y ||| z = x ||| (y ||| z) := by
@@ -875,12 +845,12 @@ instance : Std.LawfulCommIdentity (α := BitVec n) (· ||| · ) (0#n) where
   simp
 
 @[simp] theorem or_allOnes {x : BitVec w} : x ||| allOnes w = allOnes w := by
-  ext i h
-  simp [h]
+  ext i
+  simp
 
 @[simp] theorem allOnes_or {x : BitVec w} : allOnes w ||| x = allOnes w := by
-  ext i h
-  simp [h]
+  ext i
+  simp
 
 /-! ### and -/
 
@@ -914,8 +884,8 @@ instance : Std.LawfulCommIdentity (α := BitVec n) (· ||| · ) (0#n) where
 
 @[simp] theorem setWidth_and {x y : BitVec w} :
     (x &&& y).setWidth k = x.setWidth k &&& y.setWidth k := by
-  ext i h
-  simp [h]
+  ext
+  simp
 
 theorem and_assoc (x y z : BitVec w) :
     x &&& y &&& z = x &&& (y &&& z) := by
@@ -945,15 +915,15 @@ instance : Std.IdempotentOp (α := BitVec n) (· &&& · ) where
   simp
 
 @[simp] theorem and_allOnes {x : BitVec w} : x &&& allOnes w = x := by
-  ext i h
-  simp [h]
+  ext i
+  simp
 
 instance : Std.LawfulCommIdentity (α := BitVec n) (· &&& · ) (allOnes n) where
   right_id _ := BitVec.and_allOnes
 
 @[simp] theorem allOnes_and {x : BitVec w} : allOnes w &&& x = x := by
-  ext i h
-  simp [h]
+  ext i
+  simp
 
 /-! ### xor -/
 
@@ -990,8 +960,8 @@ instance : Std.LawfulCommIdentity (α := BitVec n) (· &&& · ) (allOnes n) wher
 
 @[simp] theorem setWidth_xor {x y : BitVec w} :
     (x ^^^ y).setWidth k = x.setWidth k ^^^ y.setWidth k := by
-  ext i h
-  simp [h]
+  ext
+  simp
 
 theorem xor_assoc (x y z : BitVec w) :
     x ^^^ y ^^^ z = x ^^^ (y ^^^ z) := by
@@ -1084,9 +1054,9 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
   rw [Nat.testBit_two_pow_sub_succ x.isLt]
   simp [h]
 
-@[simp] theorem setWidth_not {x : BitVec w} (_ : k ≤ w) :
+@[simp] theorem setWidth_not {x : BitVec w} (h : k ≤ w) :
     (~~~x).setWidth k = ~~~(x.setWidth k) := by
-  ext i h
+  ext
   simp [h]
   omega
 
@@ -1099,17 +1069,17 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
   simp
 
 @[simp] theorem xor_allOnes {x : BitVec w} : x ^^^ allOnes w = ~~~ x := by
-  ext i h
-  simp [h]
+  ext i
+  simp
 
 @[simp] theorem allOnes_xor {x : BitVec w} : allOnes w ^^^ x = ~~~ x := by
-  ext i h
-  simp [h]
+  ext i
+  simp
 
 @[simp]
 theorem not_not {b : BitVec w} : ~~~(~~~b) = b := by
-  ext i h
-  simp [h]
+  ext i
+  simp
 
 theorem not_eq_comm {x y : BitVec w} : ~~~ x = y ↔ x = ~~~ y := by
   constructor
@@ -1184,21 +1154,24 @@ theorem zero_shiftLeft (n : Nat) : 0#w <<< n = 0#w := by
 
 theorem shiftLeft_xor_distrib (x y : BitVec w) (n : Nat) :
     (x ^^^ y) <<< n = (x <<< n) ^^^ (y <<< n) := by
-  ext i h
-  simp only [getLsbD_shiftLeft, h, decide_true, Bool.true_and, getLsbD_xor]
-  by_cases h' : i < n <;> simp [h']
+  ext i
+  simp only [getLsbD_shiftLeft, Fin.is_lt, decide_true, Bool.true_and, getLsbD_xor]
+  by_cases h : i < n
+    <;> simp [h]
 
 theorem shiftLeft_and_distrib (x y : BitVec w) (n : Nat) :
     (x &&& y) <<< n = (x <<< n) &&& (y <<< n) := by
-  ext i h
-  simp only [getLsbD_shiftLeft, h, decide_true, Bool.true_and, getLsbD_and]
-  by_cases h' : i < n <;> simp [h']
+  ext i
+  simp only [getLsbD_shiftLeft, Fin.is_lt, decide_true, Bool.true_and, getLsbD_and]
+  by_cases h : i < n
+    <;> simp [h]
 
 theorem shiftLeft_or_distrib (x y : BitVec w) (n : Nat) :
     (x ||| y) <<< n = (x <<< n) ||| (y <<< n) := by
-  ext i h
-  simp only [getLsbD_shiftLeft, h, decide_true, Bool.true_and, getLsbD_or]
-  by_cases h' : i < n <;> simp [h']
+  ext i
+  simp only [getLsbD_shiftLeft, Fin.is_lt, decide_true, Bool.true_and, getLsbD_or]
+  by_cases h : i < n
+    <;> simp [h]
 
 @[simp] theorem getMsbD_shiftLeft (x : BitVec w) (i) :
     (x <<< i).getMsbD k = x.getMsbD (k + i) := by
@@ -1537,12 +1510,12 @@ theorem msb_sshiftRight {n : Nat} {x : BitVec w} :
     simp [show n = 0 by omega]
 
 @[simp] theorem sshiftRight_zero {x : BitVec w} : x.sshiftRight 0 = x := by
-  ext i h
-  simp [getLsbD_sshiftRight, h]
+  ext i
+  simp [getLsbD_sshiftRight]
 
 @[simp] theorem zero_sshiftRight {n : Nat} : (0#w).sshiftRight n = 0#w := by
-  ext i h
-  simp [getLsbD_sshiftRight, h]
+  ext i
+  simp [getLsbD_sshiftRight]
 
 theorem sshiftRight_add {x : BitVec w} {m n : Nat} :
     x.sshiftRight (m + n) = (x.sshiftRight m).sshiftRight n := by
@@ -1643,7 +1616,7 @@ private theorem Int.negSucc_emod (m : Nat) (n : Int) :
     -(m + 1) % n = Int.subNatNat (Int.natAbs n) ((m % Int.natAbs n) + 1) := rfl
 
 /-- The sign extension is the same as zero extending when `msb = false`. -/
-theorem signExtend_eq_setWidth_of_msb_false {x : BitVec w} {v : Nat} (hmsb : x.msb = false) :
+theorem signExtend_eq_not_setWidth_not_of_msb_false {x : BitVec w} {v : Nat} (hmsb : x.msb = false) :
     x.signExtend v = x.setWidth v := by
   ext i
   by_cases hv : i < v
@@ -1679,36 +1652,21 @@ theorem signExtend_eq_not_setWidth_not_of_msb_true {x : BitVec w} {v : Nat} (hms
 theorem getLsbD_signExtend (x  : BitVec w) {v i : Nat} :
     (x.signExtend v).getLsbD i = (decide (i < v) && if i < w then x.getLsbD i else x.msb) := by
   rcases hmsb : x.msb with rfl | rfl
-  · rw [signExtend_eq_setWidth_of_msb_false hmsb]
+  · rw [signExtend_eq_not_setWidth_not_of_msb_false hmsb]
     by_cases (i < v) <;> by_cases (i < w) <;> simp_all <;> omega
   · rw [signExtend_eq_not_setWidth_not_of_msb_true hmsb]
     by_cases (i < v) <;> by_cases (i < w) <;> simp_all <;> omega
 
-theorem getMsbD_signExtend {x : BitVec w} {v i : Nat} :
-    (x.signExtend v).getMsbD i =
-      (decide (i < v) && if v - w ≤ i then x.getMsbD (i + w - v) else x.msb) := by
-  rcases hmsb : x.msb with rfl | rfl
-  · simp only [signExtend_eq_setWidth_of_msb_false hmsb, getMsbD_setWidth]
-    by_cases h : v - w ≤ i <;> simp [h, getMsbD] <;> omega
-  · simp only [signExtend_eq_not_setWidth_not_of_msb_true hmsb, getMsbD_not, getMsbD_setWidth]
-    by_cases h : i < v <;> by_cases h' : v - w ≤ i <;> simp [h, h'] <;> omega
-
 theorem getElem_signExtend {x  : BitVec w} {v i : Nat} (h : i < v) :
     (x.signExtend v)[i] = if i < w then x.getLsbD i else x.msb := by
   rw [←getLsbD_eq_getElem, getLsbD_signExtend]
   simp [h]
 
-theorem msb_signExtend {x : BitVec w} :
-    (x.signExtend v).msb = (decide (0 < v) && if w ≥ v then x.getMsbD (w - v) else x.msb) := by
-  by_cases h : w ≥ v
-  · simp [h, BitVec.msb, getMsbD_signExtend, show v - w = 0 by omega]
-  · simp [h, BitVec.msb, getMsbD_signExtend, show ¬ (v - w = 0) by omega]
-
 /-- Sign extending to a width smaller than the starting width is a truncation. -/
 theorem signExtend_eq_setWidth_of_lt (x : BitVec w) {v : Nat} (hv : v ≤ w):
   x.signExtend v = x.setWidth v := by
-  ext i h
-  simp only [getLsbD_signExtend, h, decide_true, Bool.true_and, getLsbD_setWidth,
+  ext i
+  simp only [getLsbD_signExtend, Fin.is_lt, decide_true, Bool.true_and, getLsbD_setWidth,
     ite_eq_left_iff, Nat.not_lt]
   omega
 
@@ -1802,34 +1760,35 @@ theorem append_def (x : BitVec v) (y : BitVec w) :
   rfl
 
 theorem getLsbD_append {x : BitVec n} {y : BitVec m} :
-    getLsbD (x ++ y) i = if i < m then getLsbD y i else getLsbD x (i - m) := by
+    getLsbD (x ++ y) i = bif i < m then getLsbD y i else getLsbD x (i - m) := by
   simp only [append_def, getLsbD_or, getLsbD_shiftLeftZeroExtend, getLsbD_setWidth']
   by_cases h : i < m
   · simp [h]
   · simp_all [h]
 
 theorem getElem_append {x : BitVec n} {y : BitVec m} (h : i < n + m) :
-    (x ++ y)[i] = if i < m then getLsbD y i else getLsbD x (i - m) := by
+    (x ++ y)[i] = bif i < m then getLsbD y i else getLsbD x (i - m) := by
   simp only [append_def, getElem_or, getElem_shiftLeftZeroExtend, getElem_setWidth']
   by_cases h' : i < m
   · simp [h']
   · simp_all [h']
 
 @[simp] theorem getMsbD_append {x : BitVec n} {y : BitVec m} :
-    getMsbD (x ++ y) i = if n ≤ i then getMsbD y (i - n) else getMsbD x i := by
+    getMsbD (x ++ y) i = bif n ≤ i then getMsbD y (i - n) else getMsbD x i := by
   simp only [append_def]
   by_cases h : n ≤ i
   · simp [h]
   · simp [h]
 
 theorem msb_append {x : BitVec w} {y : BitVec v} :
-    (x ++ y).msb = if w = 0 then y.msb else x.msb := by
+    (x ++ y).msb = bif (w == 0) then (y.msb) else (x.msb) := by
   rw [← append_eq, append]
   simp only [msb_or, msb_shiftLeftZeroExtend, msb_setWidth']
   by_cases h : w = 0
   · subst h
     simp [BitVec.msb, getMsbD]
-  · have q : 0 < w + v := by omega
+  · rw [cond_eq_if]
+    have q : 0 < w + v := by omega
     have t : y.getLsbD (w + v - 1) = false := getLsbD_ge _ _ (by omega)
     simp [h, q, t, BitVec.msb, getMsbD]
 
@@ -1845,7 +1804,7 @@ theorem msb_append {x : BitVec w} {y : BitVec v} :
 
 @[simp] theorem zero_append_zero : 0#v ++ 0#w = 0#(v + w) := by
   ext
-  simp only [getLsbD_append, getLsbD_zero, ite_self]
+  simp only [getLsbD_append, getLsbD_zero, Bool.cond_self]
 
 @[simp] theorem cast_append_right (h : w + v = w + v') (x : BitVec w) (y : BitVec v) :
     (x ++ y).cast h = x ++ y.cast (by omega) := by
@@ -1865,19 +1824,21 @@ theorem msb_append {x : BitVec w} {y : BitVec v} :
 
 theorem setWidth_append {x : BitVec w} {y : BitVec v} :
     (x ++ y).setWidth k = if h : k ≤ v then y.setWidth k else (x.setWidth (k - v) ++ y).cast (by omega) := by
-  ext i h
-  simp only [getLsbD_setWidth, h, getLsbD_append]
-  split <;> rename_i h₁ <;> split <;> rename_i h₂
-  · simp [h]
-  · simp [getLsbD_append, h₁]
-  · omega
-  · simp [getLsbD_append, h₁]
-    omega
+  apply eq_of_getLsbD_eq
+  intro i
+  simp only [getLsbD_setWidth, Fin.is_lt, decide_true, getLsbD_append, Bool.true_and]
+  split
+  · have t : i < v := by omega
+    simp [t]
+  · by_cases t : i < v
+    · simp [t, getLsbD_append]
+    · have t' : i - v < k - v := by omega
+      simp [t, t', getLsbD_append]
 
 @[simp] theorem setWidth_append_of_eq {x : BitVec v} {y : BitVec w} (h : w' = w) : setWidth (v' + w') (x ++ y) = setWidth v' x ++ setWidth w' y := by
   subst h
-  ext i h
-  simp only [getLsbD_setWidth, h, decide_true, getLsbD_append, cond_eq_if,
+  ext i
+  simp only [getLsbD_setWidth, Fin.is_lt, decide_true, getLsbD_append, cond_eq_if,
     decide_eq_true_eq, Bool.true_and, setWidth_eq]
   split
   · simp_all
@@ -1927,12 +1888,12 @@ theorem shiftLeft_ushiftRight {x : BitVec w} {n : Nat}:
   case succ n ih =>
     rw [BitVec.shiftLeft_add, Nat.add_comm, BitVec.shiftRight_add, ih,
        Nat.add_comm, BitVec.shiftLeft_add, BitVec.shiftLeft_and_distrib]
-    ext i h
+    ext i
     by_cases hw : w = 0
     · simp [hw]
-    · by_cases hi₂ : i = 0
+    · by_cases hi₂ : i.val = 0
       · simp [hi₂]
-      · simp [Nat.lt_one_iff, hi₂, h, show 1 + (i - 1) = i by omega]
+      · simp [Nat.lt_one_iff, hi₂, show 1 + (i.val - 1) = i by omega]
 
 @[simp]
 theorem msb_shiftLeft {x : BitVec w} {n : Nat} :
@@ -2017,12 +1978,13 @@ theorem getElem_cons {b : Bool} {n} {x : BitVec n} {i : Nat} (h : i < n + 1) :
 
 theorem setWidth_succ (x : BitVec w) :
     setWidth (i+1) x = cons (getLsbD x i) (setWidth i x) := by
-  ext j h
-  simp only [getLsbD_setWidth, getLsbD_cons, h, decide_true, Bool.true_and]
-  if j_eq : j = i then
+  apply eq_of_getLsbD_eq
+  intro j
+  simp only [getLsbD_setWidth, getLsbD_cons, j.isLt, decide_true, Bool.true_and]
+  if j_eq : j.val = i then
     simp [j_eq]
   else
-    have j_lt : j < i := Nat.lt_of_le_of_ne (Nat.le_of_succ_le_succ h) j_eq
+    have j_lt : j.val < i := Nat.lt_of_le_of_ne (Nat.le_of_succ_le_succ j.isLt) j_eq
     simp [j_eq, j_lt]
 
 @[simp] theorem cons_msb_setWidth (x : BitVec (w+1)) : (cons x.msb (x.setWidth w)) = x := by
@@ -2136,19 +2098,19 @@ theorem msb_concat {w : Nat} {b : Bool} {x : BitVec w} :
   simp [← Fin.val_inj]
 
 @[simp] theorem not_concat (x : BitVec w) (b : Bool) : ~~~(concat x b) = concat (~~~x) !b := by
-  ext (_ | i) h <;> simp [getLsbD_concat]
+  ext i; cases i using Fin.succRecOn <;> simp [*, Nat.succ_lt_succ]
 
 @[simp] theorem concat_or_concat (x y : BitVec w) (a b : Bool) :
     (concat x a) ||| (concat y b) = concat (x ||| y) (a || b) := by
-  ext (_ | i) h <;> simp [getLsbD_concat]
+  ext i; cases i using Fin.succRecOn <;> simp
 
 @[simp] theorem concat_and_concat (x y : BitVec w) (a b : Bool) :
     (concat x a) &&& (concat y b) = concat (x &&& y) (a && b) := by
-  ext (_ | i) h <;> simp [getLsbD_concat]
+  ext i; cases i using Fin.succRecOn <;> simp
 
 @[simp] theorem concat_xor_concat (x y : BitVec w) (a b : Bool) :
     (concat x a) ^^^ (concat y b) = concat (x ^^^ y) (a ^^ b) := by
-  ext (_ | i) h <;> simp [getLsbD_concat]
+  ext i; cases i using Fin.succRecOn <;> simp
 
 @[simp] theorem zero_concat_false : concat 0#w false = 0#(w + 1) := by
   ext
@@ -2169,8 +2131,8 @@ theorem getLsbD_shiftConcat_eq_decide (x : BitVec w) (b : Bool) (i : Nat) :
 
 theorem shiftRight_sub_one_eq_shiftConcat (n : BitVec w) (hwn : 0 < wn) :
     n >>> (wn - 1) = (n >>> wn).shiftConcat (n.getLsbD (wn - 1)) := by
-  ext i h
-  simp only [getLsbD_ushiftRight, getLsbD_shiftConcat, h, decide_true, Bool.true_and]
+  ext i
+  simp only [getLsbD_ushiftRight, getLsbD_shiftConcat, Fin.is_lt, decide_true, Bool.true_and]
   split
   · simp [*]
   · congr 1; omega
@@ -3181,8 +3143,8 @@ theorem setWidth_setWidth_succ_eq_setWidth_setWidth_of_getLsbD_false
   {x : BitVec w} {i : Nat} (hx : x.getLsbD i = false) :
     setWidth w (x.setWidth (i + 1)) =
       setWidth w (x.setWidth i) := by
-  ext k h
-  simp only [getLsbD_setWidth, h, decide_true, Bool.true_and, getLsbD_or, getLsbD_and]
+  ext k
+  simp only [getLsbD_setWidth, Fin.is_lt, decide_true, Bool.true_and, getLsbD_or, getLsbD_and]
   by_cases hik : i = k
   · subst hik
     simp [hx]
@@ -3197,17 +3159,20 @@ theorem setWidth_setWidth_succ_eq_setWidth_setWidth_or_twoPow_of_getLsbD_true
     {x : BitVec w} {i : Nat} (hx : x.getLsbD i = true) :
     setWidth w (x.setWidth (i + 1)) =
       setWidth w (x.setWidth i) ||| (twoPow w i) := by
-  ext k h
-  simp only [getLsbD_setWidth, h, decide_true, Bool.true_and, getLsbD_or, getLsbD_and]
+  ext k
+  simp only [getLsbD_setWidth, Fin.is_lt, decide_true, Bool.true_and, getLsbD_or, getLsbD_and]
   by_cases hik : i = k
   · subst hik
-    simp [hx, h]
+    simp [hx]
   · by_cases hik' : k < i + 1 <;> simp [hik, hik'] <;> omega
 
 /-- Bitwise and of `(x : BitVec w)` with `1#w` equals zero extending `x.lsb` to `w`. -/
 theorem and_one_eq_setWidth_ofBool_getLsbD {x : BitVec w} :
     (x &&& 1#w) = setWidth w (ofBool (x.getLsbD 0)) := by
-  ext (_ | i) h <;> simp [Bool.and_comm]
+  ext i
+  simp only [getLsbD_and, getLsbD_one, getLsbD_setWidth, Fin.is_lt, decide_true, getLsbD_ofBool,
+    Bool.true_and]
+  by_cases h : ((i : Nat) = 0) <;> simp [h] <;> omega
 
 @[simp]
 theorem replicate_zero_eq {x : BitVec w} : x.replicate 0 = 0#0 := by
@@ -3231,7 +3196,7 @@ theorem getLsbD_replicate {n w : Nat} (x : BitVec w) :
     · simp only [hi, decide_true, Bool.true_and]
       by_cases hi' : i < w * n
       · simp [hi', ih]
-      · simp [hi', decide_false]
+      · simp only [hi', decide_false, cond_false]
         rw [Nat.sub_mul_eq_mod_of_lt_of_le] <;> omega
     · rw [Nat.mul_succ] at hi ⊢
       simp only [show ¬i < w * n by omega, decide_false, cond_false, hi, Bool.false_and]
@@ -3537,7 +3502,7 @@ theorem forall_zero_iff {P : BitVec 0 → Prop} :
   · intro h
     apply h
   · intro h v
-    obtain (rfl : v = 0#0) := (by ext i ⟨⟩)
+    obtain (rfl : v = 0#0) := (by ext ⟨i, h⟩; simp at h)
     apply h
 
 theorem forall_cons_iff {P : BitVec (n + 1) → Prop} :
@@ -3553,7 +3518,7 @@ theorem forall_cons_iff {P : BitVec (n + 1) → Prop} :
 instance instDecidableForallBitVecZero (P : BitVec 0 → Prop) :
     ∀ [Decidable (P 0#0)], Decidable (∀ v, P v)
   | .isTrue h => .isTrue fun v => by
-    obtain (rfl : v = 0#0) := (by ext i ⟨⟩)
+    obtain (rfl : v = 0#0) := (by ext ⟨i, h⟩; cases h)
     exact h
   | .isFalse h => .isFalse (fun w => h (w _))
 
@@ -3598,9 +3563,6 @@ instance instDecidableExistsBitVec :
 
 set_option linter.missingDocs false
 
-@[deprecated signExtend_eq_setWidth_of_msb_false (since := "2024-12-08")]
-abbrev signExtend_eq_not_setWidth_not_of_msb_false := @signExtend_eq_setWidth_of_msb_false
-
 @[deprecated truncate_eq_setWidth (since := "2024-09-18")]
 abbrev truncate_eq_zeroExtend := @truncate_eq_setWidth
 
@@ -3703,8 +3665,8 @@ abbrev truncate_xor := @setWidth_xor
 @[deprecated setWidth_not (since := "2024-09-18")]
 abbrev truncate_not := @setWidth_not
 
-@[deprecated signExtend_eq_setWidth_of_msb_false  (since := "2024-09-18")]
-abbrev signExtend_eq_not_zeroExtend_not_of_msb_false  := @signExtend_eq_setWidth_of_msb_false
+@[deprecated signExtend_eq_not_setWidth_not_of_msb_false  (since := "2024-09-18")]
+abbrev signExtend_eq_not_zeroExtend_not_of_msb_false  := @signExtend_eq_not_setWidth_not_of_msb_false
 
 @[deprecated signExtend_eq_not_setWidth_not_of_msb_true (since := "2024-09-18")]
 abbrev signExtend_eq_not_zeroExtend_not_of_msb_true := @signExtend_eq_not_setWidth_not_of_msb_true

src/Init/Data/Float32.lean

@@ -1,180 +0,0 @@
-/-
-Copyright (c) 2023 Amazon.com, Inc. or its affiliates. All Rights Reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
--/
-prelude
-import Init.Core
-import Init.Data.Int.Basic
-import Init.Data.ToString.Basic
-import Init.Data.Float
-
-/-
-#exit -- TODO: Remove after update stage0
-
--- Just show FloatSpec is inhabited.
-opaque float32Spec : FloatSpec := {
-  float := Unit,
-  val   := (),
-  lt    := fun _ _ => True,
-  le    := fun _ _ => True,
-  decLt := fun _ _ => inferInstanceAs (Decidable True),
-  decLe := fun _ _ => inferInstanceAs (Decidable True)
-}
-
-/-- Native floating point type, corresponding to the IEEE 754 *binary32* format
-(`float` in C or `f32` in Rust). -/
-structure Float32 where
-  val : float32Spec.float
-
-instance : Nonempty Float32 := ⟨{ val := float32Spec.val }⟩
-
-@[extern "lean_float32_add"] opaque Float32.add : Float32 → Float32 → Float32
-@[extern "lean_float32_sub"] opaque Float32.sub : Float32 → Float32 → Float32
-@[extern "lean_float32_mul"] opaque Float32.mul : Float32 → Float32 → Float32
-@[extern "lean_float32_div"] opaque Float32.div : Float32 → Float32 → Float32
-@[extern "lean_float32_negate"] opaque Float32.neg : Float32 → Float32
-
-set_option bootstrap.genMatcherCode false
-def Float32.lt : Float32 → Float32 → Prop := fun a b =>
-  match a, b with
-  | ⟨a⟩, ⟨b⟩ => float32Spec.lt a b
-
-def Float32.le : Float32 → Float32 → Prop := fun a b =>
-  float32Spec.le a.val b.val
-
-/--
-Raw transmutation from `UInt32`.
-
-Float32s and UInts have the same endianness on all supported platforms.
-IEEE 754 very precisely specifies the bit layout of floats.
--/
-@[extern "lean_float32_of_bits"] opaque Float32.ofBits : UInt32 → Float32
-
-/--
-Raw transmutation to `UInt32`.
-
-Float32s and UInts have the same endianness on all supported platforms.
-IEEE 754 very precisely specifies the bit layout of floats.
-
-Note that this function is distinct from `Float32.toUInt32`, which attempts
-to preserve the numeric value, and not the bitwise value.
--/
-@[extern "lean_float32_to_bits"] opaque Float32.toBits : Float32 → UInt32
-
-instance : Add Float32 := ⟨Float32.add⟩
-instance : Sub Float32 := ⟨Float32.sub⟩
-instance : Mul Float32 := ⟨Float32.mul⟩
-instance : Div Float32 := ⟨Float32.div⟩
-instance : Neg Float32 := ⟨Float32.neg⟩
-instance : LT Float32  := ⟨Float32.lt⟩
-instance : LE Float32  := ⟨Float32.le⟩
-
-/-- Note: this is not reflexive since `NaN != NaN`.-/
-@[extern "lean_float32_beq"] opaque Float32.beq (a b : Float32) : Bool
-
-instance : BEq Float32 := ⟨Float32.beq⟩
-
-@[extern "lean_float32_decLt"] opaque Float32.decLt (a b : Float32) : Decidable (a < b) :=
-  match a, b with
-  | ⟨a⟩, ⟨b⟩ => float32Spec.decLt a b
-
-@[extern "lean_float32_decLe"] opaque Float32.decLe (a b : Float32) : Decidable (a ≤ b) :=
-  match a, b with
-  | ⟨a⟩, ⟨b⟩ => float32Spec.decLe a b
-
-instance float32DecLt (a b : Float32) : Decidable (a < b) := Float32.decLt a b
-instance float32DecLe (a b : Float32) : Decidable (a ≤ b) := Float32.decLe a b
-
-@[extern "lean_float32_to_string"] opaque Float32.toString : Float32 → String
-/-- If the given float is non-negative, truncates the value to the nearest non-negative integer.
-If negative or NaN, returns `0`.
-If larger than the maximum value for `UInt8` (including Inf), returns the maximum value of `UInt8`
-(i.e. `UInt8.size - 1`).
--/
-@[extern "lean_float32_to_uint8"] opaque Float32.toUInt8 : Float32 → UInt8
-/-- If the given float is non-negative, truncates the value to the nearest non-negative integer.
-If negative or NaN, returns `0`.
-If larger than the maximum value for `UInt16` (including Inf), returns the maximum value of `UInt16`
-(i.e. `UInt16.size - 1`).
--/
-@[extern "lean_float32_to_uint16"] opaque Float32.toUInt16 : Float32 → UInt16
-/-- If the given float is non-negative, truncates the value to the nearest non-negative integer.
-If negative or NaN, returns `0`.
-If larger than the maximum value for `UInt32` (including Inf), returns the maximum value of `UInt32`
-(i.e. `UInt32.size - 1`).
--/
-@[extern "lean_float32_to_uint32"] opaque Float32.toUInt32 : Float32 → UInt32
-/-- If the given float is non-negative, truncates the value to the nearest non-negative integer.
-If negative or NaN, returns `0`.
-If larger than the maximum value for `UInt64` (including Inf), returns the maximum value of `UInt64`
-(i.e. `UInt64.size - 1`).
--/
-@[extern "lean_float32_to_uint64"] opaque Float32.toUInt64 : Float32 → UInt64
-/-- If the given float is non-negative, truncates the value to the nearest non-negative integer.
-If negative or NaN, returns `0`.
-If larger than the maximum value for `USize` (including Inf), returns the maximum value of `USize`
-(i.e. `USize.size - 1`). This value is platform dependent).
--/
-@[extern "lean_float32_to_usize"] opaque Float32.toUSize : Float32 → USize
-
-@[extern "lean_float32_isnan"] opaque Float32.isNaN : Float32 → Bool
-@[extern "lean_float32_isfinite"] opaque Float32.isFinite : Float32 → Bool
-@[extern "lean_float32_isinf"] opaque Float32.isInf : Float32 → Bool
-/-- Splits the given float `x` into a significand/exponent pair `(s, i)`
-such that `x = s * 2^i` where `s ∈ (-1;-0.5] ∪ [0.5; 1)`.
-Returns an undefined value if `x` is not finite.
--/
-@[extern "lean_float32_frexp"] opaque Float32.frExp : Float32 → Float32 × Int
-
-instance : ToString Float32 where
-  toString := Float32.toString
-
-@[extern "lean_uint64_to_float"] opaque UInt64.toFloat32 (n : UInt64) : Float32
-
-instance : Inhabited Float32 where
-  default := UInt64.toFloat32 0
-
-instance : Repr Float32 where
-  reprPrec n prec := if n < UInt64.toFloat32 0 then Repr.addAppParen (toString n) prec else toString n
-
-instance : ReprAtom Float32  := ⟨⟩
-
-@[extern "sinf"] opaque Float32.sin : Float32 → Float32
-@[extern "cosf"] opaque Float32.cos : Float32 → Float32
-@[extern "tanf"] opaque Float32.tan : Float32 → Float32
-@[extern "asinf"] opaque Float32.asin : Float32 → Float32
-@[extern "acosf"] opaque Float32.acos : Float32 → Float32
-@[extern "atanf"] opaque Float32.atan : Float32 → Float32
-@[extern "atan2f"] opaque Float32.atan2 : Float32 → Float32 → Float32
-@[extern "sinhf"] opaque Float32.sinh : Float32 → Float32
-@[extern "coshf"] opaque Float32.cosh : Float32 → Float32
-@[extern "tanhf"] opaque Float32.tanh : Float32 → Float32
-@[extern "asinhf"] opaque Float32.asinh : Float32 → Float32
-@[extern "acoshf"] opaque Float32.acosh : Float32 → Float32
-@[extern "atanhf"] opaque Float32.atanh : Float32 → Float32
-@[extern "expf"] opaque Float32.exp : Float32 → Float32
-@[extern "exp2f"] opaque Float32.exp2 : Float32 → Float32
-@[extern "logf"] opaque Float32.log : Float32 → Float32
-@[extern "log2f"] opaque Float32.log2 : Float32 → Float32
-@[extern "log10f"] opaque Float32.log10 : Float32 → Float32
-@[extern "powf"] opaque Float32.pow : Float32 → Float32 → Float32
-@[extern "sqrtf"] opaque Float32.sqrt : Float32 → Float32
-@[extern "cbrtf"] opaque Float32.cbrt : Float32 → Float32
-@[extern "ceilf"] opaque Float32.ceil : Float32 → Float32
-@[extern "floorf"] opaque Float32.floor : Float32 → Float32
-@[extern "roundf"] opaque Float32.round : Float32 → Float32
-@[extern "fabsf"] opaque Float32.abs : Float32 → Float32
-
-instance : HomogeneousPow Float32 := ⟨Float32.pow⟩
-
-instance : Min Float32 := minOfLe
-
-instance : Max Float32 := maxOfLe
-
-/--
-Efficiently computes `x * 2^i`.
--/
-@[extern "lean_float32_scaleb"]
-opaque Float32.scaleB (x : Float32) (i : @& Int) : Float32
--/

src/Init/Data/List/Basic.lean

@@ -666,14 +666,10 @@ def isEmpty : List α → Bool
 /-! ### elem -/
 
 /--
-`O(|l|)`.
-`l.contains a` or `elem a l` is true if there is an element in `l` equal (according to `==`) to `a`.
+`O(|l|)`. `elem a l` or `l.contains a` is true if there is an element in `l` equal to `a`.
 
-* `[1, 4, 2, 3, 3, 7].contains 3 = true`
-* `[1, 4, 2, 3, 3, 7].contains 5 = false`
-
-The preferred simp normal form is `l.contains a`, and when `LawfulBEq α` is available,
-`l.contains a = true ↔ a ∈ l` and `l.contains a = false ↔ a ∉ l`.
+* `elem 3 [1, 4, 2, 3, 3, 7] = true`
+* `elem 5 [1, 4, 2, 3, 3, 7] = false`
 -/
 def elem [BEq α] (a : α) : List α → Bool
   | []    => false

src/Init/Data/List/Lemmas.lean

@@ -253,21 +253,8 @@ theorem getElem_eq_getElem?_get (l : List α) (i : Nat) (h : i < l.length) :
     l[i] = l[i]?.get (by simp [getElem?_eq_getElem, h]) := by
   simp [getElem_eq_iff]
 
-theorem getD_getElem? (l : List α) (i : Nat) (d : α) :
-    l[i]?.getD d = if p : i < l.length then l[i]'p else d := by
-  if h : i < l.length then
-    simp [h, getElem?_def]
-  else
-    have p : i ≥ l.length := Nat.le_of_not_gt h
-    simp [getElem?_eq_none p, h]
-
 @[simp] theorem getElem?_nil {n : Nat} : ([] : List α)[n]? = none := rfl
 
-theorem getElem_cons {l : List α} (w : i < (a :: l).length) :
-    (a :: l)[i] =
-      if h : i = 0 then a else l[i-1]'(match i, h with | i+1, _ => succ_lt_succ_iff.mp w) := by
-  cases i <;> simp
-
 theorem getElem?_cons_zero {l : List α} : (a::l)[0]? = some a := by simp
 
 @[simp] theorem getElem?_cons_succ {l : List α} : (a::l)[n+1]? = l[n]? := by
@@ -277,6 +264,11 @@ theorem getElem?_cons_zero {l : List α} : (a::l)[0]? = some a := by simp
 theorem getElem?_cons : (a :: l)[i]? = if i = 0 then some a else l[i-1]? := by
   cases i <;> simp
 
+theorem getElem_cons {l : List α} (w : i < (a :: l).length) :
+    (a :: l)[i] =
+      if h : i = 0 then a else l[i-1]'(match i, h with | i+1, _ => succ_lt_succ_iff.mp w) := by
+  cases i <;> simp
+
 @[simp] theorem getElem_singleton (a : α) (h : i < 1) : [a][i] = a :=
   match i, h with
   | 0, _ => rfl
@@ -459,10 +451,6 @@ theorem forall_getElem {l : List α} {p : α → Prop} :
         simp only [getElem_cons_succ]
         exact getElem_mem (lt_of_succ_lt_succ h)
 
-@[simp] theorem elem_eq_contains [BEq α] {a : α} {l : List α} :
-    elem a l = l.contains a := by
-  simp [contains]
-
 @[simp] theorem decide_mem_cons [BEq α] [LawfulBEq α] {l : List α} :
     decide (y ∈ a :: l) = (y == a || decide (y ∈ l)) := by
   cases h : y == a <;> simp_all
@@ -470,27 +458,16 @@ theorem forall_getElem {l : List α} {p : α → Prop} :
 theorem elem_iff [BEq α] [LawfulBEq α] {a : α} {as : List α} :
     elem a as = true ↔ a ∈ as := ⟨mem_of_elem_eq_true, elem_eq_true_of_mem⟩
 
-theorem contains_iff [BEq α] [LawfulBEq α] {a : α} {as : List α} :
-    as.contains a = true ↔ a ∈ as := ⟨mem_of_elem_eq_true, elem_eq_true_of_mem⟩
-
-theorem elem_eq_mem [BEq α] [LawfulBEq α] (a : α) (as : List α) :
+@[simp] theorem elem_eq_mem [BEq α] [LawfulBEq α] (a : α) (as : List α) :
     elem a as = decide (a ∈ as) := by rw [Bool.eq_iff_iff, elem_iff, decide_eq_true_iff]
 
-@[simp] theorem contains_eq_mem [BEq α] [LawfulBEq α] (a : α) (as : List α) :
-    as.contains a = decide (a ∈ as) := by rw [Bool.eq_iff_iff, elem_iff, decide_eq_true_iff]
-
-@[simp] theorem contains_cons [BEq α] {a : α} {b : α} {l : List α} :
-    (a :: l).contains b = (b == a || l.contains b) := by
-  simp only [contains, elem_cons]
-  split <;> simp_all
-
 /-! ### `isEmpty` -/
 
 theorem isEmpty_iff {l : List α} : l.isEmpty ↔ l = [] := by
   cases l <;> simp
 
 theorem isEmpty_eq_false_iff_exists_mem {xs : List α} :
-    xs.isEmpty = false ↔ ∃ x, x ∈ xs := by
+    (List.isEmpty xs = false) ↔ ∃ x, x ∈ xs := by
   cases xs <;> simp
 
 theorem isEmpty_iff_length_eq_zero {l : List α} : l.isEmpty ↔ l.length = 0 := by
@@ -528,21 +505,17 @@ theorem decide_forall_mem {l : List α} {p : α → Prop} [DecidablePred p] :
 @[simp] theorem all_eq_false {l : List α} : l.all p = false ↔ ∃ x, x ∈ l ∧ ¬p x := by
   simp [all_eq]
 
-theorem any_beq [BEq α] {l : List α} {a : α} : (l.any fun x => a == x) = l.contains a := by
-  induction l <;> simp_all [contains_cons]
+theorem any_beq [BEq α] [LawfulBEq α] {l : List α} : (l.any fun x => a == x) ↔ a ∈ l := by
+  simp
 
-/-- Variant of `any_beq` with `==` reversed. -/
-theorem any_beq' [BEq α] [PartialEquivBEq α] {l : List α} :
-    (l.any fun x => x == a) = l.contains a := by
-  simp only [BEq.comm, any_beq]
+theorem any_beq' [BEq α] [LawfulBEq α] {l : List α} : (l.any fun x => x == a) ↔ a ∈ l := by
+  simp
 
-theorem all_bne [BEq α] {l : List α} : (l.all fun x => a != x) = !l.contains a := by
-  induction l <;> simp_all [bne]
+theorem all_bne [BEq α] [LawfulBEq α] {l : List α} : (l.all fun x => a != x) ↔ a ∉ l := by
+  induction l <;> simp_all
 
-/-- Variant of `all_bne` with `!=` reversed. -/
-theorem all_bne' [BEq α] [PartialEquivBEq α] {l : List α} :
-    (l.all fun x => x != a) = !l.contains a := by
-  simp only [bne_comm, all_bne]
+theorem all_bne' [BEq α] [LawfulBEq α] {l : List α} : (l.all fun x => x != a) ↔ a ∉ l := by
+  induction l <;> simp_all [eq_comm (a := a)]
 
 /-! ### set -/
 
@@ -2855,6 +2828,11 @@ theorem leftpad_suffix (n : Nat) (a : α) (l : List α) : l <:+ (leftpad n a l)
 
 theorem elem_cons_self [BEq α] [LawfulBEq α] {a : α} : (a::as).elem a = true := by simp
 
+@[simp] theorem contains_cons [BEq α] :
+    (a :: as : List α).contains x = (x == a || as.contains x) := by
+  simp only [contains, elem]
+  split <;> simp_all
+
 theorem contains_eq_any_beq [BEq α] (l : List α) (a : α) : l.contains a = l.any (a == ·) := by
   induction l with simp | cons b l => cases b == a <;> simp [*]
 

src/Init/Data/List/ToArray.lean

@@ -363,12 +363,4 @@ theorem takeWhile_go_toArray (p : α → Bool) (l : List α) (i : Nat) :
     l.toArray.takeWhile p = (l.takeWhile p).toArray := by
   simp [Array.takeWhile, takeWhile_go_toArray]
 
-@[simp] theorem setIfInBounds_toArray (l : List α) (i : Nat) (a : α) :
-    l.toArray.setIfInBounds i a  = (l.set i a).toArray := by
-  apply ext'
-  simp only [setIfInBounds]
-  split
-  · simp
-  · simp_all [List.set_eq_of_length_le]
-
 end List

src/Init/Data/Nat/Lemmas.lean

@@ -1046,25 +1046,6 @@ instance decidableExistsLE [DecidablePred p] : DecidablePred fun n => ∃ m : Na
   fun n => decidable_of_iff (∃ m, m < n + 1 ∧ p m)
     (exists_congr fun _ => and_congr_left' Nat.lt_succ_iff)
 
-/-- Dependent version of `decidableExistsLT`. -/
-instance decidableExistsLT' {p : (m : Nat) → m < k → Prop} [I : ∀ m h, Decidable (p m h)] :
-    Decidable (∃ m : Nat, ∃ h : m < k, p m h) :=
-  match k, p, I with
-  | 0, _, _ => isFalse (by simp)
-  | (k + 1), p, I => @decidable_of_iff _ ((∃ m, ∃ h : m < k, p m (by omega)) ∨ p k (by omega))
-      ⟨by rintro (⟨m, h, w⟩ | w); exact ⟨m, by omega, w⟩; exact ⟨k, by omega, w⟩,
-        fun ⟨m, h, w⟩ => if h' : m < k then .inl ⟨m, h', w⟩ else
-          by obtain rfl := (by omega : m = k); exact .inr w⟩
-      (@instDecidableOr _ _
-        (decidableExistsLT' (p := fun m h => p m (by omega)) (I := fun m h => I m (by omega)))
-        inferInstance)
-
-/-- Dependent version of `decidableExistsLE`. -/
-instance decidableExistsLE' {p : (m : Nat) → m ≤ k → Prop} [I : ∀ m h, Decidable (p m h)] :
-    Decidable (∃ m : Nat, ∃ h : m ≤ k, p m h) :=
-  decidable_of_iff (∃ m, ∃ h : m < k + 1, p m (by omega)) (exists_congr fun _ =>
-    ⟨fun ⟨h, w⟩ => ⟨le_of_lt_succ h, w⟩, fun ⟨h, w⟩ => ⟨lt_add_one_of_le h, w⟩⟩)
-
 /-! ### Results about `List.sum` specialized to `Nat` -/
 
 protected theorem sum_pos_iff_exists_pos {l : List Nat} : 0 < l.sum ↔ ∃ x ∈ l, 0 < x := by

src/Init/PropLemmas.lean

@@ -386,15 +386,6 @@ theorem exists_comm {p : α → β → Prop} : (∃ a b, p a b) ↔ (∃ b a, p
 theorem forall_prop_of_false {p : Prop} {q : p → Prop} (hn : ¬p) : (∀ h' : p, q h') ↔ True :=
   iff_true_intro fun h => hn.elim h
 
-@[simp] theorem and_exists_self (P : Prop) (Q : P → Prop) : (P ∧ ∃ p, Q p) ↔ ∃ p, Q p :=
-  ⟨fun ⟨_, h⟩ => h, fun ⟨p, q⟩ => ⟨p, ⟨p, q⟩⟩⟩
-
-@[simp] theorem exists_and_self (P : Prop) (Q : P → Prop) : ((∃ p, Q p) ∧ P) ↔ ∃ p, Q p :=
-  ⟨fun ⟨h, _⟩ => h, fun ⟨p, q⟩ => ⟨⟨p, q⟩, p⟩⟩
-
-@[simp] theorem forall_self_imp (P : Prop) (Q : P → Prop) : (∀ p : P, P → Q p) ↔ ∀ p, Q p :=
-  ⟨fun h p => h p p, fun h _ p => h p⟩
-
 end quantifiers
 
 /-! ## membership -/

src/Lean/Compiler/IR/Basic.lean

@@ -81,7 +81,6 @@ then one of the following must hold in each (execution) branch.
 inductive IRType where
   | float | uint8 | uint16 | uint32 | uint64 | usize
   | irrelevant | object | tobject
-  | float32
   | struct (leanTypeName : Option Name) (types : Array IRType) : IRType
   | union (leanTypeName : Name) (types : Array IRType) : IRType
   deriving Inhabited, Repr
@@ -90,7 +89,6 @@ namespace IRType
 
 partial def beq : IRType → IRType → Bool
   | float,          float          => true
-  | float32,        float32        => true
   | uint8,          uint8          => true
   | uint16,         uint16         => true
   | uint32,         uint32         => true
@@ -106,14 +104,13 @@ partial def beq : IRType → IRType → Bool
 instance : BEq IRType := ⟨beq⟩
 
 def isScalar : IRType → Bool
-  | float    => true
-  | float32  => true
-  | uint8    => true
-  | uint16   => true
-  | uint32   => true
-  | uint64   => true
-  | usize    => true
-  | _        => false
+  | float  => true
+  | uint8  => true
+  | uint16 => true
+  | uint32 => true
+  | uint64 => true
+  | usize  => true
+  | _      => false
 
 def isObj : IRType → Bool
   | object  => true
@@ -614,11 +611,10 @@ def mkIf (x : VarId) (t e : FnBody) : FnBody :=
 
 def getUnboxOpName (t : IRType) : String :=
   match t with
-  | IRType.usize    => "lean_unbox_usize"
-  | IRType.uint32   => "lean_unbox_uint32"
-  | IRType.uint64   => "lean_unbox_uint64"
-  | IRType.float    => "lean_unbox_float"
-  | IRType.float32  => "lean_unbox_float32"
-  | _               => "lean_unbox"
+  | IRType.usize  => "lean_unbox_usize"
+  | IRType.uint32 => "lean_unbox_uint32"
+  | IRType.uint64 => "lean_unbox_uint64"
+  | IRType.float  => "lean_unbox_float"
+  | _             => "lean_unbox"
 
 end Lean.IR

src/Lean/Compiler/IR/EmitC.lean

@@ -55,7 +55,6 @@ def emitArg (x : Arg) : M Unit :=
 
 def toCType : IRType → String
   | IRType.float      => "double"
-  | IRType.float32    => "float"
   | IRType.uint8      => "uint8_t"
   | IRType.uint16     => "uint16_t"
   | IRType.uint32     => "uint32_t"
@@ -312,13 +311,12 @@ def emitUSet (x : VarId) (n : Nat) (y : VarId) : M Unit := do
 
 def emitSSet (x : VarId) (n : Nat) (offset : Nat) (y : VarId) (t : IRType) : M Unit := do
   match t with
-  | IRType.float   => emit "lean_ctor_set_float"
-  | IRType.float32 => emit "lean_ctor_set_float32"
-  | IRType.uint8   => emit "lean_ctor_set_uint8"
-  | IRType.uint16  => emit "lean_ctor_set_uint16"
-  | IRType.uint32  => emit "lean_ctor_set_uint32"
-  | IRType.uint64  => emit "lean_ctor_set_uint64"
-  | _              => throw "invalid instruction";
+  | IRType.float  => emit "lean_ctor_set_float"
+  | IRType.uint8  => emit "lean_ctor_set_uint8"
+  | IRType.uint16 => emit "lean_ctor_set_uint16"
+  | IRType.uint32 => emit "lean_ctor_set_uint32"
+  | IRType.uint64 => emit "lean_ctor_set_uint64"
+  | _             => throw "invalid instruction";
   emit "("; emit x; emit ", "; emitOffset n offset; emit ", "; emit y; emitLn ");"
 
 def emitJmp (j : JoinPointId) (xs : Array Arg) : M Unit := do
@@ -388,13 +386,12 @@ def emitUProj (z : VarId) (i : Nat) (x : VarId) : M Unit := do
 def emitSProj (z : VarId) (t : IRType) (n offset : Nat) (x : VarId) : M Unit := do
   emitLhs z;
   match t with
-  | IRType.float    => emit "lean_ctor_get_float"
-  | IRType.float32  => emit "lean_ctor_get_float32"
-  | IRType.uint8    => emit "lean_ctor_get_uint8"
-  | IRType.uint16   => emit "lean_ctor_get_uint16"
-  | IRType.uint32   => emit "lean_ctor_get_uint32"
-  | IRType.uint64   => emit "lean_ctor_get_uint64"
-  | _               => throw "invalid instruction"
+  | IRType.float  => emit "lean_ctor_get_float"
+  | IRType.uint8  => emit "lean_ctor_get_uint8"
+  | IRType.uint16 => emit "lean_ctor_get_uint16"
+  | IRType.uint32 => emit "lean_ctor_get_uint32"
+  | IRType.uint64 => emit "lean_ctor_get_uint64"
+  | _             => throw "invalid instruction"
   emit "("; emit x; emit ", "; emitOffset n offset; emitLn ");"
 
 def toStringArgs (ys : Array Arg) : List String :=
@@ -449,12 +446,11 @@ def emitApp (z : VarId) (f : VarId) (ys : Array Arg) : M Unit :=
 
 def emitBoxFn (xType : IRType) : M Unit :=
   match xType with
-  | IRType.usize   => emit "lean_box_usize"
-  | IRType.uint32  => emit "lean_box_uint32"
-  | IRType.uint64  => emit "lean_box_uint64"
-  | IRType.float   => emit "lean_box_float"
-  | IRType.float32 => emit "lean_box_float32"
-  | _              => emit "lean_box"
+  | IRType.usize  => emit "lean_box_usize"
+  | IRType.uint32 => emit "lean_box_uint32"
+  | IRType.uint64 => emit "lean_box_uint64"
+  | IRType.float  => emit "lean_box_float"
+  | _             => emit "lean_box"
 
 def emitBox (z : VarId) (x : VarId) (xType : IRType) : M Unit := do
   emitLhs z; emitBoxFn xType; emit "("; emit x; emitLn ");"

src/Lean/Compiler/IR/EmitLLVM.lean

@@ -315,7 +315,6 @@ def callLeanCtorSetTag (builder : LLVM.Builder llvmctx)
 def toLLVMType (t : IRType) : M llvmctx (LLVM.LLVMType llvmctx) := do
   match t with
   | IRType.float      => LLVM.doubleTypeInContext llvmctx
-  | IRType.float32    => LLVM.floatTypeInContext llvmctx
   | IRType.uint8      => LLVM.intTypeInContext llvmctx 8
   | IRType.uint16     => LLVM.intTypeInContext llvmctx 16
   | IRType.uint32     => LLVM.intTypeInContext llvmctx 32
@@ -818,13 +817,12 @@ def emitSProj (builder : LLVM.Builder llvmctx)
     (z : VarId) (t : IRType) (n offset : Nat) (x : VarId) : M llvmctx Unit := do
   let (fnName, retty) ←
     match t with
-    | IRType.float   => pure ("lean_ctor_get_float", ← LLVM.doubleTypeInContext llvmctx)
-    | IRType.float32 => pure ("lean_ctor_get_float32", ← LLVM.floatTypeInContext llvmctx)
-    | IRType.uint8   => pure ("lean_ctor_get_uint8", ← LLVM.i8Type llvmctx)
-    | IRType.uint16  => pure ("lean_ctor_get_uint16", ←  LLVM.i16Type llvmctx)
-    | IRType.uint32  => pure ("lean_ctor_get_uint32", ← LLVM.i32Type llvmctx)
-    | IRType.uint64  => pure ("lean_ctor_get_uint64", ← LLVM.i64Type llvmctx)
-    | _              => throw s!"Invalid type for lean_ctor_get: '{t}'"
+    | IRType.float  => pure ("lean_ctor_get_float", ← LLVM.doubleTypeInContext llvmctx)
+    | IRType.uint8  => pure ("lean_ctor_get_uint8", ← LLVM.i8Type llvmctx)
+    | IRType.uint16 => pure ("lean_ctor_get_uint16", ←  LLVM.i16Type llvmctx)
+    | IRType.uint32 => pure ("lean_ctor_get_uint32", ← LLVM.i32Type llvmctx)
+    | IRType.uint64 => pure ("lean_ctor_get_uint64", ← LLVM.i64Type llvmctx)
+    | _             => throw s!"Invalid type for lean_ctor_get: '{t}'"
   let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.unsignedType llvmctx]
   let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
   let xval ← emitLhsVal builder x
@@ -864,12 +862,11 @@ def emitBox (builder : LLVM.Builder llvmctx) (z : VarId) (x : VarId) (xType : IR
   let xv ← emitLhsVal builder x
   let (fnName, argTy, xv) ←
     match xType with
-    | IRType.usize   => pure ("lean_box_usize", ← LLVM.size_tType llvmctx, xv)
-    | IRType.uint32  => pure ("lean_box_uint32", ← LLVM.i32Type llvmctx, xv)
-    | IRType.uint64  => pure ("lean_box_uint64", ← LLVM.size_tType llvmctx, xv)
-    | IRType.float   => pure ("lean_box_float", ← LLVM.doubleTypeInContext llvmctx, xv)
-    | IRType.float32 => pure ("lean_box_float32", ← LLVM.floatTypeInContext llvmctx, xv)
-    | _              =>
+    | IRType.usize  => pure ("lean_box_usize", ← LLVM.size_tType llvmctx, xv)
+    | IRType.uint32 => pure ("lean_box_uint32", ← LLVM.i32Type llvmctx, xv)
+    | IRType.uint64 => pure ("lean_box_uint64", ← LLVM.size_tType llvmctx, xv)
+    | IRType.float  => pure ("lean_box_float", ← LLVM.doubleTypeInContext llvmctx, xv)
+    | _             => do
          -- sign extend smaller values into i64
          let xv ← LLVM.buildSext builder xv (← LLVM.size_tType llvmctx)
          pure ("lean_box", ← LLVM.size_tType llvmctx, xv)
@@ -895,12 +892,11 @@ def callUnboxForType (builder : LLVM.Builder llvmctx)
     (retName : String := "") : M llvmctx (LLVM.Value llvmctx) := do
   let (fnName, retty) ←
      match t with
-     | IRType.usize   => pure ("lean_unbox_usize", ← toLLVMType t)
-     | IRType.uint32  => pure ("lean_unbox_uint32", ← toLLVMType t)
-     | IRType.uint64  => pure ("lean_unbox_uint64", ← toLLVMType t)
-     | IRType.float   => pure ("lean_unbox_float", ← toLLVMType t)
-     | IRType.float32 => pure ("lean_unbox_float32", ← toLLVMType t)
-     | _              => pure ("lean_unbox", ← LLVM.size_tType llvmctx)
+     | IRType.usize  => pure ("lean_unbox_usize", ← toLLVMType t)
+     | IRType.uint32 => pure ("lean_unbox_uint32", ← toLLVMType t)
+     | IRType.uint64 => pure ("lean_unbox_uint64", ← toLLVMType t)
+     | IRType.float  => pure ("lean_unbox_float", ← toLLVMType t)
+     | _             => pure ("lean_unbox", ← LLVM.size_tType llvmctx)
   let argtys := #[← LLVM.voidPtrType llvmctx ]
   let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
   let fnty ← LLVM.functionType retty argtys
@@ -1045,13 +1041,12 @@ def emitJmp (builder : LLVM.Builder llvmctx) (jp : JoinPointId) (xs : Array Arg)
 def emitSSet (builder : LLVM.Builder llvmctx) (x : VarId) (n : Nat) (offset : Nat) (y : VarId) (t : IRType) : M llvmctx Unit := do
   let (fnName, setty) ←
   match t with
-  | IRType.float   => pure ("lean_ctor_set_float", ← LLVM.doubleTypeInContext llvmctx)
-  | IRType.float32 => pure ("lean_ctor_set_float32", ← LLVM.floatTypeInContext llvmctx)
-  | IRType.uint8   => pure ("lean_ctor_set_uint8", ← LLVM.i8Type llvmctx)
-  | IRType.uint16  => pure ("lean_ctor_set_uint16", ← LLVM.i16Type llvmctx)
-  | IRType.uint32  => pure ("lean_ctor_set_uint32", ← LLVM.i32Type llvmctx)
-  | IRType.uint64  => pure ("lean_ctor_set_uint64", ← LLVM.i64Type llvmctx)
-  | _              => throw s!"invalid type for 'lean_ctor_set': '{t}'"
+  | IRType.float  => pure ("lean_ctor_set_float", ← LLVM.doubleTypeInContext llvmctx)
+  | IRType.uint8  => pure ("lean_ctor_set_uint8", ← LLVM.i8Type llvmctx)
+  | IRType.uint16 => pure ("lean_ctor_set_uint16", ← LLVM.i16Type llvmctx)
+  | IRType.uint32 => pure ("lean_ctor_set_uint32", ← LLVM.i32Type llvmctx)
+  | IRType.uint64 => pure ("lean_ctor_set_uint64", ← LLVM.i64Type llvmctx)
+  | _             => throw s!"invalid type for 'lean_ctor_set': '{t}'"
   let argtys := #[ ← LLVM.voidPtrType llvmctx, ← LLVM.unsignedType llvmctx, setty]
   let retty  ← LLVM.voidType llvmctx
   let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys

src/Lean/Compiler/IR/Format.lean

@@ -55,7 +55,6 @@ instance : ToString Expr := ⟨fun e => Format.pretty (format e)⟩
 
 private partial def formatIRType : IRType → Format
   | IRType.float        => "float"
-  | IRType.float32      => "float32"
   | IRType.uint8        => "u8"
   | IRType.uint16       => "u16"
   | IRType.uint32       => "u32"

src/Lean/Elab/PreDefinition/Main.lean

@@ -22,8 +22,7 @@ private def addAndCompilePartial (preDefs : Array PreDefinition) (useSorry := fa
       let value ← if useSorry then
         mkLambdaFVars xs (← mkSorry type (synthetic := true))
       else
-        let msg := m!"failed to compile 'partial' definition '{preDef.declName}'"
-        liftM <| mkInhabitantFor msg xs type
+        liftM <| mkInhabitantFor preDef.declName xs type
       addNonRec { preDef with
         kind  := DefKind.«opaque»
         value

src/Lean/Elab/PreDefinition/MkInhabitant.lean

@@ -50,13 +50,13 @@ private partial def mkInhabitantForAux? (xs insts : Array Expr) (type : Expr) (u
       return none
 
 /- TODO: add a global IO.Ref to let users customize/extend this procedure -/
-def mkInhabitantFor (failedToMessage : MessageData) (xs : Array Expr) (type : Expr) : MetaM Expr :=
+def mkInhabitantFor (declName : Name) (xs : Array Expr) (type : Expr) : MetaM Expr :=
   withInhabitedInstances xs fun insts => do
     if let some val ← mkInhabitantForAux? xs insts type false <||> mkInhabitantForAux? xs insts type true then
       return val
     else
       throwError "\
-        {failedToMessage}, could not prove that the type\
+        failed to compile 'partial' definition '{declName}', could not prove that the type\
         {indentExpr (← mkForallFVars xs type)}\n\
         is nonempty.\n\
         \n\

src/Lean/Elab/PreDefinition/WF/Eqns.lean

@@ -20,7 +20,6 @@ structure EqnInfo extends EqnInfoCore where
   declNameNonRec  : Name
   fixedPrefixSize : Nat
   argsPacker      : ArgsPacker
-  hasInduct       : Bool
   deriving Inhabited
 
 private partial def deltaLHSUntilFix (mvarId : MVarId) : MetaM MVarId := mvarId.withContext do
@@ -102,7 +101,7 @@ def mkEqns (declName : Name) (info : EqnInfo) : MetaM (Array Name) :=
 builtin_initialize eqnInfoExt : MapDeclarationExtension EqnInfo ← mkMapDeclarationExtension
 
 def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fixedPrefixSize : Nat)
-    (argsPacker : ArgsPacker) (hasInduct : Bool) : MetaM Unit := do
+    (argsPacker : ArgsPacker) : MetaM Unit := do
   preDefs.forM fun preDef => ensureEqnReservedNamesAvailable preDef.declName
   /-
   See issue #2327.
@@ -115,7 +114,7 @@ def registerEqnsInfo (preDefs : Array PreDefinition) (declNameNonRec : Name) (fi
       modifyEnv fun env =>
         preDefs.foldl (init := env) fun env preDef =>
           eqnInfoExt.insert env preDef.declName { preDef with
-            declNames, declNameNonRec, fixedPrefixSize, argsPacker, hasInduct }
+            declNames, declNameNonRec, fixedPrefixSize, argsPacker }
 
 def getEqnsFor? (declName : Name) : MetaM (Option (Array Name)) := do
   if let some info := eqnInfoExt.find? (← getEnv) declName then

src/Lean/Elab/PreDefinition/WF/Fix.lean

@@ -178,8 +178,7 @@ def groupGoalsByFunction (argsPacker : ArgsPacker) (numFuncs : Nat) (goals : Arr
     let type ← goal.getType
     let (.mdata _ (.app _ param)) := type
         | throwError "MVar does not look like a recursive call:{indentExpr type}"
-    let some (funidx, _) := argsPacker.unpack param
-        | throwError "Cannot unpack param, unexpected expression:{indentExpr param}"
+    let (funidx, _) ← argsPacker.unpack param
     r := r.modify funidx (·.push goal)
   return r
 

src/Lean/Elab/PreDefinition/WF/GuessLex.lean

@@ -352,10 +352,8 @@ def collectRecCalls (unaryPreDef : PreDefinition) (fixedPrefixSize : Nat)
         throwError "Insufficient arguments in recursive call"
       let arg := args[fixedPrefixSize]!
       trace[Elab.definition.wf] "collectRecCalls: {unaryPreDef.declName} ({param}) → {unaryPreDef.declName} ({arg})"
-      let some (caller, params) := argsPacker.unpack param
-        | throwError "Cannot unpack param, unexpected expression:{indentExpr param}"
-      let some (callee, args) := argsPacker.unpack arg
-        | throwError "Cannot unpack arg, unexpected expression:{indentExpr arg}"
+      let (caller, params) ← argsPacker.unpack param
+      let (callee, args) ← argsPacker.unpack arg
       RecCallWithContext.create (← getRef) caller (ys ++ params) callee (ys ++ args)
 
 /-- Is the expression a `<`-like comparison of `Nat` expressions -/
@@ -773,8 +771,6 @@ Main entry point of this module:
 
 Try to find a lexicographic ordering of the arguments for which the recursive definition
 terminates. See the module doc string for a high-level overview.
-
-The `preDefs` are used to determine arity and types of arguments; the bodies are ignored.
 -/
 def guessLex (preDefs : Array PreDefinition) (unaryPreDef : PreDefinition)
     (fixedPrefixSize : Nat) (argsPacker : ArgsPacker) :

src/Lean/Elab/PreDefinition/WF/Main.lean

@@ -110,7 +110,7 @@ def wfRecursion (preDefs : Array PreDefinition) (termArg?s : Array (Option Termi
     unless type.isForall do
       throwError "wfRecursion: expected unary function type: {type}"
     let packedArgType := type.bindingDomain!
-    elabWFRel (preDefs.map (·.declName)) unaryPreDef.declName prefixArgs argsPacker packedArgType wf fun wfRel => do
+    elabWFRel preDefs unaryPreDef.declName prefixArgs argsPacker packedArgType wf fun wfRel => do
       trace[Elab.definition.wf] "wfRel: {wfRel}"
       let (value, envNew) ← withoutModifyingEnv' do
         addAsAxiom unaryPreDef
@@ -142,7 +142,7 @@ def wfRecursion (preDefs : Array PreDefinition) (termArg?s : Array (Option Termi
   -- Reason: the nested proofs may be referring to the _unsafe_rec.
   addAndCompilePartialRec preDefs
   let preDefs ← preDefs.mapM (abstractNestedProofs ·)
-  registerEqnsInfo preDefs preDefNonRec.declName fixedPrefixSize argsPacker (hasInduct := true)
+  registerEqnsInfo preDefs preDefNonRec.declName fixedPrefixSize argsPacker
   for preDef in preDefs do
     markAsRecursive preDef.declName
     generateEagerEqns preDef.declName

src/Lean/Elab/PreDefinition/WF/Rel.lean

@@ -51,12 +51,12 @@ If the `termArgs` map the packed argument `argType` to `β`, then this function
 continuation a value of type `WellFoundedRelation argType` that is derived from the instance
 for `WellFoundedRelation β` using `invImage`.
 -/
-def elabWFRel (declNames : Array Name) (unaryPreDefName : Name) (prefixArgs : Array Expr)
+def elabWFRel (preDefs : Array PreDefinition) (unaryPreDefName : Name) (prefixArgs : Array Expr)
     (argsPacker : ArgsPacker) (argType : Expr) (termArgs : TerminationArguments)
     (k : Expr → TermElabM α) : TermElabM α := withDeclName unaryPreDefName do
   let α := argType
   let u ← getLevel α
-  let β ← checkCodomains declNames prefixArgs argsPacker.arities termArgs
+  let β ← checkCodomains (preDefs.map (·.declName)) prefixArgs argsPacker.arities termArgs
   let v ← getLevel β
   let packedF ← argsPacker.uncurryND (termArgs.map (·.fn.beta prefixArgs))
   let inst ← synthInstance (.app (.const ``WellFoundedRelation [v]) β)

src/Lean/Expr.lean

@@ -1235,9 +1235,6 @@ def getRevArg!' : Expr → Nat → Expr
 @[inline] def getArgD (e : Expr) (i : Nat) (v₀ : Expr) (n := e.getAppNumArgs) : Expr :=
   getRevArgD e (n - i - 1) v₀
 
-/-- Return `true` if `e` contains any loose bound variables.
-
-This is a constant time operation. -/
 def hasLooseBVars (e : Expr) : Bool :=
   e.looseBVarRange > 0
 
@@ -1250,11 +1247,6 @@ def isArrow (e : Expr) : Bool :=
   | forallE _ _ b _ => !b.hasLooseBVars
   | _ => false
 
-/--
-Return `true` if `e` contains the specified loose bound variable with index `bvarIdx`.
-
-This operation traverses the expression tree.
--/
 @[extern "lean_expr_has_loose_bvar"]
 opaque hasLooseBVar (e : @& Expr) (bvarIdx : @& Nat) : Bool
 

src/Lean/Meta/ArgsPacker.lean

@@ -87,7 +87,7 @@ Unpacks a unary packed argument created with `Unary.pack`.
 
 Throws an error if the expression is not of that form.
 -/
-def unpack (arity : Nat) (e : Expr) : Option (Array Expr) := do
+def unpack (arity : Nat) (e : Expr) : MetaM (Array Expr) := do
   let mut e := e
   let mut args := #[]
   while args.size + 1 < arity do
@@ -95,10 +95,11 @@ def unpack (arity : Nat) (e : Expr) : Option (Array Expr) := do
       args := args.push (e.getArg! 2)
       e := e.getArg! 3
     else
-      none
+      throwError "Unexpected expression while unpacking n-ary argument"
   args := args.push e
   return args
 
+
 /--
   Given a (dependent) tuple `t` (using `PSigma`) of the given arity.
   Return an array containing its "elements".
@@ -257,7 +258,7 @@ argument and function index.
 
 Throws an error if the expression is not of that form.
 -/
-def unpack (numFuncs : Nat) (expr : Expr) : Option (Nat × Expr) := do
+def unpack (numFuncs : Nat) (expr : Expr) : MetaM (Nat × Expr) := do
   let mut funidx := 0
   let mut e := expr
   while funidx + 1 < numFuncs do
@@ -268,7 +269,7 @@ def unpack (numFuncs : Nat) (expr : Expr) : Option (Nat × Expr) := do
       e := e.getArg! 2
       break
     else
-      none
+      throwError "Unexpected expression while unpacking mutual argument:{indentExpr expr}"
   return (funidx, e)
 
 
@@ -376,17 +377,14 @@ and `(z : C) → R₂[z]`, returns an expression of type
 (x : A ⊕' C) → (match x with | .inl x => R₁[x] | .inr R₂[z])
 ```
 -/
-def uncurryWithType (resultType : Expr) (es : Array Expr) : MetaM Expr := do
+def uncurry (es : Array Expr) : MetaM Expr := do
+  let types ← es.mapM inferType
+  let resultType ← uncurryType types
   forallBoundedTelescope resultType (some 1) fun xs codomain => do
     let #[x] := xs | unreachable!
     let value ← casesOn x codomain es.toList
     mkLambdaFVars #[x] value
 
-def uncurry (es : Array Expr) : MetaM Expr := do
-  let types ← es.mapM inferType
-  let resultType ← uncurryType types
-  uncurryWithType resultType es
-
 /--
 Given unary expressions `e₁`, `e₂` with types `(x : A) → R`
 and `(z : C) → R`, returns an expression of type
@@ -416,7 +414,7 @@ def curryType (n : Nat) (type : Expr) : MetaM (Array Expr) := do
 
 end Mutual
 
--- Now for the main definitions in this module
+-- Now for the main definitions in this moduleo
 
 /-- The number of functions being packed -/
 def numFuncs (argsPacker : ArgsPacker) : Nat := argsPacker.varNamess.size
@@ -424,10 +422,6 @@ def numFuncs (argsPacker : ArgsPacker) : Nat := argsPacker.varNamess.size
 /-- The arities of the functions being packed -/
 def arities (argsPacker : ArgsPacker) : Array Nat := argsPacker.varNamess.map (·.size)
 
-def onlyOneUnary (argsPacker : ArgsPacker) :=
-  argsPacker.varNamess.size = 1 &&
-  argsPacker.varNamess[0]!.size = 1
-
 def pack (argsPacker : ArgsPacker) (domain : Expr) (fidx : Nat) (args : Array Expr)
     : MetaM Expr := do
   assert! fidx < argsPacker.numFuncs
@@ -442,13 +436,14 @@ return the function index that is called and the arguments individually.
 
 We expect precisely the expressions produced by `pack`, with manifest
 `PSum.inr`, `PSum.inl` and `PSigma.mk` constructors, and thus take them apart
-rather than using projections.
+rather than using projectinos.
 -/
-def unpack (argsPacker : ArgsPacker) (e : Expr) : Option (Nat × Array Expr) := do
+def unpack (argsPacker : ArgsPacker) (e : Expr) : MetaM (Nat × Array Expr) := do
   let (funidx, e) ← Mutual.unpack argsPacker.numFuncs e
   let args ← Unary.unpack argsPacker.varNamess[funidx]!.size e
   return (funidx, args)
 
+
 /--
 Given types `(x : A) → (y : B[x]) → R₁[x,y]` and `(z : C) → R₂[z]`, returns the type uncurried type
 ```
@@ -470,10 +465,6 @@ def uncurry (argsPacker : ArgsPacker) (es : Array Expr) : MetaM Expr := do
   let unary ← (Array.zipWith argsPacker.varNamess es Unary.uncurry).mapM id
   Mutual.uncurry unary
 
-def uncurryWithType (argsPacker : ArgsPacker) (resultType : Expr) (es : Array Expr) : MetaM Expr := do
-  let unary ← (Array.zipWith argsPacker.varNamess es Unary.uncurry).mapM id
-  Mutual.uncurryWithType resultType unary
-
 /--
 Given expressions `e₁`, `e₂` with types `(x : A) → (y : B[x]) → R`
 and `(z : C) → R`, returns an expression of type

src/Lean/Meta/Tactic/FunInd.lean

@@ -810,8 +810,7 @@ def cleanPackedArgs (eqnInfo : WF.EqnInfo) (value : Expr) : MetaM Expr := do
       let args := e.getAppArgs
       if eqnInfo.fixedPrefixSize + 1 ≤ args.size then
         let packedArg := args.back!
-          let some (i, unpackedArgs) := eqnInfo.argsPacker.unpack packedArg
-            | throwError "Unexpected packedArg:{indentExpr packedArg}"
+          let (i, unpackedArgs) ← eqnInfo.argsPacker.unpack packedArg
           let e' := .const eqnInfo.declNames[i]! e.getAppFn.constLevels!
           let e' := mkAppN e' args.pop
           let e' := mkAppN e' unpackedArgs
@@ -1111,16 +1110,11 @@ def isFunInductName (env : Environment) (name : Name) : Bool := Id.run do
   let .str p s := name | return false
   match s with
   | "induct" =>
-    if let some eqnInfo := WF.eqnInfoExt.find? env p then
-      unless eqnInfo.hasInduct do
-        return false
-      return true
+    if (WF.eqnInfoExt.find? env p).isSome then return true
     if (Structural.eqnInfoExt.find? env p).isSome then return true
     return false
   | "mutual_induct" =>
     if let some eqnInfo := WF.eqnInfoExt.find? env p then
-      unless eqnInfo.hasInduct do
-        return false
       if h : eqnInfo.declNames.size > 1 then
         return eqnInfo.declNames[0] = p
     if let some eqnInfo := Structural.eqnInfoExt.find? env p then

src/Lean/ResolveName.lean

@@ -398,22 +398,16 @@ Aliases are considered first.
 
 When `fullNames` is true, returns either `n₀` or `_root_.n₀`.
 
-When `allowHorizAliases` is false, then "horizontal aliases" (ones that are not put into a parent namespace) are filtered out.
-The assumption is that non-horizontal aliases are "API exports" (i.e., intentional exports that should be considered to be the new canonical name).
-"Non-API exports" arise from (1) using `export` to add names to a namespace for dot notation or (2) projects that want names to be conveniently and permanently accessible in their own namespaces.
-
 This function is meant to be used for pretty printing.
 If `n₀` is an accessible name, then the result will be an accessible name.
 -/
-def unresolveNameGlobal [Monad m] [MonadResolveName m] [MonadEnv m] (n₀ : Name) (fullNames := false) (allowHorizAliases := false) : m Name := do
+def unresolveNameGlobal [Monad m] [MonadResolveName m] [MonadEnv m] (n₀ : Name) (fullNames := false) : m Name := do
   if n₀.hasMacroScopes then return n₀
   if fullNames then
     match (← resolveGlobalName n₀) with
       | [(potentialMatch, _)] => if (privateToUserName? potentialMatch).getD potentialMatch == n₀ then return n₀ else return rootNamespace ++ n₀
       | _ => return n₀ -- if can't resolve, return the original
   let mut initialNames := (getRevAliases (← getEnv) n₀).toArray
-  unless allowHorizAliases do
-    initialNames := initialNames.filter fun n => n.getPrefix.isPrefixOf n₀.getPrefix
   initialNames := initialNames.push (rootNamespace ++ n₀)
   for initialName in initialNames do
     if let some n ← unresolveNameCore initialName then

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean

@@ -77,8 +77,12 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) :
     simp only [go, denote_blastAppend, RefVec.get_cast, Ref.cast_eq, eval_append,
       BitVec.getLsbD_append]
     split
-    · next hsplit => rw [rih]
-    · next hsplit => rw [go_denote_mem_prefix, lih]
+    · next hsplit =>
+      simp only [hsplit, decide_true, cond_true]
+      rw [rih]
+    · next hsplit =>
+      simp only [hsplit, decide_false, cond_false]
+      rw [go_denote_mem_prefix, lih]
   | replicate n expr ih => simp [go, ih, hidx]
   | signExtend v inner ih =>
     rename_i originalWidth
@@ -91,7 +95,7 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) :
       rw [blastSignExtend_empty_eq_zeroExtend] at hgo
       · rw [← hgo]
         simp only [eval_signExtend]
-        rw [BitVec.signExtend_eq_setWidth_of_msb_false]
+        rw [BitVec.signExtend_eq_not_setWidth_not_of_msb_false]
         · simp only [denote_blastZeroExtend, ih, dite_eq_ite, Bool.if_false_right,
             BitVec.getLsbD_setWidth, hidx, decide_true, Bool.true_and, Bool.and_iff_right_iff_imp,
             decide_eq_true_eq]

src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Operations/Eq.lean

@@ -30,9 +30,9 @@ theorem mkEq_denote_eq (aig : AIG α) (pair : AIG.BinaryRefVec aig w) (assign :
   simp only [RefVec.denote_fold_and, RefVec.denote_zip, denote_mkBEqCached, beq_iff_eq]
   constructor
   · intro h
-    ext i h'
+    ext
     rw [← hleft, ← hright]
-    · simp [h, h']
+    · simp [h]
     · omega
     · omega
   · intro h idx hidx

src/Std/Tactic/BVDecide/Normalize/BitVec.lean

@@ -168,13 +168,13 @@ attribute [bv_normalize] BitVec.and_self
 
 @[bv_normalize]
 theorem BitVec.and_contra (a : BitVec w) : a &&& ~~~a = 0#w := by
-  ext i h
-  simp [h]
+  ext
+  simp
 
 @[bv_normalize]
 theorem BitVec.and_contra' (a : BitVec w) : ~~~a &&& a = 0#w := by
-  ext i h
-  simp [h]
+  ext
+  simp
 
 @[bv_normalize]
 theorem BitVec.add_not (a : BitVec w) : a + ~~~a = (-1#w) := by

src/include/lean/lean.h

@@ -614,11 +614,6 @@ static inline double lean_ctor_get_float(b_lean_obj_arg o, unsigned offset) {
     return *((double*)((uint8_t*)(lean_ctor_obj_cptr(o)) + offset));
 }
 
-static inline float lean_ctor_get_float32(b_lean_obj_arg o, unsigned offset) {
-    assert(offset >= lean_ctor_num_objs(o) * sizeof(void*));
-    return *((float*)((uint8_t*)(lean_ctor_obj_cptr(o)) + offset));
-}
-
 static inline void lean_ctor_set_usize(b_lean_obj_arg o, unsigned i, size_t v) {
     assert(i >= lean_ctor_num_objs(o));
     *((size_t*)(lean_ctor_obj_cptr(o) + i)) = v;
@@ -649,11 +644,6 @@ static inline void lean_ctor_set_float(b_lean_obj_arg o, unsigned offset, double
     *((double*)((uint8_t*)(lean_ctor_obj_cptr(o)) + offset)) = v;
 }
 
-static inline void lean_ctor_set_float32(b_lean_obj_arg o, unsigned offset, float v) {
-    assert(offset >= lean_ctor_num_objs(o) * sizeof(void*));
-    *((float*)((uint8_t*)(lean_ctor_obj_cptr(o)) + offset)) = v;
-}
-
 /* Closures */
 
 static inline void * lean_closure_fun(lean_object * o) { return lean_to_closure(o)->m_fun; }
@@ -2571,15 +2561,6 @@ LEAN_EXPORT uint8_t lean_float_isfinite(double a);
 LEAN_EXPORT uint8_t lean_float_isinf(double a);
 LEAN_EXPORT lean_obj_res lean_float_frexp(double a);
 
-/* Float32 */
-
-LEAN_EXPORT lean_obj_res lean_float32_to_string(float a);
-LEAN_EXPORT float lean_float32_scaleb(float a, b_lean_obj_arg b);
-LEAN_EXPORT uint8_t lean_float32_isnan(float a);
-LEAN_EXPORT uint8_t lean_float32_isfinite(float a);
-LEAN_EXPORT uint8_t lean_float32_isinf(float a);
-LEAN_EXPORT lean_obj_res lean_float32_frexp(float a);
-
 /* Boxing primitives */
 
 static inline lean_obj_res lean_box_uint32(uint32_t v) {
@@ -2634,16 +2615,6 @@ static inline double lean_unbox_float(b_lean_obj_arg o) {
     return lean_ctor_get_float(o, 0);
 }
 
-static inline lean_obj_res lean_box_float32(float v) {
-    lean_obj_res r = lean_alloc_ctor(0, 0, sizeof(float)); // NOLINT
-    lean_ctor_set_float32(r, 0, v);
-    return r;
-}
-
-static inline float lean_unbox_float32(b_lean_obj_arg o) {
-    return lean_ctor_get_float32(o, 0);
-}
-
 /* Debugging helper functions */
 
 LEAN_EXPORT lean_object * lean_dbg_trace(lean_obj_arg s, lean_obj_arg fn);
@@ -2758,40 +2729,6 @@ static inline uint8_t lean_float_decLe(double a, double b) { return a <= b; }
 static inline uint8_t lean_float_decLt(double a, double b) { return a < b; }
 static inline double lean_uint64_to_float(uint64_t a) { return (double) a; }
 
-/* float32 primitives */
-static inline uint8_t lean_float32_to_uint8(float a) {
-    return 0. <= a ? (a < 256. ? (uint8_t)a : UINT8_MAX) : 0;
-}
-static inline uint16_t lean_float32_to_uint16(float a) {
-    return 0. <= a ? (a < 65536. ? (uint16_t)a : UINT16_MAX) : 0;
-}
-static inline uint32_t lean_float32_to_uint32(float a) {
-    return 0. <= a ? (a < 4294967296. ? (uint32_t)a : UINT32_MAX) : 0;
-}
-static inline uint64_t lean_float32_to_uint64(float a) {
-    return 0. <= a ? (a < 18446744073709551616. ? (uint64_t)a : UINT64_MAX) : 0;
-}
-static inline size_t lean_float32_to_usize(float a) {
-    if (sizeof(size_t) == sizeof(uint64_t)) // NOLINT
-        return (size_t) lean_float32_to_uint64(a); // NOLINT
-    else
-        return (size_t) lean_float32_to_uint32(a); // NOLINT
-}
-LEAN_EXPORT float lean_float32_of_bits(uint32_t u);
-LEAN_EXPORT uint32_t lean_float32_to_bits(float d);
-static inline float lean_float32_add(float a, float b) { return a + b; }
-static inline float lean_float32_sub(float a, float b) { return a - b; }
-static inline float lean_float32_mul(float a, float b) { return a * b; }
-static inline float lean_float32_div(float a, float b) { return a / b; }
-static inline float lean_float32_negate(float a) { return -a; }
-static inline uint8_t lean_float32_beq(float a, float b) { return a == b; }
-static inline uint8_t lean_float32_decLe(float a, float b) { return a <= b; }
-static inline uint8_t lean_float32_decLt(float a, float b) { return a < b; }
-static inline float lean_uint64_to_float32(uint64_t a) { return (float) a; }
-
-static inline float lean_float_to_float32(double a) { return (float)a; }
-static inline double lean_float32_to_float(float a) { return (double)a; }
-
 /* Efficient C implementations of defns used by the compiler */
 static inline size_t lean_hashmap_mk_idx(lean_obj_arg sz, uint64_t hash) {
     return (size_t)(hash & (lean_unbox(sz) - 1));

src/library/compiler/ir.cpp

@@ -123,8 +123,6 @@ static ir::type to_ir_type(expr const & e) {
             return ir::type::USize;
         } else if (const_name(e) == get_float_name()) {
             return ir::type::Float;
-        } else if (const_name(e) == get_float32_name()) {
-            return ir::type::Float32;
         }
      } else if (is_pi(e)) {
         return ir::type::Object;
@@ -352,16 +350,6 @@ class to_ir_fn {
         return ir::mk_sset(to_var_id(args[0]), n, offset, to_var_id(args[1]), ir::type::Float, b);
     }
 
-    ir::fn_body visit_f32set(local_decl const & decl, ir::fn_body const & b) {
-        expr val = *decl.get_value();
-        buffer<expr> args;
-        expr const & fn = get_app_args(val, args);
-        lean_assert(args.size() == 2);
-        unsigned n, offset;
-        lean_verify(is_llnf_f32set(fn, n, offset));
-        return ir::mk_sset(to_var_id(args[0]), n, offset, to_var_id(args[1]), ir::type::Float32, b);
-    }
-
     ir::fn_body visit_uset(local_decl const & decl, ir::fn_body const & b) {
         expr val = *decl.get_value();
         buffer<expr> args;
@@ -429,8 +417,6 @@ class to_ir_fn {
                 return visit_sset(decl, b);
             else if (is_llnf_fset(fn))
                 return visit_fset(decl, b);
-            else if (is_llnf_f32set(fn))
-                return visit_f32set(decl, b);
             else if (is_llnf_uset(fn))
                 return visit_uset(decl, b);
             else if (is_llnf_proj(fn))
@@ -463,7 +449,7 @@ class to_ir_fn {
                 expr new_fvar   = m_lctx.mk_local_decl(ngen(), n, type, val);
                 fvars.push_back(new_fvar);
                 expr const & op = get_app_fn(val);
-                if (is_llnf_sset(op) || is_llnf_fset(op) || is_llnf_f32set(op) || is_llnf_uset(op)) {
+                if (is_llnf_sset(op) || is_llnf_fset(op) || is_llnf_uset(op)) {
                     /* In the Lean IR, sset and uset are instructions that perform destructive updates. */
                     subst.push_back(app_arg(app_fn(val)));
                 } else {

src/library/compiler/ir.h

@@ -14,13 +14,12 @@ namespace ir {
 inductive IRType
 | float | uint8 | uint16 | uint32 | uint64 | usize
 | irrelevant | object | tobject
-| float32
 | struct (leanTypeName : Option Name) (types : Array IRType) : IRType
 | union (leanTypeName : Name) (types : Array IRType) : IRType
 
 Remark: we don't create struct/union types from C++.
 */
-enum class type { Float, UInt8, UInt16, UInt32, UInt64, USize, Irrelevant, Object, TObject, Float32, Struct, Union };
+enum class type { Float, UInt8, UInt16, UInt32, UInt64, USize, Irrelevant, Object, TObject };
 
 typedef nat        var_id;
 typedef nat        jp_id;

src/library/compiler/ir_interpreter.cpp

@@ -188,11 +188,6 @@ option_ref<decl> find_ir_decl(environment const & env, name const & n) {
 
 extern "C" double lean_float_of_nat(lean_obj_arg a);
 
-// TODO: define in Lean like `lean_float_of_nat`
-float lean_float32_of_nat(lean_obj_arg a) {
-    return lean_float_of_nat(a);
-}
-
 static string_ref * g_mangle_prefix = nullptr;
 static string_ref * g_boxed_suffix = nullptr;
 static string_ref * g_boxed_mangled_suffix = nullptr;
@@ -232,7 +227,6 @@ union value {
     uint64   m_num; // big enough for any unboxed integral type
     static_assert(sizeof(size_t) <= sizeof(uint64), "uint64 should be the largest unboxed type"); // NOLINT
     double   m_float;
-    float    m_float32;
     object * m_obj;
 
     value() {}
@@ -246,50 +240,36 @@ union value {
         v.m_float = f;
         return v;
     }
-
-    static value from_float32(float f) {
-        value v;
-        v.m_float32 = f;
-        return v;
-    }
 };
 
 object * box_t(value v, type t) {
     switch (t) {
-    case type::Float:   return box_float(v.m_float);
-    case type::Float32: return box_float(v.m_float32);
-    case type::UInt8:   return box(v.m_num);
-    case type::UInt16:  return box(v.m_num);
-    case type::UInt32:  return box_uint32(v.m_num);
-    case type::UInt64:  return box_uint64(v.m_num);
-    case type::USize:   return box_size_t(v.m_num);
-    case type::Object:
-    case type::TObject:
-    case type::Irrelevant:
-        return v.m_obj;
-    case type::Struct:
-    case type::Union:
-        throw exception("not implemented yet");
+        case type::Float: return box_float(v.m_float);
+        case type::UInt8: return box(v.m_num);
+        case type::UInt16: return box(v.m_num);
+        case type::UInt32: return box_uint32(v.m_num);
+        case type::UInt64: return box_uint64(v.m_num);
+        case type::USize: return box_size_t(v.m_num);
+        case type::Object:
+        case type::TObject:
+        case type::Irrelevant:
+            return v.m_obj;
     }
     lean_unreachable();
 }
 
 value unbox_t(object * o, type t) {
     switch (t) {
-    case type::Float:   return value::from_float(unbox_float(o));
-    case type::Float32: return value::from_float32(unbox_float32(o));
-    case type::UInt8:   return unbox(o);
-    case type::UInt16:  return unbox(o);
-    case type::UInt32:  return unbox_uint32(o);
-    case type::UInt64:  return unbox_uint64(o);
-    case type::USize:   return unbox_size_t(o);
-    case type::Irrelevant:
-    case type::Object:
-    case type::TObject:
-        break;
-    case type::Struct:
-    case type::Union:
-        throw exception("not implemented yet");
+        case type::Float: return value::from_float(unbox_float(o));
+        case type::UInt8: return unbox(o);
+        case type::UInt16: return unbox(o);
+        case type::UInt32: return unbox_uint32(o);
+        case type::UInt64: return unbox_uint64(o);
+        case type::USize: return unbox_size_t(o);
+        case type::Irrelevant:
+        case type::Object:
+        case type::TObject:
+            break;
     }
     lean_unreachable();
 }
@@ -298,8 +278,6 @@ value unbox_t(object * o, type t) {
 void print_value(tout & ios, value const & v, type t) {
     if (t == type::Float) {
         ios << v.m_float;
-    } else if (t == type::Float32) {
-        ios << v.m_float32;
     } else if (type_is_scalar(t)) {
         ios << v.m_num;
     } else {
@@ -494,7 +472,6 @@ private:
                 object * o = var(expr_sproj_obj(e)).m_obj;
                 switch (t) {
                     case type::Float: return value::from_float(cnstr_get_float(o, offset));
-                    case type::Float32: return value::from_float32(cnstr_get_float32(o, offset));
                     case type::UInt8: return cnstr_get_uint8(o, offset);
                     case type::UInt16: return cnstr_get_uint16(o, offset);
                     case type::UInt32: return cnstr_get_uint32(o, offset);
@@ -503,8 +480,6 @@ private:
                     case type::Irrelevant:
                     case type::Object:
                     case type::TObject:
-                    case type::Struct:
-                    case type::Union:
                         break;
                 }
                 throw exception("invalid instruction");
@@ -555,9 +530,6 @@ private:
                             case type::Float:
                                 lean_inc(n.raw());
                                 return value::from_float(lean_float_of_nat(n.raw()));
-                            case type::Float32:
-                                lean_inc(n.raw());
-                                return value::from_float32(lean_float32_of_nat(n.raw()));
                             case type::UInt8:
                             case type::UInt16:
                             case type::UInt32:
@@ -571,9 +543,6 @@ private:
                                 return n.to_obj_arg();
                             case type::Irrelevant:
                                 break;
-                            case type::Union:
-                            case type::Struct:
-                                break;
                         }
                         throw exception("invalid instruction");
                     }
@@ -685,7 +654,6 @@ private:
                     lean_assert(is_exclusive(o));
                     switch (fn_body_sset_type(b)) {
                         case type::Float: cnstr_set_float(o, offset, v.m_float); break;
-                        case type::Float32: cnstr_set_float32(o, offset, v.m_float32); break;
                         case type::UInt8: cnstr_set_uint8(o, offset, v.m_num); break;
                         case type::UInt16: cnstr_set_uint16(o, offset, v.m_num); break;
                         case type::UInt32: cnstr_set_uint32(o, offset, v.m_num); break;
@@ -694,8 +662,6 @@ private:
                         case type::Irrelevant:
                         case type::Object:
                         case type::TObject:
-                        case type::Struct:
-                        case type::Union:
                             throw exception(sstream() << "invalid instruction");
                     }
                     b = fn_body_sset_cont(b);
@@ -841,7 +807,6 @@ private:
             // constants do not have boxed wrappers, but we'll survive
             switch (t) {
                 case type::Float: return value::from_float(*static_cast<double *>(e.m_addr));
-                case type::Float32: return value::from_float32(*static_cast<float *>(e.m_addr));
                 case type::UInt8: return *static_cast<uint8 *>(e.m_addr);
                 case type::UInt16: return *static_cast<uint16 *>(e.m_addr);
                 case type::UInt32: return *static_cast<uint32 *>(e.m_addr);
@@ -851,9 +816,6 @@ private:
                 case type::TObject:
                 case type::Irrelevant:
                     return *static_cast<object **>(e.m_addr);
-                case type::Struct:
-                case type::Union:
-                    throw exception("not implemented yet");
             }
         }
 

src/library/compiler/llnf.cpp

@@ -34,7 +34,6 @@ static char const * g_cnstr = "_cnstr";
 static name * g_reuse       = nullptr;
 static name * g_reset       = nullptr;
 static name * g_fset        = nullptr;
-static name * g_f32set      = nullptr;
 static name * g_sset        = nullptr;
 static name * g_uset        = nullptr;
 static name * g_proj        = nullptr;
@@ -163,9 +162,6 @@ bool is_llnf_sset(expr const & e, unsigned & sz, unsigned & n, unsigned & offset
 expr mk_llnf_fset(unsigned n, unsigned offset) { return mk_constant(name(name(*g_fset, n), offset)); }
 bool is_llnf_fset(expr const & e, unsigned & n, unsigned & offset) { return is_llnf_binary_primitive(e, *g_fset, n, offset); }
 
-expr mk_llnf_f32set(unsigned n, unsigned offset) { return mk_constant(name(name(*g_f32set, n), offset)); }
-bool is_llnf_f32set(expr const & e, unsigned & n, unsigned & offset) { return is_llnf_binary_primitive(e, *g_f32set, n, offset); }
-
 /* The `_uset.<n>` instruction sets a `usize` value in a constructor object at offset `sizeof(void*)*n`. */
 expr mk_llnf_uset(unsigned n) { return mk_constant(name(*g_uset, n)); }
 bool is_llnf_uset(expr const & e, unsigned & n) { return is_llnf_unary_primitive(e, *g_uset, n); }
@@ -222,7 +218,6 @@ bool is_llnf_op(expr const & e) {
         is_llnf_reset(e)   ||
         is_llnf_sset(e)    ||
         is_llnf_fset(e)    ||
-        is_llnf_f32set(e)  ||
         is_llnf_uset(e)    ||
         is_llnf_proj(e)    ||
         is_llnf_sproj(e)   ||
@@ -525,10 +520,6 @@ class to_lambda_pure_fn {
         return mk_app(mk_llnf_fset(num, offset), major, v);
     }
 
-    expr mk_f32set(expr const & major, unsigned num, unsigned offset, expr const & v) {
-        return mk_app(mk_llnf_f32set(num, offset), major, v);
-    }
-
     expr mk_uset(expr const & major, unsigned idx, expr const & v) {
         return mk_app(mk_llnf_uset(idx), major, v);
     }
@@ -595,7 +586,7 @@ class to_lambda_pure_fn {
                         fields.push_back(mk_let_decl(info.get_type(), mk_uproj(major, info.m_idx)));
                         break;
                     case field_info::Scalar:
-                        if (info.is_float() || info.is_float32()) {
+                        if (info.is_float()) {
                             fields.push_back(mk_let_decl(info.get_type(), mk_fproj(major, info.m_idx, info.m_offset)));
                         } else {
                             fields.push_back(mk_let_decl(info.get_type(), mk_sproj(major, info.m_size, info.m_idx, info.m_offset)));
@@ -695,8 +686,6 @@ class to_lambda_pure_fn {
                 }
                 if (info.is_float()) {
                     r = mk_let_decl(mk_enf_object_type(), mk_fset(r, info.m_idx, info.m_offset, args[j]));
-                } else if (info.is_float32()) {
-                    r = mk_let_decl(mk_enf_object_type(), mk_f32set(r, info.m_idx, info.m_offset, args[j]));
                 } else {
                     r = mk_let_decl(mk_enf_object_type(), mk_sset(r, info.m_size, info.m_idx, info.m_offset, args[j]));
                 }
@@ -742,7 +731,7 @@ class to_lambda_pure_fn {
                 break;
             case field_info::Scalar:
                 if (proj_idx(e) == i) {
-                    if (info.is_float() || info.is_float32()) {
+                    if (info.is_float()) {
                         return mk_fproj(visit(proj_expr(e)), info.m_idx, info.m_offset);
                     } else {
                         return mk_sproj(visit(proj_expr(e)), info.m_size, info.m_idx, info.m_offset);
@@ -845,8 +834,6 @@ void initialize_llnf() {
     mark_persistent(g_sset->raw());
     g_fset      = new name("_fset");
     mark_persistent(g_fset->raw());
-    g_f32set      = new name("_f32set");
-    mark_persistent(g_f32set->raw());
     g_uset      = new name("_uset");
     mark_persistent(g_uset->raw());
     g_proj      = new name("_proj");
@@ -877,7 +864,6 @@ void finalize_llnf() {
     delete g_reset;
     delete g_sset;
     delete g_fset;
-    delete g_f32set;
     delete g_proj;
     delete g_sproj;
     delete g_fproj;

src/library/compiler/llnf.h

@@ -26,7 +26,6 @@ bool is_llnf_fproj(expr const & e, unsigned & n, unsigned & offset);
 bool is_llnf_uproj(expr const & e, unsigned & idx);
 bool is_llnf_sset(expr const & e, unsigned & sz, unsigned & n, unsigned & offset);
 bool is_llnf_fset(expr const & e, unsigned & n, unsigned & offset);
-bool is_llnf_f32set(expr const & e, unsigned & n, unsigned & offset);
 bool is_llnf_uset(expr const & e, unsigned & n);
 bool is_llnf_jmp(expr const & e);
 bool is_llnf_unbox(expr const & e, unsigned & n);
@@ -44,7 +43,6 @@ inline bool is_llnf_fproj(expr const & e) { unsigned d1, d2; return is_llnf_fpro
 inline bool is_llnf_uproj(expr const & e) { unsigned d; return is_llnf_uproj(e, d); }
 inline bool is_llnf_sset(expr const & e) { unsigned d1, d2, d3; return is_llnf_sset(e, d1, d2, d3); }
 inline bool is_llnf_fset(expr const & e) { unsigned d1, d2; return is_llnf_fset(e, d1, d2); }
-inline bool is_llnf_f32set(expr const & e) { unsigned d1, d2; return is_llnf_f32set(e, d1, d2); }
 inline bool is_llnf_uset(expr const & e) { unsigned d; return is_llnf_uset(e, d); }
 inline bool is_llnf_box(expr const & e) { unsigned n; return is_llnf_box(e, n); }
 inline bool is_llnf_unbox(expr const & e) { unsigned n; return is_llnf_unbox(e, n); }
@@ -68,7 +66,6 @@ struct field_info {
         m_kind(Scalar), m_size(sz), m_idx(num), m_offset(offset), m_type(type) {}
     expr get_type() const { return m_type; }
     bool is_float() const { return is_constant(m_type, get_float_name()); }
-    bool is_float32() const { return is_constant(m_type, get_float32_name()); }
     static field_info mk_irrelevant() { return field_info(); }
     static field_info mk_object(unsigned idx) { return field_info(idx); }
     static field_info mk_usize() { return field_info(0, true); }

src/library/compiler/util.cpp

@@ -386,7 +386,6 @@ bool is_runtime_builtin_type(name const & n) {
         n == get_uint64_name() ||
         n == get_usize_name()  ||
         n == get_float_name()  ||
-        n == get_float32_name() ||
         n == get_thunk_name()  ||
         n == get_task_name()   ||
         n == get_array_name()  ||
@@ -404,8 +403,7 @@ bool is_runtime_scalar_type(name const & n) {
         n == get_uint32_name() ||
         n == get_uint64_name() ||
         n == get_usize_name()  ||
-        n == get_float_name()  ||
-        n == get_float32_name();
+        n == get_float_name();
 }
 
 bool is_llnf_unboxed_type(expr const & type) {
@@ -495,8 +493,6 @@ expr mk_runtime_type(type_checker::state & st, local_ctx const & lctx, expr e) {
                 return e;
             } else if (c == get_float_name()) {
                 return e;
-            } else if (c == get_float32_name()) {
-                return e;
             } else if (optional<unsigned> nbytes = is_enum_type(st.env(), c)) {
                 return *to_uint_type(*nbytes);
             }
@@ -811,7 +807,6 @@ void initialize_compiler_util() {
     g_builtin_scalar_size->emplace_back(get_uint32_name(), 4);
     g_builtin_scalar_size->emplace_back(get_uint64_name(), 8);
     g_builtin_scalar_size->emplace_back(get_float_name(),  8);
-    g_builtin_scalar_size->emplace_back(get_float32_name(), 4);
 }
 
 void finalize_compiler_util() {

src/library/constants.cpp

@@ -44,7 +44,6 @@ name const * g_eq_subst = nullptr;
 name const * g_eq_symm = nullptr;
 name const * g_eq_trans = nullptr;
 name const * g_float = nullptr;
-name const * g_float32 = nullptr;
 name const * g_float_array = nullptr;
 name const * g_float_array_data = nullptr;
 name const * g_false = nullptr;
@@ -192,8 +191,6 @@ void initialize_constants() {
     mark_persistent(g_eq_trans->raw());
     g_float = new name{"Float"};
     mark_persistent(g_float->raw());
-    g_float32 = new name{"Float32"};
-    mark_persistent(g_float32->raw());
     g_float_array = new name{"FloatArray"};
     mark_persistent(g_float_array->raw());
     g_float_array_data = new name{"FloatArray", "data"};
@@ -365,7 +362,6 @@ void finalize_constants() {
     delete g_eq_symm;
     delete g_eq_trans;
     delete g_float;
-    delete g_float32;
     delete g_float_array;
     delete g_float_array_data;
     delete g_false;
@@ -472,7 +468,6 @@ name const & get_eq_subst_name() { return *g_eq_subst; }
 name const & get_eq_symm_name() { return *g_eq_symm; }
 name const & get_eq_trans_name() { return *g_eq_trans; }
 name const & get_float_name() { return *g_float; }
-name const & get_float32_name() { return *g_float32; }
 name const & get_float_array_name() { return *g_float_array; }
 name const & get_float_array_data_name() { return *g_float_array_data; }
 name const & get_false_name() { return *g_false; }

src/library/constants.h

@@ -46,7 +46,6 @@ name const & get_eq_subst_name();
 name const & get_eq_symm_name();
 name const & get_eq_trans_name();
 name const & get_float_name();
-name const & get_float32_name();
 name const & get_float_array_name();
 name const & get_float_array_data_name();
 name const & get_false_name();

src/library/constants.txt

@@ -39,7 +39,6 @@ Eq.subst
 Eq.symm
 Eq.trans
 Float
-Float32
 FloatArray
 FloatArray.data
 False

src/runtime/object.cpp

@@ -1661,58 +1661,6 @@ extern "C" LEAN_EXPORT uint64_t lean_float_to_bits(double d)
     return ret;
 }
 
-// =======================================
-// Float32
-
-extern "C" LEAN_EXPORT lean_obj_res lean_float32_to_string(float a) {
-    if (isnan(a))
-        // override NaN because we don't want NaNs to be distinguishable
-        // because the sign bit / payload bits can be architecture-dependent
-        return mk_ascii_string_unchecked("NaN");
-    else
-        return mk_ascii_string_unchecked(std::to_string(a));
-}
-
-extern "C" LEAN_EXPORT float lean_float32_scaleb(float a, b_lean_obj_arg b) {
-   if (lean_is_scalar(b)) {
-     return scalbn(a, lean_scalar_to_int(b));
-   } else if (a == 0 || mpz_value(b).is_neg()) {
-     return 0;
-   } else {
-     return a * (1.0 / 0.0);
-   }
-}
-
-extern "C" LEAN_EXPORT uint8_t lean_float32_isnan(float a) { return (bool) isnan(a); }
-extern "C" LEAN_EXPORT uint8_t lean_float32_isfinite(float a) { return (bool) isfinite(a); }
-extern "C" LEAN_EXPORT uint8_t lean_float32_isinf(float a) { return (bool) isinf(a); }
-extern "C" LEAN_EXPORT obj_res lean_float32_frexp(float a) {
-    object* r = lean_alloc_ctor(0, 2, 0);
-    int exp;
-    lean_ctor_set(r, 0, lean_box_float32(frexp(a, &exp)));
-    lean_ctor_set(r, 1, isfinite(a) ? lean_int_to_int(exp) : lean_box(0));
-    return r;
-}
-
-extern "C" LEAN_EXPORT float lean_float32_of_bits(uint32_t u)
-{
-    static_assert(sizeof(float) == sizeof(u), "`float` unexpected size.");
-    float ret;
-    std::memcpy(&ret, &u, sizeof(float));
-    if (isnan(ret))
-        ret = std::numeric_limits<float>::quiet_NaN();
-    return ret;
-}
-
-extern "C" LEAN_EXPORT uint32_t lean_float32_to_bits(float d)
-{
-    uint32_t ret;
-    if (isnan(d))
-        d = std::numeric_limits<float>::quiet_NaN();
-    std::memcpy(&ret, &d, sizeof(float));
-    return ret;
-}
-
 // =======================================
 // Strings
 

src/runtime/object.h

@@ -85,13 +85,11 @@ inline uint16 cnstr_get_uint16(b_obj_arg o, unsigned offset) { return lean_ctor_
 inline uint32 cnstr_get_uint32(b_obj_arg o, unsigned offset) { return lean_ctor_get_uint32(o, offset); }
 inline uint64 cnstr_get_uint64(b_obj_arg o, unsigned offset) { return lean_ctor_get_uint64(o, offset); }
 inline double cnstr_get_float(b_obj_arg o, unsigned offset) { return lean_ctor_get_float(o, offset); }
-inline float cnstr_get_float32(b_obj_arg o, unsigned offset) { return lean_ctor_get_float32(o, offset); }
 inline void cnstr_set_uint8(b_obj_arg o, unsigned offset, uint8 v) { lean_ctor_set_uint8(o, offset, v); }
 inline void cnstr_set_uint16(b_obj_arg o, unsigned offset, uint16 v) { lean_ctor_set_uint16(o, offset, v); }
 inline void cnstr_set_uint32(b_obj_arg o, unsigned offset, uint32 v) { lean_ctor_set_uint32(o, offset, v); }
 inline void cnstr_set_uint64(b_obj_arg o, unsigned offset, uint64 v) { lean_ctor_set_uint64(o, offset, v); }
 inline void cnstr_set_float(b_obj_arg o, unsigned offset, double v) { lean_ctor_set_float(o, offset, v); }
-inline void cnstr_set_float32(b_obj_arg o, unsigned offset, float v) { lean_ctor_set_float32(o, offset, v); }
 
 // =======================================
 // Closures
@@ -374,7 +372,6 @@ inline obj_res box_uint64(unsigned long long v) { return lean_box_uint64(v); }
 inline unsigned long long unbox_uint64(b_obj_arg o) { return lean_unbox_uint64(o); }
 inline obj_res box_float(double v) { return lean_box_float(v); }
 inline double unbox_float(b_obj_arg o) { return lean_unbox_float(o); }
-inline float unbox_float32(b_obj_arg o) { return lean_unbox_float32(o); }
 inline obj_res box_size_t(size_t v) { return lean_box_usize(v); }
 inline size_t unbox_size_t(b_obj_arg o) { return lean_unbox_usize(o); }
 

tests/lean/run/5689.lean

@@ -1,17 +0,0 @@
-/-!
-# Pretty printing shouldn't make use of "non-API exports"
--/
-
-namespace A
-def n : Nat := 22
-end A
-
-namespace B
-export A (n)
-end B
-
-/-!
-Was `B.n`
--/
-/-- info: A.n : Nat -/
-#guard_msgs in #check (A.n)

tests/lean/run/DVec.lean

@@ -41,7 +41,7 @@ example (v : Vec Nat 1) : Nat :=
 -- Does not work: Aliases find that `v` could be the `TypeVec` argument since `TypeVec` is an abbrev for `Vec`.
 /--
 error: application type mismatch
-  @DVec.hd ?_ v
+  @Vec.hd ?_ v
 argument
   v
 has type

tests/lean/run/alias.lean

@@ -26,7 +26,7 @@ However, this dot notation fails since there is no `FinSet` argument.
 However, unfolding is the preferred method.
 -/
 /--
-error: invalid field notation, function 'Set.union' does not have argument with type (FinSet ...) that can be used, it must be explicit or implicit with a unique name
+error: invalid field notation, function 'FinSet.union' does not have argument with type (FinSet ...) that can be used, it must be explicit or implicit with a unique name
 -/
 #guard_msgs in
 example (x y : FinSet 10) : FinSet 10 :=

tests/lean/run/bv_uninterpreted.lean

@@ -5,8 +5,8 @@ example {x y z : BitVec w} :
     (x &&& y) ||| (x &&& z) ||| (y &&& z) ||| x ||| y ||| z
       =
     ~~~ ((~~~ x) &&& (~~~ y) &&& (~~~ z)) := by
-  ext i h
-  simp [h]
+  ext
+  simp
   bv_decide
 
 @[irreducible]

tests/lean/run/wfOverapplicationIssue.lean

@@ -1,6 +1,6 @@
 theorem Array.sizeOf_lt_of_mem' [DecidableEq α] [SizeOf α] {as : Array α} (h : as.contains a) : sizeOf a < sizeOf as := by
   simp [Membership.mem, contains, any, Id.run, BEq.beq, anyM] at h
-  let rec aux (j : Nat) : anyM.loop (m := Id) (fun b => decide (a = b)) as as.size (Nat.le_refl ..) j = true → sizeOf a < sizeOf as := by
+  let rec aux (j : Nat) : anyM.loop (m := Id) (fun b => decide (b = a)) as as.size (Nat.le_refl ..) j = true → sizeOf a < sizeOf as := by
     unfold anyM.loop
     intro h
     split at h