Proof of an HMU problem

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 .
• 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