initial definition of indexed regex

Author: awalterschulze

Katydid.lean

@@ -1,4 +1,5 @@
 import Katydid.Std.Ordering
+import Katydid.Std.Decidable
 import Katydid.Std.OrderingThunk
 import Katydid.Std.Lists
 import Katydid.Std.Ltac
@@ -9,5 +10,6 @@ import Katydid.Example.SimpLibrary
 import Katydid.Regex.Regex
 import Katydid.Regex.Language
 import Katydid.Regex.Commutes
+import Katydid.Regex.IndexedRegex
 
 import Katydid.Expr.Desc

Katydid/Regex/IndexedRegex.lean

@@ -0,0 +1,31 @@
+import Katydid.Std.Decidable
+
+import Katydid.Regex.Language
+
+namespace IndexedRegex
+
+open List
+
+inductive Regex (α: Type): (List α -> Prop) -> Type where
+  | emptyset : Regex α Language.emptyset
+  | emptystr : Regex α Language.emptystr
+  | char : (a: α) → Regex α (Language.char a)
+  | or : Regex α x → Regex α y → Regex α (Language.or x y)
+  | concat : Regex α x → Regex α y → Regex α (Language.concat x y)
+  | star : Regex α x → Regex α (Language.star x)
+
+def null (r: Regex α l): Decidable (Language.null l) :=
+  match r with
+  | Regex.emptyset => Decidable.isFalse (Language.not_null_if_emptyset)
+  | Regex.emptystr => Decidable.isTrue (Language.null_if_emptystr)
+  | Regex.char _ => Decidable.isFalse (Language.not_null_if_char)
+  | Regex.or x y =>
+    Decidable.map (symm Language.null_iff_or)
+      (Decidable.or (null x) (null y))
+  | Regex.concat x y =>
+    Decidable.map (symm Language.null_iff_concat)
+      (Decidable.and (null x) (null y))
+  | Regex.star _ => Decidable.isTrue (Language.null_if_star)
+
+def derive [DecidableEq α] (r: Regex α l) (a: α): Regex α (Language.derive l a) := by
+  sorry

Katydid/Regex/Language.lean

@@ -30,16 +30,16 @@ def and {α: Type} (P : Lang α) (Q : Lang α) : Lang α :=
   fun w => P w /\ Q w
 
 def concat {α: Type} (P : Lang α) (Q : Lang α) : Lang α :=
-  fun (w : List α) =>
-    ∃ (x : List α) (y : List α), P x /\ Q y /\ w = (x ++ y)
+  fun (xs : List α) =>
+    ∃ (ys : List α) (zs : List α), P ys /\ Q zs /\ xs = (ys ++ zs)
 
 inductive All {α: Type} (P : α -> Prop) : (List α -> Prop) where
   | nil : All P []
   | cons : ∀ {x xs} (_px : P x) (_pxs : All P xs), All P (x :: xs)
 
 def star {α: Type} (R : Lang α) : Lang α :=
-  fun (w : List α) =>
-    ∃ (ws : List (List α)), All R ws /\ w = (List.flatten ws)
+  fun (xs : List α) =>
+    ∃ (xss : List (List α)), All R xss /\ xs = (List.flatten xss)
 
 -- attribute [simp] allows these definitions to be unfolded when using the simp tactic.
 attribute [simp] universal emptyset emptystr char onlyif or and concat star
@@ -116,6 +116,14 @@ def null_emptyset {α: Type}:
   @null α emptyset = False :=
   rfl
 
+def null_iff_emptyset {α: Type}:
+  @null α emptyset <-> False := by
+  rw [null_emptyset]
+
+def not_null_if_emptyset {α: Type}:
+  @null α emptyset -> False :=
+  null_iff_emptyset.mp
+
 def null_universal {α: Type}:
   @null α universal = True :=
   rfl
@@ -126,6 +134,10 @@ def null_iff_emptystr {α: Type}:
     (fun _ => True.intro)
     (fun _ => rfl)
 
+def null_if_emptystr {α: Type}:
+  @null α emptystr :=
+  rfl
+
 def null_emptystr {α: Type}:
   @null α emptystr = True := by
   rw [null_iff_emptystr]
@@ -134,6 +146,10 @@ def null_iff_char {α: Type} {c: α}:
   null (char c) <-> False :=
   Iff.intro nofun nofun
 
+def not_null_if_char {α: Type} {c: α}:
+  null (char c) -> False :=
+  nofun
+
 def null_char {α: Type} {c: α}:
   null (char c) = False := by
   rw [null_iff_char]
@@ -142,6 +158,10 @@ def null_or {α: Type} {P Q: Lang α}:
   null (or P Q) = ((null P) \/ (null Q)) :=
   rfl
 
+def null_iff_or {α: Type} {P Q: Lang α}:
+  null (or P Q) <-> ((null P) \/ (null Q)) := by
+  rw [null_or]
+
 def null_and {α: Type} {P Q: Lang α}:
   null (and P Q) = ((null P) /\ (null Q)) :=
   rfl
@@ -170,6 +190,14 @@ def null_star {α: Type} {P: Lang α}:
   · intro l hl
     cases hl
 
+def null_iff_star {α: Type} {P: Lang α}:
+  null (star P) <-> True := by
+  rw [null_star]
+
+def null_if_star {α: Type} {P: Lang α}:
+  null (star P) :=
+  null_iff_star.mpr True.intro
+
 def derive_emptyset {α: Type} {a: α}:
   (derive emptyset a) = emptyset :=
   rfl
