The Coq mailing list

[Adam Koprowski <koper AT astercity.net>]

  Hello. My journey with Coq has started recently. I'm working on termination 
of higher-order recursive path ordering and for that I need formalization of 
multiset order on which I'm working now.
  I wanted to conform to the library and thus first decided to use its 
definition of multisets (over A), that is:

* Inductive multiset : Set :=
*     Bag : (A -> nat) -> multiset.

  There is a nice proof of well-foundedness of multiset order due to Wilfried 
Buchholz presented by Tobias Nipkow 
(http://www4.informatik.tu-muenchen.de/~nipkow/misc/multiset.ps). However it 
uses induction on the size of multiset which is impossible to perform with this 
definition (the problem is somehow more serious because this definition allows 
infinite multisets in general which is undesirable in this case of course).
  Does anybody have an idea what can I do? Is there any chance to stick to 
library definition of multisets, like, let's say, by refining it somehow (how?) 
to finite multisets in a way that allows induction on their size? Or should I 
just forget about library and use other representation of multisets (like lists?).
  Thank you in advance for any comments/suggestions.
   Adam Koprowski

--
----------------------------------------------------
-         
akoprow AT cs.vu.nl,
 ICQ: 3204612           -
-  The difference between impossible and possible  -
-      lies in determination (Tommy Lasorda)       -
----------------------------------------------------