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)