NonEmptyList.mergeReps

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

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'

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)