smart or constructor now applies most rules

CONTRIBUTING.md

@@ -21,10 +21,6 @@
  - Do we like comments? Yes we do.
  - Are they required? No.
 
-### When to use a separate file
-
-Now. When you are starting to ask this question, it is time to start using a separate file.
-
 ### Tactics
 
 Tactics unlike proofs, definitions, etc. don't have any types.

Katydid/Regex/SmartRegex.lean

@@ -8,41 +8,52 @@ namespace SmartRegex
 
 inductive Predicate (α: Type) where
   | mk
+    (o: Ord α)
     (desc: String)
     (func: α -> Prop)
-    (dec: DecidablePred func)
+    (d: DecidablePred func)
   : Predicate α
 
-def Predicate.desc (p: Predicate α): String :=
+def Predicate.desc {α: Type} (p: Predicate α): String :=
   match p with
-  | ⟨ desc, _, _ ⟩ => desc
+  | ⟨ _, desc, _, _ ⟩ => desc
+
+def Predicate.compare (x: Predicate α) (y: Predicate α): Ordering :=
+  let xd: String := x.desc
+  let yd: String := y.desc
+  Ord.compare xd yd
+
+instance : Ord (Predicate α) where
+  compare: Predicate α → Predicate α → Ordering := Predicate.compare
+
+def Predicate.mkAny [o: Ord α]: Predicate α := by
+  apply @Predicate.mk α o "any"
+  · sorry
+  · exact fun _ => True
+
+def Predicate.mkChar (c: Char): Predicate Char := by
+  apply @Predicate.mk Char inferInstance (String.mk [c])
+  · sorry
+  · exact fun a: Char => a = c
 
 def Predicate.func (p: Predicate α): α -> Prop :=
   match p with
-  | ⟨ _, f, _ ⟩ => f
+  | ⟨ _, _, f, _ ⟩ => f
 
 def Predicate.decfunc (p: Predicate α): DecidablePred p.func := by
   cases p with
-  | mk desc f dec =>
+  | mk _ _ f dec =>
     intro a
     unfold DecidablePred at dec
     unfold Predicate.func
-    simp
+    simp only
     apply dec
 
 def evalPredicate (p: Predicate α) (a: α): Bool := by
   cases p.decfunc a with
   | isFalse => exact Bool.false
   | isTrue => exact Bool.true
 
-def Predicate.compare (x: Predicate α) (y: Predicate α): Ordering :=
-  let xd: String := x.desc
-  let yd: String := y.desc
-  Ord.compare xd yd
-
-instance : Ord (Predicate α) where
-  compare: Predicate α → Predicate α → Ordering := Predicate.compare
-
 inductive Regex (α: Type): Type where
   | emptyset : Regex α
   | emptystr : Regex α
@@ -51,6 +62,83 @@ inductive Regex (α: Type): Type where
   | concat : Regex α → Regex α → Regex α
   | star : Regex α → Regex α
 
+def Regex.compare (x y: Regex α): Ordering :=
+  match x with
+  | Regex.emptyset =>
+    match y with
+    | Regex.emptyset =>
+      Ordering.eq
+    | _ =>
+      Ordering.lt
+  | Regex.emptystr =>
+    match y with
+    | Regex.emptyset =>
+      Ordering.gt
+    | Regex.emptystr =>
+      Ordering.eq
+    | _ =>
+      Ordering.lt
+  | Regex.pred p1 =>
+    match y with
+    | Regex.emptyset =>
+      Ordering.gt
+    | Regex.emptystr =>
+      Ordering.gt
+    | Regex.pred p2 =>
+      Ord.compare p1 p2
+    | _ =>
+      Ordering.lt
+  | Regex.or x1 x2 =>
+    match y with
+    | Regex.emptyset =>
+      Ordering.gt
+    | Regex.emptystr =>
+      Ordering.gt
+    | Regex.pred _ =>
+      Ordering.gt
+    | Regex.or y1 y2 =>
+      match Regex.compare x1 y1 with
+      | Ordering.eq =>
+        Regex.compare x2 y2
+      | o => o
+    | _ =>
+      Ordering.lt
+  | Regex.concat x1 x2 =>
+    match y with
+    | Regex.emptyset =>
+      Ordering.gt
+    | Regex.emptystr =>
+      Ordering.gt
+    | Regex.pred _ =>
+      Ordering.gt
+    | Regex.or _ _ =>
+      Ordering.gt
+    | Regex.concat y1 y2 =>
+      match Regex.compare x1 y1 with
+      | Ordering.eq =>
+        Regex.compare x2 y2
+      | o => o
+    | _ =>
+      Ordering.lt
+  | Regex.star x1 =>
+    match y with
+    | Regex.star y1 =>
+      Regex.compare x1 y1
+    | _ =>
+      Ordering.lt
+
+instance : Ord (Regex α) where
+  compare (x y: Regex α): Ordering := Regex.compare x y
+
+instance : LE (Regex α) where
+  le x y := (Ord.compare x y).isLE
+
+instance : BEq (Regex α) where
+  beq x y := Ord.compare x y == Ordering.eq
+
+def Regex.le (x y: Regex α): Bool :=
+  x <= y
+
 def null (r: Regex α): Bool :=
   match r with
   | Regex.emptyset => false
