1
$\begingroup$

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.
$\endgroup$
  • 2
    $\begingroup$ Related: stackoverflow.com/questions/32662889/… $\endgroup$ – gallais Aug 28 '17 at 15:37
  • $\begingroup$ What do T and M represent? What is the implementation of incr? These might help us give good answers. $\endgroup$ – cody Aug 28 '17 at 16:30
  • $\begingroup$ @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. $\endgroup$ – Morin Aug 28 '17 at 16:49
5
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Morin Aug 28 '17 at 16:22
  • 2
    $\begingroup$ @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. $\endgroup$ – Gilles Aug 28 '17 at 20:52
  • 2
    $\begingroup$ Machines are never wrogn. $\endgroup$ – Andrej Bauer Aug 29 '17 at 10:38

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.