Binary system in Coq taken from More Exercises section of https://www.seas.upenn.edu/~cis500/current/sf/Basics.html

binarySystem.v

(* taken from More Exercies - exercie 3 of https://www.seas.upenn.edu/~cis500/current/sf/Basics.html *)

Inductive bin : Type :=
| Zero : bin
| Twice : bin -> bin
| More : bin -> bin.

Function bin_incr (n : bin) : bin :=
  match n with
  | Zero => More Zero
  | Twice n' => More n'
  | More n' => Twice (bin_incr n')
  end.

Example test_bin_incr_Zero : bin_incr Zero = More Zero.
Proof. simpl. reflexivity. Qed.

Example test_bin_incr_Twice : bin_incr (Twice Zero) = More Zero.
Proof. simpl. reflexivity. Qed.

Example test_bin_incr_More : bin_incr (More Zero) = Twice (More Zero).
Proof. simpl. reflexivity. Qed.

Function bin_to_nat (b : bin) : nat :=
 match b with
 | Zero => O
 | Twice b' => 2 * (bin_to_nat b')
 | More b' => 2 * (bin_to_nat b') + 1
 end.

Example test_bin_incr_1 : bin_to_nat (bin_incr Zero) = 1.
Proof. simpl. reflexivity. Qed.

Example test_bin_incr_2 : bin_to_nat (Twice (bin_incr Zero)) = 2.
Proof. simpl. reflexivity. Qed.

Example test_bin_incr_3 : bin_to_nat (More (bin_incr Zero)) = 3.
Proof. simpl. reflexivity. Qed.

Example test_bin_incr_4 : bin_to_nat (bin_incr (More (More (Zero)))) = 4.
Proof. simpl. reflexivity. Qed.

Example test_bin_incr_5 : bin_to_nat (bin_incr (bin_incr (More (More (Zero))))) = 5.
Proof. simpl. reflexivity. Qed.

bin_incr and bin_to_nat were checked against http://staff.ustc.edu.cn/~bjhua/courses/theory/2014/slides/lec1notes.html in addition to the examples.