前からやりたいと思っていたCoqを初めてみる。心が沈んで何もする気がしなかったのだけれど、夜の12時くらいに何となくCoqを書き出してみると、久しぶりに味わうような高揚感があり気がつくと朝に。自分の単純さがちょっとおかしくなる。

入門となる資料としては、主に Software Foundations を参考にしたのだけれど、どうも古いバージョンに基づいた記述なのか、そのままじゃ動かないところがあった。

Software Foundationsに載っているExerciseを一つ一つやるのも面倒くさかったので、Proof By Inductionの Advanced Exercise として載っていた、SuccとZeroによる自然数の表現と二進数としての表現の間の変換が正しいことの証明を行ってみることに。二進表現の一番上の桁に無駄に0が入ってしまわないように正規化しないと同じ自然数に複数の二進表現が対応してしまう。Exerciseでは列表現を二進表現にしてまた列表現に戻して元の表現になることだけを示せば良いのでこのことは問題にならないが、さらに正規化されているなら二進表現を列表現にしてまた二進表現にして元の表現が帰ることを確かめる証明も自分で行った。

とりあえず証明のコード。試行錯誤で書いてみたが、全然綺麗に書けていない。CoqIDEを使うと仮定の中身を示してくれるので仮定の名前を適当にしたまま証明が書けてしまうが、後から読み返すと読みづらい。あと、途中まで簡約した上でrewriteすれば済むところを、rewriteの対象となるtermおよびrewriteに用いるequationの両方をsimplしてからrewriteしているところがあるのだけど、途中まで簡約するのはどうするのだろうか、もしくはこういうのはsimplしてしまうのが一般的なのだろうか？

話がそれるけれど、GNU Source-highlightはCoqに対応していないのね……。Camlのシンタックスハイライト扱いにしてお茶を濁したけれど、Pygmentを使ってみるのも良いのかもしれない。

Inductive binary := Eb : binary | Zb : binary -> binary | Sb : binary -> binary.

Fixpoint bin_to_nat b :=
  match b with
    | Eb => 0
    | Zb b' => bin_to_nat b' + bin_to_nat b'
    | Sb b' => S (bin_to_nat b' + bin_to_nat b')
  end.

Fixpoint succ_bin b :=
  match b with
    | Eb => Sb Eb
    | Zb b' => Sb b'
    | Sb b' => Zb (succ_bin b')
  end.

Fixpoint nat_to_bin n :=
  match n with
    | 0 => Eb
    | S n => succ_bin (nat_to_bin n)
  end.

Lemma plus_n_Sm : forall n m : nat, n + S m = S (n + m).
  intros n m.
  induction n.
    reflexivity.
    simpl. rewrite -> IHn. reflexivity.
  Qed.

Lemma homo_succ : forall b : binary, bin_to_nat (succ_bin b) = S (bin_to_nat b).
  intros b.
  induction b.

    reflexivity.

    reflexivity.

    simpl.
    assert (forall n : nat, (S n) + (S n) = S (S (n + n))).
      intros n.
      induction n.
        reflexivity.
        simpl. rewrite -> plus_n_Sm. reflexivity.
    rewrite -> IHb. rewrite -> H.
    reflexivity.
  Qed.

Theorem id_nat_bin_nat : forall n : nat, bin_to_nat (nat_to_bin n) = n.
  intros n.
  induction n.
    reflexivity.
    simpl. rewrite -> homo_succ. rewrite -> IHn. reflexivity.
  Qed.

Inductive regular_bin : binary -> Prop :=
  | regular_se : regular_bin (Sb Eb)
  | regular_zind : forall b, regular_bin b -> regular_bin (Zb b)
  | regular_sind : forall b, regular_bin b -> regular_bin (Sb b).

Lemma homo_double_z : forall n : nat, nat_to_bin (n + n) = match n with 0 => Eb | S _ => Zb (nat_to_bin n) end.
  destruct n.
    reflexivity.
    induction n.
      reflexivity.
      rewrite plus_n_Sm. simpl. simpl in IHn. rewrite IHn. reflexivity.
  Qed.

Lemma regular_z : forall b : binary, regular_bin b -> bin_to_nat b = 0 -> b = Eb.
  intros.
  destruct b.
    reflexivity.

    assert (bin_to_nat b = 0).
      simpl in H0. destruct (bin_to_nat b). reflexivity. inversion H0.
    induction b.
      inversion H. inversion H3.

      assert (bin_to_nat b = 0). simpl in H1. destruct (bin_to_nat b). reflexivity. inversion H1.
      inversion H. apply IHb in H4. inversion H4. apply H1. apply H2. inversion H0.

    inversion H0.
  Qed.

Theorem id_bin_nat_bin : forall b : binary, regular_bin b -> nat_to_bin (bin_to_nat b) = b.
  intros b.
  intros H.
  induction b.
    reflexivity.

    simpl.
    inversion H.
    destruct b.
      inversion H1.

      pose H1. apply IHb in r. rewrite homo_double_z.
      assert (~(bin_to_nat (Zb b) = 0)). unfold not. intros. apply regular_z in H1. inversion H1. exact H2.
        case_eq
          (bin_to_nat (Zb b)). intros. unfold not in H2. apply H2 in H3. intuition.
          intros. rewrite <- H3. rewrite r. reflexivity.

      apply IHb in H1. rewrite homo_double_z. simpl. simpl in H1. rewrite H1. reflexivity.

    simpl.
    inversion H.
      reflexivity.
      destruct b.
        reflexivity.

        intros. rewrite homo_double_z.
        case_eq (bin_to_nat (Zb b)).
          intros. apply regular_z in H2. inversion H2. exact H1.
          intros. rewrite <- H2. apply IHb in H1. rewrite H1. reflexivity.

        apply IHb in H1. rewrite homo_double_z. simpl. simpl in H1. rewrite H1. reflexivity.
  Qed.