Soren (May 28 2020 at 18:53): 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: Oct 13 2024 at 01:02 UTC