@@ -200,45 +288,32 @@ theorem orToList_is_orFromList (x: Regex α):
   · 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)
--- 3. If at any following step the set is size one, simply return
--- 4. If the set contains star (any) then return star (any) (Language.simp_or_universal_r_is_universal and Language.simp_or_universal_l_is_universal)
--- 5. Delete emptyset from the set (Language.simp_or_emptyset_r_is_l and Language.simp_or_emptyset_l_is_r)
--- 6. If any of the set is nullable, remove emptystr from the set (Language.simp_or_emptystr_null_r_is_r and Language.simp_or_null_l_emptystr_is_l)
--- 7. create a sorted list from the set (Language.simp_or_assoc and Language.simp_or_comm)
+-- 1. If x or y is emptyset then return the other (Language.simp_or_emptyset_r_is_l and Language.simp_or_emptyset_l_is_r)
+-- 2. If x or y is star (any) then return star (any) (Language.simp_or_universal_r_is_universal and Language.simp_or_universal_l_is_universal)
+-- 3. Get the lists of ors using orToList (Language.simp_or_assoc)
+-- 4. Merge sort the sorrted lists (Language.simp_or_comm and Language.simp_or_assoc)
+-- 5. Remove duplicates from the list (or create a set) (Language.simp_or_idemp)
+-- 6. If at any following step the set is size one, simply return
+-- TODO: 7. If any of the set is nullable, remove emptystr from the set (Language.simp_or_emptystr_null_r_is_r and Language.simp_or_null_l_emptystr_is_l)
+-- 8. Reconstruct Regex.or from the list using orFromList (Language.simp_or_assoc)
 def smartOr (x y: Regex α): Regex α :=
   match x with
   | Regex.emptyset => y
+  | Regex.star (Regex.pred (Predicate.mk _ "any" _ _)) => x
   | _ =>
-    match y with
-    | Regex.emptyset => x
-    | _ => Regex.or x y
-
-private theorem smartOr_is_or_righthand (x y: Regex α) (hx_emptyset: x ≠ Regex.emptyset):
-  denote (Regex.or x y) = denote (smartOr x y) := by
-  cases y <;> (try simp [smartOr])
-  · case emptyset =>
-    simp [denote]
-    exact (Language.simp_or_emptyset_r_is_l (denote x))
+  match y with
+  | 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, 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
 
 theorem smartOr_is_or (x y: Regex α):
   denote (Regex.or x y) = denote (smartOr x y) := by
-  have hy := smartOr_is_or_righthand x y
-  match x with
-  | Regex.emptyset =>
-    unfold smartOr
-    simp [denote]
-    exact (Language.simp_or_emptyset_l_is_r (denote y))
-  | Regex.emptystr =>
-    exact hy (by simp)
-  | Regex.pred p =>
-    exact hy (by simp)
-  | Regex.or x1 x2 =>
-    exact hy (by simp)
-  | Regex.concat x1 x2 =>
-    exact hy (by simp)
-  | Regex.star x1 =>
-    exact hy (by simp)
+  sorry

Katydid/Std/Lists.lean

@@ -11,11 +11,36 @@ import Mathlib.Tactic.Linarith
 import Mathlib.Tactic.SplitIfs
 
 import Katydid.Std.BEq
