The Coq mailing list

[Hendrik Tews <tews AT os.inf.tu-dresden.de>]

Michiel Helvensteijn 
<mhelvens AT gmail.com>
 writes:

   Thanks! You do make the sumor idiom seem very attractive. :-)

Well, I should have added to my summary, that the sumor idiom may
become a nuisance in expressing properties. I did not elaborate
on that, because it is mostly obvious. With sumor, your function
does not easily compose any more and therefore many of your
theorems need a case distinction.


For instance, in http://askra.de/science/coalgebraic-cut I use a
partial nth function

   Fixpoint nth(l : list A)(n : nat)(inside : n < length l) : A

and the file lists.v contains many results about this nth. There
are only 5 generalize's (which I recently reduced to 2 using some
more clever lemma). With the sumor idiom, many of the theorems
would look much more ugly, because of the case distinction. With
sumor, properties such as

   forall(f : A -> B)(l : list A)(n : nat)(n_less : n < length (map f l)),
     nth (map f l) n n_less_map = f (nth l n (nth_map_tcc f l n n_less))

become quite complicated (here, nth_map_tcc constructs a prove
for "n < length l" from n_less). Using a case distinction in this
property might make it unsuitable for rewriting.

Bye,

Hendrik