bin_numb.v

(**
 * 自然数の二進表現
 * 例: (10010) は O I O O I Z
 * 一つの数の表現が一意でないことに注意
 *)
Inductive bin_numb :=
  | I : bin_numb -> bin_numb
  | O : bin_numb -> bin_numb
  | Z : bin_numb.

(** bin_numb -> nat の変換 *)
Fixpoint f (b: bin_numb): nat :=
  match b with
  | I x => 2 * f x + 1
  | O x => 2 * f x
  | Z => 0
  end.

(** bin_numb上のインクリメント関数 *)
Fixpoint inc(b: bin_numb): bin_numb :=
  match b with
  | I x => O (inc x)
  | O x => I x
  | Z => I Z
  end.

(** nat -> bin_numb の変換 *)
Fixpoint g (n: nat): bin_numb :=
  match n with
  | 0 => Z
  | S x => inc (g x)
  end.

(**
 * 複数あるbin_numbの表現を一意に扱うための
 * bin_numbの正規系を導く関数
 * 具体的には上位にある連続したゼロを消す
 * 問題分にあるように、fやgに依存せずダイレクトリィに定義
 *)
Fixpoint norm(b: bin_numb) :=
  match b with
  | I x => I (norm x)
  | O x =>
    match norm x with
    | I y => O (I y)
    | Z => Z
    | O y => O (O y)
    end
  | Z => Z
  end.

Compute norm (O Z).
Compute norm (I (O Z)).
Compute norm (O (I (O Z))).
Compute norm (I (O (I (O Z)))).

(** 再帰関数の、関数呼び出しに関する帰納法をできるようにする。
 * パターンマッチが入れ子になったりしている複雑な再帰関数のときに便利
 *)
Functional Scheme norm_ind := Induction for norm Sort Prop.

(** norm の冪等性 *)
Theorem norm_idenpotence: forall x, norm (norm x) = norm x.
Proof.
 intros x. functional induction (norm x).
 - simpl. now rewrite IHb.
 - rewrite <-e0. simpl. now rewrite IHb, e0.
 - rewrite <-e0. simpl. now rewrite IHb, e0.
 - now auto.
 - now auto.
Qed.

(** incとnormは交換可能 *)
Theorem inc_norm: forall x, norm (inc x) = inc (norm x).
Proof.
 intro x. functional induction (norm x).
 - simpl. rewrite IHb. case_eq (inc (norm x)); [now auto|now auto|].
   now destruct (norm x).
 - simpl. now rewrite e0.
 - simpl. now rewrite e0.
 - simpl. now rewrite e0.
 - reflexivity.
Qed.

Theorem twice_comm: forall n, g (2 * n) = norm (O (g n)).
Proof.
 induction n; [now auto|].
 cutrewrite (2 * S n = S (S (2 * n))); [|simpl; now auto with arith].
 unfold g. fold g. rewrite IHn. now do 2 rewrite <-inc_norm.
Qed.

Theorem ex_c : forall x, g (f x) = norm x.
Proof.
 intros x. functional induction (norm x).
 - simpl.
   cutrewrite (f x + (f x + 0) + 1 = 1 + 2 * f x); [|now auto with arith].
   cutrewrite (g (1 + 2 * f x) = inc (g (2 * f x))); [|reflexivity].
   rewrite twice_comm. rewrite <- inc_norm. simpl.
   now rewrite IHb, norm_idenpotence.
 - simpl. cutrewrite (f x + (f x + 0) = 2 * f x); [|now auto with arith].
   rewrite twice_comm. rewrite IHb. simpl. rewrite norm_idenpotence.
   now rewrite e0.
 - simpl. cutrewrite (f x + (f x + 0) = 2 * f x); [|now auto with arith].
   rewrite twice_comm. rewrite IHb. simpl. rewrite norm_idenpotence.
   now rewrite e0.
 - simpl. cutrewrite (f x + (f x + 0) = 2 * f x); [|now auto with arith].
   rewrite twice_comm. now rewrite IHb, e0.
 - now reflexivity.
Qed.