The Coq mailing list

[Thomas Schilling <nominolo AT googlemail.com>]

On 15 Feb 2011, at 13:26, Adam Chlipala wrote:

> Thomas Schilling wrote:
>> I'm working through Adam's Certified Programming with Dependent Types and 
>> Coq fails to accept the following definition from the book:
>> [...]
>> 
>> Is this a limitation of my version of Coq?  I'm using Coq 8.2pl1 (latest 
>> on MacPorts).  Or am I missing something obvious?
>>   
> 
> The book is only tested with Coq 8.2pl2 and 8.3pl1.  There were definitely 
> some bugs in 8.2pl1 that prevented some of the code from type-checking, 
> though I don't remember seeing your particular example mentioned before.

Ok, I managed to fix it.  I used "Print nat_rect" to figure out the 
definition of the auto-generated induction principles and then via trial and 
error I got it to accept the following.  (The changes are the "as .. return 
.." annotations.)


  Fixpoint nat_tree_ind' (tr : nat_tree) : P tr :=
    match tr as tr0 return (P tr0) with
      | NLeaf => NLeaf_case
      | NNode n ls => NNode_case n ls
          ((fix list_nat_tree_ind (ls : list nat_tree) : All P ls :=
            match ls as ls0 return All P ls0 with
              | nil => I
              | cons tr rest =>
                  conj (nat_tree_ind' tr) (list_nat_tree_ind rest)
            end) ls)
    end.

It indeed appears to be a limitation of my version of Coq.

BTW, thank you for making the sources for your book available.  It allowed me 
to create a special version for easier reading on my Kindle.

 / Thomas