The Coq mailing list

[Thomas Schilling <nominolo AT googlemail.com>]

I'm working through Adam's Certified Programming with Dependent Types and Coq 
fails to accept the following definition from the book:


Require Import List.

Set Implicit Arguments.

Inductive nat_tree : Set :=
  | NLeaf : nat_tree
  | NNode : nat -> list nat_tree -> nat_tree.

Section All.
  Variable T : Set.
  Variable P : T -> Prop.

  Fixpoint All (ls : list T) : Prop :=
    match ls with
      | nil => True
      | cons h t => P h /\ All t
    end.
End All.

Section nat_tree_ind.
  Variable P : nat_tree -> Prop.
  Hypothesis NLeaf_case : P NLeaf.
  Hypothesis NNode_case :
    forall (n : nat) (ls : list nat_tree),
      All P ls -> P (NNode n ls).
  
  Fixpoint nat_tree_ind' (tr : nat_tree) : P tr :=
    match tr with
      | NLeaf => NLeaf_case   (* ***** fails here ***** *)
      | NNode n ls => NNode_case n ls
          ((fix list_nat_tree_ind (ls : list nat_tree) : All P ls :=
            match ls with
              | nil => I
              | cons tr rest =>
                  conj (nat_tree_ind tr) (list_nat_tree_ind rest)
            end) ls)
    end.


It claims that NLeaf_case has type 'P NLeaf' instead of 'P ?42'.  I would 
have thought, that Coq would figure out that 'tr' has shape 'NLeaf' in the 
given case.  If I replace 'NLeaf_case' with '_' it complains about the use of 
'I', again because it can't figure out that if 'ls' is 'nil' the 'All P ls' 
is 'True'.

Is this a limitation of my version of Coq?  I'm using Coq 8.2pl1 (latest on 
MacPorts).  Or am I missing something obvious?

/ Thomas