gistfile1.coq

AddPath "/home/omer/sf/" as.
Require Export Basics.

Inductive bin : Set :=
| Zero : bin
| TwoZero : bin -> bin
| TwoZeroPOne : bin -> bin.

Fixpoint inc (b : bin) : bin :=
  match b with
  | Zero => TwoZeroPOne Zero
  | TwoZero b' => TwoZeroPOne b'
  | TwoZeroPOne b' => TwoZero (inc b')
  end.

Fixpoint bin_to_unary (b : bin) : nat :=
  match b with
  | Zero => O
  | TwoZero b' => 2 * bin_to_unary b'
  | TwoZeroPOne b' => 2 * bin_to_unary b' + 1
  end.

Require Import Arith.

Theorem bin_unary_commute : forall b : bin,
  bin_to_unary (inc b) = 1 + bin_to_unary b.
Proof.
  intros b. simpl. induction b as [|b'|b'].
  Case "b = Zero".
    reflexivity.
  Case "b = TwoZero b'".
    simpl. rewrite <- plus_n_O. rewrite <- plus_comm. reflexivity.
  Case "b = TwoZeroPOne b'".
    simpl. rewrite <- plus_n_O. rewrite <- plus_n_O.
    replace (bin_to_unary b' + bin_to_unary b' + 1) with (1 + bin_to_unary b' + bin_to_unary b'). simpl.
    rewrite -> IHb'. simpl.
    replace (bin_to_unary b' + S (bin_to_unary b')) with (S (bin_to_unary b' + bin_to_unary b')).
    reflexivity.

  SCase "first assertion".
    rewrite <- plus_n_Sm. reflexivity.

  SCase "second assertion".
    rewrite <- plus_assoc. rewrite <- plus_n_Sm. rewrite <- plus_n_O. simpl. reflexivity.
Qed.