Advices wanted on modeling finite executions

Stream: general

[Ching-Tsun Chou]

I'm developing some automata theory, in which automata and finite executions of automata are modeled as follows (where A is the type of an "alphabet"):

class Automata (A : Type*) where
  State : Type*
  init : Set State
  next : State → A → Set State

variable {A : Type*}

def FinRun (M : Automata A) (n : ℕ) (as : Fin n → A) (ss : Fin (n + 1) → M.State) :=
  ss 0 ∈ M.init ∧ ∀ k : Fin n, ss (k + 1) ∈ M.next (ss k) (as k)

Unfortunately, working with Fin types proved to be extremely painful. I found that it is much easier to work with infinite sequences whose elements are Option types:

def OptFinRun (M : Automata A) (n : ℕ) (as' : ℕ → Option A) (ss' : ℕ → Option M.State) :=
  (∃ s0 ∈ M.init, ss' 0 = some s0) ∧
  (∀ k < n, ∃ sk ak sk_1, sk_1 ∈ M.next sk ak ∧ ss' k = some sk ∧ as' k = some ak ∧ ss' (k + 1) = some sk_1)

This works, but then I have to move back and forth between FinRun and OptFinRun, which is straightforward but very tedious. So I'm wondering whether it is a good idea to require that the types A and M.State to be inhabited, so that finite sequences can be modeled by infinite sequences whose elements are default from some point on and I can make definitions like the following:

variable [Inhabited A] (M : Automata A) [Inhabited M.State]

def FinRun' (M : Automata A) (n : ℕ) (as : ℕ → A) (ss : ℕ → M.State) :=
  ss 0 ∈ M.init ∧ ∀ k < n, ss (k + 1) ∈ M.next (ss k) (as k)

My general question is: Is this a good idea? Does it look strange from a stylistic POV to use infinite sequences when we are really talking about finite sequences? (Mathematically I think it is perfectly fine and we are not interested in automata whose alphabet or states are uninhabited types anyway.)

I also have a technical question: How do I bundle the [Inhabited M.State] assumption into the class definition of Automata. I tried but it doesn't work.

[Marcus Rossel]

Isn't a finite sequence over type A just a List A? Or if you really want to include the length, then a Vector A n. Then you'd get something like:

def FinRun (M : Automata A) (n : ℕ) (as : Vector A n) (ss : Vector M.State (n + 1)) :=
  ss[0] ∈ M.init ∧ ∀ k : Fin n, ss[k.succ] ∈ M.next ss[k] as[k]

[Ching-Tsun Chou]

I should have given more context: I want my automata to work on both finite and infinite sequences. It is natural to model infinite executions with functions of type ℕ → .... The following is what I've got so far (sorry, no comments in the code yet):
https://github.com/ctchou/AutomataTheory.git
So far I've proved that regular languages are closed under union, intersection, and complementation and that omega-regular languages are closed under union and intersection. The next step is to prove that omega-regular languages are closed under complementation, which is highly nontrivial. Note that I do use lists to model finite words (see AutomataBasic.lean and RegLang.lean).

As to your specific proposal, I can say from painful personal experience that even the ∀ k : Fin n will give your plenty of trouble when you try to prove the theorem automata_pset_opt_fin_run in AutomataPSet.lean. This is because you'll need to deal with Fin types of different sizes and converting between them. That's why I ended up reasoning about OptFinRun, even though that requires me to translate the result back to FinRun.

[Ching-Tsun Chou]

My experience with Fin types is that simp doesn't really work and there are no effective decision procedures. In contrast, simp works great on Nat and all the trivial results can be blasted away using omega. So I would avoid Fin as much as possible.

[Malvin Gattinger]

The problem reminded me of docs#SimpleGraph.Walk which is defined inductively. You could doe something like this?

import Mathlib -- No idea what imports you had before ;-)

class Automata (A : Type*) where
  State : Type*
  init : Set State
  next : State → A → Set State

variable {A : Type*}

def FinRun' (M : Automata A) (n : ℕ) (as : Fin n → A) (ss : Fin (n + 1) → M.State) :=
  ss 0 ∈ M.init ∧ ∀ k : Fin n, ss (k + 1) ∈ M.next (ss k) (as k)

inductive FinPathFrom (M : Automata A) (x : M.State)
  | nil : FinPathFrom M x
  | step {a y} : y ∈ M.next x a → FinPathFrom M x

inductive FinRun (M : Automata A)
  | go : x ∈ M.init → FinPathFrom M x → FinRun M

def FinPathFrom.toList : FinPathFrom M x → List M.State := sorry

def FinRun.toList : FinRun M → List M.State := sorry

[Ching-Tsun Chou]

Note that I want to treat both finite and infinite executions in as uniform a fashion as possible. I'm not sure how the inductive approach can deal with infinite executions.

[Ching-Tsun Chou]

I think what I'm going to do is this: I'll give two definitions of FinRun:

def FinRun (M : Automaton A) (n : ℕ) (as : Fin n → A) (ss : Fin (n + 1) → M.State) :=
  ss 0 ∈ M.init ∧ ∀ k : Fin n, ss (k + 1) ∈ M.next (ss k) (as k)

def FinRun' (M : Automaton A) (n : ℕ) (as : ℕ → A) (ss : ℕ → M.State) :=
  ss 0 ∈ M.init ∧ ∀ k < n, ss (k + 1) ∈ M.next (ss k) (as k)

Then I'll prove that they are basically equivalent (modulo certain Inhabited assumptions):

variable (M : Automaton A) (n : ℕ)

theorem FinRun_lemma1 (as : ℕ → A) (ss : ℕ → M.State) (h : FinRun' M n as ss) :
    FinRun M n (fun k ↦ as k) (fun k ↦ ss k) := by
  sorry

theorem FinRun_lemma2 (as : Fin n → A) (ss : Fin (n + 1) → M.State) (h : FinRun M n as ss) :
    ∀ as', (∀ k : Fin n, as' k = as k) → ∀ ss', (∀ k : Fin (n + 1), ss' k = ss k) → FinRun' M n as' ss' := by
  sorry

