The Coq mailing list

[Jean-Francois Monin <jean-francois.monin AT imag.fr>]

Hello,

It is much simpler (and efficient) to define nat_to_bin as follows:

Fixpoint sbin b := 
  match b with
    | O' => ST O'
    | T b => ST b
    | ST b => T (sbin b)
  end.

Fixpoint nat_to_bin n := 
  match n with
   | O => O'
   | S n => sbin (nat_to_bin n)
  end.

(as you intend if I read correctly).

HOWEVER, your intended interpretation of bin is dangerous:
zero has many different representations (O', T O', etc.).

For instance you can prove  forall n, interp (nat_to_bin n) = n
with
Fixpoint interp b := 
  match b with
    | O' => O
    | T b => let n := interp b in n + n
    | ST b => let n := interp b in S (n + n)
  end.

But the converse does not hold because you would need O' = T O'.

The usual trick is to consider that bin represents only 
positive nats, that is to interpret O' as 1 instead of 0:

Fixpoint interp b := 
  match b with
    | O' => (S O)
    | T b => let n := interp b in n + n
    | ST b => let n := interp b in S (n + n)
  end.

Fixpoint sbin b := 
  match b with
    | O' => T O'
    | T b => ST b
    | ST b => T (sbin b)
  end.

Fixpoint Snat_to_bin n := 
  match n with
   | O => O'
   | S n => sbin (Snat_to_bin n)
  end.

(* nat_to_bin O is considered as irrelevant *)
Definition nat_to_bin n := Snat_to_bin (pred n).

Then you can check:

Theorem interp_nat_to_bin : forall n, interp (nat_to_bin (S n)) = S n.
Theorem nat_to_bin_interp : forall b, nat_to_bin (interp b) = b.

Hope this helps,
JFM

On Sat, Feb 07, 2015 at 06:33:25PM -0500, Holden Lee wrote:
>    I define "strong" recursion for natural numbers:
>    Definition strong_rec (P: nat -> Type) : 
>      (forall n: nat, 
>        (forall m: nat, (m<n) -> P m) -> P n) -> (forall m: nat, P m).
>    Now I try to define a function to convert from unary to binary: 
>    Definition nat_to_bin : (nat -> bin) :=
>    strong_rec (fun _ => bin) (fun n => (fun F => 
>      match n with 
>        | O => O'
>        | S n' => 
>          match (div2rem n) with
>            | (x, O) => T (F (fst (div2rem (S n'))) (div2smaller n'))
>            | (x, S y) => ST (F (fst (div2rem (S n'))) (div2smaller n'))
>          end
>      end)).
>    Basically I define nat_to_bin n in terms of nat_to_bin (n/2)
>    Here div2smaller n' is a proof that (S n')/2<S n' so that we can use
>    strong_rec.
>    Lemma div2smaller:
>      forall n, fst (div2rem (S n))<S n.
>    However this gives the error
>    Error:
>    In environment
>    n : nat
>    F : forall m : nat, m < n -> bin
>    n' : nat
>    x : nat
>    n0 : nat
>    The term "div2smaller n'" has type "fst (div2rem (S n')) < S n'"
>     while it is expected to have type "fst (div2rem (S n')) < n".
>    How can I tell Coq that n=S n'?
>    For reference here is the definition for bin:
>    Inductive bin : Type :=
>       | O' : bin
>       | T : bin -> bin (*twice*)
>       | ST: bin -> bin. (*one more than twice*)
>    Thanks,
>    Holden

-- 
Jean-Francois Monin