chore: upstream List.modify, add lemmas, relate to Array.modify

feat: add BitVec.toInt_sub, simplify BitVec.toInt_neg (#5772 )
This also requires us to expand the theory of `Int.bmod`. --------- Co-authored-by: Alex Keizer <alex@keizer.dev>
2026-03-17 18:34:06 +00:00 · 2024-10-22 11:06:54 +11:00 · 2024-10-21 22:38:29 +00:00 · 2024-10-21 16:56:30 +00:00 · 2024-10-21 08:45:18 +00:00 · 2024-10-21 07:37:40 +00:00
42 changed files with 817 additions and 196 deletions
--- a/src/Init.lean
+++ b/src/Init.lean
@@ -35,3 +35,4 @@ import Init.Ext
 import Init.Omega
 import Init.MacroTrace
 import Init.Grind
+import Init.While
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -80,6 +80,26 @@ theorem ext' {as bs : Array α} (h : as.toList = bs.toList) : as = bs := by

@[simp] theorem size_toArray (as : List α) : as.toArray.size = as.length := by simp [size]

+@[simp] theorem getElem_toList {a : Array α} {i : Nat} (h : i < a.size) : a.toList[i] = a[i] := rfl
+
+end Array
+
+namespace List
+
+@[simp] theorem toArray_toList (a : Array α) : a.toList.toArray = a := rfl
+
+@[simp] theorem getElem_toArray {a : List α} {i : Nat} (h : i < a.toArray.size) :
+    a.toArray[i] = a[i]'(by simpa using h) := rfl
+
+@[simp] theorem getElem?_toArray {a : List α} {i : Nat} : a.toArray[i]? = a[i]? := rfl
+
+@[simp] theorem getElem!_toArray [Inhabited α] {a : List α} {i : Nat} :
+    a.toArray[i]! = a[i]! := rfl
+
+end List
+
+namespace Array
+
@[deprecated toList_toArray (since := "2024-09-09")] abbrev data_toArray := @toList_toArray

@[deprecated Array.toList (since := "2024-09-10")] abbrev Array.data := @Array.toList
@@ -398,20 +418,25 @@ def mapM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (f : α
  decreasing_by simp_wf; decreasing_trivial_pre_omega
  map 0 (mkEmpty as.size)

+/-- Variant of `mapIdxM` which receives the index as a `Fin as.size`. -/
@[inline]
-def mapIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : Fin as.size → α → m β) : m (Array β) :=
+def mapFinIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m]
+    (as : Array α) (f : Fin as.size → α → m β) : m (Array β) :=
  let rec @[specialize] map (i : Nat) (j : Nat) (inv : i + j = as.size) (bs : Array β) : m (Array β) := do
    match i, inv with
    | 0,    _  => pure bs
    | i+1, inv =>
-      have : j < as.size := by
+      have j_lt : j < as.size := by
        rw [← inv, Nat.add_assoc, Nat.add_comm 1 j, Nat.add_comm]
        apply Nat.le_add_right
-      let idx : Fin as.size := ⟨j, this⟩
      have : i + (j + 1) = as.size := by rw [← inv, Nat.add_comm j 1, Nat.add_assoc]
-      map i (j+1) this (bs.push (← f idx (as.get idx)))
+      map i (j+1) this (bs.push (← f ⟨j, j_lt⟩ (as.get ⟨j, j_lt⟩)))
  map as.size 0 rfl (mkEmpty as.size)

+@[inline]
+def mapIdxM {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : Nat → α → m β) : m (Array β) :=
+  as.mapFinIdxM fun i a => f i a
+
@[inline]
 def findSomeM? {α : Type u} {β : Type v} {m : Type v → Type w} [Monad m] (as : Array α) (f : α → m (Option β)) : m (Option β) := do
  for a in as do
