NFA.Path and NFA.IsPath

Stream: mathlib4

[Maja Kądziołka]

I'm working on the formalization of NFAs. Following EpsilonNFA, I have the written the following definition, and proven a few things about it:

/-- `M.IsPath` represents a traversal in `M` from a start state to an end state by following a list
of transitions in order. -/
@[mk_iff]
inductive IsPath : σ → σ → List α → Prop
  | nil (s : σ) : IsPath s s []
  | cons (t s u : σ) (a : α) (x : List α) :
      t ∈ M.step s a → IsPath t u x → IsPath s u (a :: x)

However, since the definition is in Prop, you can't talk about stuff like the set of states visited by a particular path. This suggests a slightly different definition:

inductive Path : σ → σ → List α → Type (max u v)
  | nil (s : σ) : Path s s []
  | cons (t s u : σ) (a : α) (x : List α) :
      t ∈ M.step s a → Path t u x → Path s u (a :: x)

Now, should we still have IsPath? NFAs are different in that there's no need to be explicit about where the epsilon-transitions are being taken, so we have s₂ ∈ M.evalFrom {s₁} x ↔ M.IsPath s₁ s₂ x. But it feels like IsPath could still be useful, for its induction schema if anything?

[Maja Kądziołka]

also, how do I spell "product type" when one part is Type and the other is Prop? currently I have this ugly thing:

def Path.split_of_mem_supp [DecidableEq σ] {x : List α} {s t u : σ} (p : M.Path s u x)
  (h : t ∈ p.supp) : (x₁ x₂ : List α) × M.Path s t x₁ × {whatever : M.Path t u x₂ // x₁ ++ x₂ = x} :=

[Maja Kądziołka]

okay, I've found ×', is it reasonable to use it here?

def Path.split_of_mem_supp [DecidableEq σ] {x : List α} {s t u : σ}
    (p : M.Path s u x) (h : t ∈ p.supp) :
    (x₁ x₂ : List α) × M.Path s t x₁ × M.Path t u x₂ ×' x₁ ++ x₂ = x :=

[Aaron Liu]

Maybe docs#Subtype

[Maja Kądziołka]

okay but i don't care about naming the first element of the pair (see whatever in the example above)

[Maja Kądziołka]

does ×' make sense as an alternative?