Complete proof that regular languages are closed under Kleene star

Author: yisiox

TraceTheory/TraceTheory/Computability.lean

@@ -30,9 +30,9 @@ lemma IsPath.concat_lift_inl {εM₁ : εNFA α σ₁} {εM₂ : εNFA α σ₂}
     (h : εM₁.IsPath s t x) : (concat εM₁ εM₂).IsPath (Sum.inl s) (Sum.inl t) x := by
   induction h with
   | nil _ =>
-    exact (εNFA.isPath_nil (concat εM₁ εM₂)).mpr rfl
+    exact (isPath_nil (concat εM₁ εM₂)).mpr rfl
   | cons t' s' u oa x' h_step h_path ih =>
-    apply εNFA.IsPath.cons (Sum.inl t') (Sum.inl s') (Sum.inl u)
+    apply IsPath.cons (Sum.inl t') (Sum.inl s') (Sum.inl u)
     · simp [concat]
       cases oa with
       | some a =>
@@ -45,9 +45,9 @@ lemma IsPath.concat_lift_inr {εM₁ : εNFA α σ₁} {εM₂ : εNFA α σ₂}
     (h : εM₂.IsPath s t x) : (concat εM₁ εM₂).IsPath (Sum.inr s) (Sum.inr t) x := by
   induction h with
   | nil _ =>
-    exact (εNFA.isPath_nil (concat εM₁ εM₂)).mpr rfl
+    exact (isPath_nil (concat εM₁ εM₂)).mpr rfl
   | cons t' s' u _ _ h_step _ ih =>
-    apply εNFA.IsPath.cons (Sum.inr t') (Sum.inr s') (Sum.inr u)
+    apply IsPath.cons (Sum.inr t') (Sum.inr s') (Sum.inr u)
     · simp [concat]
       exact h_step
     · exact ih
@@ -66,7 +66,7 @@ lemma IsPath.concat_proj_inr {εM₁ : εNFA α σ₁} {εM₂ : εNFA α σ₂}
     subst hs' ht'
     simp [concat] at h_step
     rcases h_step with ⟨q, hq, rfl⟩
-    apply εNFA.IsPath.cons q s t
+    apply IsPath.cons q s t
     · exact hq
     · simp [ih]
 
