The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

The exercise you describe in your mail is erroneous, because it is
true that the bijection between the two types Z_btree and Z_fbtree
cannot be proved unless you have added an axiom to the coq theory.  We 
had overlooked this aspect, when we first included the exercise in
book draft.

The future version of the book has a corrected version, but we do not
make it available on the internet until we have an agreement with the
publisher for the paper version.  At that time, we may even need to
remove access to that old version.

With respect to your analysis of the problem, it seems all correct:
extensionality is needed.  All experienced users that have stumbled on 
this problem have decided that you could not do it with an
extenionality axiom.  Still, we try in general to avoid this kind of
problem.

This example of functional binary trees is rather artificial and the
problem we have with the exercise happens rarely in real usage.  Even
the infinitely branching trees are seldom used, so that even
experienced users have little experience with this kind of
data-structure.  This examples are actually used as precursors to the
notion of accessibility that reappears only much later (in chapt. 13)
and where extensionality does not play a role either.

I hope this helps.

Yves

Yves.Bertot AT inria.fr
  Tel: (+33/0)4 92 38 77 39  Fax: (+33/0)4 92 38 50 60
INRIA Sophia-Antipolis 2004, route des lucioles, B.P. 93,
06902 Sophia Antipolis Cedex (France).
http://www.inria.fr/lemme/Yves.Bertot