@@ -293,17 +321,17 @@ inductive starplus {α: Type} (R: Lang α): Lang α where
     -> starplus R qs
     -> starplus R w
 
-theorem star_is_starplus: ∀ {α: Type} (R: Lang α) (w: List α),
-  star R w -> starplus R w := by
-  intro α R w
+theorem star_is_starplus: ∀ {α: Type} (R: Lang α) (xs: List α),
+  star R xs -> starplus R xs := by
+  intro α R xs
   unfold star
   intro s
   match s with
   | Exists.intro ws (And.intro sl sr) =>
     clear s
     rw [sr]
     clear sr
-    clear w
+    clear xs
     induction ws with
     | nil =>
       simp
@@ -319,6 +347,37 @@ theorem star_is_starplus: ∀ {α: Type} (R: Lang α) (w: List α),
         · assumption
         · assumption
 
+theorem starplus_is_star: ∀ {α: Type} (R: Lang α) (xs: List α),
+  starplus R xs -> star R xs := by
+  intro α R xs
+  intro hs
+  induction xs with
+  | nil =>
+    simp
+    exists []
+    apply And.intro ?_ (by simp)
+    apply All.nil
+  | cons x' xs' ih =>
+    cases hs with
+    | more ps qs _ xxspsqs Rps sRqs =>
+      unfold star
+      have hxs := list_split_cons (x' :: xs')
+      cases hxs with
+      | inl h =>
+        contradiction
+      | inr h =>
+        cases h with
+        | intro x h =>
+        cases h with
+        | intro xs h =>
+        cases h with
+        | intro ys h =>
+        rw [h]
+        have hys := list_split_flatten ys
+        cases hys with
+        | intro yss hyss =>
+        sorry
+
 inductive starcons {α: Type} (R: Lang α): Lang α where
   | zero: starcons R []
   | more: ∀ (p: α) (ps qs w: List α),
@@ -395,8 +454,8 @@ theorem star_is_starcons: ∀ {α: Type} (R: Lang α) (xs: List α),
         | intro h2l h2r =>
         sorry
 
-def derive_iff_star {α: Type} {a: α} {P: Lang α} {w: List α}:
-  (derive (star P) a) w <-> (concat (derive P a) (star P)) w := by
+def derive_iff_star {α: Type} {x: α} {R: Lang α} {xs: List α}:
+  (derive (star R) x) xs <-> (concat (derive R x) (star R)) xs := by
   refine Iff.intro ?toFun ?invFun
   case toFun =>
     sorry

Katydid/Regex/Regex.lean

@@ -97,11 +97,11 @@ def derive [DecidableEq α] (r: Regex α) (a: α): Regex α :=
   match r with
   | Regex.emptyset => Regex.emptyset
   | Regex.emptystr => Regex.emptyset
-  | Regex.char c => Regex.onlyif (a == c) Regex.emptystr
+  | Regex.char c => onlyif (a == c) Regex.emptystr
   | Regex.or x y => Regex.or (derive x a) (derive y a)
   | Regex.concat x y =>
       Regex.or
         (Regex.concat (derive x a) y)
-        (Regex.onlyif (null x) (derive y a))
+        (onlyif (null x) (derive y a))
   | Regex.star x =>
       Regex.concat (derive x a) (Regex.star x)

Katydid/Std/Decidable.lean

@@ -0,0 +1,33 @@
+namespace Decidable
+
+def or {α β: Prop} (a: Decidable α) (b: Decidable β): Decidable (α \/ β) :=
+  match (a, b) with
+  | (Decidable.isFalse a, Decidable.isFalse b) =>
+    Decidable.isFalse (fun ab =>
+      match ab with
+      | Or.inl sa => a sa
+      | Or.inr sb => b sb
+    )
+  | (Decidable.isTrue a, Decidable.isFalse _) =>
+    Decidable.isTrue (Or.inl a)
+  | (_, Decidable.isTrue b) =>
+    Decidable.isTrue (Or.inr b)
+
+def and {α β: Prop} (a : Decidable α) (b : Decidable β) : Decidable (α /\ β) :=
+  match a with
+  | isTrue ha =>
+    match b with
+    | isTrue hb  => isTrue ⟨ha, hb⟩
+    | isFalse hb => isFalse (fun h => hb (And.right h))
+  | isFalse ha =>
+    isFalse (fun h => ha (And.left h))
+
+def map' {α β: Prop} (ab: α -> β) (ba: β -> α) (a: Decidable α): Decidable β :=
+  match a with
+  | Decidable.isTrue a =>
+    Decidable.isTrue (ab a)
+  | Decidable.isFalse nota =>
+    Decidable.isFalse (nota ∘ ba)
+
+def map {α β: Prop} (ab: α <-> β) (a: Decidable α): Decidable β :=
+  map' ab.mp ab.mpr a

Katydid/Std/Lists.lean

@@ -981,3 +981,12 @@ theorem list_split_cons {α: Type} (xs: List α):
     simp only [cons_append, cons.injEq, true_and]
     exists []
     exists ys
+
+theorem list_split_flatten {α: Type} (zs: List α):
+  ∃ (zss: List (List α)), zs = zss.flatten :=
+  match zs with
+  | nil => by
+    exists []
+  | cons x ys => by
+    exists [[x], ys]
+    simp