The Coq mailing list

[Jean-Francois Monin <jeanfrancois.monin AT rd.francetelecom.com>]

My motivation was to use "general recursive functions" for
reflexion. Suppose that you need the log function, informally defined as:
  log 0 = 0
  log 1 = 0
  log n+2 = S (log n/2)

A reasonable option is to use well-founded recursion and to rely
on the theorems about le, lt, etc.
However, after Randy's message, I decided to quickly redevelop
an ad-hoc theory based on an ad-hoc accessibility predicate called
acc_div2, and proved/defined: 

Definition all_acc_div2: (n:nat) (acc_div2 n).

Fixpoint flog [n:nat; a:(acc_div2 n)] :  nat :=
  Cases (test_O_1_else n) of
  | (C0 _) => O
  | (C1 _) => O
  | (C2 p) => (S (flog (div2 n) (inv_acc_div2 n a p)))
  end.

Definition log [n:nat] := (flog n (all_acc_div2 n)).

Then it is easy to see that, when computing (log (1000)),
almost all computation time is spent in computing the
termination certificate (all_acc_div2 (1000)).

Note that, in this case, the termination certificate is very
short. My first idea was then that the latter could be safely
computed by an external program -- using a kind of extraction 
for example. 

But after all, I don't see why the termination certificate should
be normalized at all: its (constructive) existence should be enough.
I may miss something important, but please tell me what.
If this is true, then, returning to the point of Randy,
we don't need to make all theorems transparent. As far as
efficiency is concerned, this is probably a not-so-good idea:
Prop can be interpreted as the location where computations
are not performed; it is an interesting feature if this behavior is 
captured by the type system.

For example, in the log function, only one theorem is used for 
inverting the accessibility predicate. Everything else could
have been developed using standard lemmas on lt.

Interested readers can play with the attached short script 
(all definitions are from scratch, lt is of course carefully avoided).

  Jean-Francois

Attachment: log2.v
Description: log2.v