How to create a state machine from inductive types in Coq?

Question

How could be created a correct state machine (without a way to construct it in invalid way) in Coq entirely from inductive types?

Starting from something like:

Inductive Cmd :=
| Open
| Send
| Close.

Inductive SocketState :=
| Ready
| Opened
| Closed.

For example transition from Ready to Opened should happen only after Open command.

Answer 1

From the formal definition of deterministic finite state machine:

A deterministic finite automaton M is a 5-tuple Q, Sigma, delta, q0, F, consisting of

• a finite set of states Q
• a finite set of input symbols called the alphabet Sigma
• a transition function delta: Q * Sigma -> Q
• an initial or start state q0 in Q
• a set of accept states F being a subset of Q

You gave two out of the five, namely Q = SocketState and Sigma = Cmd. Assuming that your application has an implicit initial state (probably Ready) and no specific "accept states", the only thing needed for your state machine is the transition function.

From the definition, the transition function has the type (SocketState * Cmd) -> SocketState, but the curried version SocketState -> Cmd -> SocketState is equally powerful.

If your state machine has external inputs, add them as parameters to the function. If you want side effects, or some kind of output associated with the transition itself, you can use SocketState -> Cmd -> (SomeOutput * SocketState).

---

Edit: Transition as a relation (Extension to keep_learning's answer)

If you want to reason about a series of valid commands and transitions, you might want to encode it into a ternary relation instead.

First, let's define what constitutes for valid transitions.

Previous state -> (Command) -> Next state
-----------------------------------------
Ready          -> (Open)    -> Opened
Opened         -> (Send)    -> Opened
Opened         -> (Close)   -> Closed

Then, encode it as a ternary relation. The following is just an example, similar to Hoare triples from programming language models.

Inductive Transition : SocketState -> Cmd -> SocketState -> Prop :=
  | t_open  : Transition Ready  Open  Opened
  | t_send  : Transition Opened Send  Opened
  | t_close : Transition Opened Close Closed.

The above talks about a single transition. What about a series of transitions? We can define a reflexive-transitive closure, taking a list of commands (this is very similar to Hoare triples, in the sense that both define a precondition, a sequence of steps, and a postcondition):

From Coq Require Import List.
Import ListNotations.

Inductive TransitionRTC : SocketState -> list Cmd -> SocketState -> Prop :=
  | t_rtc_refl : forall s : SocketState, TransitionRTC s [] s
  | t_rtc_trans1 : forall s1 c s2 clist s3,
      Transition s1 c s2 ->
      TransitionRTC s2 clist s3 ->
      TransitionRTC s1 (c :: clist) s3.

The function analogue of RTC relation would be (the fold_left in Coq has the last two arguments swapped, compared to Haskell's foldl or Ocaml's fold_left):

Axiom transition : SocketState -> Cmd -> SocketState.
Definition multistep_transition (state0 : SocketState) (clist : list Cmd) :=
  fold_left transition clist state0.