Search code examples
coqlogical-foundations

Inductive types carrying proofs

There is this one exercise in "Software Foundations" that I've been trying to solve correctly for some time now but I've actually hit a wall in terms of trying to write down the function being asked for. Here is the relevant part of the exercise

Consider a different, more efficient representation of natural numbers using a binary rather than unary system. That is, instead of saying that each natural number is either zero or the successor of a natural number, we can say that each binary number is either

  • zero,
  • twice a binary number, or
  • one more than twice a binary number.

(a) First, write an inductive definition of the type bin corresponding to this description of binary numbers.

The naive definition doesn't quite work because you end up being able to construct terms that add 1 to a number that already had 1 added to it or multiplying zero with 2 for no good reason. In order to avoid those I figured I would encode some kind of state transition into the constructors to avoid those but this is kinda tricky so this was the best I could come up with

Inductive tag : Type := z | nz | m. (* zero | nonzero | multiply by 2 *)

Inductive bin_nat : tag -> Type :=
  (* zero *)
  | Zero : bin_nat z
  (* nonzero *)
  | One : bin_nat nz
  (* multiply by 2 -> nonzero *)
  | PlusOne : bin_nat m -> bin_nat nz
  (* nonzero | multiply by 2 -> multiply by 2 *)
  | Multiply : forall {t : tag}, (t = m \/ t = nz) -> bin_nat t -> bin_nat m.

With the above representation I avoid the issues of terms that don't make sense but now I have to carry around proofs whenever I multiply by 2. I actually have no idea how to use these things in recursive functions though.

I know how to construct the proofs and the terms and they look like this

(* nonzero *)
Definition binr (t : tag) := or_intror (t = m) (eq_refl nz).
(* multiply by 2 *)
Definition binl (t : tag) := or_introl (t = nz) (eq_refl tag m).
(* some terms *)
Check Zero.
Check One.
Check (Multiply (binr _) One).
Check (Multiply (binl _) (Multiply (binr _) One)).
Check PlusOne (Multiply (binl _) (Multiply (binr _) One)).

I can also write down a "proof" of the theorem that I want to correspond to a function but I don't know how to actually convert it to a function. Here's the proof for the conversion function

Definition binary_to_nat : forall t : tag, bin_nat t -> nat.
Proof.
intros.
einduction H as [ | | b | t proof b ].
  { exact 0. } (* Zero *)
  { exact 1. } (* One *)
  { exact (S (IHb b)). } (* PlusOne *)
  { (* Multiply *)
    edestruct t.
    cut False.
    intros F.
    case F.
    case proof.
    intros F.
    inversion F.
    intros F.
    inversion F.
    exact (2 * (IHb b)).
    exact (2 * (IHb b)).
  }
Defined.

I know this term is the function I want because I can verify that I get the right answers when I compute with it

Section Examples.

Example a : binary_to_nat z Zero = 0.
Proof.
lazy.
trivial.
Qed.

Example b : binary_to_nat nz One = 1.
Proof.
lazy.
trivial.
Qed.

Example c : binary_to_nat m ((Multiply (binl _) (Multiply (binr _) One))) = 4.
Proof.
lazy.
trivial.
Qed.

End Examples.

So finally the question, is there an easy way to convert the above proof term to an actual function in a simple way or do I have to try to reverse engineer the proof term?

Solution

  • I like your idea of representing a valid binary number using states and an indexed inductive type. However, as the question indicates, it's possible to get away with just three constructors on the inductive type: zero, multiply by 2, and multiply by 2 and add one. That means that the only transition we need to avoid is multiplying zero by 2.

    Inductive tag : Type := z | nz. (* zero | nonzero *)

Inductive bin_nat : tag -> Type :=
  (* zero *)
  | Zero : bin_nat z
  (* multiply by 2 *)
  | TimesTwo : bin_nat nz -> bin_nat nz
  (* multiply by 2 and add one *)
  | TimesTwoPlusOne : forall {t : tag}, bin_nat t -> bin_nat nz.

    Then, for example,

    Let One := TimesTwoPlusOne Zero. (* 1 *)
Let Two := TimesTwo One. (* 10 *)
Let Three := TimesTwoPlusOne One. (* 11 *)
Let Four := TimesTwo Two. (* 100 *)

    So TimesTwo adds a zero to the end of the binary representation and TimesTwoPlusOne adds a one.

    If you want to try this yourself, don't look any further.

    (I would have put this in spoiler tags, but apparently code blocks in spoiler tags are glitchy)

    Incrementing a binary number.

    Fixpoint bin_incr {t: tag} (n: bin_nat t): bin_nat nz :=
match n with
| Zero => One
| TimesTwo n' => TimesTwoPlusOne n'
| @TimesTwoPlusOne _ n' => TimesTwo (bin_incr n')
end.

    A helper definition for converting nat to binary.

    Definition nat_tag (n: nat): tag :=
match n with
| 0 => z
| S _ => nz
end.

    Converting nat to binary.

    Fixpoint nat_to_bin (n: nat): bin_nat (nat_tag n) :=
match n with
| 0 => Zero
| S n' => bin_incr (nat_to_bin n')
end.

    Converting binary to nat. Note that this uses the notations for multiplication and addition of natural numbers. If this doesn't work, you may not have the right scopes open.

    Fixpoint bin_to_nat {t: tag} (n: bin_nat t): nat :=
match n with
| Zero => 0
| TimesTwo n' => 2 * (bin_to_nat n')
| @TimesTwoPlusOne _ n' => 1 + 2 * (bin_to_nat n')
end.

    We get actual functions from these definitions (note that 20 is 10100 in binary).

    Compute nat_to_bin 20.
= TimesTwo
     (TimesTwo (TimesTwoPlusOne (TimesTwo (TimesTwoPlusOne Zero))))
 : bin_nat (nat_tag 20)

Compute bin_to_nat (nat_to_bin 20).
= 20
 : nat

    One further technical note. I used this code on two versions of Coq (8.6 and 8.9+alpha) and one version demanded that I put the tag in explicitly when matching on TimesTwoPlusOne, while the other allowed it to stay implicit. The above code should work in either case.