automaton.v

Require Import List.
Import ListNotations.

Inductive State := Q1 | Q2.
Inductive Alphabet := A | B.

Inductive trans : State -> Alphabet -> State -> Prop :=
| tr1A : trans Q1 A Q2
| tr1B : trans Q1 B Q1
| tr2A : trans Q2 A Q1
| tr2B : trans Q2 B Q2.

Inductive acceptb : State -> list Alphabet -> bool -> Prop :=
| accept : acceptb Q1 [] true
| notacc : acceptb Q2 [] false
| consacc : forall q q' c str b,
    acceptb q' str b -> trans q c q' -> acceptb q (c::str) b.

Hint Constructors trans acceptb.

Example ex2 : { b | acceptb Q1 [A;B;B;A;A;B;A] b }.
eexists.
eauto 10.
Defined.

Eval simpl in proj1_sig ex2.