bin2.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) *)

(* (a) *)
Inductive bin : Type :=
  | Z : bin
  | B0 : bin -> bin
  | B1 : bin -> bin
.

(* (b) *)
Fixpoint incr (b : bin) : bin :=
  match b with
    | Z => B1 Z
    | B0 b' => B1 b'
    | B1 b' => B0 (incr b')
  end.


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


(* (c) *)
Theorem bin2nat_inc_bin_comm :
  forall b : bin, bin2nat (incr 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) *)

(* (a) *)
Fixpoint nat2bin (n:nat) : bin :=
  match n with
    | O => Z
    | S n' => incr (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) *)


Fixpoint zerop (b:bin) : bool :=
  match b with
  | Z => true
  | B0 x => zerop x
  | B1 _ => false
  end
.

Lemma not_zerop_incr : forall b:bin, zerop (incr b) = false.
Proof.
  intros b.
  induction b.
  + reflexivity.
  + reflexivity.
  + simpl. assumption.
Qed.

Eval compute in (zerop (B0 (B0 (B0 (B0 Z))))).
Eval compute in (zerop (B1 (B0 (B0 (B0 Z))))).

Fixpoint normalize2 (b:bin) : bin :=
  match zerop b with
  | true  => Z
  | false => match b with
             | Z => Z
             | B0 x => B0 (normalize2 x)
             | B1 x => B1 (normalize2 x)
             end
  end.

Eval compute in (normalize2 (B0 (B0 (B0 (B0 Z))))).
Eval compute in (normalize2 (B1 (B0 (B0 (B0 Z))))).

Lemma normalize_inc : forall b:bin, normalize2 (incr b) = incr (normalize2 b).
Proof.
  intros b.
  induction b.
  + reflexivity.
  + destruct b.
    - reflexivity.
    - simpl. destruct (zerop b).
      * reflexivity.
      * reflexivity.
    - reflexivity.
  + simpl.
    rewrite not_zerop_incr.
    rewrite IHb.
    reflexivity.
Qed.