The Coq mailing list

[Fl�vio Leonardo Cavalcanti de Moura <flaviomoura AT unb.br>]

Em Ter, 2009-12-01 Ã s 17:24 +0100, Guillaume Melquiond escreveu:
> 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

Thank you Guillaume!