The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

Adam Koprowski wrote:
>    Dear all,
>
>   I have problems with reducing a function defined by means of a 
> Program with a measure.
> [...]
> Program Fixpoint eval (T : Type) (x : X T) (n : nat)
>   { measure (build_ctx x n) (x_measure) } : Res T :=
>   match x return Res T with
>   | _ => @Fail T
>   end.
> Next Obligation.
> Proof with auto.
>   unfold MR. intro x.
>   apply acc_fun_image with (S := x_measure)
>     (f := fun (x : {T : Type & { _ : X T & nat}}) =>
>     let xx := projT2 x in build_ctx (projT1 xx) (projT2 xx))...
>   apply x_measure_wf.
> Defined.
>
> Eval lazy in eval Nil 0.
Hi,

You over-simplified the test case: reduction is blocked by acc_fun_image 
(argument r of fixpoint).
Eval lazy in eval Nil 0.
    = (fix Fix_F_sub (x : {T : Type &  {_ : X T &  nat}})
                     (r : ...) {struct r} :
         Res (let (a, _) := x in a) := Fail (let (a, _) := x in a))
        (existT ...)
        (acc_fun_image ...) ...

Double check that the lemmas used in the accessibility proof are saved 
using Defined, to allow reduction. It is also possible that you use an 
opaque lemma of the standard library. To check if a lemma is unfoldable, 
use Eval red in ...

Bruno Barras.