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?

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.

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.

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.

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

@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: Oct 03 2023 at 04:02 UTC