cleanup

src/Std/Data/DHashMap/Internal/List/Associative.lean

@@ -6,7 +6,8 @@ Authors: Markus Himmel
 prelude
 import Init.Data.BEq
 import Init.Data.Nat.Simproc
-import Std.Data.DHashMap.Internal.List.Pairwise
+import Init.Data.List.Perm
+import Std.Data.DHashMap.Internal.List.Defs
 
 /-!
 This is an internal implementation file of the hash map. Users of the hash map should not rely on
@@ -22,7 +23,7 @@ universe u v w
 
 variable {α : Type u} {β : α → Type v} {γ : α → Type w}
 
-open List (Perm)
+open List (Perm Sublist pairwise_cons erase_sublist filter_sublist)
 
 namespace Std.DHashMap.Internal.List
 
@@ -689,7 +690,7 @@ theorem sublist_eraseKey [BEq α] {l : List ((a : α) × β a)} {k : α} :
     rw [eraseKey_cons]
     cases k' == k
     · simpa
-    · simpa using Sublist.cons_right Sublist.refl
+    · simp
 
 theorem length_eraseKey [BEq α] {l : List ((a : α) × β a)} {k : α} :
     (eraseKey k l).length = if containsKey k l then l.length - 1 else l.length := by
@@ -753,7 +754,7 @@ open List
 
 theorem DistinctKeys.perm_keys [BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)}
     (h : Perm (keys l') (keys l)) : DistinctKeys l → DistinctKeys l'
-  | ⟨h'⟩ => ⟨h'.perm BEq.symm_false h.symm⟩
+  | ⟨h'⟩ => ⟨h'.perm h.symm BEq.symm_false⟩
 
 theorem DistinctKeys.perm [BEq α] [PartialEquivBEq α] {l l' : List ((a : α) × β a)}
     (h : Perm l' l) : DistinctKeys l → DistinctKeys l' :=
@@ -773,7 +774,7 @@ theorem distinctKeys_of_sublist [BEq α] {l l' : List ((a : α) × β a)} (h : S
 
 theorem DistinctKeys.of_keys_eq [BEq α] {l : List ((a : α) × β a)} {l' : List ((a : α) × γ a)}
     (h : keys l = keys l') : DistinctKeys l → DistinctKeys l' :=
-  distinctKeys_of_sublist_keys (h ▸ Sublist.refl)
+  distinctKeys_of_sublist_keys (h ▸ Sublist.refl _)
 
 theorem containsKey_iff_exists [BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a : α} :
     containsKey a l ↔ ∃ a' ∈ keys l, a == a' := by

src/Std/Data/DHashMap/Internal/List/Defs.lean

@@ -20,12 +20,9 @@ universe u v w
 
 variable {α : Type u} {β : α → Type v} {γ : α → Type w}
 
-namespace Std.DHashMap.Internal.List
+open List (Pairwise)
 
-/-- Internal implementation detail of the hash map -/
-def Pairwise (P : α → α → Prop) : List α → Prop
-| [] => True
-| (x::xs) => (∀ y ∈ xs, P x y) ∧ Pairwise P xs
+namespace Std.DHashMap.Internal.List
 
 /-- Internal implementation detail of the hash map -/
 def keys : List ((a : α) × β a) → List α

src/Std/Data/DHashMap/Internal/List/Pairwise.lean

@@ -1,64 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
--/
-prelude
-import Init.Data.List.Perm
-import Std.Data.DHashMap.Internal.List.Defs
-import Std.Data.DHashMap.Internal.List.Sublist
-
-/-!
-This is an internal implementation file of the hash map. Users of the hash map should not rely on
-the contents of this file.
-
-File contents: tiny private implementation of `List.Pairwise`
--/
-
-set_option linter.missingDocs true
-set_option autoImplicit false
-
-open List (Perm)
-
-namespace Std.DHashMap.Internal.List
-
-
-universe u
-
-variable {α : Type u}
-
-@[simp]
-theorem Pairwise.nil {P : α → α → Prop} : Pairwise P [] :=
-  trivial
-
-theorem Pairwise.perm {P : α → α → Prop} (hP : ∀ {x y}, P x y → P y x) {l l' : List α}
-    (h : Perm l l') : Pairwise P l → Pairwise P l' := by
-  induction h
-  · exact id
-  · next l₁ l₂ a h ih => exact fun hx => ⟨fun y hy => hx.1 _ (h.mem_iff.2 hy), ih hx.2⟩
-  · next l₁ a a' =>
-    intro ⟨hx₁, hx₂, hx⟩
-    refine ⟨?_, ?_, hx⟩
-    · intro y hy
-      rcases List.mem_cons.1 hy with rfl|hy
-      · exact hP (hx₁ _ (List.mem_cons_self _ _))
-      · exact hx₂ _ hy
-    · exact fun y hy => hx₁ _ (List.mem_cons_of_mem _ hy)
-  · next ih₁ ih₂ => exact ih₂ ∘ ih₁
-
-theorem Pairwise.sublist {P : α → α → Prop} {l l' : List α} (h : Sublist l l') :
-    Pairwise P l' → Pairwise P l := by
-  induction h
-  · exact id
-  · next a l₁ l₂ h ih =>
-    intro ⟨hx₁, hx⟩
-    exact ⟨fun y hy => hx₁ _ (h.mem hy), ih hx⟩
-  · next a l₁ l₂ _ ih =>
-    intro ⟨_, hx⟩
-    exact ih hx
-
-theorem pairwise_cons {P : α → α → Prop} {a : α} {l : List α} :
-    Pairwise P (a::l) ↔ (∀ y ∈ l, P a y) ∧ Pairwise P l :=
-  Iff.rfl
-
-end Std.DHashMap.Internal.List

src/Std/Data/DHashMap/Internal/List/Sublist.lean

@@ -1,97 +0,0 @@
-/-
-Copyright (c) 2024 Lean FRO, LLC. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Markus Himmel
--/
-prelude
-import Init.Omega
-
-/-!
-This is an internal implementation file of the hash map. Users of the hash map should not rely on
-the contents of this file.
-
-File contents: tiny private implementation of `List.Sublist`
--/
-
-set_option linter.missingDocs true
-set_option autoImplicit false
-
-universe u v
-
-variable {α : Type u} {β : Type v}
-
-namespace Std.DHashMap.Internal.List
-
-/-- Internal implementation detail of the hash map -/
-inductive Sublist : List α → List α → Prop where
-  /-- Internal implementation detail of the hash map -/
-  | refl {l} : Sublist l l
-  /-- Internal implementation detail of the hash map -/
-  | cons {a} {l l'} : Sublist l l' → Sublist (a::l) (a::l')
-    /-- Internal implementation detail of the hash map -/
-  | cons_right {a} {l l'} : Sublist l l' → Sublist l (a::l')
-
-@[simp]
-theorem sublist_nil {l : List α} : Sublist [] l := by
-  induction l
-  · exact .refl
-  · exact .cons_right ‹_›
-
-theorem Sublist.length_le {l₁ l₂ : List α} (h : Sublist l₁ l₂) : l₁.length ≤ l₂.length := by
-  induction h <;> simp_all <;> omega
-
-theorem Sublist.of_cons_left {l₁ l₂ : List α} {a : α} (h : Sublist (a::l₁) l₂) : Sublist l₁ l₂ := by
-  cases h
-  · exact .cons_right .refl
-  · exact .cons_right ‹_›
-  · next h t ih => exact .cons_right (Sublist.of_cons_left ‹_›)
-
-@[simp]
-theorem Sublist.cons_iff {a : α} {l₁ l₂ : List α} : Sublist (a::l₁) (a::l₂) ↔ Sublist l₁ l₂ := by
-  refine ⟨fun h => ?_, .cons⟩
-  cases h
-  · exact .refl
-  · exact ‹_›
-  · next h =>
-    cases l₂
-    · simpa using h.length_le
-    · next b t => exact Sublist.of_cons_left h
-
-theorem Sublist.map (f : α → β) {l₁ l₂ : List α} (h : Sublist l₁ l₂) :
-    Sublist (l₁.map f) (l₂.map f) := by
-  induction h
-  · exact .refl
-  · exact .cons ‹_›
-  · exact .cons_right ‹_›
-
-theorem Sublist.mem {l₁ l₂ : List α} (h : Sublist l₁ l₂) {a : α} : a ∈ l₁ → a ∈ l₂ := by
-  induction h
-  · exact id
-  · next ih =>
-    simp only [List.mem_cons]
-    rintro (ha|ha)
-    · exact Or.inl ha
-    · exact Or.inr (ih ha)
-  · next ih =>
-    simp only [List.mem_cons]
-    exact fun ha => Or.inr (ih ha)
-
-theorem erase_sublist [BEq α] (l : List α) (a : α) : Sublist (l.erase a) l := by
-  induction l
-  · simp
-  · next h t ih =>
-    simp only [List.erase_cons]
-    split
-    · exact .cons_right .refl
-    · exact .cons ih
-
-theorem filter_sublist (l : List α) {f : α → Bool} : Sublist (l.filter f) l := by
-  induction l
-  · simp
-  · next h t ih =>
-    simp only [List.filter_cons]
-    split
-    · exact .cons ih
-    · exact .cons_right ih
-
-end Std.DHashMap.Internal.List