## Stream: Coq users

### Topic: Encoding and reasoning about FSMs

#### Soren (May 28 2020 at 18:53):

I have a `IsEmpty: MyState -> Prop` and `Steps: MyState -> list MyState`. I want to prove that, for every starting state that satisfies `IsEmpty`, there exists at least one state that satisfies `IsEmpty` after exactly 10 steps. Is there a good guide/example on how to prove stuff FSM stuff like this with Coq?

Additionally, is it possible to _enumerate_ valid `IsEmpty` output states given an input state?

#### Karl Palmskog (May 28 2020 at 19:18):

something with type `MyState -> list MyState` is not necessarily an FSM, so it can't be proven in general. If you're looking for more carefully constructed Coq types for which FSM properties hold, see https://github.com/coq-community/reglang

If `MyState` is indeed finite you can show that it is a finite type (`finType`) and hook into all the results about, e.g., DFAs and NFAs. finTypes give access to all kinds of enumerations as lists/finite sets.

#### Soren (May 28 2020 at 19:25):

Ah, `MyState -> list MyState` is the list of "next" states by a certain transformation. I'm certain I can express it as a DFA, I'll check that out.

#### Karl Palmskog (May 28 2020 at 19:31):

first step would simply be to prove that `MyState` is finite by defining a list with type members and showing that the list is sound and complete. This means that `MyState -> list MyState` can be expressed as a finite function (`finfun`), which is essentially what NFAs and DFAs use for their transition relation. Note that if your only goal is to prove a simple reachability property, reglang might be considered a heavyweight library, so you could also take a look at https://github.com/coq-community/atbr or https://github.com/damien-pous/relation-algebra for other encodings of FSMs.

#### Soren (May 28 2020 at 19:49):

I'll probably use reglang just in case I need to do more with it than prove reachability

#### Christian Doczkal (May 29 2020 at 08:04):

@Soren As the main developer of the `reglang` package, I would be happy to know if the library turns out useful for you or not, and for what reason. IIRC, the representation for "finite automata" in `relation-algebra` is matrices over regular expressions (elements of a Kleene algebra), with NFAs carved out as a predicate. Can't say much about `atbr` except that that I recall the automata model do be geared for execution (the statespace ist described as "all n below a given bound") rather than for simple proofs (by using finite types).

Last updated: Jun 18 2024 at 00:02 UTC