From e0c69a78f12d0c509dcc5ad6d62c8bcced88a50a Mon Sep 17 00:00:00 2001
From: Walter Schulze <awalterschulze@gmail.com>
Date: Mon, 23 Dec 2024 14:11:17 +0000
Subject: [PATCH] NonEmptyList.mergeReps

---
 Katydid/Regex/SmartRegex.lean |  9 ++++-----
 Katydid/Std/Lists.lean        | 19 ++++++++++++++++++
 Katydid/Std/NonEmptyList.lean | 37 ++++++++++-------------------------
 3 files changed, 33 insertions(+), 32 deletions(-)

diff --git a/Katydid/Regex/SmartRegex.lean b/Katydid/Regex/SmartRegex.lean
index 2d7fa49..6ae9e8a 100644
--- a/Katydid/Regex/SmartRegex.lean
+++ b/Katydid/Regex/SmartRegex.lean
@@ -345,11 +345,10 @@ def smartOr (x y: Regex α): Regex α :=
     -- it is implied that xs is sorted, given it was created using smartOr
     let xs := orToList x
     let ys := orToList y
-    -- merge the sorted lists, resulting in a sorted list
-    let ors := NonEmptyList.merge xs ys
-    -- remove duplicates from sorted list using erase repititions
-    let uniqueOrs := NonEmptyList.eraseReps ors
-    orFromList uniqueOrs
+    -- merge the sorted lists and remove duplicates,
+    -- resulting in a sorted list of unique items.
+    let ors := NonEmptyList.mergeReps xs ys
+    orFromList ors
 
 theorem smartOr_is_or (x y: Regex α):
   denote (Regex.or x y) = denote (smartOr x y) := by
diff --git a/Katydid/Std/Lists.lean b/Katydid/Std/Lists.lean
index 45ace2b..a5c3bea 100644
--- a/Katydid/Std/Lists.lean
+++ b/Katydid/Std/Lists.lean
@@ -41,6 +41,25 @@ instance [Ord α]: LE (List α) where
 def Lists.merge [Ord α] (xs: List α) (ys: List α): List α :=
   List.merge xs ys (fun x y => (Ord.compare x y).isLE)
 
+def Lists.eraseReps [BEq α] (xs: List α): List α :=
+  match xs with
+  | [] => []
+  | [x] => [x]
+  | (x1::x2::xs) =>
+    if x1 == x2
+    then Lists.eraseReps (x2::xs)
+    else x1 :: List.eraseReps (x2::xs)
+
+def Lists.mergeReps [BEq α] [Ord α] (xs ys: List α): List α :=
+  match xs, ys with
+  | [], ys => ys
+  | xs, [] => xs
+  | x :: xs, y :: ys =>
+    match Ord.compare x y with
+    | Ordering.eq => Lists.mergeReps xs (y::ys)
+    | Ordering.lt => x :: Lists.mergeReps xs (y::ys)
+    | Ordering.gt => y :: Lists.mergeReps (x::xs) ys
+
 theorem list_cons_ne_nil (x : α) (xs : List α):
   x :: xs ≠ [] := by
   intro h'
diff --git a/Katydid/Std/NonEmptyList.lean b/Katydid/Std/NonEmptyList.lean
index cd94653..8db1de7 100644
--- a/Katydid/Std/NonEmptyList.lean
+++ b/Katydid/Std/NonEmptyList.lean
@@ -53,34 +53,17 @@ def eraseReps [BEq α] (xs: NonEmptyList α): NonEmptyList α :=
     | (x''::xs'') =>
       if x' == x''
       then NonEmptyList.eraseReps (NonEmptyList.mk x'' xs'')
-      else NonEmptyList.mk x' (List.eraseReps xs')
-
-def mergeRep [BEq α] [Ord α] (x: α) (ys zs : List α): NonEmptyList α :=
-  match ys, zs with
-  | [], [] =>
-    NonEmptyList.mk x []
-  | (y::ys), [] =>
-    match Ord.compare x y with
-    | Ordering.eq =>
-        NonEmptyList.eraseReps (NonEmptyList.mk y ys)
-    | Ordering.lt =>
-        NonEmptyList.cons x (NonEmptyList.eraseReps (NonEmptyList.mk y ys))
-    | Ordering.gt =>
-        NonEmptyList.cons y (NonEmptyList.eraseReps (NonEmptyList.mk x ys))
-  | [], (y::ys) =>
-    match Ord.compare x y with
-    | Ordering.eq => eraseReps (NonEmptyList.mk y ys)
-    | Ordering.lt => NonEmptyList.cons x (eraseReps (NonEmptyList.mk y ys))
-    | Ordering.gt => NonEmptyList.cons y (eraseReps (NonEmptyList.mk x ys))
-  | (y::ys'), (z::zs') =>
-    sorry
+      else NonEmptyList.mk x' (Lists.eraseReps xs')
 
 def mergeReps [BEq α] [Ord α] (xs ys : NonEmptyList α): NonEmptyList α :=
   match xs, ys with
-  | NonEmptyList.mk x [], NonEmptyList.mk y ys' =>
+  | NonEmptyList.mk x xs, NonEmptyList.mk y ys =>
     match Ord.compare x y with
-    | Ordering.eq => NonEmptyList.eraseReps ys
-    | Ordering.lt => NonEmptyList.cons x (NonEmptyList.eraseReps ys)
-    | Ordering.gt => NonEmptyList.cons y (NonEmptyList.eraseReps (NonEmptyList.mk x ys'))
-  | NonEmptyList.mk x xs', NonEmptyList.mk y ys' =>
-   sorry
+    | Ordering.eq =>
+        match xs with
+        | [] =>
+            NonEmptyList.mk y ys
+        | (x'::xs') =>
+            NonEmptyList.mergeReps (NonEmptyList.mk x' xs') (NonEmptyList.mk y ys)
+    | Ordering.lt => NonEmptyList.mk x (Lists.mergeReps xs (y::ys))
+    | Ordering.gt => NonEmptyList.mk y (Lists.mergeReps (x::xs) ys)