The Coq mailing list

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

Em Ter, 2009-12-01 Ã s 11:21 -0500, Adam Chlipala escreveu:
> Flávio Leonardo Cavalcanti de Moura wrote:
> > I am stucked in the end of a proof because I need to 'evaluate' a
> > pattern matching.
> >
> > [snip]
> >
> >    ============================
> >     (fix ith_remainder (d : pair_t) (i0 : nat) {struct i0} : nat :=
> >        match d with
> >        | pair a0 b0 =>
> >            if zerop b0
> >            then 0
> >            else
> >             match i0 with
> >             | 0 =>  mod a0 b0
> >             | S n =>  mod b0 (ith_remainder (pair a0 b0) n)
> >             end
> >        end) (pair a b) (S i + 1)<  ith_remainder (pair a b) (S i)
> >    
> 
> The key is in the [{struct i0}] annotation.  This says that your 
> function [ith_remainder] is defined as structurally recursive on the 
> [i0] argument.  Thus, a call to [ith_remainder] will only simplify when 
> the top-level structure of the [i0] argument is known.  In your example 
> code, it is clear that this argument is greater than 0, but deducing 
> this takes a little more smarts than Coq's computation rules will 
> apply.  If you manage to rewrite [S i + 1] into [S (S i)] (or any other 
> term built directly from [S]), then you will see the reduction you are 
> looking for.
> 
> Feel free to write again if it you need any help on how to perform this 
> rewrite.

Dear Adam, 

        Thank you for the tip. I managed to complete the proof!

Cheers,

Flávio.