feat(Computability/EpsilonNFA): define path relation

Mathlib/Computability/EpsilonNFA.lean

@@ -1,9 +1,10 @@
 /-
 Copyright (c) 2021 Fox Thomson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Fox Thomson, Yaël Dillies
+Authors: Fox Thomson, Yaël Dillies, Anthony DeRossi
 -/
 import Mathlib.Computability.NFA
+import Mathlib.Data.List.ReduceOption
 
 /-!
 # Epsilon Nondeterministic Finite Automata
@@ -63,6 +64,18 @@ theorem εClosure_empty : M.εClosure ∅ = ∅ :=
 theorem εClosure_univ : M.εClosure univ = univ :=
   eq_univ_of_univ_subset <| subset_εClosure _ _
 
+theorem mem_εClosure_iff_exists {s : σ} {S : Set σ} :
+    s ∈ M.εClosure S ↔ ∃ t ∈ S, s ∈ M.εClosure {t} where
+  mp h := by
+    induction' h with s _ _ _ _ _ ih
+    · tauto
+    · obtain ⟨s, _, _⟩ := ih
+      use s
+      solve_by_elim [εClosure.step]
+  mpr := by
+    intro ⟨_, _, h⟩
+    induction' h <;> subst_vars <;> solve_by_elim [εClosure.step]
+
 /-- `M.stepSet S a` is the union of the ε-closure of `M.step s a` for all `s ∈ S`. -/
 def stepSet (S : Set σ) (a : α) : Set σ :=
   ⋃ s ∈ S, M.εClosure (M.step s a)
@@ -103,6 +116,13 @@ theorem evalFrom_empty (x : List α) : M.evalFrom ∅ x = ∅ := by
   · rw [evalFrom_nil, εClosure_empty]
   · rw [evalFrom_append_singleton, ih, stepSet_empty]
 
+theorem mem_evalFrom_iff_exists {s : σ} {S : Set σ} {x : List α} :
+    s ∈ M.evalFrom S x ↔ ∃ t ∈ S, s ∈ M.evalFrom {t} x := by
+  induction' x using List.reverseRecOn with _ _ ih generalizing s
+  · apply mem_εClosure_iff_exists
+  · simp_rw [evalFrom_append_singleton, mem_stepSet_iff, ih]
+    tauto
+
 /-- `M.eval x` computes all possible paths through `M` with input `x` starting at an element of
 `M.start`. -/
 def eval :=
@@ -124,6 +144,107 @@ theorem eval_append_singleton (x : List α) (a : α) : M.eval (x ++ [a]) = M.ste
 def accepts : Language α :=
   { x | ∃ S ∈ M.accept, S ∈ M.eval x }
 
