start proving smart or

Katydid.lean

@@ -1,10 +1,12 @@
+import Katydid.Std.BEq
 import Katydid.Std.Ordering
 import Katydid.Std.Decidable
 import Katydid.Std.OrderingThunk
 import Katydid.Std.Nat
 import Katydid.Std.Lists
 import Katydid.Std.Ltac
 import Katydid.Std.Balistic
+import Katydid.Std.NonEmptyList
 
 import Katydid.Example.SimpLibrary
 

Katydid/Regex/SmartRegex.lean

@@ -1,3 +1,5 @@
+import Katydid.Std.NonEmptyList
+
 import Katydid.Regex.Language
 
 open List
@@ -177,6 +179,28 @@ theorem smartConcat_is_concat {α: Type} (x y: Regex α):
     · case emptystr =>
       apply Language.simp_concat_emptystr_r_is_l
 
+def orToList (x: Regex α): NonEmptyList (Regex α) :=
+  match x with
+  | Regex.or x1 x2 =>
+    -- smartOr guarantees that left hand side will not be an Regex.or so a recursive call is only required on the right hand side.
+    NonEmptyList.cons x1 (orToList x2)
+  | _ =>
+    NonEmptyList.mk x []
+
+def orFromList (xs: NonEmptyList (Regex α)): Regex α :=
+  match xs with
+  | NonEmptyList.mk x1 [] =>
+    x1
+  | NonEmptyList.mk x1 (x2::xs) =>
+    Regex.or x1 (orFromList (NonEmptyList.mk x2 xs))
+
+theorem orToList_is_orFromList (x: Regex α):
+  orFromList (orToList x) = x := by
+  induction x <;> (try simp [orToList, orFromList])
+  · case or x1 x2 ih1 ih2 =>
+    sorry
+
+
 -- TODO: incorporate more simplification rules into the smart constructor
 -- 1. Get the list of ors (Language.simp_or_assoc)
 -- 2. Remove duplicates from the list (create a set) (Language.simp_or_comm and Language.simp_or_idemp and Language.simp_or_assoc)

Katydid/Std/BEq.lean

@@ -0,0 +1,22 @@
+theorem beq_eq_or_neq {α: Type} [BEq α] (x y: α):
+  BEq.beq x y \/ (Not (BEq.beq x y)) := by
+  by_cases BEq.beq x y
+  · left
+    assumption
+  · right
+    assumption
+
+theorem beq_eq_or_neq_prop {α: Type} [BEq α] [LawfulBEq α] (x y: α):
+  x = y \/ (Not (x = y)) := by
+  have h := beq_eq_or_neq x y
+  cases h
+  · case inl h =>
+    left
+    rw [beq_iff_eq] at h
+    assumption
+  · case inr h =>
+    right
+    intro h'
+    apply h
+    rw [h']
+    rw [beq_iff_eq]

Katydid/Std/Lists.lean

@@ -8,7 +8,9 @@
 -- https://github.com/leanprover/lean4/blob/master/src/Init/Tactics.lean
 
 import Mathlib.Tactic.Linarith
+import Mathlib.Tactic.SplitIfs
 
+import Katydid.Std.BEq
 import Katydid.Std.Nat
 
 open Nat
@@ -942,3 +944,69 @@ theorem list_splitAt_length_exists {α: Type} (xs: List α):
   exists []
   exists xs
   simp
+
+theorem list_eraseDup_does_not_erase_singleton (α: Type) [BEq α] (x: α):
+  List.eraseDup [x] = [x] := by
+  simp [eraseDup]
+
+theorem list_notin_cons (y: α) (x: α) (xs: List α):
+  y ∉ x :: xs -> y ≠ x /\ y ∉ xs := by
+  intro h
+  apply And.intro
+  · intro xy
+    apply h
+    rw [xy]
+    apply Mem.head
+  · intro yinxs
+    apply h
+    apply Mem.tail
+    exact yinxs
+
+theorem list_eraseReps_finishes {α: Type} [BEq α] (x: α) (xs: List α):
+  List.eraseReps (List.eraseReps xs) = List.eraseReps xs := by
+  sorry
+
+theorem list_eraseReps_xx {α: Type} [BEq α] (x: α) (xs: List α):
+  List.eraseReps (x::(x::xs)) = List.eraseReps (x::xs) := by
+  sorry
+
+-- theorem list_eraseReps_does_not_erase_head (α: Type) [BEq α] (x: α) (xs: List α) (h: x ∉ xs):
+--   ∃ exs, List.eraseReps (x::xs) = x::exs := by
+--   induction xs with
+--   | nil =>
+--     exists []
+--   | cons ix ixs ih =>
+--     have h' := list_notin_cons x ix ixs h
+--     clear h
+--     cases h' with
+--     | intro xix xixs =>
+--     have ih' := ih xixs
+--     clear ih
+--     cases ih' with
+--     | intro exs ih' =>
+--     simp [List.eraseReps]
+--     exists List.eraseReps (ix :: ixs)
+--     simp [eraseReps.loop]
+
+theorem list_eraseReps_has_same_head (α: Type) [BEq α] [LawfulBEq α] (x: α) (xs: List α):
+  ∃ (xs': List α), (x::xs') = List.eraseReps (x::xs) := by
+  induction xs with
+  | nil =>
+    exists []
+  | cons ix ixs ih =>
+    cases ih with
+    | intro xs ih =>
+    have xix := beq_eq_or_neq_prop x ix
+    cases xix
+    · case inl xix =>
+      rw [xix]
+      rw [list_eraseReps_xx]
+      rw [<- xix]
+      exists xs
+    · case inr xix =>
+      exists (List.eraseReps (ix::ixs))
+      simp only [List.eraseReps]
+      simp only [List.eraseReps.loop]
+      split
+      · sorry
+      · sorry

Katydid/Std/NonEmptyList.lean

@@ -0,0 +1,8 @@
+structure NonEmptyList (α: Type) where
+  head : α
+  tail : List α
+
+namespace NonEmptyList
+
+def cons (x: α) (xs: NonEmptyList α): NonEmptyList α :=
+  NonEmptyList.mk x (xs.head :: xs.tail)