Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Problem with definition from CPDT

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Problem with definition from CPDT


chronological Thread 
  • From: Thomas Schilling <nominolo AT googlemail.com>
  • To: coq-club AT inria.fr
  • Subject: [Coq-Club] Problem with definition from CPDT
  • Date: Tue, 15 Feb 2011 12:07:10 +0000
  • Domainkey-signature: a=rsa-sha1; c=nofws; d=googlemail.com; s=gamma; h=from:content-type:content-transfer-encoding:subject:date:message-id :to:mime-version:x-mailer; b=wByhrh1hirq4KwWhTtp1VvKV0evHKStOXiM/ge4+fcKvyzylyKHc3MNAqvotOMYqRS tlze6UPDhxnxawqurpX/WlECk5SRbLAva/a4i5CBxYEuAskquU7OQuXJL1U27Mp2MfQl sxU0vml8vXRTUGcOtQ/qlSQ8v7YjU6kw9fTeA=

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



Archive powered by MhonArc 2.6.16.

Top of Page