+/-- `M.IsPath` represents a traversal in `M` from a start state to an end state by following a list
+  of transitions in order. -/
+inductive IsPath : σ → σ → List (Option α) → Prop
+  | nil : ∀ s, IsPath s s []
+  | cons (t s u : σ) (a : Option α) (x : List (Option α)) :
+      t ∈ M.step s a → IsPath t u x → IsPath s u (a :: x)
+
+theorem IsPath.eq_of_nil {s t : σ} : M.IsPath s t [] → s = t := by
+  rintro ⟨⟩
+  rfl
+
+@[simp]
+theorem isPath_singleton {s t : σ} {a : Option α} : M.IsPath s t [a] ↔ t ∈ M.step s a where
+  mp := by
+    rintro (_ | ⟨_, _, _, _, _, _, ⟨⟩⟩)
+    assumption
+  mpr := by tauto
+
+alias ⟨_, IsPath.singleton⟩ := isPath_singleton
+
+theorem isPath_append {s u : σ} {x y : List (Option α)} :
+    M.IsPath s u (x ++ y) ↔ ∃ t, M.IsPath s t x ∧ M.IsPath t u y where
+  mp := by
+    induction' x with _ _ ih generalizing s
+    · rw [List.nil_append]
+      tauto
+    · rintro (_ | ⟨_, _, _, _, _, _, h⟩)
+      apply ih at h
+      tauto
+  mpr := by
+    intro ⟨_, hx, _⟩
+    induction x generalizing s <;> cases hx <;> tauto
+
+theorem εClosure_path {s₁ s₂ : σ} :
+    s₂ ∈ M.εClosure {s₁} ↔ ∃ n, M.IsPath s₁ s₂ (List.replicate n none) where
+  mp h := by
+    induction' h with t _ _ _ _ _ ih
+    · use 0
+      subst t
+      apply IsPath.nil
+    · obtain ⟨n, _⟩ := ih
+      use n + 1
+      rw [List.replicate_add, isPath_append]
+      tauto
+  mpr := by
+    intro ⟨n, h⟩
+    induction n generalizing s₂
+    · rw [List.replicate_zero] at h
+      apply IsPath.eq_of_nil at h
+      solve_by_elim
+    · simp_rw [List.replicate_add, isPath_append, List.replicate_one, isPath_singleton] at h
+      obtain ⟨_, _, _⟩ := h
+      solve_by_elim [εClosure.step]
+
+theorem evalFrom_path {s₁ s₂ : σ} {x : List α} :
+    s₂ ∈ M.evalFrom {s₁} x ↔ ∃ x', x'.reduceOption = x ∧ M.IsPath s₁ s₂ x' := by
+  induction' x using List.reverseRecOn with _ a ih generalizing s₂
+  · rw [evalFrom_nil, εClosure_path]
+    constructor
+    · intro ⟨n, _⟩
+      use List.replicate n none
+      rw [List.reduceOption_replicate_none]
+      trivial
+    · simp_rw [List.reduceOption_eq_nil_iff]
+      rintro ⟨_, ⟨⟨_, ⟨⟩⟩, _⟩⟩
+      tauto
+  · rw [evalFrom_append_singleton, mem_stepSet_iff]
+    constructor
+    · intro ⟨_, ht, h⟩
+      obtain ⟨x', _, _⟩ := ih.mp ht
+      rw [mem_εClosure_iff_exists] at h
+      simp_rw [εClosure_path] at h
+      obtain ⟨_, _, ⟨n, _⟩⟩ := h
+      use x' ++ some a :: List.replicate n none
+      rw [List.reduceOption_append, List.reduceOption_cons_of_some,
+        List.reduceOption_replicate_none, isPath_append]
+      tauto
+    · simp_rw [← List.concat_eq_append, List.reduceOption_eq_concat_iff,
+        List.reduceOption_eq_nil_iff]
+      rintro ⟨_, ⟨_, _, ⟨⟩, _, ⟨_, ⟨⟩⟩⟩, h⟩
+      rw [isPath_append] at h
+      obtain ⟨t, _, _ | _⟩ := h
+      use t
+      rw [mem_εClosure_iff_exists, ih]
+      simp_rw [εClosure_path]
+      tauto
+
+theorem mem_accepts_iff_exists_path {x : List α} :
+    x ∈ M.accepts ↔
+      ∃ s₁ s₂ x', s₁ ∈ M.start ∧ s₂ ∈ M.accept ∧ x'.reduceOption = x ∧ M.IsPath s₁ s₂ x' where
+  mp := by
+    intro ⟨_, _, h⟩
+    rw [eval, mem_evalFrom_iff_exists] at h
+    obtain ⟨_, _, h⟩ := h
+    rw [evalFrom_path] at h
+    tauto
+  mpr := by
+    intro ⟨_, _, _, hs₁, _, h⟩
+    have := M.mem_evalFrom_iff_exists.mpr ⟨_, hs₁, M.evalFrom_path.mpr ⟨_, h⟩⟩
+    tauto
+
 /-! ### Conversions between `εNFA` and `NFA` -/