@@ -517,8 +542,13 @@ def foldr {α : Type u} {β : Type v} (f : α → β → β) (init : β) (as : A
 def map {α : Type u} {β : Type v} (f : α → β) (as : Array α) : Array β :=
  Id.run <| as.mapM f

+/-- Variant of `mapIdx` which receives the index as a `Fin as.size`. -/
@[inline]
-def mapIdx {α : Type u} {β : Type v} (as : Array α) (f : Fin as.size → α → β) : Array β :=
+def mapFinIdx {α : Type u} {β : Type v} (as : Array α) (f : Fin as.size → α → β) : Array β :=
+  Id.run <| as.mapFinIdxM f
+
+@[inline]
+def mapIdx {α : Type u} {β : Type v} (as : Array α) (f : Nat → α → β) : Array β :=
  Id.run <| as.mapIdxM f

 /-- Turns `#[a, b]` into `#[(a, 0), (b, 1)]`. -/
--- a/src/Init/Data/Array/Bootstrap.lean
+++ b/src/Init/Data/Array/Bootstrap.lean
@@ -42,7 +42,7 @@ theorem foldrM_eq_reverse_foldlM_toList.aux [Monad m]
  unfold foldrM.fold
  match i with
  | 0 => simp [List.foldlM, List.take]
-  | i+1 => rw [← List.take_concat_get _ _ h]; simp [← (aux f arr · i)]; rfl
+  | i+1 => rw [← List.take_concat_get _ _ h]; simp [← (aux f arr · i)]

 theorem foldrM_eq_reverse_foldlM_toList [Monad m] (f : α → β → m β) (init : β) (arr : Array α) :
    arr.foldrM f init = arr.toList.reverse.foldlM (fun x y => f y x) init := by
--- a/src/Init/Data/Array/DecidableEq.lean
+++ b/src/Init/Data/Array/DecidableEq.lean
@@ -6,6 +6,8 @@ Authors: Leonardo de Moura
 prelude
 import Init.Data.Array.Basic
 import Init.Data.BEq
+import Init.Data.Nat.Lemmas
+import Init.Data.List.Nat.BEq
 import Init.ByCases

 namespace Array
@@ -26,6 +28,14 @@ theorem rel_of_isEqvAux
      subst hj'
      exact heqv.left

+theorem isEqvAux_of_rel (r : α → α → Bool) (a b : Array α) (hsz : a.size = b.size) (i : Nat) (hi : i ≤ a.size)
+    (w : ∀ j, (hj : j < i) → r (a[j]'(Nat.lt_of_lt_of_le hj hi)) (b[j]'(Nat.lt_of_lt_of_le hj (hsz ▸ hi)))) : Array.isEqvAux a b hsz r i hi := by
+  induction i with
+  | zero => simp [Array.isEqvAux]
+  | succ i ih =>
+    simp only [isEqvAux, Bool.and_eq_true]
+    exact ⟨w i (Nat.lt_add_one i), ih _ fun j hj => w j (Nat.lt_add_right 1 hj)⟩
+
 theorem rel_of_isEqv (r : α → α → Bool) (a b : Array α) :
    Array.isEqv a b r → ∃ h : a.size = b.size, ∀ (i : Nat) (h' : i < a.size), r (a[i]) (b[i]'(h ▸ h')) := by
  simp only [isEqv]
@@ -33,6 +43,29 @@ theorem rel_of_isEqv (r : α → α → Bool) (a b : Array α) :
  · exact fun h' => ⟨h, rel_of_isEqvAux r a b h a.size (Nat.le_refl ..) h'⟩
  · intro; contradiction

+theorem isEqv_iff_rel (a b : Array α) (r) :
+    Array.isEqv a b r ↔ ∃ h : a.size = b.size, ∀ (i : Nat) (h' : i < a.size), r (a[i]) (b[i]'(h ▸ h')) :=
+  ⟨rel_of_isEqv r a b, fun ⟨h, w⟩ => by
+    simp only [isEqv, ← h, ↓reduceDIte]
+    exact isEqvAux_of_rel r a b h a.size (by simp [h]) w⟩
+
+theorem isEqv_eq_decide (a b : Array α) (r) :
+    Array.isEqv a b r =
+      if h : a.size = b.size then decide (∀ (i : Nat) (h' : i < a.size), r (a[i]) (b[i]'(h ▸ h'))) else false := by
+  by_cases h : Array.isEqv a b r
+  · simp only [h, Bool.true_eq]
+    simp only [isEqv_iff_rel] at h
+    obtain ⟨h, w⟩ := h
+    simp [h, w]
+  · let h' := h
+    simp only [Bool.not_eq_true] at h
+    simp only [h, Bool.false_eq, dite_eq_right_iff, decide_eq_false_iff_not, Classical.not_forall,
+      Bool.not_eq_true]
+    simpa [isEqv_iff_rel] using h'
+
+@[simp] theorem isEqv_toList [BEq α] (a b : Array α) : (a.toList.isEqv b.toList r) = (a.isEqv b r) := by
+  simp [isEqv_eq_decide, List.isEqv_eq_decide]
+
 theorem eq_of_isEqv [DecidableEq α] (a b : Array α) (h : Array.isEqv a b (fun x y => x = y)) : a = b := by
  have ⟨h, h'⟩ := rel_of_isEqv (fun x y => x = y) a b h
  exact ext _ _ h (fun i lt _ => by simpa using h' i lt)
@@ -56,4 +89,22 @@ instance [DecidableEq α] : DecidableEq (Array α) :=
    | true  => isTrue (eq_of_isEqv a b h)
    | false => isFalse fun h' => by subst h'; rw [isEqv_self] at h; contradiction

+theorem beq_eq_decide [BEq α] (a b : Array α) :
+    (a == b) = if h : a.size = b.size then
+      decide (∀ (i : Nat) (h' : i < a.size), a[i] == b[i]'(h ▸ h')) else false := by
+  simp [BEq.beq, isEqv_eq_decide]
+
+@[simp] theorem beq_toList [BEq α] (a b : Array α) : (a.toList == b.toList) = (a == b) := by
+  simp [beq_eq_decide, List.beq_eq_decide]
+
 end Array
+
+namespace List
+
+@[simp] theorem isEqv_toArray [BEq α] (a b : List α) : (a.toArray.isEqv b.toArray r) = (a.isEqv b r) := by
+  simp [isEqv_eq_decide, Array.isEqv_eq_decide]
+
+@[simp] theorem beq_toArray [BEq α] (a b : List α) : (a.toArray == b.toArray) = (a == b) := by
+  simp [beq_eq_decide, Array.beq_eq_decide]
+
+end List
--- a/src/Init/Data/Array/GetLit.lean
+++ b/src/Init/Data/Array/GetLit.lean
@@ -41,6 +41,6 @@ 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, *]
+    induction i <;> simp only [List.drop, toListLitAux, getLit_eq, List.get_drop_eq_drop, *]

 end Array
--- a/src/Init/Data/Array/Lemmas.lean
+++ b/src/Init/Data/Array/Lemmas.lean
@@ -8,6 +8,8 @@ import Init.Data.Nat.Lemmas
 import Init.Data.List.Impl
 import Init.Data.List.Monadic
 import Init.Data.List.Range
+import Init.Data.List.Nat.TakeDrop
+import Init.Data.List.Nat.Modify
 import Init.Data.Array.Mem
 import Init.TacticsExtra

@@ -17,8 +19,6 @@ import Init.TacticsExtra

 namespace Array

-@[simp] theorem getElem_toList {a : Array α} {i : Nat} (h : i < a.size) : a.toList[i] = a[i] := rfl
-
@[simp] theorem getElem_mk {xs : List α} {i : Nat} (h : i < xs.length) : (Array.mk xs)[i] = xs[i] := rfl

 theorem getElem_eq_getElem_toList {a : Array α} (h : i < a.size) : a[i] = a.toList[i] := by
@@ -43,21 +43,32 @@ theorem getElem?_eq_getElem?_toList (a : Array α) (i : Nat) : a[i]? = a.toList[
  rw [getElem?_eq]
  split <;> simp_all

-theorem get_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
+theorem getElem_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
    have : i < (a.push x).size := by simp [*, Nat.lt_succ_of_le, Nat.le_of_lt]
    (a.push x)[i] = a[i] := by
  simp only [push, getElem_eq_getElem_toList, List.concat_eq_append, List.getElem_append_left, h]

-@[simp] theorem get_push_eq (a : Array α) (x : α) : (a.push x)[a.size] = x := by
+@[simp] theorem getElem_push_eq (a : Array α) (x : α) : (a.push x)[a.size] = x := by
  simp only [push, getElem_eq_getElem_toList, List.concat_eq_append]
  rw [List.getElem_append_right] <;> simp [getElem_eq_getElem_toList, Nat.zero_lt_one]

-theorem get_push (a : Array α) (x : α) (i : Nat) (h : i < (a.push x).size) :
+theorem getElem_push (a : Array α) (x : α) (i : Nat) (h : i < (a.push x).size) :
    (a.push x)[i] = if h : i < a.size then a[i] else x := by
  by_cases h' : i < a.size
-  · simp [get_push_lt, h']
+  · simp [getElem_push_lt, h']
  · simp at h
-    simp [get_push_lt, Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.ge_of_not_lt h')]
+    simp [getElem_push_lt, Nat.le_antisymm (Nat.le_of_lt_succ h) (Nat.ge_of_not_lt h')]
+
+@[deprecated getElem_push (since := "2024-10-21")] abbrev get_push := @getElem_push
+@[deprecated getElem_push_lt (since := "2024-10-21")] abbrev get_push_lt := @getElem_push_lt
+@[deprecated getElem_push_eq (since := "2024-10-21")] abbrev get_push_eq := @getElem_push_eq
+
+@[simp] theorem get!_eq_getElem! [Inhabited α] (a : Array α) (i : Nat) : a.get! i = a[i]! := by
+  simp [getElem!_def, get!, getD]
+  split <;> rename_i h
+  · simp [getElem?_eq_getElem h]
+    rfl
+  · simp [getElem?_eq_none_iff.2 (by simpa using h)]

 end Array

@@ -74,13 +85,6 @@ We prefer to pull `List.toArray` outwards.
    (a.toArrayAux b).size = b.size + a.length := by
  simp [size]

-@[simp] theorem toArray_toList (a : Array α) : a.toList.toArray = a := rfl
-
-@[simp] theorem getElem_toArray {a : List α} {i : Nat} (h : i < a.toArray.size) :
-    a.toArray[i] = a[i]'(by simpa using h) := rfl
-
-@[simp] theorem getElem?_toArray {a : List α} {i : Nat} : a.toArray[i]? = a[i]? := rfl
-
@[simp] theorem push_toArray (l : List α) (a : α) : l.toArray.push a = (l ++ [a]).toArray := by
  apply ext'
  simp
@@ -90,6 +94,14 @@ We prefer to pull `List.toArray` outwards.
  funext a
  simp

+@[simp] theorem isEmpty_toArray (l : List α) : l.toArray.isEmpty = l.isEmpty := by
+  cases l <;> simp
+
+@[simp] theorem toArray_singleton (a : α) : (List.singleton a).toArray = singleton a := rfl
+
+@[simp] theorem back_toArray [Inhabited α] (l : List α) : l.toArray.back = l.getLast! := by
+  simp only [back, size_toArray, Array.get!_eq_getElem!, getElem!_toArray, getLast!_eq_getElem!]
+
 theorem foldrM_toArray [Monad m] (f : α → β → m β) (init : β) (l : List α) :
    l.toArray.foldrM f init = l.foldrM f init := by
  rw [foldrM_eq_reverse_foldlM_toList]
@@ -147,6 +159,9 @@ namespace Array

@[simp] theorem singleton_def (v : α) : singleton v = #[v] := rfl

+-- This is a duplicate of `List.toArray_toList`.
+-- It's confusing to guess which namespace this theorem should live in,
+-- so we provide both.
@[simp] theorem toArray_toList (a : Array α) : a.toList.toArray = a := rfl

@[simp] theorem length_toList {l : Array α} : l.toList.length = l.size := rfl
@@ -248,7 +263,7 @@ theorem size_uset (a : Array α) (v i h) : (uset a i v h).size = a.size := by si
@[simp] theorem get_eq_getElem (a : Array α) (i : Fin _) : a.get i = a[i.1] := rfl

 theorem getElem?_lt
-    (a : Array α) {i : Nat} (h : i < a.size) : a[i]? = some (a[i]) := dif_pos h
+    (a : Array α) {i : Nat} (h : i < a.size) : a[i]? = some a[i] := dif_pos h

 theorem getElem?_ge
    (a : Array α) {i : Nat} (h : i ≥ a.size) : a[i]? = none := dif_neg (Nat.not_lt_of_le h)
@@ -271,8 +286,10 @@ theorem getD_get? (a : Array α) (i : Nat) (d : α) :

 theorem get!_eq_getD [Inhabited α] (a : Array α) : a.get! n = a.getD n default := rfl

-@[simp] theorem get!_eq_getElem? [Inhabited α] (a : Array α) (i : Nat) : a.get! i = (a.get? i).getD default := by
-  by_cases p : i < a.size <;> simp [getD_get?, get!_eq_getD, p]
+@[simp] theorem get!_eq_getElem? [Inhabited α] (a : Array α) (i : Nat) :
+    a.get! i = (a.get? i).getD default := by
+  by_cases p : i < a.size <;>
+  simp only [get!_eq_getD, getD_eq_get?, getD_get?, p, get?_eq_getElem?]

 /-! # set -/

@@ -352,8 +369,8 @@ theorem getElem_ofFn_go (f : Fin n → α) (i) {acc k}
    simp only [dif_pos hin]
    rw [getElem_ofFn_go f (i+1) _ hin (by simp [*]) (fun j hj => ?hacc)]
    cases (Nat.lt_or_eq_of_le <| Nat.le_of_lt_succ (by simpa using hj)) with
-    | inl hj => simp [get_push, hj, hacc j hj]
-    | inr hj => simp [get_push, *]
+    | inl hj => simp [getElem_push, hj, hacc j hj]
+    | inr hj => simp [getElem_push, *]
  else
    simp [hin, hacc k (Nat.lt_of_lt_of_le hki (Nat.le_of_not_lt (hi ▸ hin)))]
 termination_by n - i
@@ -421,7 +438,7 @@ theorem lt_of_getElem {x : α} {a : Array α} {idx : Nat} {hidx : idx < a.size}
    idx < a.size :=
  hidx

-theorem getElem_mem {l : Array α} {i : Nat} (h : i < l.size) : l[i] ∈ l := by
+@[simp] theorem getElem_mem {l : Array α} {i : Nat} (h : i < l.size) : l[i] ∈ l := by
  erw [Array.mem_def, getElem_eq_getElem_toList]
  apply List.get_mem

@@ -430,9 +447,11 @@ theorem getElem_fin_eq_getElem_toList (a : Array α) (i : Fin a.size) : a[i] = a
@[simp] theorem ugetElem_eq_getElem (a : Array α) {i : USize} (h : i.toNat < a.size) :
  a[i] = a[i.toNat] := rfl

-theorem get?_len_le (a : Array α) (i : Nat) (h : a.size ≤ i) : a[i]? = none := by
+theorem getElem?_size_le (a : Array α) (i : Nat) (h : a.size ≤ i) : a[i]? = none := by
  simp [getElem?_neg, h]

+@[deprecated getElem?_size_le (since := "2024-10-21")] abbrev get?_len_le := @getElem?_size_le
+
 theorem getElem_mem_toList (a : Array α) (h : i < a.size) : a[i] ∈ a.toList := by
  simp only [getElem_eq_getElem_toList, List.getElem_mem]

@@ -440,35 +459,39 @@ theorem get?_eq_get?_toList (a : Array α) (i : Nat) : a.get? i = a.toList.get?
  simp [getElem?_eq_getElem?_toList]

 theorem get!_eq_get? [Inhabited α] (a : Array α) : a.get! n = (a.get? n).getD default := by
-  simp [get!_eq_getD]
+  simp only [get!_eq_getElem?, get?_eq_getElem?]

 theorem getElem?_eq_some_iff {as : Array α} : as[n]? = some a ↔ ∃ h : n < as.size, as[n] = a := by
  cases as
  simp [List.getElem?_eq_some_iff]

@[simp] theorem back_eq_back? [Inhabited α] (a : Array α) : a.back = a.back?.getD default := by
-  simp [back, back?]
+  simp only [back, get!_eq_getElem?, get?_eq_getElem?, back?]

@[simp] theorem back?_push (a : Array α) : (a.push x).back? = some x := by
  simp [back?, getElem?_eq_getElem?_toList]

 theorem back_push [Inhabited α] (a : Array α) : (a.push x).back = x := by simp

-theorem get?_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
+theorem getElem?_push_lt (a : Array α) (x : α) (i : Nat) (h : i < a.size) :
    (a.push x)[i]? = some a[i] := by
-  rw [getElem?_pos, get_push_lt]
+  rw [getElem?_pos, getElem_push_lt]

-theorem get?_push_eq (a : Array α) (x : α) : (a.push x)[a.size]? = some x := by
-  rw [getElem?_pos, get_push_eq]
+@[deprecated getElem?_push_lt (since := "2024-10-21")] abbrev get?_push_lt := @getElem?_push_lt

-theorem get?_push {a : Array α} : (a.push x)[i]? = if i = a.size then some x else a[i]? := by
+theorem getElem?_push_eq (a : Array α) (x : α) : (a.push x)[a.size]? = some x := by
+  rw [getElem?_pos, getElem_push_eq]
+
+@[deprecated getElem?_push_eq (since := "2024-10-21")] abbrev get?_push_eq := @getElem?_push_eq
+
+theorem getElem?_push {a : Array α} : (a.push x)[i]? = if i = a.size then some x else a[i]? := by
  match Nat.lt_trichotomy i a.size with
  | Or.inl g =>
    have h1 : i < a.size + 1 := by omega
    have h2 : i ≠ a.size := by omega
-    simp [getElem?_def, size_push, g, h1, h2, get_push_lt]
+    simp [getElem?_def, size_push, g, h1, h2, getElem_push_lt]
  | Or.inr (Or.inl heq) =>
-    simp [heq, getElem?_pos, get_push_eq]
+    simp [heq, getElem?_pos, getElem_push_eq]
  | Or.inr (Or.inr g) =>
    simp only [getElem?_def, size_push]
    have h1 : ¬ (i < a.size) := by omega
@@ -476,9 +499,13 @@ theorem get?_push {a : Array α} : (a.push x)[i]? = if i = a.size then some x el
    have h3 : i ≠ a.size := by omega
    simp [h1, h2, h3]

-@[simp] theorem get?_size {a : Array α} : a[a.size]? = none := by
+@[deprecated getElem?_push (since := "2024-10-21")] abbrev get?_push := @getElem?_push
+
+@[simp] theorem getElem?_size {a : Array α} : a[a.size]? = none := by
  simp only [getElem?_def, Nat.lt_irrefl, dite_false]

+@[deprecated getElem?_size (since := "2024-10-21")] abbrev get?_size := @getElem?_size
+
@[simp] theorem toList_set (a : Array α) (i v) : (a.set i v).toList = a.toList.set i.1 v := rfl

 theorem get_set_eq (a : Array α) (i : Fin a.size) (v : α) :
@@ -528,6 +555,9 @@ theorem getElem?_swap (a : Array α) (i j : Fin a.size) (k : Nat) : (a.swap i j)
@[simp] theorem swapAt_def (a : Array α) (i : Fin a.size) (v : α) :
    a.swapAt i v = (a[i.1], a.set i v) := rfl

+@[simp] theorem size_swapAt (a : Array α) (i : Fin a.size) (v : α) :
+    (a.swapAt i v).2.size = a.size := by simp [swapAt_def]
+
@[simp]
 theorem swapAt!_def (a : Array α) (i : Nat) (v : α) (h : i < a.size) :
    a.swapAt! i v = (a[i], a.set ⟨i, h⟩ v) := by simp [swapAt!, h]
@@ -560,11 +590,11 @@ theorem eq_push_pop_back_of_size_ne_zero [Inhabited α] {as : Array α} (h : as.
  · simp [Nat.sub_add_cancel (Nat.zero_lt_of_ne_zero h)]
  · intros i h h'
    if hlt : i < as.pop.size then
-      rw [get_push_lt (h:=hlt), getElem_pop]
+      rw [getElem_push_lt (h:=hlt), getElem_pop]
    else
      have heq : i = as.pop.size :=
        Nat.le_antisymm (size_pop .. ▸ Nat.le_pred_of_lt h) (Nat.le_of_not_gt hlt)
-      cases heq; rw [get_push_eq, back, ←size_pop, get!_eq_getD, getD, dif_pos h]; rfl
+      cases heq; rw [getElem_push_eq, back, ←size_pop, get!_eq_getD, getD, dif_pos h]; rfl

 theorem eq_push_of_size_ne_zero {as : Array α} (h : as.size ≠ 0) :
    ∃ (bs : Array α) (c : α), as = bs.push c :=
@@ -773,9 +803,9 @@ theorem map_induction (as : Array α) (f : α → β) (motive : Nat → Prop) (h
    · intro j h
      simp at h ⊢
      by_cases h' : j < size b
-      · rw [get_push]
+      · rw [getElem_push]
        simp_all
-      · rw [get_push, dif_neg h']
+      · rw [getElem_push, dif_neg h']
        simp only [show j = i by omega]
        exact (hs _ m).1

@@ -800,7 +830,7 @@ theorem map_spec (as : Array α) (f : α → β) (p : Fin as.size → β → Pro
    (as.push x).map f = (as.map f).push (f x) := by
  ext
  · simp
-  · simp only [getElem_map, get_push, size_map]
+  · simp only [getElem_map, getElem_push, size_map]
    split <;> rfl

@[simp] theorem map_pop {f : α → β} {as : Array α} :
@@ -822,6 +852,12 @@ theorem getElem_modify {as : Array α} {x i} (h : i < (as.modify x f).size) :
  · simp only [Id.bind_eq, get_set _ _ _ (by simpa using h)]; split <;> simp [*]
  · rw [if_neg (mt (by rintro rfl; exact h) (by simp_all))]

+@[simp] theorem toList_modify (as : Array α) (f : α → α) :
+    (as.modify x f).toList = as.toList.modify f x := by
+  apply List.ext_getElem
+  · simp
+  · simp [getElem_modify, List.getElem_modify]
+
 theorem getElem_modify_self {as : Array α} {i : Nat} (f : α → α) (h : i < (as.modify i f).size) :
    (as.modify i f)[i] = f (as[i]'(by simpa using h)) := by
  simp [getElem_modify h]
@@ -831,6 +867,11 @@ theorem getElem_modify_of_ne {as : Array α} {i : Nat} (h : i ≠ j)
    (as.modify i f)[j] = as[j]'(by simpa using hj) := by
  simp [getElem_modify hj, h]

+theorem getElem?_modify {as : Array α} {i : Nat} {f : α → α} {j : Nat} :
+    (as.modify i f)[j]? = if i = j then as[j]?.map f else as[j]? := by
+  simp only [getElem?_def, size_modify, getElem_modify, Option.map_dif]
+  split <;> split <;> rfl
+
 /-! ### filter -/

@[simp] theorem toList_filter (p : α → Bool) (l : Array α) :
@@ -892,7 +933,7 @@ theorem filterMap_congr {as bs : Array α} (h : as = bs)

 theorem size_empty : (#[] : Array α).size = 0 := rfl

-theorem toList_empty : (#[] : Array α).toList = [] := rfl
+@[simp] theorem toList_empty : (#[] : Array α).toList = [] := rfl

 /-! ### append -/

@@ -1050,7 +1091,7 @@ theorem getElem_extract_loop_ge (as bs : Array α) (size start : Nat) (hge : i
      have h₂ : bs.size < (extract.loop as size (start+1) (bs.push as[start])).size := by
        rw [size_extract_loop]; apply Nat.lt_of_lt_of_le h₁; exact Nat.le_add_right ..
      have h : (extract.loop as size (start + 1) (push bs as[start]))[bs.size] = as[start] := by
-        rw [getElem_extract_loop_lt as (bs.push as[start]) size (start+1) h₁ h₂, get_push_eq]
+        rw [getElem_extract_loop_lt as (bs.push as[start]) size (start+1) h₁ h₂, getElem_push_eq]
      rw [h]; congr; rw [Nat.add_sub_cancel]
    else
      have hge : bs.size + 1 ≤ i := Nat.lt_of_le_of_ne hge hi
@@ -1077,6 +1118,14 @@ theorem getElem?_extract {as : Array α} {start stop : Nat} :
    · omega
  · rfl

+@[simp] theorem toList_extract (as : Array α) (start stop : Nat) :
+    (as.extract start stop).toList = (as.toList.drop start).take (stop - start) := by
+  apply List.ext_getElem
+  · simp only [length_toList, size_extract, List.length_take, List.length_drop]
+    omega
+  · intros n h₁ h₂
+    simp
+
@[simp] theorem extract_all (as : Array α) : as.extract 0 as.size = as := by
  apply ext
  · rw [size_extract, Nat.min_self, Nat.sub_zero]
@@ -1246,7 +1295,7 @@ open Fin
      · assumption

 theorem getElem_swap' (a : Array α) (i j : Fin a.size) (k : Nat) (hk : k < a.size) :
-    (a.swap i j)[k]'(by simp_all) = if k = i then a[j] else if k = j then a[i]  else a[k] := by
+    (a.swap i j)[k]'(by simp_all) = if k = i then a[j] else if k = j then a[i] else a[k] := by
  split
  · simp_all only [getElem_swap_left]
  · split <;> simp_all
@@ -1256,7 +1305,7 @@ theorem getElem_swap (a : Array α) (i j : Fin a.size) (k : Nat) (hk : k < (a.sw
  apply getElem_swap'

@[simp] theorem swap_swap (a : Array α) {i j : Fin a.size} :
-    (a.swap i j).swap ⟨i.1, (a.size_swap ..).symm ▸i.2⟩ ⟨j.1, (a.size_swap ..).symm ▸j.2⟩ = a := by
+    (a.swap i j).swap ⟨i.1, (a.size_swap ..).symm ▸ i.2⟩ ⟨j.1, (a.size_swap ..).symm ▸ j.2⟩ = a := by
  apply ext
  · simp only [size_swap]
  · intros
@@ -1391,6 +1440,11 @@ theorem all_toArray (p : α → Bool) (l : List α) : l.toArray.all p = l.all p
  apply ext'
  simp

+@[simp] theorem modify_toArray (f : α → α) (l : List α) :
+    l.toArray.modify i f = (l.modify f i).toArray := by
+  apply ext'
+  simp
+
@[simp] theorem filter_toArray' (p : α → Bool) (l : List α) (h : stop = l.toArray.size) :
    l.toArray.filter p 0 stop = (l.filter p).toArray := by
  subst h
@@ -1419,6 +1473,11 @@ theorem filterMap_toArray (f : α → Option β) (l : List α) :
  apply ext'
  simp

+@[simp] theorem toArray_extract (l : List α) (start stop : Nat) :
+    l.toArray.extract start stop = ((l.drop start).take (stop - start)).toArray := by
+  apply ext'
+  simp
+
 end List

 /-! ### Deprecations -/
--- a/src/Init/Data/Array/MapIdx.lean
+++ b/src/Init/Data/Array/MapIdx.lean
@@ -9,56 +9,84 @@ import Init.Data.List.MapIdx

 namespace Array

-
-/-! ### mapIdx -/
+/-! ### mapFinIdx -/

 -- This could also be proved from `SatisfiesM_mapIdxM` in Batteries.
-theorem mapIdx_induction (as : Array α) (f : Fin as.size → α → β)
+theorem mapFinIdx_induction (as : Array α) (f : Fin as.size → α → β)
    (motive : Nat → Prop) (h0 : motive 0)
    (p : Fin as.size → β → Prop)
    (hs : ∀ i, motive i.1 → p i (f i as[i]) ∧ motive (i + 1)) :
-    motive as.size ∧ ∃ eq : (Array.mapIdx as f).size = as.size,
-      ∀ i h, p ⟨i, h⟩ ((Array.mapIdx as f)[i]) := by
+    motive as.size ∧ ∃ eq : (Array.mapFinIdx as f).size = as.size,
+      ∀ i h, p ⟨i, h⟩ ((Array.mapFinIdx as f)[i]) := by
  let rec go {bs i j h} (h₁ : j = bs.size) (h₂ : ∀ i h h', p ⟨i, h⟩ bs[i]) (hm : motive j) :
-    let arr : Array β := Array.mapIdxM.map (m := Id) as f i j h bs
+    let arr : Array β := Array.mapFinIdxM.map (m := Id) as f i j h bs
    motive as.size ∧ ∃ eq : arr.size = as.size, ∀ i h, p ⟨i, h⟩ arr[i] := by
-    induction i generalizing j bs with simp [mapIdxM.map]
+    induction i generalizing j bs with simp [mapFinIdxM.map]
    | zero =>
      have := (Nat.zero_add _).symm.trans h
      exact ⟨this ▸ hm, h₁ ▸ this, fun _ _ => h₂ ..⟩
    | succ i ih =>
      apply @ih (bs.push (f ⟨j, by omega⟩ as[j])) (j + 1) (by omega) (by simp; omega)
      · intro i i_lt h'
-        rw [get_push]
+        rw [getElem_push]
        split
        · apply h₂
        · simp only [size_push] at h'
          obtain rfl : i = j := by omega
          apply (hs ⟨i, by omega⟩ hm).1
      · exact (hs ⟨j, by omega⟩ hm).2
-  simp [mapIdx, mapIdxM]; exact go rfl nofun h0
+  simp [mapFinIdx, mapFinIdxM]; exact go rfl nofun h0

-theorem mapIdx_spec (as : Array α) (f : Fin as.size → α → β)
+theorem mapFinIdx_spec (as : Array α) (f : Fin as.size → α → β)
+    (p : Fin as.size → β → Prop) (hs : ∀ i, p i (f i as[i])) :
+    ∃ eq : (Array.mapFinIdx as f).size = as.size,
+      ∀ i h, p ⟨i, h⟩ ((Array.mapFinIdx as f)[i]) :=
+  (mapFinIdx_induction _ _ (fun _ => True) trivial p fun _ _ => ⟨hs .., trivial⟩).2
+
+@[simp] theorem size_mapFinIdx (a : Array α) (f : Fin a.size → α → β) : (a.mapFinIdx f).size = a.size :=
+  (mapFinIdx_spec (p := fun _ _ => True) (hs := fun _ => trivial)).1
+
+@[simp] theorem size_zipWithIndex (as : Array α) : as.zipWithIndex.size = as.size :=
+  Array.size_mapFinIdx _ _
+
+@[simp] theorem getElem_mapFinIdx (a : Array α) (f : Fin a.size → α → β) (i : Nat)
+    (h : i < (mapFinIdx a f).size) :
+    (a.mapFinIdx f)[i] = f ⟨i, by simp_all⟩ (a[i]'(by simp_all)) :=
+  (mapFinIdx_spec _ _ (fun i b => b = f i a[i]) fun _ => rfl).2 i _
+
+@[simp] theorem getElem?_mapFinIdx (a : Array α) (f : Fin a.size → α → β) (i : Nat) :
+    (a.mapFinIdx f)[i]? =
+      a[i]?.pbind fun b h => f ⟨i, (getElem?_eq_some_iff.1 h).1⟩ b := by
+  simp only [getElem?_def, size_mapFinIdx, getElem_mapFinIdx]
+  split <;> simp_all
+
+/-! ### mapIdx -/
+
+theorem mapIdx_induction (as : Array α) (f : Nat → α → β)
+    (motive : Nat → Prop) (h0 : motive 0)
+    (p : Fin as.size → β → Prop)
+    (hs : ∀ i, motive i.1 → p i (f i as[i]) ∧ motive (i + 1)) :
+    motive as.size ∧ ∃ eq : (Array.mapIdx as f).size = as.size,
+      ∀ i h, p ⟨i, h⟩ ((Array.mapIdx as f)[i]) :=
+  mapFinIdx_induction as (fun i a => f i a) motive h0 p hs
+
+theorem mapIdx_spec (as : Array α) (f : Nat → α → β)
    (p : Fin as.size → β → Prop) (hs : ∀ i, p i (f i as[i])) :
    ∃ eq : (Array.mapIdx as f).size = as.size,
      ∀ i h, p ⟨i, h⟩ ((Array.mapIdx as f)[i]) :=
  (mapIdx_induction _ _ (fun _ => True) trivial p fun _ _ => ⟨hs .., trivial⟩).2

-@[simp] theorem size_mapIdx (a : Array α) (f : Fin a.size → α → β) : (a.mapIdx f).size = a.size :=
+@[simp] theorem size_mapIdx (a : Array α) (f : Nat → α → β) : (a.mapIdx f).size = a.size :=
  (mapIdx_spec (p := fun _ _ => True) (hs := fun _ => trivial)).1

-@[simp] theorem size_zipWithIndex (as : Array α) : as.zipWithIndex.size = as.size :=
-  Array.size_mapIdx _ _
-
-@[simp] theorem getElem_mapIdx (a : Array α) (f : Fin a.size → α → β) (i : Nat)
+@[simp] theorem getElem_mapIdx (a : Array α) (f : Nat → α → β) (i : Nat)
    (h : i < (mapIdx a f).size) :
-    (a.mapIdx f)[i] = f ⟨i, by simp_all⟩ (a[i]'(by simp_all)) :=
-  (mapIdx_spec _ _ (fun i b => b = f i a[i]) fun _ => rfl).2 i _
+    (a.mapIdx f)[i] = f i (a[i]'(by simp_all)) :=
+  (mapIdx_spec _ _ (fun i b => b = f i a[i]) fun _ => rfl).2 i (by simp_all)

-@[simp] theorem getElem?_mapIdx (a : Array α) (f : Fin a.size → α → β) (i : Nat) :
+@[simp] theorem getElem?_mapIdx (a : Array α) (f : Nat → α → β) (i : Nat) :
    (a.mapIdx f)[i]? =
-      a[i]?.pbind fun b h => f ⟨i, (getElem?_eq_some_iff.1 h).1⟩ b := by
-  simp only [getElem?_def, size_mapIdx, getElem_mapIdx]
-  split <;> simp_all
+      a[i]?.map (f i) := by
+  simp [getElem?_def, size_mapIdx, getElem_mapIdx]

 end Array
--- a/src/Init/Data/BitVec/Lemmas.lean
+++ b/src/Init/Data/BitVec/Lemmas.lean
@@ -316,6 +316,12 @@ theorem getLsbD_ofNat (n : Nat) (x : Nat) (i : Nat) :
  simp [Nat.sub_sub_eq_min, Nat.min_eq_right]
  omega

+@[simp] theorem sub_add_bmod_cancel {x y : BitVec w} :
+    ((((2 ^ w : Nat) - y.toNat) : Int) + x.toNat).bmod (2 ^ w) =
+      ((x.toNat : Int) - y.toNat).bmod (2 ^ w) := by
+  rw [Int.sub_eq_add_neg, Int.add_assoc, Int.add_comm, Int.bmod_add_cancel, Int.add_comm,
+    Int.sub_eq_add_neg]
+
 private theorem lt_two_pow_of_le {x m n : Nat} (lt : x < 2 ^ m) (le : m ≤ n) : x < 2 ^ n :=
  Nat.lt_of_lt_of_le lt (Nat.pow_le_pow_of_le_right (by trivial : 0 < 2) le)

@@ -1974,6 +1980,10 @@ theorem sub_def {n} (x y : BitVec n) : x - y = .ofNat n ((2^n - y.toNat) + x.toN
@[simp] theorem toNat_sub {n} (x y : BitVec n) :
    (x - y).toNat = (((2^n - y.toNat) + x.toNat) % 2^n) := rfl

+@[simp, bv_toNat] theorem toInt_sub {x y : BitVec w} :
+    (x - y).toInt = (x.toInt - y.toInt).bmod (2 ^ w) := by
+  simp [toInt_eq_toNat_bmod, @Int.ofNat_sub y.toNat (2 ^ w) (by omega)]
+
 -- We prefer this lemma to `toNat_sub` for the `bv_toNat` simp set.
 -- For reasons we don't yet understand, unfolding via `toNat_sub` sometimes
 -- results in `omega` generating proof terms that are very slow in the kernel.
@@ -1996,6 +2006,8 @@ theorem ofNat_sub_ofNat {n} (x y : Nat) : BitVec.ofNat n x - BitVec.ofNat n y =

@[simp] protected theorem sub_zero (x : BitVec n) : x - 0#n = x := by apply eq_of_toNat_eq ; simp

+@[simp] protected theorem zero_sub (x : BitVec n) : 0#n - x = -x := rfl
+
@[simp] protected theorem sub_self (x : BitVec n) : x - x = 0#n := by
  apply eq_of_toNat_eq
  simp only [toNat_sub]
@@ -2008,18 +2020,8 @@ theorem ofNat_sub_ofNat {n} (x y : Nat) : BitVec.ofNat n x - BitVec.ofNat n y =

 theorem toInt_neg {x : BitVec w} :
    (-x).toInt = (-x.toInt).bmod (2 ^ w) := by
-  simp only [toInt_eq_toNat_bmod, toNat_neg, Int.ofNat_emod, Int.emod_bmod_congr]
-  rw [← Int.subNatNat_of_le (by omega), Int.subNatNat_eq_coe, Int.sub_eq_add_neg, Int.add_comm,
-    Int.bmod_add_cancel]
-  by_cases h : x.toNat < ((2 ^ w) + 1) / 2
-  · rw [Int.bmod_pos (x := x.toNat)]
-    all_goals simp only [toNat_mod_cancel']
-    norm_cast
-  · rw [Int.bmod_neg (x := x.toNat)]
-    · simp only [toNat_mod_cancel']
-      rw_mod_cast [Int.neg_sub, Int.sub_eq_add_neg, Int.add_comm, Int.bmod_add_cancel]
-    · norm_cast
-      simp_all
+  rw [← BitVec.zero_sub, toInt_sub]
+  simp [BitVec.toInt_ofNat]

@[simp] theorem toFin_neg (x : BitVec n) :
    (-x).toFin = Fin.ofNat' (2^n) (2^n - x.toNat) :=
--- a/src/Init/Data/Int/DivModLemmas.lean
+++ b/src/Init/Data/Int/DivModLemmas.lean
@@ -1125,6 +1125,17 @@ theorem emod_add_bmod_congr (x : Int) (n : Nat) : Int.bmod (x%n + y) n = Int.bmo
  simp [Int.emod_def, Int.sub_eq_add_neg]
  rw [←Int.mul_neg, Int.add_right_comm,  Int.bmod_add_mul_cancel]

+@[simp]
+theorem emod_sub_bmod_congr (x : Int) (n : Nat) : Int.bmod (x%n - y) n = Int.bmod (x - y) n := by
+  simp only [emod_def, Int.sub_eq_add_neg]
+  rw [←Int.mul_neg, Int.add_right_comm,  Int.bmod_add_mul_cancel]
+
+@[simp]
+theorem sub_emod_bmod_congr (x : Int) (n : Nat) : Int.bmod (x - y%n) n = Int.bmod (x - y) n := by
+  simp only [emod_def]
+  rw [Int.sub_eq_add_neg, Int.neg_sub, Int.sub_eq_add_neg, ← Int.add_assoc, Int.add_right_comm,
+    Int.bmod_add_mul_cancel, Int.sub_eq_add_neg]
+
@[simp]
 theorem emod_mul_bmod_congr (x : Int) (n : Nat) : Int.bmod (x%n * y) n = Int.bmod (x * y) n := by
  simp [Int.emod_def, Int.sub_eq_add_neg]
@@ -1140,9 +1151,28 @@ theorem bmod_add_bmod_congr : Int.bmod (Int.bmod x n + y) n = Int.bmod (x + y) n
    rw [Int.sub_eq_add_neg, Int.add_right_comm, ←Int.sub_eq_add_neg]
    simp

+@[simp]
+theorem bmod_sub_bmod_congr : Int.bmod (Int.bmod x n - y) n = Int.bmod (x - y) n := by
+  rw [Int.bmod_def x n]
+  split
+  next p =>
+    simp only [emod_sub_bmod_congr]
+  next p =>
+    rw [Int.sub_eq_add_neg, Int.sub_eq_add_neg, Int.add_right_comm, ←Int.sub_eq_add_neg, ← Int.sub_eq_add_neg]
+    simp [emod_sub_bmod_congr]
+
@[simp] theorem add_bmod_bmod : Int.bmod (x + Int.bmod y n) n = Int.bmod (x + y) n := by
  rw [Int.add_comm x, Int.bmod_add_bmod_congr, Int.add_comm y]

+@[simp] theorem sub_bmod_bmod : Int.bmod (x - Int.bmod y n) n = Int.bmod (x - y) n := by
+  rw [Int.bmod_def y n]
+  split
+  next p =>
+    simp [sub_emod_bmod_congr]
+  next p =>
+    rw [Int.sub_eq_add_neg, Int.sub_eq_add_neg, Int.neg_add, Int.neg_neg, ← Int.add_assoc, ← Int.sub_eq_add_neg]
+    simp [sub_emod_bmod_congr]
+
@[simp]
 theorem bmod_mul_bmod : Int.bmod (Int.bmod x n * y) n = Int.bmod (x * y) n := by
  rw [bmod_def x n]
--- a/src/Init/Data/List/Basic.lean
+++ b/src/Init/Data/List/Basic.lean
@@ -38,7 +38,7 @@ The operations are organized as follow:
 * Sublists: `take`, `drop`, `takeWhile`, `dropWhile`, `partition`, `dropLast`,
  `isPrefixOf`, `isPrefixOf?`, `isSuffixOf`, `isSuffixOf?`, `Subset`, `Sublist`,
  `rotateLeft` and `rotateRight`.
-* Manipulating elements: `replace`, `insert`, `erase`, `eraseP`, `eraseIdx`.
+* Manipulating elements: `replace`, `insert`, `modify`, `erase`, `eraseP`, `eraseIdx`.
 * Finding elements: `find?`, `findSome?`, `findIdx`, `indexOf`, `findIdx?`, `indexOf?`,
 `countP`, `count`, and `lookup`.
 * Logic: `any`, `all`, `or`, and `and`.
@@ -122,6 +122,11 @@ protected def beq [BEq α] : List α → List α → Bool
  | a::as, b::bs => a == b && List.beq as bs
  | _,     _     => false

+@[simp] theorem beq_nil_nil [BEq α] : List.beq ([] : List α) ([] : List α) = true := rfl
+@[simp] theorem beq_cons_nil [BEq α] (a : α) (as : List α) : List.beq (a::as) [] = false := rfl
+@[simp] theorem beq_nil_cons [BEq α] (a : α) (as : List α) : List.beq [] (a::as) = false := rfl
+theorem beq_cons₂ [BEq α] (a b : α) (as bs : List α) : List.beq (a::as) (b::bs) = (a == b && List.beq as bs) := rfl
+
 instance [BEq α] : BEq (List α) := ⟨List.beq⟩

 instance [BEq α] [LawfulBEq α] : LawfulBEq (List α) where
@@ -1114,6 +1119,35 @@ theorem replace_cons [BEq α] {a : α} :
@[inline] protected def insert [BEq α] (a : α) (l : List α) : List α :=
  if l.elem a then l else a :: l

+/-! ### modify -/
+
+/--
+Apply a function to the nth tail of `l`. Returns the input without
+using `f` if the index is larger than the length of the List.
+```
+modifyTailIdx f 2 [a, b, c] = [a, b] ++ f [c]
+```
+-/
+@[simp] def modifyTailIdx (f : List α → List α) : Nat → List α → List α
+  | 0, l => f l
+  | _+1, [] => []
+  | n+1, a :: l => a :: modifyTailIdx f n l
+
+/-- Apply `f` to the head of the list, if it exists. -/
+@[inline] def modifyHead (f : α → α) : List α → List α
+  | [] => []
+  | a :: l => f a :: l
+
+@[simp] theorem modifyHead_nil (f : α → α) : [].modifyHead f = [] := by rw [modifyHead]
+@[simp] theorem modifyHead_cons (a : α) (l : List α) (f : α → α) :
+    (a :: l).modifyHead f = f a :: l := by rw [modifyHead]
+
+/--
+Apply `f` to the nth element of the list, if it exists, replacing that element with the result.
+-/
+def modify (f : α → α) : Nat → List α → List α :=
+  modifyTailIdx (modifyHead f)
+
 /-! ### erase -/

 /--
--- a/src/Init/Data/List/Impl.lean
+++ b/src/Init/Data/List/Impl.lean
@@ -38,7 +38,7 @@ The following operations were already given `@[csimp]` replacements in `Init/Dat

 The following operations are given `@[csimp]` replacements below:
 `set`, `filterMap`, `foldr`, `append`, `bind`, `join`,
-`take`, `takeWhile`, `dropLast`, `replace`, `erase`, `eraseIdx`, `zipWith`,
+`take`, `takeWhile`, `dropLast`, `replace`, `modify`, `erase`, `eraseIdx`, `zipWith`,
 `enumFrom`, and `intercalate`.

 -/
@@ -197,6 +197,24 @@ The following operations are given `@[csimp]` replacements below:
    · simp [*]
    · intro h; rw [IH] <;> simp_all

+/-! ### modify -/
+
+/-- Tail-recursive version of `modify`. -/
+def modifyTR (f : α → α) (n : Nat) (l : List α) : List α := go l n #[] where
+  /-- Auxiliary for `modifyTR`: `modifyTR.go f l n acc = acc.toList ++ modify f n l`. -/
+  go : List α → Nat → Array α → List α
+  | [], _, acc => acc.toList
+  | a :: l, 0, acc => acc.toListAppend (f a :: l)
+  | a :: l, n+1, acc => go l n (acc.push a)
+
+theorem modifyTR_go_eq : ∀ l n, modifyTR.go f l n acc = acc.toList ++ modify f n l
+  | [], n => by cases n <;> simp [modifyTR.go, modify]
+  | a :: l, 0 => by simp [modifyTR.go, modify]
+  | a :: l, n+1 => by simp [modifyTR.go, modify, modifyTR_go_eq l]
+
+@[csimp] theorem modify_eq_modifyTR : @modify = @modifyTR := by
+  funext α f n l; simp [modifyTR, modifyTR_go_eq]
+
 /-! ### erase -/

 /-- Tail recursive version of `List.erase`. -/
--- a/src/Init/Data/List/Lemmas.lean
+++ b/src/Init/Data/List/Lemmas.lean
@@ -1047,9 +1047,6 @@ theorem get_cons_length (x : α) (xs : List α) (n : Nat) (h : n = xs.length) :

@[simp] theorem getLast?_singleton (a : α) : getLast? [a] = a := rfl

-theorem getLast!_of_getLast? [Inhabited α] : ∀ {l : List α}, getLast? l = some a → getLast! l = a
-  | _ :: _, rfl => rfl
-
 theorem getLast?_eq_getLast : ∀ l h, @getLast? α l = some (getLast l h)
  | [], h => nomatch h rfl
  | _ :: _, _ => rfl
@@ -1083,6 +1080,21 @@ theorem getLast?_concat (l : List α) : getLast? (l ++ [a]) = some a := by
 theorem getLastD_concat (a b l) : @getLastD α (l ++ [b]) a = b := by
  rw [getLastD_eq_getLast?, getLast?_concat]; rfl

+/-! ### getLast! -/
+
+@[simp] theorem getLast!_nil [Inhabited α] : ([] : List α).getLast! = default := rfl
+
+theorem getLast!_of_getLast? [Inhabited α] : ∀ {l : List α}, getLast? l = some a → getLast! l = a
+  | _ :: _, rfl => rfl
+
+theorem getLast!_eq_getElem! [Inhabited α] {l : List α} : l.getLast! = l[l.length - 1]! := by
+  cases l with
+  | nil => simp
+  | cons _ _ =>
+    apply getLast!_of_getLast?
+    rw [getElem!_pos, getElem_cons_length (h := by simp)]
+    rfl
+
 /-! ## Head and tail -/

 /-! ### head -/
--- a/src/Init/Data/List/Nat.lean
+++ b/src/Init/Data/List/Nat.lean
@@ -12,3 +12,5 @@ import Init.Data.List.Nat.TakeDrop
 import Init.Data.List.Nat.Count
 import Init.Data.List.Nat.Erase
 import Init.Data.List.Nat.Find
+import Init.Data.List.Nat.BEq
+import Init.Data.List.Nat.Modify
--- a/src/Init/Data/List/Nat/BEq.lean
+++ b/src/Init/Data/List/Nat/BEq.lean
@@ -0,0 +1,47 @@
+/-
+Copyright (c) 2024 Lean FRO All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kim Morrison
+-/
+prelude
+import Init.Data.Nat.Lemmas
+import Init.Data.List.Basic
+
+namespace List
+
+/-! ### isEqv-/
+
+theorem isEqv_eq_decide (a b : List α) (r) :
+    isEqv a b r = if h : a.length = b.length then
+      decide (∀ (i : Nat) (h' : i < a.length), r (a[i]'(h ▸ h')) (b[i]'(h ▸ h'))) else false := by
+  induction a generalizing b with
+  | nil =>
+    cases b <;> simp
+  | cons a as ih =>
+    cases b with
+    | nil => simp
+    | cons b bs =>
+      simp only [isEqv, ih, length_cons, Nat.add_right_cancel_iff]
+      split <;> simp [Nat.forall_lt_succ_left']
+
+/-! ### beq -/
+
+theorem beq_eq_isEqv [BEq α] (a b : List α) : a.beq b = isEqv a b (· == ·) := by
+  induction a generalizing b with
+  | nil =>
+    cases b <;> simp
+  | cons a as ih =>
+    cases b with
+    | nil => simp
+    | cons b bs =>
+      simp only [beq_cons₂, ih, isEqv_eq_decide, length_cons, Nat.add_right_cancel_iff,
+        Nat.forall_lt_succ_left', getElem_cons_zero, getElem_cons_succ, Bool.decide_and,
+        Bool.decide_eq_true]
+      split <;> simp
+
+theorem beq_eq_decide [BEq α] (a b : List α) :
+    (a == b) = if h : a.length = b.length then
+      decide (∀ (i : Nat) (h' : i < a.length), a[i] == b[i]'(h ▸ h')) else false := by
+  simp [BEq.beq, beq_eq_isEqv, isEqv_eq_decide]
+
+end List
--- a/src/Init/Data/List/Nat/Modify.lean
+++ b/src/Init/Data/List/Nat/Modify.lean
@@ -0,0 +1,102 @@
+/-
+Copyright (c) 2014 Parikshit Khanna. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn, Mario Carneiro
+-/
+
+prelude
+import Init.Data.List.Nat.TakeDrop
+
+namespace List
+
+/-! ### modifyHead -/
+
+@[simp] theorem modifyHead_modifyHead (l : List α) (f g : α → α) :
+    (l.modifyHead f).modifyHead g = l.modifyHead (g ∘ f) := by cases l <;> simp [modifyHead]
+
+/-! ### modify -/
+
+@[simp] theorem modify_nil (f : α → α) (n) : [].modify f n = [] := by cases n <;> rfl
+
+@[simp] theorem modify_zero_cons (f : α → α) (a : α) (l : List α) :
+    (a :: l).modify f 0 = f a :: l := rfl
+
+@[simp] theorem modify_succ_cons (f : α → α) (a : α) (l : List α) (n) :
+    (a :: l).modify f (n + 1) = a :: l.modify f n := by rfl
+
+theorem modifyTailIdx_id : ∀ n (l : List α), l.modifyTailIdx id n = l
+  | 0, _ => rfl
+  | _+1, [] => rfl
+  | n+1, a :: l => congrArg (cons a) (modifyTailIdx_id n l)
+
+theorem eraseIdx_eq_modifyTailIdx : ∀ n (l : List α), eraseIdx l n = modifyTailIdx tail n l
+  | 0, l => by cases l <;> rfl
+  | _+1, [] => rfl
+  | _+1, _ :: _ => congrArg (cons _) (eraseIdx_eq_modifyTailIdx _ _)
+
+theorem getElem?_modify (f : α → α) :
+    ∀ n (l : List α) m, (modify f n l)[m]? = (fun a => if n = m then f a else a) <$> l[m]?
+  | n, l, 0 => by cases l <;> cases n <;> simp
+  | n, [], _+1 => by cases n <;> rfl
+  | 0, _ :: l, m+1 => by cases h : l[m]? <;> simp [h, modify, m.succ_ne_zero.symm]
+  | n+1, a :: l, m+1 => by
+    simp only [modify_succ_cons, getElem?_cons_succ, Nat.reduceEqDiff, Option.map_eq_map]
+    refine (getElem?_modify f n l m).trans ?_
+    cases h' : l[m]? <;> by_cases h : n = m <;>
+      simp [h, if_pos, if_neg, Option.map, mt Nat.succ.inj, not_false_iff, h']
+
+@[simp] theorem length_modifyTailIdx (f : List α → List α) (H : ∀ l, length (f l) = length l) :
+    ∀ n l, length (modifyTailIdx f n l) = length l
+  | 0, _ => H _
+  | _+1, [] => rfl
+  | _+1, _ :: _ => congrArg (·+1) (length_modifyTailIdx _ H _ _)
+
+theorem modifyTailIdx_add (f : List α → List α) (n) (l₁ l₂ : List α) :
+    modifyTailIdx f (l₁.length + n) (l₁ ++ l₂) = l₁ ++ modifyTailIdx f n l₂ := by
+  induction l₁ <;> simp [*, Nat.succ_add]
+
+@[simp] theorem length_modify (f : α → α) : ∀ n l, length (modify f n l) = length l :=
+  length_modifyTailIdx _ fun l => by cases l <;> rfl
+
+@[simp] theorem getElem?_modify_eq (f : α → α) (n) (l : List α) :
+    (modify f n l)[n]? = f <$> l[n]? := by
+  simp only [getElem?_modify, if_pos]
+
+@[simp] theorem getElem?_modify_ne (f : α → α) {m n} (l : List α) (h : m ≠ n) :
+    (modify f m l)[n]? = l[n]? := by
+  simp only [getElem?_modify, if_neg h, id_map']
+
+theorem getElem_modify (f : α → α) (n) (l : List α) (m) (h : m < (modify f n l).length) :
+    (modify f n l)[m] =
+      if n = m then f (l[m]'(by simp at h; omega)) else l[m]'(by simp at h; omega) := by
+  rw [getElem_eq_iff, getElem?_modify]
+  simp at h
+  simp [h]
+
+theorem modifyTailIdx_eq_take_drop (f : List α → List α) (H : f [] = []) :
+    ∀ n l, modifyTailIdx f n l = take n l ++ f (drop n l)
+  | 0, _ => rfl
+  | _ + 1, [] => H.symm
+  | n + 1, b :: l => congrArg (cons b) (modifyTailIdx_eq_take_drop f H n l)
+
+theorem modify_eq_take_drop (f : α → α) :
+    ∀ n l, modify f n l = take n l ++ modifyHead f (drop n l) :=
+  modifyTailIdx_eq_take_drop _ rfl
+
+theorem modify_eq_take_cons_drop (f : α → α) {n l} (h : n < length l) :
+    modify f n l = take n l ++ f l[n] :: drop (n + 1) l := by
+  rw [modify_eq_take_drop, drop_eq_getElem_cons h]; rfl
+
+theorem exists_of_modifyTailIdx (f : List α → List α) {n} {l : List α} (h : n ≤ l.length) :
+    ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁.length = n ∧ modifyTailIdx f n l = l₁ ++ f l₂ :=
+  have ⟨_, _, eq, hl⟩ : ∃ l₁ l₂, l = l₁ ++ l₂ ∧ l₁.length = n :=
+    ⟨_, _, (take_append_drop n l).symm, length_take_of_le h⟩
+  ⟨_, _, eq, hl, hl ▸ eq ▸ modifyTailIdx_add (n := 0) ..⟩
+
+theorem exists_of_modify (f : α → α) {n} {l : List α} (h : n < l.length) :
+    ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ l₁.length = n ∧ modify f n l = l₁ ++ f a :: l₂ :=
+  match exists_of_modifyTailIdx _ (Nat.le_of_lt h) with
+  | ⟨_, _::_, eq, hl, H⟩ => ⟨_, _, _, eq, hl, H⟩
+  | ⟨_, [], eq, hl, _⟩ => nomatch Nat.ne_of_gt h (eq ▸ append_nil _ ▸ hl)
+
+end List
--- a/src/Init/Data/Nat/Lemmas.lean
+++ b/src/Init/Data/Nat/Lemmas.lean
@@ -32,6 +32,77 @@ namespace Nat
@[simp] theorem exists_add_one_eq : (∃ n, n + 1 = a) ↔ 0 < a :=
  ⟨fun ⟨n, h⟩ => by omega, fun h => ⟨a - 1, by omega⟩⟩

+/-- Dependent variant of `forall_lt_succ_right`. -/
+theorem forall_lt_succ_right' {p : (m : Nat) → (m < n + 1) → Prop} :
+    (∀ m (h : m < n + 1), p m h) ↔ (∀ m (h : m < n), p m (by omega)) ∧ p n (by omega) := by
+  simp only [Nat.lt_succ_iff, Nat.le_iff_lt_or_eq]
+  constructor
+  · intro w
+    constructor
+    · intro m h
+      exact w _ (.inl h)
+    · exact w _ (.inr rfl)
+  · rintro w m (h|rfl)
+    · exact w.1 _ h
+    · exact w.2
+
+/-- See `forall_lt_succ_right'` for a variant where `p` takes the bound as an argument. -/
+theorem forall_lt_succ_right {p : Nat → Prop} :
+    (∀ m, m < n + 1 → p m) ↔ (∀ m, m < n → p m) ∧ p n := by
+  simpa using forall_lt_succ_right' (p := fun m _ => p m)
+
+/-- Dependent variant of `forall_lt_succ_left`. -/
+theorem forall_lt_succ_left' {p : (m : Nat) → (m < n + 1) → Prop} :
+    (∀ m (h : m < n + 1), p m h) ↔ p 0 (by omega) ∧ (∀ m (h : m < n), p (m + 1) (by omega)) := by
+  constructor
+  · intro w
+    constructor
+    · exact w 0 (by omega)
+    · intro m h
+      exact w (m + 1) (by omega)
+  · rintro ⟨h₀, h₁⟩ m h
+    cases m with
+    | zero => exact h₀
+    | succ m => exact h₁ m (by omega)
+
+/-- See `forall_lt_succ_left'` for a variant where `p` takes the bound as an argument. -/
+theorem forall_lt_succ_left {p : Nat → Prop} :
+    (∀ m, m < n + 1 → p m) ↔ p 0 ∧ (∀ m, m < n → p (m + 1)) := by
+  simpa using forall_lt_succ_left' (p := fun m _ => p m)
+
+/-- Dependent variant of `exists_lt_succ_right`. -/
+theorem exists_lt_succ_right' {p : (m : Nat) → (m < n + 1) → Prop} :
+    (∃ m, ∃ (h : m < n + 1), p m h) ↔ (∃ m, ∃ (h : m < n), p m (by omega)) ∨ p n (by omega) := by
+  simp only [Nat.lt_succ_iff, Nat.le_iff_lt_or_eq]
+  constructor
+  · rintro ⟨m, (h|rfl), w⟩
+    · exact .inl ⟨m, h, w⟩
+    · exact .inr w
+  · rintro (⟨m, h, w⟩ | w)
+    · exact ⟨m, by omega, w⟩
+    · exact ⟨n, by omega, w⟩
+
+/-- See `exists_lt_succ_right'` for a variant where `p` takes the bound as an argument. -/
+theorem exists_lt_succ_right {p : Nat → Prop} :
+    (∃ m, m < n + 1 ∧ p m) ↔ (∃ m, m < n ∧ p m) ∨ p n := by
+  simpa using exists_lt_succ_right' (p := fun m _ => p m)
+
+/-- Dependent variant of `exists_lt_succ_left`. -/
+theorem exists_lt_succ_left' {p : (m : Nat) → (m < n + 1) → Prop} :
+    (∃ m, ∃ (h : m < n + 1), p m h) ↔ p 0 (by omega) ∨ (∃ m, ∃ (h : m < n), p (m + 1) (by omega)) := by
+  constructor
+  · rintro ⟨_|m, h, w⟩
+    · exact .inl w
+    · exact .inr ⟨m, by omega, w⟩
+  · rintro (w|⟨m, h, w⟩)
+    · exact ⟨0, by omega, w⟩
+    · exact ⟨m + 1, by omega, w⟩
+
+/-- See `exists_lt_succ_left'` for a variant where `p` takes the bound as an argument. -/
+theorem exists_lt_succ_left {p : Nat → Prop} :
+    (∃ m, m < n + 1 ∧ p m) ↔ p 0 ∨ (∃ m, m < n ∧ p (m + 1)) := by
+  simpa using exists_lt_succ_left' (p := fun m _ => p m)
+
 /-! ## add -/

 protected theorem add_add_add_comm (a b c d : Nat) : (a + b) + (c + d) = (a + c) + (b + d) := by
--- a/src/Init/NotationExtra.lean
+++ b/src/Init/NotationExtra.lean
@@ -10,6 +10,7 @@ import Init.Data.ToString.Basic
 import Init.Data.Array.Subarray
 import Init.Conv
 import Init.Meta
+import Init.While

 namespace Lean

@@ -344,42 +345,6 @@ syntax (name := solveTactic) "solve" withPosition((ppDedent(ppLine) colGe "| " t
 macro_rules
  | `(tactic| solve $[| $ts]* ) => `(tactic| focus first $[| ($ts); done]*)

-/-! # `repeat` and `while` notation -/
-
-inductive Loop where
-  | mk
-
-@[inline]
-partial def Loop.forIn {β : Type u} {m : Type u → Type v} [Monad m] (_ : Loop) (init : β) (f : Unit → β → m (ForInStep β)) : m β :=
-  let rec @[specialize] loop (b : β) : m β := do
-    match ← f () b with
-      | ForInStep.done b  => pure b
-      | ForInStep.yield b => loop b
-  loop init
-
-instance : ForIn m Loop Unit where
-  forIn := Loop.forIn
-
-syntax "repeat " doSeq : doElem
-
-macro_rules
-  | `(doElem| repeat $seq) => `(doElem| for _ in Loop.mk do $seq)
-
-syntax "while " ident " : " termBeforeDo " do " doSeq : doElem
-
-macro_rules
-  | `(doElem| while $h : $cond do $seq) => `(doElem| repeat if $h : $cond then $seq else break)
-
-syntax "while " termBeforeDo " do " doSeq : doElem
-
-macro_rules
-  | `(doElem| while $cond do $seq) => `(doElem| repeat if $cond then $seq else break)
-
-syntax "repeat " doSeq ppDedent(ppLine) "until " term : doElem
-
-macro_rules
-  | `(doElem| repeat $seq until $cond) => `(doElem| repeat do $seq:doSeq; if $cond then break)
-
 macro:50 e:term:51 " matches " p:sepBy1(term:51, " | ") : term =>
  `(((match $e:term with | $[$p:term]|* => true | _ => false) : Bool))

--- a/src/Init/While.lean
+++ b/src/Init/While.lean
@@ -0,0 +1,51 @@
+/-
+Copyright (c) 2020 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Init.Core
+
+/-!
+# Notation for `while` and `repeat` loops.
+-/
+
+namespace Lean
+
+/-! # `repeat` and `while` notation -/
+
+inductive Loop where
+  | mk
+
+@[inline]
+partial def Loop.forIn {β : Type u} {m : Type u → Type v} [Monad m] (_ : Loop) (init : β) (f : Unit → β → m (ForInStep β)) : m β :=
+  let rec @[specialize] loop (b : β) : m β := do
+    match ← f () b with
+      | ForInStep.done b  => pure b
+      | ForInStep.yield b => loop b
+  loop init
+
+instance : ForIn m Loop Unit where
+  forIn := Loop.forIn
+
+syntax "repeat " doSeq : doElem
+
+macro_rules
+  | `(doElem| repeat $seq) => `(doElem| for _ in Loop.mk do $seq)
+
+syntax "while " ident " : " termBeforeDo " do " doSeq : doElem
+
+macro_rules
+  | `(doElem| while $h : $cond do $seq) => `(doElem| repeat if $h : $cond then $seq else break)
+
+syntax "while " termBeforeDo " do " doSeq : doElem
+
+macro_rules
+  | `(doElem| while $cond do $seq) => `(doElem| repeat if $cond then $seq else break)
+
+syntax "repeat " doSeq ppDedent(ppLine) "until " term : doElem
+
+macro_rules
+  | `(doElem| repeat $seq until $cond) => `(doElem| repeat do $seq:doSeq; if $cond then break)
+
+end Lean
--- a/src/Lean/Declaration.lean
+++ b/src/Lean/Declaration.lean
@@ -369,8 +369,13 @@ def RecursorVal.getFirstIndexIdx (v : RecursorVal) : Nat :=
 def RecursorVal.getFirstMinorIdx (v : RecursorVal) : Nat :=
  v.numParams + v.numMotives

-def RecursorVal.getInduct (v : RecursorVal) : Name :=
-  v.name.getPrefix
+/-- The inductive type of the major argument of the recursor. -/
+def RecursorVal.getMajorInduct (v : RecursorVal) : Name :=
+  go v.getMajorIdx v.type
+where
+  go
+  | 0, e => e.bindingDomain!.getAppFn.constName!
+  | n+1, e => go n e.bindingBody!

 inductive QuotKind where
  | type  -- `Quot`
--- a/src/Lean/Elab/Syntax.lean
+++ b/src/Lean/Elab/Syntax.lean
@@ -146,7 +146,7 @@ where
      let args ← args.mapM fun arg => withNestedParser do process arg
      mkParserSeq args
    else
-      let args ← args.mapIdxM fun i arg => withReader (fun ctx => { ctx with first := ctx.first && i.val == 0 }) do process arg
+      let args ← args.mapIdxM fun i arg => withReader (fun ctx => { ctx with first := ctx.first && i == 0 }) do process arg
      mkParserSeq args

  ensureNoPrec (stx : Syntax) :=
--- a/src/Lean/Elab/Tactic/Conv/Pattern.lean
+++ b/src/Lean/Elab/Tactic/Conv/Pattern.lean
@@ -119,7 +119,7 @@ private def pre (pattern : AbstractMVarsResult) (state : IO.Ref PatternMatchStat
        let ids ← ids.mapIdxM fun i id =>
          match id.getNat with
          | 0 => throwErrorAt id "positive integer expected"
-          | n+1 => pure (n, i.1)
+          | n+1 => pure (n, i)
        let ids := ids.qsort (·.1 < ·.1)
        unless @Array.allDiff _ ⟨(·.1 == ·.1)⟩ ids do
          throwError "occurrence list is not distinct"
--- a/src/Lean/Meta/IndPredBelow.lean
+++ b/src/Lean/Meta/IndPredBelow.lean
@@ -54,7 +54,7 @@ def mkContext (declName : Name) : MetaM Context := do
  let typeInfos ← indVal.all.toArray.mapM getConstInfoInduct
  let motiveTypes ← typeInfos.mapM motiveType
  let motives ← motiveTypes.mapIdxM fun j motive =>
-    return (← motiveName motiveTypes j.val, motive)
+    return (← motiveName motiveTypes j, motive)
  let headers ← typeInfos.mapM $ mkHeader motives indVal.numParams
  return {
    motives := motives
@@ -214,7 +214,7 @@ def mkConstructor (ctx : Context) (i : Nat) (ctor : Name) : MetaM Constructor :=

 def mkInductiveType
    (ctx : Context)
-    (i : Fin ctx.typeInfos.size)
+    (i : Nat)
    (indVal : InductiveVal) : MetaM InductiveType := do
  return {
    name := ctx.belowNames[i]!
@@ -340,11 +340,11 @@ where
  mkIH
      (params : Array Expr)
      (motives : Array Expr)
-      (idx : Fin ctx.motives.size)
+      (idx : Nat)
      (motive : Name × Expr) : MetaM $ Name × (Array Expr → MetaM Expr) := do
    let name :=
      if ctx.motives.size > 1
-      then mkFreshUserName <| .mkSimple s!"ih_{idx.val.succ}"
+      then mkFreshUserName <| .mkSimple s!"ih_{idx + 1}"
      else mkFreshUserName <| .mkSimple "ih"
    let ih ← instantiateForall motive.2 params
    let mkDomain (_ : Array Expr) : MetaM Expr :=
@@ -353,7 +353,7 @@ where
        let args := params ++ motives ++ ys
        let premise :=
          mkAppN
-            (mkConst ctx.belowNames[idx.val]! levels) args
+            (mkConst ctx.belowNames[idx]! levels) args
        let conclusion :=
          mkAppN motives[idx]! ys
        mkForallFVars ys (←mkArrow premise conclusion)
--- a/src/Lean/Meta/Match/CaseArraySizes.lean
+++ b/src/Lean/Meta/Match/CaseArraySizes.lean
@@ -70,7 +70,7 @@ def caseArraySizes (mvarId : MVarId) (fvarId : FVarId) (sizes : Array Nat) (xNam
      let subst  := subgoal.subst
      let mvarId := subgoal.mvarId
      let hEqSz  := (subst.get hEq).fvarId!
-      if h : i.val < sizes.size then
+      if h : i < sizes.size then
         let n := sizes.get ⟨i, h⟩
         let mvarId ← mvarId.clear subgoal.newHs[0]!
         let mvarId ← mvarId.clear (subst.get aSizeFVarId).fvarId!
--- a/src/Lean/Meta/Match/Match.lean
+++ b/src/Lean/Meta/Match/Match.lean
@@ -545,7 +545,7 @@ private def processValue (p : Problem) : MetaM (Array Problem) := do
  let subgoals ← caseValues p.mvarId x.fvarId! values (substNewEqs := true)
  subgoals.mapIdxM fun i subgoal => do
    trace[Meta.Match.match] "processValue subgoal\n{MessageData.ofGoal subgoal.mvarId}"
-    if h : i.val < values.size then
+    if h : i < values.size then
      let value := values.get ⟨i, h⟩
      -- (x = value) branch
      let subst := subgoal.subst
@@ -599,7 +599,7 @@ private def processArrayLit (p : Problem) : MetaM (Array Problem) := do
  let sizes := collectArraySizes p
  let subgoals ← caseArraySizes p.mvarId x.fvarId! sizes
  subgoals.mapIdxM fun i subgoal => do
-    if i.val < sizes.size then
+    if i < sizes.size then
      let size     := sizes.get! i
      let subst    := subgoal.subst
      let elems    := subgoal.elems.toList
--- a/src/Lean/Meta/Tactic/FunInd.lean
+++ b/src/Lean/Meta/Tactic/FunInd.lean
@@ -643,7 +643,7 @@ def abstractIndependentMVars (mvars : Array MVarId) (index : Nat) (e : Expr) : M
      pure mvar
  trace[Meta.FunInd] "abstractIndependentMVars, reverted mvars: {mvars}"
  let decls := mvars.mapIdx fun i mvar =>
-    (.mkSimple s!"case{i.val+1}", (fun _ => mvar.getType))
+    (.mkSimple s!"case{i+1}", (fun _ => mvar.getType))
  Meta.withLocalDeclsD decls fun xs => do
      for mvar in mvars, x in xs do
        mvar.assign x
@@ -971,7 +971,7 @@ def deriveInductionStructural (names : Array Name) (numFixed : Nat) : MetaM Unit
            mkForallFVars ys (.sort levelZero)
        let motiveArities ← infos.mapM fun info => do
          lambdaTelescope (← instantiateLambda info.value xs) fun ys _ => pure ys.size
-        let motiveDecls ← motiveTypes.mapIdxM fun ⟨i,_⟩ motiveType => do
+        let motiveDecls ← motiveTypes.mapIdxM fun i motiveType => do
          let n := if infos.size = 1 then .mkSimple "motive"
                                     else .mkSimple s!"motive_{i+1}"
          pure (n, fun _ => pure motiveType)
--- a/src/Lean/Meta/WHNF.lean
+++ b/src/Lean/Meta/WHNF.lean
@@ -95,7 +95,7 @@ private def toCtorWhenK (recVal : RecursorVal) (major : Expr) : MetaM Expr := do
  let majorType ← inferType major
  let majorType ← instantiateMVars (← whnf majorType)
  let majorTypeI := majorType.getAppFn
-  if !majorTypeI.isConstOf recVal.getInduct then
+  if !majorTypeI.isConstOf recVal.getMajorInduct then
    return major
  else if majorType.hasExprMVar && majorType.getAppArgs[recVal.numParams:].any Expr.hasExprMVar then
    return major
@@ -197,7 +197,7 @@ private def reduceRec (recVal : RecursorVal) (recLvls : List Level) (recArgs : A
      major ← toCtorWhenK recVal major
    major := major.toCtorIfLit
    major ← cleanupNatOffsetMajor major
-    major ← toCtorWhenStructure recVal.getInduct major
+    major ← toCtorWhenStructure recVal.getMajorInduct major
    match getRecRuleFor recVal major with
    | some rule =>
      let majorArgs := major.getAppArgs
--- a/src/Lean/Parser/Extra.lean
+++ b/src/Lean/Parser/Extra.lean
@@ -189,7 +189,7 @@ open PrettyPrinter Syntax.MonadTraverser Formatter in
@[combinator_formatter sepByIndent]
 def sepByIndent.formatter (p : Formatter) (_sep : String) (pSep : Formatter) : Formatter := do
  let stx ← getCur
-  let hasNewlineSep := stx.getArgs.mapIdx (fun ⟨i, _⟩ n =>
+  let hasNewlineSep := stx.getArgs.mapIdx (fun i n =>
    i % 2 == 1 && n.matchesNull 0 && i != stx.getArgs.size - 1) |>.any id
  visitArgs do
    for i in (List.range stx.getArgs.size).reverse do
--- a/src/Lean/Server/Completion.lean
+++ b/src/Lean/Server/Completion.lean
@@ -1004,7 +1004,7 @@ private def assignSortTexts (completions : CompletionList) : CompletionList := I
  if completions.items.isEmpty then
    return completions
  let items := completions.items.mapIdx fun i item =>
-    { item with sortText? := toString i.val }
+    { item with sortText? := toString i }
  let maxDigits := items[items.size - 1]!.sortText?.get!.length
  let items := items.map fun item =>
    let sortText := item.sortText?.get!
--- a/src/Std/Sat/AIG/Basic.lean
+++ b/src/Std/Sat/AIG/Basic.lean
@@ -128,7 +128,7 @@ theorem Cache.get?_property {decls : Array (Decl α)} {idx : Nat} (c : Cache α
  induction hcache generalizing decl with
  | empty => simp at hfound
  | push_id wf ih =>
-    rw [Array.get_push]
+    rw [Array.getElem_push]
    split
    · apply ih
      simp [hfound]
@@ -140,7 +140,7 @@ theorem Cache.get?_property {decls : Array (Decl α)} {idx : Nat} (c : Cache α
      assumption
  | push_cache wf ih =>
    rename_i decl'
-    rw [Array.get_push]
+    rw [Array.getElem_push]
    split
    · simp only [HashMap.getElem?_insert] at hfound
      match heq : decl == decl' with
@@ -464,7 +464,7 @@ def mkGate (aig : AIG α) (input : GateInput aig) : Entrypoint α :=
  let cache := aig.cache.noUpdate
  have invariant := by
    intro i lhs' rhs' linv' rinv' h1 h2
-    simp only [Array.get_push] at h2
+    simp only [Array.getElem_push] at h2
    split at h2
    · apply aig.invariant <;> assumption
    · injections
@@ -483,7 +483,7 @@ def mkAtom (aig : AIG α) (n : α) : Entrypoint α :=
  let cache := aig.cache.noUpdate
  have invariant := by
    intro i lhs rhs linv rinv h1 h2
-    simp only [Array.get_push] at h2
+    simp only [Array.getElem_push] at h2
    split at h2
    · apply aig.invariant <;> assumption
    · contradiction
@@ -499,7 +499,7 @@ def mkConst (aig : AIG α) (val : Bool) : Entrypoint α :=
  let cache := aig.cache.noUpdate
  have invariant := by
    intro i lhs rhs linv rinv h1 h2
-    simp only [Array.get_push] at h2
+    simp only [Array.getElem_push] at h2
    split at h2
    · apply aig.invariant <;> assumption
    · contradiction
--- a/src/Std/Sat/AIG/Cached.lean
+++ b/src/Std/Sat/AIG/Cached.lean
@@ -36,7 +36,7 @@ def mkAtomCached (aig : AIG α) (n : α) : Entrypoint α :=
    let decls := decls.push decl
    have inv := by
      intro i lhs rhs linv rinv h1 h2
-      simp only [Array.get_push] at h2
+      simp only [Array.getElem_push] at h2
      split at h2
      · apply inv <;> assumption
      · contradiction
@@ -58,7 +58,7 @@ def mkConstCached (aig : AIG α) (val : Bool) : Entrypoint α :=
    let decls := decls.push decl
    have inv := by
      intro i lhs rhs linv rinv h1 h2
-      simp only [Array.get_push] at h2
+      simp only [Array.getElem_push] at h2
      split at h2
      · apply inv <;> assumption
      · contradiction
@@ -121,7 +121,7 @@ where
          have inv := by
            intro i lhs rhs linv rinv h1 h2
            simp only [decls] at *
-            simp only [Array.get_push] at h2
+            simp only [Array.getElem_push] at h2
            split at h2
            · apply inv <;> assumption
            · injections; omega
--- a/src/Std/Sat/AIG/CachedLemmas.lean
+++ b/src/Std/Sat/AIG/CachedLemmas.lean
@@ -60,7 +60,7 @@ theorem mkAtomCached_decl_eq (aig : AIG α) (var : α) (idx : Nat) {h : idx < ai
    simp [this]
  | none =>
    have := mkAtomCached_miss_aig aig hcache
-    simp only [this, Array.get_push]
+    simp only [this, Array.getElem_push]
    split
    · rfl
    · contradiction
@@ -134,7 +134,7 @@ theorem mkConstCached_decl_eq (aig : AIG α) (val : Bool) (idx : Nat) {h : idx <
    simp [this]
  | none =>
    have := mkConstCached_miss_aig aig hcache
-    simp only [this, Array.get_push]
+    simp only [this, Array.getElem_push]
    split
    · rfl
    · contradiction
@@ -257,7 +257,7 @@ theorem mkGateCached.go_decl_eq (aig : AIG α) (input : GateInput aig) :
          · rw [← hres]
            dsimp only
            intro idx h1 h2
-            rw [Array.get_push]
+            rw [Array.getElem_push]
            simp [h2]

 /--
--- a/src/Std/Sat/AIG/Lemmas.lean
+++ b/src/Std/Sat/AIG/Lemmas.lean
@@ -78,7 +78,7 @@ The AIG produced by `AIG.mkGate` agrees with the input AIG on all indices that a
 theorem mkGate_decl_eq idx (aig : AIG α) (input : GateInput aig) {h : idx < aig.decls.size} :
    have := mkGate_le_size aig input
    (aig.mkGate input).aig.decls[idx]'(by omega) = aig.decls[idx] := by
-  simp only [mkGate, Array.get_push]
+  simp only [mkGate, Array.getElem_push]
  split
  · rfl
  · contradiction
@@ -99,13 +99,13 @@ theorem denote_mkGate {aig : AIG α} {input : GateInput aig} :
    unfold denote denote.go
  split
  · next heq =>
-    rw [mkGate, Array.get_push_eq] at heq
+    rw [mkGate, Array.getElem_push_eq] at heq
    contradiction
  · next heq =>
-    rw [mkGate, Array.get_push_eq] at heq
+    rw [mkGate, Array.getElem_push_eq] at heq
    contradiction
  · next heq =>
-    rw [mkGate, Array.get_push_eq] at heq
+    rw [mkGate, Array.getElem_push_eq] at heq
    injection heq with heq1 heq2 heq3 heq4
    dsimp only
    congr 2
@@ -132,7 +132,7 @@ The AIG produced by `AIG.mkAtom` agrees with the input AIG on all indices that a
 -/
 theorem mkAtom_decl_eq (aig : AIG α) (var : α) (idx : Nat) {h : idx < aig.decls.size} {hbound} :
    (aig.mkAtom var).aig.decls[idx]'hbound = aig.decls[idx] := by
-  simp only [mkAtom, Array.get_push]
+  simp only [mkAtom, Array.getElem_push]
  split
  · rfl
  · contradiction
@@ -149,14 +149,14 @@ theorem denote_mkAtom {aig : AIG α} :
  unfold denote denote.go
  split
  · next heq =>
-    rw [mkAtom, Array.get_push_eq] at heq
+    rw [mkAtom, Array.getElem_push_eq] at heq
    contradiction
  · next heq =>
-    rw [mkAtom, Array.get_push_eq] at heq
+    rw [mkAtom, Array.getElem_push_eq] at heq
    injection heq with heq
    rw [heq]
  · next heq =>
-    rw [mkAtom, Array.get_push_eq] at heq
+    rw [mkAtom, Array.getElem_push_eq] at heq
    contradiction

 /--
@@ -172,7 +172,7 @@ The AIG produced by `AIG.mkConst` agrees with the input AIG on all indices that
 theorem mkConst_decl_eq (aig : AIG α) (val : Bool) (idx : Nat) {h : idx < aig.decls.size} :
    have := mkConst_le_size aig val
    (aig.mkConst val).aig.decls[idx]'(by omega) = aig.decls[idx] := by
-  simp only [mkConst, Array.get_push]
+  simp only [mkConst, Array.getElem_push]
  split
  · rfl
  · contradiction
@@ -188,14 +188,14 @@ theorem denote_mkConst {aig : AIG α} : ⟦(aig.mkConst val), assign⟧ = val :=
  unfold denote denote.go
  split
  · next heq =>
-    rw [mkConst, Array.get_push_eq] at heq
+    rw [mkConst, Array.getElem_push_eq] at heq
    injection heq with heq
    rw [heq]
  · next heq =>
-    rw [mkConst, Array.get_push_eq] at heq
+    rw [mkConst, Array.getElem_push_eq] at heq
    contradiction
  · next heq =>
-    rw [mkConst, Array.get_push_eq] at heq
+    rw [mkConst, Array.getElem_push_eq] at heq
    contradiction

 /--
--- a/src/Std/Sat/AIG/RefVec.lean
+++ b/src/Std/Sat/AIG/RefVec.lean
@@ -59,7 +59,7 @@ def push (s : RefVec aig len) (ref : AIG.Ref aig) : RefVec aig (len + 1) :=
    by simp [hlen],
    by
      intro i hi
-      simp only [Array.get_push]
+      simp only [Array.getElem_push]
      split
      · apply hrefs
        omega
@@ -85,7 +85,7 @@ theorem get_push_ref_lt (s : RefVec aig len) (ref : AIG.Ref aig) (idx : Nat)
  simp only [get, push, Ref.mk.injEq]
  cases ref
  simp only [Ref.mk.injEq]
-  rw [Array.get_push_lt]
+  rw [Array.getElem_push_lt]

@[simp]
 theorem get_cast {aig1 aig2 : AIG α} (s : RefVec aig1 len) (idx : Nat) (hidx : idx < len)
--- a/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
+++ b/src/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
@@ -111,7 +111,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
          ⟨units.size, units_size_lt_updatedUnits_size⟩
        have i_gt_zero : i.1 > 0 := by rw [i_eq_l]; exact l.1.2.1
        refine ⟨mostRecentUnitIdx, l.2, i_gt_zero, ?_⟩
-        simp only [insertUnit, h3, ite_false, Array.get_push_eq, i_eq_l, reduceCtorEq]
+        simp only [insertUnit, h3, ite_false, Array.getElem_push_eq, i_eq_l, reduceCtorEq]
        constructor
        · rfl
        · constructor
@@ -132,7 +132,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
                · intro h
                  simp only [← h, not_true, mostRecentUnitIdx] at hk
                  exact hk rfl
-              rw [Array.get_push_lt _ _ _ k_in_bounds]
+              rw [Array.getElem_push_lt _ _ _ k_in_bounds]
              rw [i_eq_l] at h2
              exact h2 ⟨k.1, k_in_bounds⟩
      · next i_ne_l =>
@@ -142,7 +142,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
        constructor
        · exact h1
        · intro j
-          rw [Array.get_push]
+          rw [Array.getElem_push]
          by_cases h : j.val < Array.size units
          · simp only [h, dite_true]
            exact h2 ⟨j.1, h⟩
@@ -189,9 +189,9 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
          exact h5 (has_add _ true)
        | true, false =>
          refine ⟨⟨j.1, j_lt_updatedUnits_size⟩, mostRecentUnitIdx, i_gt_zero, ?_⟩
-          simp only [insertUnit, h5, ite_false, Array.get_push_eq, ne_eq, reduceCtorEq]
+          simp only [insertUnit, h5, ite_false, Array.getElem_push_eq, ne_eq, reduceCtorEq]
          constructor
-          · rw [Array.get_push_lt units l j.1 j.2, h1]
+          · rw [Array.getElem_push_lt units l j.1 j.2, h1]
          · constructor
            · simp [i_eq_l, ← hl]
              rfl
@@ -210,7 +210,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
                    simp [hasAssignment, hl, getElem!, l_in_bounds, h2, hasNegAssignment, decidableGetElem?] at h5
                  | both => simp (config := {decide := true}) only [h] at h3
                · intro k k_ne_j k_ne_l
-                  rw [Array.get_push]
+                  rw [Array.getElem_push]
                  by_cases h : k.1 < units.size
                  · simp only [h, dite_true]
                    have k_ne_j : ⟨k.1, h⟩ ≠ j := by
@@ -226,12 +226,12 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
                      exact k_ne_l rfl
        | false, true =>
          refine ⟨mostRecentUnitIdx, ⟨j.1, j_lt_updatedUnits_size⟩, i_gt_zero, ?_⟩
-          simp [insertUnit, h5, ite_false, Array.get_push_eq, ne_eq]
+          simp [insertUnit, h5, ite_false, Array.getElem_push_eq, ne_eq]
          constructor
          · simp [i_eq_l, ← hl]
            rfl
          · constructor
-            · rw [Array.get_push_lt units l j.1 j.2, h1]
+            · rw [Array.getElem_push_lt units l j.1 j.2, h1]
            · constructor
              · simp only [i_eq_l]
                rw [Array.getElem_modify_self]
@@ -247,7 +247,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
                  | neg  => simp (config := {decide := true}) only [h] at h3
                  | both => simp (config := {decide := true}) only [h] at h3
                · intro k k_ne_l k_ne_j
-                  rw [Array.get_push]
+                  rw [Array.getElem_push]
                  by_cases h : k.1 < units.size
                  · simp only [h, dite_true]
                    have k_ne_j : ⟨k.1, h⟩ ≠ j := by
@@ -275,13 +275,13 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
        refine ⟨⟨j.1, j_lt_updatedUnits_size⟩, b,i_gt_zero, ?_⟩
        simp only [insertUnit, h5, ite_false, reduceCtorEq]
        constructor
-        · rw [Array.get_push_lt units l j.1 j.2, h1]
+        · rw [Array.getElem_push_lt units l j.1 j.2, h1]
        · constructor
          · rw [Array.getElem_modify_of_ne (Ne.symm i_ne_l), h2]
          · constructor
            · exact h3
            · intro k k_ne_j
-              rw [Array.get_push]
+              rw [Array.getElem_push]
              by_cases h : k.val < units.size
              · simp only [h, dite_true]
                have k_ne_j : ⟨k.1, h⟩ ≠ j := by
@@ -307,11 +307,11 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
    constructor
    · split
      · exact h1
-      · simp only [Array.get_push_lt units l j1.1 j1.2, h1]
+      · simp only [Array.getElem_push_lt units l j1.1 j1.2, h1]
    · constructor
      · split
        · exact h2
-        · simp only [Array.get_push_lt units l j2.1 j2.2, h2]
+        · simp only [Array.getElem_push_lt units l j2.1 j2.2, h2]
      · constructor
        · split
          · exact h3
@@ -336,7 +336,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
              split
              · exact h5 ⟨k.1, k_in_bounds⟩ k_ne_j1 k_ne_j2
              · simp only [ne_eq]
-                rw [Array.get_push]
+                rw [Array.getElem_push]
                simp only [k_in_bounds, dite_true]
                exact h5 ⟨k.1, k_in_bounds⟩ k_ne_j1 k_ne_j2
            · next k_not_lt_units_size =>
@@ -354,7 +354,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
                  rcases Nat.lt_or_eq_of_le <| Nat.le_of_lt_succ k_property with k_lt_units_size | k_eq_units_size
                  · exfalso; exact k_not_lt_units_size k_lt_units_size
                  · exact k_eq_units_size
-                simp only [k_eq_units_size, Array.get_push_eq, ne_eq]
+                simp only [k_eq_units_size, Array.getElem_push_eq, ne_eq]
                intro l_eq_i
                simp [getElem!, l_eq_i, i_in_bounds, h3, has_both, decidableGetElem?] at h

--- a/src/kernel/declaration.cpp
+++ b/src/kernel/declaration.cpp
@@ -126,7 +126,6 @@ constructor_val::constructor_val(name const & n, names const & lparams, expr con
    object_ref(lean_mk_constructor_val(n.to_obj_arg(), lparams.to_obj_arg(), type.to_obj_arg(), induct.to_obj_arg(),
                                       nat(cidx).to_obj_arg(), nat(nparams).to_obj_arg(), nat(nfields).to_obj_arg(), is_unsafe)) {
 }
-
 bool constructor_val::is_unsafe() const { return lean_constructor_val_is_unsafe(to_obj_arg()); }

 extern "C" object * lean_mk_recursor_val(object * n, object * lparams, object * type, object * all,
@@ -143,6 +142,18 @@ recursor_val::recursor_val(name const & n, names const & lparams, expr const & t
                                    nat(nminors).to_obj_arg(), rules.to_obj_arg(), k, is_unsafe)) {
 }

+name const & recursor_val::get_major_induct() const {
+    unsigned int n = get_major_idx();
+    expr const * t = &(to_constant_val().get_type());
+    for (unsigned int i = 0; i < n; i++) {
+        t = &(binding_body(*t));
+    }
+    t = &(binding_domain(*t));
+    t = &(get_app_fn(*t));
+    return const_name(*t);
+}
+
+
 bool recursor_val::is_k() const { return lean_recursor_k(to_obj_arg()); }
 bool recursor_val::is_unsafe() const { return lean_recursor_is_unsafe(to_obj_arg()); }

--- a/src/kernel/declaration.h
+++ b/src/kernel/declaration.h
@@ -370,7 +370,7 @@ public:
    recursor_val & operator=(recursor_val && other) { object_ref::operator=(std::move(other)); return *this; }
    constant_val const & to_constant_val() const { return static_cast<constant_val const &>(cnstr_get_ref(*this, 0)); }
    name const & get_name() const { return to_constant_val().get_name(); }
-    name const & get_induct() const { return get_name().get_prefix(); }
+    name const & get_major_induct() const;
    names const & get_all() const { return static_cast<names const &>(cnstr_get_ref(*this, 1)); }
    unsigned get_nparams() const { return static_cast<nat const &>(cnstr_get_ref(*this, 2)).get_small_value(); }
    unsigned get_nindices() const { return static_cast<nat const &>(cnstr_get_ref(*this, 3)).get_small_value(); }
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -79,21 +79,22 @@ extern "C" object * lean_lit_type(obj_arg e);
 expr lit_type(literal const & lit) { return expr(lean_lit_type(lit.to_obj_arg())); }

 extern "C" uint64_t lean_expr_hash(obj_arg e);
-unsigned hash(expr const & e) {
-    object * o = e.raw();
-    unsigned r = static_cast<unsigned>(lean_ctor_get_uint64(o, lean_ctor_num_objs(o)*sizeof(object*)));
-    lean_assert(r == lean_expr_hash(e.to_obj_arg()));
-    return r;
+unsigned hash_core(expr const & e) {
+    return lean_expr_hash(e.to_obj_arg());
 }

 extern "C" uint8 lean_expr_has_fvar(obj_arg e);
-bool has_fvar(expr const & e) { return lean_expr_has_fvar(e.to_obj_arg()); }
+bool has_fvar_core(expr const & e) {
+    return lean_expr_has_fvar(e.to_obj_arg());
+}

 extern "C" uint8 lean_expr_has_expr_mvar(obj_arg e);
-bool has_expr_mvar(expr const & e) { return lean_expr_has_expr_mvar(e.to_obj_arg()); }
+bool has_expr_mvar_core(expr const & e) {
+    return lean_expr_has_expr_mvar(e.to_obj_arg());
+}

 extern "C" uint8 lean_expr_has_level_mvar(obj_arg e);
-bool has_univ_mvar(expr const & e) { return lean_expr_has_level_mvar(e.to_obj_arg()); }
+bool has_univ_mvar_core(expr const & e) { return lean_expr_has_level_mvar(e.to_obj_arg()); }

 extern "C" uint8 lean_expr_has_level_param(obj_arg e);
 bool has_univ_param(expr const & e) { return lean_expr_has_level_param(e.to_obj_arg()); }
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -123,11 +123,37 @@ inline bool is_eqp(optional<expr> const & a, optional<expr> const & b) {
    return static_cast<bool>(a) == static_cast<bool>(b) && (!a || is_eqp(*a, *b));
 }

-unsigned hash(expr const & e);
-bool has_expr_mvar(expr const & e);
-bool has_univ_mvar(expr const & e);
+inline uint64_t get_data(expr const & e) {
+    return lean_ctor_get_uint64(e.raw(), lean_ctor_num_objs(e.raw())*sizeof(object*));
+}
+/* This is the implementation in Lean */
+unsigned hash_core(expr const & e);
+inline unsigned hash(expr const & e) {
+    unsigned r = static_cast<unsigned>(get_data(e));
+    lean_assert(r == hash_core(e));
+    return r;
+}
+/* This is the implementation in Lean */
+bool has_expr_mvar_core(expr const & e);
+inline bool has_expr_mvar(expr const & e) {
+    bool r = ((get_data(e) >> 41) & 1) == 1;
+    lean_assert(r == has_expr_mvar_core(e)); // ensure the C++ implementation matches the Lean one.
+    return r;
+}
+bool has_univ_mvar_core(expr const & e);
+inline bool has_univ_mvar(expr const & e) {
+    bool r = ((get_data(e) >> 42) & 1) == 1;
+    lean_assert(r == has_univ_mvar_core(e)); // ensure the C++ implementation matches the Lean one.
+    return r;
+}
 inline bool has_mvar(expr const & e) { return has_expr_mvar(e) || has_univ_mvar(e); }
-bool has_fvar(expr const & e);
+/* This is the implementation in Lean */
+bool has_fvar_core(expr const & e);
+inline bool has_fvar(expr const & e) {
+    bool r = ((get_data(e) >> 40) & 1) == 1;
+    lean_assert(r == has_fvar_core(e)); // ensure the C++ implementation matches the Lean one.
+    return r;
+}
 bool has_univ_param(expr const & e);
 unsigned get_loose_bvar_range(expr const & e);

--- a/src/kernel/inductive.h
+++ b/src/kernel/inductive.h
@@ -33,7 +33,7 @@ inline expr to_cnstr_when_K(environment const & env, recursor_val const & rval,
    lean_assert(rval.is_k());
    expr app_type    = whnf(infer_type(e));
    expr const & app_type_I = get_app_fn(app_type);
-    if (!is_constant(app_type_I) || const_name(app_type_I) != rval.get_induct()) return e; // type incorrect
+    if (!is_constant(app_type_I) || const_name(app_type_I) != rval.get_major_induct()) return e; // type incorrect
    if (has_expr_mvar(app_type)) {
        buffer<expr> app_type_args;
        get_app_args(app_type, app_type_args);
@@ -94,7 +94,7 @@ inline optional<expr> inductive_reduce_rec(environment const & env, expr const &
    else if (is_string_lit(major))
        major = string_lit_to_constructor(major);
    else
-        major = to_cnstr_when_structure(env, rec_val.get_induct(), major, whnf, infer_type);
+        major = to_cnstr_when_structure(env, rec_val.get_major_induct(), major, whnf, infer_type);
    optional<recursor_rule> rule = get_rec_rule_for(rec_val, major);
    if (!rule) return none_expr();
    buffer<expr> major_args;
--- a/tests/lean/run/array_isEqvAux.lean
+++ b/tests/lean/run/array_isEqvAux.lean
@@ -17,6 +17,8 @@ After unfolding the instances 'instDecidableEqNat', 'Array.instDecidableEq' and

 example : #[0, 1] = #[0, 1] := by decide

+example : let a := Array.range (10^6); a == a := by native_decide
+
 /-!
 There are other `Array` functions that use well-founded recursion,
 which we've marked as `@[semireducible]`. We test that `decide` can unfold them here.
--- a/tests/lean/run/issue5661.lean
+++ b/tests/lean/run/issue5661.lean
@@ -0,0 +1,73 @@
+import Lean.Meta.Basic
+
+inductive StructLike α where
+  | mk : α → StructLike α
+
+inductive Nested where
+  | nest : StructLike Nested → Nested
+  | other
+
+/--
+info: theorem Nested.nest.sizeOf_spec : ∀ (a : StructLike Nested), sizeOf (Nested.nest a) = 1 + sizeOf a :=
+fun a => Eq.refl (1 + sizeOf a)
+-/
+#guard_msgs in
+#print Nested.nest.sizeOf_spec
+
+/-- info: StructLike -/
+#guard_msgs in
+open Lean Meta in
+run_meta do
+  let i ← getConstInfoRec ``Nested.rec_1
+  logInfo m!"{i.getMajorInduct}"
+
+theorem works (x : StructLike Nested) : StructLike.rec
+  (motive := fun _ => Bool)
+  (mk := fun _ => true)
+  x = true
+  := rfl
+
+theorem failed_before (x : StructLike Nested) : Nested.rec_1
+  (motive_1 := fun _ => Bool) (motive_2 := fun _ => Bool)
+  (nest := fun _ _ => true)
+  (other := true)
+  (mk := fun _ _ => true)
+  x = true
+  := rfl
+
+
+-- The original surface bug
+
+inductive Set (α : Type u) where
+  | mk (l : List α)
+
+inductive Value where
+  | prim
+  | set (s : Set Value)
+
+instance : DecidableEq Value := sorry
+
+mutual
+
+def Value.lt : Value → Value → Bool
+  | .prim, .prim => false
+  | .set (.mk vs₁), .set (.mk vs₂) => Values.lt vs₁ vs₂
+  | .prim, .set _ => true
+  | .set _, .prim => false
+
+def Values.lt : List Value → List Value → Bool
+  | [], [] => false
+  | [], _ => true
+  | _, [] => false
+  | v₁ :: vs₁, v₂ :: vs₂ => Value.lt v₁ v₂ || (v₁ = v₂ && Values.lt vs₁ vs₂)
+
+end
+
+theorem Value.lt_irrefl (v : Value) :
+  ¬ Value.lt v v
+:= by
+  cases v
+  case set a =>
+    show ¬Values.lt a.1 a.1 = true
+    sorry
+  all_goals sorry
--- a/tests/lean/simpArrayIdx.lean
+++ b/tests/lean/simpArrayIdx.lean
@@ -10,7 +10,7 @@ variable (j_lt : j < (a.set! i v).size)
 #check_simp (i + 0) ~> i

 #check_simp (a.set! i v).get ⟨i, g⟩ ~> v
-#check_simp (a.set! i v).get! i ~> if i < a.size then v else default
+#check_simp (a.set! i v).get! i ~> (a.setD i v)[i]!
 #check_simp (a.set! i v).getD i d ~> if i < a.size then v else d
 #check_simp (a.set! i v)[i] ~> v
Author	SHA1	Message	Date
Kim Morrison	7b7ca92383	chore: upstream List.modify, add lemmas, relate to Array.modify	2024-10-22 11:06:54 +11:00
Tobias Grosser	8d789f7b63	feat: add BitVec.toInt_sub, simplify BitVec.toInt_neg (#5772 ) This also requires us to expand the theory of `Int.bmod`. --------- Co-authored-by: Alex Keizer <alex@keizer.dev>	2024-10-21 22:38:29 +00:00
Leonardo de Moura	82d31a1793	perf: `has_univ_mvar`, `has_univ_mvar`, and `has_fvar` in C++ (#5793 ) `instantiate_mvars` is now implemented in C/C++, and makes many calls to `has_fvar`, `has_mvar`. The new C/C++ implementations are inlined and avoid unnecessary RC inc/decs.	2024-10-21 16:56:30 +00:00
Joachim Breitner	76164b284b	fix: RecursorVal.getInduct to return name of major argument’s type (#5679 ) Previously `RecursorVal.getInduct` would return the prefix of the recursor’s name, which is unlikely the right value for the “derived” recursors in nested recursion. The code using `RecursorVal.getInduct` seems to expect the name of the inductive type of major argument here. If we return that name, this fixes #5661. This bug becomes more visible now that we have structural mutual recursion. Also, to avoid confusion, renames the function to ``getMajorInduct`.	2024-10-21 08:45:18 +00:00
Kim Morrison	51377afd6c	feat: simp lemmas for Array.isEqv and beq (#5786 ) - [ ] depends on: #5785	2024-10-21 07:37:40 +00:00
Kim Morrison	6f642abe70	feat: Nat.forall_lt_succ and variants (#5785 )	2024-10-21 06:51:23 +00:00
Kim Morrison	8151ac79d6	chore: Array cleanup (#5782 ) More cleanup of Array API. More to come.	2024-10-21 06:00:37 +00:00
Kim Morrison	4f18c29cb4	chore: make 'while' available earlier (#5784 )	2024-10-21 05:56:37 +00:00
Kim Morrison	5d155d8b02	chore: simplify signature of Array.mapIdx (#5749 ) This PR simplifies the signature of `Array.mapIdx`, to take a function `f : Nat \to \a \to \b` rather than a function `f : Fin as.size \to \a \to \b`. Lean doesn't actually use the extra generality anywhere (so in fact this change simplifies all the call sites of `Array.mapIdx`, since we no longer need to throw away the proof). This change would make the function signature equivalent to `List.mapIdx`, hence making it easier to write verification lemmas. We keep the original behaviour as `Array.mapFinIdx`.	2024-10-21 05:48:42 +00:00