coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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:
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:
Thanks!end.| n => 1 + bin_len (div2 x)match x withIdeally, I wantThus, 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?expands to the nastiness shown in the url).Unfortunately, I find it very very hard to reason with (in particular,"binlen 0 <= binlen 1"
unfold bin_len in "bin_len x" ==>
| 0 => 1
| 1 => 1
- [Coq-Club] Defining binlen (log), t x, 09/27/2013
- Re: [Coq-Club] Defining binlen (log), Jason Gross, 09/27/2013
- Re: [Coq-Club] Defining binlen (log), Jason Gross, 09/27/2013
- Re: [Coq-Club] Defining binlen (log), N. Raghavendra, 09/27/2013
- Re: [Coq-Club] Defining binlen (log), Jason Gross, 09/27/2013
Archive powered by MHonArc 2.6.18.