The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

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.