Proof of an HMU problem

Contents hide

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 , or , and ‘s length is .
- For the case
  - 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
  - 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

Thoughts on Computing

英雄无岁，江湖无辈

The problem

Proof in informal language

Prove using coq

Leave a ReplyCancel reply