chore: reordering in Array.Basic

This is to simplify the manual's cross-referencing.

src/Init/ByCases.lean

@@ -40,21 +40,23 @@ theorem apply_ite (f : α → β) (P : Prop) [Decidable P] (x y : α) :
 /-- A `dite` whose results do not actually depend on the condition may be reduced to an `ite`. -/
 @[simp] theorem dite_eq_ite [Decidable P] : (dite P (fun _ => a) fun _ => b) = ite P a b := rfl
 
--- We don't mark this as `simp` as it is already handled by `ite_eq_right_iff`.
+@[deprecated "Use `ite_eq_right_iff`" (since := "2024-09-18")]
 theorem ite_some_none_eq_none [Decidable P] :
     (if P then some x else none) = none ↔ ¬ P := by
   simp only [ite_eq_right_iff, reduceCtorEq]
   rfl
 
-@[simp] theorem ite_some_none_eq_some [Decidable P] :
+@[deprecated "Use `Option.ite_none_right_eq_some`" (since := "2024-09-18")]
+theorem ite_some_none_eq_some [Decidable P] :
     (if P then some x else none) = some y ↔ P ∧ x = y := by
   split <;> simp_all
 
--- This is not marked as `simp` as it is already handled by `dite_eq_right_iff`.
+@[deprecated "Use `dite_eq_right_iff" (since := "2024-09-18")]
 theorem dite_some_none_eq_none [Decidable P] {x : P → α} :
     (if h : P then some (x h) else none) = none ↔ ¬P := by
   simp
 
-@[simp] theorem dite_some_none_eq_some [Decidable P] {x : P → α} {y : α} :
+@[deprecated "Use `Option.dite_none_right_eq_some`" (since := "2024-09-18")]
+theorem dite_some_none_eq_some [Decidable P] {x : P → α} {y : α} :
     (if h : P then some (x h) else none) = some y ↔ ∃ h : P, x h = y := by
   by_cases h : P <;> simp [h]

src/Init/Core.lean

