(* natural numbers are defined with the following inductive:
Inductive nat :=
| O: nat
| S: nat -> nat.
These are unary numbers (base 1), so that most operations are exponentially slower than necessary
1. Define a datatype [bin] for binary natural numbers
2. Define a conversion function [bn: bin -> nat].
3. Define addition [bplus] and multiplication [bmult] on [bin]
4. Prove that [bn,bplus,bmult] is a morphism:
forall x y, bn (badd x y) = bn x + bn y
forall x y, bn (bmult x y) = bn x * bn y
5. Define a conversion function [nb: nat -> bin]
6. What can you prove between [bn] and [nb] ?
*)
Require Import ArithRing.
(* to use the tactic [ring], solving polynomial equations on [nat] *)
(* NB: answer file is only 126 lines long, including the above comments; do not make it over-complicated... *)