# Proof of an HMU problem

Contents

## The problem

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

We want to prove a property about this automata’s language $L(A)$: if a string $w \in L(A)$, then the number of  “$1$” in $w$ is odd.

I can prove it on paper by induction on the length of $w$. 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

$P_1: \forall w, \hat{\delta} (A, w) = A \iff w \text{ has even } 1 \text{s} \\ P_2: \forall w, \hat{\delta} (A, w) = B \iff w \text { has odd } 1 \text{s}$

Here we jsut present how to prove $\implies$ instead of $\iff$ for simplicity.

Let’s prove $P_1 \wedge P_2$. We do this by induction on the length of $w$.

• Base case: let’s verify that for  all $w$ with length $1$,  $P_1 \wedge P_2$ hold.  Now, $w$ can only either be “$0$” or “$1$“. And it’s satisfied(remember $False$ can imply any propositions).
• Inductive Hypothesis: $\forall w, length(w) \le l, \hat{\delta}(A, w) = A \implies w \text{ has even } 1 \text{s} \wedge \hat{\delta} (A, w) = B \implies w \text { has odd } 1 \text{s}$. And let’s try to prove $l+1$‘s situation.
• For any $w, length(w)=l+1$, $w = x1$ or $w = y0$, $x$ and $y$‘s length is $l$.
• For the case $w = x1$
• if it stops at state $B$, then $x$ must stop at state $A$, and according to inductive hypothesis, we know  $x$ has even $1$s. So $P_1 \wedge P_2$ hold for $l+1$.
• if it stops at state $A$, then $x$ must stop at state $B$, and according to inductive hypothesis, we know $x$ has odd $1$s. So $P_1 \wedge P_2$ hold for $l +1$.
• For the case $w=y0$
• if it stops at state $A$, then $y$ must stop at state $A$, and according to inductive hypothesis, we know $y$ has even $1$s. So $P_1 \wedge P_2$ hold for $l+1$.
• if it stops at state $B$, then $y$ must stop at state $B$, and according to inductive hypothesis, we know $y$ has odd $1$s. So $P_1 \wedge P_2$ hold for $l+1$.
• So we have proved for $l+1$ (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

This site uses Akismet to reduce spam. Learn how your comment data is processed.