The Coq mailing list

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

Dear Coq users,

        I am stucked in the end of a proof because I need to 'evaluate' a
pattern matching. I looked for a solution on the web but I couldn't
find... The current proof step is:

  a : nat
  b : nat
  i : nat
  H : ith_remainder (pair a b) (i + 1) < ith_remainder (pair a b) i
  H0 : ith_remainder (pair a b) (S i) > 0
  l : 0 < b
  ============================
   (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)

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.

Cheers,

Flávio.