The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

Le 11/08/2020 à 16:13, Agnishom Chattopadhyay a écrit :
> As an example, consider lists. The default way to induct/recurse on
> lists is to pattern match on the list as either [] or (cons x xs).
> 
> One can use a different induction principle on lists by defining an
> appropriate lemma. (See this <https://stackoverflow.com/a/33072357/1955231>)
> 
> Is there something similar I can do for the purpose of defining
> functions on lists?

Certainly. There are two things to keep in mind.

First, the StackOverflow answer uses a predicate P: list X -> Prop, but
you can just as well prove a statement that uses a function P: list X ->
Set (or Type) with the exact same proof. This gives you a recurrence
principle instead of an induction principle, which you can use to define
functions.

Second, the recurrence principle should end with Defined rather than
Qed. Otherwise, computations will get stuck. Also, you might want to
define lemmas (ending with Qed) or use the "abstract" tactic so as to
make opaque as many computationally irrelevant parts of the induction
principle as possible. Conversely, avoid using Qed-ended lemmas in the
computationally relevant parts, e.g., rev_involutive (see below).

Here is the example of an inefficient function to compute the length of
a list:

Theorem list_rec_rcons:
  forall {X:Type} (P:list X -> Set),
  P nil ->
  (forall x l, P l -> P (rcons l x)) ->
  forall l, P l.
Proof. ... Defined.

Definition rlength {X} :=
  @list_rec_rcons X (fun _ => nat) 0 (fun _ _ v => S v).

Note that, if your proof of list_rec_rcons starts by applying
rev_involutive (or rather a Defined variant of it) before performing a
trivial structural induction on the reversed list, then the recurrence
principle you will obtain in the end is quite similar to your current
way of defining a function.

This should not come as a surprise. Indeed, there is not that many ways
to define an efficient recursive function that starts scanning a list
from its end. Reversing the list once and for all is one of them.

So, to summarize, your current way of defining a function is presumably
the best way. While theoretically possible, there is usually no
practical benefit to defining a custom recurrence principle.

Best regards,

Guillaume