The Coq mailing list

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

Flávio Leonardo Cavalcanti de Moura a écrit :
>   l : 0 < b
>   ============================
>    (fix ith_remainder (d : pair_t) (i0 : nat) {struct i0} : nat :=
>       match d with
>       end) (pair a b) (S i + 1) < ith_remainder (pair a b) (S i)
>
> I need to evaluate the function ith_remainder with the arguments (pair a
> b) and (S i + 1). If I manage to do so, I will get
>
> mod b (ith_remainder (pair a b) (S i)) < ith_remainder (pair a b) (S i)
>
> and I can close the proof with mod_lt. Any help is very much welcome.

Note that the evaluation can only happen if i0 starts with a 
constructor. You may try "replace (S i + 1) with (S (S i))" and see if 
it helps. You haven't provided the script so I can only guess, but I 
suppose you also have an "unfold ith_remainder" somewhere before; you 
may have to remove it.

Best regards,

Guillaume