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
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.
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: Jan 27 2023 at 02:04 UTC