The Coq mailing list

[Adam Megacz <megacz AT cs.berkeley.edu>]

Section 14.3.3 [*] of Coq'Art explains the "nested fix" trick for
recursing over mutually inductive types that haven't been defined
mutually via the "with" keyword.  This has been a real life-saver.

This trick essential for inductive types which have a constructor which
takes a polymorphic container (tree, list, etc) instantiated at the type
being defined.  In practice programs using these types can be rewritten
in other ways (for example with a separate monomorphic tree type for
each instantiation), but in large-scale developments this can result in
an unmanageable level level of of repetition repetition.

My question is this: is there a simple way to generate XXX_rect induction
principles for these mutually-recursive-but-not-declared-mutual types?

I find myself needing to repeatedly prove facts about these sorts of
types, and while I can manage to write terms explicitly with the Coq'Art
trick without much trouble, it doesn't work very well with the tactical
approach.  In particular it's very hard to use "refine" on these
nested-fix terms and still pass the final structurally-decreasing check
-- I'm even starting to suspect the check is slightly stricter when
using tacticals, or that there's a special exception for nested fix that
isn't being allowed when building a term using tactics.  Or maybe I just
missed something.

Many thanks,

  - a


[*] here is a link on google books:

    
http://books.google.com/books?id=m5w5PRj5Nj4C&lpg=PA400&ots=VGsA_PW_0e&dq=coq%20%22list%20of%20trees%22&pg=PA404#v=onepage&q=coq%20%22list%20of%20trees%22&f=false