The Coq mailing list

[Eugene Kirpichov <ekirpichov AT gmail.com>]

Hello, coq-club!

I'm walking through Adam Chipala's terrific CPDT book
(http://adam.chlipala.net/cpdt/) and while solving exercise 5 on page
61 I ran into something that looks to me strange, if not buggy.

Inductive btree (t:Set) :=
 | BLeaf : t -> btree t
 | BNode : btree t -> btree t -> btree t.

Inductive trexp : Set :=
 | TLeaf : nat -> trexp
 | TNode : btree trexp -> trexp.

Fixpoint total (t:trexp) :=
 match t with
 | TLeaf n => n
 | TNode b => btotal b
 end
with btotal (b:btree trexp) :=
 match b with
 | BLeaf t => total t (* An error here? *)
 | BNode b1 b2 => btotal b1 + btotal b2
 end.

I get the following error for 'total':

Error:
Recursive definition of btotal is ill-formed.
In environment
total : trexp -> nat
btotal : btree trexp -> nat
b : btree trexp
t : trexp
Recursive call to total has principal argument equal to
"t"
instead of a subterm of b.

But "t" *is* a subterm of b, because b has form BLeaf t!
Am I misunderstanding something?

Even more strangely, the following seemingly equivalent definition is 
accepted:

Definition total := fix total t :=
 match t with
 | TLeaf n => n
 | TNode b => (fix btotal b :=
   match b with
   | BLeaf t => total t
   | BNode b1 b2 => btotal b1 + btotal b2
   end) b
 end.

(I'm using Coqide 8.2pl1, compiled from source)

--
Eugene Kirpichov
Web IR developer, market.yandex.ru