diff --git a/Batteries.lean b/Batteries.lean index 1efcac66e7..e08a94afb1 100644 --- a/Batteries.lean +++ b/Batteries.lean @@ -94,7 +94,6 @@ import Batteries.Tactic.ShowUnused import Batteries.Tactic.SqueezeScope import Batteries.Tactic.Trans import Batteries.Tactic.Unreachable -import Batteries.Tactic.Where import Batteries.Util.Cache import Batteries.Util.ExtendedBinder import Batteries.Util.LibraryNote diff --git a/Batteries/Data/Array/Lemmas.lean b/Batteries/Data/Array/Lemmas.lean index 9bfa7c43d0..50a541131f 100644 --- a/Batteries/Data/Array/Lemmas.lean +++ b/Batteries/Data/Array/Lemmas.lean @@ -49,7 +49,7 @@ where ((l.toList.drop i).indexOf? a).map (·+i) = (indexOfAux l a i).map Fin.val := by rw [indexOfAux] if h : i < l.size then - rw [List.drop_eq_getElem_cons h, ←getElem_eq_getElem_toList, List.indexOf?_cons] + rw [List.drop_eq_getElem_cons h, getElem_toList, List.indexOf?_cons] if h' : l[i] == a then simp [h, h'] else @@ -76,8 +76,6 @@ theorem size_set! (a : Array α) (i v) : (a.set! i v).size = a.size := by simp /-! ### mem -/ -theorem mem_singleton : a ∈ #[b] ↔ a = b := by simp - /-! ### insertAt -/ @[simp] private theorem size_insertIdx_loop (as : Array α) (i : Nat) (j : Fin as.size) : diff --git a/Batteries/Data/Char.lean b/Batteries/Data/Char.lean index 4f3c59ef0b..a283599237 100644 --- a/Batteries/Data/Char.lean +++ b/Batteries/Data/Char.lean @@ -9,9 +9,6 @@ import Batteries.Tactic.Alias theorem Char.le_antisymm_iff {x y : Char} : x = y ↔ x ≤ y ∧ y ≤ x := Char.ext_iff.trans UInt32.le_antisymm_iff -theorem Char.le_antisymm {x y : Char} (h1 : x ≤ y) (h2 : y ≤ x) : x = y := - Char.le_antisymm_iff.2 ⟨h1, h2⟩ - instance : Batteries.LawfulOrd Char := .compareOfLessAndEq (fun _ => Nat.lt_irrefl _) Nat.lt_trans Nat.not_lt Char.le_antisymm diff --git a/Batteries/Data/HashMap/WF.lean b/Batteries/Data/HashMap/WF.lean index aa33711633..af33401646 100644 --- a/Batteries/Data/HashMap/WF.lean +++ b/Batteries/Data/HashMap/WF.lean @@ -26,7 +26,7 @@ theorem toList_update (self : Buckets α β) (i d h) : theorem exists_of_update (self : Buckets α β) (i d h) : ∃ l₁ l₂, self.1.toList = l₁ ++ self.1[i] :: l₂ ∧ List.length l₁ = i.toNat ∧ (self.update i d h).1.toList = l₁ ++ d :: l₂ := by - simp only [Array.length_toList, Array.ugetElem_eq_getElem, Array.getElem_eq_getElem_toList] + simp only [Array.length_toList, Array.ugetElem_eq_getElem, Array.getElem_toList] exact List.exists_of_set h theorem update_update (self : Buckets α β) (i d d' h h') : @@ -46,7 +46,7 @@ theorem WF.mk' [BEq α] [Hashable α] (h) : (Buckets.mk n h : Buckets α β).WF refine ⟨fun _ h => ?_, fun i h => ?_⟩ · simp only [Buckets.mk, mkArray, List.mem_replicate, ne_eq] at h simp [h, List.Pairwise.nil] - · simp [Buckets.mk, empty', mkArray, Array.getElem_eq_getElem_toList, AssocList.All] + · simp [Buckets.mk, empty', Array.getElem_toList, AssocList.All] theorem WF.update [BEq α] [Hashable α] {buckets : Buckets α β} {i d h} (H : buckets.WF) (h₁ : ∀ [PartialEquivBEq α] [LawfulHashable α], @@ -60,7 +60,7 @@ theorem WF.update [BEq α] [Hashable α] {buckets : Buckets α β} {i d h} (H : | .inl hl => H.1 _ hl | .inr rfl => h₁ (H.1 _ (Array.getElem_mem_toList ..)) · revert hp - simp only [Array.getElem_eq_getElem_toList, toList_update, List.getElem_set, + simp only [← Array.getElem_toList, toList_update, List.getElem_set, Array.length_toList, update_size] split <;> intro hp · next eq => exact eq ▸ h₂ (H.2 _ _) _ hp @@ -110,7 +110,7 @@ where List.length_nil, Nat.sum_append, List.sum_cons, Nat.zero_add, Array.length_toList] rw [Nat.add_assoc, Nat.add_assoc, Nat.add_assoc]; congr 1 (conv => rhs; rw [Nat.add_left_comm]); congr 1 - rw [← Array.getElem_eq_getElem_toList] + rw [Array.getElem_toList] have := @reinsertAux_size α β _; simp [Buckets.size] at this induction source[i].toList generalizing target <;> simp [*, Nat.succ_add]; rfl · next H => @@ -173,7 +173,7 @@ where · match List.mem_or_eq_of_mem_set hl with | .inl hl => exact hs₁ _ hl | .inr e => exact e ▸ .nil - · simp only [Array.length_toList, Array.size_set, Array.getElem_eq_getElem_toList, + · simp only [Array.length_toList, Array.size_set, ← Array.getElem_toList, Array.toList_set, List.getElem_set] split · nofun @@ -371,7 +371,7 @@ theorem WF.filterMap {α β γ} {f : α → β → Option γ} [BEq α] [Hashable have := H.out.2.1 _ h rw [← List.pairwise_map (R := (¬ · == ·))] at this ⊢ exact this.sublist (H3 l.toList) - · simp only [Array.size_mk, List.length_map, Array.length_toList, Array.getElem_eq_getElem_toList, + · simp only [Array.size_toArray, List.length_map, Array.length_toList, ← Array.getElem_toList, List.getElem_map] at h ⊢ have := H.out.2.2 _ h simp only [AssocList.All, List.toList_toAssocList, List.mem_reverse, List.mem_filterMap, diff --git a/Batteries/Data/PairingHeap.lean b/Batteries/Data/PairingHeap.lean index e1263fca0e..658af68055 100644 --- a/Batteries/Data/PairingHeap.lean +++ b/Batteries/Data/PairingHeap.lean @@ -123,7 +123,7 @@ theorem Heap.size_merge_node (le) (a₁ : α) (c₁ s₁ : Heap α) (a₂ : α) theorem Heap.size_merge (le) {s₁ s₂ : Heap α} (h₁ : s₁.NoSibling) (h₂ : s₂.NoSibling) : (merge le s₁ s₂).size = s₁.size + s₂.size := by match h₁, h₂ with - | .nil, .nil | .nil, .node _ _ | .node _ _, .nil => simp [size] + | .nil, .nil | .nil, .node _ _ | .node _ _, .nil => simp [merge, size] | .node _ _, .node _ _ => unfold merge; dsimp; split <;> simp_arith [size] theorem Heap.size_combine (le) (s : Heap α) : diff --git a/Batteries/Data/Range/Lemmas.lean b/Batteries/Data/Range/Lemmas.lean index 3fd893daa9..0fe11aacce 100644 --- a/Batteries/Data/Range/Lemmas.lean +++ b/Batteries/Data/Range/Lemmas.lean @@ -8,100 +8,24 @@ import Batteries.Data.List.Lemmas namespace Std.Range -/-- The number of elements contained in a `Std.Range`. -/ -def numElems (r : Range) : Nat := - if r.step = 0 then - -- This is a very weird choice, but it is chosen to coincide with the `forIn` impl - if r.stop ≤ r.start then 0 else r.stop - else - (r.stop - r.start + r.step - 1) / r.step +@[deprecated size (since := "2024-12-19")] alias numElems := size -theorem numElems_stop_le_start : ∀ r : Range, r.stop ≤ r.start → r.numElems = 0 - | ⟨start, stop, step⟩, h => by - simp [numElems]; split <;> simp_all - apply Nat.div_eq_of_lt; simp [Nat.sub_eq_zero_of_le h] - exact Nat.pred_lt ‹_› +theorem size_stop_le_start : ∀ r : Range, r.stop ≤ r.start → r.size = 0 + | ⟨start, stop, step, _⟩, h => by + simp_all [size, Nat.div_eq_zero_iff_lt] + omega -theorem numElems_step_1 (start stop) : numElems ⟨start, stop, 1⟩ = stop - start := by - simp [numElems] +@[deprecated size_stop_le_start (since := "2024-12-19")] +alias numElems_stop_le_start := size_stop_le_start -private theorem numElems_le_iff {start stop step i} (hstep : 0 < step) : - (stop - start + step - 1) / step ≤ i ↔ stop ≤ start + step * i := - calc (stop - start + step - 1) / step ≤ i - _ ↔ stop - start + step - 1 < step * i + step := by - rw [← Nat.lt_succ (n := i), Nat.div_lt_iff_lt_mul hstep, Nat.mul_comm, ← Nat.mul_succ] - _ ↔ stop - start + step - 1 < step * i + 1 + (step - 1) := by - rw [Nat.add_right_comm, Nat.add_assoc, Nat.sub_add_cancel hstep] - _ ↔ stop ≤ start + step * i := by - rw [Nat.add_sub_assoc hstep, Nat.add_lt_add_iff_right, Nat.lt_succ, - Nat.sub_le_iff_le_add'] +theorem size_step_1 (start stop) : size ⟨start, stop, 1, by decide⟩ = stop - start := by + simp [size] -theorem mem_range'_elems (r : Range) (h : x ∈ List.range' r.start r.numElems r.step) : x ∈ r := by - obtain ⟨i, h', rfl⟩ := List.mem_range'.1 h - refine ⟨Nat.le_add_right .., ?_⟩ - unfold numElems at h'; split at h' - · split at h' <;> [cases h'; simp_all] - · next step0 => - refine Nat.not_le.1 fun h => - Nat.not_le.2 h' <| (numElems_le_iff (Nat.pos_of_ne_zero step0)).2 h +@[deprecated size_step_1 (since := "2024-12-19")] +alias numElems_step_1 := size_step_1 -theorem forIn'_eq_forIn_range' [Monad m] (r : Std.Range) - (init : β) (f : (a : Nat) → a ∈ r → β → m (ForInStep β)) : - forIn' r init f = - forIn - ((List.range' r.start r.numElems r.step).pmap Subtype.mk fun _ => mem_range'_elems r) - init (fun ⟨a, h⟩ => f a h) := by - let ⟨start, stop, step⟩ := r - let L := List.range' start (numElems ⟨start, stop, step⟩) step - let f' : { a // start ≤ a ∧ a < stop } → _ := fun ⟨a, h⟩ => f a h - suffices ∀ H, forIn' [start:stop:step] init f = forIn (L.pmap Subtype.mk H) init f' from this _ - intro H; dsimp only [forIn', Range.forIn'] - if h : start < stop then - simp only [numElems, Nat.not_le.2 h, ↓reduceIte, L]; split - · subst step - suffices ∀ n H init, - forIn'.loop start stop 0 f n start (Nat.le_refl _) init = - forIn ((List.range' start n 0).pmap Subtype.mk H) init f' from this _ .. - intro n; induction n with - (intro H init - unfold forIn'.loop - simp only [↓reduceDIte, Nat.add_zero, List.pmap, List.forIn_cons, List.forIn_nil, h]) - | succ n ih => simp [ih (List.forall_mem_cons.1 H).2]; rfl - · next step0 => - have hstep := Nat.pos_of_ne_zero step0 - suffices ∀ fuel l i hle H, l ≤ fuel → - (∀ j, stop ≤ i + step * j ↔ l ≤ j) → ∀ init, - forIn'.loop start stop step f fuel i hle init = - forIn ((List.range' i l step).pmap Subtype.mk H) init f' by - refine this _ _ _ _ _ - ((numElems_le_iff hstep).2 (Nat.le_trans ?_ (Nat.le_add_left ..))) - (fun _ => (numElems_le_iff hstep).symm) _ - conv => lhs; rw [← Nat.one_mul stop] - exact Nat.mul_le_mul_right stop hstep - intro fuel; induction fuel with intro l i hle H h1 h2 init - | zero => simp [forIn'.loop, Nat.le_zero.1 h1] - | succ fuel ih => - cases l with - | zero => rw [forIn'.loop]; simp [Nat.not_lt.2 <| by simpa using (h2 0).2 (Nat.le_refl _)] - | succ l => - have ih := ih _ _ (Nat.le_trans hle (Nat.le_add_right ..)) - (List.forall_mem_cons.1 H).2 (Nat.le_of_succ_le_succ h1) fun i => by - rw [Nat.add_right_comm, Nat.add_assoc, ← Nat.mul_succ, h2, Nat.succ_le_succ_iff] - have := h2 0 - simp only [Nat.mul_zero, Nat.add_zero, Nat.le_zero_eq, Nat.add_one_ne_zero, iff_false, - Nat.not_le] at this - rw [forIn'.loop] - simp only [this, ↓reduceDIte, ih, List.pmap, List.forIn_cons] - rfl - else - simp only [numElems_stop_le_start ⟨start, stop, step⟩ (Nat.not_lt.1 h), List.range'_zero, - List.pmap, List.forIn_nil, L] - cases stop <;> unfold forIn'.loop <;> simp [List.forIn', h] +@[deprecated mem_of_mem_range' (since := "2024-12-19")] +alias mem_range'_elems := mem_of_mem_range' -theorem forIn_eq_forIn_range' [Monad m] (r : Std.Range) - (init : β) (f : Nat → β → m (ForInStep β)) : - forIn r init f = forIn (List.range' r.start r.numElems r.step) init f := by - refine Eq.trans ?_ <| (forIn'_eq_forIn_range' r init (fun x _ => f x)).trans ?_ - · simp [forIn, forIn'] - · suffices ∀ L H, forIn (List.pmap Subtype.mk L H) init (f ·.1) = forIn L init f from this _ .. - intro L; induction L generalizing init <;> intro H <;> simp [*] +@[deprecated forIn'_eq_forIn'_range' (since := "2024-12-19")] +alias forIn'_eq_forIn_range' := forIn'_eq_forIn'_range' diff --git a/Batteries/Data/String/Lemmas.lean b/Batteries/Data/String/Lemmas.lean index 642029cdd1..a94944dffd 100644 --- a/Batteries/Data/String/Lemmas.lean +++ b/Batteries/Data/String/Lemmas.lean @@ -14,13 +14,9 @@ namespace String -- TODO(kmill): add `@[ext]` attribute to `String.ext` in core. attribute [ext (iff := false)] ext -theorem lt_trans {s₁ s₂ s₃ : String} : s₁ < s₂ → s₂ < s₃ → s₁ < s₃ := - List.lt_trans (α := Char) Nat.lt_trans - (fun h1 h2 => Nat.not_lt.2 <| Nat.le_trans (Nat.not_lt.1 h2) (Nat.not_lt.1 h1)) - -theorem lt_antisymm {s₁ s₂ : String} (h₁ : ¬s₁ < s₂) (h₂ : ¬s₂ < s₁) : s₁ = s₂ := - ext <| List.lt_antisymm (α := Char) - (fun h1 h2 => Char.le_antisymm (Nat.not_lt.1 h2) (Nat.not_lt.1 h1)) h₁ h₂ +theorem lt_antisymm {s₁ s₂ : String} (h₁ : ¬s₁ < s₂) (h₂ : ¬s₂ < s₁) : s₁ = s₂ := by + simp at h₁ h₂ + exact String.le_antisymm h₂ h₁ instance : Batteries.TransOrd String := .compareOfLessAndEq String.lt_irrefl String.lt_trans String.lt_antisymm @@ -153,7 +149,7 @@ theorem utf8GetAux_of_valid (cs cs' : List Char) {i p : Nat} (hp : i + utf8Len c | [], [] => rfl | [], c::cs' => simp [← hp, utf8GetAux] | c::cs, cs' => - simp only [utf8GetAux, List.append_eq, Char.reduceDefault, ↓Char.isValue] + simp only [List.cons_append, utf8GetAux, Char.reduceDefault] rw [if_neg] case hnc => simp only [← hp, utf8Len_cons, Pos.ext_iff]; exact ne_self_add_add_utf8Size refine utf8GetAux_of_valid cs cs' ?_ @@ -172,7 +168,7 @@ theorem utf8GetAux?_of_valid (cs cs' : List Char) {i p : Nat} (hp : i + utf8Len | [], [] => rfl | [], c::cs' => simp [← hp, utf8GetAux?] | c::cs, cs' => - simp only [utf8GetAux?, List.append_eq] + simp only [List.cons_append, utf8GetAux?] rw [if_neg] case hnc => simp only [← hp, Pos.ext_iff]; exact ne_self_add_add_utf8Size refine utf8GetAux?_of_valid cs cs' ?_ @@ -224,7 +220,7 @@ theorem utf8PrevAux_of_valid {cs cs' : List Char} {c : Char} {i p : Nat} match cs with | [] => simp [utf8PrevAux, ← hp, Pos.addChar_eq] | c'::cs => - simp only [utf8PrevAux, Pos.addChar_eq, ← hp, utf8Len_cons, List.append_eq] + simp only [utf8PrevAux, List.cons_append, utf8Len_cons, ← hp] rw [if_neg] case hnc => simp only [Pos.ext_iff] @@ -361,7 +357,7 @@ theorem extract.go₂_append_left : ∀ (s t : List Char) (i e : Nat), e = utf8Len s + i → go₂ (s ++ t) ⟨i⟩ ⟨e⟩ = s | [], t, i, _, rfl => by cases t <;> simp [go₂] | c :: cs, t, i, _, rfl => by - simp only [go₂, utf8Len_cons, Pos.ext_iff, ne_add_utf8Size_add_self, ↓reduceIte, List.append_eq, + simp only [List.cons_append, utf8Len_cons, go₂, Pos.ext_iff, ne_add_utf8Size_add_self, ↓reduceIte, Pos.addChar_eq, List.cons.injEq, true_and] apply go₂_append_left; rw [Nat.add_right_comm, Nat.add_assoc] @@ -388,7 +384,7 @@ theorem extract.go₁_append_right : ∀ (s t : List Char) (i b : Nat) (e : Pos) b = utf8Len s + i → go₁ (s ++ t) ⟨i⟩ ⟨b⟩ e = go₂ t ⟨b⟩ e | [], t, i, _, e, rfl => by cases t <;> simp [go₁, go₂] | c :: cs, t, i, _, e, rfl => by - simp only [go₁, utf8Len_cons, Pos.ext_iff, ne_add_utf8Size_add_self, ↓reduceIte, List.append_eq, + simp only [go₁, utf8Len_cons, Pos.ext_iff, ne_add_utf8Size_add_self, ↓reduceIte, List.cons_append, Pos.addChar_eq] apply go₁_append_right; rw [Nat.add_right_comm, Nat.add_assoc] diff --git a/Batteries/Data/UnionFind/Basic.lean b/Batteries/Data/UnionFind/Basic.lean index 3328834ec2..fc093a0f16 100644 --- a/Batteries/Data/UnionFind/Basic.lean +++ b/Batteries/Data/UnionFind/Basic.lean @@ -296,7 +296,6 @@ theorem findAux_s {self : UnionFind} {x : Fin self.size} : apply dif_pos exact parent'_lt .. -set_option linter.deprecated false in theorem rankD_findAux {self : UnionFind} {x : Fin self.size} : rankD (findAux self x).s i = self.rank i := by if h : i < self.size then @@ -307,11 +306,10 @@ theorem rankD_findAux {self : UnionFind} {x : Fin self.size} : split <;> simp [← rankD_eq, rankD_findAux (x := ⟨_, self.parent'_lt _ x.2⟩), -Array.get_eq_getElem] else - simp only [rankD, Array.data_length, Array.get_eq_getElem, rank] + simp only [rankD, Array.length_toList, Array.get_eq_getElem, rank] rw [dif_neg (by rwa [FindAux.size_eq]), dif_neg h] termination_by self.rankMax - self.rank x -set_option linter.deprecated false in theorem parentD_findAux {self : UnionFind} {x : Fin self.size} : parentD (findAux self x).s i = if i = x then self.rootD x else parentD (self.findAux ⟨_, self.parent'_lt _ x.2⟩).s i := by @@ -321,7 +319,7 @@ theorem parentD_findAux {self : UnionFind} {x : Fin self.size} : · next h => rw [parentD]; split <;> rename_i h' · rw [Array.getElem_modify (by simpa using h')] - simp only [Array.data_length, @eq_comm _ i] + simp only [Array.length_toList, @eq_comm _ i] split <;> simp [← parentD_eq, -Array.get_eq_getElem] · rw [if_neg (mt (by rintro rfl; simp [FindAux.size_eq]) h')] rw [parentD, dif_neg]; simpa using h' diff --git a/Batteries/Tactic/Where.lean b/Batteries/Tactic/Where.lean deleted file mode 100644 index 3ef51a46c9..0000000000 --- a/Batteries/Tactic/Where.lean +++ /dev/null @@ -1,83 +0,0 @@ -/- -Copyright (c) 2023 Kyle Miller. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. -Authors: Kyle Miller --/ -import Lean.Elab.Command - -/-! # `#where` command - -The `#where` command prints information about the current location, including the namespace, -active `open`, `universe`, and `variable` commands, and any options set with `set_option`. --/ - -open Lean Elab Command - -namespace Batteries.Tactic.Where - -private def describeOpenDecls (ds : List OpenDecl) : MessageData := Id.run do - let mut lines := #[] - let mut simple := #[] - let flush (lines simple : Array MessageData) : Array MessageData × Array MessageData := - if simple.isEmpty then - (lines, simple) - else - (lines.push ("open " ++ MessageData.joinSep simple.toList " "), #[]) - for d in ds do - match d with - | .explicit id decl => - (lines, simple) := flush lines simple - lines := lines.push m!"open {id} → {decl}" - | .simple ns ex => - if ex == [] then - simple := simple.push ns - else - (lines, simple) := flush lines simple - let ex' := ex.map toMessageData - lines := lines.push m!"open {ns} hiding {MessageData.joinSep ex' ", "}" - (lines, _) := flush lines simple - return MessageData.joinSep lines.toList "\n" - -private def describeOptions (opts : Options) : CommandElabM (Option MessageData) := do - let mut lines := #[] - let decls ← getOptionDecls - for (name, val) in opts do - match decls.find? name with - | some decl => - if val != decl.defValue then - lines := lines.push m!"set_option {name} {val}" - | none => - lines := lines.push m!"-- set_option {name} {val} -- unknown" - if lines.isEmpty then - return none - else - return MessageData.joinSep lines.toList "\n" - -/-- `#where` gives a description of the global scope at this point in the module. -This includes the namespace, `open` namespaces, `universe` and `variable` commands, -and options set with `set_option`. -/ -elab "#where" : command => do - let scope ← getScope - let mut msg : Array MessageData := #[] - -- Noncomputable - if scope.isNoncomputable then - msg := msg.push m!"noncomputable section" - -- Namespace - if !scope.currNamespace.isAnonymous then - msg := msg.push m!"namespace {scope.currNamespace}" - -- Open namespaces - if !scope.openDecls.isEmpty then - msg := msg.push <| describeOpenDecls scope.openDecls.reverse - -- Universe levels - if !scope.levelNames.isEmpty then - let levels := scope.levelNames.reverse.map toMessageData - msg := msg.push <| "universe " ++ MessageData.joinSep levels " " - -- Variables - if !scope.varDecls.isEmpty then - msg := msg.push <| ← `(command| variable $scope.varDecls*) - -- Options - if let some m ← describeOptions scope.opts then - msg := msg.push m - if msg.isEmpty then - msg := #[m!"-- In root namespace with initial scope"] - logInfo <| m!"{MessageData.joinSep msg.toList "\n\n"}" diff --git a/BatteriesTest/where.lean b/BatteriesTest/where.lean index a88f1ed8e5..eb715d6ad6 100644 --- a/BatteriesTest/where.lean +++ b/BatteriesTest/where.lean @@ -1,4 +1,7 @@ -import Batteries.Tactic.Where +-- None of these imports are really necessary, except to create namespace mentioned below. +import Lean.Elab.Term +import Lean.Elab.Command +import Batteries.Data.UnionFind.Basic -- Return to pristine state set_option linter.missingDocs false @@ -68,6 +71,6 @@ open Array renaming map -> listMap info: open Lean Lean.Meta open Lean.Elab hiding TermElabM open Lean.Elab.Command Batteries -open listMap → Array.map +open Array renaming map → listMap -/ #guard_msgs in #where