diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean index 458ba8bf92..62272a03dc 100644 --- a/src/Init/Data/Array/Lemmas.lean +++ b/src/Init/Data/Array/Lemmas.lean @@ -401,6 +401,46 @@ namespace Array @[simp] theorem empty_eq {xs : Array α} : #[] = xs ↔ xs = #[] := by cases xs <;> simp +/-! ### size -/ + +theorem eq_empty_of_size_eq_zero (h : l.size = 0) : l = #[] := by + cases l + simp_all + +theorem ne_empty_of_size_eq_add_one (h : l.size = n + 1) : l ≠ #[] := by + cases l + simpa using List.ne_nil_of_length_eq_add_one h + +theorem ne_empty_of_size_pos (h : 0 < l.size) : l ≠ #[] := by + cases l + simpa using List.ne_nil_of_length_pos h + +@[simp] theorem size_eq_zero : l.size = 0 ↔ l = #[] := + ⟨eq_empty_of_size_eq_zero, fun h => h ▸ rfl⟩ + +theorem size_pos_of_mem {a : α} {l : Array α} (h : a ∈ l) : 0 < l.size := by + cases l + simp only [mem_toArray] at h + simpa using List.length_pos_of_mem h + +theorem exists_mem_of_size_pos {l : Array α} (h : 0 < l.size) : ∃ a, a ∈ l := by + cases l + simpa using List.exists_mem_of_length_pos h + +theorem size_pos_iff_exists_mem {l : Array α} : 0 < l.size ↔ ∃ a, a ∈ l := + ⟨exists_mem_of_size_pos, fun ⟨_, h⟩ => size_pos_of_mem h⟩ + +theorem exists_mem_of_size_eq_add_one {l : Array α} (h : l.size = n + 1) : ∃ a, a ∈ l := by + cases l + simpa using List.exists_mem_of_length_eq_add_one h + +theorem size_pos {l : Array α} : 0 < l.size ↔ l ≠ #[] := + Nat.pos_iff_ne_zero.trans (not_congr size_eq_zero) + +theorem size_eq_one {l : Array α} : l.size = 1 ↔ ∃ a, l = #[a] := by + cases l + simpa using List.length_eq_one + /-! ### push -/ theorem push_ne_empty {a : α} {xs : Array α} : xs.push a ≠ #[] := by @@ -442,49 +482,33 @@ theorem push_eq_push {a b : α} {xs ys : Array α} : xs.push a = ys.push b ↔ a · rintro ⟨rfl, rfl⟩ rfl -/-! ### size -/ +theorem exists_push_of_ne_empty {xs : Array α} (h : xs ≠ #[]) : + ∃ (ys : Array α) (a : α), xs = ys.push a := by + rcases xs with ⟨xs⟩ + simp only [ne_eq, mk.injEq] at h + exact ⟨(xs.take (xs.length - 1)).toArray, xs.getLast h, by simp⟩ -theorem eq_empty_of_size_eq_zero (h : l.size = 0) : l = #[] := by - cases l - simp_all +theorem ne_empty_iff_exists_push {xs : Array α} : + xs ≠ #[] ↔ ∃ (ys : Array α) (a : α), xs = ys.push a := + ⟨exists_push_of_ne_empty, fun ⟨_, _, eq⟩ => eq.symm ▸ push_ne_empty⟩ -theorem ne_empty_of_size_eq_add_one (h : l.size = n + 1) : l ≠ #[] := by - cases l - simpa using List.ne_nil_of_length_eq_add_one h +theorem exists_push_of_size_pos {xs : Array α} (h : 0 < xs.size) : + ∃ (ys : Array α) (a : α), xs = ys.push a := by + replace h : xs ≠ #[] := size_pos.mp h + exact exists_push_of_ne_empty h -theorem ne_empty_of_size_pos (h : 0 < l.size) : l ≠ #[] := by - cases l - simpa using List.ne_nil_of_length_pos h +theorem size_pos_iff_exists_push {xs : Array α} : + 0 < xs.size ↔ ∃ (ys : Array α) (a : α), xs = ys.push a := + ⟨exists_push_of_size_pos, fun ⟨_, _, eq⟩ => by simp [eq]⟩ -@[simp] theorem size_eq_zero : l.size = 0 ↔ l = #[] := - ⟨eq_empty_of_size_eq_zero, fun h => h ▸ rfl⟩ +theorem exists_push_of_size_eq_add_one {xs : Array α} (h : xs.size = n + 1) : + ∃ (ys : Array α) (a : α), xs = ys.push a := + exists_push_of_size_pos (by simp [h]) -theorem size_pos_of_mem {a : α} {l : Array α} (h : a ∈ l) : 0 < l.size := by - cases l - simp only [mem_toArray] at h - simpa using List.length_pos_of_mem h +/-! ## L[i] and L[i]? -/ -theorem exists_mem_of_size_pos {l : Array α} (h : 0 < l.size) : ∃ a, a ∈ l := by - cases l - simpa using List.exists_mem_of_length_pos h - -theorem size_pos_iff_exists_mem {l : Array α} : 0 < l.size ↔ ∃ a, a ∈ l := - ⟨exists_mem_of_size_pos, fun ⟨_, h⟩ => size_pos_of_mem h⟩ - -theorem exists_mem_of_size_eq_add_one {l : Array α} (h : l.size = n + 1) : ∃ a, a ∈ l := by - cases l - simpa using List.exists_mem_of_length_eq_add_one h - -theorem size_pos {l : Array α} : 0 < l.size ↔ l ≠ #[] := - Nat.pos_iff_ne_zero.trans (not_congr size_eq_zero) - -theorem size_eq_one {l : Array α} : l.size = 1 ↔ ∃ a, l = #[a] := by - cases l - simpa using List.length_eq_one - -/-! ### mem -/ - -@[simp] theorem getElem_mk {xs : List α} {i : Nat} (h : i < xs.length) : (Array.mk xs)[i] = xs[i] := rfl +@[deprecated List.getElem_toArray (since := "2024-11-29")] +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] := rfl @@ -1512,6 +1536,18 @@ theorem getElem?_append {as bs : Array α} {n : Nat} : · exact getElem?_append_left h · exact getElem?_append_right (by simpa using h) +@[simp] theorem toArray_eq_append_iff {xs : List α} {as bs : Array α} : + xs.toArray = as ++ bs ↔ xs = as.toList ++ bs.toList := by + cases as + cases bs + simp + +@[simp] theorem append_eq_toArray_iff {as bs : Array α} {xs : List α} : + as ++ bs = xs.toArray ↔ as.toList ++ bs.toList = xs := by + cases as + cases bs + simp + /-! ### flatten -/ @[simp] theorem toList_flatten {l : Array (Array α)} : diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index 8c510b8f4b..1c165b9cf7 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/src/Init/Data/List/Lemmas.lean @@ -83,44 +83,12 @@ open Nat @[simp] theorem nil_eq {α} {xs : List α} : [] = xs ↔ xs = [] := by cases xs <;> simp -/-! ### cons -/ - -theorem cons_ne_nil (a : α) (l : List α) : a :: l ≠ [] := nofun - -@[simp] -theorem cons_ne_self (a : α) (l : List α) : a :: l ≠ l := mt (congrArg length) (Nat.succ_ne_self _) - -@[simp] theorem ne_cons_self {a : α} {l : List α} : l ≠ a :: l := by - rw [ne_eq, eq_comm] - simp - -theorem head_eq_of_cons_eq (H : h₁ :: t₁ = h₂ :: t₂) : h₁ = h₂ := (cons.inj H).1 - -theorem tail_eq_of_cons_eq (H : h₁ :: t₁ = h₂ :: t₂) : t₁ = t₂ := (cons.inj H).2 - -theorem cons_inj_right (a : α) {l l' : List α} : a :: l = a :: l' ↔ l = l' := - ⟨tail_eq_of_cons_eq, congrArg _⟩ - -@[deprecated cons_inj_right (since := "2024-06-15")] abbrev cons_inj := @cons_inj_right - -theorem cons_eq_cons {a b : α} {l l' : List α} : a :: l = b :: l' ↔ a = b ∧ l = l' := - List.cons.injEq .. ▸ .rfl - -theorem exists_cons_of_ne_nil : ∀ {l : List α}, l ≠ [] → ∃ b L, l = b :: L - | c :: l', _ => ⟨c, l', rfl⟩ - -theorem singleton_inj {α : Type _} {a b : α} : [a] = [b] ↔ a = b := by - simp - /-! ### length -/ theorem eq_nil_of_length_eq_zero (_ : length l = 0) : l = [] := match l with | [] => rfl theorem ne_nil_of_length_eq_add_one (_ : length l = n + 1) : l ≠ [] := fun _ => nomatch l -@[deprecated ne_nil_of_length_eq_add_one (since := "2024-06-16")] -abbrev ne_nil_of_length_eq_succ := @ne_nil_of_length_eq_add_one - theorem ne_nil_of_length_pos (_ : 0 < length l) : l ≠ [] := fun _ => nomatch l @[simp] theorem length_eq_zero : length l = 0 ↔ l = [] := @@ -156,6 +124,36 @@ theorem length_pos {l : List α} : 0 < length l ↔ l ≠ [] := theorem length_eq_one {l : List α} : length l = 1 ↔ ∃ a, l = [a] := ⟨fun h => match l, h with | [_], _ => ⟨_, rfl⟩, fun ⟨_, h⟩ => by simp [h]⟩ +/-! ### cons -/ + +theorem cons_ne_nil (a : α) (l : List α) : a :: l ≠ [] := nofun + +@[simp] +theorem cons_ne_self (a : α) (l : List α) : a :: l ≠ l := mt (congrArg length) (Nat.succ_ne_self _) + +@[simp] theorem ne_cons_self {a : α} {l : List α} : l ≠ a :: l := by + rw [ne_eq, eq_comm] + simp + +theorem head_eq_of_cons_eq (H : h₁ :: t₁ = h₂ :: t₂) : h₁ = h₂ := (cons.inj H).1 + +theorem tail_eq_of_cons_eq (H : h₁ :: t₁ = h₂ :: t₂) : t₁ = t₂ := (cons.inj H).2 + +theorem cons_inj_right (a : α) {l l' : List α} : a :: l = a :: l' ↔ l = l' := + ⟨tail_eq_of_cons_eq, congrArg _⟩ + +theorem cons_eq_cons {a b : α} {l l' : List α} : a :: l = b :: l' ↔ a = b ∧ l = l' := + List.cons.injEq .. ▸ .rfl + +theorem exists_cons_of_ne_nil : ∀ {l : List α}, l ≠ [] → ∃ b L, l = b :: L + | c :: l', _ => ⟨c, l', rfl⟩ + +theorem ne_nil_iff_exists_cons {l : List α} : l ≠ [] ↔ ∃ b L, l = b :: L := + ⟨exists_cons_of_ne_nil, fun ⟨_, _, eq⟩ => eq.symm ▸ cons_ne_nil _ _⟩ + +theorem singleton_inj {α : Type _} {a b : α} : [a] = [b] ↔ a = b := by + simp + /-! ## L[i] and L[i]? -/ /-! ### `get` and `get?`. @@ -163,57 +161,29 @@ theorem length_eq_one {l : List α} : length l = 1 ↔ ∃ a, l = [a] := We simplify `l.get i` to `l[i.1]'i.2` and `l.get? i` to `l[i]?`. -/ -theorem get_cons_zero : get (a::l) (0 : Fin (l.length + 1)) = a := rfl +@[simp] theorem get_eq_getElem (l : List α) (i : Fin l.length) : l.get i = l[i.1]'i.2 := rfl -theorem get_cons_succ {as : List α} {h : i + 1 < (a :: as).length} : - (a :: as).get ⟨i+1, h⟩ = as.get ⟨i, Nat.lt_of_succ_lt_succ h⟩ := rfl - -theorem get_cons_succ' {as : List α} {i : Fin as.length} : - (a :: as).get i.succ = as.get i := rfl - -@[deprecated "Deprecated without replacement." (since := "2024-07-09")] -theorem get_cons_cons_one : (a₁ :: a₂ :: as).get (1 : Fin (as.length + 2)) = a₂ := rfl - -theorem get_mk_zero : ∀ {l : List α} (h : 0 < l.length), l.get ⟨0, h⟩ = l.head (length_pos.mp h) - | _::_, _ => rfl - -theorem get?_zero (l : List α) : l.get? 0 = l.head? := by cases l <;> rfl - -theorem get?_len_le : ∀ {l : List α} {n}, length l ≤ n → l.get? n = none +theorem get?_eq_none : ∀ {l : List α} {n}, length l ≤ n → l.get? n = none | [], _, _ => rfl - | _ :: l, _+1, h => get?_len_le (l := l) <| Nat.le_of_succ_le_succ h + | _ :: l, _+1, h => get?_eq_none (l := l) <| Nat.le_of_succ_le_succ h theorem get?_eq_get : ∀ {l : List α} {n} (h : n < l.length), l.get? n = some (get l ⟨n, h⟩) | _ :: _, 0, _ => rfl | _ :: l, _+1, _ => get?_eq_get (l := l) _ -theorem get?_eq_some : l.get? n = some a ↔ ∃ h, get l ⟨n, h⟩ = a := +theorem get?_eq_some_iff : l.get? n = some a ↔ ∃ h, get l ⟨n, h⟩ = a := ⟨fun e => - have : n < length l := Nat.gt_of_not_le fun hn => by cases get?_len_le hn ▸ e + have : n < length l := Nat.gt_of_not_le fun hn => by cases get?_eq_none hn ▸ e ⟨this, by rwa [get?_eq_get this, Option.some.injEq] at e⟩, fun ⟨_, e⟩ => e ▸ get?_eq_get _⟩ -theorem get?_eq_none : l.get? n = none ↔ length l ≤ n := - ⟨fun e => Nat.ge_of_not_lt (fun h' => by cases e ▸ get?_eq_some.2 ⟨h', rfl⟩), get?_len_le⟩ +theorem get?_eq_none_iff : l.get? n = none ↔ length l ≤ n := + ⟨fun e => Nat.ge_of_not_lt (fun h' => by cases e ▸ get?_eq_some_iff.2 ⟨h', rfl⟩), get?_eq_none⟩ @[simp] theorem get?_eq_getElem? (l : List α) (i : Nat) : l.get? i = l[i]? := by - simp only [getElem?, decidableGetElem?]; split + simp only [getElem?_def]; split · exact (get?_eq_get ‹_›) - · exact (get?_eq_none.2 <| Nat.not_lt.1 ‹_›) - -@[simp] theorem get_eq_getElem (l : List α) (i : Fin l.length) : l.get i = l[i.1]'i.2 := rfl - -theorem getElem?_eq_some {l : List α} : l[i]? = some a ↔ ∃ h : i < l.length, l[i]'h = a := by - simpa using get?_eq_some - -/-- -If one has `l.get i` in an expression (with `i : Fin l.length`) and `h : l = l'`, -`rw [h]` will give a "motive it not type correct" error, as it cannot rewrite the -`i : Fin l.length` to `Fin l'.length` directly. The theorem `get_of_eq` can be used to make -such a rewrite, with `rw [get_of_eq h]`. --/ -theorem get_of_eq {l l' : List α} (h : l = l') (i : Fin l.length) : - get l i = get l' ⟨i, h ▸ i.2⟩ := by cases h; rfl + · exact (get?_eq_none_iff.2 <| Nat.not_lt.1 ‹_›) /-! ### getD @@ -224,42 +194,29 @@ Because of this, there is only minimal API for `getD`. @[simp] theorem getD_eq_getElem?_getD (l) (n) (a : α) : getD l n a = (l[n]?).getD a := by simp [getD] -@[deprecated getD_eq_getElem?_getD (since := "2024-06-12")] -theorem getD_eq_get? : ∀ l n (a : α), getD l n a = (get? l n).getD a := by simp - /-! ### get! We simplify `l.get! n` to `l[n]!`. -/ -theorem get!_of_get? [Inhabited α] : ∀ {l : List α} {n}, get? l n = some a → get! l n = a - | _a::_, 0, rfl => rfl - | _::l, _+1, e => get!_of_get? (l := l) e - theorem get!_eq_getD [Inhabited α] : ∀ (l : List α) n, l.get! n = l.getD n default | [], _ => rfl | _a::_, 0 => rfl | _a::l, n+1 => get!_eq_getD l n -theorem get!_len_le [Inhabited α] : ∀ {l : List α} {n}, length l ≤ n → l.get! n = (default : α) - | [], _, _ => rfl - | _ :: l, _+1, h => get!_len_le (l := l) <| Nat.le_of_succ_le_succ h - @[simp] theorem get!_eq_getElem! [Inhabited α] (l : List α) (n) : l.get! n = l[n]! := by simp [get!_eq_getD] rfl -/-! ### getElem! -/ +/-! ### getElem! -@[simp] theorem getElem!_nil [Inhabited α] {n : Nat} : ([] : List α)[n]! = default := rfl +We simplify `l[n]!` to `(l[n]?).getD default`. +-/ -@[simp] theorem getElem!_cons_zero [Inhabited α] {l : List α} : (a::l)[0]! = a := by - rw [getElem!_pos] <;> simp - -@[simp] theorem getElem!_cons_succ [Inhabited α] {l : List α} : (a::l)[n+1]! = l[n]! := by - by_cases h : n < l.length - · rw [getElem!_pos, getElem!_pos] <;> simp_all [Nat.succ_lt_succ_iff] - · rw [getElem!_neg, getElem!_neg] <;> simp_all [Nat.succ_lt_succ_iff] +@[simp] theorem getElem!_eq_getElem?_getD [Inhabited α] (l : List α) (n : Nat) : + l[n]! = (l[n]?).getD (default : α) := by + simp only [getElem!_def] + split <;> simp_all /-! ### getElem? and getElem -/ @@ -267,23 +224,19 @@ theorem get!_len_le [Inhabited α] : ∀ {l : List α} {n}, length l ≤ n → l simp only [getElem?_def, h, ↓reduceDIte] 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] + simp only [← get?_eq_getElem?, get?_eq_some_iff, 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 only [← get?_eq_getElem?, get?_eq_none_iff] @[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) : - l[i]? = if h : i < l.length then some l[i] else none := by - split <;> simp_all - @[simp] theorem some_getElem_eq_getElem?_iff {α} (xs : List α) (i : Nat) (h : i < xs.length) : (some xs[i] = xs[i]?) ↔ True := by simp [h] @@ -300,9 +253,6 @@ theorem getElem_eq_getElem?_get (l : List α) (i : Nat) (h : i < l.length) : l[i] = l[i]?.get (by simp [getElem?_eq_getElem, h]) := by simp [getElem_eq_iff] -@[deprecated getElem_eq_getElem?_get (since := "2024-09-04")] abbrev getElem_eq_getElem? := - @getElem_eq_getElem?_get - @[simp] theorem getElem?_nil {n : Nat} : ([] : List α)[n]? = none := rfl theorem getElem?_cons_zero {l : List α} : (a::l)[0]? = some a := by simp @@ -314,11 +264,6 @@ theorem getElem?_cons_zero {l : List α} : (a::l)[0]? = some a := by simp theorem getElem?_cons : (a :: l)[i]? = if i = 0 then some a else l[i-1]? := by cases i <;> simp -theorem getElem?_len_le : ∀ {l : List α} {n}, length l ≤ n → l[n]? = none - | [], _, _ => rfl - | _ :: l, _+1, h => by - rw [getElem?_cons_succ, getElem?_len_le (l := l) <| Nat.le_of_succ_le_succ h] - /-- If one has `l[i]` in an expression and `h : l = l'`, `rw [h]` will give a "motive it not type correct" error, as it cannot rewrite the @@ -332,20 +277,10 @@ theorem getElem_of_eq {l l' : List α} (h : l = l') {i : Nat} (w : i < l.length) match i, h with | 0, _ => rfl -@[deprecated getElem_singleton (since := "2024-06-12")] -theorem get_singleton (a : α) (n : Fin 1) : get [a] n = a := by simp - theorem getElem_zero {l : List α} (h : 0 < l.length) : l[0] = l.head (length_pos.mp h) := match l, h with | _ :: _, _ => rfl -theorem getElem!_of_getElem? [Inhabited α] : ∀ {l : List α} {n : Nat}, l[n]? = some a → l[n]! = a - | _a::_, 0, _ => by - rw [getElem!_pos] <;> simp_all - | _::l, _+1, e => by - simp at e - simp_all [getElem!_of_getElem? (l := l) e] - @[ext] theorem ext_getElem? {l₁ l₂ : List α} (h : ∀ n : Nat, l₁[n]? = l₂[n]?) : l₁ = l₂ := ext_get? fun n => by simp_all @@ -356,11 +291,7 @@ theorem ext_getElem {l₁ l₂ : List α} (hl : length l₁ = length l₂) simp_all [getElem?_eq_getElem] else by have h₁ := Nat.le_of_not_lt h₁ - rw [getElem?_len_le h₁, getElem?_len_le]; rwa [← hl] - -theorem ext_get {l₁ l₂ : List α} (hl : length l₁ = length l₂) - (h : ∀ n h₁ h₂, get l₁ ⟨n, h₁⟩ = get l₂ ⟨n, h₂⟩) : l₁ = l₂ := - ext_getElem hl (by simp_all) + rw [getElem?_eq_none h₁, getElem?_eq_none]; rwa [← hl] @[simp] theorem getElem_concat_length : ∀ (l : List α) (a : α) (i) (_ : i = l.length) (w), (l ++ [a])[i]'w = a | [], a, _, h, _ => by subst h; simp @@ -369,19 +300,11 @@ theorem ext_get {l₁ l₂ : List α} (hl : length l₁ = length l₂) theorem getElem?_concat_length (l : List α) (a : α) : (l ++ [a])[l.length]? = some a := by simp -@[deprecated getElem?_concat_length (since := "2024-06-12")] -theorem get?_concat_length (l : List α) (a : α) : (l ++ [a]).get? l.length = some a := by simp +theorem isSome_getElem? {l : List α} {n : Nat} : l[n]?.isSome ↔ n < l.length := by + simp -@[simp] theorem isSome_getElem? {l : List α} {n : Nat} : l[n]?.isSome ↔ n < l.length := by - by_cases h : n < l.length - · simp_all - · simp [h] - simp_all - -@[simp] theorem isNone_getElem? {l : List α} {n : Nat} : l[n]?.isNone ↔ l.length ≤ n := by - by_cases h : n < l.length - · simp_all - · simp [h] +theorem isNone_getElem? {l : List α} {n : Nat} : l[n]?.isNone ↔ l.length ≤ n := by + simp /-! ### mem -/ @@ -493,42 +416,18 @@ theorem getElem_of_mem : ∀ {a} {l : List α}, a ∈ l → ∃ (n : Nat) (h : n | _, _ :: _, .head .. => ⟨0, Nat.succ_pos _, rfl⟩ | _, _ :: _, .tail _ m => let ⟨n, h, e⟩ := getElem_of_mem m; ⟨n+1, Nat.succ_lt_succ h, e⟩ -theorem get_of_mem {a} {l : List α} (h : a ∈ l) : ∃ n, get l n = a := by - obtain ⟨n, h, e⟩ := getElem_of_mem h - exact ⟨⟨n, h⟩, e⟩ - theorem getElem?_of_mem {a} {l : List α} (h : a ∈ l) : ∃ n : Nat, l[n]? = some a := let ⟨n, _, e⟩ := getElem_of_mem h; ⟨n, e ▸ getElem?_eq_getElem _⟩ -theorem get?_of_mem {a} {l : List α} (h : a ∈ l) : ∃ n, l.get? n = some a := - let ⟨⟨n, _⟩, e⟩ := get_of_mem h; ⟨n, e ▸ get?_eq_get _⟩ - -theorem get_mem : ∀ (l : List α) n, get l n ∈ l - | _ :: _, ⟨0, _⟩ => .head .. - | _ :: l, ⟨_+1, _⟩ => .tail _ (get_mem l ..) - theorem mem_of_getElem? {l : List α} {n : Nat} {a : α} (e : l[n]? = some a) : a ∈ l := let ⟨_, e⟩ := getElem?_eq_some_iff.1 e; e ▸ getElem_mem .. -@[deprecated mem_of_getElem? (since := "2024-09-06")] abbrev getElem?_mem := @mem_of_getElem? - -theorem mem_of_get? {l : List α} {n a} (e : l.get? n = some a) : a ∈ l := - let ⟨_, e⟩ := get?_eq_some.1 e; e ▸ get_mem .. - -@[deprecated mem_of_get? (since := "2024-09-06")] abbrev get?_mem := @mem_of_get? - theorem mem_iff_getElem {a} {l : List α} : a ∈ l ↔ ∃ (n : Nat) (h : n < l.length), l[n]'h = a := ⟨getElem_of_mem, fun ⟨_, _, e⟩ => e ▸ getElem_mem ..⟩ -theorem mem_iff_get {a} {l : List α} : a ∈ l ↔ ∃ n, get l n = a := - ⟨get_of_mem, fun ⟨_, e⟩ => e ▸ get_mem ..⟩ - theorem mem_iff_getElem? {a} {l : List α} : a ∈ l ↔ ∃ n : Nat, l[n]? = some a := by simp [getElem?_eq_some_iff, mem_iff_getElem] -theorem mem_iff_get? {a} {l : List α} : a ∈ l ↔ ∃ n, l.get? n = some a := by - simp [getElem?_eq_some_iff, Fin.exists_iff, mem_iff_get] - theorem forall_getElem {l : List α} {p : α → Prop} : (∀ (n : Nat) h, p (l[n]'h)) ↔ ∀ a, a ∈ l → p a := by induction l with @@ -579,18 +478,6 @@ theorem isEmpty_iff_length_eq_zero {l : List α} : l.isEmpty ↔ l.length = 0 := /-! ### any / all -/ -theorem any_beq [BEq α] [LawfulBEq α] {l : List α} : (l.any fun x => a == x) ↔ a ∈ l := by - induction l <;> simp_all - -theorem any_beq' [BEq α] [LawfulBEq α] {l : List α} : (l.any fun x => x == a) ↔ a ∈ l := by - induction l <;> simp_all [eq_comm (a := a)] - -theorem all_bne [BEq α] [LawfulBEq α] {l : List α} : (l.all fun x => a != x) ↔ a ∉ l := by - induction l <;> simp_all - -theorem all_bne' [BEq α] [LawfulBEq α] {l : List α} : (l.all fun x => x != a) ↔ a ∉ l := by - induction l <;> simp_all [eq_comm (a := a)] - theorem any_eq {l : List α} : l.any p = decide (∃ x, x ∈ l ∧ p x) := by induction l <;> simp [*] theorem all_eq {l : List α} : l.all p = decide (∀ x, x ∈ l → p x) := by induction l <;> simp [*] @@ -615,6 +502,18 @@ theorem decide_forall_mem {l : List α} {p : α → Prop} [DecidablePred p] : @[simp] theorem all_eq_false {l : List α} : l.all p = false ↔ ∃ x, x ∈ l ∧ ¬p x := by simp [all_eq] +theorem any_beq [BEq α] [LawfulBEq α] {l : List α} : (l.any fun x => a == x) ↔ a ∈ l := by + simp + +theorem any_beq' [BEq α] [LawfulBEq α] {l : List α} : (l.any fun x => x == a) ↔ a ∈ l := by + simp + +theorem all_bne [BEq α] [LawfulBEq α] {l : List α} : (l.all fun x => a != x) ↔ a ∉ l := by + induction l <;> simp_all + +theorem all_bne' [BEq α] [LawfulBEq α] {l : List α} : (l.all fun x => x != a) ↔ a ∉ l := by + induction l <;> simp_all [eq_comm (a := a)] + /-! ### set -/ -- As `List.set` is defined in `Init.Prelude`, we write the basic simplification lemmas here. @@ -632,19 +531,10 @@ theorem decide_forall_mem {l : List α} {p : α → Prop} [DecidablePred p] : | _ :: _, 0 => by simp | _ :: l, i + 1 => by simp [getElem_set_self] -@[deprecated getElem_set_self (since := "2024-09-04")] abbrev getElem_set_eq := @getElem_set_self - -@[deprecated getElem_set_self (since := "2024-06-12")] -theorem get_set_eq {l : List α} {i : Nat} {a : α} (h : i < (l.set i a).length) : - (l.set i a).get ⟨i, h⟩ = a := by - simp - @[simp] theorem getElem?_set_self {l : List α} {i : Nat} {a : α} (h : i < l.length) : (l.set i a)[i]? = some a := by simp_all [getElem?_eq_some_iff] -@[deprecated getElem?_set_self (since := "2024-09-04")] abbrev getElem?_set_eq := @getElem?_set_self - /-- This differs from `getElem?_set_self` by monadically mapping `Function.const _ a` over the `Option` returned by `l[i]?`. -/ theorem getElem?_set_self' {l : List α} {i : Nat} {a : α} : @@ -666,12 +556,6 @@ theorem getElem?_set_self' {l : List α} {i : Nat} {a : α} : have g : i ≠ j := h ∘ congrArg (· + 1) simp [getElem_set_ne g] -@[deprecated getElem_set_ne (since := "2024-06-12")] -theorem get_set_ne {l : List α} {i j : Nat} (h : i ≠ j) {a : α} - (hj : j < (l.set i a).length) : - (l.set i a).get ⟨j, hj⟩ = l.get ⟨j, by simp at hj; exact hj⟩ := by - simp [h] - @[simp] theorem getElem?_set_ne {l : List α} {i j : Nat} (h : i ≠ j) {a : α} : (l.set i a)[j]? = l[j]? := by by_cases hj : j < (l.set i a).length @@ -686,11 +570,6 @@ theorem getElem_set {l : List α} {m n} {a} (h) : else simp [h] -@[deprecated getElem_set (since := "2024-06-12")] -theorem get_set {l : List α} {m n} {a : α} (h) : - (set l m a).get ⟨n, h⟩ = if m = n then a else l.get ⟨n, length_set .. ▸ h⟩ := by - simp [getElem_set] - theorem getElem?_set {l : List α} {i j : Nat} {a : α} : (l.set i a)[j]? = if i = j then if i < l.length then some a else none else l[j]? := by if h : i = j then @@ -724,8 +603,6 @@ theorem set_eq_of_length_le {l : List α} {n : Nat} (h : l.length ≤ n) {a : α @[simp] theorem set_eq_nil_iff {l : List α} (n : Nat) (a : α) : l.set n a = [] ↔ l = [] := by cases l <;> cases n <;> simp [set] -@[deprecated set_eq_nil_iff (since := "2024-09-05")] abbrev set_eq_nil := @set_eq_nil_iff - theorem set_comm (a b : α) : ∀ {n m : Nat} (l : List α), n ≠ m → (l.set n a).set m b = (l.set m b).set n a | _, _, [], _ => by simp @@ -3445,17 +3322,137 @@ theorem all_eq_not_any_not (l : List α) (p : α → Bool) : l.all p = !l.any (! (l.insert a).all f = (f a && l.all f) := by simp [all_eq] +/-! ### Legacy lemmas about `get`, `get?`, and `get!`. + +Hopefully these should not be needed, in favour of lemmas about `xs[i]`, `xs[i]?`, and `xs[i]!`, +to which these simplify. + +We may consider deprecating or downstreaming these lemmas. +-/ + +theorem get_cons_zero : get (a::l) (0 : Fin (l.length + 1)) = a := rfl + +theorem get_cons_succ {as : List α} {h : i + 1 < (a :: as).length} : + (a :: as).get ⟨i+1, h⟩ = as.get ⟨i, Nat.lt_of_succ_lt_succ h⟩ := rfl + +theorem get_cons_succ' {as : List α} {i : Fin as.length} : + (a :: as).get i.succ = as.get i := rfl + +theorem get_mk_zero : ∀ {l : List α} (h : 0 < l.length), l.get ⟨0, h⟩ = l.head (length_pos.mp h) + | _::_, _ => rfl + +theorem get?_zero (l : List α) : l.get? 0 = l.head? := by cases l <;> rfl + +/-- +If one has `l.get i` in an expression (with `i : Fin l.length`) and `h : l = l'`, +`rw [h]` will give a "motive is not type correct" error, as it cannot rewrite the +`i : Fin l.length` to `Fin l'.length` directly. The theorem `get_of_eq` can be used to make +such a rewrite, with `rw [get_of_eq h]`. +-/ +theorem get_of_eq {l l' : List α} (h : l = l') (i : Fin l.length) : + get l i = get l' ⟨i, h ▸ i.2⟩ := by cases h; rfl + +theorem get!_of_get? [Inhabited α] : ∀ {l : List α} {n}, get? l n = some a → get! l n = a + | _a::_, 0, rfl => rfl + | _::l, _+1, e => get!_of_get? (l := l) e + +theorem get!_len_le [Inhabited α] : ∀ {l : List α} {n}, length l ≤ n → l.get! n = (default : α) + | [], _, _ => rfl + | _ :: l, _+1, h => get!_len_le (l := l) <| Nat.le_of_succ_le_succ h + +theorem getElem!_nil [Inhabited α] {n : Nat} : ([] : List α)[n]! = default := rfl + +theorem getElem!_cons_zero [Inhabited α] {l : List α} : (a::l)[0]! = a := by + rw [getElem!_pos] <;> simp + +theorem getElem!_cons_succ [Inhabited α] {l : List α} : (a::l)[n+1]! = l[n]! := by + by_cases h : n < l.length + · rw [getElem!_pos, getElem!_pos] <;> simp_all [Nat.succ_lt_succ_iff] + · rw [getElem!_neg, getElem!_neg] <;> simp_all [Nat.succ_lt_succ_iff] + +theorem getElem!_of_getElem? [Inhabited α] : ∀ {l : List α} {n : Nat}, l[n]? = some a → l[n]! = a + | _a::_, 0, _ => by + rw [getElem!_pos] <;> simp_all + | _::l, _+1, e => by + simp at e + simp_all [getElem!_of_getElem? (l := l) e] + +theorem ext_get {l₁ l₂ : List α} (hl : length l₁ = length l₂) + (h : ∀ n h₁ h₂, get l₁ ⟨n, h₁⟩ = get l₂ ⟨n, h₂⟩) : l₁ = l₂ := + ext_getElem hl (by simp_all) + +theorem get_of_mem {a} {l : List α} (h : a ∈ l) : ∃ n, get l n = a := by + obtain ⟨n, h, e⟩ := getElem_of_mem h + exact ⟨⟨n, h⟩, e⟩ + +theorem get?_of_mem {a} {l : List α} (h : a ∈ l) : ∃ n, l.get? n = some a := + let ⟨⟨n, _⟩, e⟩ := get_of_mem h; ⟨n, e ▸ get?_eq_get _⟩ + +theorem get_mem : ∀ (l : List α) n, get l n ∈ l + | _ :: _, ⟨0, _⟩ => .head .. + | _ :: l, ⟨_+1, _⟩ => .tail _ (get_mem l ..) + +theorem mem_of_get? {l : List α} {n a} (e : l.get? n = some a) : a ∈ l := + let ⟨_, e⟩ := get?_eq_some_iff.1 e; e ▸ get_mem .. + +theorem mem_iff_get {a} {l : List α} : a ∈ l ↔ ∃ n, get l n = a := + ⟨get_of_mem, fun ⟨_, e⟩ => e ▸ get_mem ..⟩ + +theorem mem_iff_get? {a} {l : List α} : a ∈ l ↔ ∃ n, l.get? n = some a := by + simp [getElem?_eq_some_iff, Fin.exists_iff, mem_iff_get] + /-! ### Deprecations -/ +@[deprecated getD_eq_getElem?_getD (since := "2024-06-12")] +theorem getD_eq_get? : ∀ l n (a : α), getD l n a = (get? l n).getD a := by simp +@[deprecated getElem_singleton (since := "2024-06-12")] +theorem get_singleton (a : α) (n : Fin 1) : get [a] n = a := by simp +@[deprecated getElem?_concat_length (since := "2024-06-12")] +theorem get?_concat_length (l : List α) (a : α) : (l ++ [a]).get? l.length = some a := by simp +@[deprecated getElem_set_self (since := "2024-06-12")] +theorem get_set_eq {l : List α} {i : Nat} {a : α} (h : i < (l.set i a).length) : + (l.set i a).get ⟨i, h⟩ = a := by + simp +@[deprecated getElem_set_ne (since := "2024-06-12")] +theorem get_set_ne {l : List α} {i j : Nat} (h : i ≠ j) {a : α} + (hj : j < (l.set i a).length) : + (l.set i a).get ⟨j, hj⟩ = l.get ⟨j, by simp at hj; exact hj⟩ := by + simp [h] +@[deprecated getElem_set (since := "2024-06-12")] +theorem get_set {l : List α} {m n} {a : α} (h) : + (set l m a).get ⟨n, h⟩ = if m = n then a else l.get ⟨n, length_set .. ▸ h⟩ := by + simp [getElem_set] +@[deprecated cons_inj_right (since := "2024-06-15")] abbrev cons_inj := @cons_inj_right +@[deprecated ne_nil_of_length_eq_add_one (since := "2024-06-16")] +abbrev ne_nil_of_length_eq_succ := @ne_nil_of_length_eq_add_one + +@[deprecated "Deprecated without replacement." (since := "2024-07-09")] +theorem get_cons_cons_one : (a₁ :: a₂ :: as).get (1 : Fin (as.length + 2)) = a₂ := rfl + +@[deprecated filter_flatten (since := "2024-08-26")] +theorem join_map_filter (p : α → Bool) (l : List (List α)) : + (l.map (filter p)).flatten = (l.flatten).filter p := by + rw [filter_flatten] + +@[deprecated getElem_eq_getElem?_get (since := "2024-09-04")] abbrev getElem_eq_getElem? := + @getElem_eq_getElem?_get +@[deprecated flatten_eq_nil_iff (since := "2024-09-05")] abbrev join_eq_nil := @flatten_eq_nil_iff +@[deprecated flatten_ne_nil_iff (since := "2024-09-05")] abbrev join_ne_nil := @flatten_ne_nil_iff +@[deprecated flatten_eq_cons_iff (since := "2024-09-05")] abbrev join_eq_cons_iff := @flatten_eq_cons_iff +@[deprecated flatten_eq_cons_iff (since := "2024-09-05")] abbrev join_eq_cons := @flatten_eq_cons_iff +@[deprecated flatten_eq_append_iff (since := "2024-09-05")] abbrev join_eq_append := @flatten_eq_append_iff +@[deprecated mem_of_getElem? (since := "2024-09-06")] abbrev getElem?_mem := @mem_of_getElem? +@[deprecated mem_of_get? (since := "2024-09-06")] abbrev get?_mem := @mem_of_get? +@[deprecated getElem_set_self (since := "2024-09-04")] abbrev getElem_set_eq := @getElem_set_self +@[deprecated getElem?_set_self (since := "2024-09-04")] abbrev getElem?_set_eq := @getElem?_set_self +@[deprecated set_eq_nil_iff (since := "2024-09-05")] abbrev set_eq_nil := @set_eq_nil_iff @[deprecated flatten_nil (since := "2024-10-14")] abbrev join_nil := @flatten_nil @[deprecated flatten_cons (since := "2024-10-14")] abbrev join_cons := @flatten_cons @[deprecated length_flatten (since := "2024-10-14")] abbrev length_join := @length_flatten @[deprecated flatten_singleton (since := "2024-10-14")] abbrev join_singleton := @flatten_singleton @[deprecated mem_flatten (since := "2024-10-14")] abbrev mem_join := @mem_flatten -@[deprecated flatten_eq_nil_iff (since := "2024-09-05")] abbrev join_eq_nil := @flatten_eq_nil_iff @[deprecated flatten_eq_nil_iff (since := "2024-10-14")] abbrev join_eq_nil_iff := @flatten_eq_nil_iff -@[deprecated flatten_ne_nil_iff (since := "2024-09-05")] abbrev join_ne_nil := @flatten_ne_nil_iff @[deprecated flatten_ne_nil_iff (since := "2024-10-14")] abbrev join_ne_nil_iff := @flatten_ne_nil_iff @[deprecated exists_of_mem_flatten (since := "2024-10-14")] abbrev exists_of_mem_join := @exists_of_mem_flatten @[deprecated mem_flatten_of_mem (since := "2024-10-14")] abbrev mem_join_of_mem := @mem_flatten_of_mem @@ -3469,16 +3466,9 @@ theorem all_eq_not_any_not (l : List α) (p : α → Bool) : l.all p = !l.any (! @[deprecated filter_flatten (since := "2024-10-14")] abbrev filter_join := @filter_flatten @[deprecated flatten_filter_not_isEmpty (since := "2024-10-14")] abbrev join_filter_not_isEmpty := @flatten_filter_not_isEmpty @[deprecated flatten_filter_ne_nil (since := "2024-10-14")] abbrev join_filter_ne_nil := @flatten_filter_ne_nil -@[deprecated filter_flatten (since := "2024-08-26")] -theorem join_map_filter (p : α → Bool) (l : List (List α)) : - (l.map (filter p)).flatten = (l.flatten).filter p := by - rw [filter_flatten] @[deprecated flatten_append (since := "2024-10-14")] abbrev join_append := @flatten_append @[deprecated flatten_concat (since := "2024-10-14")] abbrev join_concat := @flatten_concat @[deprecated flatten_flatten (since := "2024-10-14")] abbrev join_join := @flatten_flatten -@[deprecated flatten_eq_cons_iff (since := "2024-09-05")] abbrev join_eq_cons_iff := @flatten_eq_cons_iff -@[deprecated flatten_eq_cons_iff (since := "2024-09-05")] abbrev join_eq_cons := @flatten_eq_cons_iff -@[deprecated flatten_eq_append_iff (since := "2024-09-05")] abbrev join_eq_append := @flatten_eq_append_iff @[deprecated flatten_eq_append_iff (since := "2024-10-14")] abbrev join_eq_append_iff := @flatten_eq_append_iff @[deprecated eq_iff_flatten_eq (since := "2024-10-14")] abbrev eq_iff_join_eq := @eq_iff_flatten_eq @[deprecated flatten_replicate_nil (since := "2024-10-14")] abbrev join_replicate_nil := @flatten_replicate_nil @@ -3513,4 +3503,18 @@ theorem join_map_filter (p : α → Bool) (l : List (List α)) : @[deprecated any_flatMap (since := "2024-10-16")] abbrev any_bind := @any_flatMap @[deprecated all_flatMap (since := "2024-10-16")] abbrev all_bind := @all_flatMap +@[deprecated get?_eq_none (since := "2024-11-29")] abbrev get?_len_le := @get?_eq_none +@[deprecated getElem?_eq_some_iff (since := "2024-11-29")] +abbrev getElem?_eq_some := @getElem?_eq_some_iff +@[deprecated get?_eq_some_iff (since := "2024-11-29")] +abbrev get?_eq_some := @get?_eq_some_iff +@[deprecated LawfulGetElem.getElem?_def (since := "2024-11-29")] +theorem getElem?_eq (l : List α) (i : Nat) : + l[i]? = if h : i < l.length then some l[i] else none := + getElem?_def _ _ +@[deprecated getElem?_eq_none (since := "2024-11-29")] abbrev getElem?_len_le := @getElem?_eq_none + + + + end List diff --git a/src/Init/Data/List/MapIdx.lean b/src/Init/Data/List/MapIdx.lean index c00d8e8d74..d259236174 100644 --- a/src/Init/Data/List/MapIdx.lean +++ b/src/Init/Data/List/MapIdx.lean @@ -87,8 +87,8 @@ theorem mapFinIdx_eq_ofFn {as : List α} {f : Fin as.length → α → β} : apply ext_getElem <;> simp @[simp] theorem getElem?_mapFinIdx {l : List α} {f : Fin l.length → α → β} {i : Nat} : - (l.mapFinIdx f)[i]? = l[i]?.pbind fun x m => f ⟨i, by simp [getElem?_eq_some] at m; exact m.1⟩ x := by - simp only [getElem?_eq, length_mapFinIdx, getElem_mapFinIdx] + (l.mapFinIdx f)[i]? = l[i]?.pbind fun x m => f ⟨i, by simp [getElem?_eq_some_iff] at m; exact m.1⟩ x := by + simp only [getElem?_def, length_mapFinIdx, getElem_mapFinIdx] split <;> simp @[simp] @@ -126,7 +126,8 @@ theorem mapFinIdx_singleton {a : α} {f : Fin 1 → α → β} : theorem mapFinIdx_eq_enum_map {l : List α} {f : Fin l.length → α → β} : l.mapFinIdx f = l.enum.attach.map - fun ⟨⟨i, x⟩, m⟩ => f ⟨i, by rw [mk_mem_enum_iff_getElem?, getElem?_eq_some] at m; exact m.1⟩ x := by + fun ⟨⟨i, x⟩, m⟩ => + f ⟨i, by rw [mk_mem_enum_iff_getElem?, getElem?_eq_some_iff] at m; exact m.1⟩ x := by apply ext_getElem <;> simp @[simp] @@ -235,7 +236,7 @@ theorem getElem?_mapIdx_go : ∀ {l : List α} {arr : Array β} {i : Nat}, (mapIdx.go f l arr)[i]? = if h : i < arr.size then some arr[i] else Option.map (f i) l[i - arr.size]? | [], arr, i => by - simp only [mapIdx.go, Array.toListImpl_eq, getElem?_eq, Array.length_toList, + simp only [mapIdx.go, Array.toListImpl_eq, getElem?_def, Array.length_toList, Array.getElem_eq_getElem_toList, length_nil, Nat.not_lt_zero, ↓reduceDIte, Option.map_none'] | a :: l, arr, i => by rw [mapIdx.go, getElem?_mapIdx_go] diff --git a/src/Init/Data/List/TakeDrop.lean b/src/Init/Data/List/TakeDrop.lean index e6e5f33063..cedd835b3a 100644 --- a/src/Init/Data/List/TakeDrop.lean +++ b/src/Init/Data/List/TakeDrop.lean @@ -192,6 +192,24 @@ theorem take_concat_get (l : List α) (i : Nat) (h : i < l.length) : Eq.symm <| (append_left_inj _).1 <| (take_append_drop (i+1) l).trans <| by rw [concat_eq_append, append_assoc, singleton_append, getElem_cons_drop_succ_eq_drop, take_append_drop] +@[simp] theorem take_append_getElem (l : List α) (i : Nat) (h : i < l.length) : + (l.take i) ++ [l[i]] = l.take (i+1) := by + simpa using take_concat_get l i h + +@[simp] theorem take_append_getLast (l : List α) (h : l ≠ []) : + (l.take (l.length - 1)) ++ [l.getLast h] = l := by + rw [getLast_eq_getElem] + cases l + · contradiction + · simp + +@[simp] theorem take_append_getLast? (l : List α) : + (l.take (l.length - 1)) ++ l.getLast?.toList = l := by + match l with + | [] => simp + | x :: xs => + simpa using take_append_getLast (x :: xs) (by simp) + @[deprecated take_succ_cons (since := "2024-07-25")] theorem take_cons_succ : (a::as).take (i+1) = a :: as.take i := rfl diff --git a/src/Init/GetElem.lean b/src/Init/GetElem.lean index 3a4b1adfcc..d4a26f57ab 100644 --- a/src/Init/GetElem.lean +++ b/src/Init/GetElem.lean @@ -172,6 +172,16 @@ theorem getElem!_neg [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem d simp only [getElem?_def] at h ⊢ split <;> simp_all +@[simp] theorem isNone_getElem? [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom] + (c : cont) (i : idx) [Decidable (dom c i)] : c[i]?.isNone = ¬dom c i := by + simp only [getElem?_def] + split <;> simp_all + +@[simp] theorem isSome_getElem? [GetElem? cont idx elem dom] [LawfulGetElem cont idx elem dom] + (c : cont) (i : idx) [Decidable (dom c i)] : c[i]?.isSome = dom c i := by + simp only [getElem?_def] + split <;> simp_all + namespace Fin instance instGetElemFinVal [GetElem cont Nat elem dom] : GetElem cont (Fin n) elem fun xs i => dom xs i where diff --git a/src/Init/Omega/IntList.lean b/src/Init/Omega/IntList.lean index 31cbff7d9f..8726d35632 100644 --- a/src/Init/Omega/IntList.lean +++ b/src/Init/Omega/IntList.lean @@ -32,13 +32,9 @@ theorem get_map {xs : IntList} (h : f 0 = 0) : get (xs.map f) i = f (xs.get i) : cases xs[i]? <;> simp_all theorem get_of_length_le {xs : IntList} (h : xs.length ≤ i) : xs.get i = 0 := by - rw [get, List.get?_eq_none.mpr h] + rw [get, List.get?_eq_none_iff.mpr h] rfl --- theorem lt_length_of_get_nonzero {xs : IntList} (h : xs.get i ≠ 0) : i < xs.length := by --- revert h --- simpa using mt get_of_length_le - /-- Like `List.set`, but right-pad with zeroes as necessary first. -/ def set (xs : IntList) (i : Nat) (y : Int) : IntList := match xs, i with