## The problem

This problem is originated from HMU’s homework for DFA. The automata is shown by the picture below:

We want to prove a property about this automata’s language : if a string , then the number of “” in is odd.

I can prove it on paper by induction on the length of . But I fail to prove it using coq. I know how to solve the problem “not general” on paper but fail to use the same idea in coq. Here is my question on stackoverflow: https://stackoverflow.com/questions/45872719/how-to-do-induction-on-the-length-of-a-list-in-coq. And this answer helps me solve the problem.

## Proof in informal language

Let’s restate the problem. We have

Here we jsut present how to prove instead of for simplicity.

Let’s prove . We do this by induction on the length of .

- Base case: let’s verify that for all with length , hold. Now, can only either be “” or ““. And it’s satisfied(remember can imply any propositions).
- Inductive Hypothesis: . And let’s try to prove ‘s situation.
- For any , or , and ‘s length is .
- For the case
- if it stops at state , then must stop at state , and according to inductive hypothesis, we know has even s. So hold for .
- if it stops at state , then must stop at state , and according to inductive hypothesis, we know has odd s. So hold for .

- For the case
- if it stops at state , then must stop at state , and according to inductive hypothesis, we know has even $1$s. So hold for .
- if it stops at state , then must stop at state , and according to inductive hypothesis, we know has odd $1$s. So hold for .

- For the case
- So we have proved for (the inductive step).
- We finish our proof.

## Prove using coq

After proving it on paper, I decided to try use coq to verify this property. At first I just want to mimic what I have done on paper but fail to find out how to do induction on list length in coq. So I raised a question in StackOverflow, and someone kindly replied me that all I should do for this concrete problem is to build a more general theorem.

Inspired by the answer, I manage it. The code is here. I also paste the code below:

```
Require Import Coq.Init.Nat.
Require Import Coq.Bool.Bool.
Require Import Coq.Lists.List.
Import ListNotations.
Inductive state : Type :=
| A: state
| B: state.
Inductive input : Type :=
| zero: input
| one: input.
Definition delta (s : state) (n : input) : state :=
match s, n with
| A, zero => A
| A, one => B
| B, zero => B
| B, one => A
end.
Fixpoint extend_delta (s :state) (w : list input) : state :=
match w with
| [] => s
| n :: tl =>
delta (extend_delta s tl) n
end.
Fixpoint one_num (w : list input) : nat :=
match w with
| [] => 0
| one :: tl => S (one_num tl)
| zero :: tl=> one_num tl
end.
Fixpoint listlen (w : list input) : nat :=
match w with
| [] => 0
| hd :: tl => S (listlen tl)
end.
Definition flip_state (s : state) : state :=
match s with
| A => B
| B => A
end.
Lemma odd_even_s : forall (n : nat),
negb (odd n) = (odd (S n)).
Proof.
induction n as [| n' IHn].
- simpl. reflexivity.
- rewrite <- IHn.
apply negb_involutive.
Qed.
Lemma automata221_general : forall (w : list input) (s : state),
extend_delta s w = if odd (one_num w) then (flip_state s) else s.
Proof.
intros w s.
induction w as [|hd tl IHw].
- simpl. reflexivity.
- destruct hd.
+ simpl. rewrite IHw.
destruct (odd (one_num tl)) eqn:H.
* destruct (flip_state s) eqn:H1.
simpl. reflexivity.
simpl. reflexivity.
* destruct s.
reflexivity.
reflexivity.
+ simpl. rewrite IHw.
destruct (odd (one_num tl)) eqn:H.
assert ((odd (S (one_num tl))) = false).
{
rewrite <- odd_even_s.
rewrite H. simpl. reflexivity.
}
rewrite H0.
destruct s.
reflexivity.
reflexivity.
assert ((odd (S (one_num tl))) = true).
{
rewrite <- odd_even_s.
rewrite H.
simpl. reflexivity.
}
rewrite H0.
destruct s.
reflexivity.
reflexivity.
Qed.
Theorem automata221: forall (w : list input),
extend_delta A w = B <-> odd (one_num w) = true.
Proof.
intros w.
split.
- induction w as [|hd tl IHw].
+ simpl. intros H. inversion H.
+ assert (extend_delta A tl = if odd (one_num tl) then (flip_state A) else A).
{
apply automata221_general.
}
destruct hd.
* simpl.
destruct (odd (one_num tl)) eqn:H1.
{
simpl in H.
rewrite H.
simpl. intros. reflexivity.
}
{
rewrite H.
simpl. intros. inversion H0.
}
* simpl.
destruct (odd (one_num tl)) eqn:H1.
{
simpl in H.
rewrite H.
simpl. intros. inversion H0.
}
{
rewrite H.
simpl. intros.
rewrite <- odd_even_s.
rewrite H1.
simpl. reflexivity.
}
- assert (extend_delta A w = if odd (one_num w) then (flip_state A) else A).
{
apply automata221_general.
}
intros.
rewrite H0 in H.
rewrite H.
reflexivity.
Qed.
```

A more concise version is provided in the answer: https://stackoverflow.com/a/45872869/3879009