coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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
- [Coq-Club] Problem with definition from CPDT, Thomas Schilling
- Re: [Coq-Club] Problem with definition from CPDT,
Adam Chlipala
- Re: [Coq-Club] Problem with definition from CPDT, Thomas Schilling
- Re: [Coq-Club] Problem with definition from CPDT,
Adam Chlipala
Archive powered by MhonArc 2.6.16.