The Coq mailing list

[Rui Baptista <rpgcbaptista AT gmail.com>]

The Function command automatically proves a theorem about the equation of the function. Check out bin_len_equation.

Require Import Recdef.

Function bin_len (n: nat) {measure id n} :=

  match n with

  | 0 => 1

  | 1 => 1

  | n => 1 + bin_len (div2 n)

  end.

Proof. unfold id. intros. subst. apply lem__div2_decr. omega. Qed.

Check bin_len_equation.

On Fri, Sep 27, 2013 at 5:16 PM, t x <txrev319 AT gmail.com> 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!