Im trying to define a generalized DFA in COQ. I think I did it with this
But Now I am trying to make an example DFA that accepts strings with an even number of 1s. (which i can’t attach because i can only attach one image)
The problem I’m running into is saying that it accepts all strings that have an even number of 1s. I think we would do that by saying that if it is in state A then it is accepted because that means it is even. Can anyone provide any guidance? I don’t have any professors to reach out to as we’re not using COQ in my class
May I assume your automata has two states : A and B, A being both initial and accepting,
with transitions A -> 0 ->A, A -> 1 -> B, B -> 0 -> B, B -> 1 -> A ?
You may define a function run: state -> list Alphabet -> state, then prove a lemma of the form forall w q, (w has an even number of 1s) <-> run q w = q.
Once proven this property on both states, you can apply it to A.
1 Like
This is actually our code for the example dfa that accepts strings with an even number of 1s.
Inductive dfa1_alphabet : Type :=
| one
| zero.
Inductive dfa1_states : Type :=
| A
| B.
(** s indicates it is a list of states, a indicates it is a list alphabet input **)
Notation “s[ x ; … ; y ]” := (cons dfa1_states x … (cons dfa1_states y(nil dfa1_states))…).
Notation “a[ x ; … ; y ]” := (cons dfa1_alphabet x … (cons dfa1_alphabet y(nil dfa1_alphabet))…).
Example test1 : length_of_list dfa1_alphabet a[one;zero] = S(S O).
Proof. simpl. reflexivity. Qed.
Definition dfa1 : dfa dfa1_states dfa1_alphabet := {|
start_state := A;
all_states := s[A;B];
is_accepting_state state :=
match state with
| A => true
| B => false end;
transition s x :=
match s, x with
| A, zero => A
| A, one => B
| B, zero => B
| B, one => A
end;
|}.
(** To show that this DFA only accepts input with even number of 1’s
we must first define what evenness is, then count how many 1’s there are.
This is done with the following fixpoint **)
Fixpoint even (n:nat) : bool :=
match n with
| O => true
| S O => false
| S (S n’) => even n’
end.
Fixpoint count_occurrences_of_ones (s : list dfa1_alphabet) : nat :=
match s with
| nil _ => O
| cons _ h t =>
match h with
| one => S ( count_occurrences_of_ones t)
| zero => (count_occurrences_of_ones t)
end
end.
Example test_even_ones_true : even (count_occurrences_of_ones a[one;one]) = true.
Proof. simpl. reflexivity. Qed.
Example test_even_ones_false : even (count_occurrences_of_ones a[one;zero]) = false.
Proof. simpl. reflexivity. Qed.
So I’m guessing it would look something like
Definition run_DFA1 list dfa1_alphabet dfa1States:=
?
I’m sorry I’m not very familiar with coq
You may try the following definition:
Definition transition q x :=
match q, x with
_, zero => q
| A, one => B
| B, one => A
end.
Fixpoint run w q := match w with
nil => q
| x::w' => run w' (transition q x)
end.
Compute run [zero;one;one;zero;one; zero] A.
Compute run [one; zero;one;one;zero;one; zero] A.
A possible way to solve the exercise (thanks to the symmetry of the automaton):
Definition P w := even (count_occurrences_of_ones w)= true.
Lemma OK: forall w q, run w q = q <-> P w.
(* Proof by induction on w *)
Otherwise, you could prove that every run starting from A leads to A iff w has an even number of 1s, and leads to B otherwise. But the proof by induction may be a little longer with this definition of run.
It is perhaps simpler to focus on the accepting state, and prove that any run which arrives at A has the Property P if and only if the run has started on A.
1 Like
Ah I see. Thank you so much for your time I greatly appreciate it! @casteran