# How to prove T Z = Z for binary representation of natural numbers in Coq

I have defined an Inductive in Coq for binary representation of natural numbers as follows:

Inductive bin : Type :=
| Z : bin
| T : bin -> bin
| M : bin -> bin.


and two recursive functions to convert between nat and bin types as:

Fixpoint nat_to_bin (n : nat) : bin :=
match n with
| O => Z
| S n' => incr (nat_to_bin n')
end.


and

Fixpoint bin_to_nat (b : bin) : nat :=
match b with
| Z => O
| M b' => S (mult 2 (bin_to_nat b'))
| T b' => mult 2 (bin_to_nat b')
end.


to show that bin_to_nat is the inverse of nat_to_bin I need to prove that T Z = Z by using these tactics that I know: simpl reflexivity destruct rewrite replace induction please recommend some clues showing how to do this. Thank you!

Edit

The incr implementation is

Fixpoint incr (b : bin) : bin :=
match b with
| Z => M Z
| T b' => M b'
| M b' => T (incr b')
end.

• – gallais Aug 28 '17 at 15:37
• What do T and M represent? What is the implementation of incr? These might help us give good answers. – cody Aug 28 '17 at 16:30
• @cody T doubles its argument and returns the result, M doubles its argument, adds one to it and returns the result, incr just adds one to a binary number we have given to it. – Morin Aug 28 '17 at 16:49

to show that bin_to_nat is the inverse of nat_to_bin I need to prove that T Z = Z

No, you can't prove that T Z = Z because it is false:

Lemma TZ_neq_Z : T Z <> Z.
Proof.
discriminate.
Qed.


Indeed, distinct constructors of an inductive type always lead to distinct terms.

That doesn't mean you can't prove that bin_to_nat is the inverse of nat_to_bin though.

• Thank you! I just forgot that Coq is a mechanical proof assistant and while it is obvious for us as human beings that T Z = Z but Coq sees it as a sequence of symbols. – Morin Aug 28 '17 at 16:22
• @Morin T Z = Z is false, even for a human. $2 * 0 = 0$ is true, but that's not what T Z = Z means. Z and T Z are not integers, they are representations of integers. Interpreting T as doubling and Z as zero is an interpretation. Using this interpretation, $2 * 0 = 0$ can be expressed in Coq as bin_to_nat (T Z) = bin_to_nat Z. – Gilles Aug 28 '17 at 20:52
• Machines are never wrogn. – Andrej Bauer Aug 29 '17 at 10:38