The Coq mailing list

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

Hello,

Consider the following context:

A, B : Set.
Inductive accessible : A -> Prop := ...
Fixpoint f [x:A; a:(accessible x)] : B := ...

Now, given a closed value x:A and a non canonical proof a:(accessible x),
I would expect that a lazy evaluation of (f x a) reduces to its normal
form without evaluating a.
But it does not seem to be the case. For example, if the following
is an opaque theorem:
   Theorem all_acc : (x:A)(accessible x),
you can observe that (f x (all_acc x)) is not computed in Coq V3.1,
though the value of the second argument is not used the result
(only its existence is important).

On the other hand, it works if a is not the decreasing argument
of the fixpoint f. 

What is happening ?

  Jean-Francois