The Coq mailing list

[t x <txrev319 AT gmail.com>]

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!