add initial smart constructors

Katydid.lean

@@ -11,5 +11,6 @@ import Katydid.Example.SimpLibrary
 import Katydid.Regex.Language
 import Katydid.Regex.SimpleRegex
 import Katydid.Regex.IndexedRegex
+import Katydid.Regex.SmartRegex
 
 import Katydid.Expr.Desc

Katydid/Regex/SimpleRegex.lean

@@ -226,3 +226,6 @@ theorem derive_commutes {α: Type} (r: Regex α) (x: α):
     congrm ((Language.concat ?_ (Language.star (denote r))))
     guard_target = denote (derive r x) = Language.derive (denote r) x
     exact ih
+
+def decidableDenote (r: Regex α): DecidablePred (denote r) := by
+  sorry

Katydid/Regex/SmartRegex.lean

@@ -0,0 +1,60 @@
+import Katydid.Regex.Language
+
+open List
+
+namespace SmartRegex
+
+inductive Regex (α: Type): Type where
+  | emptyset : Regex α
+  | emptystr : Regex α
+  | pred : (p: α -> Prop) → [DecidablePred p] → Regex α
+  | or : Regex α → Regex α → Regex α
+  | concat : Regex α → Regex α → Regex α
+  | star : Regex α → Regex α
+
+def denote {α: Type} (r: Regex α): Language.Lang α :=
+  match r with
+  | Regex.emptyset => Language.emptyset
+  | Regex.emptystr => Language.emptystr
+  | Regex.pred p => Language.pred p
+  | Regex.or x y => Language.or (denote x) (denote y)
+  | Regex.concat x y => Language.concat (denote x) (denote y)
+  | Regex.star x => Language.star (denote x)
+
+-- TODO: incorporate more simplification rules into the smart constructor
+def smartOr (x y: Regex α): Regex α :=
+  match x with
+  | Regex.emptyset => y
+  | _ =>
+    match y with
+    | Regex.emptyset => x
+    | _ => Regex.or x y
+
+-- TODO: incorporate more simplification rules into the smart constructor
+def smartConcat (x y: Regex α): Regex α :=
+  match x with
+  | Regex.emptystr => y
+  | _ =>
+    match y with
+    | Regex.emptystr => x
+    | _ => Regex.concat x y
+
+-- TODO: incorporate more simplification rules into the smart constructor
+def smartStar (x: Regex α): Regex α :=
+  match x with
+  | Regex.star x' =>
+    Regex.star x'
+  | _ =>
+    Regex.star x
+
+theorem smartOr_is_correct (x y: Regex α):
+  denote (Regex.or x y) = denote (smartOr x y) := by
+  sorry
+
+theorem smartConcat_is_correct (x y: Regex α):
+  denote (Regex.concat x y) = denote (smartConcat x y) := by
+  sorry
+
+theorem smartStar_is_correct (x: Regex α):
+  denote (Regex.star x) = denote (smartStar x) := by
+  sorry

README.md

@@ -16,7 +16,7 @@ This is just a quick overview of the steps towards our goal.
 
 Prove theorems about Symbolic regular expressions as a foundation to build upon.
 
-- [ ] Prove correctness of derivative algorithm via a commuting diagram.
+- [x] Prove correctness of derivative algorithm via a commuting diagram.
 - [ ] Prove correctness of derivative algorithm via a Regex type indexed with Language.
 - [ ] Prove decidability of derivative algorithm.
 - [ ] Prove correctness of simplification rules.