State-machines in Coq

Question

Can I use Coq to prove that a state machine cannot reach an invalid state? How?

Answer 1

Here is how to translate stm from here to Coq.

Require Import Coq.Lists.List.                                                                                                                                                                

Inductive alpha : Set := A | B | C | D.

Fixpoint s1 (xs : list alpha) : bool :=
  match xs with
    | C :: rest => s2 rest
    | _ => false
  end

with s2 (xs : list alpha) : bool :=
  match xs with
    | nil => true
    | A :: rest => s2 rest
    | B :: rest => s2 rest
    | C :: rest => s3 rest
    | _ => false
  end

with s3 (xs : list alpha) : bool :=
  match xs with
    | D :: rest => s2 rest
    | _ => false
  end.

Here is the theorem stating that STM can't reach invalid state:

Theorem t : forall xs, s1 xs = false.

But obviously it is not true for this STM. In general case it could be proved by induction.

It will be easier to help you if you provide some more information on what is your actual state machine.