From 98a34f9e4078be501e0c17a5607f9881bf756ea3 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Fri, 7 Jun 2024 20:31:57 +1000 Subject: [PATCH 01/20] initial work on switching the normal to L[n] and L[n]? --- src/Init/Data/Array/Lemmas.lean | 2 +- src/Init/Data/List/BasicAux.lean | 4 +- src/Init/Data/List/Lemmas.lean | 311 +++++++++++++++++++++++-------- 3 files changed, 238 insertions(+), 79 deletions(-) diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean index 9743ea8cf7a0..906661d64223 100644 --- a/src/Init/Data/Array/Lemmas.lean +++ b/src/Init/Data/Array/Lemmas.lean @@ -533,7 +533,7 @@ theorem size_eq_length_data (as : Array α) : as.size = as.data.length := rfl split · match a with | ⟨[]⟩ | ⟨[_]⟩ => rfl · have := Nat.sub_add_cancel (Nat.le_of_not_le ‹_›) - refine List.ext <| go _ _ _ _ (by simp [this]) rfl fun k => ?_ + refine List.ext_get? <| go _ _ _ _ (by simp [this]) rfl fun k => ?_ split · rfl · rename_i h diff --git a/src/Init/Data/List/BasicAux.lean b/src/Init/Data/List/BasicAux.lean index a44764a39b4c..33f331e81791 100644 --- a/src/Init/Data/List/BasicAux.lean +++ b/src/Init/Data/List/BasicAux.lean @@ -44,13 +44,13 @@ See also `get?` and `get!`. def getD (as : List α) (i : Nat) (fallback : α) : α := (as.get? i).getD fallback -@[ext] theorem ext : ∀ {l₁ l₂ : List α}, (∀ n, l₁.get? n = l₂.get? n) → l₁ = l₂ +theorem ext_get? : ∀ {l₁ l₂ : List α}, (∀ n, l₁.get? n = l₂.get? n) → l₁ = l₂ | [], [], _ => rfl | a :: l₁, [], h => nomatch h 0 | [], a' :: l₂, h => nomatch h 0 | a :: l₁, a' :: l₂, h => by have h0 : some a = some a' := h 0 - injection h0 with aa; simp only [aa, ext fun n => h (n+1)] + injection h0 with aa; simp only [aa, ext_get? fun n => h (n+1)] /-- Returns the first element in the list. diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index 94bc391e93ba..5cc47a6e51fb 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/src/Init/Data/List/Lemmas.lean @@ -41,6 +41,64 @@ attribute [simp] concat_eq_append append_assoc @[simp] theorem and_nil : [].and = true := rfl @[simp] theorem and_cons : (a::l).and = (a && l.and) := rfl +theorem get?_len_le : ∀ {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 + +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 := + ⟨fun e => + have : n < length l := Nat.gt_of_not_le fun hn => by cases get?_len_le hn ▸ e + ⟨this, by rwa [get?_eq_get this, Option.some.injEq] at e⟩, + fun ⟨h, 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⟩ + +@[simp] theorem get?_eq_getElem? (l : List α) (i : Nat) : l.get? i = l[i]? := by + simp only [getElem?]; 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 + +@[simp] theorem getElem?_nil {n : Nat} : ([] : List α)[n]? = none := rfl + +@[simp] theorem getElem?_cons_zero {l : List α} : (a::l)[0]? = some a := by + simp only [← get?_eq_getElem?] + rfl + +@[simp] theorem getElem?_cons_succ {l : List α} : (a::l)[n+1]? = l[n]? := by + simp only [← get?_eq_getElem?] + rfl + +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] + +theorem getElem?_eq_getElem {l : List α} {n} (h : n < l.length) : l[n]? = some l[n] := by + simp only [← get?_eq_getElem?, get?_eq_get, h, get_eq_getElem] + +theorem getElem?_eq_some {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] theorem getElem?_eq_none : l[n]? = none ↔ length l ≤ n := by + simp only [← get?_eq_getElem?, get?_eq_none] + +@[simp] theorem getElem!_nil [Inhabited α] {n : Nat} : ([] : List α)[n]! = default := rfl + +@[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] + /-! ### length -/ theorem eq_nil_of_length_eq_zero (_ : length l = 0) : l = [] := match l with | [] => rfl @@ -100,10 +158,14 @@ theorem append_left_inj {s₁ s₂ : List α} (t) : s₁ ++ t = s₂ ++ t ↔ s @[simp] theorem append_eq_nil : p ++ q = [] ↔ p = [] ∧ q = [] := by cases p <;> simp -theorem get_append : ∀ {l₁ l₂ : List α} (n : Nat) (h : n < l₁.length), - (l₁ ++ l₂).get ⟨n, length_append .. ▸ Nat.lt_add_right _ h⟩ = l₁.get ⟨n, h⟩ +theorem getElem_append : ∀ {l₁ l₂ : List α} (n : Nat) (h : n < l₁.length), + (l₁ ++ l₂)[n]'(length_append .. ▸ Nat.lt_add_right _ h) = l₁[n] | a :: l, _, 0, h => rfl -| a :: l, _, n+1, h => by simp only [get, cons_append]; apply get_append +| a :: l, _, n+1, h => by simp only [get, cons_append]; apply getElem_append + +theorem get_append {l₁ l₂ : List α} (n : Nat) (h : n < l₁.length) : + (l₁ ++ l₂).get ⟨n, length_append .. ▸ Nat.lt_add_right _ h⟩ = l₁.get ⟨n, h⟩ := by + simp [getElem_append, h] /-! ### map -/ @@ -171,48 +233,53 @@ theorem reverse_map (f : α → β) (l : List α) : (l.map f).reverse = l.revers /-! ### nth element -/ -theorem get_of_mem : ∀ {a} {l : List α}, a ∈ l → ∃ n, get l n = a - | _, _ :: _, .head .. => ⟨⟨0, Nat.succ_pos _⟩, rfl⟩ - | _, _ :: _, .tail _ m => let ⟨⟨n, h⟩, e⟩ := get_of_mem m; ⟨⟨n+1, Nat.succ_lt_succ h⟩, e⟩ +theorem getElem_of_mem : ∀ {a} {l : List α}, a ∈ l → ∃ (n : Nat) (h : n < l.length), l[n]'h = a + | _, _ :: _, .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_mem : ∀ (l : List α) n (h : n < l.length), l[n]'h ∈ l + | _ :: _, 0, _ => .head .. + | _ :: l, _+1, _ => .tail _ (getElem_mem l ..) theorem get_mem : ∀ (l : List α) n h, get l ⟨n, h⟩ ∈ l | _ :: _, 0, _ => .head .. | _ :: l, _+1, _ => .tail _ (get_mem l ..) +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 get?_len_le : ∀ {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 - -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 := - ⟨fun e => - have : n < length l := Nat.gt_of_not_le fun hn => by cases get?_len_le hn ▸ e - ⟨this, by rwa [get?_eq_get this, Option.some.injEq] at e⟩, - fun ⟨h, e⟩ => e ▸ get?_eq_get _⟩ - -@[simp] 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⟩ +@[simp] theorem getElem?_map (f : α → β) : ∀ (l : List α) (n : Nat), (map f l)[n]? = Option.map f l[n]? + | [], _ => rfl + | _ :: _, 0 => by simp + | _ :: l, n+1 => by simp [getElem?_map f l n] -@[simp] theorem get?_map (f : α → β) : ∀ l n, (map f l).get? n = (l.get? n).map f +theorem get?_map (f : α → β) : ∀ l n, (map f l).get? n = (l.get? n).map f | [], _ => rfl | _ :: _, 0 => rfl | _ :: l, n+1 => get?_map f l n -theorem get?_append {l₁ l₂ : List α} {n : Nat} (hn : n < l₁.length) : - (l₁ ++ l₂).get? n = l₁.get? n := by +theorem getElem?_append {l₁ l₂ : List α} {n : Nat} (hn : n < l₁.length) : + (l₁ ++ l₂)[n]? = l₁[n]? := by have hn' : n < (l₁ ++ l₂).length := Nat.lt_of_lt_of_le hn <| length_append .. ▸ Nat.le_add_right .. - rw [get?_eq_get hn, get?_eq_get hn', get_append] + simp_all [getElem?_eq_getElem, getElem_append] -@[simp] theorem get?_concat_length : ∀ (l : List α) (a : α), (l ++ [a]).get? l.length = some a +theorem get?_append {l₁ l₂ : List α} {n : Nat} (hn : n < l₁.length) : + (l₁ ++ l₂).get? n = l₁.get? n := by + simp [getElem?_append hn] + +@[simp] theorem getElem?_concat_length : ∀ (l : List α) (a : α), (l ++ [a])[l.length]? = some a | [], a => rfl - | b :: l, a => by rw [cons_append, length_cons]; simp only [get?, get?_concat_length] + | b :: l, a => by rw [cons_append, length_cons]; simp [getElem?_concat_length] + +theorem get?_concat_length (l : List α) (a : α) : (l ++ [a]).get? l.length = some a := by simp theorem getLast_eq_get : ∀ (l : List α) (h : l ≠ []), getLast l h = l.get ⟨l.length - 1, by @@ -236,51 +303,71 @@ theorem getLast?_eq_get? : ∀ (l : List α), getLast? l = l.get? (l.length - 1) @[simp] theorem getLast?_concat (l : List α) : getLast? (l ++ [a]) = some a := by simp [getLast?_eq_get?, Nat.succ_sub_succ] -theorem getD_eq_get? : ∀ l n (a : α), getD l n a = (get? l n).getD a - | [], _, _ => rfl - | _a::_, 0, _ => rfl - | _::l, _+1, _ => getD_eq_get? (l := l) .. +@[simp] theorem getD_eq_getElem? (l) (n) (a : α) : getD l n a = (l[n]?).getD a := by + simp [getD] -theorem get?_append_right : ∀ {l₁ l₂ : List α} {n : Nat}, l₁.length ≤ n → - (l₁ ++ l₂).get? n = l₂.get? (n - l₁.length) +theorem getElem?_append_right : ∀ {l₁ l₂ : List α} {n : Nat}, l₁.length ≤ n → + (l₁ ++ l₂)[n]? = l₂[n - l₁.length]? | [], _, n, _ => rfl | a :: l, _, n+1, h₁ => by rw [cons_append] - simp [Nat.succ_sub_succ_eq_sub, get?_append_right (Nat.lt_succ.1 h₁)] + simp [Nat.succ_sub_succ_eq_sub, getElem?_append_right (Nat.lt_succ.1 h₁)] + +theorem get?_append_right {l₁ l₂ : List α} {n : Nat} (h : l₁.length ≤ n) : + (l₁ ++ l₂).get? n = l₂.get? (n - l₁.length) := by + simp [getElem?_append_right, h] -theorem get?_reverse' : ∀ {l : List α} (i j), i + j + 1 = length l → - get? l.reverse i = get? l j +theorem getElem?_reverse' : ∀ {l : List α} {i j}, i + j + 1 = length l → + l.reverse[i]? = l[j]? | [], _, _, _ => rfl - | a::l, i, 0, h => by simp [Nat.succ.injEq] at h; simp [h, get?_append_right, Nat.succ.injEq] + | a::l, i, 0, h => by simp [Nat.succ.injEq] at h; simp [h, getElem?_append_right, Nat.succ.injEq] | a::l, i, j+1, h => by have := Nat.succ.inj h; simp at this ⊢ - rw [get?_append, get?_reverse' _ j this] + rw [getElem?_append, getElem?_reverse' this] rw [length_reverse, ← this]; apply Nat.lt_add_of_pos_right (Nat.succ_pos _) -theorem get?_reverse {l : List α} (i) (h : i < length l) : - get? l.reverse i = get? l (l.length - 1 - i) := - get?_reverse' _ _ <| by +theorem get?_reverse' {l : List α} {i j} (h : i + j + 1 = length l) : get? l.reverse i = get? l j := by + simp [getElem?_reverse' h] + +theorem getElem?_reverse {l : List α} {i} (h : i < length l) : + l.reverse[i]? = l[l.length - 1 - i]? := + getElem?_reverse' <| by rw [Nat.add_sub_of_le (Nat.le_sub_one_of_lt h), Nat.sub_add_cancel (Nat.lt_of_le_of_lt (Nat.zero_le _) h)] +theorem get?_reverse {l : List α} {i} (h : i < length l) : + get? l.reverse i = get? l (l.length - 1 - i) := by + simp [getElem?_reverse h] + @[simp] theorem getD_nil : getD [] n d = d := rfl @[simp] theorem getD_cons_zero : getD (x :: xs) 0 d = x := rfl @[simp] theorem getD_cons_succ : getD (x :: xs) (n + 1) d = getD xs n d := rfl -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 fun n => +@[ext] theorem ext_getElem? {l₁ l₂ : List α} (h : ∀ n : Nat, l₁[n]? = l₂[n]?) : l₁ = l₂ := + ext_get? fun n => by simp_all + +theorem ext_getElem {l₁ l₂ : List α} (hl : length l₁ = length l₂) + (h : ∀ (n : Nat) (h₁ : n < l₁.length) (h₂ : n < l₂.length), l₁[n]'h₁ = l₂[n]'h₂) : l₁ = l₂ := + ext_getElem? fun n => if h₁ : n < length l₁ then by - rw [get?_eq_get, get?_eq_get, h n h₁ (by rwa [← hl])] + simp_all [getElem?_eq_getElem] else by have h₁ := Nat.le_of_not_lt h₁ - rw [get?_len_le h₁, get?_len_le]; rwa [← hl] + rw [getElem?_len_le h₁, getElem?_len_le]; rwa [← hl] -@[simp] theorem get_map (f : α → β) {l n} : - get (map f l) n = f (get l ⟨n, length_map l f ▸ n.2⟩) := - Option.some.inj <| by rw [← get?_eq_get, get?_map, get?_eq_get]; rfl +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) + +@[simp] theorem getElem_map (f : α → β) {l n} {h : n < (map f l).length} : + (map f l)[n] = f (get l ⟨n, length_map l f ▸ h⟩) := + Option.some.inj <| by rw [← getElem?_eq_getElem, getElem?_map, getElem?_eq_getElem]; rfl + +theorem get_map (f : α → β) {l n} : + get (map f l) n = f (get l ⟨n, length_map l f ▸ n.2⟩) := by + simp /-! ### take and drop -/ @@ -436,7 +523,7 @@ theorem mapM'_eq_mapM [Monad m] [LawfulMonad m] (f : α → m β) (l : List α) /-! ### forM -/ -- We use `List.forM` as the simp normal form, rather that `ForM.forM`. --- As such we need to replace `List.forM_nil` and `List.forM_cons` from Lean: +-- As such we need to replace `List.forM_nil` and `List.forM_cons`: @[simp] theorem forM_nil' [Monad m] : ([] : List α).forM f = (pure .unit : m PUnit) := rfl @@ -484,6 +571,7 @@ theorem filter_eq_nil {l} : filter p l = [] ↔ ∀ a, a ∈ l → ¬p a := by /-! ### findSome? -/ @[simp] theorem findSome?_nil : ([] : List α).findSome? f = none := rfl + theorem findSome?_cons {f : α → Option β} : (a::as).findSome? f = match f a with | some b => some b | none => as.findSome? f := rfl @@ -491,27 +579,33 @@ theorem findSome?_cons {f : α → Option β} : /-! ### replace -/ @[simp] theorem replace_nil [BEq α] : ([] : List α).replace a b = [] := rfl + theorem replace_cons [BEq α] {a : α} : (a::as).replace b c = match a == b with | true => c::as | false => a :: replace as b c := rfl + @[simp] theorem replace_cons_self [BEq α] [LawfulBEq α] {a : α} : (a::as).replace a b = b::as := by simp [replace_cons] /-! ### elem -/ @[simp] theorem elem_nil [BEq α] : ([] : List α).elem a = false := rfl + theorem elem_cons [BEq α] {a : α} : (a::as).elem b = match b == a with | true => true | false => as.elem b := rfl + @[simp] theorem elem_cons_self [BEq α] [LawfulBEq α] {a : α} : (a::as).elem a = true := by simp [elem_cons] /-! ### lookup -/ @[simp] theorem lookup_nil [BEq α] : ([] : List (α × β)).lookup a = none := rfl + theorem lookup_cons [BEq α] {k : α} : ((k,b)::es).lookup a = match a == k with | true => some b | false => es.lookup a := rfl + @[simp] theorem lookup_cons_self [BEq α] [LawfulBEq α] {k : α} : ((k,b)::es).lookup k = some b := by simp [lookup_cons] @@ -527,8 +621,8 @@ theorem lookup_cons [BEq α] {k : α} : zipWith f (a :: as) (b :: bs) = f a b :: zipWith f as bs := by rfl -theorem zipWith_get? {f : α → β → γ} : - (List.zipWith f as bs).get? i = match as.get? i, bs.get? i with +theorem getElem?_zipWith {f : α → β → γ} {i : Nat} : + (List.zipWith f as bs)[i]? = match as[i]?, bs[i]? with | some a, some b => some (f a b) | _, _ => none := by induction as generalizing bs i with | nil => cases bs with @@ -538,10 +632,17 @@ theorem zipWith_get? {f : α → β → γ} : | nil => simp | cons b bs => cases i <;> simp_all +theorem get?_zipWith {f : α → β → γ} : + (List.zipWith f as bs).get? i = match as.get? i, bs.get? i with + | some a, some b => some (f a b) | _, _ => none := by + simp [getElem?_zipWith] + +@[deprecated (since := "2024-06-07")] abbrev zipWith_get? := @get?_zipWith + /-! ### zipWithAll -/ -theorem zipWithAll_get? {f : Option α → Option β → γ} : - (zipWithAll f as bs).get? i = match as.get? i, bs.get? i with +theorem getElem?_zipWithAll {f : Option α → Option β → γ} {i : Nat } : + (zipWithAll f as bs)[i]? = match as[i]?, bs[i]? with | none, none => .none | a?, b? => some (f a? b?) := by induction as generalizing bs i with | nil => induction bs generalizing i with @@ -553,6 +654,13 @@ theorem zipWithAll_get? {f : Option α → Option β → γ} : cases i <;> simp_all | cons b bs => cases i <;> simp_all +theorem get?_zipWithAll {f : Option α → Option β → γ} : + (zipWithAll f as bs).get? i = match as.get? i, bs.get? i with + | none, none => .none | a?, b? => some (f a? b?) := by + simp [getElem?_zipWithAll] + +@[deprecated (since := "2024-06-07")] abbrev zipWithAll_get? := @get?_zipWithAll + /-! ### zip -/ @[simp] theorem zip_nil_left : zip ([] : List α) (l : List β) = [] := by @@ -567,6 +675,7 @@ theorem zipWithAll_get? {f : Option α → Option β → γ} : /-! ### unzip -/ @[simp] theorem unzip_nil : ([] : List (α × β)).unzip = ([], []) := rfl + @[simp] theorem unzip_cons {h : α × β} : (h :: t).unzip = match unzip t with | (al, bl) => (h.1::al, h.2::bl) := rfl @@ -703,8 +812,8 @@ theorem minimum?_eq_some_iff [Min α] [LE α] [anti : Antisymm ((· : α) ≤ · @[simp] theorem set_succ (x : α) (xs : List α) (n : Nat) (a : α) : (x :: xs).set n.succ a = x :: xs.set n a := rfl -@[simp] theorem get_set_eq (l : List α) (i : Nat) (a : α) (h : i < (l.set i a).length) : - (l.set i a).get ⟨i, h⟩ = a := +@[simp] theorem getElem_set_eq (l : List α) (i : Nat) (a : α) (h : i < (l.set i a).length) : + (l.set i a)[i] = a := match l, i with | [], _ => by simp at h @@ -712,11 +821,15 @@ theorem minimum?_eq_some_iff [Min α] [LE α] [anti : Antisymm ((· : α) ≤ · | _ :: _, 0 => by simp | _ :: l, i + 1 => by - simp [get_set_eq l] + simp [getElem_set_eq l] + +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 get_set_ne (l : List α) {i j : Nat} (h : i ≠ j) (a : α) +@[simp] theorem getElem_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⟩ := + (l.set i a)[j] = l[j]'(by simp at hj; exact hj) := match l, i, j with | [], _, _ => by simp @@ -728,8 +841,12 @@ theorem minimum?_eq_some_iff [Min α] [LE α] [anti : Antisymm ((· : α) ≤ · simp | _ :: l, i + 1, j + 1 => by have g : i ≠ j := h ∘ congrArg (· + 1) - simp [get_set_ne l g] + simp [getElem_set_ne l g] +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] open Nat @@ -1245,31 +1362,46 @@ theorem Fin.exists_iff (p : Fin n → Prop) : (∃ i, p i) ↔ ∃ i h, p ⟨i, ⟨fun ⟨i, h⟩ => ⟨i.1, i.2, h⟩, fun ⟨i, hi, h⟩ => ⟨⟨i, hi⟩, h⟩⟩ theorem mem_iff_get? {a} {l : List α} : a ∈ l ↔ ∃ n, l.get? n = some a := by - simp [get?_eq_some, Fin.exists_iff, mem_iff_get] + simp [get?_eq_some, getElem?_eq_some, Fin.exists_iff, mem_iff_get] theorem get?_zero (l : List α) : l.get? 0 = l.head? := by cases l <;> rfl -@[simp] theorem getElem_eq_get (l : List α) (i : Nat) (h) : l[i]'h = l.get ⟨i, h⟩ := rfl - -@[simp] theorem getElem?_eq_get? (l : List α) (i : Nat) : l[i]? = l.get? i := by - simp only [getElem?]; split - · exact (get?_eq_get ‹_›).symm - · exact (get?_eq_none.2 <| Nat.not_lt.1 ‹_›).symm +/-- +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 +implicit `i < l.length` to `i < l'.length` directly. The theorem `getElem_of_eq` can be used to make +such a rewrite, with `rw [getElem_of_eq h]`. +-/ +theorem getElem_of_eq {l l' : List α} (h : l = l') {i : Nat} (w : i < l.length) : + l[i] = l'[i]'(h ▸ w) := by cases h; rfl /-- -If one has `get l i hi` in a formula and `h : l = l'`, one can not `rw h` in the formula as -`hi` gives `i < l.length` and not `i < l'.length`. The theorem `get_of_eq` can be used to make +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 -@[simp] theorem get_singleton (a : α) : (n : Fin 1) → get [a] n = a - | ⟨0, _⟩ => rfl +@[simp] theorem getElem_singleton (a : α) (h : i < 1) : [a][i] = a := + match i, h with + | 0, _ => rfl + +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 get_mk_zero : ∀ {l : List α} (h : 0 < l.length), l.get ⟨0, h⟩ = l.head (length_pos.mp h) | _::_, _ => rfl +theorem getElem_append_right' {l₁ l₂ : List α} {n : Nat} (h₁ : l₁.length ≤ n) (h₂) : + (l₁ ++ l₂)[n]'h₂ = + l₂[n - l₁.length]'(by rw [length_append] at h₂; exact Nat.sub_lt_left_of_lt_add h₁ h₂) := + Option.some.inj <| by rw [← getElem?_eq_getElem, ← getElem?_eq_getElem, getElem?_append_right h₁] + theorem get_append_right_aux {l₁ l₂ : List α} {n : Nat} (h₁ : l₁.length ≤ n) (h₂ : n < (l₁ ++ l₂).length) : n - l₁.length < l₂.length := by rw [length_append] at h₂ @@ -1277,7 +1409,12 @@ theorem get_append_right_aux {l₁ l₂ : List α} {n : Nat} theorem get_append_right' {l₁ l₂ : List α} {n : Nat} (h₁ : l₁.length ≤ n) (h₂) : (l₁ ++ l₂).get ⟨n, h₂⟩ = l₂.get ⟨n - l₁.length, get_append_right_aux h₁ h₂⟩ := -Option.some.inj <| by rw [← get?_eq_get, ← get?_eq_get, get?_append_right h₁] + Option.some.inj <| by rw [← get?_eq_get, ← get?_eq_get, get?_append_right h₁] + +theorem getElem_of_append {l : List α} (eq : l = l₁ ++ a :: l₂) (h : l₁.length = n) : + l[n]'(eq ▸ h ▸ by simp_arith) = a := Option.some.inj <| by + rw [← getElem?_eq_getElem, eq, getElem?_append_right (h ▸ Nat.le_refl _), h] + simp theorem get_of_append_proof {l : List α} (eq : l = l₁ ++ a :: l₂) (h : l₁.length = n) : n < length l := eq ▸ h ▸ by simp_arith @@ -1286,15 +1423,30 @@ theorem get_of_append {l : List α} (eq : l = l₁ ++ a :: l₂) (h : l₁.lengt l.get ⟨n, get_of_append_proof eq h⟩ = a := Option.some.inj <| by rw [← get?_eq_get, eq, get?_append_right (h ▸ Nat.le_refl _), h, Nat.sub_self]; rfl -@[simp] theorem get_replicate (a : α) {n : Nat} (m : Fin _) : (replicate n a).get m = a := +@[simp] theorem getElem_replicate (a : α) {n : Nat} {m} (h : m < (replicate n a).length) : + (replicate n a)[m] = a := eq_of_mem_replicate (get_mem _ _ _) +theorem get_replicate (a : α) {n : Nat} (m : Fin _) : (replicate n a).get m = a := by + simp + @[simp] theorem getLastD_concat (a b l) : @getLastD α (l ++ [b]) a = b := by rw [getLastD_eq_getLast?, getLast?_concat]; rfl +theorem getElem_cons_length (x : α) (xs : List α) (n : Nat) (h : n = xs.length) : + (x :: xs)[n]'(by simp [h]) = (x :: xs).getLast (cons_ne_nil x xs) := by + rw [getLast_eq_get]; cases h; rfl + theorem get_cons_length (x : α) (xs : List α) (n : Nat) (h : n = xs.length) : (x :: xs).get ⟨n, by simp [h]⟩ = (x :: xs).getLast (cons_ne_nil x xs) := by - rw [getLast_eq_get]; cases h; rfl + simp [getElem_cons_length, h] + +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 get!_of_get? [Inhabited α] : ∀ {l : List α} {n}, get? l n = some a → get! l n = a | _a::_, 0, rfl => rfl @@ -1324,9 +1476,16 @@ theorem set_set (a b : α) : ∀ (l : List α) (n : Nat), (l.set n a).set n b = | _ :: _, 0 => by simp [set] | _ :: _, _+1 => by simp [set, set_set] +theorem getElem_set (a : α) {m n} (l : List α) (h) : + (set l m a)[n]'h = if m = n then a else l[n]'(length_set .. ▸ h) := by + if h : m = n then + subst m; simp only [getElem_set_eq, ↓reduceIte] + else + simp [h] + theorem get_set (a : α) {m n} (l : List α) (h) : (set l m a).get ⟨n, h⟩ = if m = n then a else l.get ⟨n, length_set .. ▸ h⟩ := by - if h : m = n then subst m; simp else simp [h] + simp [getElem_set] theorem mem_or_eq_of_mem_set : ∀ {l : List α} {n : Nat} {a b : α}, a ∈ l.set n b → a ∈ l ∨ a = b | _ :: _, 0, _, _, h => ((mem_cons ..).1 h).symm.imp_left (.tail _) From 157b8e0cefbed2df35d20e97da26a7062ea5c285 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sat, 8 Jun 2024 05:12:41 +1000 Subject: [PATCH 02/20] fix Array.reverse_data --- src/Init/Data/Array/Lemmas.lean | 4 ++-- src/Init/Data/List/BasicAux.lean | 2 ++ src/Init/Data/List/Lemmas.lean | 10 +++++----- 3 files changed, 9 insertions(+), 7 deletions(-) diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean index 906661d64223..ab9842240256 100644 --- a/src/Init/Data/Array/Lemmas.lean +++ b/src/Init/Data/Array/Lemmas.lean @@ -517,10 +517,10 @@ theorem size_eq_length_data (as : Array α) : as.size = as.data.length := rfl simp only [H, getElem_eq_data_get, ← List.get?_eq_get, Nat.le_of_lt h₁, getElem?_eq_data_get?] split <;> rename_i h₂ · simp only [← h₂, Nat.not_le.2 (Nat.lt_succ_self _), Nat.le_refl, and_false] - exact (List.get?_reverse' _ _ (Eq.trans (by simp_arith) h)).symm + exact (List.get?_reverse' (j+1) i (Eq.trans (by simp_arith) h)).symm split <;> rename_i h₃ · simp only [← h₃, Nat.not_le.2 (Nat.lt_succ_self _), Nat.le_refl, false_and] - exact (List.get?_reverse' _ _ (Eq.trans (by simp_arith) h)).symm + exact (List.get?_reverse' i (j+1) (Eq.trans (by simp_arith) h)).symm simp only [Nat.succ_le, Nat.lt_iff_le_and_ne.trans (and_iff_left h₃), Nat.lt_succ.symm.trans (Nat.lt_iff_le_and_ne.trans (and_iff_left (Ne.symm h₂)))] · rw [H]; split <;> rename_i h₂ diff --git a/src/Init/Data/List/BasicAux.lean b/src/Init/Data/List/BasicAux.lean index 33f331e81791..053f261adbb0 100644 --- a/src/Init/Data/List/BasicAux.lean +++ b/src/Init/Data/List/BasicAux.lean @@ -52,6 +52,8 @@ theorem ext_get? : ∀ {l₁ l₂ : List α}, (∀ n, l₁.get? n = l₂.get? n) have h0 : some a = some a' := h 0 injection h0 with aa; simp only [aa, ext_get? fun n => h (n+1)] +@[deprecated (since := "2024-06-07")] abbrev ext := @ext_get? + /-- Returns the first element in the list. diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index 5cc47a6e51fb..9090cb6f68c3 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/src/Init/Data/List/Lemmas.lean @@ -317,21 +317,21 @@ theorem get?_append_right {l₁ l₂ : List α} {n : Nat} (h : l₁.length ≤ n (l₁ ++ l₂).get? n = l₂.get? (n - l₁.length) := by simp [getElem?_append_right, h] -theorem getElem?_reverse' : ∀ {l : List α} {i j}, i + j + 1 = length l → +theorem getElem?_reverse' : ∀ {l : List α} (i j), i + j + 1 = length l → l.reverse[i]? = l[j]? | [], _, _, _ => rfl | a::l, i, 0, h => by simp [Nat.succ.injEq] at h; simp [h, getElem?_append_right, Nat.succ.injEq] | a::l, i, j+1, h => by have := Nat.succ.inj h; simp at this ⊢ - rw [getElem?_append, getElem?_reverse' this] + rw [getElem?_append, getElem?_reverse' _ _ this] rw [length_reverse, ← this]; apply Nat.lt_add_of_pos_right (Nat.succ_pos _) -theorem get?_reverse' {l : List α} {i j} (h : i + j + 1 = length l) : get? l.reverse i = get? l j := by - simp [getElem?_reverse' h] +theorem get?_reverse' {l : List α} (i j) (h : i + j + 1 = length l) : get? l.reverse i = get? l j := by + simp [getElem?_reverse' _ _ h] theorem getElem?_reverse {l : List α} {i} (h : i < length l) : l.reverse[i]? = l[l.length - 1 - i]? := - getElem?_reverse' <| by + getElem?_reverse' _ _ <| by rw [Nat.add_sub_of_le (Nat.le_sub_one_of_lt h), Nat.sub_add_cancel (Nat.lt_of_le_of_lt (Nat.zero_le _) h)] From 6ddbc5fe154eb118287fdf2f36b28b07316329d6 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sat, 8 Jun 2024 05:16:29 +1000 Subject: [PATCH 03/20] cleanup comments --- src/Init/Data/Array/Lemmas.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean index ab9842240256..278c9c4c22bf 100644 --- a/src/Init/Data/Array/Lemmas.lean +++ b/src/Init/Data/Array/Lemmas.lean @@ -14,7 +14,7 @@ import Init.TacticsExtra /-! ## Bootstrapping theorems about arrays -This file contains some theorems about `Array` and `List` needed for `Std.List.Basic`. +This file contains some theorems about `Array` and `List` needed for `Init.Data.List.Impl`. -/ namespace Array From 576e2ba7c37f7b3fe90eef198f99745feb19c560 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sat, 8 Jun 2024 06:00:05 +1000 Subject: [PATCH 04/20] add getElem_eq_data_getElem --- src/Init/Data/Array/Lemmas.lean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean index 278c9c4c22bf..101945e1a758 100644 --- a/src/Init/Data/Array/Lemmas.lean +++ b/src/Init/Data/Array/Lemmas.lean @@ -34,9 +34,12 @@ attribute [simp] data_toArray uset @[simp] theorem size_mk (as : List α) : (Array.mk as).size = as.length := by simp [size] -theorem getElem_eq_data_get (a : Array α) (h : i < a.size) : a[i] = a.data.get ⟨i, h⟩ := by +theorem getElem_eq_data_getElem (a : Array α) (h : i < a.size) : a[i] = a.data[i] := by by_cases i < a.size <;> (try simp [*]) <;> rfl +theorem getElem_eq_data_get (a : Array α) (h : i < a.size) : a[i] = a.data.get ⟨i, h⟩ := by + simp [getElem_eq_data_getElem] + theorem foldlM_eq_foldlM_data.aux [Monad m] (f : β → α → m β) (arr : Array α) (i j) (H : arr.size ≤ i + j) (b) : foldlM.loop f arr arr.size (Nat.le_refl _) i j b = (arr.data.drop j).foldlM f b := by From c7c1b59a90d1122fd5ef52ee461564643a923fb8 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Sat, 8 Jun 2024 15:12:13 +1000 Subject: [PATCH 05/20] deprecation --- src/Init/Omega/IntList.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Init/Omega/IntList.lean b/src/Init/Omega/IntList.lean index 3813fe5c30b2..e34d42d289ef 100644 --- a/src/Init/Omega/IntList.lean +++ b/src/Init/Omega/IntList.lean @@ -66,7 +66,7 @@ theorem add_def (xs ys : IntList) : rfl @[simp] theorem add_get (xs ys : IntList) (i : Nat) : (xs + ys).get i = xs.get i + ys.get i := by - simp only [add_def, get, List.zipWithAll_get?, List.get?_eq_none] + simp only [add_def, get, List.get?_zipWithAll, List.get?_eq_none] cases xs.get? i <;> cases ys.get? i <;> simp @[simp] theorem add_nil (xs : IntList) : xs + [] = xs := by simp [add_def] @@ -83,7 +83,7 @@ theorem mul_def (xs ys : IntList) : xs * ys = List.zipWith (· * ·) xs ys := rfl @[simp] theorem mul_get (xs ys : IntList) (i : Nat) : (xs * ys).get i = xs.get i * ys.get i := by - simp only [mul_def, get, List.zipWith_get?] + simp only [mul_def, get, List.get?_zipWith] cases xs.get? i <;> cases ys.get? i <;> simp @[simp] theorem mul_nil_left : ([] : IntList) * ys = [] := rfl From 41a0d26d286f5a7fcac864467f0bd93f25f38bf7 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 11 Jun 2024 15:50:42 +1000 Subject: [PATCH 06/20] restore lemma --- src/Init/Data/List/Lemmas.lean | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index 9090cb6f68c3..8f0b7bd884af 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/src/Init/Data/List/Lemmas.lean @@ -306,6 +306,8 @@ theorem getLast?_eq_get? : ∀ (l : List α), getLast? l = l.get? (l.length - 1) @[simp] theorem getD_eq_getElem? (l) (n) (a : α) : getD l n a = (l[n]?).getD a := by simp [getD] +theorem getD_eq_get? : ∀ l n (a : α), getD l n a = (get? l n).getD a := by simp + theorem getElem?_append_right : ∀ {l₁ l₂ : List α} {n : Nat}, l₁.length ≤ n → (l₁ ++ l₂)[n]? = l₂[n - l₁.length]? | [], _, n, _ => rfl From 2bc98d907dde3366be3e16dcfa5885b22071e278 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 11 Jun 2024 21:15:51 +1000 Subject: [PATCH 07/20] more lemmas --- src/Init/Data/List/Lemmas.lean | 18 ++++++++++++++---- 1 file changed, 14 insertions(+), 4 deletions(-) diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index 8f0b7bd884af..39339b5ecc4f 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/src/Init/Data/List/Lemmas.lean @@ -1333,10 +1333,14 @@ theorem dropLast_append_cons : dropLast (l₁ ++ b::l₂) = l₁ ++ dropLast (b: | [] => rfl | x::xs => by simp -@[simp] theorem get_dropLast : ∀ (xs : List α) (i : Fin xs.dropLast.length), - xs.dropLast.get i = xs.get ⟨i, Nat.lt_of_lt_of_le i.isLt (length_dropLast .. ▸ Nat.pred_le _)⟩ - | _::_::_, ⟨0, _⟩ => rfl - | _::_::_, ⟨i+1, _⟩ => get_dropLast _ ⟨i, _⟩ +@[simp] theorem getElem_dropLast : ∀ (xs : List α) (i : Nat) (h : i < xs.dropLast.length), + xs.dropLast[i] = xs[i]'(Nat.lt_of_lt_of_le h (length_dropLast .. ▸ Nat.pred_le _)) + | _::_::_, 0, _ => rfl + | _::_::_, i+1, _ => getElem_dropLast _ i _ + +theorem get_dropLast (xs : List α) (i : Fin xs.dropLast.length) : + xs.dropLast.get i = xs.get ⟨i, Nat.lt_of_lt_of_le i.isLt (length_dropLast .. ▸ Nat.pred_le _)⟩ := by + simp /-! ### nth element -/ @@ -1353,9 +1357,15 @@ theorem get!_len_le [Inhabited α] : ∀ {l : List α} {n}, length l ≤ n → l | [], _, _ => rfl | _ :: l, _+1, h => get!_len_le (l := l) <| Nat.le_of_succ_le_succ h +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 getElem?_mem {l : List α} {n : Nat} {a : α} (e : l[n]? = some a) : a ∈ l := + let ⟨_, e⟩ := getElem?_eq_some.1 e; e ▸ getElem_mem .. + theorem get?_mem {l : List α} {n a} (e : l.get? n = some a) : a ∈ l := let ⟨_, e⟩ := get?_eq_some.1 e; e ▸ get_mem .. From 20700d8fd007d3d370fd89e01dc42f3e0216f5a2 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 12 Jun 2024 10:51:55 +1000 Subject: [PATCH 08/20] lemmas --- src/Init/Data/List/Lemmas.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index 39339b5ecc4f..185704d717d0 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/src/Init/Data/List/Lemmas.lean @@ -363,8 +363,8 @@ 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) -@[simp] theorem getElem_map (f : α → β) {l n} {h : n < (map f l).length} : - (map f l)[n] = f (get l ⟨n, length_map l f ▸ h⟩) := +@[simp] theorem getElem_map (f : α → β) {l} {n : Nat} {h : n < (map f l).length} : + (map f l)[n] = f (l[n]'(length_map l f ▸ h)) := Option.some.inj <| by rw [← getElem?_eq_getElem, getElem?_map, getElem?_eq_getElem]; rfl theorem get_map (f : α → β) {l n} : From 6105916a0976d34407a9a5e48a0d3a3db866cd50 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 12 Jun 2024 12:29:09 +1000 Subject: [PATCH 09/20] lemma --- src/Init/Data/List/TakeDrop.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/Init/Data/List/TakeDrop.lean b/src/Init/Data/List/TakeDrop.lean index 32b41c933cdf..af7502d9cc14 100644 --- a/src/Init/Data/List/TakeDrop.lean +++ b/src/Init/Data/List/TakeDrop.lean @@ -86,6 +86,12 @@ theorem take_append {l₁ l₂ : List α} (i : Nat) : take (l₁.length + i) (l₁ ++ l₂) = l₁ ++ take i l₂ := by rw [take_append_eq_append_take, take_all_of_le (Nat.le_add_right _ _), Nat.add_sub_cancel_left] +/-- The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of +length `> i`. Version designed to rewrite from the big list to the small list. -/ +theorem getElem_take (L : List α) {i j : Nat} (hi : i < L.length) (hj : i < j) : + L[i] = (L.take j)[i]'(length_take .. ▸ Nat.lt_min.mpr ⟨hj, hi⟩) := + getElem_of_eq (take_append_drop j L).symm _ ▸ getElem_append .. + /-- The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of length `> i`. Version designed to rewrite from the big list to the small list. -/ theorem get_take (L : List α) {i j : Nat} (hi : i < L.length) (hj : i < j) : From 5ffca9b98f42b7cedc3fbf2a5461b00dcc3d8bf9 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 12 Jun 2024 13:36:20 +1000 Subject: [PATCH 10/20] more lemmas --- src/Init/Data/List/TakeDrop.lean | 27 ++++++++++++++++++++++----- src/Init/GetElem.lean | 8 ++++++-- 2 files changed, 28 insertions(+), 7 deletions(-) diff --git a/src/Init/Data/List/TakeDrop.lean b/src/Init/Data/List/TakeDrop.lean index af7502d9cc14..2bbd21e1efc1 100644 --- a/src/Init/Data/List/TakeDrop.lean +++ b/src/Init/Data/List/TakeDrop.lean @@ -260,12 +260,26 @@ theorem lt_length_drop (L : List α) {i j : Nat} (h : i + j < L.length) : j < (L /-- The `i + j`-th element of a list coincides with the `j`-th element of the list obtained by dropping the first `i` elements. Version designed to rewrite from the big list to the small list. -/ -theorem get_drop (L : List α) {i j : Nat} (h : i + j < L.length) : - get L ⟨i + j, h⟩ = get (L.drop i) ⟨j, lt_length_drop L h⟩ := by +theorem getElem_drop (L : List α) {i j : Nat} (h : i + j < L.length) : + L[i + j] = (L.drop i)[j]'(lt_length_drop L h) := by have : i ≤ L.length := Nat.le_trans (Nat.le_add_right _ _) (Nat.le_of_lt h) - rw [get_of_eq (take_append_drop i L).symm ⟨i + j, h⟩, get_append_right'] <;> + rw [getElem_of_eq (take_append_drop i L).symm h, getElem_append_right'] <;> simp [Nat.min_eq_left this, Nat.add_sub_cancel_left, Nat.le_add_right] +/-- The `i + j`-th element of a list coincides with the `j`-th element of the list obtained by +dropping the first `i` elements. Version designed to rewrite from the big list to the small list. -/ +theorem get_drop (L : List α) {i j : Nat} (h : i + j < L.length) : + get L ⟨i + j, h⟩ = get (L.drop i) ⟨j, lt_length_drop L h⟩ := by + simp [getElem_drop] + +/-- The `i + j`-th element of a list coincides with the `j`-th element of the list obtained by +dropping the first `i` elements. Version designed to rewrite from the small list to the big list. -/ +theorem getElem_drop' (L : List α) {i : Nat} {j : Nat} {h : j < (L.drop i).length} : + (L.drop i)[j] = L[i + j]'(by + rw [Nat.add_comm] + exact Nat.add_lt_of_lt_sub (length_drop i L ▸ h)) := by + rw [getElem_drop] + /-- The `i + j`-th element of a list coincides with the `j`-th element of the list obtained by dropping the first `i` elements. Version designed to rewrite from the small list to the big list. -/ theorem get_drop' (L : List α) {i j} : @@ -275,9 +289,9 @@ theorem get_drop' (L : List α) {i j} : rw [get_drop] @[simp] -theorem get?_drop (L : List α) (i j : Nat) : get? (L.drop i) j = get? L (i + j) := by +theorem getElem?_drop (L : List α) (i j : Nat) : (L.drop i)[j]? = L[i + j]? := by ext - simp only [get?_eq_some, get_drop', Option.mem_def] + simp only [getElem?_eq_some, getElem_drop', Option.mem_def] constructor <;> intro ⟨h, ha⟩ · exact ⟨_, ha⟩ · refine ⟨?_, ha⟩ @@ -285,6 +299,9 @@ theorem get?_drop (L : List α) (i j : Nat) : get? (L.drop i) j = get? L (i + j) rw [Nat.add_comm] at h apply Nat.lt_sub_of_add_lt h +theorem get?_drop (L : List α) (i j : Nat) : get? (L.drop i) j = get? L (i + j) := by + simp + @[simp] theorem drop_drop (n : Nat) : ∀ (m) (l : List α), drop n (drop m l) = drop (n + m) l | m, [] => by simp | 0, l => by simp diff --git a/src/Init/GetElem.lean b/src/Init/GetElem.lean index bcfefaa366de..2b9508ff03a5 100644 --- a/src/Init/GetElem.lean +++ b/src/Init/GetElem.lean @@ -141,12 +141,16 @@ instance : GetElem (List α) Nat α fun as i => i < as.length where instance : LawfulGetElem (List α) Nat α fun as i => i < as.length where -@[simp] theorem cons_getElem_zero (a : α) (as : List α) (h : 0 < (a :: as).length) : getElem (a :: as) 0 h = a := by +@[simp] theorem getElem_cons_zero (a : α) (as : List α) (h : 0 < (a :: as).length) : getElem (a :: as) 0 h = a := by rfl -@[simp] theorem cons_getElem_succ (a : α) (as : List α) (i : Nat) (h : i + 1 < (a :: as).length) : getElem (a :: as) (i+1) h = getElem as i (Nat.lt_of_succ_lt_succ h) := by +@[deprecated (since := "2024-6-12")] abbrev cons_getElem_zero := @getElem_cons_zero + +@[simp] theorem getElem_cons_succ (a : α) (as : List α) (i : Nat) (h : i + 1 < (a :: as).length) : getElem (a :: as) (i+1) h = getElem as i (Nat.lt_of_succ_lt_succ h) := by rfl +@[deprecated (since := "2024-6-12")] abbrev cons_getElem_succ := @getElem_cons_succ + theorem get_drop_eq_drop (as : List α) (i : Nat) (h : i < as.length) : as[i] :: as.drop (i+1) = as.drop i := match as, i with | _::_, 0 => rfl From a6c3520043af1ae535e1a8c8c03f5f0fa498c510 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 12 Jun 2024 13:39:39 +1000 Subject: [PATCH 11/20] more --- src/Init/Data/List/TakeDrop.lean | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/src/Init/Data/List/TakeDrop.lean b/src/Init/Data/List/TakeDrop.lean index 2bbd21e1efc1..eeb511b57644 100644 --- a/src/Init/Data/List/TakeDrop.lean +++ b/src/Init/Data/List/TakeDrop.lean @@ -105,7 +105,7 @@ theorem get_take' (L : List α) {j i} : get L ⟨i.1, Nat.lt_of_lt_of_le i.2 (length_take_le' _ _)⟩ := by let ⟨i, hi⟩ := i; rw [length_take, Nat.lt_min] at hi; rw [get_take L _ hi.1] -theorem get?_take {l : List α} {n m : Nat} (h : m < n) : (l.take n).get? m = l.get? m := by +theorem getElem?_take {l : List α} {n m : Nat} (h : m < n) : (l.take n)[m]? = l[m]? := by induction n generalizing l m with | zero => exact absurd h (Nat.not_lt_of_le m.zero_le) @@ -114,8 +114,11 @@ theorem get?_take {l : List α} {n m : Nat} (h : m < n) : (l.take n).get? m = l. | nil => simp only [take_nil] | cons hd tl => cases m - · simp only [get?, take] - · simpa only using hn (Nat.lt_of_succ_lt_succ h) + · simp + · simpa using hn (Nat.lt_of_succ_lt_succ h) + +theorem get?_take {l : List α} {n m : Nat} (h : m < n) : (l.take n).get? m = l.get? m := by + simp [getElem?_take, h] theorem get?_take_eq_none {l : List α} {n m : Nat} (h : n ≤ m) : (l.take n).get? m = none := From 2a3d66e8071a0644fe8eb6a6e0504f7b75d8f305 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 12 Jun 2024 15:08:09 +1000 Subject: [PATCH 12/20] add deprecations --- src/Init/Data/Array/Lemmas.lean | 40 +++++++++++++++++--------------- src/Init/Data/List/BasicAux.lean | 4 ++-- src/Init/Data/List/Lemmas.lean | 8 +++++++ 3 files changed, 31 insertions(+), 21 deletions(-) diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean index 101945e1a758..8e4349e7bd69 100644 --- a/src/Init/Data/Array/Lemmas.lean +++ b/src/Init/Data/Array/Lemmas.lean @@ -37,6 +37,7 @@ attribute [simp] data_toArray uset theorem getElem_eq_data_getElem (a : Array α) (h : i < a.size) : a[i] = a.data[i] := by by_cases i < a.size <;> (try simp [*]) <;> rfl +@[deprecated (since := "2024-06-12")] theorem getElem_eq_data_get (a : Array α) (h : i < a.size) : a[i] = a.data.get ⟨i, h⟩ := by simp [getElem_eq_data_getElem] @@ -117,11 +118,11 @@ theorem foldr_push (f : α → β → β) (init : β) (arr : Array α) (a : α) theorem get_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_data_get, List.concat_eq_append, List.get_append_left, h] + simp only [push, getElem_eq_data_getElem, 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 only [push, getElem_eq_data_get, List.concat_eq_append] - rw [List.get_append_right] <;> simp [getElem_eq_data_get, Nat.zero_lt_one] + simp only [push, getElem_eq_data_getElem, List.concat_eq_append] + rw [List.getElem_append_right] <;> simp [getElem_eq_data_getElem, Nat.zero_lt_one] theorem get_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 @@ -236,11 +237,11 @@ theorem get!_eq_getD [Inhabited α] (a : Array α) : a.get! n = a.getD n default @[simp] theorem getElem_set_eq (a : Array α) (i : Fin a.size) (v : α) {j : Nat} (eq : i.val = j) (p : j < (a.set i v).size) : (a.set i v)[j]'p = v := by - simp [set, getElem_eq_data_get, ←eq] + simp [set, getElem_eq_data_getElem, ←eq] @[simp] theorem getElem_set_ne (a : Array α) (i : Fin a.size) (v : α) {j : Nat} (pj : j < (a.set i v).size) (h : i.val ≠ j) : (a.set i v)[j]'pj = a[j]'(size_set a i v ▸ pj) := by - simp only [set, getElem_eq_data_get, List.get_set_ne _ h] + simp only [set, getElem_eq_data_getElem, List.getElem_set_ne _ h] theorem getElem_set (a : Array α) (i : Fin a.size) (v : α) (j : Nat) (h : j < (a.set i v).size) : @@ -324,7 +325,7 @@ termination_by n - i @[simp] theorem mkArray_data (n : Nat) (v : α) : (mkArray n v).data = List.replicate n v := rfl @[simp] theorem getElem_mkArray (n : Nat) (v : α) (h : i < (mkArray n v).size) : - (mkArray n v)[i] = v := by simp [Array.getElem_eq_data_get] + (mkArray n v)[i] = v := by simp [Array.getElem_eq_data_getElem] /-- # mem -/ @@ -335,7 +336,7 @@ theorem not_mem_nil (a : α) : ¬ a ∈ #[] := nofun /-- # get lemmas -/ theorem getElem?_mem {l : Array α} {i : Fin l.size} : l[i] ∈ l := by - erw [Array.mem_def, getElem_eq_data_get] + erw [Array.mem_def, getElem_eq_data_getElem] apply List.get_mem theorem getElem_fin_eq_data_get (a : Array α) (i : Fin _) : a[i] = a.data.get i := rfl @@ -350,7 +351,7 @@ theorem get?_len_le (a : Array α) (i : Nat) (h : a.size ≤ i) : a[i]? = none : simp [getElem?_neg, h] theorem getElem_mem_data (a : Array α) (h : i < a.size) : a[i] ∈ a.data := by - simp only [getElem_eq_data_get, List.get_mem] + simp only [getElem_eq_data_getElem, List.getElem_mem] theorem getElem?_eq_data_get? (a : Array α) (i : Nat) : a[i]? = a.data.get? i := by by_cases i < a.size <;> simp_all [getElem?_pos, getElem?_neg, List.get?_eq_get, eq_comm]; rfl @@ -398,7 +399,7 @@ theorem get?_push {a : Array α} : (a.push x)[i]? = if i = a.size then some x el theorem get_set_eq (a : Array α) (i : Fin a.size) (v : α) : (a.set i v)[i.1] = v := by - simp only [set, getElem_eq_data_get, List.get_set_eq] + simp only [set, getElem_eq_data_getElem, List.getElem_set_eq] theorem get?_set_eq (a : Array α) (i : Fin a.size) (v : α) : (a.set i v)[i.1]? = v := by simp [getElem?_pos, i.2] @@ -417,7 +418,7 @@ theorem get_set (a : Array α) (i : Fin a.size) (j : Nat) (hj : j < a.size) (v : @[simp] theorem get_set_ne (a : Array α) (i : Fin a.size) {j : Nat} (v : α) (hj : j < a.size) (h : i.1 ≠ j) : (a.set i v)[j]'(by simp [*]) = a[j] := by - simp only [set, getElem_eq_data_get, List.get_set_ne _ h] + simp only [set, getElem_eq_data_getElem, List.getElem_set_ne _ h] theorem getElem_setD (a : Array α) (i : Nat) (v : α) (h : i < (setD a i v).size) : (setD a i v)[i] = v := by @@ -503,6 +504,7 @@ theorem size_eq_length_data (as : Array α) : as.size = as.data.length := rfl simp only [mkEmpty_eq, size_push] at * omega +set_option linter.deprecated false in @[simp] theorem reverse_data (a : Array α) : a.reverse.data = a.data.reverse := by let rec go (as : Array α) (i j hj) (h : i + j + 1 = a.size) (h₂ : as.size = a.size) @@ -772,17 +774,17 @@ theorem size_append (as bs : Array α) : (as ++ bs).size = as.size + bs.size := theorem get_append_left {as bs : Array α} {h : i < (as ++ bs).size} (hlt : i < as.size) : (as ++ bs)[i] = as[i] := by - simp only [getElem_eq_data_get] + simp only [getElem_eq_data_getElem] have h' : i < (as.data ++ bs.data).length := by rwa [← data_length, append_data] at h - conv => rhs; rw [← List.get_append_left (bs:=bs.data) (h':=h')] + conv => rhs; rw [← List.getElem_append_left (bs := bs.data) (h' := h')] apply List.get_of_eq; rw [append_data] theorem get_append_right {as bs : Array α} {h : i < (as ++ bs).size} (hle : as.size ≤ i) (hlt : i - as.size < bs.size := Nat.sub_lt_left_of_lt_add hle (size_append .. ▸ h)) : (as ++ bs)[i] = bs[i - as.size] := by - simp only [getElem_eq_data_get] + simp only [getElem_eq_data_getElem] have h' : i < (as.data ++ bs.data).length := by rwa [← data_length, append_data] at h - conv => rhs; rw [← List.get_append_right (h':=h') (h:=Nat.not_lt_of_ge hle)] + conv => rhs; rw [← List.getElem_append_right (h' := h') (h := Nat.not_lt_of_ge hle)] apply List.get_of_eq; rw [append_data] @[simp] theorem append_nil (as : Array α) : as ++ #[] = as := by @@ -990,13 +992,13 @@ theorem all_eq_true (p : α → Bool) (as : Array α) : all as p ↔ ∀ i : Fin simp [all_iff_forall, Fin.isLt] theorem all_def {p : α → Bool} (as : Array α) : as.all p = as.data.all p := by - rw [Bool.eq_iff_iff, all_eq_true, List.all_eq_true]; simp only [List.mem_iff_get] + rw [Bool.eq_iff_iff, all_eq_true, List.all_eq_true]; simp only [List.mem_iff_getElem] constructor - · rintro w x ⟨r, rfl⟩ - rw [← getElem_eq_data_get] - apply w + · rintro w x ⟨r, h, rfl⟩ + rw [← getElem_eq_data_getElem] + exact w ⟨r, h⟩ · intro w i - exact w as[i] ⟨i, (getElem_eq_data_get as i.2).symm⟩ + exact w as[i] ⟨i, i.2, (getElem_eq_data_getElem as i.2).symm⟩ theorem all_eq_true_iff_forall_mem {l : Array α} : l.all p ↔ ∀ x, x ∈ l → p x := by simp only [all_def, List.all_eq_true, mem_def] diff --git a/src/Init/Data/List/BasicAux.lean b/src/Init/Data/List/BasicAux.lean index 053f261adbb0..3ff98f4c6330 100644 --- a/src/Init/Data/List/BasicAux.lean +++ b/src/Init/Data/List/BasicAux.lean @@ -193,7 +193,7 @@ def rotateRight (xs : List α) (n : Nat := 1) : List α := let e := xs.drop n e ++ b -theorem get_append_left (as bs : List α) (h : i < as.length) {h'} : (as ++ bs).get ⟨i, h'⟩ = as.get ⟨i, h⟩ := by +theorem getElem_append_left (as bs : List α) (h : i < as.length) {h'} : (as ++ bs)[i] = as[i] := by induction as generalizing i with | nil => trivial | cons a as ih => @@ -201,7 +201,7 @@ theorem get_append_left (as bs : List α) (h : i < as.length) {h'} : (as ++ bs). | zero => rfl | succ i => apply ih -theorem get_append_right (as bs : List α) (h : ¬ i < as.length) {h' h''} : (as ++ bs).get ⟨i, h'⟩ = bs.get ⟨i - as.length, h''⟩ := by +theorem getElem_append_right (as bs : List α) (h : ¬ i < as.length) {h' h''} : (as ++ bs)[i]'h' = bs[i - as.length]'h'' := by induction as generalizing i with | nil => trivial | cons a as ih => diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index 185704d717d0..1c14c97556fb 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/src/Init/Data/List/Lemmas.lean @@ -167,6 +167,14 @@ theorem get_append {l₁ l₂ : List α} (n : Nat) (h : n < l₁.length) : (l₁ ++ l₂).get ⟨n, length_append .. ▸ Nat.lt_add_right _ h⟩ = l₁.get ⟨n, h⟩ := by simp [getElem_append, h] +@[deprecated getElem_append_left (since := "2024-06-12")] +theorem get_append_left (as bs : List α) (h : i < as.length) {h'} : (as ++ bs).get ⟨i, h'⟩ = as.get ⟨i, h⟩ := by + simp [getElem_append_left, h, h'] + +@[deprecated getElem_append_right (since := "2024-06-12")] +theorem get_append_right (as bs : List α) (h : ¬ i < as.length) {h' h''} : (as ++ bs).get ⟨i, h'⟩ = bs.get ⟨i - as.length, h''⟩ := by + simp [getElem_append_right, h, h', h''] + /-! ### map -/ @[simp] theorem map_nil {f : α → β} : map f [] = [] := rfl From 6488ffbc8c170c7fdf67b35b1e21724f2d039e01 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Wed, 12 Jun 2024 16:23:48 +1000 Subject: [PATCH 13/20] more deprecations --- src/Init/Data/List/Lemmas.lean | 30 ++++++++++++++++++++++++++++-- 1 file changed, 28 insertions(+), 2 deletions(-) diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index 1c14c97556fb..e1d198d39243 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/src/Init/Data/List/Lemmas.lean @@ -163,6 +163,7 @@ theorem getElem_append : ∀ {l₁ l₂ : List α} (n : Nat) (h : n < l₁.lengt | a :: l, _, 0, h => rfl | a :: l, _, n+1, h => by simp only [get, cons_append]; apply getElem_append +@[deprecated getElem_append (since := "2024-06-12")] theorem get_append {l₁ l₂ : List α} (n : Nat) (h : n < l₁.length) : (l₁ ++ l₂).get ⟨n, length_append .. ▸ Nat.lt_add_right _ h⟩ = l₁.get ⟨n, h⟩ := by simp [getElem_append, h] @@ -268,6 +269,7 @@ theorem mem_iff_get {a} {l : List α} : a ∈ l ↔ ∃ n, get l n = a := | _ :: _, 0 => by simp | _ :: l, n+1 => by simp [getElem?_map f l n] +@[deprecated getElem?_map (since := "2024-06-12")] theorem get?_map (f : α → β) : ∀ l n, (map f l).get? n = (l.get? n).map f | [], _ => rfl | _ :: _, 0 => rfl @@ -279,6 +281,7 @@ theorem getElem?_append {l₁ l₂ : List α} {n : Nat} (hn : n < l₁.length) : length_append .. ▸ Nat.le_add_right .. simp_all [getElem?_eq_getElem, getElem_append] +@[deprecated (since := "2024-06-12")] theorem get?_append {l₁ l₂ : List α} {n : Nat} (hn : n < l₁.length) : (l₁ ++ l₂).get? n = l₁.get? n := by simp [getElem?_append hn] @@ -287,6 +290,7 @@ theorem get?_append {l₁ l₂ : List α} {n : Nat} (hn : n < l₁.length) : | [], a => rfl | b :: l, a => by rw [cons_append, length_cons]; simp [getElem?_concat_length] +@[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 getLast_eq_get : ∀ (l : List α) (h : l ≠ []), @@ -314,6 +318,7 @@ theorem getLast?_eq_get? : ∀ (l : List α), getLast? l = l.get? (l.length - 1) @[simp] theorem getD_eq_getElem? (l) (n) (a : α) : getD l n a = (l[n]?).getD a := by simp [getD] +@[deprecated getD_eq_getElem? (since := "2024-06-12")] theorem getD_eq_get? : ∀ l n (a : α), getD l n a = (get? l n).getD a := by simp theorem getElem?_append_right : ∀ {l₁ l₂ : List α} {n : Nat}, l₁.length ≤ n → @@ -323,6 +328,7 @@ theorem getElem?_append_right : ∀ {l₁ l₂ : List α} {n : Nat}, l₁.length rw [cons_append] simp [Nat.succ_sub_succ_eq_sub, getElem?_append_right (Nat.lt_succ.1 h₁)] +@[deprecated getElem?_append_right (since := "2024-06-12")] theorem get?_append_right {l₁ l₂ : List α} {n : Nat} (h : l₁.length ≤ n) : (l₁ ++ l₂).get? n = l₂.get? (n - l₁.length) := by simp [getElem?_append_right, h] @@ -336,6 +342,7 @@ theorem getElem?_reverse' : ∀ {l : List α} (i j), i + j + 1 = length l → rw [getElem?_append, getElem?_reverse' _ _ this] rw [length_reverse, ← this]; apply Nat.lt_add_of_pos_right (Nat.succ_pos _) +@[deprecated getElem?_reverse' (since := "2024-06-12")] theorem get?_reverse' {l : List α} (i j) (h : i + j + 1 = length l) : get? l.reverse i = get? l j := by simp [getElem?_reverse' _ _ h] @@ -345,6 +352,7 @@ theorem getElem?_reverse {l : List α} {i} (h : i < length l) : rw [Nat.add_sub_of_le (Nat.le_sub_one_of_lt h), Nat.sub_add_cancel (Nat.lt_of_le_of_lt (Nat.zero_le _) h)] +@[deprecated getElem?_reverse (since := "2024-06-12")] theorem get?_reverse {l : List α} {i} (h : i < length l) : get? l.reverse i = get? l (l.length - 1 - i) := by simp [getElem?_reverse h] @@ -375,6 +383,7 @@ theorem ext_get {l₁ l₂ : List α} (hl : length l₁ = length l₂) (map f l)[n] = f (l[n]'(length_map l f ▸ h)) := Option.some.inj <| by rw [← getElem?_eq_getElem, getElem?_map, getElem?_eq_getElem]; rfl +@[deprecated getElem_map (since := "2024-06-12")] theorem get_map (f : α → β) {l n} : get (map f l) n = f (get l ⟨n, length_map l f ▸ n.2⟩) := by simp @@ -642,12 +651,14 @@ theorem getElem?_zipWith {f : α → β → γ} {i : Nat} : | nil => simp | cons b bs => cases i <;> simp_all +@[deprecated getElem?_zipWith (since := "2024-06-12")] theorem get?_zipWith {f : α → β → γ} : (List.zipWith f as bs).get? i = match as.get? i, bs.get? i with | some a, some b => some (f a b) | _, _ => none := by simp [getElem?_zipWith] -@[deprecated (since := "2024-06-07")] abbrev zipWith_get? := @get?_zipWith +set_option linter.deprecated false in +@[deprecated getElem?_zipWith (since := "2024-06-07")] abbrev zipWith_get? := @get?_zipWith /-! ### zipWithAll -/ @@ -664,12 +675,14 @@ theorem getElem?_zipWithAll {f : Option α → Option β → γ} {i : Nat } : cases i <;> simp_all | cons b bs => cases i <;> simp_all +@[deprecated getElem?_zipWithAll (since := "2024-06-12")] theorem get?_zipWithAll {f : Option α → Option β → γ} : (zipWithAll f as bs).get? i = match as.get? i, bs.get? i with | none, none => .none | a?, b? => some (f a? b?) := by simp [getElem?_zipWithAll] -@[deprecated (since := "2024-06-07")] abbrev zipWithAll_get? := @get?_zipWithAll +set_option linter.deprecated false in +@[deprecated getElem?_zipWithAll (since := "2024-06-07")] abbrev zipWithAll_get? := @get?_zipWithAll /-! ### zip -/ @@ -833,6 +846,7 @@ theorem minimum?_eq_some_iff [Min α] [LE α] [anti : Antisymm ((· : α) ≤ · | _ :: l, i + 1 => by simp [getElem_set_eq l] +@[deprecated getElem_set_eq (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 @@ -853,6 +867,7 @@ theorem get_set_eq (l : List α) (i : Nat) (a : α) (h : i < (l.set i a).length) have g : i ≠ j := h ∘ congrArg (· + 1) simp [getElem_set_ne l 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 @@ -1346,6 +1361,7 @@ theorem dropLast_append_cons : dropLast (l₁ ++ b::l₂) = l₁ ++ dropLast (b: | _::_::_, 0, _ => rfl | _::_::_, i+1, _ => getElem_dropLast _ i _ +@[deprecated getElem_dropLast (since := "2024-06-12")] theorem get_dropLast (xs : List α) (i : Fin xs.dropLast.length) : xs.dropLast.get i = xs.get ⟨i, Nat.lt_of_lt_of_le i.isLt (length_dropLast .. ▸ Nat.pred_le _)⟩ := by simp @@ -1408,6 +1424,7 @@ theorem get_of_eq {l l' : List α} (h : l = l') (i : Fin 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) := @@ -1422,11 +1439,14 @@ theorem getElem_append_right' {l₁ l₂ : List α} {n : Nat} (h₁ : l₁.lengt l₂[n - l₁.length]'(by rw [length_append] at h₂; exact Nat.sub_lt_left_of_lt_add h₁ h₂) := Option.some.inj <| by rw [← getElem?_eq_getElem, ← getElem?_eq_getElem, getElem?_append_right h₁] +@[deprecated (since := "2024-06-12")] theorem get_append_right_aux {l₁ l₂ : List α} {n : Nat} (h₁ : l₁.length ≤ n) (h₂ : n < (l₁ ++ l₂).length) : n - l₁.length < l₂.length := by rw [length_append] at h₂ exact Nat.sub_lt_left_of_lt_add h₁ h₂ +set_option linter.deprecated false in +@[deprecated getElem_append_right' (since := "2024-06-12")] theorem get_append_right' {l₁ l₂ : List α} {n : Nat} (h₁ : l₁.length ≤ n) (h₂) : (l₁ ++ l₂).get ⟨n, h₂⟩ = l₂.get ⟨n - l₁.length, get_append_right_aux h₁ h₂⟩ := Option.some.inj <| by rw [← get?_eq_get, ← get?_eq_get, get?_append_right h₁] @@ -1436,9 +1456,12 @@ theorem getElem_of_append {l : List α} (eq : l = l₁ ++ a :: l₂) (h : l₁.l rw [← getElem?_eq_getElem, eq, getElem?_append_right (h ▸ Nat.le_refl _), h] simp +@[deprecated (since := "2024-06-12")] theorem get_of_append_proof {l : List α} (eq : l = l₁ ++ a :: l₂) (h : l₁.length = n) : n < length l := eq ▸ h ▸ by simp_arith +set_option linter.deprecated false in +@[deprecated getElem_of_append (since := "2024-06-12")] theorem get_of_append {l : List α} (eq : l = l₁ ++ a :: l₂) (h : l₁.length = n) : l.get ⟨n, get_of_append_proof eq h⟩ = a := Option.some.inj <| by rw [← get?_eq_get, eq, get?_append_right (h ▸ Nat.le_refl _), h, Nat.sub_self]; rfl @@ -1447,6 +1470,7 @@ theorem get_of_append {l : List α} (eq : l = l₁ ++ a :: l₂) (h : l₁.lengt (replicate n a)[m] = a := eq_of_mem_replicate (get_mem _ _ _) +@[deprecated getElem_replicate (since := "2024-06-12")] theorem get_replicate (a : α) {n : Nat} (m : Fin _) : (replicate n a).get m = a := by simp @@ -1457,6 +1481,7 @@ theorem getElem_cons_length (x : α) (xs : List α) (n : Nat) (h : n = xs.length (x :: xs)[n]'(by simp [h]) = (x :: xs).getLast (cons_ne_nil x xs) := by rw [getLast_eq_get]; cases h; rfl +@[deprecated getElem_cons_length (since := "2024-06-12")] theorem get_cons_length (x : α) (xs : List α) (n : Nat) (h : n = xs.length) : (x :: xs).get ⟨n, by simp [h]⟩ = (x :: xs).getLast (cons_ne_nil x xs) := by simp [getElem_cons_length, h] @@ -1503,6 +1528,7 @@ theorem getElem_set (a : α) {m n} (l : List α) (h) : else simp [h] +@[deprecated getElem_set (since := "2024-06-12")] theorem get_set (a : α) {m n} (l : List α) (h) : (set l m a).get ⟨n, h⟩ = if m = n then a else l.get ⟨n, length_set .. ▸ h⟩ := by simp [getElem_set] From 6f5f994a5e045f6c0b09fcbddc34907f5ae21e3a Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 13 Jun 2024 10:05:29 +1000 Subject: [PATCH 14/20] deprecations --- src/Init/Omega/IntList.lean | 20 +++++++------- versions | 52 +++++++++++++++++++++++++++++++++++++ 2 files changed, 62 insertions(+), 10 deletions(-) create mode 100755 versions diff --git a/src/Init/Omega/IntList.lean b/src/Init/Omega/IntList.lean index e34d42d289ef..245f4d631bd6 100644 --- a/src/Init/Omega/IntList.lean +++ b/src/Init/Omega/IntList.lean @@ -28,8 +28,8 @@ def get (xs : IntList) (i : Nat) : Int := (xs.get? i).getD 0 @[simp] theorem get_cons_succ : get (x :: xs) (i+1) = get xs i := rfl theorem get_map {xs : IntList} (h : f 0 = 0) : get (xs.map f) i = f (xs.get i) := by - simp only [get, List.get?_map] - cases xs.get? i <;> simp_all + simp only [get, List.get?_eq_getElem?, List.getElem?_map] + 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] @@ -66,8 +66,8 @@ theorem add_def (xs ys : IntList) : rfl @[simp] theorem add_get (xs ys : IntList) (i : Nat) : (xs + ys).get i = xs.get i + ys.get i := by - simp only [add_def, get, List.get?_zipWithAll, List.get?_eq_none] - cases xs.get? i <;> cases ys.get? i <;> simp + simp only [get, add_def, List.get?_eq_getElem?, List.getElem?_zipWithAll] + cases xs[i]? <;> cases ys[i]? <;> simp @[simp] theorem add_nil (xs : IntList) : xs + [] = xs := by simp [add_def] @[simp] theorem nil_add (xs : IntList) : [] + xs = xs := by simp [add_def] @@ -83,8 +83,8 @@ theorem mul_def (xs ys : IntList) : xs * ys = List.zipWith (· * ·) xs ys := rfl @[simp] theorem mul_get (xs ys : IntList) (i : Nat) : (xs * ys).get i = xs.get i * ys.get i := by - simp only [mul_def, get, List.get?_zipWith] - cases xs.get? i <;> cases ys.get? i <;> simp + simp only [get, mul_def, List.get?_eq_getElem?, List.getElem?_zipWith] + cases xs[i]? <;> cases ys[i]? <;> simp @[simp] theorem mul_nil_left : ([] : IntList) * ys = [] := rfl @[simp] theorem mul_nil_right : xs * ([] : IntList) = [] := List.zipWith_nil_right @@ -98,8 +98,8 @@ instance : Neg IntList := ⟨neg⟩ theorem neg_def (xs : IntList) : - xs = xs.map fun x => -x := rfl @[simp] theorem neg_get (xs : IntList) (i : Nat) : (- xs).get i = - xs.get i := by - simp only [neg_def, get, List.get?_map] - cases xs.get? i <;> simp + simp only [get, neg_def, List.get?_eq_getElem?, List.getElem?_map] + cases xs[i]? <;> simp @[simp] theorem neg_nil : (- ([] : IntList)) = [] := rfl @[simp] theorem neg_cons : (- (x::xs : IntList)) = -x :: -xs := rfl @@ -124,8 +124,8 @@ instance : HMul Int IntList IntList where theorem smul_def (xs : IntList) (i : Int) : i * xs = xs.map fun x => i * x := rfl @[simp] theorem smul_get (xs : IntList) (a : Int) (i : Nat) : (a * xs).get i = a * xs.get i := by - simp only [smul_def, get, List.get?_map] - cases xs.get? i <;> simp + simp only [get, smul_def, List.get?_eq_getElem?, List.getElem?_map] + cases xs[i]? <;> simp @[simp] theorem smul_nil {i : Int} : i * ([] : IntList) = [] := rfl @[simp] theorem smul_cons {i : Int} : i * (x::xs : IntList) = i * x :: i * xs := rfl diff --git a/versions b/versions new file mode 100755 index 000000000000..53373adef643 --- /dev/null +++ b/versions @@ -0,0 +1,52 @@ +#!/bin/bash +# Must be run in a copy of the `lean4` repository, and you'll need to login with `gh auth` first. + +check_rate_limit() { + remaining=$(gh api rate_limit | jq '.resources.search.remaining') + if [[ $remaining -le 1 ]]; then + echo "API rate limit exceeded, retrying after a short wait..." + sleep $1 # Wait for the specified time before retrying + return 1 + else + return 0 + fi +} + +perform_search() { + local search_term=$1 + local retries=5 + local wait_time=10 + + for ((i=0; i Date: Thu, 13 Jun 2024 10:06:34 +1000 Subject: [PATCH 15/20] deprecations --- src/Init/Data/Array/Lemmas.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean index 8e4349e7bd69..2c4dff73ad58 100644 --- a/src/Init/Data/Array/Lemmas.lean +++ b/src/Init/Data/Array/Lemmas.lean @@ -456,7 +456,7 @@ theorem swapAt!_def (a : Array α) (i : Nat) (v : α) (h : i < a.size) : @[simp] theorem getElem_pop (a : Array α) (i : Nat) (hi : i < a.pop.size) : a.pop[i] = a[i]'(Nat.lt_of_lt_of_le (a.size_pop ▸ hi) (Nat.sub_le _ _)) := - List.get_dropLast .. + List.getElem_dropLast .. theorem eq_empty_of_size_eq_zero {as : Array α} (h : as.size = 0) : as = #[] := by apply ext From 42f4a4dfc56904df46110a1594038aae1771ab27 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 13 Jun 2024 10:08:45 +1000 Subject: [PATCH 16/20] deprecations --- src/Init/Data/List/TakeDrop.lean | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/Init/Data/List/TakeDrop.lean b/src/Init/Data/List/TakeDrop.lean index eeb511b57644..ea3c3697bc28 100644 --- a/src/Init/Data/List/TakeDrop.lean +++ b/src/Init/Data/List/TakeDrop.lean @@ -92,6 +92,7 @@ theorem getElem_take (L : List α) {i j : Nat} (hi : i < L.length) (hj : i < j) L[i] = (L.take j)[i]'(length_take .. ▸ Nat.lt_min.mpr ⟨hj, hi⟩) := getElem_of_eq (take_append_drop j L).symm _ ▸ getElem_append .. +set_option linter.deprecated false in /-- The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of length `> i`. Version designed to rewrite from the big list to the small list. -/ theorem get_take (L : List α) {i j : Nat} (hi : i < L.length) (hj : i < j) : @@ -134,14 +135,14 @@ theorem get?_take_eq_if {l : List α} {n m : Nat} : theorem nth_take_of_succ {l : List α} {n : Nat} : (l.take (n + 1)).get? n = l.get? n := get?_take (Nat.lt_succ_self n) -theorem take_succ {l : List α} {n : Nat} : l.take (n + 1) = l.take n ++ (l.get? n).toList := by +theorem take_succ {l : List α} {n : Nat} : l.take (n + 1) = l.take n ++ l[n]?.toList := by induction l generalizing n with | nil => - simp only [Option.toList, get?, take_nil, append_nil] + simp only [take_nil, Option.toList, getElem?_nil, append_nil] | cons hd tl hl => cases n - · simp only [Option.toList, get?, eq_self_iff_true, take, nil_append] - · simp only [hl, cons_append, get?, eq_self_iff_true, take] + · simp only [take, Option.toList, getElem?_cons_zero, nil_append] + · simp only [take, hl, getElem?_cons_succ, cons_append] @[simp] theorem take_eq_nil_iff {l : List α} {k : Nat} : l.take k = [] ↔ l = [] ∨ k = 0 := by From 8a8635d523ddf2ff28cdecf2d7c112486b262bc8 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 13 Jun 2024 16:04:18 +1000 Subject: [PATCH 17/20] more lemmas --- src/Init/Data/List/TakeDrop.lean | 18 +++++++++++++----- 1 file changed, 13 insertions(+), 5 deletions(-) diff --git a/src/Init/Data/List/TakeDrop.lean b/src/Init/Data/List/TakeDrop.lean index ea3c3697bc28..905c9a987485 100644 --- a/src/Init/Data/List/TakeDrop.lean +++ b/src/Init/Data/List/TakeDrop.lean @@ -121,15 +121,23 @@ theorem getElem?_take {l : List α} {n m : Nat} (h : m < n) : (l.take n)[m]? = l theorem get?_take {l : List α} {n m : Nat} (h : m < n) : (l.take n).get? m = l.get? m := by simp [getElem?_take, h] +theorem getElem?_take_eq_none {l : List α} {n m : Nat} (h : n ≤ m) : + (l.take n)[m]? = none := + getElem?_eq_none.mpr <| Nat.le_trans (length_take_le _ _) h + theorem get?_take_eq_none {l : List α} {n m : Nat} (h : n ≤ m) : - (l.take n).get? m = none := - get?_eq_none.mpr <| Nat.le_trans (length_take_le _ _) h + (l.take n).get? m = none := by + simp [getElem?_take_eq_none h] + +theorem getElem?_take_eq_if {l : List α} {n m : Nat} : + (l.take n)[m]? = if m < n then l[m]? else none := by + split + · next h => exact getElem?_take h + · next h => exact getElem?_take_eq_none (Nat.le_of_not_lt h) theorem get?_take_eq_if {l : List α} {n m : Nat} : (l.take n).get? m = if m < n then l.get? m else none := by - split - · next h => exact get?_take h - · next h => exact get?_take_eq_none (Nat.le_of_not_lt h) + simp [getElem?_take_eq_if] @[simp] theorem nth_take_of_succ {l : List α} {n : Nat} : (l.take (n + 1)).get? n = l.get? n := From d58b845520175fe1ac10dc6946d4c30187748684 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 13 Jun 2024 16:29:20 +1000 Subject: [PATCH 18/20] another --- src/Init/Data/List/Lemmas.lean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/Init/Data/List/Lemmas.lean b/src/Init/Data/List/Lemmas.lean index e1d198d39243..18192a690d56 100644 --- a/src/Init/Data/List/Lemmas.lean +++ b/src/Init/Data/List/Lemmas.lean @@ -1397,8 +1397,11 @@ theorem get?_mem {l : List α} {n a} (e : l.get? n = some a) : a ∈ l := theorem Fin.exists_iff (p : Fin n → Prop) : (∃ i, p i) ↔ ∃ i h, p ⟨i, h⟩ := ⟨fun ⟨i, h⟩ => ⟨i.1, i.2, h⟩, fun ⟨i, hi, h⟩ => ⟨⟨i, hi⟩, h⟩⟩ +theorem mem_iff_getElem? {a} {l : List α} : a ∈ l ↔ ∃ n : Nat, l[n]? = some a := by + simp [getElem?_eq_some, mem_iff_getElem] + theorem mem_iff_get? {a} {l : List α} : a ∈ l ↔ ∃ n, l.get? n = some a := by - simp [get?_eq_some, getElem?_eq_some, Fin.exists_iff, mem_iff_get] + simp [getElem?_eq_some, Fin.exists_iff, mem_iff_get] theorem get?_zero (l : List α) : l.get? 0 = l.head? := by cases l <;> rfl From e2a00739758b4eb8cddf76ce1eeeec0ca9266175 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 13 Jun 2024 18:43:02 +1000 Subject: [PATCH 19/20] more lemmas/deprecations --- src/Init/Data/Array/Lemmas.lean | 2 +- src/Init/Data/List/TakeDrop.lean | 47 ++++++++++++++++++++++++-------- 2 files changed, 36 insertions(+), 13 deletions(-) diff --git a/src/Init/Data/Array/Lemmas.lean b/src/Init/Data/Array/Lemmas.lean index 2c4dff73ad58..13407928658e 100644 --- a/src/Init/Data/Array/Lemmas.lean +++ b/src/Init/Data/Array/Lemmas.lean @@ -37,7 +37,7 @@ attribute [simp] data_toArray uset theorem getElem_eq_data_getElem (a : Array α) (h : i < a.size) : a[i] = a.data[i] := by by_cases i < a.size <;> (try simp [*]) <;> rfl -@[deprecated (since := "2024-06-12")] +@[deprecated getElem_eq_data_getElem (since := "2024-06-12")] theorem getElem_eq_data_get (a : Array α) (h : i < a.size) : a[i] = a.data.get ⟨i, h⟩ := by simp [getElem_eq_data_getElem] diff --git a/src/Init/Data/List/TakeDrop.lean b/src/Init/Data/List/TakeDrop.lean index 905c9a987485..d72c517584d2 100644 --- a/src/Init/Data/List/TakeDrop.lean +++ b/src/Init/Data/List/TakeDrop.lean @@ -92,19 +92,27 @@ theorem getElem_take (L : List α) {i j : Nat} (hi : i < L.length) (hj : i < j) L[i] = (L.take j)[i]'(length_take .. ▸ Nat.lt_min.mpr ⟨hj, hi⟩) := getElem_of_eq (take_append_drop j L).symm _ ▸ getElem_append .. -set_option linter.deprecated false in +/-- The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of +length `> i`. Version designed to rewrite from the small list to the big list. -/ +theorem getElem_take' (L : List α) {j i : Nat} {h : i < (L.take j).length} : + (L.take j)[i] = + L[i]'(Nat.lt_of_lt_of_le h (length_take_le' _ _)) := by + rw [length_take, Nat.lt_min] at h; rw [getElem_take L _ h.1] + /-- The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of length `> i`. Version designed to rewrite from the big list to the small list. -/ +@[deprecated getElem_take (since := "2024-06-12")] theorem get_take (L : List α) {i j : Nat} (hi : i < L.length) (hj : i < j) : - get L ⟨i, hi⟩ = get (L.take j) ⟨i, length_take .. ▸ Nat.lt_min.mpr ⟨hj, hi⟩⟩ := - get_of_eq (take_append_drop j L).symm _ ▸ get_append .. + get L ⟨i, hi⟩ = get (L.take j) ⟨i, length_take .. ▸ Nat.lt_min.mpr ⟨hj, hi⟩⟩ := by + simp [getElem_take _ hi hj] /-- The `i`-th element of a list coincides with the `i`-th element of any of its prefixes of length `> i`. Version designed to rewrite from the small list to the big list. -/ +@[deprecated getElem_take (since := "2024-06-12")] theorem get_take' (L : List α) {j i} : get (L.take j) i = get L ⟨i.1, Nat.lt_of_lt_of_le i.2 (length_take_le' _ _)⟩ := by - let ⟨i, hi⟩ := i; rw [length_take, Nat.lt_min] at hi; rw [get_take L _ hi.1] + simp [getElem_take'] theorem getElem?_take {l : List α} {n m : Nat} (h : m < n) : (l.take n)[m]? = l[m]? := by induction n generalizing l m with @@ -118,6 +126,7 @@ theorem getElem?_take {l : List α} {n m : Nat} (h : m < n) : (l.take n)[m]? = l · simp · simpa using hn (Nat.lt_of_succ_lt_succ h) +@[deprecated getElem?_take (since := "2024-06-12")] theorem get?_take {l : List α} {n m : Nat} (h : m < n) : (l.take n).get? m = l.get? m := by simp [getElem?_take, h] @@ -125,6 +134,7 @@ theorem getElem?_take_eq_none {l : List α} {n m : Nat} (h : n ≤ m) : (l.take n)[m]? = none := getElem?_eq_none.mpr <| Nat.le_trans (length_take_le _ _) h +@[deprecated getElem?_take_eq_none (since := "2024-06-12")] theorem get?_take_eq_none {l : List α} {n m : Nat} (h : n ≤ m) : (l.take n).get? m = none := by simp [getElem?_take_eq_none h] @@ -135,13 +145,14 @@ theorem getElem?_take_eq_if {l : List α} {n m : Nat} : · next h => exact getElem?_take h · next h => exact getElem?_take_eq_none (Nat.le_of_not_lt h) +@[deprecated getElem?_take_eq_if (since := "2024-06-12")] theorem get?_take_eq_if {l : List α} {n m : Nat} : (l.take n).get? m = if m < n then l.get? m else none := by simp [getElem?_take_eq_if] @[simp] -theorem nth_take_of_succ {l : List α} {n : Nat} : (l.take (n + 1)).get? n = l.get? n := - get?_take (Nat.lt_succ_self n) +theorem get?_take_of_succ {l : List α} {n : Nat} : (l.take (n + 1))[n]? = l[n]? := + getElem?_take (Nat.lt_succ_self n) theorem take_succ {l : List α} {n : Nat} : l.take (n + 1) = l.take n ++ l[n]?.toList := by induction l generalizing n with @@ -280,6 +291,7 @@ theorem getElem_drop (L : List α) {i j : Nat} (h : i + j < L.length) : /-- The `i + j`-th element of a list coincides with the `j`-th element of the list obtained by dropping the first `i` elements. Version designed to rewrite from the big list to the small list. -/ +@[deprecated getElem_drop (since := "2024-06-12")] theorem get_drop (L : List α) {i j : Nat} (h : i + j < L.length) : get L ⟨i + j, h⟩ = get (L.drop i) ⟨j, lt_length_drop L h⟩ := by simp [getElem_drop] @@ -294,11 +306,12 @@ theorem getElem_drop' (L : List α) {i : Nat} {j : Nat} {h : j < (L.drop i).leng /-- The `i + j`-th element of a list coincides with the `j`-th element of the list obtained by dropping the first `i` elements. Version designed to rewrite from the small list to the big list. -/ +@[deprecated getElem_drop' (since := "2024-06-12")] theorem get_drop' (L : List α) {i j} : get (L.drop i) j = get L ⟨i + j, by rw [Nat.add_comm] exact Nat.add_lt_of_lt_sub (length_drop i L ▸ j.2)⟩ := by - rw [get_drop] + simp [getElem_drop'] @[simp] theorem getElem?_drop (L : List α) (i j : Nat) : (L.drop i)[j]? = L[i + j]? := by @@ -311,6 +324,7 @@ theorem getElem?_drop (L : List α) (i j : Nat) : (L.drop i)[j]? = L[i + j]? := rw [Nat.add_comm] at h apply Nat.lt_sub_of_add_lt h +@[deprecated getElem?_drop (since := "2024-06-12")] theorem get?_drop (L : List α) (i j : Nat) : get? (L.drop i) j = get? L (i + j) := by simp @@ -366,12 +380,21 @@ theorem reverse_take {α} {xs : List α} (n : Nat) (h : n ≤ xs.length) : rfl @[simp] -theorem get_cons_drop : ∀ (l : List α) i, get l i :: drop (i + 1) l = drop i l - | _::_, ⟨0, _⟩ => rfl - | _::_, ⟨i+1, _⟩ => get_cons_drop _ ⟨i, _⟩ +theorem getElem_cons_drop : ∀ (l : List α) (i : Nat) (h : i < l.length), + l[i] :: drop (i + 1) l = drop i l + | _::_, 0, _ => rfl + | _::_, i+1, _ => getElem_cons_drop _ i _ + +@[deprecated getElem_cons_drop (since := "2024-06-12")] +theorem get_cons_drop (l : List α) (i) : get l i :: drop (i + 1) l = drop i l := by + simp + +theorem drop_eq_getElem_cons {n} {l : List α} (h) : drop n l = l[n] :: drop (n + 1) l := + (getElem_cons_drop _ n h).symm -theorem drop_eq_get_cons {n} {l : List α} (h) : drop n l = get l ⟨n, h⟩ :: drop (n + 1) l := - (get_cons_drop _ ⟨n, h⟩).symm +@[deprecated drop_eq_getElem_cons (since := "2024-06-12")] +theorem drop_eq_get_cons {n} {l : List α} (h) : drop n l = get l ⟨n, h⟩ :: drop (n + 1) l := by + simp [drop_eq_getElem_cons] theorem drop_eq_nil_of_eq_nil : ∀ {as : List α} {i}, as = [] → as.drop i = [] | _, _, rfl => drop_nil From 3f7a503ce499f7f6b8d83e2a911e1411ddf0c534 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 13 Jun 2024 18:49:34 +1000 Subject: [PATCH 20/20] Delete versions --- versions | 52 ---------------------------------------------------- 1 file changed, 52 deletions(-) delete mode 100755 versions diff --git a/versions b/versions deleted file mode 100755 index 53373adef643..000000000000 --- a/versions +++ /dev/null @@ -1,52 +0,0 @@ -#!/bin/bash -# Must be run in a copy of the `lean4` repository, and you'll need to login with `gh auth` first. - -check_rate_limit() { - remaining=$(gh api rate_limit | jq '.resources.search.remaining') - if [[ $remaining -le 1 ]]; then - echo "API rate limit exceeded, retrying after a short wait..." - sleep $1 # Wait for the specified time before retrying - return 1 - else - return 0 - fi -} - -perform_search() { - local search_term=$1 - local retries=5 - local wait_time=10 - - for ((i=0; i