bin.v

Theorem plus_0_r : forall n:nat, n + 0 = n.
Proof.
  intros n. induction n as [| n'].
  (* Case "n = 0". *)    +  reflexivity.
  (* Case "n = S n'". *) +  simpl. rewrite -> IHn'. reflexivity.  Qed.

(** **** 練習問題: ★★★★, recommended (binary) *)
(** これまでとは異なる、通常表記の自然数ではなく2進のシステムで、自然数のより効率的な表現を考えなさい。それは自然数をゼロとゼロに1を加える加算器からなるものを定義する代わりに、以下のような2進の形で表すものです。2進数とは、
      - ゼロであるか,
      - 2進数を2倍したものか,
      - 2進数を2倍したものに1を加えたもの.

    (a) まず、以下のnatの定義に対応するような2進型[bin]の帰納的な定義を完成させなさい。
    (ヒント: [nat]型の定義を思い出してください。
[[
    Inductive nat : Type :=
      | O : nat
      | S : nat -> nat.
]]
    nat型の定義[O]や[S]の意味が何かを語るものではなく、（[O]が実際に何であろうが）[O]がnatであって、[n]がnatなら[S]が何であろうと[S n]はnatである、ということを示しているだけです。「[O]がゼロで、[S]は1を加える」という実装がそれを自然数としてみて実際に関数を書き、実行したり証明したりしてみてはじめて実際に意識されます。ここで定義するbinも同様で、次に書く関数が書かれてはじめて型binに実際の数学的な意味が与えられます。)

    (b) 先に定義したbin型の値をインクリメントする関数を作成しなさい。また、bin型をnat型に変換する関数も作成しなさい。

    (c) 最後にbで作成したインクリメント関数と、2進→自然数関数が可換であることを証明しなさい。これを証明するには、bin値をまずインクリメントしたものを自然数に変換したものが、先に自然数変換した後にインクリメントした元の値と等しいことを証明すればよい。
*)

(* (a) *)
Inductive bin : Type :=
  | B0 : bin
  | Be : bin -> bin
  | Bo : bin -> bin
.

(* (b) *)
Fixpoint inc_bin (b : bin) : bin :=
  match b with
    | B0 => Bo B0
    | Be b' => Bo b'
    | Bo b' => Be (inc_bin b')
  end.

Fixpoint bin2nat (b : bin) : nat :=
  match b with
    | B0 => O
    | Be b' => 2 * bin2nat b'
    | Bo b' => 1 + 2 * bin2nat b'
  end.

Example bin2nat_sixteen : bin2nat (Be (Be (Be (Be (Bo B0))))) = 16.
Proof. reflexivity. Qed.

Example bin2nat_twenty_one : bin2nat (Bo (Be (Bo (Be (Bo B0))))) = 21.
Proof. reflexivity. Qed.

(* (c) *)
Theorem bin2nat_inc_bin_comm :
  forall b : bin, bin2nat (inc_bin b) = S (bin2nat b).
Proof.
  intros b.
  induction b as [| be | bo].
    (* Case "b = B0".  *)
    + reflexivity.
    (* Case "b = Be be". *)
    + simpl. reflexivity.
    (* Case "b = Bo bo". *)
    + simpl.
      rewrite -> plus_0_r.
      rewrite -> plus_0_r.
      rewrite -> IHbo.
      rewrite <- plus_n_Sm.
      simpl.
      reflexivity.
Qed.
(** [] *)

(** **** 練習問題: ★★★★★ (binary_inverse) *)
(** この練習問題は前の問題の続きで、2進数に関するものである。前の問題で作成された定義や定理をここで用いてもよい。


    (a) まず自然数を2進数に変換する関数を書きなさい。そして「任意の自然数からスタートし、それを2進数にコンバートし、それをさらに自然数にコンバートすると、スタート時の自然数に戻ることを証明しなさい。


    (b) あなたはきっと、逆方向についての証明をしたほうがいいのでは、と考えているでしょう。それは、任意の2進数から始まり、それを自然数にコンバートしてから、また2進数にコンバートし直したものが、元の自然数と一致する、という証明です。しかしながら、この結果はtrueにはなりません。！！その原因を説明しなさい。


    (c) 2進数を引数として取り、それを一度自然数に変換した後、また2進数に変換したものを返すnormalize関数を作成し、証明しなさい。
*)

(* (a) *)
Fixpoint nat2bin (n:nat) : bin :=
  match n with
    | O => B0
    | S n' => inc_bin (nat2bin n')
  end.

Theorem nat_bin_nat : forall n:nat, bin2nat (nat2bin n) = n.
Proof.
  intros n. induction n as [| n'].
  (* Case "n = 0". *)
  + reflexivity.
  (* Case "n = S n'". *)
  + simpl. rewrite -> bin2nat_inc_bin_comm. rewrite -> IHn'.
    reflexivity. Qed.

(* (b) *)

(* 自然数に対して nat は一通りに表現が決定されるが、bin は複数の表現がありうるため。 *)

(* (c) *)

Definition normalize (b:bin) : bin := nat2bin (bin2nat b).

Theorem normalize_refl : forall b:bin, normalize b = nat2bin (bin2nat b).
Proof. reflexivity. Qed.

Theorem normalized_idempotent : forall b:bin, normalize (normalize b) = normalize b.
Proof.
  intros b.
  rewrite -> normalize_refl.
  rewrite -> normalize_refl.
  rewrite -> nat_bin_nat.
  reflexivity. Qed.