The Coq mailing list

[Adam Chlipala <adamc AT hcoop.net>]

Adam Koprowski wrote:
>   Sure, you can do the same thing without Program, but it gets 
> slightly more complicated as you need to manually get the equality for 
> the pattern-matched variable:
>
> Section testing.
>
> Variable P : forall i, i < 10 -> nat -> nat.
>
> Definition check (i : nat) (H : i < 10) : nat.
> Proof.
>   refine (fix check (i : nat) (H : i < 10) {struct i} : nat :=
>     match i as j return i = j -> nat with
>     | 0 => fun _ => 0
>     | S n => fun ij => P n _ (check n _)
>     end refl); subst; auto with arith.
> Defined.
>
> End testing.

You can usually avoid introducing intermediate equality proofs by 
pushing arguments later in a function definition, like this:

Require Import Arith.

Section testing.
 Variable P : forall i, i < 10 -> nat -> nat.

 Definition check (i : nat) (H : i < 10) : nat.
 Proof.
   refine (fix check (i : nat) : i < 10 -> nat :=
     match i return i < 10 -> _ with
       | 0 => fun _ => 0
       | S n => fun _ => P n _ (check n _)
     end); auto with arith.
 Defined.
End testing.