The Coq mailing list

["N. Raghavendra" <raghu AT hri.res.in>]

At 2013-09-27T16:16:42Z, t x wrote:

> Hi,
>
>   I have a definition of binlen (basically log) at https://
> gist.github.com/anonymous/6731044
>
>   Unfortunately, I find it very very hard to reason with (in
> particular,
>
>   "binlen 0 <= binlen 1"
>
>   expands to the nastiness shown in the url).
>
>   Thus, my question -- is there a way where I can spend a bit more
> work in my definition of bin_len so that when I need to prove things
> about it, it's nicer?
>
>   Ideally, I want
>
>   unfold bin_len in "bin_len x" ==>
>
>   match x with
>   | 0 => 1
>   | 1 => 1
>   | n => 1 + bin_len (div2 x)
>   end.
>
> Thanks!
>
>

This may be off the mark, but here is some stuff from exercises in
Pierce's book:

----------------------------------------------------------------------
(* Notation : A binary number is a finite sequence of the symbols a and
   b, e.g., a, b, bb, aab, abaab.  Thus, every binary number is either
   the empty sequence E, or a binary number obtained by suffixing a or b
   to another binary number. *)

Inductive bin : Type :=
| E : bin
| A : bin -> bin          (* E => a, a => aa, b => ba, ..., s => sa *)
| B : bin -> bin.         (* E => b, a => ab, b => bb, ..., s => sb *)

Fixpoint succ_bin (s : bin) : bin :=
  match s with
    | E => B E
    | A t => B t
    | B t => A (succ_bin t)
  end.

Fixpoint nat_to_bin (n : nat) : bin :=
  match n with
    | O => E
    | S p => succ_bin (nat_to_bin p)
  end.

Fixpoint bin_length (s : bin) : nat :=
  match s with
    | E => O
    | A t => S (bin_length t)
    | B t => S (bin_length t)
  end.

Definition binlen (n : nat) : nat :=
  bin_length (nat_to_bin n).

----------------------------------------------------------------------

It's obviously an overkill to compute the binary representation of a nat
to get its bit-length.  An alternative is to define a function

binlen_aux (n p e : nat) : nat

such that

binlen_aux n p e = p if n < e

and 

binlen_aux n p e = binlen_aux n (p+1) (2*e) if n >= e.

This definition has to be rephrased to satisfy Coq's requirements on
decreasing arguments for fixpoints.  Then, one can define

binlen n = binlen_aux n 0 1.

Best regards,
Raghu.

-- 
N. Raghavendra 
<raghu AT hri.res.in>,
 http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/