@@ -93,38 +93,36 @@ lemma IsPath.concat_split_inl_inr
       use some a :: u, v, s_acc, s_start
       and_intros
       · simp [hx']
-      · exact εNFA.IsPath.cons q s s_acc (some a) u hq h_path_rest
+      · exact IsPath.cons q s s_acc (some a) u hq h_path_rest
       · exact h_acc
       · exact h_bridge
       · exact h_path_M₂
     | none =>
       by_cases h_mem : s ∈ εM₁.accept
       · simp [concat, h_mem] at h_step
         rcases h_step with ⟨q, hq, rfl⟩ | ⟨q, hq, rfl⟩
-        · have ⟨u, v, s_acc, s_start, hx', h_path_rest, h_acc, h_bridge, h_path_M₂⟩ :=
-            ih (Eq.refl _) (Eq.refl _)
+        · have ⟨u, v, s_acc, s_start, hx', h_path_rest, h_acc, h_bridge, h_path_M₂⟩ := ih rfl rfl
           use none :: u, v, s_acc, s_start
           and_intros
           · simp [hx']
-          · exact εNFA.IsPath.cons q s s_acc none u hq h_path_rest
+          · exact IsPath.cons q s s_acc none u hq h_path_rest
           · exact h_acc
           · exact h_bridge
           · exact h_path_M₂
         · use [], x', s, q
           and_intros
           · simp
-          · exact (εNFA.isPath_nil εM₁).mpr rfl
+          · exact (isPath_nil εM₁).mpr rfl
           · exact h_mem
           · exact hq
           · exact IsPath.concat_proj_inr h_path
       · simp [concat, h_mem] at h_step
         rcases h_step with ⟨q, hq, rfl⟩
-        have ⟨u, v, s_acc, s_start, hx', h_path_rest, h_acc, h_bridge, h_path_M₂⟩ :=
-          ih (Eq.refl _) (Eq.refl _)
+        have ⟨u, v, s_acc, s_start, hx', h_path_rest, h_acc, h_bridge, h_path_M₂⟩ := ih rfl rfl
         use none :: u, v, s_acc, s_start
         and_intros
         · simp [hx']
-        · exact εNFA.IsPath.cons q s s_acc none u hq h_path_rest
+        · exact IsPath.cons q s s_acc none u hq h_path_rest
         · exact h_acc
         · exact h_bridge
         · exact h_path_M₂
@@ -135,7 +133,7 @@ theorem accepts_concat {εM₁ : εNFA α σ₁} {εM₂ : εNFA α σ₂} :
   constructor
   · intro h
     have ⟨q₁, q₂, x', hq₁, hq₂, hx', hεM⟩ :=
-      (εNFA.mem_accepts_iff_exists_path (concat εM₁ εM₂)).mp h
+      (mem_accepts_iff_exists_path (concat εM₁ εM₂)).mp h
     simp [concat] at hq₁ hq₂
     rcases hq₁ with ⟨s, hs, rfl⟩
     rcases hq₂ with ⟨t, ht, rfl⟩
@@ -144,28 +142,28 @@ theorem accepts_concat {εM₁ : εNFA α σ₁} {εM₂ : εNFA α σ₂} :
     apply Language.mem_mul.mpr
     use u'.reduceOption
     constructor
-    · apply (εNFA.mem_accepts_iff_exists_path εM₁).mpr
+    · apply (mem_accepts_iff_exists_path εM₁).mpr
       use s, s_acc, u'
     · use v'.reduceOption
       constructor
-      · apply (εNFA.mem_accepts_iff_exists_path εM₂).mpr
+      · apply (mem_accepts_iff_exists_path εM₂).mpr
         use s_start, t, v'
       · rw [← hx', ← List.reduceOption_append, hx]
         simp [List.reduceOption_append, List.reduceOption_cons_of_none]
   · simp [Language.mul_def, Set.image2]
     rw [Set.mem_setOf_eq]
     intro ⟨u, hu, v, hv, hx⟩
-    have ⟨uq₁, uq₂, u', huq₁, huq₂, hu', hεM₁⟩ := (εNFA.mem_accepts_iff_exists_path εM₁).mp hu
-    have ⟨vq₁, vq₂, v', hvq₁, hvq₂, hv', hεM₂⟩ := (εNFA.mem_accepts_iff_exists_path εM₂).mp hv
-    apply (εNFA.mem_accepts_iff_exists_path (concat εM₁ εM₂)).mpr
+    have ⟨uq₁, uq₂, u', huq₁, huq₂, hu', hεM₁⟩ := (mem_accepts_iff_exists_path εM₁).mp hu
+    have ⟨vq₁, vq₂, v', hvq₁, hvq₂, hv', hεM₂⟩ := (mem_accepts_iff_exists_path εM₂).mp hv
+    apply (mem_accepts_iff_exists_path (concat εM₁ εM₂)).mpr
     use Sum.inl uq₁, Sum.inr vq₂, u' ++ [none] ++ v'
     and_intros
     · simp [concat]
       exact huq₁
     · simp [concat]
       exact hvq₂
     · simp [List.reduceOption_append, hx, hu', hv']
-    · simp only [εNFA.isPath_append]
+    · simp only [isPath_append]
       use (Sum.inr vq₁)
       constructor
       · use (Sum.inl uq₂)
@@ -204,7 +202,7 @@ lemma IsPath.kstar_lift_inr {εM : εNFA α σ} {s t : σ} {x : List (Option α)
   | nil _ =>
     exact (isPath_nil εM.kstar).mpr rfl
   | cons t' s' u oa x' h_step h_path ih =>
-    apply εNFA.IsPath.cons (Sum.inr t') (Sum.inr s') (Sum.inr u)
+    apply IsPath.cons (Sum.inr t') (Sum.inr s') (Sum.inr u)
     · simp [kstar]
       cases oa with
       | some a =>
@@ -213,7 +211,7 @@ lemma IsPath.kstar_lift_inr {εM : εNFA α σ} {s t : σ} {x : List (Option α)
         by_cases h_mem : s' ∈ εM.accept <;> simp [h_mem, h_step]
     · exact ih
 
-lemma exists_kstar_path_inr {εM : εNFA α σ}
+lemma kstar_exists_path_inr {εM : εNFA α σ}
     (L : List (List α)) (h_nonempty : L ≠ []) (h_all : ∀ y ∈ L, y ∈ εM.accepts) :
     ∃ (s : σ) (q : Unit ⊕ σ) (x : List (Option α)),
       s ∈ εM.start ∧
@@ -225,7 +223,7 @@ lemma exists_kstar_path_inr {εM : εNFA α σ}
     contradiction
   | cons y L' ih =>
     have hy := h_all y List.mem_cons_self
-    have ⟨s, t, x, hs, ht, hy', hx⟩ := (εNFA.mem_accepts_iff_exists_path εM).mp hy
+    have ⟨s, t, x, hs, ht, hy', hx⟩ := (mem_accepts_iff_exists_path εM).mp hy
     subst hy'
     cases L' with
     | nil =>
@@ -255,10 +253,210 @@ lemma exists_kstar_path_inr {εM : εNFA α σ}
           · simp [kstar, ht, hs']
           · simp [hx']
 
+lemma kstar_no_return {εM : εNFA α σ} {s : σ} {t : Unit ⊕ σ} {x : List (Option α)}
+    (h : (kstar εM).IsPath (Sum.inr s) t x) : t ≠ Sum.inl () := by
+  generalize hs' : Sum.inr s = s' at h
+  induction h generalizing s with
+  | nil u =>
+    subst hs'
+    simp
+  | cons t' s'' u oa x' h_step h_path ih =>
+    subst hs'
+    have h_next_is_inr : ∃ y, Sum.inr y = t' := by
+      simp [kstar] at h_step
+      cases oa with
+      | some a =>
+        simp at h_step
+        rcases h_step with ⟨y, _, rfl⟩
+        use y
+      | none =>
+        simp at h_step
+        split_ifs at h_step with h_mem
+        · rcases h_step with ⟨y, _, rfl⟩ | ⟨y, _, rfl⟩
+          · use y
+          · use y
+        · rcases h_step with ⟨y, _, rfl⟩
+          use y
+    rcases h_next_is_inr with ⟨y, rfl⟩
+    exact ih rfl
+
+lemma IsPath.kstar_split_inr {s t : σ} {x : List (Option α)}
+    (h : (kstar εM).IsPath (Sum.inr s) (Sum.inr t) x) :
+    (∃ x', x'.reduceOption = x.reduceOption ∧ εM.IsPath s t x') ∨
+    (∃ (u v : List (Option α)) (q_acc : σ) (s_next : σ),
+      x.reduceOption = u.reduceOption ++ v.reduceOption ∧
+      εM.IsPath s q_acc u ∧
+      q_acc ∈ εM.accept ∧
+      s_next ∈ εM.start ∧
+      (kstar εM).IsPath (Sum.inr s_next) (Sum.inr t) v ∧
+      v.length < x.length) := by
+  generalize hs' : Sum.inr s = s' at h
+  generalize ht' : Sum.inr t = t' at h
+  induction h generalizing s with
+  | nil q =>
+    left
+    use []
+    simp
+    cases hs'
+    cases ht'
+    rfl
+  | cons u' s'' t'' oa x'' h_step h_path ih =>
+    subst hs' ht'
+    cases oa with
+    | some a =>
+      simp [kstar] at h_step
+      have ⟨s_next, hs_next, hu'⟩ := h_step
+      rcases ih hu' rfl with
+        ⟨y, hx'', hy⟩ |
+        ⟨u, v, q_acc, s_next', huv, hu, hq_acc, hs_next', hv, hlt⟩
+      · left
+        use some a :: y
+        constructor
+        · simp [hx'']
+        · exact IsPath.cons s_next s t (some a) y hs_next hy
+      · right
+        use some a :: u, v, q_acc, s_next'
+        and_intros
+        · simp [huv]
+        · exact IsPath.cons s_next s q_acc (some a) u hs_next hu
+        · exact hq_acc
+        · exact hs_next'
+        · exact hv
+        · simp
+          exact Nat.lt_add_right 1 hlt
+    | none =>
+      simp [kstar] at h_step
+      split_ifs at h_step with h_mem
+      · simp at h_step
+        rcases h_step with ⟨s_next, hs_next, hu'⟩ | ⟨s_start, hs_start, hu'⟩
+        · rcases ih hu' rfl with
+            ⟨y, hx'', hy⟩ |
+            ⟨u, v, q_acc, s_next', huv, hu, hq_acc, hs_next', hv, hlt⟩
+          · left
+            use none :: y
+            constructor
+            · simp [hx'']
+            · exact cons s_next s t none y hs_next hy
+          · right
+            use none :: u, v, q_acc, s_next'
+            and_intros
+            · simp [huv]
+            · exact IsPath.cons s_next s q_acc none u hs_next hu
+            · exact hq_acc
+            · exact hs_next'
+            · exact hv
+            · simp
+              exact Nat.lt_add_right 1 hlt
+        · right
+          use [], x'', s, s_start
+          and_intros
+          · simp
+          · exact (isPath_nil εM).mpr rfl
+          · exact h_mem
+          · exact hs_start
+          · simp [hu', h_path]
+          · simp
+      · simp at h_step
+        rcases h_step with ⟨s_next, hs_next, hu'⟩
+        rcases ih hu' rfl with
+          ⟨y, hx'', hy⟩ |
+          ⟨u, v, q_acc, s_next', huv, hu, hq_acc, hs_next', hv, hlt⟩
+        · left
+          use none :: y
+          constructor
+          · simp [hx'']
+          · exact IsPath.cons s_next s t none y hs_next hy
+        · right
+          use none :: u, v, q_acc, s_next'
+          and_intros
+          · simp [huv]
+          · exact IsPath.cons s_next s q_acc none u hs_next hu
+          · exact hq_acc
+          · exact hs_next'
+          · exact hv
+          · simp
+            exact Nat.lt_add_right 1 hlt
+
+lemma IsPath.kstar_exists_decomp {εM : εNFA α σ} {s t : σ} {x : List (Option α)}
+    (h : (kstar εM).IsPath (Sum.inr s) (Sum.inr t) x)
+    (hs : s ∈ εM.start) (ht : t ∈ εM.accept) :
+    ∃ (L : List (List α)), L.flatten = x.reduceOption ∧ ∀ y ∈ L, y ∈ εM.accepts := by
+  generalize h_len : x.length = n
+  induction n using Nat.strong_induction_on generalizing s x with
+  | h n ih =>
+    rcases IsPath.kstar_split_inr h with
+      ⟨x', hx, hx'⟩ |
+      ⟨u, v, q_acc, s_next, hx, hu, h_acc, h_next, hv, hlt⟩
+    · use [x'.reduceOption]
+      constructor
+      · simp [hx]
+      · intro y hy
+        simp at hy
+        subst hy
+        apply (mem_accepts_iff_exists_path εM).mpr
+        use s, t, x'
+    · have hu_acc : u.reduceOption ∈ εM.accepts := by
+        apply (mem_accepts_iff_exists_path εM).mpr
+        use s, q_acc, u
+      subst h_len
+      have ⟨L', hv', hL'⟩ := ih v.length hlt hv h_next rfl
+      use u.reduceOption :: L'
+      constructor
+      · simp [hv', hx]
+      · intro y hy
+        simp at hy
+        rcases hy with hy | hy
+        · simp [hu_acc, hy]
+        · exact hL' y hy
+
 theorem accepts_kstar {εM : εNFA α σ} : (kstar εM).accepts = (εM.accepts)∗ := by
   ext x
   constructor
-  · sorry
+  · intro h
+    rw [Language.kstar_def, Set.mem_setOf_eq]
+    have ⟨s, t, x', hs, ht, hx, h_path⟩ := (mem_accepts_iff_exists_path εM.kstar).mp h
+    match t with
+    | Sum.inl _ =>
+      use []
+      simp [kstar] at hs
+      simp [hs] at h_path
+      cases h_path with
+      | nil _ =>
+        simpa using hx
+      | cons t' s' u oa x'' h_step h_path =>
+        simp [kstar] at h_step
+        cases oa with
+        | some a =>
+          simp at h_step
+        | none =>
+          simp at h_step
+          rcases h_step with ⟨y, _, rfl⟩
+          have h_absurd := kstar_no_return h_path
+          contradiction
+    | Sum.inr t' =>
+      cases x' with
+      | nil =>
+        simp [kstar] at hs h_path
+        subst hs
+        contradiction
+      | cons oa x'' =>
+        rw [← List.singleton_append, isPath_append] at h_path
+        have ⟨u, hsu, hut⟩ := h_path
+        simp [kstar] at hs
+        subst hs
+        cases oa with
+        | some a =>
+          simp [kstar] at hsu
+        | none =>
+          simp [kstar] at hsu ht
+          rcases hsu with ⟨u', hu', hu⟩
+          subst hu
+          have ⟨L, hx', hL⟩ := IsPath.kstar_exists_decomp hut hu' ht
+          use L
+          constructor
+          · simp at hx
+            simp [hx, hx']
+          · exact hL
   · intro h
     rw [Language.kstar_def, Set.mem_setOf_eq] at h
     rcases h with ⟨L, hx, hL⟩
@@ -270,7 +468,7 @@ theorem accepts_kstar {εM : εNFA α σ} : (kstar εM).accepts = (εM.accepts)
     | cons l L' =>
       expose_names
       have h_nonempty : l :: L' ≠ [] := by simp
-      have ⟨s, q, x', hs, hq, hL', hx'⟩ := exists_kstar_path_inr (l :: L') h_nonempty hL
+      have ⟨s, q, x', hs, hq, hL', hx'⟩ := kstar_exists_path_inr (l :: L') h_nonempty hL
       use Sum.inl (), q, none :: x'
       and_intros
       · simp [kstar]