@@ -823,6 +823,8 @@ theorem iff_iff_implies_and_implies {a b : Prop} : (a ↔ b) ↔ (a → b) ∧ (
 protected theorem Iff.rfl {a : Prop} : a ↔ a :=
   Iff.refl a
 
+macro_rules | `(tactic| rfl) => `(tactic| exact Iff.rfl)
+
 theorem Iff.of_eq (h : a = b) : a ↔ b := h ▸ Iff.rfl
 
 theorem Iff.trans (h₁ : a ↔ b) (h₂ : b ↔ c) : a ↔ c :=
@@ -1191,6 +1193,21 @@ end
 
 /-! # Product -/
 
+instance [h1 : Nonempty α] [h2 : Nonempty β] : Nonempty (α × β) :=
+  Nonempty.elim h1 fun x =>
+    Nonempty.elim h2 fun y =>
+      ⟨(x, y)⟩
+
+instance [h1 : Nonempty α] [h2 : Nonempty β] : Nonempty (MProd α β) :=
+  Nonempty.elim h1 fun x =>
+    Nonempty.elim h2 fun y =>
+      ⟨⟨x, y⟩⟩
+
+instance [h1 : Nonempty α] [h2 : Nonempty β] : Nonempty (PProd α β) :=
+  Nonempty.elim h1 fun x =>
+    Nonempty.elim h2 fun y =>
+      ⟨⟨x, y⟩⟩
+
 instance [Inhabited α] [Inhabited β] : Inhabited (α × β) where
   default := (default, default)
 

src/Init/Data/Array.lean

@@ -15,3 +15,4 @@ import Init.Data.Array.BasicAux
 import Init.Data.Array.Lemmas
 import Init.Data.Array.TakeDrop
 import Init.Data.Array.Bootstrap
+import Init.Data.Array.GetLit

src/Init/Data/Array/Basic.lean

@@ -13,43 +13,76 @@ import Init.Data.ToString.Basic
 import Init.GetElem
 universe u v w
 
-namespace Array
+/-! ### Array literal syntax -/
+
+syntax "#[" withoutPosition(sepBy(term, ", ")) "]" : term
+
+macro_rules
+  | `(#[ $elems,* ]) => `(List.toArray [ $elems,* ])
+
 variable {α : Type u}
 
+namespace Array
+
+/-! ### Preliminary theorems -/
+
+@[simp] theorem size_set (a : Array α) (i : Fin a.size) (v : α) : (set a i v).size = a.size :=
+  List.length_set ..
+
+@[simp] theorem size_push (a : Array α) (v : α) : (push a v).size = a.size + 1 :=
+  List.length_concat ..
+
+theorem ext (a b : Array α)
+    (h₁ : a.size = b.size)
+    (h₂ : (i : Nat) → (hi₁ : i < a.size) → (hi₂ : i < b.size) → a[i] = b[i])
+    : a = b := by
+  let rec extAux (a b : List α)
+      (h₁ : a.length = b.length)
+      (h₂ : (i : Nat) → (hi₁ : i < a.length) → (hi₂ : i < b.length) → a.get ⟨i, hi₁⟩ = b.get ⟨i, hi₂⟩)
+      : a = b := by
+    induction a generalizing b with
+    | nil =>
+      cases b with
+      | nil       => rfl
+      | cons b bs => rw [List.length_cons] at h₁; injection h₁
+    | cons a as ih =>
+      cases b with
+      | nil => rw [List.length_cons] at h₁; injection h₁
+      | cons b bs =>
+        have hz₁ : 0 < (a::as).length := by rw [List.length_cons]; apply Nat.zero_lt_succ
+        have hz₂ : 0 < (b::bs).length := by rw [List.length_cons]; apply Nat.zero_lt_succ
+        have headEq : a = b := h₂ 0 hz₁ hz₂
+        have h₁' : as.length = bs.length := by rw [List.length_cons, List.length_cons] at h₁; injection h₁
+        have h₂' : (i : Nat) → (hi₁ : i < as.length) → (hi₂ : i < bs.length) → as.get ⟨i, hi₁⟩ = bs.get ⟨i, hi₂⟩ := by
+          intro i hi₁ hi₂
+          have hi₁' : i+1 < (a::as).length := by rw [List.length_cons]; apply Nat.succ_lt_succ; assumption
+          have hi₂' : i+1 < (b::bs).length := by rw [List.length_cons]; apply Nat.succ_lt_succ; assumption
+          have : (a::as).get ⟨i+1, hi₁'⟩ = (b::bs).get ⟨i+1, hi₂'⟩ := h₂ (i+1) hi₁' hi₂'
+          apply this
+        have tailEq : as = bs := ih bs h₁' h₂'
+        rw [headEq, tailEq]
+  cases a; cases b
+  apply congrArg
+  apply extAux
+  assumption
+  assumption
+
+theorem ext' {as bs : Array α} (h : as.toList = bs.toList) : as = bs := by
+  cases as; cases bs; simp at h; rw [h]
+
+@[simp] theorem toArrayAux_eq (as : List α) (acc : Array α) : (as.toArrayAux acc).toList = acc.toList ++ as := by
+  induction as generalizing acc <;> simp [*, List.toArrayAux, Array.push, List.append_assoc, List.concat_eq_append]
+
+@[simp] theorem toList_toArray (as : List α) : as.toArray.toList = as := by
+  simp [List.toArray, Array.mkEmpty]
+
+@[simp] theorem size_toArray (as : List α) : as.toArray.size = as.length := by simp [size]
+
+@[deprecated toList_toArray (since := "2024-09-09")] abbrev data_toArray := @toList_toArray
+
 @[deprecated Array.toList (since := "2024-09-10")] abbrev Array.data := @Array.toList
 
-@[extern "lean_mk_array"]
-def mkArray {α : Type u} (n : Nat) (v : α) : Array α where
-  toList := List.replicate n v
-
-/--
-`ofFn f` with `f : Fin n → α` returns the list whose ith element is `f i`.
-```
-ofFn f = #[f 0, f 1, ... , f(n - 1)]
-``` -/
-def ofFn {n} (f : Fin n → α) : Array α := go 0 (mkEmpty n) where
-  /-- Auxiliary for `ofFn`. `ofFn.go f i acc = acc ++ #[f i, ..., f(n - 1)]` -/
-  go (i : Nat) (acc : Array α) : Array α :=
-    if h : i < n then go (i+1) (acc.push (f ⟨i, h⟩)) else acc
-termination_by n - i
-decreasing_by simp_wf; decreasing_trivial_pre_omega
-
-/-- The array `#[0, 1, ..., n - 1]`. -/
-def range (n : Nat) : Array Nat :=
-  n.fold (flip Array.push) (mkEmpty n)
-
-@[simp] theorem size_mkArray (n : Nat) (v : α) : (mkArray n v).size = n :=
-  List.length_replicate ..
-
-instance : EmptyCollection (Array α) := ⟨Array.empty⟩
-instance : Inhabited (Array α) where
-  default := Array.empty
-
-@[simp] def isEmpty (a : Array α) : Bool :=
-  a.size = 0
-
-def singleton (v : α) : Array α :=
-  mkArray 1 v
+/-! ### Externs -/
 
 /-- Low-level version of `size` that directly queries the C array object cached size.
     While this is not provable, `usize` always returns the exact size of the array since
@@ -65,29 +98,6 @@ def usize (a : @& Array α) : USize := a.size.toUSize
 def uget (a : @& Array α) (i : USize) (h : i.toNat < a.size) : α :=
   a[i.toNat]
 
-instance : GetElem (Array α) USize α fun xs i => i.toNat < xs.size where
-  getElem xs i h := xs.uget i h
-
-def back [Inhabited α] (a : Array α) : α :=
-  a.get! (a.size - 1)
-
-def get? (a : Array α) (i : Nat) : Option α :=
-  if h : i < a.size then some a[i] else none
-
-def back? (a : Array α) : Option α :=
-  a.get? (a.size - 1)
-
--- auxiliary declaration used in the equation compiler when pattern matching array literals.
-abbrev getLit {α : Type u} {n : Nat} (a : Array α) (i : Nat) (h₁ : a.size = n) (h₂ : i < n) : α :=
-  have := h₁.symm ▸ h₂
-  a[i]
-
-@[simp] theorem size_set (a : Array α) (i : Fin a.size) (v : α) : (set a i v).size = a.size :=
-  List.length_set ..
-
-@[simp] theorem size_push (a : Array α) (v : α) : (push a v).size = a.size + 1 :=
-  List.length_concat ..
-
 /-- Low-level version of `fset` which is as fast as a C array fset.
    `Fin` values are represented as tag pointers in the Lean runtime. Thus,
    `fset` may be slightly slower than `uset`. -/
@@ -95,6 +105,19 @@ abbrev getLit {α : Type u} {n : Nat} (a : Array α) (i : Nat) (h₁ : a.size =
 def uset (a : Array α) (i : USize) (v : α) (h : i.toNat < a.size) : Array α :=
   a.set ⟨i.toNat, h⟩ v
 
+@[extern "lean_array_pop"]
+def pop (a : Array α) : Array α where
+  toList := a.toList.dropLast
+
+@[simp] theorem size_pop (a : Array α) : a.pop.size = a.size - 1 := by
+  match a with
+  | ⟨[]⟩ => rfl
+  | ⟨a::as⟩ => simp [pop, Nat.succ_sub_succ_eq_sub, size]
+
+@[extern "lean_mk_array"]
+def mkArray {α : Type u} (n : Nat) (v : α) : Array α where
+  toList := List.replicate n v
+
 /--
 Swaps two entries in an array.
 
@@ -108,6 +131,10 @@ def swap (a : Array α) (i j : @& Fin a.size) : Array α :=
   let a'  := a.set i v₂
   a'.set (size_set a i v₂ ▸ j) v₁
 
+@[simp] theorem size_swap (a : Array α) (i j : Fin a.size) : (a.swap i j).size = a.size := by
+  show ((a.set i (a.get j)).set (size_set a i _ ▸ j) (a.get i)).size = a.size
+  rw [size_set, size_set]
+
 /--
 Swaps two entries in an array, or returns the array unchanged if either index is out of bounds.
 
@@ -121,6 +148,66 @@ def swap! (a : Array α) (i j : @& Nat) : Array α :=
   else a
   else a
 
+/-! ### GetElem instance for `USize`, backed by `uget` -/
+
+instance : GetElem (Array α) USize α fun xs i => i.toNat < xs.size where
+  getElem xs i h := xs.uget i h
+
+/-! ### Definitions -/
+
+instance : EmptyCollection (Array α) := ⟨Array.empty⟩
+instance : Inhabited (Array α) where
+  default := Array.empty
+
+@[simp] def isEmpty (a : Array α) : Bool :=
+  a.size = 0
+
+-- TODO(Leo): cleanup
+@[specialize]
+def isEqvAux (a b : Array α) (hsz : a.size = b.size) (p : α → α → Bool) (i : Nat) : Bool :=
+  if h : i < a.size then
+     have : i < b.size := hsz ▸ h
+     p a[i] b[i] && isEqvAux a b hsz p (i+1)
+  else
+    true
+decreasing_by simp_wf; decreasing_trivial_pre_omega
+
+@[inline] def isEqv (a b : Array α) (p : α → α → Bool) : Bool :=
+  if h : a.size = b.size then
+    isEqvAux a b h p 0
+  else
+    false
+
+instance [BEq α] : BEq (Array α) :=
+  ⟨fun a b => isEqv a b BEq.beq⟩
+
+/--
+`ofFn f` with `f : Fin n → α` returns the list whose ith element is `f i`.
+```
+ofFn f = #[f 0, f 1, ... , f(n - 1)]
+``` -/
+def ofFn {n} (f : Fin n → α) : Array α := go 0 (mkEmpty n) where
+  /-- Auxiliary for `ofFn`. `ofFn.go f i acc = acc ++ #[f i, ..., f(n - 1)]` -/
+  go (i : Nat) (acc : Array α) : Array α :=
+    if h : i < n then go (i+1) (acc.push (f ⟨i, h⟩)) else acc
+decreasing_by simp_wf; decreasing_trivial_pre_omega
+
+/-- The array `#[0, 1, ..., n - 1]`. -/
+def range (n : Nat) : Array Nat :=
+  n.fold (flip Array.push) (mkEmpty n)
+
+def singleton (v : α) : Array α :=
+  mkArray 1 v
+
+def back [Inhabited α] (a : Array α) : α :=
+  a.get! (a.size - 1)
+
+def get? (a : Array α) (i : Nat) : Option α :=
+  if h : i < a.size then some a[i] else none
+
+def back? (a : Array α) : Option α :=
+  a.get? (a.size - 1)
+
 @[inline] def swapAt (a : Array α) (i : Fin a.size) (v : α) : α × Array α :=
   let e := a.get i
   let a := a.set i v
@@ -134,10 +221,6 @@ def swapAt! (a : Array α) (i : Nat) (v : α) : α × Array α :=
     have : Inhabited α := ⟨v⟩
     panic! ("index " ++ toString i ++ " out of bounds")
 
-@[extern "lean_array_pop"]
-def pop (a : Array α) : Array α where
-  toList := a.toList.dropLast
-
 def shrink (a : Array α) (n : Nat) : Array α :=
   let rec loop
     | 0,   a => a
@@ -311,7 +394,6 @@ def mapM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α
       map (i+1) (r.push (← f as[i]))
     else
       pure r
-  termination_by as.size - i
   decreasing_by simp_wf; decreasing_trivial_pre_omega
   map 0 (mkEmpty as.size)
 
@@ -384,7 +466,6 @@ def anyM {α : Type u} {m : Type → Type w} [Monad m] (p : α → m Bool) (as :
           loop (j+1)
       else
         pure false
-      termination_by stop - j
       decreasing_by simp_wf; decreasing_trivial_pre_omega
     loop start
   if h : stop ≤ as.size then
@@ -470,12 +551,22 @@ def findIdx? {α : Type u} (as : Array α) (p : α → Bool) : Option Nat :=
     if h : j < as.size then
       if p as[j] then some j else loop (j + 1)
     else none
-    termination_by as.size - j
     decreasing_by simp_wf; decreasing_trivial_pre_omega
   loop 0
 
 def getIdx? [BEq α] (a : Array α) (v : α) : Option Nat :=
-a.findIdx? fun a => a == v
+  a.findIdx? fun a => a == v
+
+def indexOfAux [BEq α] (a : Array α) (v : α) (i : Nat) : Option (Fin a.size) :=
+  if h : i < a.size then
+    let idx : Fin a.size := ⟨i, h⟩;
+    if a.get idx == v then some idx
+    else indexOfAux a v (i+1)
+  else none
+decreasing_by simp_wf; decreasing_trivial_pre_omega
+
+def indexOf? [BEq α] (a : Array α) (v : α) : Option (Fin a.size) :=
+  indexOfAux a v 0
 
 @[inline]
 def any (as : Array α) (p : α → Bool) (start := 0) (stop := as.size) : Bool :=
@@ -491,13 +582,6 @@ def contains [BEq α] (as : Array α) (a : α) : Bool :=
 def elem [BEq α] (a : α) (as : Array α) : Bool :=
   as.contains a
 
-@[inline] def getEvenElems (as : Array α) : Array α :=
-  (·.2) <| as.foldl (init := (true, Array.empty)) fun (even, r) a =>
-    if even then
-      (false, r.push a)
-    else
-      (true, r)
-
 /-- Convert a `Array α` into an `List α`. This is O(n) in the size of the array.  -/
 -- This function is exported to C, where it is called by `Array.toList`
 -- (the projection) to implement this functionality.
@@ -510,17 +594,6 @@ def toListImpl (as : Array α) : List α :=
 def toListAppend (as : Array α) (l : List α) : List α :=
   as.foldr List.cons l
 
-instance {α : Type u} [Repr α] : Repr (Array α) where
-  reprPrec a _ :=
-    let _ : Std.ToFormat α := ⟨repr⟩
-    if a.size == 0 then
-      "#[]"
-    else
-      Std.Format.bracketFill "#[" (Std.Format.joinSep (toList a) ("," ++ Std.Format.line)) "]"
-
-instance [ToString α] : ToString (Array α) where
-  toString a := "#" ++ toString a.toList
-
 protected def append (as : Array α) (bs : Array α) : Array α :=
   bs.foldl (init := as) fun r v => r.push v
 
@@ -546,44 +619,13 @@ def concatMap (f : α → Array β) (as : Array α) : Array β :=
 def flatten (as : Array (Array α)) : Array α :=
   as.foldl (init := empty) fun r a => r ++ a
 
-end Array
-
-export Array (mkArray)
-
-syntax "#[" withoutPosition(sepBy(term, ", ")) "]" : term
-
-macro_rules
-  | `(#[ $elems,* ]) => `(List.toArray [ $elems,* ])
-
-namespace Array
-
--- TODO(Leo): cleanup
-@[specialize]
-def isEqvAux (a b : Array α) (hsz : a.size = b.size) (p : α → α → Bool) (i : Nat) : Bool :=
-  if h : i < a.size then
-     have : i < b.size := hsz ▸ h
-     p a[i] b[i] && isEqvAux a b hsz p (i+1)
-  else
-    true
-termination_by a.size - i
-decreasing_by simp_wf; decreasing_trivial_pre_omega
-
-@[inline] def isEqv (a b : Array α) (p : α → α → Bool) : Bool :=
-  if h : a.size = b.size then
-    isEqvAux a b h p 0
-  else
-    false
-
-instance [BEq α] : BEq (Array α) :=
-  ⟨fun a b => isEqv a b BEq.beq⟩
-
 @[inline]
 def filter (p : α → Bool) (as : Array α) (start := 0) (stop := as.size) : Array α :=
   as.foldl (init := #[]) (start := start) (stop := stop) fun r a =>
     if p a then r.push a else r
 
 @[inline]
-def filterM [Monad m] (p : α → m Bool) (as : Array α) (start := 0) (stop := as.size) : m (Array α) :=
+def filterM {α : Type} [Monad m] (p : α → m Bool) (as : Array α) (start := 0) (stop := as.size) : m (Array α) :=
   as.foldlM (init := #[]) (start := start) (stop := stop) fun r a => do
     if (← p a) then return r.push a else return r
 
@@ -618,92 +660,23 @@ def partition (p : α → Bool) (as : Array α) : Array α × Array α := Id.run
       cs := cs.push a
   return (bs, cs)
 
-theorem ext (a b : Array α)
-    (h₁ : a.size = b.size)
-    (h₂ : (i : Nat) → (hi₁ : i < a.size) → (hi₂ : i < b.size) → a[i] = b[i])
-    : a = b := by
-  let rec extAux (a b : List α)
-      (h₁ : a.length = b.length)
-      (h₂ : (i : Nat) → (hi₁ : i < a.length) → (hi₂ : i < b.length) → a.get ⟨i, hi₁⟩ = b.get ⟨i, hi₂⟩)
-      : a = b := by
-    induction a generalizing b with
-    | nil =>
-      cases b with
-      | nil       => rfl
-      | cons b bs => rw [List.length_cons] at h₁; injection h₁
-    | cons a as ih =>
-      cases b with
-      | nil => rw [List.length_cons] at h₁; injection h₁
-      | cons b bs =>
-        have hz₁ : 0 < (a::as).length := by rw [List.length_cons]; apply Nat.zero_lt_succ
-        have hz₂ : 0 < (b::bs).length := by rw [List.length_cons]; apply Nat.zero_lt_succ
-        have headEq : a = b := h₂ 0 hz₁ hz₂
-        have h₁' : as.length = bs.length := by rw [List.length_cons, List.length_cons] at h₁; injection h₁
-        have h₂' : (i : Nat) → (hi₁ : i < as.length) → (hi₂ : i < bs.length) → as.get ⟨i, hi₁⟩ = bs.get ⟨i, hi₂⟩ := by
-          intro i hi₁ hi₂
-          have hi₁' : i+1 < (a::as).length := by rw [List.length_cons]; apply Nat.succ_lt_succ; assumption
-          have hi₂' : i+1 < (b::bs).length := by rw [List.length_cons]; apply Nat.succ_lt_succ; assumption
-          have : (a::as).get ⟨i+1, hi₁'⟩ = (b::bs).get ⟨i+1, hi₂'⟩ := h₂ (i+1) hi₁' hi₂'
-          apply this
-        have tailEq : as = bs := ih bs h₁' h₂'
-        rw [headEq, tailEq]
-  cases a; cases b
-  apply congrArg
-  apply extAux
-  assumption
-  assumption
-
-theorem extLit {n : Nat}
-    (a b : Array α)
-    (hsz₁ : a.size = n) (hsz₂ : b.size = n)
-    (h : (i : Nat) → (hi : i < n) → a.getLit i hsz₁ hi = b.getLit i hsz₂ hi) : a = b :=
-  Array.ext a b (hsz₁.trans hsz₂.symm) fun i hi₁ _ => h i (hsz₁ ▸ hi₁)
-
-end Array
-
--- CLEANUP the following code
-namespace Array
-
-def indexOfAux [BEq α] (a : Array α) (v : α) (i : Nat) : Option (Fin a.size) :=
-  if h : i < a.size then
-    let idx : Fin a.size := ⟨i, h⟩;
-    if a.get idx == v then some idx
-    else indexOfAux a v (i+1)
-  else none
-termination_by a.size - i
-decreasing_by simp_wf; decreasing_trivial_pre_omega
-
-def indexOf? [BEq α] (a : Array α) (v : α) : Option (Fin a.size) :=
-  indexOfAux a v 0
-
-@[simp] theorem size_swap (a : Array α) (i j : Fin a.size) : (a.swap i j).size = a.size := by
-  show ((a.set i (a.get j)).set (size_set a i _ ▸ j) (a.get i)).size = a.size
-  rw [size_set, size_set]
-
-@[simp] theorem size_pop (a : Array α) : a.pop.size = a.size - 1 := by
-  match a with
-  | ⟨[]⟩ => rfl
-  | ⟨a::as⟩ => simp [pop, Nat.succ_sub_succ_eq_sub, size]
-
-theorem reverse.termination {i j : Nat} (h : i < j) : j - 1 - (i + 1) < j - i := by
-  rw [Nat.sub_sub, Nat.add_comm]
-  exact Nat.lt_of_le_of_lt (Nat.pred_le _) (Nat.sub_succ_lt_self _ _ h)
-
 def reverse (as : Array α) : Array α :=
   if h : as.size ≤ 1 then
     as
   else
     loop as 0 ⟨as.size - 1, Nat.pred_lt (mt (fun h : as.size = 0 => h ▸ by decide) h)⟩
 where
+  termination {i j : Nat} (h : i < j) : j - 1 - (i + 1) < j - i := by
+    rw [Nat.sub_sub, Nat.add_comm]
+    exact Nat.lt_of_le_of_lt (Nat.pred_le _) (Nat.sub_succ_lt_self _ _ h)
   loop (as : Array α) (i : Nat) (j : Fin as.size) :=
     if h : i < j then
-      have := reverse.termination h
+      have := termination h
       let as := as.swap ⟨i, Nat.lt_trans h j.2⟩ j
       have : j-1 < as.size := by rw [size_swap]; exact Nat.lt_of_le_of_lt (Nat.pred_le _) j.2
       loop as (i+1) ⟨j-1, this⟩
     else
       as
-termination_by j - i
 
 def popWhile (p : α → Bool) (as : Array α) : Array α :=
   if h : as.size > 0 then
@@ -713,7 +686,6 @@ def popWhile (p : α → Bool) (as : Array α) : Array α :=
       as
   else
     as
-termination_by as.size
 decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 def takeWhile (p : α → Bool) (as : Array α) : Array α :=
@@ -726,7 +698,6 @@ def takeWhile (p : α → Bool) (as : Array α) : Array α :=
         r
     else
       r
-    termination_by as.size - i
     decreasing_by simp_wf; decreasing_trivial_pre_omega
   go 0 #[]
 
@@ -744,6 +715,7 @@ def feraseIdx (a : Array α) (i : Fin a.size) : Array α :=
 termination_by a.size - i.val
 decreasing_by simp_wf; exact Nat.sub_succ_lt_self _ _ i.isLt
 
+-- This is required in `Lean.Data.PersistentHashMap`.
 theorem size_feraseIdx (a : Array α) (i : Fin a.size) : (a.feraseIdx i).size = a.size - 1 := by
   induction a, i using Array.feraseIdx.induct with
   | @case1 a i h a' _ ih =>
@@ -774,7 +746,6 @@ def erase [BEq α] (as : Array α) (a : α) : Array α :=
       loop as ⟨j', by rw [size_swap]; exact j'.2⟩
     else
       as
-    termination_by j.1
     decreasing_by simp_wf; decreasing_trivial_pre_omega
   let j := as.size
   let as := as.push a
@@ -786,41 +757,6 @@ def insertAt! (as : Array α) (i : Nat) (a : α) : Array α :=
     insertAt as ⟨i, Nat.lt_succ_of_le h⟩ a
   else panic! "invalid index"
 
-def toListLitAux (a : Array α) (n : Nat) (hsz : a.size = n) : ∀ (i : Nat), i ≤ a.size → List α → List α
-  | 0,     _,  acc => acc
-  | (i+1), hi, acc => toListLitAux a n hsz i (Nat.le_of_succ_le hi) (a.getLit i hsz (Nat.lt_of_lt_of_eq (Nat.lt_of_lt_of_le (Nat.lt_succ_self i) hi) hsz) :: acc)
-
-def toArrayLit (a : Array α) (n : Nat) (hsz : a.size = n) : Array α :=
-  List.toArray <| toListLitAux a n hsz n (hsz ▸ Nat.le_refl _) []
-
-theorem ext' {as bs : Array α} (h : as.toList = bs.toList) : as = bs := by
-  cases as; cases bs; simp at h; rw [h]
-
-@[simp] theorem toArrayAux_eq (as : List α) (acc : Array α) : (as.toArrayAux acc).toList = acc.toList ++ as := by
-  induction as generalizing acc <;> simp [*, List.toArrayAux, Array.push, List.append_assoc, List.concat_eq_append]
-
-@[simp] theorem toList_toArray (as : List α) : as.toArray.toList = as := by
-  simp [List.toArray, Array.mkEmpty]
-
-@[deprecated toList_toArray (since := "2024-09-09")] abbrev data_toArray := @toList_toArray
-
-@[simp] theorem size_toArray (as : List α) : as.toArray.size = as.length := by simp [size]
-
-theorem toArrayLit_eq (as : Array α) (n : Nat) (hsz : as.size = n) : as = toArrayLit as n hsz := by
-  apply ext'
-  simp [toArrayLit, toList_toArray]
-  have hle : n ≤ as.size := hsz ▸ Nat.le_refl _
-  have hge : as.size ≤ n := hsz ▸ Nat.le_refl _
-  have := go n hle
-  rw [List.drop_eq_nil_of_le hge] at this
-  rw [this]
-where
-  getLit_eq (as : Array α) (i : Nat) (h₁ : as.size = n) (h₂ : i < n) : as.getLit i h₁ h₂ = getElem as.toList i ((id (α := as.toList.length = n) h₁) ▸ h₂) :=
-    rfl
-
-  go (i : Nat) (hi : i ≤ as.size) : toListLitAux as n hsz i hi (as.toList.drop i) = as.toList := by
-    induction i <;> simp [getLit_eq, List.get_drop_eq_drop, toListLitAux, List.drop, *]
-
 def isPrefixOfAux [BEq α] (as bs : Array α) (hle : as.size ≤ bs.size) (i : Nat) : Bool :=
   if h : i < as.size then
     let a := as[i]
@@ -832,7 +768,6 @@ def isPrefixOfAux [BEq α] (as bs : Array α) (hle : as.size ≤ bs.size) (i : N
       false
   else
     true
-termination_by as.size - i
 decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 /-- Return true iff `as` is a prefix of `bs`.
@@ -843,23 +778,6 @@ def isPrefixOf [BEq α] (as bs : Array α) : Bool :=
   else
     false
 
-private def allDiffAuxAux [BEq α] (as : Array α) (a : α) : forall (i : Nat), i < as.size → Bool
-  | 0,   _ => true
-  | i+1, h =>
-    have : i < as.size := Nat.lt_trans (Nat.lt_succ_self _) h;
-    a != as[i] && allDiffAuxAux as a i this
-
-private def allDiffAux [BEq α] (as : Array α) (i : Nat) : Bool :=
-  if h : i < as.size then
-    allDiffAuxAux as as[i] i h && allDiffAux as (i+1)
-  else
-    true
-termination_by as.size - i
-decreasing_by simp_wf; decreasing_trivial_pre_omega
-
-def allDiff [BEq α] (as : Array α) : Bool :=
-  allDiffAux as 0
-
 @[specialize] def zipWithAux (f : α → β → γ) (as : Array α) (bs : Array β) (i : Nat) (cs : Array γ) : Array γ :=
   if h : i < as.size then
     let a := as[i]
@@ -870,7 +788,6 @@ def allDiff [BEq α] (as : Array α) : Bool :=
       cs
   else
     cs
-termination_by as.size - i
 decreasing_by simp_wf; decreasing_trivial_pre_omega
 
 @[inline] def zipWith (as : Array α) (bs : Array β) (f : α → β → γ) : Array γ :=
@@ -886,4 +803,47 @@ def split (as : Array α) (p : α → Bool) : Array α × Array α :=
   as.foldl (init := (#[], #[])) fun (as, bs) a =>
     if p a then (as.push a, bs) else (as, bs.push a)
 
+/-! ### Auxiliary functions used in metaprogramming.
+
+We do not intend to provide verification theorems for these functions.
+-/
+
+private def allDiffAuxAux [BEq α] (as : Array α) (a : α) : forall (i : Nat), i < as.size → Bool
+  | 0,   _ => true
+  | i+1, h =>
+    have : i < as.size := Nat.lt_trans (Nat.lt_succ_self _) h;
+    a != as[i] && allDiffAuxAux as a i this
+
+private def allDiffAux [BEq α] (as : Array α) (i : Nat) : Bool :=
+  if h : i < as.size then
+    allDiffAuxAux as as[i] i h && allDiffAux as (i+1)
+  else
+    true
+decreasing_by simp_wf; decreasing_trivial_pre_omega
+
+def allDiff [BEq α] (as : Array α) : Bool :=
+  allDiffAux as 0
+
+@[inline] def getEvenElems (as : Array α) : Array α :=
+  (·.2) <| as.foldl (init := (true, Array.empty)) fun (even, r) a =>
+    if even then
+      (false, r.push a)
+    else
+      (true, r)
+
+/-! ### Repr and ToString -/
+
+instance {α : Type u} [Repr α] : Repr (Array α) where
+  reprPrec a _ :=
+    let _ : Std.ToFormat α := ⟨repr⟩
+    if a.size == 0 then
+      "#[]"
+    else
+      Std.Format.bracketFill "#[" (Std.Format.joinSep (toList a) ("," ++ Std.Format.line)) "]"
+
+instance [ToString α] : ToString (Array α) where
+  toString a := "#" ++ toString a.toList
+
 end Array
+
+export Array (mkArray)

src/Init/Data/Array/GetLit.lean

@@ -0,0 +1,46 @@
+/-
+Copyright (c) 2018 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+
+prelude
+import Init.Data.Array.Basic
+
+namespace Array
+
+/-! ### getLit -/
+
+-- auxiliary declaration used in the equation compiler when pattern matching array literals.
+abbrev getLit {α : Type u} {n : Nat} (a : Array α) (i : Nat) (h₁ : a.size = n) (h₂ : i < n) : α :=
+  have := h₁.symm ▸ h₂
+  a[i]
+
+theorem extLit {n : Nat}
+    (a b : Array α)
+    (hsz₁ : a.size = n) (hsz₂ : b.size = n)
+    (h : (i : Nat) → (hi : i < n) → a.getLit i hsz₁ hi = b.getLit i hsz₂ hi) : a = b :=
+  Array.ext a b (hsz₁.trans hsz₂.symm) fun i hi₁ _ => h i (hsz₁ ▸ hi₁)
+
+def toListLitAux (a : Array α) (n : Nat) (hsz : a.size = n) : ∀ (i : Nat), i ≤ a.size → List α → List α
+  | 0,     _,  acc => acc
+  | (i+1), hi, acc => toListLitAux a n hsz i (Nat.le_of_succ_le hi) (a.getLit i hsz (Nat.lt_of_lt_of_eq (Nat.lt_of_lt_of_le (Nat.lt_succ_self i) hi) hsz) :: acc)
+
+def toArrayLit (a : Array α) (n : Nat) (hsz : a.size = n) : Array α :=
+  List.toArray <| toListLitAux a n hsz n (hsz ▸ Nat.le_refl _) []
+
+theorem toArrayLit_eq (as : Array α) (n : Nat) (hsz : as.size = n) : as = toArrayLit as n hsz := by
+  apply ext'
+  simp [toArrayLit, toList_toArray]
+  have hle : n ≤ as.size := hsz ▸ Nat.le_refl _
+  have hge : as.size ≤ n := hsz ▸ Nat.le_refl _
+  have := go n hle
+  rw [List.drop_eq_nil_of_le hge] at this
+  rw [this]
+where
+  getLit_eq (as : Array α) (i : Nat) (h₁ : as.size = n) (h₂ : i < n) : as.getLit i h₁ h₂ = getElem as.toList i ((id (α := as.toList.length = n) h₁) ▸ h₂) :=
+    rfl
+  go (i : Nat) (hi : i ≤ as.size) : toListLitAux as n hsz i hi (as.toList.drop i) = as.toList := by
+    induction i <;> simp [getLit_eq, List.get_drop_eq_drop, toListLitAux, List.drop, *]
+
+end Array

src/Init/Data/Array/Lemmas.lean

@@ -19,7 +19,7 @@ This file contains some theorems about `Array` and `List` needed for `Init.Data.
 
 namespace Array
 
-attribute [simp] data_toArray uset
+attribute [simp] uset
 
 @[simp] theorem singleton_def (v : α) : singleton v = #[v] := rfl
 
@@ -271,6 +271,9 @@ termination_by n - i
 
 /-- # mkArray -/
 
+@[simp] theorem size_mkArray (n : Nat) (v : α) : (mkArray n v).size = n :=
+  List.length_replicate ..
+
 @[simp] theorem toList_mkArray (n : Nat) (v : α) : (mkArray n v).toList = List.replicate n v := rfl
 
 @[deprecated toList_mkArray (since := "2024-09-09")]
@@ -495,7 +498,6 @@ abbrev size_eq_length_data := @size_eq_length_toList
   let rec go (as : Array α) (i j) : (reverse.loop as i j).size = as.size := by
     rw [reverse.loop]
     if h : i < j then
-      have := reverse.termination h
       simp [(go · (i+1) ⟨j-1, ·⟩), h]
     else simp [h]
     termination_by j - i
@@ -527,9 +529,8 @@ set_option linter.deprecated false in
       (H : ∀ k, as.toList.get? k = if i ≤ k ∧ k ≤ j then a.toList.get? k else a.toList.reverse.get? k)
       (k) : (reverse.loop as i ⟨j, hj⟩).toList.get? k = a.toList.reverse.get? k := by
     rw [reverse.loop]; dsimp; split <;> rename_i h₁
-    · have p := reverse.termination h₁
-      match j with | j+1 => ?_
-      simp only [Nat.add_sub_cancel] at p ⊢
+    · match j with | j+1 => ?_
+      simp only [Nat.add_sub_cancel]
       rw [(go · (i+1) j)]
       · rwa [Nat.add_right_comm i]
       · simp [size_swap, h₂]
@@ -1113,5 +1114,4 @@ theorem swap_comm (a : Array α) {i j : Fin a.size} : a.swap i j = a.swap j i :=
     · split <;> simp_all
     · split <;> simp_all
 
-
 end Array

src/Init/Data/BitVec/Basic.lean

@@ -174,8 +174,7 @@ theorem getElem_eq_testBit_toNat (x : BitVec w) (i : Nat) (h : i < w) :
   x[i] = x.toNat.testBit i := rfl
 
 theorem getLsbD_eq_getElem {x : BitVec w} {i : Nat} (h : i < w) :
-    x.getLsbD i = x[i] := by
-  simp [getLsbD, getElem_eq_testBit_toNat]
+    x.getLsbD i = x[i] := rfl
 
 end getElem
 
@@ -454,13 +453,15 @@ SMT-Lib name: `extract`.
 def extractLsb (hi lo : Nat) (x : BitVec n) : BitVec (hi - lo + 1) := extractLsb' lo _ x
 
 /--
-A version of `zeroExtend` that requires a proof, but is a noop.
+A version of `setWidth` that requires a proof, but is a noop.
 -/
-def zeroExtend' {n w : Nat} (le : n ≤ w) (x : BitVec n) : BitVec w :=
+def setWidth' {n w : Nat} (le : n ≤ w) (x : BitVec n) : BitVec w :=
   x.toNat#'(by
     apply Nat.lt_of_lt_of_le x.isLt
     exact Nat.pow_le_pow_of_le_right (by trivial) le)
 
+@[deprecated setWidth' (since := "2024-09-18"), inherit_doc setWidth'] abbrev zeroExtend' := @setWidth'
+
 /--
 `shiftLeftZeroExtend x n` returns `zeroExtend (w+n) x <<< n` without
 needing to compute `x % 2^(2+n)`.
@@ -473,22 +474,35 @@ def shiftLeftZeroExtend (msbs : BitVec w) (m : Nat) : BitVec (w + m) :=
   (msbs.toNat <<< m)#'(shiftLeftLt msbs.isLt m)
 
 /--
-Zero extend vector `x` of length `w` by adding zeros in the high bits until it has length `v`.
-If `v < w` then it truncates the high bits instead.
+Transform `x` of length `w` into a bitvector of length `v`, by either:
+- zero extending, that is, adding zeros in the high bits until it has length `v`, if `v > w`, or
+- truncating the high bits, if `v < w`.
 
 SMT-Lib name: `zero_extend`.
 -/
-def zeroExtend (v : Nat) (x : BitVec w) : BitVec v :=
+def setWidth (v : Nat) (x : BitVec w) : BitVec v :=
   if h : w ≤ v then
-    zeroExtend' h x
+    setWidth' h x
   else
     .ofNat v x.toNat
 
 /--
-Truncate the high bits of bitvector `x` of length `w`, resulting in a vector of length `v`.
-If `v > w` then it zero-extends the vector instead.
+Transform `x` of length `w` into a bitvector of length `v`, by either:
+- zero extending, that is, adding zeros in the high bits until it has length `v`, if `v > w`, or
+- truncating the high bits, if `v < w`.
+
+SMT-Lib name: `zero_extend`.
 -/
-abbrev truncate := @zeroExtend
+abbrev zeroExtend := @setWidth
+
+/--
+Transform `x` of length `w` into a bitvector of length `v`, by either:
+- zero extending, that is, adding zeros in the high bits until it has length `v`, if `v > w`, or
+- truncating the high bits, if `v < w`.
+
+SMT-Lib name: `zero_extend`.
+-/
+abbrev truncate := @setWidth
 
 /--
 Sign extend a vector of length `w`, extending with `i` additional copies of the most significant
@@ -639,7 +653,7 @@ input is on the left, so `0xAB#8 ++ 0xCD#8 = 0xABCD#16`.
 SMT-Lib name: `concat`.
 -/
 def append (msbs : BitVec n) (lsbs : BitVec m) : BitVec (n+m) :=
-  shiftLeftZeroExtend msbs m ||| zeroExtend' (Nat.le_add_left m n) lsbs
+  shiftLeftZeroExtend msbs m ||| setWidth' (Nat.le_add_left m n) lsbs
 
 instance : HAppend (BitVec w) (BitVec v) (BitVec (w + v)) := ⟨.append⟩
 

src/Init/Data/BitVec/Bitblast.lean

@@ -132,18 +132,18 @@ theorem toNat_add_of_and_eq_zero {x y : BitVec w} (h : x &&& y = 0#w) :
   simp [not_eq_true, carry_of_and_eq_zero h]
 
 /-- Carry function for bitwise addition. -/
-def adcb (x y c : Bool) : Bool × Bool := (atLeastTwo x y c, Bool.xor x (Bool.xor y c))
+def adcb (x y c : Bool) : Bool × Bool := (atLeastTwo x y c, x ^^ (y ^^ c))
 
 /-- Bitwise addition implemented via a ripple carry adder. -/
 def adc (x y : BitVec w) : Bool → Bool × BitVec w :=
   iunfoldr fun (i : Fin w) c => adcb (x.getLsbD i) (y.getLsbD i) c
 
 theorem getLsbD_add_add_bool {i : Nat} (i_lt : i < w) (x y : BitVec w) (c : Bool) :
-    getLsbD (x + y + zeroExtend w (ofBool c)) i =
-      Bool.xor (getLsbD x i) (Bool.xor (getLsbD y i) (carry i x y c)) := by
+    getLsbD (x + y + setWidth w (ofBool c)) i =
+      (getLsbD x i ^^ (getLsbD y i ^^ carry i x y c)) := by
   let ⟨x, x_lt⟩ := x
   let ⟨y, y_lt⟩ := y
-  simp only [getLsbD, toNat_add, toNat_zeroExtend, i_lt, toNat_ofFin, toNat_ofBool,
+  simp only [getLsbD, toNat_add, toNat_setWidth, i_lt, toNat_ofFin, toNat_ofBool,
     Nat.mod_add_mod, Nat.add_mod_mod]
   apply Eq.trans
   rw [← Nat.div_add_mod x (2^i), ← Nat.div_add_mod y (2^i)]
@@ -161,15 +161,15 @@ theorem getLsbD_add_add_bool {i : Nat} (i_lt : i < w) (x y : BitVec w) (c : Bool
 
 theorem getLsbD_add {i : Nat} (i_lt : i < w) (x y : BitVec w) :
     getLsbD (x + y) i =
-      Bool.xor (getLsbD x i) (Bool.xor (getLsbD y i) (carry i x y false)) := by
+      (getLsbD x i ^^ (getLsbD y i ^^ carry i x y false)) := by
   simpa using getLsbD_add_add_bool i_lt x y false
 
 theorem adc_spec (x y : BitVec w) (c : Bool) :
-    adc x y c = (carry w x y c, x + y + zeroExtend w (ofBool c)) := by
+    adc x y c = (carry w x y c, x + y + setWidth w (ofBool c)) := by
   simp only [adc]
   apply iunfoldr_replace
           (fun i => carry i x y c)
-          (x + y + zeroExtend w (ofBool c))
+          (x + y + setWidth w (ofBool c))
           c
   case init =>
     simp [carry, Nat.mod_one]
@@ -306,12 +306,12 @@ theorem mulRec_succ_eq (x y : BitVec w) (s : Nat) :
 Recurrence lemma: truncating to `i+1` bits and then zero extending to `w`
 equals truncating upto `i` bits `[0..i-1]`, and then adding the `i`th bit of `x`.
 -/
-theorem zeroExtend_truncate_succ_eq_zeroExtend_truncate_add_twoPow (x : BitVec w) (i : Nat) :
-    zeroExtend w (x.truncate (i + 1)) =
-      zeroExtend w (x.truncate i) + (x &&& twoPow w i) := by
+theorem setWidth_setWidth_succ_eq_setWidth_setWidth_add_twoPow (x : BitVec w) (i : Nat) :
+    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
-    simp only [getLsbD_zeroExtend, Fin.is_lt, decide_True, Bool.true_and, getLsbD_or, getLsbD_and]
+    simp only [getLsbD_setWidth, Fin.is_lt, decide_True, Bool.true_and, getLsbD_or, getLsbD_and]
     by_cases hik : i = k
     · subst hik
       simp
@@ -322,27 +322,32 @@ theorem zeroExtend_truncate_succ_eq_zeroExtend_truncate_add_twoPow (x : BitVec w
       · have hik'' : ¬ (k < i) := by omega
         simp [hik', hik'']
   · ext k
-    simp only [and_twoPow, getLsbD_and, getLsbD_zeroExtend, Fin.is_lt, decide_True, Bool.true_and,
+    simp only [and_twoPow, getLsbD_and, getLsbD_setWidth, Fin.is_lt, decide_True, Bool.true_and,
       getLsbD_zero, and_eq_false_imp, and_eq_true, decide_eq_true_eq, and_imp]
     by_cases hi : x.getLsbD i <;> simp [hi] <;> omega
 
+@[deprecated setWidth_setWidth_succ_eq_setWidth_setWidth_add_twoPow (since := "2024-09-18"),
+  inherit_doc setWidth_setWidth_succ_eq_setWidth_setWidth_add_twoPow]
+abbrev zeroExtend_truncate_succ_eq_zeroExtend_truncate_add_twoPow :=
+  @setWidth_setWidth_succ_eq_setWidth_setWidth_add_twoPow
+
 /--
 Recurrence lemma: multiplying `x` with the first `s` bits of `y` is the
 same as truncating `y` to `s` bits, then zero extending to the original length,
 and performing the multplication. -/
-theorem mulRec_eq_mul_signExtend_truncate (x y : BitVec w) (s : Nat) :
-    mulRec x y s = x * ((y.truncate (s + 1)).zeroExtend w) := by
+theorem mulRec_eq_mul_signExtend_setWidth (x y : BitVec w) (s : Nat) :
+    mulRec x y s = x * ((y.setWidth (s + 1)).setWidth w) := by
   induction s
   case zero =>
     simp only [mulRec_zero_eq, ofNat_eq_ofNat, Nat.reduceAdd]
     by_cases y.getLsbD 0
     case pos hy =>
-      simp only [hy, ↓reduceIte, truncate, zeroExtend_one_eq_ofBool_getLsb_zero,
+      simp only [hy, ↓reduceIte, setWidth_one_eq_ofBool_getLsb_zero,
         ofBool_true, ofNat_eq_ofNat]
-      rw [zeroExtend_ofNat_one_eq_ofNat_one_of_lt (by omega)]
+      rw [setWidth_ofNat_one_eq_ofNat_one_of_lt (by omega)]
       simp
     case neg hy =>
-      simp [hy, zeroExtend_one_eq_ofBool_getLsb_zero]
+      simp [hy, setWidth_one_eq_ofBool_getLsb_zero]
   case succ s' hs =>
     rw [mulRec_succ_eq, hs]
     have heq :
@@ -350,13 +355,16 @@ theorem mulRec_eq_mul_signExtend_truncate (x y : BitVec w) (s : Nat) :
         (x * (y &&& (BitVec.twoPow w (s' + 1)))) := by
       simp only [ofNat_eq_ofNat, and_twoPow]
       by_cases hy : y.getLsbD (s' + 1) <;> simp [hy]
-    rw [heq, ← BitVec.mul_add, ← zeroExtend_truncate_succ_eq_zeroExtend_truncate_add_twoPow]
+    rw [heq, ← BitVec.mul_add, ← setWidth_setWidth_succ_eq_setWidth_setWidth_add_twoPow]
+
+@[deprecated mulRec_eq_mul_signExtend_setWidth (since := "2024-09-18"),
+  inherit_doc mulRec_eq_mul_signExtend_setWidth]
+abbrev mulRec_eq_mul_signExtend_truncate := @mulRec_eq_mul_signExtend_setWidth
 
 theorem getLsbD_mul (x y : BitVec w) (i : Nat) :
     (x * y).getLsbD i = (mulRec x y w).getLsbD i := by
-  simp only [mulRec_eq_mul_signExtend_truncate]
-  rw [truncate, ← truncate_eq_zeroExtend, ← truncate_eq_zeroExtend,
-    truncate_truncate_of_le]
+  simp only [mulRec_eq_mul_signExtend_setWidth]
+  rw [setWidth_setWidth_of_le]
   · simp
   · omega
 
@@ -402,22 +410,22 @@ theorem shiftLeft_or_of_and_eq_zero {x : BitVec w₁} {y z : BitVec w₂}
 `shiftLeftRec x y n` shifts `x` to the left by the first `n` bits of `y`.
 -/
 theorem shiftLeftRec_eq {x : BitVec w₁} {y : BitVec w₂} {n : Nat} :
-    shiftLeftRec x y n = x <<< (y.truncate (n + 1)).zeroExtend w₂ := by
+    shiftLeftRec x y n = x <<< (y.setWidth (n + 1)).setWidth w₂ := by
   induction n generalizing x y
   case zero =>
     ext i
-    simp only [shiftLeftRec_zero, twoPow_zero, Nat.reduceAdd, truncate_one,
-      and_one_eq_zeroExtend_ofBool_getLsbD]
+    simp only [shiftLeftRec_zero, twoPow_zero, Nat.reduceAdd, setWidth_one,
+      and_one_eq_setWidth_ofBool_getLsbD]
   case succ n ih =>
     simp only [shiftLeftRec_succ, and_twoPow]
     rw [ih]
     by_cases h : y.getLsbD (n + 1)
     · simp only [h, ↓reduceIte]
-      rw [zeroExtend_truncate_succ_eq_zeroExtend_truncate_or_twoPow_of_getLsbD_true h,
+      rw [setWidth_setWidth_succ_eq_setWidth_setWidth_or_twoPow_of_getLsbD_true h,
         shiftLeft_or_of_and_eq_zero]
       simp [and_twoPow]
     · simp only [h, false_eq_true, ↓reduceIte, shiftLeft_zero']
-      rw [zeroExtend_truncate_succ_eq_zeroExtend_truncate_of_getLsbD_false (i := n + 1)]
+      rw [setWidth_setWidth_succ_eq_setWidth_setWidth_of_getLsbD_false (i := n + 1)]
       simp [h]
 
 /--
@@ -466,18 +474,18 @@ theorem sshiftRight'_or_of_and_eq_zero {x : BitVec w₁} {y z : BitVec w₂}
     toNat_add_of_and_eq_zero h, sshiftRight_add]
 
 theorem sshiftRightRec_eq (x : BitVec w₁) (y : BitVec w₂) (n : Nat) :
-    sshiftRightRec x y n = x.sshiftRight' ((y.truncate (n + 1)).zeroExtend w₂) := by
+    sshiftRightRec x y n = x.sshiftRight' ((y.setWidth (n + 1)).setWidth w₂) := by
   induction n generalizing x y
   case zero =>
     ext i
-    simp [twoPow_zero, Nat.reduceAdd, and_one_eq_zeroExtend_ofBool_getLsbD, truncate_one]
+    simp [twoPow_zero, Nat.reduceAdd, and_one_eq_setWidth_ofBool_getLsbD, setWidth_one]
   case succ n ih =>
     simp only [sshiftRightRec_succ_eq, and_twoPow, ih]
     by_cases h : y.getLsbD (n + 1)
-    · rw [zeroExtend_truncate_succ_eq_zeroExtend_truncate_or_twoPow_of_getLsbD_true h,
+    · rw [setWidth_setWidth_succ_eq_setWidth_setWidth_or_twoPow_of_getLsbD_true h,
         sshiftRight'_or_of_and_eq_zero (by simp [and_twoPow]), h]
       simp
-    · rw [zeroExtend_truncate_succ_eq_zeroExtend_truncate_of_getLsbD_false (i := n + 1)
+    · rw [setWidth_setWidth_succ_eq_setWidth_setWidth_of_getLsbD_false (i := n + 1)
         (by simp [h])]
       simp [h]
 
@@ -529,20 +537,20 @@ theorem ushiftRight'_or_of_and_eq_zero {x : BitVec w₁} {y z : BitVec w₂}
   simp [← add_eq_or_of_and_eq_zero _ _ h, toNat_add_of_and_eq_zero h, shiftRight_add]
 
 theorem ushiftRightRec_eq (x : BitVec w₁) (y : BitVec w₂) (n : Nat) :
-    ushiftRightRec x y n = x >>> (y.truncate (n + 1)).zeroExtend w₂ := by
+    ushiftRightRec x y n = x >>> (y.setWidth (n + 1)).setWidth w₂ := by
   induction n generalizing x y
   case zero =>
     ext i
     simp only [ushiftRightRec_zero, twoPow_zero, Nat.reduceAdd,
-      and_one_eq_zeroExtend_ofBool_getLsbD, truncate_one]
+      and_one_eq_setWidth_ofBool_getLsbD, setWidth_one]
   case succ n ih =>
     simp only [ushiftRightRec_succ, and_twoPow]
     rw [ih]
     by_cases h : y.getLsbD (n + 1) <;> simp only [h, ↓reduceIte]
-    · rw [zeroExtend_truncate_succ_eq_zeroExtend_truncate_or_twoPow_of_getLsbD_true h,
+    · rw [setWidth_setWidth_succ_eq_setWidth_setWidth_or_twoPow_of_getLsbD_true h,
         ushiftRight'_or_of_and_eq_zero]
       simp [and_twoPow]
-    · simp [zeroExtend_truncate_succ_eq_zeroExtend_truncate_of_getLsbD_false, h]
+    · simp [setWidth_setWidth_succ_eq_setWidth_setWidth_of_getLsbD_false, h]
 
 /--
 Show that `x >>> y` can be written in terms of `ushiftRightRec`.

src/Init/Data/BitVec/Folds.lean

@@ -48,7 +48,7 @@ private theorem iunfoldr.eq_test
     simp only [init, eq_nil]
   case step =>
     intro i
-    simp_all [truncate_succ]
+    simp_all [setWidth_succ]
 
 theorem iunfoldr_getLsbD' {f : Fin w → α → α × Bool} (state : Nat → α)
     (ind : ∀(i : Fin w), (f i (state i.val)).fst = state (i.val+1)) :

src/Init/Data/BitVec/Lemmas.lean

@@ -234,6 +234,15 @@ theorem ofBool_eq_iff_eq : ∀ {b b' : Bool}, BitVec.ofBool b = BitVec.ofBool b'
 
 @[simp] theorem not_ofBool : ~~~ (ofBool b) = ofBool (!b) := by cases b <;> rfl
 
+@[simp] theorem ofBool_and_ofBool : ofBool b &&& ofBool b' = ofBool (b && b') := by
+  cases b <;> cases b' <;> rfl
+
+@[simp] theorem ofBool_or_ofBool : ofBool b ||| ofBool b' = ofBool (b || b') := by
+  cases b <;> cases b' <;> rfl
+
+@[simp] theorem ofBool_xor_ofBool : ofBool b ^^^ ofBool b' = ofBool (b ^^ b') := by
+  cases b <;> cases b' <;> rfl
+
 @[simp, bv_toNat] theorem toNat_ofFin (x : Fin (2^n)) : (BitVec.ofFin x).toNat = x.val := rfl
 
 @[simp] theorem toNat_ofNatLt (x : Nat) (p : x < 2^w) : (x#'p).toNat = x := rfl
@@ -279,21 +288,22 @@ private theorem lt_two_pow_of_le {x m n : Nat} (lt : x < 2 ^ m) (le : m ≤ n) :
 @[simp] theorem getElem_zero_ofNat_one (h : 0 < w) : (BitVec.ofNat w 1)[0] = true := by
   simp [getElem_eq_testBit_toNat, h]
 
-@[simp] theorem getElem?_zero_ofNat_zero : (BitVec.ofNat (w+1) 0)[0]? = some false := by
-  simp [getElem?_eq_getElem]
+theorem getElem?_zero_ofNat_zero : (BitVec.ofNat (w+1) 0)[0]? = some false := by
+  simp
 
-@[simp] theorem getElem?_zero_ofNat_one : (BitVec.ofNat (w+1) 1)[0]? = some true := by
-  simp [getElem?_eq_getElem]
+theorem getElem?_zero_ofNat_one : (BitVec.ofNat (w+1) 1)[0]? = some true := by
+  simp
 
-@[simp] theorem getElem?_zero_ofBool (b : Bool) : (ofBool b)[0]? = some b := by
+-- This does not need to be a `@[simp]` theorem as it is already handled by `getElem?_eq_getElem`.
+theorem getElem?_zero_ofBool (b : Bool) : (ofBool b)[0]? = some b := by
   simp [ofBool, cond_eq_if]
   split <;> simp_all
 
 @[simp] theorem getElem_zero_ofBool (b : Bool) : (ofBool b)[0] = b := by
   rw [getElem_eq_iff, getElem?_zero_ofBool]
 
-@[simp] theorem getElem?_succ_ofBool (b : Bool) (i : Nat) : (ofBool b)[i + 1]? = none := by
-  simp [ofBool]
+theorem getElem?_succ_ofBool (b : Bool) (i : Nat) : (ofBool b)[i + 1]? = none := by
+  simp
 
 @[simp]
 theorem getLsbD_ofBool (b : Bool) (i : Nat) : (ofBool b).getLsbD i = ((i = 0) && b) := by
@@ -438,46 +448,46 @@ theorem toInt_pos_iff {w : Nat} {x : BitVec w} :
     0 ≤ BitVec.toInt x ↔ 2 * x.toNat < 2 ^ w := by
   simp [toInt_eq_toNat_cond]; omega
 
-/-! ### zeroExtend and truncate -/
+/-! ### setWidth, zeroExtend and truncate -/
 
-theorem truncate_eq_zeroExtend {v : Nat} {x : BitVec w} :
-  truncate v x = zeroExtend v x := rfl
+@[simp]
+theorem truncate_eq_setWidth {v : Nat} {x : BitVec w} :
+  truncate v x = setWidth v x := rfl
 
-@[simp, bv_toNat] theorem toNat_zeroExtend' {m n : Nat} (p : m ≤ n) (x : BitVec m) :
-    (zeroExtend' p x).toNat = x.toNat := by
-  simp [zeroExtend']
+@[simp]
+theorem zeroExtend_eq_setWidth {v : Nat} {x : BitVec w} :
+  zeroExtend v x = setWidth v x := rfl
 
-@[bv_toNat] theorem toNat_zeroExtend (i : Nat) (x : BitVec n) :
-    BitVec.toNat (zeroExtend i x) = x.toNat % 2^i := by
+@[simp, bv_toNat] theorem toNat_setWidth' {m n : Nat} (p : m ≤ n) (x : BitVec m) :
+    (setWidth' p x).toNat = x.toNat := by
+  simp [setWidth']
+
+@[simp, bv_toNat] theorem toNat_setWidth (i : Nat) (x : BitVec n) :
+    BitVec.toNat (setWidth i x) = x.toNat % 2^i := by
   let ⟨x, lt_n⟩ := x
-  simp only [zeroExtend]
+  simp only [setWidth]
   if n_le_i : n ≤ i then
     have x_lt_two_i : x < 2 ^ i := lt_two_pow_of_le lt_n n_le_i
     simp [n_le_i, Nat.mod_eq_of_lt, x_lt_two_i]
   else
     simp [n_le_i, toNat_ofNat]
 
-theorem zeroExtend'_eq {x : BitVec w} (h : w ≤ v) : x.zeroExtend' h = x.zeroExtend v := by
+theorem setWidth'_eq {x : BitVec w} (h : w ≤ v) : x.setWidth' h = x.setWidth v := by
   apply eq_of_toNat_eq
-  rw [toNat_zeroExtend, toNat_zeroExtend']
+  rw [toNat_setWidth, toNat_setWidth']
   rw [Nat.mod_eq_of_lt]
   exact Nat.lt_of_lt_of_le x.isLt (Nat.pow_le_pow_right (Nat.zero_lt_two) h)
 
-@[simp, bv_toNat] theorem toNat_truncate (x : BitVec n) : (truncate i x).toNat = x.toNat % 2^i :=
-  toNat_zeroExtend i x
-
-@[simp] theorem zeroExtend_eq (x : BitVec n) : zeroExtend n x = x := by
+@[simp] theorem setWidth_eq (x : BitVec n) : setWidth n x = x := by
   apply eq_of_toNat_eq
   let ⟨x, lt_n⟩ := x
-  simp [truncate, zeroExtend]
+  simp [setWidth]
 
-@[simp] theorem zeroExtend_zero (m n : Nat) : zeroExtend m 0#n = 0#m := by
+@[simp] theorem setWidth_zero (m n : Nat) : setWidth m 0#n = 0#m := by
   apply eq_of_toNat_eq
-  simp [toNat_zeroExtend]
+  simp [toNat_setWidth]
 
-theorem truncate_eq (x : BitVec n) : truncate n x = x := zeroExtend_eq x
-
-@[simp] theorem ofNat_toNat (m : Nat) (x : BitVec n) : BitVec.ofNat m x.toNat = truncate m x := by
+@[simp] theorem ofNat_toNat (m : Nat) (x : BitVec n) : BitVec.ofNat m x.toNat = setWidth m x := by
   apply eq_of_toNat_eq
   simp
 
@@ -496,33 +506,33 @@ theorem nat_eq_toNat {x : BitVec w} {y : Nat}
   rw [@eq_comm _ _ x.toNat]
   apply toNat_eq_nat
 
-theorem getElem_zeroExtend' (x : BitVec w) (i : Nat) (h : w ≤ v) (hi : i < v) :
-    (zeroExtend' h x)[i] = x.getLsbD i := by
-  rw [getElem_eq_testBit_toNat, toNat_zeroExtend', getLsbD]
+theorem getElem_setWidth' (x : BitVec w) (i : Nat) (h : w ≤ v) (hi : i < v) :
+    (setWidth' h x)[i] = x.getLsbD i := by
+  rw [getElem_eq_testBit_toNat, toNat_setWidth', getLsbD]
 
-theorem getElem_zeroExtend (m : Nat) (x : BitVec n) (i : Nat) (h : i < m) :
-    (zeroExtend m x)[i] = x.getLsbD i := by
-  rw [zeroExtend]
+theorem getElem_setWidth (m : Nat) (x : BitVec n) (i : Nat) (h : i < m) :
+    (setWidth m x)[i] = x.getLsbD i := by
+  rw [setWidth]
   split
-  · rw [getElem_zeroExtend']
+  · rw [getElem_setWidth']
   · simp [getElem_eq_testBit_toNat, getLsbD]
     omega
 
-theorem getElem?_zeroExtend' (x : BitVec w) (i : Nat) (h : w ≤ v) :
-    (zeroExtend' h x)[i]? = if i < v then some (x.getLsbD i) else none := by
-  simp [getElem?_eq, getElem_zeroExtend']
+theorem getElem?_setWidth' (x : BitVec w) (i : Nat) (h : w ≤ v) :
+    (setWidth' h x)[i]? = if i < v then some (x.getLsbD i) else none := by
+  simp [getElem?_eq, getElem_setWidth']
 
-theorem getElem?_zeroExtend (m : Nat) (x : BitVec n) (i : Nat) :
-    (x.zeroExtend m)[i]? = if i < m then some (x.getLsbD i) else none := by
-  simp [getElem?_eq, getElem_zeroExtend]
+theorem getElem?_setWidth (m : Nat) (x : BitVec n) (i : Nat) :
+    (x.setWidth m)[i]? = if i < m then some (x.getLsbD i) else none := by
+  simp [getElem?_eq, getElem_setWidth]
 
-@[simp] theorem getLsbD_zeroExtend' (ge : m ≥ n) (x : BitVec n) (i : Nat) :
-    getLsbD (zeroExtend' ge x) i = getLsbD x i := by
-  simp [getLsbD, toNat_zeroExtend']
+@[simp] theorem getLsbD_setWidth' (ge : m ≥ n) (x : BitVec n) (i : Nat) :
+    getLsbD (setWidth' ge x) i = getLsbD x i := by
+  simp [getLsbD, toNat_setWidth']
 
-@[simp] theorem getMsbD_zeroExtend' (ge : m ≥ n) (x : BitVec n) (i : Nat) :
-    getMsbD (zeroExtend' ge x) i = (decide (i ≥ m - n) && getMsbD x (i - (m - n))) := by
-  simp only [getMsbD, getLsbD_zeroExtend', gt_iff_lt]
+@[simp] theorem getMsbD_setWidth' (ge : m ≥ n) (x : BitVec n) (i : Nat) :
+    getMsbD (setWidth' ge x) i = (decide (i ≥ m - n) && getMsbD x (i - (m - n))) := by
+  simp only [getMsbD, getLsbD_setWidth', gt_iff_lt]
   by_cases h₁ : decide (i < m) <;> by_cases h₂ : decide (i ≥ m - n) <;> by_cases h₃ : decide (i - (m - n) < n) <;>
     by_cases h₄ : n - 1 - (i - (m - n)) = m - 1 - i
   all_goals
@@ -533,15 +543,15 @@ theorem getElem?_zeroExtend (m : Nat) (x : BitVec n) (i : Nat) :
     (try apply (getLsbD_ge _ _ _).symm) <;>
     omega
 
-@[simp] theorem getLsbD_zeroExtend (m : Nat) (x : BitVec n) (i : Nat) :
-    getLsbD (zeroExtend m x) i = (decide (i < m) && getLsbD x i) := by
-  simp [getLsbD, toNat_zeroExtend, Nat.testBit_mod_two_pow]
+@[simp] theorem getLsbD_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]
 
-@[simp] theorem getMsbD_zeroExtend_add {x : BitVec w} (h : k ≤ i) :
-    (x.zeroExtend (w + k)).getMsbD i = x.getMsbD (i - k) := by
+@[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
   · subst h; simp [of_length_zero]
-  simp only [getMsbD, getLsbD_zeroExtend]
+  simp only [getMsbD, getLsbD_setWidth]
   by_cases h₁ : i < w + k <;> by_cases h₂ : i - k < w <;> by_cases h₃ : w + k - 1 - i < w + k
     <;> simp [h₁, h₂, h₃]
   · congr 1
@@ -549,87 +559,60 @@ theorem getElem?_zeroExtend (m : Nat) (x : BitVec n) (i : Nat) :
   all_goals (first | apply getLsbD_ge | apply Eq.symm; apply getLsbD_ge)
     <;> omega
 
-@[simp]
-theorem getElem_truncate (m : Nat) (x : BitVec n) (i : Nat) (hi : i < m) :
-    (truncate m x)[i] = x.getLsbD i := by
-  simp only [getElem_zeroExtend]
-
-theorem getElem?_truncate (m : Nat) (x : BitVec n) (i : Nat) :
-    (truncate m x)[i]? = if i < m then some (x.getLsbD i) else none :=
-  getElem?_zeroExtend m x i
-
-theorem getLsbD_truncate (m : Nat) (x : BitVec n) (i : Nat) :
-    getLsbD (truncate m x) i = (decide (i < m) && getLsbD x i) :=
-  getLsbD_zeroExtend m x i
-
-theorem msb_truncate (x : BitVec w) : (x.truncate (k + 1)).msb = x.getLsbD k := by
-  simp [BitVec.msb, getMsbD]
-
-@[simp] theorem cast_zeroExtend (h : v = v') (x : BitVec w) :
-    cast h (zeroExtend v x) = zeroExtend v' x := by
+@[simp] theorem cast_setWidth (h : v = v') (x : BitVec w) :
+    cast h (setWidth v x) = setWidth v' x := by
   subst h
   ext
   simp
 
-@[simp] theorem cast_truncate (h : v = v') (x : BitVec w) :
-    cast h (truncate v x) = truncate v' x := by
-  subst h
-  ext
-  simp
-
-@[simp] theorem zeroExtend_zeroExtend_of_le (x : BitVec w) (h : k ≤ l) :
-    (x.zeroExtend l).zeroExtend k = x.zeroExtend k := by
+@[simp] theorem setWidth_setWidth_of_le (x : BitVec w) (h : k ≤ l) :
+    (x.setWidth l).setWidth k = x.setWidth k := by
   ext i
-  simp only [getLsbD_zeroExtend, Fin.is_lt, decide_True, Bool.true_and]
+  simp only [getLsbD_setWidth, Fin.is_lt, decide_True, Bool.true_and]
   have p := lt_of_getLsbD (x := x) (i := i)
   revert p
   cases getLsbD x i <;> simp; omega
 
-@[simp] theorem truncate_truncate_of_le (x : BitVec w) (h : k ≤ l) :
-    (x.truncate l).truncate k = x.truncate k :=
-  zeroExtend_zeroExtend_of_le x h
-
-/-- Truncating by the bitwidth has no effect. -/
--- This doesn't need to be a `@[simp]` lemma, as `zeroExtend_eq` applies.
-theorem truncate_eq_self {x : BitVec w} : x.truncate w = x := zeroExtend_eq _
-
-@[simp] theorem truncate_cast {h : w = v} : (cast h x).truncate k = x.truncate k := by
+@[simp] theorem setWidth_cast {h : w = v} : (cast h x).setWidth k = x.setWidth k := by
   apply eq_of_getLsbD_eq
   simp
 
-theorem msb_zeroExtend (x : BitVec w) : (x.zeroExtend v).msb = (decide (0 < v) && x.getLsbD (v - 1)) := by
+theorem msb_setWidth (x : BitVec w) : (x.setWidth v).msb = (decide (0 < v) && x.getLsbD (v - 1)) := by
   rw [msb_eq_getLsbD_last]
-  simp only [getLsbD_zeroExtend]
+  simp only [getLsbD_setWidth]
   cases getLsbD x (v - 1) <;> simp; omega
 
-theorem msb_zeroExtend' (x : BitVec w) (h : w ≤ v) : (x.zeroExtend' h).msb = (decide (0 < v) && x.getLsbD (v - 1)) := by
-  rw [zeroExtend'_eq, msb_zeroExtend]
+theorem msb_setWidth' (x : BitVec w) (h : w ≤ v) : (x.setWidth' h).msb = (decide (0 < v) && x.getLsbD (v - 1)) := by
+  rw [setWidth'_eq, msb_setWidth]
+
+theorem msb_setWidth'' (x : BitVec w) : (x.setWidth (k + 1)).msb = x.getLsbD k := by
+  simp [BitVec.msb, getMsbD]
 
 /-- zero extending a bitvector to width 1 equals the boolean of the lsb. -/
-theorem zeroExtend_one_eq_ofBool_getLsb_zero (x : BitVec w) :
-    x.zeroExtend 1 = BitVec.ofBool (x.getLsbD 0) := by
+theorem setWidth_one_eq_ofBool_getLsb_zero (x : BitVec w) :
+    x.setWidth 1 = BitVec.ofBool (x.getLsbD 0) := by
   ext i
-  simp [getLsbD_zeroExtend, Fin.fin_one_eq_zero i]
+  simp [getLsbD_setWidth, Fin.fin_one_eq_zero i]
 
 /-- Zero extending `1#v` to `1#w` equals `1#w` when `v > 0`. -/
-theorem zeroExtend_ofNat_one_eq_ofNat_one_of_lt {v w : Nat} (hv : 0 < v) :
-    (BitVec.ofNat v 1).zeroExtend w = BitVec.ofNat w 1 := by
+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, hilt⟩
-  simp only [getLsbD_zeroExtend, hilt, decide_True, getLsbD_ofNat, Bool.true_and,
+  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₁
   omega
 
 /-- Truncating to width 1 produces a bitvector equal to the least significant bit. -/
-theorem truncate_one {x : BitVec w} :
-    x.truncate 1 = ofBool (x.getLsbD 0) := by
+theorem setWidth_one {x : BitVec w} :
+    x.setWidth 1 = ofBool (x.getLsbD 0) := by
   ext i
   simp [show i = 0 by omega]
 
-@[simp] theorem truncate_ofNat_of_le (h : v ≤ w) (x : Nat) : truncate v (BitVec.ofNat w x) = BitVec.ofNat v x := by
+@[simp] theorem setWidth_ofNat_of_le (h : v ≤ w) (x : Nat) : setWidth v (BitVec.ofNat w x) = BitVec.ofNat v x := by
   apply BitVec.eq_of_toNat_eq
-  simp only [toNat_truncate, toNat_ofNat]
+  simp only [toNat_setWidth, toNat_ofNat]
   rw [Nat.mod_mod_of_dvd]
   exact Nat.pow_dvd_pow_iff_le_right'.mpr h
 
@@ -710,8 +693,8 @@ theorem extractLsb'_eq_extractLsb {w : Nat} (x : BitVec w) (start len : Nat) (h
 @[simp] theorem msb_or {x y : BitVec w} : (x ||| y).msb = (x.msb || y.msb) := by
   simp [BitVec.msb]
 
-@[simp] theorem truncate_or {x y : BitVec w} :
-    (x ||| y).truncate k = x.truncate k ||| y.truncate k := by
+@[simp] theorem setWidth_or {x y : BitVec w} :
+    (x ||| y).setWidth k = x.setWidth k ||| y.setWidth k := by
   ext
   simp
 
@@ -751,8 +734,8 @@ instance : Std.Commutative (fun (x y : BitVec w) => x ||| y) := ⟨BitVec.or_com
 @[simp] theorem msb_and {x y : BitVec w} : (x &&& y).msb = (x.msb && y.msb) := by
   simp [BitVec.msb]
 
-@[simp] theorem truncate_and {x y : BitVec w} :
-    (x &&& y).truncate k = x.truncate k &&& y.truncate k := by
+@[simp] theorem setWidth_and {x y : BitVec w} :
+    (x &&& y).setWidth k = x.setWidth k &&& y.setWidth k := by
   ext
   simp
 
@@ -779,24 +762,24 @@ instance : Std.Commutative (fun (x y : BitVec w) => x &&& y) := ⟨BitVec.and_co
   exact (Nat.mod_eq_of_lt <| Nat.xor_lt_two_pow x.isLt y.isLt).symm
 
 @[simp] theorem getLsbD_xor {x y : BitVec v} :
-    (x ^^^ y).getLsbD i = (xor (x.getLsbD i) (y.getLsbD i)) := by
+    (x ^^^ y).getLsbD i = ((x.getLsbD i) ^^ (y.getLsbD i)) := by
   rw [← testBit_toNat, getLsbD, getLsbD]
   simp
 
 @[simp] theorem getMsbD_xor {x y : BitVec w} :
-    (x ^^^ y).getMsbD i = (xor (x.getMsbD i) (y.getMsbD i)) := by
+    (x ^^^ y).getMsbD i = (x.getMsbD i ^^ y.getMsbD i) := by
   simp only [getMsbD]
   by_cases h : i < w <;> simp [h]
 
-@[simp] theorem getElem_xor {x y : BitVec w} {i : Nat} (h : i < w) : (x ^^^ y)[i] = (xor x[i] y[i]) := by
+@[simp] theorem getElem_xor {x y : BitVec w} {i : Nat} (h : i < w) : (x ^^^ y)[i] = (x[i] ^^ y[i]) := by
   simp [getElem_eq_testBit_toNat]
 
 @[simp] theorem msb_xor {x y : BitVec w} :
-    (x ^^^ y).msb = (xor x.msb y.msb) := by
+    (x ^^^ y).msb = (x.msb ^^ y.msb) := by
   simp [BitVec.msb]
 
-@[simp] theorem truncate_xor {x y : BitVec w} :
-    (x ^^^ y).truncate k = x.truncate k ^^^ y.truncate k := by
+@[simp] theorem setWidth_xor {x y : BitVec w} :
+    (x ^^^ y).setWidth k = x.setWidth k ^^^ y.setWidth k := by
   ext
   simp
 
@@ -850,8 +833,8 @@ theorem not_def {x : BitVec v} : ~~~x = allOnes v ^^^ x := rfl
   rw [Nat.testBit_two_pow_sub_succ x.isLt]
   simp [h]
 
-@[simp] theorem truncate_not {x : BitVec w} (h : k ≤ w) :
-    (~~~x).truncate k = ~~~(x.truncate k) := by
+@[simp] theorem setWidth_not {x : BitVec w} (h : k ≤ w) :
+    (~~~x).setWidth k = ~~~(x.setWidth k) := by
   ext
   simp [h]
   omega
@@ -939,9 +922,9 @@ theorem shiftLeft_or_distrib (x y : BitVec w) (n : Nat) :
     <;> omega
 
 theorem shiftLeftZeroExtend_eq {x : BitVec w} :
-    shiftLeftZeroExtend x n = zeroExtend (w+n) x <<< n := by
+    shiftLeftZeroExtend x n = setWidth (w+n) x <<< n := by
   apply eq_of_toNat_eq
-  rw [shiftLeftZeroExtend, zeroExtend]
+  rw [shiftLeftZeroExtend, setWidth]
   split
   · simp
     rw [Nat.mod_eq_of_lt]
@@ -952,7 +935,7 @@ theorem shiftLeftZeroExtend_eq {x : BitVec w} :
 @[simp] theorem getLsbD_shiftLeftZeroExtend (x : BitVec m) (n : Nat) :
     getLsbD (shiftLeftZeroExtend x n) i = ((! decide (i < n)) && getLsbD x (i - n)) := by
   rw [shiftLeftZeroExtend_eq]
-  simp only [getLsbD_shiftLeft, getLsbD_zeroExtend]
+  simp only [getLsbD_shiftLeft, getLsbD_setWidth]
   cases h₁ : decide (i < n) <;> cases h₂ : decide (i - n < m + n) <;> cases h₃ : decide (i < m + n)
     <;> simp_all
     <;> (rw [getLsbD_ge]; omega)
@@ -1195,15 +1178,15 @@ 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_not_zeroExtend_not_of_msb_false {x : BitVec w} {v : Nat} (hmsb : x.msb = false) :
-    x.signExtend v = x.zeroExtend v := by
+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
-  · simp only [signExtend, getLsbD, getLsbD_zeroExtend, hv, decide_True, Bool.true_and, toNat_ofInt,
+  · simp only [signExtend, getLsbD, getLsbD_setWidth, hv, decide_True, Bool.true_and, toNat_ofInt,
       BitVec.toInt_eq_msb_cond, hmsb, ↓reduceIte, reduceCtorEq]
     rw [Int.ofNat_mod_ofNat, Int.toNat_ofNat, Nat.testBit_mod_two_pow]
     simp [BitVec.testBit_toNat]
-  · simp only [getLsbD_zeroExtend, hv, decide_False, Bool.false_and]
+  · simp only [getLsbD_setWidth, hv, decide_False, Bool.false_and]
     apply getLsbD_ge
     omega
 
@@ -1211,11 +1194,11 @@ theorem signExtend_eq_not_zeroExtend_not_of_msb_false {x : BitVec w} {v : Nat} (
 The sign extension is a bitwise not, followed by a zero extend, followed by another bitwise not
 when `msb = true`. The double bitwise not ensures that the high bits are '1',
 and the lower bits are preserved. -/
-theorem signExtend_eq_not_zeroExtend_not_of_msb_true {x : BitVec w} {v : Nat} (hmsb : x.msb = true) :
-    x.signExtend v = ~~~((~~~x).zeroExtend v) := by
+theorem signExtend_eq_not_setWidth_not_of_msb_true {x : BitVec w} {v : Nat} (hmsb : x.msb = true) :
+    x.signExtend v = ~~~((~~~x).setWidth v) := by
   apply BitVec.eq_of_toNat_eq
   simp only [signExtend, BitVec.toInt_eq_msb_cond, toNat_ofInt, toNat_not,
-    toNat_truncate, hmsb, ↓reduceIte]
+    toNat_setWidth, hmsb, ↓reduceIte]
   norm_cast
   rw [Int.ofNat_sub_ofNat_of_lt, Int.negSucc_emod]
   simp only [Int.natAbs_ofNat, Nat.succ_eq_add_one]
@@ -1231,27 +1214,27 @@ theorem signExtend_eq_not_zeroExtend_not_of_msb_true {x : BitVec w} {v : Nat} (h
 @[simp] 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_not_zeroExtend_not_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_zeroExtend_not_of_msb_true hmsb]
+  · rw [signExtend_eq_not_setWidth_not_of_msb_true hmsb]
     by_cases (i < v) <;> by_cases (i < w) <;> simp_all <;> omega
 
 /-- Sign extending to a width smaller than the starting width is a truncation. -/
-theorem signExtend_eq_truncate_of_lt (x : BitVec w) {v : Nat} (hv : v ≤ w):
-  x.signExtend v = x.truncate v := by
+theorem signExtend_eq_setWidth_of_lt (x : BitVec w) {v : Nat} (hv : v ≤ w):
+  x.signExtend v = x.setWidth v := by
   ext i
-  simp only [getLsbD_signExtend, Fin.is_lt, decide_True, Bool.true_and, getLsbD_zeroExtend,
+  simp only [getLsbD_signExtend, Fin.is_lt, decide_True, Bool.true_and, getLsbD_setWidth,
     ite_eq_left_iff, Nat.not_lt]
   omega
 
 /-- Sign extending to the same bitwidth is a no op. -/
 theorem signExtend_eq (x : BitVec w) : x.signExtend w = x := by
-  rw [signExtend_eq_truncate_of_lt _ (Nat.le_refl _), truncate_eq]
+  rw [signExtend_eq_setWidth_of_lt _ (Nat.le_refl _), setWidth_eq]
 
 /-! ### append -/
 
 theorem append_def (x : BitVec v) (y : BitVec w) :
-    x ++ y = (shiftLeftZeroExtend x w ||| zeroExtend' (Nat.le_add_left w v) y) := rfl
+    x ++ y = (shiftLeftZeroExtend x w ||| setWidth' (Nat.le_add_left w v) y) := rfl
 
 @[simp] theorem toNat_append (x : BitVec m) (y : BitVec n) :
     (x ++ y).toNat = x.toNat <<< n ||| y.toNat :=
@@ -1259,7 +1242,7 @@ theorem append_def (x : BitVec v) (y : BitVec w) :
 
 @[simp] theorem getLsbD_append {x : BitVec n} {y : BitVec m} :
     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_zeroExtend']
+  simp only [append_def, getLsbD_or, getLsbD_shiftLeftZeroExtend, getLsbD_setWidth']
   by_cases h : i < m
   · simp [h]
   · simp [h]; simp_all
@@ -1274,7 +1257,7 @@ theorem append_def (x : BitVec v) (y : BitVec w) :
 theorem msb_append {x : BitVec w} {y : BitVec v} :
     (x ++ y).msb = bif (w == 0) then (y.msb) else (x.msb) := by
   rw [← append_eq, append]
-  simp [msb_zeroExtend']
+  simp [msb_setWidth']
   by_cases h : w = 0
   · subst h
     simp [BitVec.msb, getMsbD]
@@ -1309,11 +1292,11 @@ theorem msb_append {x : BitVec w} {y : BitVec v} :
   ext
   simp
 
-theorem truncate_append {x : BitVec w} {y : BitVec v} :
-    (x ++ y).truncate k = if h : k ≤ v then y.truncate k else (x.truncate (k - v) ++ y).cast (by omega) := by
+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
   apply eq_of_getLsbD_eq
   intro i
-  simp only [getLsbD_zeroExtend, Fin.is_lt, decide_True, getLsbD_append, Bool.true_and]
+  simp only [getLsbD_setWidth, Fin.is_lt, decide_True, getLsbD_append, Bool.true_and]
   split
   · have t : i < v := by omega
     simp [t]
@@ -1322,11 +1305,11 @@ theorem truncate_append {x : BitVec w} {y : BitVec v} :
     · have t' : i - v < k - v := by omega
       simp [t, t']
 
-@[simp] theorem truncate_append_of_eq {x : BitVec v} {y : BitVec w} (h : w' = w) : truncate (v' + w') (x ++ y) = truncate v' x ++ truncate w' y := by
+@[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
-  simp only [getLsbD_zeroExtend, Fin.is_lt, decide_True, getLsbD_append, cond_eq_if,
-    decide_eq_true_eq, Bool.true_and, zeroExtend_eq]
+  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
   · simp_all only [Bool.iff_and_self, decide_eq_true_eq]
@@ -1334,8 +1317,8 @@ theorem truncate_append {x : BitVec w} {y : BitVec v} :
     have := BitVec.lt_of_getLsbD h
     omega
 
-@[simp] theorem truncate_cons {x : BitVec w} : (cons a x).truncate w = x := by
-  simp [cons, truncate_append]
+@[simp] theorem setWidth_cons {x : BitVec w} : (cons a x).setWidth w = x := by
+  simp [cons, setWidth_append]
 
 @[simp] theorem not_append {x : BitVec w} {y : BitVec v} : ~~~ (x ++ y) = (~~~ x) ++ (~~~ y) := by
   ext i
@@ -1422,18 +1405,18 @@ theorem toNat_cons' {x : BitVec w} :
 @[simp] theorem getMsbD_cons_succ : (cons a x).getMsbD (i + 1) = x.getMsbD i := by
   simp [cons, Nat.le_add_left 1 i]
 
-theorem truncate_succ (x : BitVec w) :
-    truncate (i+1) x = cons (getLsbD x i) (truncate i x) := by
+theorem setWidth_succ (x : BitVec w) :
+    setWidth (i+1) x = cons (getLsbD x i) (setWidth i x) := by
   apply eq_of_getLsbD_eq
   intro j
-  simp only [getLsbD_truncate, getLsbD_cons, j.isLt, decide_True, Bool.true_and]
+  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.val < i := Nat.lt_of_le_of_ne (Nat.le_of_succ_le_succ j.isLt) j_eq
     simp [j_eq, j_lt]
 
-theorem eq_msb_cons_truncate (x : BitVec (w+1)) : x = (cons x.msb (x.truncate w)) := by
+theorem eq_msb_cons_setWidth (x : BitVec (w+1)) : x = (cons x.msb (x.setWidth w)) := by
   ext i
   simp
   split <;> rename_i h
@@ -1447,15 +1430,18 @@ theorem eq_msb_cons_truncate (x : BitVec (w+1)) : x = (cons x.msb (x.truncate w)
 
 @[simp] theorem cons_or_cons (x y : BitVec w) (a b : Bool) :
     (cons a x) ||| (cons b y) = cons (a || b) (x ||| y) := by
-  ext i; cases i using Fin.succRecOn <;> simp <;> split <;> rfl
+  ext i
+  simp [cons]
 
 @[simp] theorem cons_and_cons (x y : BitVec w) (a b : Bool) :
     (cons a x) &&& (cons b y) = cons (a && b) (x &&& y) := by
-  ext i; cases i using Fin.succRecOn <;> simp <;> split <;> rfl
+  ext i
+  simp [cons]
 
 @[simp] theorem cons_xor_cons (x y : BitVec w) (a b : Bool) :
-    (cons a x) ^^^ (cons b y) = cons (xor a b) (x ^^^ y) := by
-  ext i; cases i using Fin.succRecOn <;> simp <;> split <;> rfl
+    (cons a x) ^^^ (cons b y) = cons (a ^^ b) (x ^^^ y) := by
+  ext i
+  simp [cons]
 
 /-! ### concat -/
 
@@ -1493,7 +1479,7 @@ theorem getLsbD_concat (x : BitVec w) (b : Bool) (i : Nat) :
   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) (xor a b) := by
+    (concat x a) ^^^ (concat y b) = concat (x ^^^ y) (a ^^ b) := by
   ext i; cases i using Fin.succRecOn <;> simp
 
 /-! ### add -/
@@ -1511,7 +1497,8 @@ Definition of bitvector addition as a nat.
   x + .ofFin y = .ofFin (x.toFin + y) := rfl
 
 theorem ofNat_add {n} (x y : Nat) : BitVec.ofNat n (x + y) = BitVec.ofNat n x + BitVec.ofNat n y := by
-  apply eq_of_toNat_eq ; simp [BitVec.ofNat]
+  apply eq_of_toNat_eq
+  simp [BitVec.ofNat, Fin.ofNat'_add]
 
 theorem ofNat_add_ofNat {n} (x y : Nat) : BitVec.ofNat n x + BitVec.ofNat n y = BitVec.ofNat n (x + y) :=
   (ofNat_add x y).symm
@@ -1531,8 +1518,8 @@ instance : Std.LawfulIdentity (α := BitVec n) (· + ·) 0#n where
   left_id := BitVec.zero_add
   right_id := BitVec.add_zero
 
-theorem truncate_add (x y : BitVec w) (h : i ≤ w) :
-    (x + y).truncate i = x.truncate i + y.truncate i := by
+theorem setWidth_add (x y : BitVec w) (h : i ≤ w) :
+    (x + y).setWidth i = x.setWidth i + y.setWidth i := by
   have dvd : 2^i ∣ 2^w := Nat.pow_dvd_pow _ h
   simp [bv_toNat, h, Nat.mod_mod_of_dvd _ dvd]
 
@@ -1565,10 +1552,12 @@ theorem sub_def {n} (x y : BitVec n) : x - y = .ofNat n ((2^n - y.toNat) + x.toN
   rfl
 @[simp] theorem sub_ofFin (x : BitVec n) (y : Fin (2^n)) : x - .ofFin y = .ofFin (x.toFin - y) :=
   rfl
+
 -- Remark: we don't use `[simp]` here because simproc` subsumes it for literals.
 -- If `x` and `n` are not literals, applying this theorem eagerly may not be a good idea.
 theorem ofNat_sub_ofNat {n} (x y : Nat) : BitVec.ofNat n x - BitVec.ofNat n y = .ofNat n ((2^n - y % 2^n) + x) := by
-  apply eq_of_toNat_eq ; simp [BitVec.ofNat]
+  apply eq_of_toNat_eq
+  simp [BitVec.ofNat, Fin.ofNat'_sub]
 
 @[simp] protected theorem sub_zero (x : BitVec n) : x - 0#n = x := by apply eq_of_toNat_eq ; simp
 
@@ -1703,7 +1692,7 @@ theorem ofInt_mul {n} (x y : Int) : BitVec.ofInt n (x * y) =
   x < BitVec.ofFin y ↔ x.toFin < y := Iff.rfl
 @[simp] theorem ofFin_lt {x : Fin (2^n)} {y : BitVec n} :
   BitVec.ofFin x < y ↔ x < y.toFin := Iff.rfl
-@[simp] theorem ofNat_lt_ofNat {n} (x y : Nat) : BitVec.ofNat n x < BitVec.ofNat n y ↔ x % 2^n < y % 2^n := by
+@[simp] theorem ofNat_lt_ofNat {n} {x y : Nat} : BitVec.ofNat n x < BitVec.ofNat n y ↔ x % 2^n < y % 2^n := by
   simp [lt_def]
 
 @[simp] protected theorem not_le {x y : BitVec n} : ¬ x ≤ y ↔ y < x := by
@@ -1988,18 +1977,18 @@ theorem twoPow_zero {w : Nat} : twoPow w 0 = 1#w := by
 theorem getLsbD_one {w i : Nat} : (1#w).getLsbD i = (decide (0 < w) && decide (0 = i)) := by
   rw [← twoPow_zero, getLsbD_twoPow]
 
-/- ### zeroExtend, truncate, and bitwise operations -/
+/- ### setWidth, setWidth, and bitwise operations -/
 
 /--
 When the `(i+1)`th bit of `x` is false,
 keeping the lower `(i + 1)` bits of `x` equals keeping the lower `i` bits.
 -/
-theorem zeroExtend_truncate_succ_eq_zeroExtend_truncate_of_getLsbD_false
+theorem setWidth_setWidth_succ_eq_setWidth_setWidth_of_getLsbD_false
   {x : BitVec w} {i : Nat} (hx : x.getLsbD i = false) :
-    zeroExtend w (x.truncate (i + 1)) =
-      zeroExtend w (x.truncate i) := by
+    setWidth w (x.setWidth (i + 1)) =
+      setWidth w (x.setWidth i) := by
   ext k
-  simp only [getLsbD_zeroExtend, Fin.is_lt, decide_True, Bool.true_and, getLsbD_or, getLsbD_and]
+  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]
@@ -2010,22 +1999,22 @@ When the `(i+1)`th bit of `x` is true,
 keeping the lower `(i + 1)` bits of `x` equalsk eeping the lower `i` bits
 and then performing bitwise-or with `twoPow i = (1 << i)`,
 -/
-theorem zeroExtend_truncate_succ_eq_zeroExtend_truncate_or_twoPow_of_getLsbD_true
+theorem setWidth_setWidth_succ_eq_setWidth_setWidth_or_twoPow_of_getLsbD_true
     {x : BitVec w} {i : Nat} (hx : x.getLsbD i = true) :
-    zeroExtend w (x.truncate (i + 1)) =
-      zeroExtend w (x.truncate i) ||| (twoPow w i) := by
+    setWidth w (x.setWidth (i + 1)) =
+      setWidth w (x.setWidth i) ||| (twoPow w i) := by
   ext k
-  simp only [getLsbD_zeroExtend, Fin.is_lt, decide_True, Bool.true_and, getLsbD_or, getLsbD_and]
+  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]
   · 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_zeroExtend_ofBool_getLsbD {x : BitVec w} :
-    (x &&& 1#w) = zeroExtend w (ofBool (x.getLsbD 0)) := by
+theorem and_one_eq_setWidth_ofBool_getLsbD {x : BitVec w} :
+    (x &&& 1#w) = setWidth w (ofBool (x.getLsbD 0)) := by
   ext i
-  simp only [getLsbD_and, getLsbD_one, getLsbD_zeroExtend, Fin.is_lt, decide_True, getLsbD_ofBool,
+  simp only [getLsbD_and, getLsbD_one, getLsbD_setWidth, Fin.is_lt, decide_True, getLsbD_ofBool,
     Bool.true_and]
   by_cases h : (0 = (i : Nat)) <;> simp [h] <;> omega
 
@@ -2137,4 +2126,143 @@ theorem toNat_sub_of_le {x y : BitVec n} (h : y ≤ x) :
   · have : 2 ^ n - y.toNat + x.toNat = 2 ^ n + (x.toNat - y.toNat) := by omega
     rw [this, Nat.add_mod_left, Nat.mod_eq_of_lt (by omega)]
 
+/-! ### Deprecations -/
+
+set_option linter.missingDocs false
+
+@[deprecated truncate_eq_setWidth (since := "2024-09-18")]
+abbrev truncate_eq_zeroExtend := @truncate_eq_setWidth
+
+@[deprecated toNat_setWidth' (since := "2024-09-18")]
+abbrev toNat_zeroExtend' := @toNat_setWidth'
+
+@[deprecated toNat_setWidth (since := "2024-09-18")]
+abbrev toNat_zeroExtend := @toNat_setWidth
+
+@[deprecated toNat_setWidth (since := "2024-09-18")]
+abbrev toNat_truncate := @toNat_setWidth
+
+@[deprecated setWidth_eq (since := "2024-09-18")]
+abbrev zeroExtend_eq := @setWidth_eq
+
+@[deprecated setWidth_eq (since := "2024-09-18")]
+abbrev truncate_eq := @setWidth_eq
+
+@[deprecated setWidth_zero (since := "2024-09-18")]
+abbrev zeroExtend_zero := @setWidth_zero
+
+@[deprecated getElem_setWidth (since := "2024-09-18")]
+abbrev getElem_zeroExtend := @getElem_setWidth
+
+@[deprecated getElem_setWidth' (since := "2024-09-18")]
+abbrev getElem_zeroExtend' := @getElem_setWidth'
+
+@[deprecated getElem?_setWidth (since := "2024-09-18")]
+abbrev getElem?_zeroExtend := @getElem?_setWidth
+
+@[deprecated getElem?_setWidth' (since := "2024-09-18")]
+abbrev getElem?_zeroExtend' := @getElem?_setWidth'
+
+@[deprecated getLsbD_setWidth (since := "2024-09-18")]
+abbrev getLsbD_zeroExtend := @getLsbD_setWidth
+
+@[deprecated getLsbD_setWidth' (since := "2024-09-18")]
+abbrev getLsbD_zeroExtend' := @getLsbD_setWidth'
+
+@[deprecated getMsbD_setWidth_add (since := "2024-09-18")]
+abbrev getMsbD_zeroExtend_add := @getMsbD_setWidth_add
+
+@[deprecated getMsbD_setWidth' (since := "2024-09-18")]
+abbrev getMsbD_zeroExtend' := @getMsbD_setWidth'
+
+@[deprecated getElem_setWidth (since := "2024-09-18")]
+abbrev getElem_truncate := @getElem_setWidth
+
+@[deprecated getElem?_setWidth (since := "2024-09-18")]
+abbrev getElem?_truncate := @getElem?_setWidth
+
+@[deprecated getLsbD_setWidth (since := "2024-09-18")]
+abbrev getLsbD_truncate := @getLsbD_setWidth
+
+@[deprecated msb_setWidth (since := "2024-09-18")]
+abbrev msb_truncate := @msb_setWidth
+
+@[deprecated cast_setWidth (since := "2024-09-18")]
+abbrev cast_zeroExtend := @cast_setWidth
+
+@[deprecated cast_setWidth (since := "2024-09-18")]
+abbrev cast_truncate := @cast_setWidth
+
+@[deprecated setWidth_setWidth_of_le (since := "2024-09-18")]
+abbrev zeroExtend_zeroExtend_of_le := @setWidth_setWidth_of_le
+
+@[deprecated setWidth_eq (since := "2024-09-18")]
+abbrev truncate_eq_self := @setWidth_eq
+
+@[deprecated setWidth_cast (since := "2024-09-18")]
+abbrev truncate_cast := @setWidth_cast
+
+@[deprecated msb_setWidth (since := "2024-09-18")]
+abbrev mbs_zeroExtend := @msb_setWidth
+
+@[deprecated msb_setWidth' (since := "2024-09-18")]
+abbrev mbs_zeroExtend' := @msb_setWidth'
+
+@[deprecated setWidth_one_eq_ofBool_getLsb_zero (since := "2024-09-18")]
+abbrev zeroExtend_one_eq_ofBool_getLsb_zero := @setWidth_one_eq_ofBool_getLsb_zero
+
+@[deprecated setWidth_ofNat_one_eq_ofNat_one_of_lt (since := "2024-09-18")]
+abbrev zeroExtend_ofNat_one_eq_ofNat_one_of_lt := @setWidth_ofNat_one_eq_ofNat_one_of_lt
+
+@[deprecated setWidth_one (since := "2024-09-18")]
+abbrev truncate_one := @setWidth_one
+
+@[deprecated setWidth_ofNat_of_le (since := "2024-09-18")]
+abbrev truncate_ofNat_of_le := @setWidth_ofNat_of_le
+
+@[deprecated setWidth_or (since := "2024-09-18")]
+abbrev truncate_or := @setWidth_or
+
+@[deprecated setWidth_and (since := "2024-09-18")]
+abbrev truncate_and := @setWidth_and
+
+@[deprecated setWidth_xor (since := "2024-09-18")]
+abbrev truncate_xor := @setWidth_xor
+
+@[deprecated setWidth_not (since := "2024-09-18")]
+abbrev truncate_not := @setWidth_not
+
+@[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
+
+@[deprecated signExtend_eq_setWidth_of_lt (since := "2024-09-18")]
+abbrev signExtend_eq_truncate_of_lt := @signExtend_eq_setWidth_of_lt
+
+@[deprecated truncate_append (since := "2024-09-18")]
+abbrev truncate_append := @setWidth_append
+
+@[deprecated truncate_append_of_eq (since := "2024-09-18")]
+abbrev truncate_append_of_eq := @setWidth_append_of_eq
+
+@[deprecated truncate_cons (since := "2024-09-18")]
+abbrev truncate_cons := @setWidth_cons
+
+@[deprecated truncate_succ (since := "2024-09-18")]
+abbrev truncate_succ := @setWidth_succ
+
+@[deprecated truncate_add (since := "2024-09-18")]
+abbrev truncate_add := @setWidth_add
+
+@[deprecated setWidth_setWidth_succ_eq_setWidth_setWidth_of_getLsbD_false (since := "2024-09-18")]
+abbrev zeroExtend_truncate_succ_eq_zeroExtend_truncate_of_getLsbD_false := @setWidth_setWidth_succ_eq_setWidth_setWidth_of_getLsbD_false
+
+@[deprecated setWidth_setWidth_succ_eq_setWidth_setWidth_or_twoPow_of_getLsbD_true (since := "2024-09-18")]
+abbrev zeroExtend_truncate_succ_eq_zeroExtend_truncate_or_twoPow_of_getLsbD_true := @setWidth_setWidth_succ_eq_setWidth_setWidth_or_twoPow_of_getLsbD_true
+
+@[deprecated and_one_eq_setWidth_ofBool_getLsbD (since := "2024-09-18")]
+abbrev and_one_eq_zeroExtend_ofBool_getLsbD := @and_one_eq_setWidth_ofBool_getLsbD
+
 end BitVec

src/Init/Data/Bool.lean

@@ -12,6 +12,8 @@ namespace Bool
 /-- Boolean exclusive or -/
 abbrev xor : Bool → Bool → Bool := bne
 
+@[inherit_doc] infixl:33 " ^^ " => xor
+
 instance (p : Bool → Prop) [inst : DecidablePred p] : Decidable (∀ x, p x) :=
   match inst true, inst false with
   | isFalse ht, _ => isFalse fun h => absurd (h _) ht
@@ -145,8 +147,8 @@ theorem and_or_distrib_right : ∀ (x y z : Bool), ((x || y) && z) = (x && z ||
 theorem or_and_distrib_left  : ∀ (x y z : Bool), (x || y && z) = ((x || y) && (x || z)) := by decide
 theorem or_and_distrib_right : ∀ (x y z : Bool), (x && y || z) = ((x || z) && (y || z)) := by decide
 
-theorem and_xor_distrib_left  : ∀ (x y z : Bool), (x && xor y z) = xor (x && y) (x && z) := by decide
-theorem and_xor_distrib_right : ∀ (x y z : Bool), (xor x y && z) = xor (x && z) (y && z) := by decide
+theorem and_xor_distrib_left  : ∀ (x y z : Bool), (x && (y ^^ z)) = ((x && y) ^^ (x && z)) := by decide
+theorem and_xor_distrib_right : ∀ (x y z : Bool), ((x ^^ y) && z) = ((x && z) ^^ (y && z)) := by decide
 
 /-- De Morgan's law for boolean and -/
 @[simp] theorem not_and : ∀ (x y : Bool), (!(x && y)) = (!x || !y) := by decide
@@ -252,15 +254,6 @@ theorem beq_eq_decide_eq [BEq α] [LawfulBEq α] [DecidableEq α] (a b : α) :
 theorem eq_not : ∀ {a b : Bool}, (a = (!b)) ↔ (a ≠ b) := by decide
 theorem not_eq : ∀ {a b : Bool}, ((!a) = b) ↔ (a ≠ b) := by decide
 
-@[simp] theorem not_eq_not : ∀ {a b : Bool}, ¬a = !b ↔ a = b := by decide
-@[simp] theorem not_not_eq : ∀ {a b : Bool}, ¬(!a) = b ↔ a = b := by decide
-
-/--
-We move `!` from the left hand side of an equality to the right hand side.
-This helps confluence, and also helps combining pairs of `!`s.
--/
-@[simp] theorem not_eq_eq_eq_not : ∀ {a b : Bool}, ((!a) = b) ↔ (a = !b) := by decide
-
 @[simp] theorem coe_iff_coe : ∀{a b : Bool}, (a ↔ b) ↔ a = b := by decide
 
 @[simp] theorem coe_true_iff_false  : ∀{a b : Bool}, (a ↔ b = false) ↔ a = (!b) := by decide
@@ -274,37 +267,37 @@ theorem beq_comm {α} [BEq α] [LawfulBEq α] {a b : α} : (a == b) = (b == a) :
 
 /-! ### xor -/
 
-theorem false_xor : ∀ (x : Bool), xor false x = x := false_bne
+theorem false_xor : ∀ (x : Bool), (false ^^ x) = x := false_bne
 
-theorem xor_false : ∀ (x : Bool), xor x false = x := bne_false
+theorem xor_false : ∀ (x : Bool), (x ^^ false) = x := bne_false
 
-theorem true_xor : ∀ (x : Bool), xor true x = !x := true_bne
+theorem true_xor : ∀ (x : Bool), (true ^^ x) = !x := true_bne
 
-theorem xor_true : ∀ (x : Bool), xor x true = !x := bne_true
+theorem xor_true : ∀ (x : Bool), (x ^^ true) = !x := bne_true
 
-theorem not_xor_self : ∀ (x : Bool), xor (!x) x = true := not_bne_self
+theorem not_xor_self : ∀ (x : Bool), (!x ^^ x) = true := not_bne_self
 
-theorem xor_not_self : ∀ (x : Bool), xor x (!x) = true := bne_not_self
+theorem xor_not_self : ∀ (x : Bool), (x ^^ !x) = true := bne_not_self
 
-theorem not_xor : ∀ (x y : Bool), xor (!x) y = !(xor x y) := by decide
+theorem not_xor : ∀ (x y : Bool), (!x ^^ y) = !(x ^^ y) := by decide
 
-theorem xor_not : ∀ (x y : Bool), xor x (!y) = !(xor x y) := by decide
+theorem xor_not : ∀ (x y : Bool), (x ^^ !y) = !(x ^^ y) := by decide
 
-theorem not_xor_not : ∀ (x y : Bool), xor (!x) (!y) = (xor x y) := not_bne_not
+theorem not_xor_not : ∀ (x y : Bool), (!x ^^ !y) = (x ^^ y) := not_bne_not
 
-theorem xor_self : ∀ (x : Bool), xor x x = false := by decide
+theorem xor_self : ∀ (x : Bool), (x ^^ x) = false := by decide
 
-theorem xor_comm : ∀ (x y : Bool), xor x y = xor y x := by decide
+theorem xor_comm : ∀ (x y : Bool), (x ^^ y) = (y ^^ x) := by decide
 
-theorem xor_left_comm : ∀ (x y z : Bool), xor x (xor y z) = xor y (xor x z) := by decide
+theorem xor_left_comm : ∀ (x y z : Bool), (x ^^ (y ^^ z)) = (y ^^ (x ^^ z)) := by decide
 
-theorem xor_right_comm : ∀ (x y z : Bool), xor (xor x y) z = xor (xor x z) y := by decide
+theorem xor_right_comm : ∀ (x y z : Bool), ((x ^^ y) ^^ z) = ((x ^^ z) ^^ y) := by decide
 
-theorem xor_assoc : ∀ (x y z : Bool), xor (xor x y) z = xor x (xor y z) := bne_assoc
+theorem xor_assoc : ∀ (x y z : Bool), ((x ^^ y) ^^ z) = (x ^^ (y ^^ z)) := bne_assoc
 
-theorem xor_left_inj : ∀ {x y z : Bool}, xor x y = xor x z ↔ y = z := bne_left_inj
+theorem xor_left_inj : ∀ {x y z : Bool}, (x ^^ y) = (x ^^ z) ↔ y = z := bne_left_inj
 
-theorem xor_right_inj : ∀ {x y z : Bool}, xor x z = xor y z ↔ x = y := bne_right_inj
+theorem xor_right_inj : ∀ {x y z : Bool}, (x ^^ z) = (y ^^ z) ↔ x = y := bne_right_inj
 
 /-! ### le/lt -/
 

src/Init/Data/Fin/Lemmas.lean

@@ -54,7 +54,12 @@ theorem mk_val (i : Fin n) : (⟨i, i.isLt⟩ : Fin n) = i := Fin.eta ..
 @[simp] theorem val_ofNat' (n : Nat) [NeZero n] (a : Nat) :
   (Fin.ofNat' n a).val = a % n := rfl
 
-@[simp] theorem ofNat'_val_eq_self [NeZero n](x : Fin n) : (Fin.ofNat' n x) = x := by
+@[simp] theorem ofNat'_self {n : Nat} [NeZero n] : Fin.ofNat' n n = 0 := by
+  ext
+  simp
+  congr
+
+@[simp] theorem ofNat'_val_eq_self [NeZero n] (x : Fin n) : (Fin.ofNat' n x) = x := by
   ext
   rw [val_ofNat', Nat.mod_eq_of_lt]
   exact x.2
@@ -68,6 +73,9 @@ theorem mk_val (i : Fin n) : (⟨i, i.isLt⟩ : Fin n) = i := Fin.eta ..
 @[simp] theorem modn_val (a : Fin n) (b : Nat) : (a.modn b).val = a.val % b :=
   rfl
 
+@[simp] theorem val_eq_zero (a : Fin 1) : a.val = 0 :=
+  Nat.eq_zero_of_le_zero <| Nat.le_of_lt_succ a.isLt
+
 theorem ite_val {n : Nat} {c : Prop} [Decidable c] {x : c → Fin n} (y : ¬c → Fin n) :
     (if h : c then x h else y h).val = if h : c then (x h).val else (y h).val := by
   by_cases c <;> simp [*]
@@ -120,7 +128,7 @@ theorem mk_le_of_le_val {b : Fin n} {a : Nat} (h : a ≤ b) :
 
 @[simp] theorem mk_lt_mk {x y : Nat} {hx hy} : (⟨x, hx⟩ : Fin n) < ⟨y, hy⟩ ↔ x < y := .rfl
 
-@[simp] theorem val_zero (n : Nat) : (0 : Fin (n + 1)).1 = 0 := rfl
+@[simp] theorem val_zero (n : Nat) [NeZero n] : ((0 : Fin n) : Nat) = 0 := rfl
 
 @[simp] theorem mk_zero : (⟨0, Nat.succ_pos n⟩ : Fin (n + 1)) = 0 := rfl
 
@@ -167,8 +175,24 @@ theorem rev_eq {n a : Nat} (i : Fin (n + 1)) (h : n = a + i) :
 @[simp] theorem rev_lt_rev {i j : Fin n} : rev i < rev j ↔ j < i := by
   rw [← Fin.not_le, ← Fin.not_le, rev_le_rev]
 
+/-! ### last -/
+
 @[simp] theorem val_last (n : Nat) : last n = n := rfl
 
+@[simp] theorem last_zero : (Fin.last 0 : Fin 1) = 0 := by
+  ext
+  simp
+
+@[simp] theorem zero_eq_last_iff {n : Nat} : (0 : Fin (n + 1)) = last n ↔ n = 0 := by
+  constructor
+  · intro h
+    simp_all [Fin.ext_iff]
+  · rintro rfl
+    simp
+
+@[simp] theorem last_eq_zero_iff {n : Nat} : Fin.last n = 0 ↔ n = 0 := by
+  simp [eq_comm (a := Fin.last n)]
+
 theorem le_last (i : Fin (n + 1)) : i ≤ last n := Nat.le_of_lt_succ i.is_lt
 
 theorem last_pos : (0 : Fin (n + 2)) < last (n + 1) := Nat.succ_pos _
@@ -202,10 +226,28 @@ instance subsingleton_one : Subsingleton (Fin 1) := subsingleton_iff_le_one.2 (b
 
 theorem fin_one_eq_zero (a : Fin 1) : a = 0 := Subsingleton.elim a 0
 
+@[simp] theorem zero_eq_one_iff {n : Nat} [NeZero n] : (0 : Fin n) = 1 ↔ n = 1 := by
+  constructor
+  · intro h
+    simp [Fin.ext_iff] at h
+    change 0 % n = 1 % n at h
+    rw [eq_comm] at h
+    simpa using h
+  · rintro rfl
+    simp
+
+@[simp] theorem one_eq_zero_iff {n : Nat} [NeZero n] : (1 : Fin n) = 0 ↔ n = 1 := by
+  rw [eq_comm]
+  simp
+
 theorem add_def (a b : Fin n) : a + b = Fin.mk ((a + b) % n) (Nat.mod_lt _ a.size_pos) := rfl
 
 theorem val_add (a b : Fin n) : (a + b).val = (a.val + b.val) % n := rfl
 
+@[simp] protected theorem zero_add {n : Nat} [NeZero n] (i : Fin n) : (0 : Fin n) + i = i := by
+  ext
+  simp [Fin.add_def, Nat.mod_eq_of_lt i.2]
+
 theorem val_add_one_of_lt {n : Nat} {i : Fin n.succ} (h : i < last _) : (i + 1).1 = i + 1 := by
   match n with
   | 0 => cases h
@@ -329,6 +371,10 @@ theorem succ_succ_ne_one (a : Fin n) : Fin.succ (Fin.succ a) ≠ 1 :=
 
 @[simp] theorem cast_mk (h : n = m) (i : Nat) (hn : i < n) : cast h ⟨i, hn⟩ = ⟨i, h ▸ hn⟩ := rfl
 
+@[simp] theorem cast_refl (n : Nat) (h : n = n) : cast h = id := by
+  ext
+  simp
+
 @[simp] theorem cast_trans {k : Nat} (h : n = m) (h' : m = k) {i : Fin n} :
     cast h' (cast h i) = cast (Eq.trans h h') i := rfl
 
@@ -437,6 +483,10 @@ theorem succ_castSucc {n : Nat} (i : Fin n) : i.castSucc.succ = castSucc i.succ
 
 @[simp] theorem coe_addNat (m : Nat) (i : Fin n) : (addNat i m : Nat) = i + m := rfl
 
+@[simp] theorem addNat_zero (n : Nat) (i : Fin n) : addNat i 0 = i := by
+  ext
+  simp
+
 @[simp] theorem addNat_one {i : Fin n} : addNat i 1 = i.succ := rfl
 
 theorem le_coe_addNat (m : Nat) (i : Fin n) : m ≤ addNat i m :=
@@ -466,7 +516,7 @@ theorem cast_addNat_left {n n' m : Nat} (i : Fin n') (h : n' + m = n + m) :
 
 theorem le_coe_natAdd (m : Nat) (i : Fin n) : m ≤ natAdd m i := Nat.le_add_right ..
 
-theorem natAdd_zero {n : Nat} : natAdd 0 = cast (Nat.zero_add n).symm := by ext; simp
+@[simp] theorem natAdd_zero {n : Nat} : natAdd 0 = cast (Nat.zero_add n).symm := by ext; simp
 
 /-- For rewriting in the reverse direction, see `Fin.cast_natAdd_right`. -/
 theorem natAdd_cast {n n' : Nat} (m : Nat) (i : Fin n') (h : n' = n) :
@@ -504,9 +554,19 @@ theorem cast_addNat {n : Nat} (m : Nat) (i : Fin n) :
 
 @[simp] theorem natAdd_last {m n : Nat} : natAdd n (last m) = last (n + m) := rfl
 
+@[simp] theorem addNat_last (n : Nat) :
+    addNat (last n) m = cast (by omega) (last (n + m)) := by
+  ext
+  simp
+
 theorem natAdd_castSucc {m n : Nat} {i : Fin m} : natAdd n (castSucc i) = castSucc (natAdd n i) :=
   rfl
 
+@[simp] theorem natAdd_eq_addNat (n : Nat) (i : Fin n) : Fin.natAdd n i = i.addNat n := by
+  ext
+  simp
+  omega
+
 theorem rev_castAdd (k : Fin n) (m : Nat) : rev (castAdd m k) = addNat (rev k) m := Fin.ext <| by
   rw [val_rev, coe_castAdd, coe_addNat, val_rev, Nat.sub_add_comm (Nat.succ_le_of_lt k.is_lt)]
 
@@ -572,6 +632,15 @@ theorem pred_add_one (i : Fin (n + 2)) (h : (i : Nat) < n + 1) :
 @[simp] theorem subNat_mk {i : Nat} (h₁ : i < n + m) (h₂ : m ≤ i) :
     subNat m ⟨i, h₁⟩ h₂ = ⟨i - m, Nat.sub_lt_right_of_lt_add h₂ h₁⟩ := rfl
 
+@[simp] theorem subNat_zero (i : Fin n) (h : 0 ≤ (i : Nat)): Fin.subNat 0 i h = i := by
+  ext
+  simp
+
+@[simp] theorem subNat_one_succ (i : Fin (n + 1)) (h : 1 ≤ ↑i) : (subNat 1 i h).succ = i := by
+  ext
+  simp
+  omega
+
 @[simp] theorem pred_castSucc_succ (i : Fin n) :
     pred (castSucc i.succ) (Fin.ne_of_gt (castSucc_pos i.succ_pos)) = castSucc i := rfl
 
@@ -582,7 +651,7 @@ theorem pred_add_one (i : Fin (n + 2)) (h : (i : Nat) < n + 1) :
     subNat m (addNat i m) h = i := Fin.ext <| Nat.add_sub_cancel i m
 
 @[simp] theorem natAdd_subNat_cast {i : Fin (n + m)} (h : n ≤ i) :
-    natAdd n (subNat n (cast (Nat.add_comm ..) i) h) = i := by simp [← cast_addNat]; rfl
+    natAdd n (subNat n (cast (Nat.add_comm ..) i) h) = i := by simp [← cast_addNat]
 
 /-! ### recursion and induction principles -/
 
@@ -750,12 +819,12 @@ theorem addCases_right {m n : Nat} {motive : Fin (m + n) → Sort _} {left right
 
 /-! ### add -/
 
-@[simp] theorem ofNat'_add [NeZero n] (x : Nat) (y : Fin n) :
+theorem ofNat'_add [NeZero n] (x : Nat) (y : Fin n) :
     Fin.ofNat' n x + y = Fin.ofNat' n (x + y.val) := by
   apply Fin.eq_of_val_eq
   simp [Fin.ofNat', Fin.add_def]
 
-@[simp] theorem add_ofNat' [NeZero n] (x : Fin n) (y : Nat) :
+theorem add_ofNat' [NeZero n] (x : Fin n) (y : Nat) :
     x + Fin.ofNat' n y = Fin.ofNat' n (x.val + y) := by
   apply Fin.eq_of_val_eq
   simp [Fin.ofNat', Fin.add_def]
@@ -765,16 +834,21 @@ theorem addCases_right {m n : Nat} {motive : Fin (m + n) → Sort _} {left right
 protected theorem coe_sub (a b : Fin n) : ((a - b : Fin n) : Nat) = ((n - b) + a) % n := by
   cases a; cases b; rfl
 
-@[simp] theorem ofNat'_sub [NeZero n] (x : Nat) (y : Fin n) :
+theorem ofNat'_sub [NeZero n] (x : Nat) (y : Fin n) :
     Fin.ofNat' n x - y = Fin.ofNat' n ((n - y.val) + x) := by
   apply Fin.eq_of_val_eq
   simp [Fin.ofNat', Fin.sub_def]
 
-@[simp] theorem sub_ofNat' [NeZero n] (x : Fin n) (y : Nat) :
+theorem sub_ofNat' [NeZero n] (x : Fin n) (y : Nat) :
     x - Fin.ofNat' n y = Fin.ofNat' n ((n - y % n) + x.val) := by
   apply Fin.eq_of_val_eq
   simp [Fin.ofNat', Fin.sub_def]
 
+@[simp] protected theorem sub_self [NeZero n] {x : Fin n} : x - x = 0 := by
+  ext
+  rw [Fin.sub_def]
+  simp
+
 private theorem _root_.Nat.mod_eq_sub_of_lt_two_mul {x n} (h₁ : n ≤ x) (h₂ : x < 2 * n) :
     x % n = x - n := by
   rw [Nat.mod_eq, if_pos (by omega), Nat.mod_eq_of_lt (by omega)]

src/Init/Data/List/Attach.lean

@@ -308,6 +308,46 @@ theorem getElem_attach {xs : List α} {i : Nat} (h : i < xs.attach.length) :
     xs.attach.tail = xs.tail.attach.map (fun ⟨x, h⟩ => ⟨x, mem_of_mem_tail h⟩) := by
   cases xs <;> simp
 
+theorem foldl_pmap (l : List α) {P : α → Prop} (f : (a : α) → P a → β)
+  (H : ∀ (a : α), a ∈ l → P a) (g : γ → β → γ) (x : γ) :
+    (l.pmap f H).foldl g x = l.attach.foldl (fun acc a => g acc (f a.1 (H _ a.2))) x := by
+  rw [pmap_eq_map_attach, foldl_map]
+
+theorem foldr_pmap (l : List α) {P : α → Prop} (f : (a : α) → P a → β)
+  (H : ∀ (a : α), a ∈ l → P a) (g : β → γ → γ) (x : γ) :
+    (l.pmap f H).foldr g x = l.attach.foldr (fun a acc => g (f a.1 (H _ a.2)) acc) x := by
+  rw [pmap_eq_map_attach, foldr_map]
+
+/--
+If we fold over `l.attach` with a function that ignores the membership predicate,
+we get the same results as folding over `l` directly.
+
+This is useful when we need to use `attach` to show termination.
+
+Unfortunately this can't be applied by `simp` because of the higher order unification problem,
+and even when rewriting we need to specify the function explicitly.
+-/
+theorem foldl_attach (l : List α) (f : β → α → β) (b : β) :
+    l.attach.foldl (fun acc t => f acc t.1) b = l.foldl f b := by
+  induction l generalizing b with
+  | nil => simp
+  | cons a l ih => rw [foldl_cons, attach_cons, foldl_cons, foldl_map, ih]
+
+/--
+If we fold over `l.attach` with a function that ignores the membership predicate,
+we get the same results as folding over `l` directly.
+
+This is useful when we need to use `attach` to show termination.
+
+Unfortunately this can't be applied by `simp` because of the higher order unification problem,
+and even when rewriting we need to specify the function explicitly.
+-/
+theorem foldr_attach (l : List α) (f : α → β → β) (b : β) :
+    l.attach.foldr (fun t acc => f t.1 acc) b = l.foldr f b := by
+  induction l generalizing b with
+  | nil => simp
+  | cons a l ih => rw [foldr_cons, attach_cons, foldr_cons, foldr_map, ih]
+
 theorem attach_map {l : List α} (f : α → β) :
     (l.map f).attach = l.attach.map (fun ⟨x, h⟩ => ⟨f x, mem_map_of_mem f h⟩) := by
   induction l <;> simp [*]

src/Init/Data/List/Erase.lean

@@ -109,6 +109,10 @@ protected theorem Sublist.eraseP : l₁ <+ l₂ → l₁.eraseP p <+ l₂.eraseP
 theorem length_eraseP_le (l : List α) : (l.eraseP p).length ≤ l.length :=
   l.eraseP_sublist.length_le
 
+theorem le_length_eraseP (l : List α) : l.length - 1 ≤ (l.eraseP p).length := by
+  rw [length_eraseP]
+  split <;> simp
+
 theorem mem_of_mem_eraseP {l : List α} : a ∈ l.eraseP p → a ∈ l := (eraseP_subset _ ·)
 
 @[simp] theorem mem_eraseP_of_neg {l : List α} (pa : ¬p a) : a ∈ l.eraseP p ↔ a ∈ l := by
@@ -332,6 +336,10 @@ theorem IsPrefix.erase (a : α) {l₁ l₂ : List α} (h : l₁ <+: l₂) : l₁
 theorem length_erase_le (a : α) (l : List α) : (l.erase a).length ≤ l.length :=
   (erase_sublist a l).length_le
 
+theorem le_length_erase [LawfulBEq α] (a : α) (l : List α) : l.length - 1 ≤ (l.erase a).length := by
+  rw [length_erase]
+  split <;> simp
+
 theorem mem_of_mem_erase {a b : α} {l : List α} (h : a ∈ l.erase b) : a ∈ l := erase_subset _ _ h
 
 @[simp] theorem mem_erase_of_ne [LawfulBEq α] {a b : α} {l : List α} (ab : a ≠ b) :
@@ -452,13 +460,22 @@ end erase
 
 /-! ### eraseIdx -/
 
-theorem length_eraseIdx : ∀ {l i}, i < length l → length (@eraseIdx α l i) = length l - 1
-  | [], _, _ => rfl
-  | _::_, 0, _ => by simp [eraseIdx]
-  | x::xs, i+1, h => by
-    have : i < length xs := Nat.lt_of_succ_lt_succ h
-    simp [eraseIdx, ← Nat.add_one]
-    rw [length_eraseIdx this, Nat.sub_add_cancel (Nat.lt_of_le_of_lt (Nat.zero_le _) this)]
+theorem length_eraseIdx (l : List α) (i : Nat) :
+    (l.eraseIdx i).length = if i < l.length then l.length - 1 else l.length := by
+  induction l generalizing i with
+  | nil => simp
+  | cons x l ih =>
+    cases i with
+    | zero => simp
+    | succ i =>
+      simp only [eraseIdx, length_cons, ih, add_one_lt_add_one_iff, Nat.add_one_sub_one]
+      split
+      · cases l <;> simp_all
+      · rfl
+
+theorem length_eraseIdx_of_lt {l : List α} {i} (h : i < length l) :
+    (l.eraseIdx i).length = length l - 1 := by
+  simp [length_eraseIdx, h]
 
 @[simp] theorem eraseIdx_zero (l : List α) : eraseIdx l 0 = tail l := by cases l <;> rfl
 
@@ -468,6 +485,8 @@ theorem eraseIdx_eq_take_drop_succ :
   | a::l, 0 => by simp
   | a::l, i + 1 => by simp [eraseIdx_eq_take_drop_succ l i]
 
+-- See `Init.Data.List.Nat.Erase` for `getElem?_eraseIdx` and `getElem_eraseIdx`.
+
 @[simp] theorem eraseIdx_eq_nil {l : List α} {i : Nat} : eraseIdx l i = [] ↔ l = [] ∨ (length l = 1 ∧ i = 0) := by
   match l, i with
   | [], _
@@ -499,6 +518,13 @@ theorem eraseIdx_eq_self : ∀ {l : List α} {k : Nat}, eraseIdx l k = l ↔ len
 theorem eraseIdx_of_length_le {l : List α} {k : Nat} (h : length l ≤ k) : eraseIdx l k = l := by
   rw [eraseIdx_eq_self.2 h]
 
+theorem length_eraseIdx_le (l : List α) (i : Nat) : length (l.eraseIdx i) ≤ length l :=
+  (eraseIdx_sublist l i).length_le
+
+theorem le_length_eraseIdx (l : List α) (i : Nat) : length l - 1 ≤ length (l.eraseIdx i) := by
+  rw [length_eraseIdx]
+  split <;> simp
+
 theorem eraseIdx_append_of_lt_length {l : List α} {k : Nat} (hk : k < length l) (l' : List α) :
     eraseIdx (l ++ l') k = eraseIdx l k ++ l' := by
   induction l generalizing k with
@@ -520,7 +546,7 @@ theorem eraseIdx_append_of_length_le {l : List α} {k : Nat} (hk : length l ≤
 theorem eraseIdx_replicate {n : Nat} {a : α} {k : Nat} :
     (replicate n a).eraseIdx k = if k < n then replicate (n - 1) a else replicate n a := by
   split <;> rename_i h
-  · rw [eq_replicate_iff, length_eraseIdx (by simpa using h)]
+  · rw [eq_replicate_iff, length_eraseIdx_of_lt (by simpa using h)]
     simp only [length_replicate, true_and]
     intro b m
     replace m := mem_of_mem_eraseIdx m

src/Init/Data/List/Find.lean

@@ -224,7 +224,7 @@ theorem find?_eq_some : xs.find? p = some b ↔ p b ∧ ∃ as bs, xs = as ++ b
           simp only [cons_append] at h₁
           obtain ⟨rfl, -⟩ := h₁
           simp_all
-    · simp only [ih, Bool.not_eq_true', exists_and_right, and_congr_right_iff]
+    · simp only [ih, Bool.not_eq_eq_eq_not, Bool.not_true, exists_and_right, and_congr_right_iff]
       intro pb
       constructor
       · rintro ⟨as, ⟨⟨bs, rfl⟩, h₁⟩⟩
@@ -620,6 +620,18 @@ theorem IsPrefix.findIdx_eq_of_findIdx_lt_length {l₁ l₂ : List α} {p : α
   · rfl
   · simp_all
 
+theorem findIdx_le_findIdx {l : List α} {p q : α → Bool} (h : ∀ x ∈ l, p x → q x) : l.findIdx q ≤ l.findIdx p := by
+  induction l with
+  | nil => simp
+  | cons x xs ih =>
+    simp only [findIdx_cons, cond_eq_if]
+    split
+    · simp
+    · split
+      · simp_all
+      · simp only [Nat.add_le_add_iff_right]
+        exact ih fun _ m w => h _ (mem_cons_of_mem x m) w
+
 /-! ### findIdx? -/
 
 @[simp] theorem findIdx?_nil : ([] : List α).findIdx? p i = none := rfl
@@ -803,7 +815,7 @@ theorem findIdx?_join {l : List (List α)} {p : α → Bool} :
     simp only [replicate, findIdx?_cons, Nat.zero_add, findIdx?_succ, zero_lt_succ, true_and]
     split <;> simp_all
 
-theorem findIdx?_eq_enum_findSome? {xs : List α} {p : α → Bool} :
+theorem findIdx?_eq_findSome?_enum {xs : List α} {p : α → Bool} :
     xs.findIdx? p = xs.enum.findSome? fun ⟨i, a⟩ => if p a then some i else none := by
   induction xs with
   | nil => simp
@@ -814,6 +826,30 @@ theorem findIdx?_eq_enum_findSome? {xs : List α} {p : α → Bool} :
     · simp_all only [enumFrom_cons, ite_false, Option.isNone_none, findSome?_cons_of_isNone, reduceCtorEq]
       simp [Function.comp_def, ← map_fst_add_enum_eq_enumFrom, findSome?_map]
 
+theorem findIdx?_eq_fst_find?_enum {xs : List α} {p : α → Bool} :
+    xs.findIdx? p = (xs.enum.find? fun ⟨_, x⟩ => p x).map (·.1) := by
+  induction xs with
+  | nil => simp
+  | cons x xs ih =>
+    simp only [findIdx?_cons, Nat.zero_add, findIdx?_start_succ, enum_cons]
+    split
+    · simp_all
+    · simp only [Option.map_map, enumFrom_eq_map_enum, Bool.false_eq_true, not_false_eq_true,
+        find?_cons_of_neg, find?_map, *]
+      congr
+
+-- See also `findIdx_le_findIdx`.
+theorem findIdx?_eq_none_of_findIdx?_eq_none {xs : List α} {p q : α → Bool} (w : ∀ x ∈ xs, p x → q x) :
+    xs.findIdx? q = none → xs.findIdx? p = none := by
+  simp only [findIdx?_eq_none_iff]
+  intro h x m
+  cases z : p x
+  · rfl
+  · exfalso
+    specialize w x m z
+    specialize h x m
+    simp_all
+
 theorem Sublist.findIdx?_isSome {l₁ l₂ : List α} (h : l₁ <+ l₂) :
     (l₁.findIdx? p).isSome → (l₂.findIdx? p).isSome := by
   simp only [List.findIdx?_isSome, any_eq_true]
@@ -878,7 +914,7 @@ theorem lookup_eq_some_iff {l : List (α × β)} {k : α} {b : β} :
   simp only [lookup_eq_findSome?, findSome?_eq_some_iff]
   constructor
   · rintro ⟨l₁, a, l₂, rfl, h₁, h₂⟩
-    simp only [beq_iff_eq, ite_some_none_eq_some] at h₁
+    simp only [beq_iff_eq, Option.ite_none_right_eq_some, Option.some.injEq] at h₁
     obtain ⟨rfl, rfl⟩ := h₁
     simp at h₂
     exact ⟨l₁, l₂, rfl, by simpa using h₂⟩

src/Init/Data/List/Lemmas.lean

@@ -266,9 +266,15 @@ theorem get!_len_le [Inhabited α] : ∀ {l : List α} {n}, length l ≤ n → l
 theorem getElem?_eq_some_iff {l : List α} : l[n]? = some a ↔ ∃ h : n < l.length, l[n] = a := by
   simp only [← get?_eq_getElem?, get?_eq_some, get_eq_getElem]
 
+theorem some_eq_getElem?_iff {l : List α} : some a = l[n]? ↔ ∃ h : n < l.length, l[n] = a := by
+  rw [eq_comm, getElem?_eq_some_iff]
+
 @[simp] theorem getElem?_eq_none_iff : l[n]? = none ↔ length l ≤ n := by
   simp only [← get?_eq_getElem?, get?_eq_none]
 
+@[simp] theorem none_eq_getElem?_iff {l : List α} {n : Nat} : none = l[n]? ↔ length l ≤ n := by
+  simp [eq_comm (a := none)]
+
 theorem getElem?_eq_none (h : length l ≤ n) : l[n]? = none := getElem?_eq_none_iff.mpr h
 
 theorem getElem?_eq (l : List α) (i : Nat) :
@@ -1946,7 +1952,7 @@ theorem map_eq_append_iff {f : α → β} :
     map f l = L₁ ++ L₂ ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ map f l₁ = L₁ ∧ map f l₂ = L₂ := by
   rw [← filterMap_eq_map, filterMap_eq_append_iff]
 
-theorem append_eq_map_iff (f : α → β) :
+theorem append_eq_map_iff {f : α → β} :
     L₁ ++ L₂ = map f l ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ map f l₁ = L₁ ∧ map f l₂ = L₂ := by
   rw [eq_comm, map_eq_append_iff]
 

src/Init/Data/List/Nat.lean

@@ -10,3 +10,5 @@ import Init.Data.List.Nat.Range
 import Init.Data.List.Nat.Sublist
 import Init.Data.List.Nat.TakeDrop
 import Init.Data.List.Nat.Count
+import Init.Data.List.Nat.Erase
+import Init.Data.List.Nat.Find

src/Init/Data/List/Nat/Basic.lean

@@ -5,6 +5,7 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M
 -/
 prelude
 import Init.Data.List.Count
+import Init.Data.List.Find
 import Init.Data.List.MinMax
 import Init.Data.Nat.Lemmas
 
@@ -57,7 +58,8 @@ theorem getElem_eq_getElem_reverse {l : List α} {i} (h : i < l.length) :
 
 /-- The length of the List returned by `List.leftpad n a l` is equal
   to the larger of `n` and `l.length` -/
-@[simp]
+-- We don't mark this as a `@[simp]` lemma since we allow `simp` to unfold `leftpad`,
+-- so the left hand side simplifies directly to `n - l.length + l.length`.
 theorem leftpad_length (n : Nat) (a : α) (l : List α) :
     (leftpad n a l).length = max n l.length := by
   simp only [leftpad, length_append, length_replicate, Nat.sub_add_eq_max]
@@ -117,6 +119,53 @@ theorem minimum?_cons' {a : Nat} {l : List Nat} :
         specialize le b h
         split <;> omega
 
+theorem foldl_min
+    {α : Type _} [Min α] [Std.IdempotentOp (min : α → α → α)] [Std.Associative (min : α → α → α)]
+    {l : List α} {a : α} :
+    l.foldl (init := a) min = min a (l.minimum?.getD a) := by
+  cases l with
+  | nil => simp [Std.IdempotentOp.idempotent]
+  | cons b l =>
+    simp only [minimum?]
+    induction l generalizing a b with
+    | nil => simp
+    | cons c l ih => simp [ih, Std.Associative.assoc]
+
+theorem foldl_min_right {α β : Type _}
+    [Min β] [Std.IdempotentOp (min : β → β → β)] [Std.Associative (min : β → β → β)]
+    {l : List α} {b : β} {f : α → β} :
+    (l.foldl (init := b) fun acc a => min acc (f a)) = min b ((l.map f).minimum?.getD b) := by
+  rw [← foldl_map, foldl_min]
+
+theorem foldl_min_le {l : List Nat} {a : Nat} : l.foldl (init := a) min ≤ a := by
+  induction l generalizing a with
+  | nil => simp
+  | cons c l ih =>
+    simp only [foldl_cons]
+    exact Nat.le_trans ih (Nat.min_le_left _ _)
+
+theorem foldl_min_min_of_le {l : List Nat} {a b : Nat} (h : a ≤ b) :
+    l.foldl (init := a) min ≤ b :=
+  Nat.le_trans (foldl_min_le) h
+
+theorem minimum?_getD_le_of_mem {l : List Nat} {a k : Nat} (h : a ∈ l) :
+    l.minimum?.getD k ≤ a := by
+  cases l with
+  | nil => simp at h
+  | cons b l =>
+    simp [minimum?_cons]
+    simp at h
+    rcases h with (rfl | h)
+    · exact foldl_min_le
+    · induction l generalizing b with
+      | nil => simp_all
+      | cons c l ih =>
+        simp only [foldl_cons]
+        simp at h
+        rcases h with (rfl | h)
+        · exact foldl_min_min_of_le (Nat.min_le_right _ _)
+        · exact ih _ h
+
 /-! ### maximum? -/
 
 -- A specialization of `maximum?_eq_some_iff` to Nat.
@@ -150,4 +199,51 @@ theorem maximum?_cons' {a : Nat} {l : List Nat} :
         specialize le b h
         split <;> omega
 
+theorem foldl_max
+    {α : Type _} [Max α] [Std.IdempotentOp (max : α → α → α)] [Std.Associative (max : α → α → α)]
+    {l : List α} {a : α} :
+    l.foldl (init := a) max = max a (l.maximum?.getD a) := by
+  cases l with
+  | nil => simp [Std.IdempotentOp.idempotent]
+  | cons b l =>
+    simp only [maximum?]
+    induction l generalizing a b with
+    | nil => simp
+    | cons c l ih => simp [ih, Std.Associative.assoc]
+
+theorem foldl_max_right {α β : Type _}
+    [Max β] [Std.IdempotentOp (max : β → β → β)] [Std.Associative (max : β → β → β)]
+    {l : List α} {b : β} {f : α → β} :
+    (l.foldl (init := b) fun acc a => max acc (f a)) = max b ((l.map f).maximum?.getD b) := by
+  rw [← foldl_map, foldl_max]
+
+theorem le_foldl_max {l : List Nat} {a : Nat} : a ≤ l.foldl (init := a) max := by
+  induction l generalizing a with
+  | nil => simp
+  | cons c l ih =>
+    simp only [foldl_cons]
+    exact Nat.le_trans (Nat.le_max_left _ _) ih
+
+theorem le_foldl_max_of_le {l : List Nat} {a b : Nat} (h : a ≤ b) :
+    a ≤ l.foldl (init := b) max :=
+  Nat.le_trans h (le_foldl_max)
+
+theorem le_maximum?_getD_of_mem {l : List Nat} {a k : Nat} (h : a ∈ l) :
+    a ≤ l.maximum?.getD k := by
+  cases l with
+  | nil => simp at h
+  | cons b l =>
+    simp [maximum?_cons]
+    simp at h
+    rcases h with (rfl | h)
+    · exact le_foldl_max
+    · induction l generalizing b with
+      | nil => simp_all
+      | cons c l ih =>
+        simp only [foldl_cons]
+        simp at h
+        rcases h with (rfl | h)
+        · exact le_foldl_max_of_le (Nat.le_max_right b a)
+        · exact ih _ h
+
 end List

src/Init/Data/List/Nat/Erase.lean

@@ -0,0 +1,66 @@
+/-
+Copyright (c) 2024 Kim Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Init.Data.List.Nat.TakeDrop
+import Init.Data.List.Erase
+
+namespace List
+
+theorem getElem?_eraseIdx (l : List α) (i : Nat) (j : Nat) :
+    (l.eraseIdx i)[j]? = if h : j < i then l[j]? else l[j + 1]? := by
+  rw [eraseIdx_eq_take_drop_succ, getElem?_append]
+  split <;> rename_i h
+  · rw [getElem?_take]
+    split
+    · rfl
+    · simp_all
+      omega
+  · rw [getElem?_drop]
+    split <;> rename_i h'
+    · simp only [length_take, Nat.min_def, Nat.not_lt] at h
+      split at h
+      · omega
+      · simp_all [getElem?_eq_none]
+        omega
+    · simp only [length_take]
+      simp only [length_take, Nat.min_def, Nat.not_lt] at h
+      split at h
+      · congr 1
+        omega
+      · rw [getElem?_eq_none, getElem?_eq_none] <;> omega
+
+theorem getElem?_eraseIdx_of_lt (l : List α) (i : Nat) (j : Nat) (h : j < i) :
+    (l.eraseIdx i)[j]? = l[j]? := by
+  rw [getElem?_eraseIdx]
+  simp [h]
+
+theorem getElem?_eraseIdx_of_ge (l : List α) (i : Nat) (j : Nat) (h : i ≤ j) :
+    (l.eraseIdx i)[j]? = l[j + 1]? := by
+  rw [getElem?_eraseIdx]
+  simp only [dite_eq_ite, ite_eq_right_iff]
+  intro h'
+  omega
+
+theorem getElem_eraseIdx (l : List α) (i : Nat) (j : Nat) (h : j < (l.eraseIdx i).length) :
+    (l.eraseIdx i)[j] = if h' : j < i then
+        l[j]'(by have := length_eraseIdx_le l i; omega)
+      else
+        l[j + 1]'(by rw [length_eraseIdx] at h; split at h <;> omega) := by
+  apply Option.some.inj
+  rw [← getElem?_eq_getElem, getElem?_eraseIdx]
+  split <;> simp
+
+theorem getElem_eraseIdx_of_lt (l : List α) (i : Nat) (j : Nat) (h : j < (l.eraseIdx i).length) (h' : j < i) :
+    (l.eraseIdx i)[j] = l[j]'(by have := length_eraseIdx_le l i; omega) := by
+  rw [getElem_eraseIdx]
+  simp only [dite_eq_left_iff, Nat.not_lt]
+  intro h'
+  omega
+
+theorem getElem_eraseIdx_of_ge (l : List α) (i : Nat) (j : Nat) (h : j < (l.eraseIdx i).length) (h' : i ≤ j) :
+    (l.eraseIdx i)[j] = l[j + 1]'(by rw [length_eraseIdx] at h; split at h <;> omega) := by
+  rw [getElem_eraseIdx, dif_neg]
+  omega

src/Init/Data/List/Nat/Find.lean

@@ -0,0 +1,32 @@
+/-
+Copyright (c) 2024 Kim Morrison. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Init.Data.List.Nat.Range
+import Init.Data.List.Find
+
+namespace List
+
+theorem findIdx?_eq_some_le_of_findIdx?_eq_some {xs : List α} {p q : α → Bool} (w : ∀ x ∈ xs, p x → q x) {i : Nat}
+    (h : xs.findIdx? p = some i) : ∃ j, j ≤ i ∧ xs.findIdx? q = some j := by
+  simp only [findIdx?_eq_findSome?_enum] at h
+  rw [findSome?_eq_some_iff] at h
+  simp only [Option.ite_none_right_eq_some, Option.some.injEq, ite_eq_right_iff, reduceCtorEq,
+    imp_false, Bool.not_eq_true, Prod.forall, exists_and_right, Prod.exists] at h
+  obtain ⟨h, h₁, b, ⟨es, h₂⟩, ⟨hb, rfl⟩, h₃⟩ := h
+  rw [enum_eq_enumFrom, enumFrom_eq_append_iff] at h₂
+  obtain ⟨l₁', l₂', rfl, rfl, h₂⟩ := h₂
+  rw [eq_comm, enumFrom_eq_cons_iff] at h₂
+  obtain ⟨a, as, rfl, h₂, rfl⟩ := h₂
+  simp only [Nat.zero_add, Prod.mk.injEq] at h₂
+  obtain ⟨rfl, rfl⟩ := h₂
+  simp only [findIdx?_append]
+  match h : findIdx? q l₁' with
+  | some j =>
+    refine ⟨j, ?_, by simp⟩
+    rw [findIdx?_eq_some_iff_findIdx_eq] at h
+    omega
+  | none =>
+    refine ⟨l₁'.length, by simp, by simp_all⟩

src/Init/Data/List/Nat/Range.lean

@@ -109,7 +109,8 @@ theorem range'_eq_append_iff : range' s n = xs ++ ys ↔ ∃ k, k ≤ n ∧ xs =
 @[simp] theorem find?_range'_eq_some {s n : Nat} {i : Nat} {p : Nat → Bool} :
     (range' s n).find? p = some i ↔ p i ∧ i ∈ range' s n ∧ ∀ j, s ≤ j → j < i → !p j := by
   rw [find?_eq_some]
-  simp only [Bool.not_eq_true', exists_and_right, mem_range'_1, and_congr_right_iff]
+  simp only [Bool.not_eq_eq_eq_not, Bool.not_true, exists_and_right, mem_range'_1,
+    and_congr_right_iff]
   simp only [range'_eq_append_iff, eq_comm (a := i :: _), range'_eq_cons_iff]
   intro h
   constructor
@@ -275,15 +276,15 @@ theorem nodup_iota (n : Nat) : Nodup (iota n) :=
   rw [getLast_eq_head_reverse]
   simp
 
-theorem find?_iota_eq_none {n : Nat} (p : Nat → Bool) :
+theorem find?_iota_eq_none {n : Nat} {p : Nat → Bool} :
     (iota n).find? p = none ↔ ∀ i, 0 < i → i ≤ n → !p i := by
   simp
 
 @[simp] theorem find?_iota_eq_some {n : Nat} {i : Nat} {p : Nat → Bool} :
     (iota n).find? p = some i ↔ p i ∧ i ∈ iota n ∧ ∀ j, i < j → j ≤ n → !p j := by
   rw [find?_eq_some]
-  simp only [iota_eq_reverse_range', reverse_eq_append_iff, reverse_cons, append_assoc,
-    singleton_append, Bool.not_eq_true', exists_and_right, mem_reverse, mem_range'_1,
+  simp only [iota_eq_reverse_range', reverse_eq_append_iff, reverse_cons, append_assoc, cons_append,
+    nil_append, Bool.not_eq_eq_eq_not, Bool.not_true, exists_and_right, mem_reverse, mem_range'_1,
     and_congr_right_iff]
   intro h
   constructor
@@ -357,17 +358,6 @@ theorem map_enumFrom (f : α → β) (n : Nat) (l : List α) :
     map (Prod.map id f) (enumFrom n l) = enumFrom n (map f l) := by
   induction l generalizing n <;> simp_all
 
-@[simp]
-theorem enumFrom_map_fst (n) :
-    ∀ (l : List α), map Prod.fst (enumFrom n l) = range' n l.length
-  | [] => rfl
-  | _ :: _ => congrArg (cons _) (enumFrom_map_fst _ _)
-
-@[simp]
-theorem enumFrom_map_snd : ∀ (n) (l : List α), map Prod.snd (enumFrom n l) = l
-  | _, [] => rfl
-  | _, _ :: _ => congrArg (cons _) (enumFrom_map_snd _ _)
-
 theorem snd_mem_of_mem_enumFrom {x : Nat × α} {n : Nat} {l : List α} (h : x ∈ enumFrom n l) : x.2 ∈ l :=
   enumFrom_map_snd n l ▸ mem_map_of_mem _ h
 
@@ -390,10 +380,6 @@ theorem mem_enumFrom {x : α} {i j : Nat} {xs : List α} (h : (i, x) ∈ xs.enum
       x = xs[i - j]'(by have := le_fst_of_mem_enumFrom h; have := fst_lt_add_of_mem_enumFrom h; omega) :=
   ⟨le_fst_of_mem_enumFrom h, fst_lt_add_of_mem_enumFrom h, snd_eq_of_mem_enumFrom h⟩
 
-theorem enumFrom_cons' (n : Nat) (x : α) (xs : List α) :
-    enumFrom n (x :: xs) = (n, x) :: (enumFrom n xs).map (Prod.map (· + 1) id) := by
-  rw [enumFrom_cons, Nat.add_comm, ← map_fst_add_enumFrom_eq_enumFrom]
-
 theorem enumFrom_map (n : Nat) (l : List α) (f : α → β) :
     enumFrom n (l.map f) = (enumFrom n l).map (Prod.map id f) := by
   induction l with
@@ -410,22 +396,39 @@ theorem enumFrom_append (xs ys : List α) (n : Nat) :
     rw [cons_append, enumFrom_cons, IH, ← cons_append, ← enumFrom_cons, length, Nat.add_right_comm,
       Nat.add_assoc]
 
-theorem enumFrom_eq_zip_range' (l : List α) {n : Nat} : l.enumFrom n = (range' n l.length).zip l :=
-  zip_of_prod (enumFrom_map_fst _ _) (enumFrom_map_snd _ _)
+theorem enumFrom_eq_cons_iff {l : List α} {n : Nat} :
+    l.enumFrom n = x :: l' ↔ ∃ a as, l = a :: as ∧ x = (n, a) ∧ l' = enumFrom (n + 1) as := by
+  rw [enumFrom_eq_zip_range', zip_eq_cons_iff]
+  constructor
+  · rintro ⟨l₁, l₂, h, rfl, rfl⟩
+    rw [range'_eq_cons_iff] at h
+    obtain ⟨rfl, -, rfl⟩ := h
+    exact ⟨x.2, l₂, by simp [enumFrom_eq_zip_range']⟩
+  · rintro ⟨a, as, rfl, rfl, rfl⟩
+    refine ⟨range' (n+1) as.length, as, ?_⟩
+    simp [enumFrom_eq_zip_range', range'_succ]
 
-@[simp]
-theorem unzip_enumFrom_eq_prod (l : List α) {n : Nat} :
-    (l.enumFrom n).unzip = (range' n l.length, l) := by
-  simp only [enumFrom_eq_zip_range', unzip_zip, length_range']
+theorem enumFrom_eq_append_iff {l : List α} {n : Nat} :
+    l.enumFrom n = l₁ ++ l₂ ↔
+      ∃ l₁' l₂', l = l₁' ++ l₂' ∧ l₁ = l₁'.enumFrom n ∧ l₂ = l₂'.enumFrom (n + l₁'.length) := by
+  rw [enumFrom_eq_zip_range', zip_eq_append_iff]
+  constructor
+  · rintro ⟨w, x, y, z, h, h', rfl, rfl, rfl⟩
+    rw [range'_eq_append_iff] at h'
+    obtain ⟨k, -, rfl, rfl⟩ := h'
+    simp only [length_range'] at h
+    obtain rfl := h
+    refine ⟨y, z, rfl, ?_⟩
+    simp only [enumFrom_eq_zip_range', length_append, true_and]
+    congr
+    omega
+  · rintro ⟨l₁', l₂', rfl, rfl, rfl⟩
+    simp only [enumFrom_eq_zip_range']
+    refine ⟨range' n l₁'.length, range' (n + l₁'.length) l₂'.length, l₁', l₂', ?_⟩
+    simp [Nat.add_comm]
 
 /-! ### enum -/
 
-theorem enum_cons : (a::as).enum = (0, a) :: as.enumFrom 1 := rfl
-
-theorem enum_cons' (x : α) (xs : List α) :
-    enum (x :: xs) = (0, x) :: (enum xs).map (Prod.map (· + 1) id) :=
-  enumFrom_cons' _ _ _
-
 @[simp]
 theorem enum_eq_nil {l : List α} : List.enum l = [] ↔ l = [] := enumFrom_eq_nil
 

src/Init/Data/List/Range.lean

@@ -5,6 +5,7 @@ Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, M
 -/
 prelude
 import Init.Data.List.Pairwise
+import Init.Data.List.Zip
 
 /-!
 # Lemmas about `List.range` and `List.enum`
@@ -241,4 +242,47 @@ theorem map_fst_add_enum_eq_enumFrom (l : List α) (n : Nat) :
     map (Prod.map (· + n) id) (enum l) = enumFrom n l :=
   map_fst_add_enumFrom_eq_enumFrom l _ _
 
+theorem enumFrom_cons' (n : Nat) (x : α) (xs : List α) :
+    enumFrom n (x :: xs) = (n, x) :: (enumFrom n xs).map (Prod.map (· + 1) id) := by
+  rw [enumFrom_cons, Nat.add_comm, ← map_fst_add_enumFrom_eq_enumFrom]
+
+@[simp]
+theorem enumFrom_map_fst (n) :
+    ∀ (l : List α), map Prod.fst (enumFrom n l) = range' n l.length
+  | [] => rfl
+  | _ :: _ => congrArg (cons _) (enumFrom_map_fst _ _)
+
+@[simp]
+theorem enumFrom_map_snd : ∀ (n) (l : List α), map Prod.snd (enumFrom n l) = l
+  | _, [] => rfl
+  | _, _ :: _ => congrArg (cons _) (enumFrom_map_snd _ _)
+
+theorem enumFrom_eq_zip_range' (l : List α) {n : Nat} : l.enumFrom n = (range' n l.length).zip l :=
+  zip_of_prod (enumFrom_map_fst _ _) (enumFrom_map_snd _ _)
+
+@[simp]
+theorem unzip_enumFrom_eq_prod (l : List α) {n : Nat} :
+    (l.enumFrom n).unzip = (range' n l.length, l) := by
+  simp only [enumFrom_eq_zip_range', unzip_zip, length_range']
+
+/-! ### enum -/
+
+theorem enum_cons : (a::as).enum = (0, a) :: as.enumFrom 1 := rfl
+
+theorem enum_cons' (x : α) (xs : List α) :
+    enum (x :: xs) = (0, x) :: (enum xs).map (Prod.map (· + 1) id) :=
+  enumFrom_cons' _ _ _
+
+theorem enum_eq_enumFrom {l : List α} : l.enum = l.enumFrom 0 := rfl
+
+theorem enumFrom_eq_map_enum (l : List α) (n : Nat) :
+    enumFrom n l = (enum l).map (Prod.map (· + n) id) := by
+  induction l generalizing n with
+  | nil => simp
+  | cons x xs ih =>
+    simp only [enumFrom_cons, ih, enum_cons, map_cons, Prod.map_apply, Nat.zero_add, id_eq, map_map,
+      cons.injEq, map_inj_left, Function.comp_apply, Prod.forall, Prod.mk.injEq, and_true, true_and]
+    intro a b _
+    exact (succ_add a n).symm
+
 end List

src/Init/Data/List/Sort/Lemmas.lean

@@ -114,14 +114,15 @@ theorem enumLE_trans (trans : ∀ a b c, le a b → le b c → le a c)
   · simp_all
   · simp_all
 
-theorem enumLE_total (total : ∀ a b, !le a b → le b a)
-    (a b : Nat × α) : !enumLE le a b → enumLE le b a := by
+theorem enumLE_total (total : ∀ a b, le a b || le b a)
+    (a b : Nat × α) : enumLE le a b || enumLE le b a := by
   simp only [enumLE]
   split <;> split
-  · simpa using Nat.le_of_lt
+  · simpa using Nat.le_total a.fst b.fst
   · simp
   · simp
-  · simp_all [total a.2 b.2]
+  · have := total a.2 b.2
+    simp_all
 
 /-! ### merge -/
 
@@ -191,12 +192,12 @@ theorem merge_stable : ∀ (xs ys) (_ : ∀ x y, x ∈ xs → y ∈ ys → x.1
 attribute [local instance] boolRelToRel
 
 /--
-If the ordering relation `le` is transitive and total (i.e. `le a b ∨ le b a` for all `a, b`)
+If the ordering relation `le` is transitive and total (i.e. `le a b || le b a` for all `a, b`)
 then the `merge` of two sorted lists is sorted.
 -/
 theorem sorted_merge
     (trans : ∀ (a b c : α), le a b → le b c → le a c)
-    (total : ∀ (a b : α), !le a b → le b a)
+    (total : ∀ (a b : α), le a b || le b a)
     (l₁ l₂ : List α) (h₁ : l₁.Pairwise le) (h₂ : l₂.Pairwise le) : (merge l₁ l₂ le).Pairwise le := by
   induction l₁ generalizing l₂ with
   | nil => simpa only [merge]
@@ -217,9 +218,10 @@ theorem sorted_merge
       · apply Pairwise.cons
         · intro z m
           rw [mem_merge, mem_cons] at m
+          simp only [Bool.not_eq_true] at h
           rcases m with (⟨rfl|m⟩|m)
-          · exact total _ _ (by simpa using h)
-          · exact trans _ _ _ (total _ _ (by simpa using h)) (rel_of_pairwise_cons h₁ m)
+          · simpa [h] using total y z
+          · exact trans _ _ _ (by simpa [h] using total x y) (rel_of_pairwise_cons h₁ m)
           · exact rel_of_pairwise_cons h₂ m
         · exact ih₂ h₂.tail
 
@@ -263,7 +265,7 @@ theorem mergeSort_perm : ∀ (l : List α) (le), mergeSort l le ~ l
         (Perm.of_eq (splitInTwo_fst_append_splitInTwo_snd _)))
 termination_by l => l.length
 
-@[simp] theorem mergeSort_length (l : List α) : (mergeSort l le).length = l.length :=
+@[simp] theorem length_mergeSort (l : List α) : (mergeSort l le).length = l.length :=
   (mergeSort_perm l le).length_eq
 
 @[simp] theorem mem_mergeSort {a : α} {l : List α} : a ∈ mergeSort l le ↔ a ∈ l :=
@@ -272,13 +274,13 @@ termination_by l => l.length
 /--
 The result of `mergeSort` is sorted,
 as long as the comparison function is transitive (`le a b → le b c → le a c`)
-and total in the sense that `le a b ∨ le b a`.
+and total in the sense that `le a b || le b a`.
 
 The comparison function need not be irreflexive, i.e. `le a b` and `le b a` is allowed even when `a ≠ b`.
 -/
 theorem sorted_mergeSort
     (trans : ∀ (a b c : α), le a b → le b c → le a c)
-    (total : ∀ (a b : α), !le a b → le b a) :
+    (total : ∀ (a b : α), le a b || le b a) :
     (l : List α) → (mergeSort l le).Pairwise le
   | [] => by simp [mergeSort]
   | [a] => by simp [mergeSort]
@@ -346,7 +348,7 @@ termination_by _ l => l.length
 
 theorem mergeSort_cons {le : α → α → Bool}
     (trans : ∀ (a b c : α), le a b → le b c → le a c)
-    (total : ∀ (a b : α), !le a b → le b a)
+    (total : ∀ (a b : α), le a b || le b a)
     (a : α) (l : List α) :
     ∃ l₁ l₂, mergeSort (a :: l) le = l₁ ++ a :: l₂ ∧ mergeSort l le = l₁ ++ l₂ ∧
       ∀ b, b ∈ l₁ → !le a b := by
@@ -405,7 +407,7 @@ then `c` is still a sublist of `mergeSort le l`.
 -/
 theorem sublist_mergeSort
     (trans : ∀ (a b c : α), le a b → le b c → le a c)
-    (total : ∀ (a b : α), !le a b → le b a) :
+    (total : ∀ (a b : α), le a b || le b a) :
     ∀ {c : List α} (_ : c.Pairwise le) (_ : c <+ l),
     c <+ mergeSort l le
   | _, _, .slnil => nil_sublist _
@@ -436,7 +438,7 @@ then `[a, b]` is still a sublist of `mergeSort le l`.
 -/
 theorem pair_sublist_mergeSort
     (trans : ∀ (a b c : α), le a b → le b c → le a c)
-    (total : ∀ (a b : α), !le a b → le b a)
+    (total : ∀ (a b : α), le a b || le b a)
     (hab : le a b) (h : [a, b] <+ l) : [a, b] <+ mergeSort l le :=
   sublist_mergeSort trans total (pairwise_pair.mpr hab) h
 

src/Init/Data/List/Zip.lean

@@ -16,87 +16,6 @@ open Nat
 
 /-! ## Zippers -/
 
-/-! ### zip -/
-
-theorem zip_map (f : α → γ) (g : β → δ) :
-    ∀ (l₁ : List α) (l₂ : List β), zip (l₁.map f) (l₂.map g) = (zip l₁ l₂).map (Prod.map f g)
-  | [], l₂ => rfl
-  | l₁, [] => by simp only [map, zip_nil_right]
-  | a :: l₁, b :: l₂ => by
-    simp only [map, zip_cons_cons, zip_map, Prod.map]; constructor
-
-theorem zip_map_left (f : α → γ) (l₁ : List α) (l₂ : List β) :
-    zip (l₁.map f) l₂ = (zip l₁ l₂).map (Prod.map f id) := by rw [← zip_map, map_id]
-
-theorem zip_map_right (f : β → γ) (l₁ : List α) (l₂ : List β) :
-    zip l₁ (l₂.map f) = (zip l₁ l₂).map (Prod.map id f) := by rw [← zip_map, map_id]
-
-@[simp] theorem tail_zip (l₁ : List α) (l₂ : List β) :
-    (zip l₁ l₂).tail = zip l₁.tail l₂.tail := by
-  cases l₁ <;> cases l₂ <;> simp
-
-theorem zip_append :
-    ∀ {l₁ r₁ : List α} {l₂ r₂ : List β} (_h : length l₁ = length l₂),
-      zip (l₁ ++ r₁) (l₂ ++ r₂) = zip l₁ l₂ ++ zip r₁ r₂
-  | [], r₁, l₂, r₂, h => by simp only [eq_nil_of_length_eq_zero h.symm]; rfl
-  | l₁, r₁, [], r₂, h => by simp only [eq_nil_of_length_eq_zero h]; rfl
-  | a :: l₁, r₁, b :: l₂, r₂, h => by
-    simp only [cons_append, zip_cons_cons, zip_append (Nat.succ.inj h)]
-
-theorem zip_map' (f : α → β) (g : α → γ) :
-    ∀ l : List α, zip (l.map f) (l.map g) = l.map fun a => (f a, g a)
-  | [] => rfl
-  | a :: l => by simp only [map, zip_cons_cons, zip_map']
-
-theorem of_mem_zip {a b} : ∀ {l₁ : List α} {l₂ : List β}, (a, b) ∈ zip l₁ l₂ → a ∈ l₁ ∧ b ∈ l₂
-  | _ :: l₁, _ :: l₂, h => by
-    cases h
-    case head => simp
-    case tail h =>
-    · have := of_mem_zip h
-      exact ⟨Mem.tail _ this.1, Mem.tail _ this.2⟩
-
-@[deprecated of_mem_zip (since := "2024-07-28")] abbrev mem_zip := @of_mem_zip
-
-theorem map_fst_zip :
-    ∀ (l₁ : List α) (l₂ : List β), l₁.length ≤ l₂.length → map Prod.fst (zip l₁ l₂) = l₁
-  | [], bs, _ => rfl
-  | _ :: as, _ :: bs, h => by
-    simp [Nat.succ_le_succ_iff] at h
-    show _ :: map Prod.fst (zip as bs) = _ :: as
-    rw [map_fst_zip as bs h]
-  | a :: as, [], h => by simp at h
-
-theorem map_snd_zip :
-    ∀ (l₁ : List α) (l₂ : List β), l₂.length ≤ l₁.length → map Prod.snd (zip l₁ l₂) = l₂
-  | _, [], _ => by
-    rw [zip_nil_right]
-    rfl
-  | [], b :: bs, h => by simp at h
-  | a :: as, b :: bs, h => by
-    simp [Nat.succ_le_succ_iff] at h
-    show _ :: map Prod.snd (zip as bs) = _ :: bs
-    rw [map_snd_zip as bs h]
-
-theorem map_prod_left_eq_zip {l : List α} (f : α → β) :
-    (l.map fun x => (x, f x)) = l.zip (l.map f) := by
-  rw [← zip_map']
-  congr
-  simp
-
-theorem map_prod_right_eq_zip {l : List α} (f : α → β) :
-    (l.map fun x => (f x, x)) = (l.map f).zip l := by
-  rw [← zip_map']
-  congr
-  simp
-
-/-- See also `List.zip_replicate` in `Init.Data.List.TakeDrop` for a generalization with different lengths. -/
-@[simp] theorem zip_replicate' {a : α} {b : β} {n : Nat} :
-    zip (replicate n a) (replicate n b) = replicate n (a, b) := by
-  induction n with
-  | zero => rfl
-  | succ n ih => simp [replicate_succ, ih]
-
 /-! ### zipWith -/
 
 theorem zipWith_comm (f : α → β → γ) :
@@ -253,6 +172,65 @@ theorem zipWith_append (f : α → β → γ) (l la : List α) (l' lb : List β)
       simp only [length_cons, Nat.succ.injEq] at h
       simp [ih _ h]
 
+theorem zipWith_eq_cons_iff {f : α → β → γ} {l₁ : List α} {l₂ : List β} :
+    zipWith f l₁ l₂ = g :: l ↔
+      ∃ a l₁' b l₂', l₁ = a :: l₁' ∧ l₂ = b :: l₂' ∧ g = f a b ∧ l = zipWith f l₁' l₂' := by
+  match l₁, l₂ with
+  | [], [] => simp
+  | [], b :: l₂ => simp
+  | a :: l₁, [] => simp
+  | a' :: l₁, b' :: l₂ =>
+    simp only [zip_cons_cons, cons.injEq, Prod.mk.injEq]
+    constructor
+    · rintro ⟨⟨rfl, rfl⟩, rfl⟩
+      refine ⟨a', l₁, b', l₂, by simp⟩
+    · rintro ⟨a, l₁, b, l₂, ⟨rfl, rfl⟩, ⟨rfl, rfl⟩, rfl, rfl⟩
+      simp
+
+theorem zipWith_eq_append_iff {f : α → β → γ} {l₁ : List α} {l₂ : List β} :
+    zipWith f l₁ l₂ = l₁' ++ l₂' ↔
+      ∃ w x y z, w.length = y.length ∧ l₁ = w ++ x ∧ l₂ = y ++ z ∧ l₁' = zipWith f w y ∧ l₂' = zipWith f x z := by
+  induction l₁ generalizing l₂ l₁' with
+  | nil =>
+    simp
+    constructor
+    · rintro ⟨rfl, rfl⟩
+      exact ⟨[], [], [], by simp⟩
+    · rintro ⟨_, _, _, -, ⟨rfl, rfl⟩, _, rfl, rfl, rfl⟩
+      simp
+  | cons x₁ l₁ ih₁ =>
+    cases l₂ with
+    | nil =>
+      constructor
+      · simp only [zipWith_nil_right, nil_eq, append_eq_nil, exists_and_left, and_imp]
+        rintro rfl  rfl
+        exact ⟨[], x₁ :: l₁, [], by simp⟩
+      · rintro ⟨w, x, y, z, h₁, _, h₃, rfl, rfl⟩
+        simp only [nil_eq, append_eq_nil] at h₃
+        obtain ⟨rfl, rfl⟩ := h₃
+        simp
+    | cons x₂ l₂ =>
+      simp only [zipWith_cons_cons]
+      rw [cons_eq_append_iff]
+      constructor
+      · rintro (⟨rfl, rfl⟩ | ⟨l₁'', rfl, h⟩)
+        · exact ⟨[], x₁ :: l₁, [], x₂ :: l₂, by simp⟩
+        · rw [ih₁] at h
+          obtain ⟨w, x, y, z, h, rfl, rfl, h', rfl⟩ := h
+          refine ⟨x₁ :: w, x, x₂ :: y, z, by simp [h, h']⟩
+      · rintro ⟨w, x, y, z, h₁, h₂, h₃, rfl, rfl⟩
+        rw [cons_eq_append_iff] at h₂
+        rw [cons_eq_append_iff] at h₃
+        obtain (⟨rfl, rfl⟩ | ⟨w', rfl, rfl⟩) := h₂
+        · simp only [zipWith_nil_left, true_and, nil_eq, reduceCtorEq, false_and, exists_const,
+          or_false]
+          obtain (⟨rfl, rfl⟩ | ⟨y', rfl, rfl⟩) := h₃
+          · simp
+          · simp_all
+        · obtain (⟨rfl, rfl⟩ | ⟨y', rfl, rfl⟩) := h₃
+          · simp_all
+          · simp_all [zipWith_append, Nat.succ_inj']
+
 /-- See also `List.zipWith_replicate` in `Init.Data.List.TakeDrop` for a generalization with different lengths. -/
 @[simp] theorem zipWith_replicate' {a : α} {b : β} {n : Nat} :
     zipWith f (replicate n a) (replicate n b) = replicate n (f a b) := by
@@ -260,6 +238,113 @@ theorem zipWith_append (f : α → β → γ) (l la : List α) (l' lb : List β)
   | zero => rfl
   | succ n ih => simp [replicate_succ, ih]
 
+/-! ### zip -/
+
+theorem zip_eq_zipWith : ∀ (l₁ : List α) (l₂ : List β), zip l₁ l₂ = zipWith Prod.mk l₁ l₂
+  | [], _ => rfl
+  | _, [] => rfl
+  | a :: l₁, b :: l₂ => by simp [zip_cons_cons, zip_eq_zipWith l₁ l₂]
+
+theorem zip_map (f : α → γ) (g : β → δ) :
+    ∀ (l₁ : List α) (l₂ : List β), zip (l₁.map f) (l₂.map g) = (zip l₁ l₂).map (Prod.map f g)
+  | [], l₂ => rfl
+  | l₁, [] => by simp only [map, zip_nil_right]
+  | a :: l₁, b :: l₂ => by
+    simp only [map, zip_cons_cons, zip_map, Prod.map]; constructor
+
+theorem zip_map_left (f : α → γ) (l₁ : List α) (l₂ : List β) :
+    zip (l₁.map f) l₂ = (zip l₁ l₂).map (Prod.map f id) := by rw [← zip_map, map_id]
+
+theorem zip_map_right (f : β → γ) (l₁ : List α) (l₂ : List β) :
+    zip l₁ (l₂.map f) = (zip l₁ l₂).map (Prod.map id f) := by rw [← zip_map, map_id]
+
+@[simp] theorem tail_zip (l₁ : List α) (l₂ : List β) :
+    (zip l₁ l₂).tail = zip l₁.tail l₂.tail := by
+  cases l₁ <;> cases l₂ <;> simp
+
+theorem zip_append :
+    ∀ {l₁ r₁ : List α} {l₂ r₂ : List β} (_h : length l₁ = length l₂),
+      zip (l₁ ++ r₁) (l₂ ++ r₂) = zip l₁ l₂ ++ zip r₁ r₂
+  | [], r₁, l₂, r₂, h => by simp only [eq_nil_of_length_eq_zero h.symm]; rfl
+  | l₁, r₁, [], r₂, h => by simp only [eq_nil_of_length_eq_zero h]; rfl
+  | a :: l₁, r₁, b :: l₂, r₂, h => by
+    simp only [cons_append, zip_cons_cons, zip_append (Nat.succ.inj h)]
+
+theorem zip_map' (f : α → β) (g : α → γ) :
+    ∀ l : List α, zip (l.map f) (l.map g) = l.map fun a => (f a, g a)
+  | [] => rfl
+  | a :: l => by simp only [map, zip_cons_cons, zip_map']
+
+theorem of_mem_zip {a b} : ∀ {l₁ : List α} {l₂ : List β}, (a, b) ∈ zip l₁ l₂ → a ∈ l₁ ∧ b ∈ l₂
+  | _ :: l₁, _ :: l₂, h => by
+    cases h
+    case head => simp
+    case tail h =>
+    · have := of_mem_zip h
+      exact ⟨Mem.tail _ this.1, Mem.tail _ this.2⟩
+
+@[deprecated of_mem_zip (since := "2024-07-28")] abbrev mem_zip := @of_mem_zip
+
+theorem map_fst_zip :
+    ∀ (l₁ : List α) (l₂ : List β), l₁.length ≤ l₂.length → map Prod.fst (zip l₁ l₂) = l₁
+  | [], bs, _ => rfl
+  | _ :: as, _ :: bs, h => by
+    simp [Nat.succ_le_succ_iff] at h
+    show _ :: map Prod.fst (zip as bs) = _ :: as
+    rw [map_fst_zip as bs h]
+  | a :: as, [], h => by simp at h
+
+theorem map_snd_zip :
+    ∀ (l₁ : List α) (l₂ : List β), l₂.length ≤ l₁.length → map Prod.snd (zip l₁ l₂) = l₂
+  | _, [], _ => by
+    rw [zip_nil_right]
+    rfl
+  | [], b :: bs, h => by simp at h
+  | a :: as, b :: bs, h => by
+    simp [Nat.succ_le_succ_iff] at h
+    show _ :: map Prod.snd (zip as bs) = _ :: bs
+    rw [map_snd_zip as bs h]
+
+theorem map_prod_left_eq_zip {l : List α} (f : α → β) :
+    (l.map fun x => (x, f x)) = l.zip (l.map f) := by
+  rw [← zip_map']
+  congr
+  simp
+
+theorem map_prod_right_eq_zip {l : List α} (f : α → β) :
+    (l.map fun x => (f x, x)) = (l.map f).zip l := by
+  rw [← zip_map']
+  congr
+  simp
+
+@[simp] theorem zip_eq_nil_iff {l₁ : List α} {l₂ : List β} :
+    zip l₁ l₂ = [] ↔ l₁ = [] ∨ l₂ = [] := by
+  simp [zip_eq_zipWith]
+
+theorem zip_eq_cons_iff {l₁ : List α} {l₂ : List β} :
+    zip l₁ l₂ = (a, b) :: l ↔
+      ∃ l₁' l₂', l₁ = a :: l₁' ∧ l₂ = b :: l₂' ∧ l = zip l₁' l₂' := by
+  simp only [zip_eq_zipWith, zipWith_eq_cons_iff]
+  constructor
+  · rintro ⟨a, l₁, b, l₂, rfl, rfl, h, rfl, rfl⟩
+    simp only [Prod.mk.injEq] at h
+    obtain ⟨rfl, rfl⟩ := h
+    simp
+  · rintro ⟨l₁', l₂', rfl, rfl, rfl⟩
+    refine ⟨a, l₁', b, l₂', by simp⟩
+
+theorem zip_eq_append_iff {l₁ : List α} {l₂ : List β} :
+    zip l₁ l₂ = l₁' ++ l₂' ↔
+      ∃ w x y z, w.length = y.length ∧ l₁ = w ++ x ∧ l₂ = y ++ z ∧ l₁' = zip w y ∧ l₂' = zip x z := by
+  simp [zip_eq_zipWith, zipWith_eq_append_iff]
+
+/-- See also `List.zip_replicate` in `Init.Data.List.TakeDrop` for a generalization with different lengths. -/
+@[simp] theorem zip_replicate' {a : α} {b : β} {n : Nat} :
+    zip (replicate n a) (replicate n b) = replicate n (a, b) := by
+  induction n with
+  | zero => rfl
+  | succ n ih => simp [replicate_succ, ih]
+
 /-! ### zipWithAll -/
 
 theorem getElem?_zipWithAll {f : Option α → Option β → γ} {i : Nat} :
@@ -367,11 +452,11 @@ theorem zip_of_prod {l : List α} {l' : List β} {lp : List (α × β)} (hl : lp
     (hr : lp.map Prod.snd = l') : lp = l.zip l' := by
   rw [← hl, ← hr, ← zip_unzip lp, ← unzip_fst, ← unzip_snd, zip_unzip, zip_unzip]
 
-@[simp] theorem tail_zip_fst {l : List (α × β)} : l.unzip.1.tail = l.tail.unzip.1 := by
-  cases l <;> simp
+theorem tail_zip_fst {l : List (α × β)} : l.unzip.1.tail = l.tail.unzip.1 := by
+  simp
 
-@[simp] theorem tail_zip_snd {l : List (α × β)} : l.unzip.2.tail = l.tail.unzip.2 := by
-  cases l <;> simp
+theorem tail_zip_snd {l : List (α × β)} : l.unzip.2.tail = l.tail.unzip.2 := by
+  simp
 
 @[simp] theorem unzip_replicate {n : Nat} {a : α} {b : β} :
     unzip (replicate n (a, b)) = (replicate n a, replicate n b) := by

src/Init/Data/Nat/Bitwise/Lemmas.lean

@@ -237,7 +237,7 @@ theorem testBit_two_pow_add_eq (x i : Nat) : testBit (2^i + x) i = !(testBit x i
   | _ p => simp [p]
 
 theorem testBit_mul_two_pow_add_eq (a b i : Nat) :
-    testBit (2^i*a + b) i = Bool.xor (a%2 = 1) (testBit b i) := by
+    testBit (2^i*a + b) i = (a%2 = 1 ^^ testBit b i) := by
   match a with
   | 0 => simp
   | a+1 =>
@@ -570,7 +570,7 @@ theorem or_div_two : (a ||| b) / 2 = a / 2 ||| b / 2 := by
 /-! ### xor -/
 
 @[simp] theorem testBit_xor (x y i : Nat) :
-    (x ^^^ y).testBit i = Bool.xor (x.testBit i) (y.testBit i) := by
+    (x ^^^ y).testBit i = ((x.testBit i) ^^ (y.testBit i)) := by
   simp [HXor.hXor, Xor.xor, xor, testBit_bitwise ]
 
 @[simp] theorem zero_xor (x : Nat) : 0 ^^^ x = x := by

src/Init/Data/Nat/Div.lean

@@ -134,6 +134,19 @@ theorem mod_eq_of_lt {a b : Nat} (h : a < b) : a % b = a :=
     if_neg h'
   (mod_eq a b).symm ▸ this
 
+@[simp] theorem one_mod_eq_zero_iff {n : Nat} : 1 % n = 0 ↔ n = 1 := by
+  match n with
+  | 0 => simp
+  | 1 => simp
+  | n + 2 =>
+    rw [mod_eq_of_lt (by exact Nat.lt_of_sub_eq_succ rfl)]
+    simp only [add_one_ne_zero, false_iff, ne_eq]
+    exact ne_of_beq_eq_false rfl
+
+@[simp] theorem Nat.zero_eq_one_mod_iff {n : Nat} : 0 = 1 % n ↔ n = 1 := by
+  rw [eq_comm]
+  simp
+
 theorem mod_eq_sub_mod {a b : Nat} (h : a ≥ b) : a % b = (a - b) % b :=
   match eq_zero_or_pos b with
   | Or.inl h₁ => h₁.symm ▸ (Nat.sub_zero a).symm ▸ rfl
@@ -157,6 +170,13 @@ theorem mod_lt (x : Nat) {y : Nat} : y > 0 → x % y < y := by
     rw [mod_eq_sub_mod h₁]
     exact h₂ h₃
 
+@[simp] protected theorem sub_mod_add_mod_cancel (a b : Nat) [NeZero a] : a - b % a + b % a = a := by
+  rw [Nat.sub_add_cancel]
+  cases a with
+  | zero => simp_all
+  | succ a =>
+    exact Nat.le_of_lt (mod_lt b (zero_lt_succ a))
+
 theorem mod_le (x y : Nat) : x % y ≤ x := by
   match Nat.lt_or_ge x y with
   | Or.inl h₁ => rw [mod_eq_of_lt h₁]; apply Nat.le_refl
@@ -197,7 +217,6 @@ decreasing_by apply div_rec_lemma; assumption
 theorem div_eq_sub_div (h₁ : 0 < b) (h₂ : b ≤ a) : a / b = (a - b) / b + 1 := by
  rw [div_eq a, if_pos]; constructor <;> assumption
 
-
 theorem mod_add_div (m k : Nat) : m % k + k * (m / k) = m := by
   induction m, k using mod.inductionOn with rw [div_eq, mod_eq]
   | base x y h => simp [h]

src/Init/Data/Nat/Lemmas.lean

@@ -230,6 +230,17 @@ instance : Std.Associative (α := Nat) min := ⟨Nat.min_assoc⟩
 @[simp] protected theorem min_self_assoc' {m n : Nat} : min n (min m n) = min n m := by
   rw [Nat.min_comm m n, ← Nat.min_assoc, Nat.min_self]
 
+@[simp] theorem min_add_left {a b : Nat} : min a (b + a) = a := by
+  rw [Nat.min_def]
+  simp
+@[simp] theorem min_add_right {a b : Nat} : min a (a + b) = a := by
+  rw [Nat.min_def]
+  simp
+@[simp] theorem add_left_min {a b : Nat} : min (b + a) a = a := by
+  rw [Nat.min_comm, min_add_left]
+@[simp] theorem add_right_min {a b : Nat} : min (a + b) a = a := by
+  rw [Nat.min_comm, min_add_right]
+
 protected theorem sub_sub_eq_min : ∀ (a b : Nat), a - (a - b) = min a b
   | 0, _ => by rw [Nat.zero_sub, Nat.zero_min]
   | _, 0 => by rw [Nat.sub_zero, Nat.sub_self, Nat.min_zero]
@@ -284,6 +295,17 @@ protected theorem max_assoc : ∀ (a b c : Nat), max (max a b) c = max a (max b
   | _+1, _+1, _+1 => by simp only [Nat.succ_max_succ]; exact congrArg succ <| Nat.max_assoc ..
 instance : Std.Associative (α := Nat) max := ⟨Nat.max_assoc⟩
 
+@[simp] theorem max_add_left {a b : Nat} : max a (b + a) = b + a := by
+  rw [Nat.max_def]
+  simp
+@[simp] theorem max_add_right {a b : Nat} : max a (a + b) = a + b := by
+  rw [Nat.max_def]
+  simp
+@[simp] theorem add_left_max {a b : Nat} : max (b + a) a = b + a := by
+  rw [Nat.max_comm, max_add_left]
+@[simp] theorem add_right_max {a b : Nat} : max (a + b) a = a + b := by
+  rw [Nat.max_comm, max_add_right]
+
 protected theorem sub_add_eq_max (a b : Nat) : a - b + b = max a b := by
   match Nat.le_total a b with
   | .inl hl => rw [Nat.max_eq_right hl, Nat.sub_eq_zero_iff_le.mpr hl, Nat.zero_add]

src/Init/Data/Option/Lemmas.lean

@@ -14,7 +14,7 @@ namespace Option
 
 theorem mem_iff {a : α} {b : Option α} : a ∈ b ↔ b = some a := .rfl
 
-@[simp] theorem mem_some {a b : α} : a ∈ some b ↔ b = a := by simp [mem_iff]
+theorem mem_some {a b : α} : a ∈ some b ↔ b = a := by simp
 
 theorem mem_some_self (a : α) : a ∈ some a := mem_some.2 rfl
 
@@ -231,7 +231,7 @@ theorem isSome_filter_of_isSome (p : α → Bool) (o : Option α) (h : (o.filter
     o.isSome := by
   cases o <;> simp at h ⊢
 
-@[simp] theorem filter_eq_none (p : α → Bool) :
+@[simp] theorem filter_eq_none {p : α → Bool} :
     Option.filter p o = none ↔ o = none ∨ ∀ a, a ∈ o → ¬ p a := by
   cases o <;> simp [filter_some]
 
@@ -448,22 +448,6 @@ end beq
 /-! ### ite -/
 section ite
 
-@[simp] theorem mem_dite_none_left {x : α} [Decidable p] {l : ¬ p → Option α} :
-    (x ∈ if h : p then none else l h) ↔ ∃ h : ¬ p, x ∈ l h := by
-  split <;> simp_all
-
-@[simp] theorem mem_dite_none_right {x : α} [Decidable p] {l : p → Option α} :
-    (x ∈ if h : p then l h else none) ↔ ∃ h : p, x ∈ l h := by
-  split <;> simp_all
-
-@[simp] theorem mem_ite_none_left {x : α} [Decidable p] {l : Option α} :
-    (x ∈ if p then none else l) ↔ ¬ p ∧ x ∈ l := by
-  split <;> simp_all
-
-@[simp] theorem mem_ite_none_right {x : α} [Decidable p] {l : Option α} :
-    (x ∈ if p then l else none) ↔ p ∧ x ∈ l := by
-  split <;> simp_all
-
 @[simp] theorem dite_none_left_eq_some {p : Prop} [Decidable p] {b : ¬p → Option β} :
     (if h : p then none else b h) = some a ↔ ∃ h, b h = some a := by
   split <;> simp_all
@@ -496,6 +480,22 @@ section ite
     some a = (if p then b else none) ↔ p ∧ some a = b := by
   split <;> simp_all
 
+theorem mem_dite_none_left {x : α} [Decidable p] {l : ¬ p → Option α} :
+    (x ∈ if h : p then none else l h) ↔ ∃ h : ¬ p, x ∈ l h := by
+  simp
+
+theorem mem_dite_none_right {x : α} [Decidable p] {l : p → Option α} :
+    (x ∈ if h : p then l h else none) ↔ ∃ h : p, x ∈ l h := by
+  simp
+
+theorem mem_ite_none_left {x : α} [Decidable p] {l : Option α} :
+    (x ∈ if p then none else l) ↔ ¬ p ∧ x ∈ l := by
+  simp
+
+theorem mem_ite_none_right {x : α} [Decidable p] {l : Option α} :
+    (x ∈ if p then l else none) ↔ p ∧ x ∈ l := by
+  simp
+
 @[simp] theorem isSome_dite {p : Prop} [Decidable p] {b : p → β} :
     (if h : p then some (b h) else none).isSome = true ↔ p := by
   split <;> simpa

src/Init/Meta.lean

@@ -7,7 +7,7 @@ Additional goodies for writing macros
 -/
 prelude
 import Init.MetaTypes
-import Init.Data.Array.Basic
+import Init.Data.Array.GetLit
 import Init.Data.Option.BasicAux
 
 namespace Lean

src/Init/SimpLemmas.lean

@@ -231,8 +231,21 @@ instance : Std.Associative (· || ·) := ⟨Bool.or_assoc⟩
 @[simp] theorem Bool.not_false : (!false) = true := by decide
 @[simp] theorem beq_true  (b : Bool) : (b == true)  =  b := by cases b <;> rfl
 @[simp] theorem beq_false (b : Bool) : (b == false) = !b := by cases b <;> rfl
-@[simp] theorem Bool.not_eq_true'  (b : Bool) : ((!b) = true) = (b = false) := by cases b <;> simp
-@[simp] theorem Bool.not_eq_false' (b : Bool) : ((!b) = false) = (b = true) := by cases b <;> simp
+
+
+/--
+We move `!` from the left hand side of an equality to the right hand side.
+This helps confluence, and also helps combining pairs of `!`s.
+-/
+@[simp] theorem Bool.not_eq_eq_eq_not {a b : Bool} : ((!a) = b) ↔ (a = !b) := by
+  cases a <;> cases b <;> simp
+
+@[simp] theorem Bool.not_eq_not {a b : Bool} : ¬a = !b ↔ a = b := by
+  cases a <;> cases b <;> simp
+theorem Bool.not_not_eq {a b : Bool} : ¬(!a) = b ↔ a = b := by simp
+
+theorem Bool.not_eq_true'  (b : Bool) : ((!b) = true) = (b = false) := by simp
+theorem Bool.not_eq_false' (b : Bool) : ((!b) = false) = (b = true) := by simp
 
 @[simp] theorem Bool.not_eq_true (b : Bool) : (¬(b = true)) = (b = false) := by cases b <;> decide
 @[simp] theorem Bool.not_eq_false (b : Bool) : (¬(b = false)) = (b = true) := by cases b <;> decide

src/Init/Tactics.lean

@@ -773,8 +773,9 @@ macro_rules
 macro "refine_lift' " e:term : tactic => `(tactic| focus (refine' no_implicit_lambda% $e; rotate_right))
 /-- Similar to `have`, but using `refine'` -/
 macro "have' " d:haveDecl : tactic => `(tactic| refine_lift' have $d:haveDecl; ?_)
-/-- Similar to `have`, but using `refine'` -/
+set_option linter.missingDocs false in -- OK, because `tactic_alt` causes inheritance of docs
 macro (priority := high) "have'" x:ident " := " p:term : tactic => `(tactic| have' $x:ident : _ := $p)
+attribute [tactic_alt tacticHave'_] «tacticHave'_:=_»
 /-- Similar to `let`, but using `refine'` -/
 macro "let' " d:letDecl : tactic => `(tactic| refine_lift' let $d:letDecl; ?_)
 

src/Lean/Elab/InfoTree/Main.lean

@@ -183,7 +183,7 @@ def UserWidgetInfo.format (info : UserWidgetInfo) : Format :=
   f!"UserWidget {info.id}\n{Std.ToFormat.format <| info.props.run' {}}"
 
 def FVarAliasInfo.format (info : FVarAliasInfo) : Format :=
-  f!"FVarAlias {info.userName.eraseMacroScopes}"
+  f!"FVarAlias {info.userName.eraseMacroScopes}: {info.id.name} -> {info.baseId.name}"
 
 def FieldRedeclInfo.format (ctx : ContextInfo) (info : FieldRedeclInfo) : Format :=
   f!"FieldRedecl @ {formatStxRange ctx info.stx}"

src/Lean/Elab/Tactic/BVDecide/Frontend/BVCheck.lean

@@ -41,9 +41,9 @@ def lratChecker (cfg : TacticContext) (bvExpr : BVLogicalExpr) : MetaM Expr := d
 
 @[inherit_doc Lean.Parser.Tactic.bvCheck]
 def bvCheck (g : MVarId) (cfg : TacticContext) : MetaM Unit := do
-  let unsatProver : UnsatProver := fun bvExpr _ => do
+  let unsatProver : UnsatProver := fun reflectionResult _ => do
     withTraceNode `sat (fun _ => return "Preparing LRAT reflection term") do
-      let proof ← lratChecker cfg bvExpr
+      let proof ← lratChecker cfg reflectionResult.bvExpr
       return ⟨proof, ""⟩
   let _ ← closeWithBVReflection g unsatProver
   return ()

src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide.lean

@@ -74,19 +74,111 @@ def reconstructCounterExample (var2Cnf : Std.HashMap BVBit Nat) (assignment : Ar
     finalMap := finalMap.push (atomExpr, ⟨BitVec.ofNat currentBit value⟩)
   return finalMap
 
+structure ReflectionResult where
+  bvExpr : BVLogicalExpr
+  proveFalse : Expr → M Expr
+  unusedHypotheses : Std.HashSet FVarId
+
 structure UnsatProver.Result where
   proof : Expr
   lratCert : LratCert
 
-abbrev UnsatProver := BVLogicalExpr → Std.HashMap Nat Expr → MetaM UnsatProver.Result
+abbrev UnsatProver := ReflectionResult → Std.HashMap Nat Expr → MetaM UnsatProver.Result
 
-def lratBitblaster (cfg : TacticContext) (bv : BVLogicalExpr)
+/--
+Contains values that will be used to diagnose spurious counter examples.
+-/
+structure DiagnosisInput where
+  unusedHypotheses : Std.HashSet FVarId
+  atomsAssignment : Std.HashMap Nat Expr
+
+/--
+The result of a spurious counter example diagnosis.
+-/
+structure Diagnosis where
+  uninterpretedSymbols : Std.HashSet Expr := {}
+  unusedRelevantHypotheses : Std.HashSet FVarId := {}
+
+abbrev DiagnosisM : Type → Type := ReaderT DiagnosisInput <| StateRefT Diagnosis MetaM
+
+namespace DiagnosisM
+
+def run (x : DiagnosisM Unit) (unusedHypotheses : Std.HashSet FVarId)
+    (atomsAssignment : Std.HashMap Nat Expr) : MetaM Diagnosis := do
+  let (_, issues) ← ReaderT.run x { unusedHypotheses, atomsAssignment } |>.run {}
+  return issues
+
+def unusedHyps : DiagnosisM (Std.HashSet FVarId) := do
+  return (← read).unusedHypotheses
+
+def atomsAssignment : DiagnosisM (Std.HashMap Nat Expr) := do
+  return (← read).atomsAssignment
+
+def addUninterpretedSymbol (e : Expr) : DiagnosisM Unit :=
+  modify fun s => { s with uninterpretedSymbols := s.uninterpretedSymbols.insert e }
+
+def addUnusedRelevantHypothesis (fvar : FVarId) : DiagnosisM Unit :=
+  modify fun s => { s with unusedRelevantHypotheses := s.unusedRelevantHypotheses.insert fvar }
+
+def checkRelevantHypsUsed (fvar : FVarId) : DiagnosisM Unit := do
+  for hyp in ← unusedHyps do
+    if (← hyp.getType).containsFVar fvar then
+      addUnusedRelevantHypothesis hyp
+
+/--
+Diagnose spurious counter examples, currently this checks:
+- Whether uninterpreted symbols were used
+- Whether all hypotheses which contain any variable that was bitblasted were included
+-/
+def diagnose : DiagnosisM Unit := do
+  for (_, expr) in ← atomsAssignment do
+    match_expr expr with
+    | BitVec.ofBool x =>
+      match x with
+      | .fvar fvarId => checkRelevantHypsUsed fvarId
+      | _ => addUninterpretedSymbol expr
+    | _ =>
+      match expr with
+      | .fvar fvarId => checkRelevantHypsUsed fvarId
+      | _ => addUninterpretedSymbol expr
+
+end DiagnosisM
+
+def uninterpretedExplainer (d : Diagnosis) : Option MessageData := do
+  guard !d.uninterpretedSymbols.isEmpty
+  let symList := d.uninterpretedSymbols.toList
+  return m!"It abstracted the following unsupported expressions as opaque variables: {symList}"
+
+def unusedRelevantHypothesesExplainer (d : Diagnosis) : Option MessageData := do
+  guard !d.unusedRelevantHypotheses.isEmpty
+  let hypList := d.unusedRelevantHypotheses.toList.map mkFVar
+  return m!"The following potentially relevant hypotheses could not be used: {hypList}"
+
+def explainers : List (Diagnosis → Option MessageData) :=
+  [uninterpretedExplainer, unusedRelevantHypothesesExplainer]
+
+def explainCounterExampleQuality (unusedHypotheses : Std.HashSet FVarId)
+    (atomsAssignment : Std.HashMap Nat Expr) : MetaM MessageData := do
+  let diagnosis ← DiagnosisM.run DiagnosisM.diagnose unusedHypotheses atomsAssignment
+  let folder acc explainer := if let some m := explainer diagnosis then acc.push m else acc
+  let explanations := explainers.foldl (init := #[]) folder
+
+  if explanations.isEmpty then
+    return m!"The prover found a counterexample, consider the following assignment:\n"
+  else
+    let mut err := m!"The prover found a potentially spurious counterexample:\n"
+    err := err ++ explanations.foldl (init := m!"") (fun acc exp => acc ++ m!"- " ++ exp ++ m!"\n")
+    err := err ++ m!"Consider the following assignment:\n"
+    return err
+
+def lratBitblaster (cfg : TacticContext) (reflectionResult : ReflectionResult)
     (atomsAssignment : Std.HashMap Nat Expr) :
     MetaM UnsatProver.Result := do
+  let bvExpr := reflectionResult.bvExpr
   let entry ←
     withTraceNode `bv (fun _ => return "Bitblasting BVLogicalExpr to AIG") do
       -- lazyPure to prevent compiler lifting
-      IO.lazyPure (fun _ => bv.bitblast)
+      IO.lazyPure (fun _ => bvExpr.bitblast)
   let aigSize := entry.aig.decls.size
   trace[Meta.Tactic.bv] s!"AIG has {aigSize} nodes."
 
@@ -108,18 +200,25 @@ def lratBitblaster (cfg : TacticContext) (bv : BVLogicalExpr)
 
   match res with
   | .ok cert =>
-    let proof ← cert.toReflectionProof cfg bv ``verifyBVExpr ``unsat_of_verifyBVExpr_eq_true
+    let proof ← cert.toReflectionProof cfg bvExpr ``verifyBVExpr ``unsat_of_verifyBVExpr_eq_true
     return ⟨proof, cert⟩
   | .error assignment =>
     let reconstructed := reconstructCounterExample map assignment aigSize atomsAssignment
-    let mut error := m!"The prover found a potential counterexample, consider the following assignment:\n"
+    let mut error ← explainCounterExampleQuality reflectionResult.unusedHypotheses atomsAssignment
     for (var, value) in reconstructed do
       error := error ++ m!"{var} = {value.bv}\n"
     throwError error
 
-def reflectBV (g : MVarId) : M (BVLogicalExpr × (Expr → M Expr)) := g.withContext do
-  let hyps ← getLocalHyps
-  let sats ← hyps.filterMapM SatAtBVLogical.of
+
+def reflectBV (g : MVarId) : M ReflectionResult := g.withContext do
+  let hyps ← getPropHyps
+  let mut sats := #[]
+  let mut unusedHypotheses := {}
+  for hyp in hyps do
+    if let some reflected ← SatAtBVLogical.of (mkFVar hyp) then
+      sats := sats.push reflected
+    else
+      unusedHypotheses := unusedHypotheses.insert hyp
   if sats.size = 0 then
     let mut error := "None of the hypotheses are in the supported BitVec fragment.\n"
     error := error ++ "There are two potential fixes for this:\n"
@@ -128,27 +227,32 @@ def reflectBV (g : MVarId) : M (BVLogicalExpr × (Expr → M Expr)) := g.withCon
     error := error ++ "   Consider expressing it in terms of different operations that are better supported."
     throwError error
   let sat := sats.foldl (init := SatAtBVLogical.trivial) SatAtBVLogical.and
-  return (sat.bvExpr, sat.proveFalse)
+  return {
+    bvExpr := sat.bvExpr,
+    proveFalse := sat.proveFalse,
+    unusedHypotheses := unusedHypotheses
+  }
+
 
 def closeWithBVReflection (g : MVarId) (unsatProver : UnsatProver) :
     MetaM LratCert := M.run do
   g.withContext do
-    let (bvLogicalExpr, f) ←
+    let reflectionResult ←
       withTraceNode `bv (fun _ => return "Reflecting goal into BVLogicalExpr") do
         reflectBV g
-    trace[Meta.Tactic.bv] "Reflected bv logical expression: {bvLogicalExpr}"
+    trace[Meta.Tactic.bv] "Reflected bv logical expression: {reflectionResult.bvExpr}"
 
     let atomsPairs := (← getThe State).atoms.toList.map (fun (expr, _, ident) => (ident, expr))
     let atomsAssignment := Std.HashMap.ofList atomsPairs
-    let ⟨bvExprUnsat, cert⟩ ← unsatProver bvLogicalExpr atomsAssignment
-    let proveFalse ← f bvExprUnsat
+    let ⟨bvExprUnsat, cert⟩ ← unsatProver reflectionResult atomsAssignment
+    let proveFalse ← reflectionResult.proveFalse bvExprUnsat
     g.assign proveFalse
     return cert
 
 def bvUnsat (g : MVarId) (cfg : TacticContext) : MetaM LratCert := M.run do
-  let unsatProver : UnsatProver := fun bvExpr atomsAssignment => do
+  let unsatProver : UnsatProver := fun reflectionResult atomsAssignment => do
     withTraceNode `bv (fun _ => return "Preparing LRAT reflection term") do
-      lratBitblaster cfg bvExpr atomsAssignment
+      lratBitblaster cfg reflectionResult atomsAssignment
   closeWithBVReflection g unsatProver
 
 structure Result where

src/Lean/Elab/Tactic/Omega/Frontend.lean

@@ -422,10 +422,11 @@ partial def addFact (p : MetaProblem) (h : Expr) : OmegaM (MetaProblem × Nat) :
     trace[omega] "adding fact: {t}"
     match t with
     | .forallE _ x y _ =>
-      if (← isProp x) && (← isProp y) then
+      if ← pure t.isArrow <&&> isProp x <&&> isProp y then
         p.addFact (mkApp4 (.const ``Decidable.not_or_of_imp []) x y
           (.app (.const ``Classical.propDecidable []) x) h)
       else
+        trace[omega] "rejecting forall: it's not an arrow, or not propositional"
         return (p, 0)
     | .app _ _ =>
       match_expr t with

src/Lean/Linter/UnusedVariables.lean

@@ -447,7 +447,10 @@ def unusedVariables : Linter where
     let fvarAliases : Std.HashMap FVarId FVarId := s.fvarAliases.fold (init := {}) fun m id baseId =>
       m.insert id (followAliases s.fvarAliases baseId)
 
+    let getCanonVar (id : FVarId) : FVarId := fvarAliases.getD id id
+
     -- Collect all non-alias fvars corresponding to `fvarUses` by resolving aliases in the list.
+    -- Unlike `s.fvarUses`, `fvarUsesRef` is guaranteed to contain no aliases.
     let fvarUsesRef ← IO.mkRef <| fvarAliases.fold (init := s.fvarUses) fun fvarUses id baseId =>
       if fvarUses.contains id then fvarUses.insert baseId else fvarUses
 
@@ -461,7 +464,7 @@ def unusedVariables : Linter where
       let fvarUses ← fvarUsesRef.get
       -- If any of the `fvar`s corresponding to this declaration is (an alias of) a variable in
       -- `fvarUses`, then it is used
-      if aliases.any fun id => fvarUses.contains (fvarAliases.getD id id) then continue
+      if aliases.any fun id => fvarUses.contains (getCanonVar id) then continue
       -- If this is a global declaration then it is (potentially) used after the command
       if s.constDecls.contains range then continue
 
@@ -493,10 +496,12 @@ def unusedVariables : Linter where
       if !initializedMVars then
         -- collect additional `fvarUses` from tactic assignments
         visitAssignments (← IO.mkRef {}) fvarUsesRef s.assignments
+        -- Resolve potential aliases again to preserve `fvarUsesRef` invariant
+        fvarUsesRef.modify fun fvarUses => fvarUses.fold (·.insert <| getCanonVar ·) {}
         initializedMVars := true
         let fvarUses ← fvarUsesRef.get
         -- Redo the initial check because `fvarUses` could be bigger now
-        if aliases.any fun id => fvarUses.contains (fvarAliases.getD id id) then continue
+        if aliases.any fun id => fvarUses.contains (getCanonVar id) then continue
 
       -- If we made it this far then the variable is unused and not ignored
       unused := unused.push (declStx, userName)

src/Lean/Meta/Tactic/Simp/BuiltinSimprocs/BitVec.lean

@@ -51,7 +51,7 @@ Helper function for reducing homogenous binary bitvector operators.
   else
     return .continue
 
-/-- Simplification procedure for `zeroExtend` and `signExtend` on `BitVec`s. -/
+/-- Simplification procedure for `setWidth`, `zeroExtend` and `signExtend` on `BitVec`s. -/
 @[inline] def reduceExtend (declName : Name)
     (op : {n : Nat} → (m : Nat) → BitVec n → BitVec m) (e : Expr) : SimpM DStep := do
   unless e.isAppOfArity declName 3 do return .continue
@@ -253,13 +253,13 @@ builtin_dsimproc [simp, seval] reduceSLT (BitVec.slt _ _) :=
 builtin_dsimproc [simp, seval] reduceSLE (BitVec.sle _ _) :=
   reduceBoolPred ``BitVec.sle 3 BitVec.sle
 
-/-- Simplification procedure for `zeroExtend'` on `BitVec`s. -/
-builtin_dsimproc [simp, seval] reduceZeroExtend' (zeroExtend' _ _) := fun e => do
-  let_expr zeroExtend' _ w _ v ← e | return .continue
+/-- Simplification procedure for `setWidth'` on `BitVec`s. -/
+builtin_dsimproc [simp, seval] reduceSetWidth' (setWidth' _ _) := fun e => do
+  let_expr setWidth' _ w _ v ← e | return .continue
   let some v ← fromExpr? v | return .continue
   let some w ← Nat.fromExpr? w | return .continue
   if h : v.n ≤ w then
-    return .done <| toExpr (v.value.zeroExtend' h)
+    return .done <| toExpr (v.value.setWidth' h)
   else
     return .continue
 
@@ -285,6 +285,9 @@ builtin_dsimproc [simp, seval] reduceReplicate (replicate _ _) := fun e => do
   let some i ← Nat.fromExpr? i | return .continue
   return .done <| toExpr (v.value.replicate i)
 
+/-- Simplification procedure for `setWidth` on `BitVec`s. -/
+builtin_dsimproc [simp, seval] reduceSetWidth (setWidth _ _) := reduceExtend ``setWidth setWidth
+
 /-- Simplification procedure for `zeroExtend` on `BitVec`s. -/
 builtin_dsimproc [simp, seval] reduceZeroExtend (zeroExtend _ _) := reduceExtend ``zeroExtend zeroExtend
 

src/Lean/Util/ShareCommon.lean

@@ -5,19 +5,18 @@ Authors: Leonardo de Moura
 -/
 prelude
 import Init.ShareCommon
-import Lean.Data.HashSet
-import Lean.Data.HashMap
+import Std.Data.HashSet
+import Std.Data.HashMap
 import Lean.Data.PersistentHashMap
 import Lean.Data.PersistentHashSet
 
 open ShareCommon
 namespace Lean.ShareCommon
 
-set_option linter.deprecated false in
 def objectFactory :=
   StateFactory.mk {
-    Map := HashMap, mkMap := (mkHashMap ·), mapFind? := (·.find?), mapInsert := (·.insert)
-    Set := HashSet, mkSet := (mkHashSet ·), setFind? := (·.find?), setInsert := (·.insert)
+    Map := Std.HashMap, mkMap := (Std.HashMap.empty ·), mapFind? := (·.get?), mapInsert := (·.insert)
+    Set := Std.HashSet, mkSet := (Std.HashSet.empty ·), setFind? := (·.get?), setInsert := (·.insert)
   }
 
 def persistentObjectFactory :=

src/Std/Sat/AIG/CNF.lean

@@ -67,7 +67,7 @@ theorem atomToCNF_eval :
 theorem gateToCNF_eval :
     (gateToCNF output lhs rhs linv rinv).eval assign
       =
-    (assign output == ((xor (assign lhs) linv) && (xor (assign rhs) rinv))) := by
+    (assign output == (((assign lhs) ^^ linv) && ((assign rhs) ^^ rinv))) := by
   simp only [CNF.eval, gateToCNF, CNF.Clause.eval, List.all_cons, List.any_cons, beq_false,
     List.any_nil, Bool.or_false, beq_true, List.all_nil, Bool.and_true]
   cases assign output

src/Std/Sat/AIG/CachedGatesLemmas.lean

@@ -32,7 +32,7 @@ private theorem or_as_aig : ∀ (a b : Bool), (!(!a && !b)) = (a || b) := by
 /--
 Encoding of XOR as boolean expression in AIG form.
 -/
-private theorem xor_as_aig : ∀ (a b : Bool), (!(a && b) && !(!a && !b)) = (xor a b) := by
+private theorem xor_as_aig : ∀ (a b : Bool), (!(a && b) && !(!a && !b)) = (a ^^ b) := by
   decide
 
 /--

src/Std/Sat/AIG/Lemmas.lean

@@ -92,11 +92,7 @@ instance : LawfulOperator α GateInput mkGate where
 theorem denote_mkGate {aig : AIG α} {input : GateInput aig} :
     ⟦aig.mkGate input, assign⟧
       =
-    (
-      (xor ⟦aig, input.lhs.ref, assign⟧ input.lhs.inv)
-        &&
-      (xor ⟦aig, input.rhs.ref, assign⟧ input.rhs.inv)
-    ) := by
+    ((⟦aig, input.lhs.ref, assign⟧ ^^ input.lhs.inv) && (⟦aig, input.rhs.ref, assign⟧ ^^ input.rhs.inv)) := by
   conv =>
     lhs
     unfold denote denote.go
@@ -224,9 +220,9 @@ theorem denote_idx_gate {aig : AIG α} {hstart} (h : aig.decls[start] = .gate lh
     ⟦aig, ⟨start, hstart⟩, assign⟧
       =
     (
-      (xor ⟦aig, ⟨lhs, by have := aig.invariant hstart h; omega⟩, assign⟧ linv)
+      (⟦aig, ⟨lhs, by have := aig.invariant hstart h; omega⟩, assign⟧ ^^ linv)
         &&
-      (xor ⟦aig, ⟨rhs, by have := aig.invariant hstart h; omega⟩, assign⟧ rinv)
+      (⟦aig, ⟨rhs, by have := aig.invariant hstart h; omega⟩, assign⟧ ^^ rinv)
     ) := by
   unfold denote
   conv =>

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

@@ -67,7 +67,7 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) :
     simp [go, hidx, denote_blastVar]
   | zeroExtend v inner ih =>
     simp only [go, denote_blastZeroExtend, ih, dite_eq_ite, Bool.if_false_right,
-      eval_zeroExtend, BitVec.getLsbD_zeroExtend, hidx, decide_True, Bool.true_and,
+      eval_zeroExtend, BitVec.getLsbD_setWidth, hidx, decide_True, Bool.true_and,
       Bool.and_iff_right_iff_imp, decide_eq_true_eq]
     apply BitVec.lt_of_getLsbD
   | append lhs rhs lih rih =>
@@ -93,9 +93,9 @@ 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_not_zeroExtend_not_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_zeroExtend, hidx, decide_True, Bool.true_and, Bool.and_iff_right_iff_imp,
+            BitVec.getLsbD_setWidth, hidx, decide_True, Bool.true_and, Bool.and_iff_right_iff_imp,
             decide_eq_true_eq]
           apply BitVec.lt_of_getLsbD
         · subst heq

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

@@ -27,7 +27,7 @@ namespace blastAdd
 theorem denote_mkFullAdderOut (assign : α → Bool) (aig : AIG α) (input : FullAdderInput aig) :
     ⟦mkFullAdderOut aig input, assign⟧
       =
-    xor (xor ⟦aig, input.lhs, assign⟧ ⟦aig, input.rhs, assign⟧) ⟦aig, input.cin, assign⟧
+    ((⟦aig, input.lhs, assign⟧ ^^ ⟦aig, input.rhs, assign⟧) ^^ ⟦aig, input.cin, assign⟧)
     := by
   simp only [mkFullAdderOut, Ref.cast_eq, denote_mkXorCached, denote_projected_entry, Bool.bne_assoc,
     Bool.bne_left_inj]
@@ -37,10 +37,7 @@ theorem denote_mkFullAdderOut (assign : α → Bool) (aig : AIG α) (input : Ful
 theorem denote_mkFullAdderCarry (assign : α → Bool) (aig : AIG α) (input : FullAdderInput aig) :
     ⟦mkFullAdderCarry aig input, assign⟧
       =
-      ((xor
-          ⟦aig, input.lhs, assign⟧
-          ⟦aig, input.rhs, assign⟧) &&
-        ⟦aig, input.cin, assign⟧ ||
+      ((⟦aig, input.lhs, assign⟧ ^^ ⟦aig, input.rhs, assign⟧) && ⟦aig, input.cin, assign⟧ ||
        ⟦aig, input.lhs, assign⟧ && ⟦aig, input.rhs, assign⟧)
     := by
   simp only [mkFullAdderCarry, Ref.cast_eq, Int.reduceNeg, denote_mkOrCached,
@@ -133,7 +130,7 @@ theorem go_get (aig : AIG α) (curr : Nat) (hcurr : curr ≤ w) (cin : Ref aig)
 theorem atLeastTwo_eq_halfAdder (lhsBit rhsBit carry : Bool) :
     Bool.atLeastTwo lhsBit rhsBit carry
       =
-    (((xor lhsBit rhsBit) && carry) || (lhsBit && rhsBit)) := by
+    (((lhsBit ^^ rhsBit) && carry) || (lhsBit && rhsBit)) := by
   revert lhsBit rhsBit carry
   decide
 

src/Std/Tactic/BVDecide/Bitblast/BoolExpr/Basic.lean

@@ -33,7 +33,7 @@ def toString : Gate → String
 def eval : Gate → Bool → Bool → Bool
   | and => (· && ·)
   | or => (· || ·)
-  | xor => Bool.xor
+  | xor => (· ^^ ·)
   | beq => (· == ·)
   | imp => (!· || ·)
 

src/Std/Tactic/BVDecide/LRAT/Checker.lean

@@ -72,7 +72,7 @@ theorem check_sound (lratProof : Array IntAction) (cnf : CNF Nat) :
           simp [← h2, WellFormedAction]
         . simp only [Option.some.injEq] at h2
           simp [← h2, WellFormedAction]
-        . simp only [ite_some_none_eq_some] at h2
+        . simp only [Option.ite_none_right_eq_some, Option.some.injEq] at h2
           rcases h2 with ⟨hleft, hright⟩
           simp [WellFormedAction, hleft, ← hright, Clause.limplies_iff_mem]
       )

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

@@ -56,8 +56,8 @@ attribute [bv_normalize] BitVec.zero_add
 attribute [bv_normalize] BitVec.neg_zero
 attribute [bv_normalize] BitVec.sub_self
 attribute [bv_normalize] BitVec.sub_zero
-attribute [bv_normalize] BitVec.zeroExtend_eq
-attribute [bv_normalize] BitVec.zeroExtend_zero
+attribute [bv_normalize] BitVec.setWidth_eq
+attribute [bv_normalize] BitVec.setWidth_zero
 attribute [bv_normalize] BitVec.getLsbD_zero
 attribute [bv_normalize] BitVec.getLsbD_zero_length
 attribute [bv_normalize] BitVec.getLsbD_concat_zero
@@ -206,5 +206,17 @@ theorem BitVec.max_ult' (a : BitVec w) : (BitVec.ult (-1#w) a) = false := by
 
 attribute [bv_normalize] BitVec.replicate_zero_eq
 
+@[bv_normalize]
+theorem BitVec.ofBool_getLsbD (a : BitVec w) (i : Nat) :
+    BitVec.ofBool (a.getLsbD i) = a.extractLsb' i 1 := by
+  ext j
+  simp
+
+@[bv_normalize]
+theorem BitVec.ofBool_getElem (a : BitVec w) (i : Nat) (h : i < w) :
+    BitVec.ofBool a[i] = a.extractLsb' i 1 := by
+  rw [← BitVec.getLsbD_eq_getElem]
+  apply ofBool_getLsbD
+
 end Normalize
 end Std.Tactic.BVDecide

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

@@ -46,7 +46,7 @@ attribute [bv_normalize] Bool.and_self_left
 attribute [bv_normalize] Bool.and_self_right
 
 @[bv_normalize]
-theorem Bool.not_xor : ∀ (a b : Bool), !(xor a b) = (a == b) := by decide
+theorem Bool.not_xor : ∀ (a b : Bool), !(a ^^ b) = (a == b) := by decide
 
 end Normalize
 end Std.Tactic.BVDecide

src/Std/Tactic/BVDecide/Reflect.lean

@@ -126,7 +126,7 @@ theorem or_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs)
   simp[*]
 
 theorem xor_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :
-    (Bool.xor lhs' rhs') = (xor lhs rhs) := by
+    (lhs' ^^ rhs') = (lhs ^^ rhs) := by
   simp[*]
 
 theorem beq_congr (lhs rhs lhs' rhs' : Bool) (h1 : lhs' = lhs) (h2 : rhs' = rhs) :

tests/bench/bv_decide_realworld.lean

@@ -29,7 +29,7 @@ def parity32_spec_rec (i : Nat) (x : BitVec 32) : Bool :=
   | 0 => false
   | i' + 1 =>
     let bit_idx := BitVec.getLsbD x i'
-    Bool.xor bit_idx (parity32_spec_rec i' x)
+    bit_idx ^^ (parity32_spec_rec i' x)
 
 def parity32_spec (x : BitVec 32) : Bool :=
   parity32_spec_rec 32 x

tests/lean/1018unknowMVarIssue.lean.expected.out

@@ -55,8 +55,8 @@ a : α
         • Fam2.any : Fam2 α α @ ⟨9, 4⟩†-⟨9, 12⟩†
           • α : Type @ ⟨9, 4⟩†-⟨9, 12⟩†
         • a (isBinder := true) : α @ ⟨8, 2⟩†-⟨10, 19⟩†
-        • FVarAlias a
-        • FVarAlias α
+        • FVarAlias a: _uniq.636 -> _uniq.312
+        • FVarAlias α: _uniq.635 -> _uniq.310
         • ?m x α a : α @ ⟨9, 18⟩-⟨9, 19⟩ @ Lean.Elab.Term.elabHole
         • [.] Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
         • Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
@@ -70,8 +70,8 @@ a : α
         • Fam2.nat n : Fam2 Nat Nat @ ⟨10, 4⟩†-⟨10, 14⟩
           • n (isBinder := true) : Nat @ ⟨10, 13⟩-⟨10, 14⟩
         • a (isBinder := true) : Nat @ ⟨8, 2⟩†-⟨10, 19⟩†
-        • FVarAlias a
-        • FVarAlias n
+        • FVarAlias a: _uniq.667 -> _uniq.312
+        • FVarAlias n: _uniq.666 -> _uniq.310
         • n : Nat @ ⟨10, 18⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabIdent
           • [.] n : some Nat @ ⟨10, 18⟩-⟨10, 19⟩
           • n : Nat @ ⟨10, 18⟩-⟨10, 19⟩

tests/lean/interactive/completionPrv.lean.expected.out

@@ -46,6 +46,30 @@
      "position": {"line": 9, "character": 11}},
     "id": {"const": {"declName": "BitVec.getMsbD_ofBoolListBE"}}}},
   {"sortText": "4",
+   "label": "BitVec.ofBool_and_ofBool",
+   "kind": 3,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionPrv.lean"},
+     "position": {"line": 9, "character": 11}},
+    "id": {"const": {"declName": "BitVec.ofBool_and_ofBool"}}}},
+  {"sortText": "5",
+   "label": "BitVec.ofBool_or_ofBool",
+   "kind": 3,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionPrv.lean"},
+     "position": {"line": 9, "character": 11}},
+    "id": {"const": {"declName": "BitVec.ofBool_or_ofBool"}}}},
+  {"sortText": "6",
+   "label": "BitVec.ofBool_xor_ofBool",
+   "kind": 3,
+   "data":
+   {"params":
+    {"textDocument": {"uri": "file:///completionPrv.lean"},
+     "position": {"line": 9, "character": 11}},
+    "id": {"const": {"declName": "BitVec.ofBool_xor_ofBool"}}}},
+  {"sortText": "7",
    "label": "BitVec.ofBoolListBE",
    "kind": 3,
    "documentation":

tests/lean/linterUnusedVariables.lean

@@ -250,6 +250,17 @@ example [ord : Ord β] (f : α → β) (x y : α) : Ordering := compare (f x) (f
 example {α β} [ord : Ord β] (f : α → β) (x y : α) : Ordering := compare (f x) (f y)
 example {h : Decidable True} (t e : α) : ite True t e = t := if_pos trivial
 
+inductive A where
+  | intro : Nat → A
+
+def A.out : A → Nat
+  | .intro n => n
+
+/-! `h` is used indirectly via an alias introduced by `match` that is used only via the mvar ctx -/
+theorem problematicAlias (n : A) (i : Nat) (h : i ≤ n.out) : i ≤ n.out :=
+  match n with
+  | .intro _ => by assumption
+
 /-!
 The wildcard pattern introduces a copy of `x` that should not be linted as it is in an
 inaccessible annotation.

tests/lean/run/5359.lean

@@ -0,0 +1,19 @@
+/-!
+Test that `Iff.rfl` is tried by the `rfl` tactic.
+-/
+universe u v w
+
+class L (F : Sort u) (α : outParam (Sort v)) (β : outParam (α → Sort w)) where
+  coe : F → ∀ a : α, β a
+
+instance {F : Sort u} {α : Sort v} {β : α → Sort w} [L F α β] :
+    CoeFun F (fun _ ↦ ∀ a : α, β a) where coe := @L.coe _ _ β _
+
+instance {π : Nat → Type u} [∀ i, LE (π i)] : LE (∀ i, π i) where le x y := ∀ i, x i ≤ y i
+
+structure S (α : Nat → Type u) where
+variable {α : Nat → Type u} [∀ i, LE (α i)]
+instance : L (S α) Nat α := sorry
+instance : LE (S α) := ⟨fun f g ↦ ∀ i, f i ≤ g i⟩
+
+example : ∀ {a b : S α}, L.coe a ≤ L.coe b ↔ a ≤ b := by rfl

tests/lean/run/bitvec_simproc.lean

@@ -99,7 +99,7 @@ example (h : x) : x = (3#3 ≥ 1#3) := by
   simp; guard_target =ₛ x; assumption
 example (h : ¬x) : x = (3#3 ≥ 4#3) := by
   simp; guard_target =ₛ ¬x; assumption
-example (h : x = (5 : BitVec 7)) : x = (5#3).zeroExtend' (by decide) := by
+example (h : x = (5 : BitVec 7)) : x = (5#3).setWidth' (by decide) := by
   simp; guard_target =ₛ x = 5#7; assumption
 example (h : x = (80 : BitVec 7)) : x = (5#3).shiftLeftZeroExtend 4 := by
   simp; guard_target =ₛ x = 80#7; assumption

tests/lean/run/bv_counterexample.lean

@@ -3,7 +3,7 @@ import Std.Tactic.BVDecide
 open BitVec
 
 /--
-error: The prover found a potential counterexample, consider the following assignment:
+error: The prover found a counterexample, consider the following assignment:
 x = 0xffffffffffffffff#64
 -/
 #guard_msgs in
@@ -11,7 +11,7 @@ example (x : BitVec 64) : x < x + 1 := by
   bv_decide
 
 /--
-error: The prover found a potential counterexample, consider the following assignment:
+error: The prover found a counterexample, consider the following assignment:
 x = 0x00000000000001ff#64
 -/
 #guard_msgs in
@@ -43,7 +43,7 @@ def optimized (x : BitVec 32) : BitVec 32 :=
     x &&& 0x0000004F
 
 /--
-error: The prover found a potential counterexample, consider the following assignment:
+error: The prover found a counterexample, consider the following assignment:
 x = 0xffffffff#32
 -/
 #guard_msgs in
@@ -53,7 +53,7 @@ example (x : BitVec 32) : pop_spec' x = optimized x := by
 
 -- limit the search domain
 /--
-error: The prover found a potential counterexample, consider the following assignment:
+error: The prover found a counterexample, consider the following assignment:
 x = 0x0007ffff#32
 -/
 #guard_msgs in
@@ -62,7 +62,7 @@ example (x : BitVec 32) (h1 : x < 0xfffff) : pop_spec' x = optimized x := by
   bv_decide
 
 /--
-error: The prover found a potential counterexample, consider the following assignment:
+error: The prover found a counterexample, consider the following assignment:
 x = 0x00000000#32
 y = 0x80000000#32
 ofBool a = 0x1#1
@@ -70,3 +70,41 @@ ofBool a = 0x1#1
 #guard_msgs in
 example (x y : BitVec 32) (a : Bool) (h : x < y) : (x = y) ↔ a := by
   bv_decide
+
+-- False counter examples but correctly detected as such.
+/--
+error: The prover found a potentially spurious counterexample:
+- The following potentially relevant hypotheses could not be used: [h]
+Consider the following assignment:
+x = 0xffffffff#32
+y = 0x7fffffff#32
+-/
+#guard_msgs in
+example (x y : BitVec 32) (h : x.toNat = y.toNat) : x = y := by
+  bv_decide
+
+def zeros (w : Nat) : BitVec w := 0#w
+
+/--
+error: The prover found a potentially spurious counterexample:
+- It abstracted the following unsupported expressions as opaque variables: [zeros 32]
+Consider the following assignment:
+x = 0xffffffff#32
+zeros 32 = 0xffffffff#32
+-/
+#guard_msgs in
+example (x : BitVec 32) (h : x = zeros 32) : x = 0 := by
+  bv_decide
+
+/--
+error: The prover found a potentially spurious counterexample:
+- It abstracted the following unsupported expressions as opaque variables: [zeros 32]
+- The following potentially relevant hypotheses could not be used: [h1]
+Consider the following assignment:
+x = 0xffffffff#32
+zeros 32 = 0xffffffff#32
+y = 0xffffffff#32
+-/
+#guard_msgs in
+example (x y : BitVec 32) (h1 : x.toNat = y.toNat) (h2 : x = zeros 32) : y = 0 := by
+  bv_decide

tests/lean/run/bv_extract.lean

@@ -13,3 +13,15 @@ theorem bv_extract_3 (h : x = 1#64) : extractLsb 63 32 x = 0#32 := by
 
 theorem bv_extract_4 (h : x = 1#64) : extractLsb 31 0 x = 1#32 := by
   bv_decide
+
+theorem bv_ofBool_1 (h : x = 1#64) : ofBool (x.getLsbD 0) = 1#1 := by
+  bv_decide
+
+theorem bv_ofBool_2 (h : x = 1#64) : ofBool (x.getLsbD 1) = 0#1 := by
+  bv_decide
+
+theorem bv_ofBool_3 (h : x = 1#64) : ofBool x[0] = 1#1 := by
+  bv_decide
+
+theorem bv_ofBool_4 (h : x = 1#64) : ofBool x[1] = 0#1 := by
+  bv_decide

tests/lean/run/bv_substructure.lean

@@ -14,7 +14,7 @@ theorem substructure_unit_1'' (x y z : BitVec 8) : (Bool.and (x = y) (y = z))
 theorem substructure_unit_2 (x y : BitVec 8) : x = y → y = x := by
   bv_decide
 
-theorem substructure_unit_3 (x y : BitVec 8) : xor (x = y) (y ≠ x) := by
+theorem substructure_unit_3 (x y : BitVec 8) : (x = y) ^^ (y ≠ x) := by
   bv_decide
 
 theorem substructure_unit_3' (x y : BitVec 8) : Bool.xor (x = y) (y ≠ x) := by

tests/lean/run/bv_unused.lean

@@ -3,7 +3,7 @@ import Std.Tactic.BVDecide
 open BitVec
 
 /--
-error: The prover found a potential counterexample, consider the following assignment:
+error: The prover found a counterexample, consider the following assignment:
 y = 0xffffffffffffffff#64
 -/
 #guard_msgs in

tests/lean/run/dsimp_bv_simproc.lean

@@ -7,7 +7,7 @@ theorem write_simplify_test_0 (a x y : BitVec 64)
   write (2 * ((8 * 8) / 8)) a (BitVec.cast h (zeroExtend (8 * 8) x ++ (zeroExtend (8 * 8) y))) s
   =
   write 16 a (x ++ y) s := by
-  simp only [zeroExtend_eq, BitVec.cast_eq]
+  simp only [setWidth_eq, BitVec.cast_eq]
 
 /--
 warning: declaration uses 'sorry'

tests/lean/run/omega.lean

@@ -506,6 +506,54 @@ example
     n = 65536 := by
   bv_omega
 
+-- From https://github.com/leanprover/lean4/issues/5315
+-- This used to fail with an unexpected bound variable error.
+
+def simple_foldl (f: β → α → β) (a: Array α) (i: Nat) (b: β): β :=
+  if h: i < a.size then
+    simple_foldl f a (i+1) (f b a[i])
+  else
+    b
+
+/--
+error: omega could not prove the goal:
+No usable constraints found. You may need to unfold definitions so `omega` can see linear arithmetic facts about `Nat` and `Int`, which may also involve multiplication, division, and modular remainder by constants.
+-/
+#guard_msgs in
+theorem simple_fold_monotonic₁ (a: Array α) (f: β → α → β) (i: Nat) {P: α → β → Prop} {x: α}
+  (base: P x b)
+  (mono: ∀ x x' y, P x y → P x (f y x')): P x (simple_foldl f a i b) := by
+    unfold simple_foldl
+    split <;> try trivial
+    apply simple_fold_monotonic₁
+    . apply mono; exact base
+    . exact mono
+  termination_by a.size - i
+  decreasing_by
+    exfalso
+    rename_i a b
+    clear a b mono base
+    rename_i a; clear a
+    clear base
+    clear x
+    rename_i a; clear a
+    clear x
+    clear P
+    rename_i a; clear a
+    clear P
+    clear i
+    rename_i a; clear a
+    clear i
+    clear f
+    rename_i a; clear a
+    clear f
+    clear a
+    rename_i a; clear a
+    clear a
+    clear b
+    rename_i a
+    omega
+
 /-! ### Error messages -/
 
 /--

tests/lean/run/regressions3210.lean

@@ -21,13 +21,15 @@ example : Not
     (@OfNat.ofNat.{0} Nat (nat_lit 0) (instOfNatNat (nat_lit 0)))) := by
   simp
 
+@[simp] theorem OfNat.ofNat_ofNat : OfNat.ofNat (no_index OfNat.ofNat n) = OfNat.ofNat n := rfl
+
 example : Not
   (@Eq.{1} Nat
     (@HMod.hMod.{0, 0, 0} Nat Nat Nat (@instHMod.{0} Nat Nat.instMod)
       (@OfNat.ofNat.{0} Nat 1 (@One.toOfNat1.{0} Nat (@One.ofOfNat1.{0} Nat (instOfNatNat 1))))
       (@OfNat.ofNat.{0} Nat 2 (instOfNatNat 2)))
     (@OfNat.ofNat.{0} Nat 0 (instOfNatNat 0))) := by
-  simp
+  simp only [reduceCtorEq, not_false_eq_true]
 
 def WithTop (α : Type) := Option α
 

tests/lean/run/scopedParsers2.lean

@@ -16,15 +16,15 @@ namespace Foo
 
 def f x y := x + y + 1
 
-scoped infix:70 "^^" => f
+scoped infix:70 "~~" => f
 
-#check 1 ^^ 2
+#check 1 ~~ 2
 
-theorem ex1 : x ^^ y = f x y := rfl
+theorem ex1 : x ~~ y = f x y := rfl
 
 end Foo
 
-#check 1 ^^ 2 -- works because we have an `open Foo` above
+#check 1 ~~ 2 -- works because we have an `open Foo` above
 
-theorem ex2 : x ^^ y = f x y := rfl
-theorem ex3 : x ^^ y = Foo.f x y := rfl
+theorem ex2 : x ~~ y = f x y := rfl
+theorem ex3 : x ~~ y = Foo.f x y := rfl