half a proof for smartOr_is_or

katydid · Feb 20, 2025 · 1278a6b · 1278a6b
1 parent ab94823
commit 1278a6b
Show file tree

Hide file tree

Showing 2 changed files with 123 additions and 28 deletions.
diff --git a/Katydid/Regex/SmartRegex.lean b/Katydid/Regex/SmartRegex.lean
@@ -393,18 +393,113 @@ def smartOr (x y: Regex α): Regex α :=
   | Regex.emptyset => x
   | Regex.star (Regex.pred (Predicate.mk "any" _)) => y
   | _ =>
-    -- 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 and remove duplicates,
-    -- resulting in a sorted list of unique items.
+    -- It is implied that xs is sorted, given it was created using smartOr.
+    -- Merge the sorted lists and remove duplicates, resulting in a sorted list of unique items.
     let ors := NonEmptyList.mergeReps xs ys
     orFromList ors
 
+private theorem smartOr_emptyset_l_is_r (x: Regex α):
+  denote (Regex.or Regex.emptyset x) = denote (smartOr Regex.emptyset x) := by
+  simp only [smartOr]
+  nth_rewrite 1 [denote]
+  nth_rewrite 1 [denote]
+  rw [Language.simp_or_emptyset_l_is_r]
+
+private theorem smartOr_emptyset_r_is_l':
+  smartOr x Regex.emptyset = x := by
+  simp only [smartOr]
+  split
+  · rfl
+  · rfl
+  · rfl
+
+private theorem smartOr_emptyset_r_is_l (x: Regex α):
+  denote (Regex.or x Regex.emptyset) = denote (smartOr x Regex.emptyset) := by
+  nth_rewrite 1 [denote]
+  nth_rewrite 1 [denote]
+  rw [Language.simp_or_emptyset_r_is_l]
+  rw [smartOr_emptyset_r_is_l']
+
+private theorem smartOr_orFromList_mergeReps_orToList_is_or (x y: Regex α):
+  denote (orFromList (NonEmptyList.mergeReps (orToList x) (orToList y))) = denote (Regex.or x y):= by
+  induction x with
+  | emptyset =>
+    simp [denote, orFromList, orToList, NonEmptyList.mergeReps]
+    sorry
+  | emptystr =>
+    sorry
+  | pred _ =>
+    sorry
+  | or x1 x2 =>
+    sorry
+  | concat x1 x2 =>
+    sorry
+  | star x1 =>
+    sorry
+
 theorem smartOr_is_or (x y: Regex α):
   denote (Regex.or x y) = denote (smartOr x y) := by
-  -- TODO
-  sorry
+  induction x with
+  | emptyset =>
+    rw [smartOr_emptyset_l_is_r]
+  | emptystr =>
+    cases y with
+    | emptyset =>
+      rw [smartOr_emptyset_r_is_l]
+    | emptystr =>
+      simp only [smartOr]
+      rw [smartOr_orFromList_mergeReps_orToList_is_or]
+    | pred _ =>
+      simp only [smartOr]
+      rw [smartOr_orFromList_mergeReps_orToList_is_or]
+    | or y1 y2 =>
+      simp only [smartOr]
+      rw [smartOr_orFromList_mergeReps_orToList_is_or]
+    | concat y1 y2 =>
+      simp only [smartOr]
+      rw [smartOr_orFromList_mergeReps_orToList_is_or]
+    | star y1 =>
+      cases y1 with
+      | emptyset =>
+        simp only [smartOr]
+        rw [smartOr_orFromList_mergeReps_orToList_is_or]
+      | emptystr =>
+        simp only [smartOr]
+        rw [smartOr_orFromList_mergeReps_orToList_is_or]
+      | pred p1 =>
+        simp only [smartOr]
+        split
+        · case _ _ h =>
+          contradiction
+        · case _ _ h _ _ h' =>
+          simp at h'
+          rw [h']
+          unfold denote
+          sorry
+        · case _ _ h _ =>
+          sorry
+      | or y11 y12 =>
+        simp only [smartOr]
+        rw [smartOr_orFromList_mergeReps_orToList_is_or]
+      | concat y11 y12 =>
+        simp only [smartOr]
+        rw [smartOr_orFromList_mergeReps_orToList_is_or]
+      | star y11 =>
+        simp only [smartOr]
+        rw [smartOr_orFromList_mergeReps_orToList_is_or]
+  | pred p =>
+    cases p
+    case mk pred dpred desc func =>
+    simp only [smartOr]
+    sorry
+  | or x1 x2 =>
+    sorry
+  | concat x1 x2 =>
+    sorry
+  | star x1 =>
+    sorry
 
 def derive (r: Regex α) (a: α): Regex α :=
   match r with

diff --git a/Katydid/Std/NonEmptyList.lean b/Katydid/Std/NonEmptyList.lean
@@ -34,36 +34,36 @@ def merge' [Ord α] (xs: NonEmptyList α) (ys: NonEmptyList α): List α :=
 
 def merge [Ord α] (xs: NonEmptyList α) (ys: NonEmptyList α): NonEmptyList α :=
   match xs with
-  | NonEmptyList.mk x' xs' =>
+  | NonEmptyList.mk x1 xs1 =>
   match ys with
-  | NonEmptyList.mk y' ys' =>
-  match Ord.compare x' y' with
+  | NonEmptyList.mk y1 ys1 =>
+  match Ord.compare x1 y1 with
   | Ordering.eq =>
-    NonEmptyList.mk x' (Lists.merge xs' ys')
+    NonEmptyList.mk x1 (Lists.merge xs1 ys1)
   | Ordering.lt =>
-    NonEmptyList.mk x' (Lists.merge xs' (y'::ys'))
+    NonEmptyList.mk x1 (Lists.merge xs1 (y1::ys1))
   | Ordering.gt =>
-    NonEmptyList.mk y' (Lists.merge (x'::xs') ys')
+    NonEmptyList.mk y1 (Lists.merge (x1::xs1) ys1)
 
 def eraseReps [BEq α] (xs: NonEmptyList α): NonEmptyList α :=
   match xs with
-  | NonEmptyList.mk x' xs' =>
-    match xs' with
-    | [] => xs
-    | (x''::xs'') =>
-      if x' == x''
-      then NonEmptyList.eraseReps (NonEmptyList.mk x'' xs'')
-      else NonEmptyList.mk x' (Lists.eraseReps xs')
+  | NonEmptyList.mk x1 xs1 =>
+  match xs1 with
+  | [] => xs
+  | (x2::xs2) =>
+    if x1 == x2
+    then NonEmptyList.eraseReps (NonEmptyList.mk x2 xs2)
+    else NonEmptyList.mk x1 (Lists.eraseReps xs1)
 
 def mergeReps [BEq α] [Ord α] (xs ys : NonEmptyList α): NonEmptyList α :=
   match xs, ys with
-  | NonEmptyList.mk x xs, NonEmptyList.mk y ys =>
-    match Ord.compare x y with
-    | 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)
+  | NonEmptyList.mk x1 xs1, NonEmptyList.mk y1 ys1 =>
+  match Ord.compare x1 y1 with
+  | Ordering.eq =>
+    match xs1 with
+    | [] =>
+      NonEmptyList.mk y1 ys1
+    | (x2::xs2) =>
+      NonEmptyList.mergeReps (NonEmptyList.mk x2 xs2) (NonEmptyList.mk y1 ys1)
+  | Ordering.lt => NonEmptyList.mk x1 (Lists.mergeReps xs1 (y1::ys1))
+  | Ordering.gt => NonEmptyList.mk y1 (Lists.mergeReps (x1::xs1) ys1)