chore: cleanup of DList api (#991)

Co-authored-by: F. G. Dorais <fgdorais@gmail.com>

Batteries/Data/DList/Basic.lean

@@ -3,6 +3,8 @@ Copyright (c) 2018 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+import Batteries.Tactic.Alias
+
 namespace Batteries
 /--
 A difference List is a Function that, given a List, returns the original
@@ -16,6 +18,8 @@ structure DList (α : Type u) where
   /-- The `apply` function of a `DList` is completely determined by the list `apply []`. -/
   invariant : ∀ l, apply l = apply [] ++ l
 
+attribute [simp] DList.apply
+
 namespace DList
 variable {α : Type u}
 open List
@@ -30,8 +34,10 @@ def empty : DList α :=
 
 instance : EmptyCollection (DList α) := ⟨DList.empty⟩
 
+instance : Inhabited (DList α) := ⟨DList.empty⟩
+
 /-- `O(apply())`. Convert a `DList α` into a `List α` by running the `apply` function. -/
-def toList : DList α → List α
+@[simp] def toList : DList α → List α
   | ⟨f, _⟩ => f []
 
 /-- `O(1)` (`apply` is `O(1)`). A `DList α` corresponding to the list `[a]`. -/
@@ -70,9 +76,11 @@ def push : DList α → α → DList α
 instance : Append (DList α) := ⟨DList.append⟩
 
 /-- Convert a lazily-evaluated `List` to a `DList` -/
-def lazy_ofList (l : Thunk (List α)) : DList α :=
+def ofThunk (l : Thunk (List α)) : DList α :=
   ⟨fun xs => l.get ++ xs, fun t => by simp⟩
 
+@[deprecated (since := "2024-10-16")] alias lazy_ofList := ofThunk
+
 /-- Concatenates a list of difference lists to form a single difference list. Similar to
 `List.join`. -/
 def join {α : Type _} : List (DList α) → DList α

Batteries/Data/DList/Lemmas.lean

@@ -18,46 +18,41 @@ This structure supports `O(1)` `append` and `push` operations on lists, making i
 useful for append-heavy uses such as logging and pretty printing.
 -/
 
-universe u
-
 namespace Batteries.DList
 
 open Function
 
-variable {α : Type u}
-
-attribute [local simp] Function.comp
-
-attribute [local simp] ofList toList empty singleton cons push append
-
 theorem toList_ofList (l : List α) : DList.toList (DList.ofList l) = l := by
-  cases l; rfl; simp only [DList.toList, DList.ofList, List.cons_append, List.append_nil]
+  cases l; rfl; simp [ofList]
 
 theorem ofList_toList (l : DList α) : DList.ofList (DList.toList l) = l := by
    obtain ⟨app, inv⟩ := l
    simp only [ofList, toList, mk.injEq]
    funext x
    rw [(inv x)]
 
-theorem toList_empty : toList (@empty α) = [] := by simp
+theorem toList_empty : toList (@empty α) = [] := by simp [empty]
 
-theorem toList_singleton (x : α) : toList (singleton x) = [x] := by simp
+theorem toList_singleton (x : α) : toList (singleton x) = [x] := by simp [singleton]
 
 theorem toList_append (l₁ l₂ : DList α) : toList (l₁ ++ l₂) = toList l₁ ++ toList l₂ := by
-  obtain ⟨_, l₁_invariant⟩ := l₁; cases l₂; simp; rw [l₁_invariant]
+  simp only [toList, append, Function.comp]; rw [invariant]
 
 theorem toList_cons (x : α) (l : DList α) : toList (cons x l) = x :: toList l := by
-  cases l; simp
+  cases l; simp [cons]
 
 theorem toList_push (x : α) (l : DList α) : toList (push l x) = toList l ++ [x] := by
-  obtain ⟨_, l_invariant⟩ := l; simp; rw [l_invariant]
+  simp only [toList, push]; rw [invariant]
 
 @[simp]
-theorem DList_singleton {α : Type _} {a : α} : singleton a = lazy_ofList [a] :=
+theorem singleton_eq_ofThunk {α : Type _} {a : α} : singleton a = ofThunk [a] :=
   rfl
 
 @[simp]
-theorem DList_lazy {α : Type _} {l : List α} : lazy_ofList l = ofList l :=
+theorem ofThunk_coe {α : Type _} {l : List α} : ofThunk l = ofList l :=
   rfl
 
+@[deprecated (since := "2024-10-16")] alias DList_singleton := singleton_eq_ofThunk
+@[deprecated (since := "2024-10-16")] alias DList_lazy := ofThunk_coe
+
 end Batteries.DList