The Coq mailing list

[Randy Pollack <rpollack AT inf.ed.ac.uk>]

A few months ago there was discussion about this subject.

Consider the following:

  Inductive X : Set :=
    Xcon : nat -> X
  | Xlst : list X -> X.

  Fixpoint flatten (A:Set) (lss: list (list A)) {struct lss} : list A :=
    match lss with
      | nil => nil
      | ks::kss => ks ++ (flatten A kss)
    end.

  Fixpoint natsInX (x:X) {struct x} : list nat :=  (* accepted *)
    match x with
      | Xcon n => n::nil
      | Xlst xs => flatten nat (map natsInX xs)
    end.

  Fixpoint NatsInX (x:X) {struct x} : list nat :=  (* not accepted *)
    match x with
      | Xcon n => n::nil
      | Xlst xs => flat_map NatsInX xs
    end.

The Fixpoint definition natsInX is accepted, and seems to do the
expected computation.  But why should it be accepted when the
recursive call to natsInX is not applied to an argument?  

Of course, this definition is terminating, but only because map (from
the library) is defined a certain way.  (I suppose this has to do with
Thorsten's message on this topic about containers).  However, If I
make a correct local definition of map, this is not accepted where the
library version of map is accepted.  So is there something
extra-logical (perhaps ad-hoc) going on?

Conversely, the Fixpoint definition NatsInX is not accepted.
(flat_map from the library.)  Why should this be, given that natsInX
is accepted?

Perhaps even more fundamentally, how does Fixpoint work at all, since
Coq's automatically inferred recursion principle for X is too weak?

Best,
Randy