Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Defining binlen (log)

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Defining binlen (log)


Chronological Thread 
  • From: Jason Gross <jasongross9 AT gmail.com>
  • To: t x <txrev319 AT gmail.com>
  • Cc: coq-club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Defining binlen (log)
  • Date: Fri, 27 Sep 2013 19:10:29 +0200

Also, when doing well-founded recursion, you should make your proofs transparent (Defined, rather than Qed).  Because the fixpoint actually needs to be able to compute through the proofs.

-Jason

On Friday, September 27, 2013, Jason Gross wrote:
Try defining binary numbers, defining conversion functions back and forth between binary numbers and natural numbers, and then defining bin_len on binary numbers.

-Jason

On Friday, September 27, 2013, 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!



Archive powered by MHonArc 2.6.18.

Top of Page