theorem FinRun_lemma3 [Inhabited A] [Inhabited M.State] (as : Fin n → A) (ss : Fin (n + 1) → M.State)
    (h : FinRun M n as ss) : ∃ as' ss', FinRun' M n as' ss' := by
  sorry

Then I'll use the second definition FinRun' exclusively.

[Yaël Dillies]

@Ching-Tsun Chou, may we diagnose the precise issues you encountered with Fin before you start advising people against it?

[Ching-Tsun Chou]

I raised some of the issues here:
#new members > Reasoning about Fin types
and here:
#new members > Inductive definition on (Fin n)?

[Ching-Tsun Chou]

In general, when we have Fin types of different sizes and perhaps also Nat, simp doesn't work well and often inserts many cast operations. Also, there is no really effective decision procedure for Fin. In contrast, if we have only Nat and a bunch of (in)equalities about Nat, simp works like a charm and omega blasts away all remaining goals.

[Ching-Tsun Chou]

When I tried to prove the theorem automata_pset_opt_fin_run in:
https://github.com/ctchou/AutomataTheory/blob/main/AutomataTheory/AutomataPSet.lean
I started with FinRun and k : Fin (n + 1) in the statement of theorem. I spent a couple of days trying to prove it but encountered along the way all sorts of trivial propositions about Fin types that I had to manually discharge. Some of them I could prove, not in any systematic way but relying on being lucky with rw?, simp?, and apply?. Some of them I just couldn't prove and had to ask on Zulip (see above). In desperation I decided to pay the price of lifting everything via Option and work in Nat. Then I found I could prove everything, even though it was slow and tedious to pack and unpack through the many existential quantifiers necessitated by using Option.

[Malvin Gattinger]

Hm, I recognize some of the struggles in your other questions, and also would love to have something like "omega working for Fin". What I did not see in the other threads yet is that, maybe because you already know anyway: you can use cases or rcases to go from Fin to Nat plus < statement. A Fin is just a pair of those. That should give you the equivalence of FinRun and FinRun'.

(Meta: it helps for people to help you if you provide #mwe code blocks that are self-contained.)

[Ching-Tsun Chou]

I started refactoring my code to use the new definition of FinRun and proved that the new and old definitions are equivalent under the assumption that the "alphabet" A is inhabited:
https://github.com/ctchou/AutomataTheory/blob/new-fin-run-1/AutomataTheory/AutomataBasic.lean
One nice thing I noticed is that I don't even need to assume any state types to be nonempty.

The above is currently in a side branch because I have not yet refactored other files to use the new definition. I expect them to become simpler and (in some cases) shorter.

[Ching-Tsun Chou]

I have completed refactoring my code to use the new FinRun definition:
https://github.com/ctchou/AutomataTheory/tree/main
The following commit shows particularly clearly how the new definition simplifies the proofs:
https://github.com/ctchou/AutomataTheory/commit/086c096d245118955119f8012c521f7c12066d9a
It occurred to me that the new FinRun definition basically regards a finite sequence as the equivalence class of all infinite sequences that have that finite sequence as a prefix and reason about finite sequences using infinite sequence representatives.
My next step is to formalize the concatenation of languages and their corresponding automata constructions, where I think not having to deal with Fin types will be very helpful indeed.

[Shreyas Srinivas]

Are you looking for something like this

[Shreyas Srinivas]

It has the nice feature that if your automata’s “run” terminates, you can model it as if the automata stays there forever

[Shreyas Srinivas]

That being said, since you are only working with finite word automaton, I don’t see the benefit of streams. If you are working on infinite word automaton, the conceptual content is sufficiently different from the finite word automata context to justify a separate treatment

[Ching-Tsun Chou]

I'm working on both finite word automata and infinite word automata. They shares the class Automaton, which do not include any accepting condition. I don't need possibly infinite sequence.