From 154385fdb9261e5a38d34840aa1c17dfc3a6dc56 Mon Sep 17 00:00:00 2001
From: Kim Morrison <scott.morrison@gmail.com>
Date: Wed, 14 Aug 2024 14:59:20 +1000
Subject: [PATCH] chore: remove dead code in Lake.Util.Compare (#5030)

While exploring refactors of `List.lt` I ran into errors here, in code
that is entirely unused. Propose cleaning up to get things out of my
way!
---
 src/lake/Lake/Util/Compare.lean | 59 ---------------------------------
 src/lake/Lake/Util/Name.lean    |  1 -
 2 files changed, 60 deletions(-)

diff --git a/src/lake/Lake/Util/Compare.lean b/src/lake/Lake/Util/Compare.lean
index d0fab1a62a..0b80c774cd 100644
--- a/src/lake/Lake/Util/Compare.lean
+++ b/src/lake/Lake/Util/Compare.lean
@@ -38,14 +38,9 @@ class EqOfCmpWrt (α : Type u) {β : Type v} (f : α → β) (cmp : α → α 
 
 export EqOfCmpWrt (eq_of_cmp_wrt)
 
-instance : EqOfCmpWrt α (fun _ => α) cmp := ⟨fun _ => rfl⟩
-
 instance [EqOfCmp α cmp] : EqOfCmpWrt α f cmp where
   eq_of_cmp_wrt h := by rw [eq_of_cmp h]
 
-instance [EqOfCmpWrt α (fun a => a) cmp] : EqOfCmp α cmp where
-  eq_of_cmp h := eq_of_cmp_wrt (f := fun a => a) h
-
 -- ## Basic Instances
 
 theorem eq_of_compareOfLessAndEq [LT α] [DecidableEq α] {a a' : α}
@@ -67,64 +62,10 @@ instance : LawfulCmpEq Nat compare where
   eq_of_cmp := eq_of_compareOfLessAndEq
   cmp_rfl := compareOfLessAndEq_rfl <| Nat.lt_irrefl _
 
-theorem Fin.eq_of_compare {n n' : Fin m} (h : compare n n' = .eq) : n = n' := by
-  dsimp only [compare] at h
-  have h' := eq_of_compareOfLessAndEq h
-  exact Fin.eq_of_val_eq h'
-
-instance : LawfulCmpEq (Fin n) compare where
-  eq_of_cmp := Fin.eq_of_compare
-  cmp_rfl := compareOfLessAndEq_rfl <| Nat.lt_irrefl _
-
 instance : LawfulCmpEq UInt64 compare where
   eq_of_cmp h := eq_of_compareOfLessAndEq h
   cmp_rfl := compareOfLessAndEq_rfl <| Nat.lt_irrefl _
 
-theorem List.lt_irrefl [LT α] (irrefl_α : ∀ a : α, ¬ a < a)
-: (a : List α) → ¬ a < a
-| _, .head _ _ h => irrefl_α _ h
-| _, .tail _ _ h3 => lt_irrefl irrefl_α _ h3
-
-@[simp] theorem String.lt_irrefl (s : String) : ¬ s < s :=
-  List.lt_irrefl (fun c => Nat.lt_irrefl c.1.1) _
-
 instance : LawfulCmpEq String compare where
   eq_of_cmp := eq_of_compareOfLessAndEq
   cmp_rfl := compareOfLessAndEq_rfl <| String.lt_irrefl _
-
-@[macro_inline]
-def Option.compareWith (cmp : α → α → Ordering) : Option α → Option α → Ordering
-| none,   none    => .eq
-| none,   some _  => .lt
-| some _, none    => .gt
-| some x, some y  => cmp x y
-
-instance [EqOfCmp α cmp] : EqOfCmp (Option α) (Option.compareWith cmp) where
-  eq_of_cmp := by
-    intro o o'
-    unfold Option.compareWith
-    cases o <;> cases o' <;> simp
-    exact eq_of_cmp
-
-instance [LawfulCmpEq α cmp] : LawfulCmpEq (Option α) (Option.compareWith cmp) where
-  cmp_rfl := by
-    intro o
-    unfold Option.compareWith
-    cases o <;> simp
-
-def Prod.compareWith
-(cmpA : α → α → Ordering) (cmpB : β → β → Ordering)
-: (α × β) → (α × β) → Ordering :=
-  fun (a, b) (a', b') => match cmpA a a' with | .eq => cmpB b b' | ord => ord
-
-instance [EqOfCmp α cmpA] [EqOfCmp β cmpB]
-: EqOfCmp (α × β) (Prod.compareWith cmpA cmpB) where
-  eq_of_cmp := by
-    intro (a, b) (a', b')
-    dsimp only [Prod.compareWith]
-    split; next ha => intro hb; rw [eq_of_cmp ha, eq_of_cmp hb]
-    intros; contradiction
-
-instance [LawfulCmpEq α cmpA] [LawfulCmpEq β cmpB]
-: LawfulCmpEq (α × β) (Prod.compareWith cmpA cmpB) where
-  cmp_rfl := by simp [Prod.compareWith]
diff --git a/src/lake/Lake/Util/Name.lean b/src/lake/Lake/Util/Name.lean
index f4060d7cd2..e9d3133293 100644
--- a/src/lake/Lake/Util/Name.lean
+++ b/src/lake/Lake/Util/Name.lean
@@ -7,7 +7,6 @@ import Lean.Data.Json
 import Lean.Data.NameMap
 import Lake.Util.DRBMap
 import Lake.Util.RBArray
-import Lake.Util.Compare
 
 open Lean