+import Katydid.Std.Ordering
 import Katydid.Std.Nat
 
 open Nat
 open List
 
+def Lists.compare [o: Ord α] (xs ys: List α): Ordering :=
+  Ordering.lex
+    (Ord.compare (length xs) (length ys))
+    (match xs with
+      | [] =>
+        match ys with
+        | [] => Ordering.eq
+        | _ => Ordering.lt -- impossible
+      | (x'::xs') =>
+        match ys with
+        | [] => Ordering.gt -- impossible
+        | (y'::ys') =>
+            Ordering.lex (Ord.compare x' y') (Lists.compare xs' ys')
+    )
+
+instance [Ord α]: Ord (List α) where
+  compare := Lists.compare
+
+instance [Ord α]: LE (List α) where
+  le xs ys := (Lists.compare xs ys).isLE
+
+def Lists.merge [Ord α] (xs: List α) (ys: List α): List α :=
+  List.merge xs ys (fun x y => (Ord.compare x y).isLE)
+
 theorem list_cons_ne_nil (x : α) (xs : List α):
   x :: xs ≠ [] := by
   intro h'
@@ -962,51 +987,14 @@ theorem list_notin_cons (y: α) (x: α) (xs: List α):
     apply Mem.tail
     exact yinxs
 
-theorem list_eraseReps_finishes {α: Type} [BEq α] (x: α) (xs: List α):
+theorem list_eraseReps_idemp {α: Type} [BEq α] (x: α) (xs: List α):
   List.eraseReps (List.eraseReps xs) = List.eraseReps xs := by
   sorry
 
-theorem list_eraseReps_xx {α: Type} [BEq α] (x: α) (xs: List α):
+theorem list_eraseReps_erases_first_rep {α: 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 α):
+theorem list_eraseReps_does_not_erase_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
+  sorry

Katydid/Std/NonEmptyList.lean

@@ -1,8 +1,56 @@
+import Katydid.Std.Ordering
+import Katydid.Std.Lists
+
 structure NonEmptyList (α: Type) where
   head : α
   tail : List α
 
 namespace NonEmptyList
 
+def compare [o: Ord α] (xs ys: NonEmptyList α): Ordering :=
+  match xs with
+  | NonEmptyList.mk x' xs' =>
+  match ys with
+  | NonEmptyList.mk y' ys' =>
+    Ordering.lex (Ord.compare x' y') (Ord.compare xs' ys')
+
+instance [Ord α] : Ord (NonEmptyList α) where
+  compare := compare
+
 def cons (x: α) (xs: NonEmptyList α): NonEmptyList α :=
   NonEmptyList.mk x (xs.head :: xs.tail)
+
+def toList (xs: NonEmptyList α): List α :=
+  match xs with
+  | NonEmptyList.mk head tail =>
+    head :: tail
+
+instance [Ord α] : LE (NonEmptyList α) where
+  le (x: NonEmptyList α) (y: NonEmptyList α) :=
+    LE.le x.toList y.toList
+
+def merge' [Ord α] (xs: NonEmptyList α) (ys: NonEmptyList α): List α :=
+  List.merge (xs.toList) (ys.toList) (fun x y => (Ord.compare x y).isLE)
+
+def merge [Ord α] (xs: NonEmptyList α) (ys: NonEmptyList α): NonEmptyList α :=
+  match xs with
+  | NonEmptyList.mk x' xs' =>
+  match ys with
+  | NonEmptyList.mk y' ys' =>
+  match Ord.compare x' y' with
+  | Ordering.eq =>
+    NonEmptyList.mk x' (Lists.merge xs' ys')
+  | Ordering.lt =>
+    NonEmptyList.mk x' (Lists.merge xs' (y'::ys'))
+  | Ordering.gt =>
+    NonEmptyList.mk y' (Lists.merge (x'::xs') ys')
+
+def eraseReps [BEq α] (xs: NonEmptyList α): NonEmptyList α :=
+  match xs with
+  | NonEmptyList.mk x' xs' =>
+    match xs' with
+    | [] => xs
+    | (x''::xs'') =>
+      if x' == x''
+      then eraseReps (NonEmptyList.mk x'' xs'')
+      else NonEmptyList.mk x' (List.eraseReps xs')