The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

An alternate solution to your original question would be to write a fixpoint 
expression that expands to a generalization of your original match statement:

Fixpoint match_at_m (f:nat->nat) (g:nat) (m n:nat) : nat :=
match m with
| 0 => match n with
       | 0 => g
       | S n' => f (S n')
       end
| S m' => match n with
          | 0 => f 0
          | S n' => match_at_m (fun n => f (S n)) g m' n'
          end
end.

Compute (fun f g => match_at_m f g 5).

Or, if the result type is dependent on n:

Fixpoint dep_match_at_m {P:nat->Type} (f:forall n:nat, P n)
  (m:nat) (g:P m) (n:nat) : P n :=
match m as m' return (P m' -> P n) with
| 0 => fun g => match n as n' return P n' with
                | 0 => g
                | S n' => f (S n')
                end
| S m' => fun g => match n as n' return P n' with
          | 0 => f 0
          | S n' => dep_match_at_m (fun n => f (S n)) m' g n'
          end
end g.

Compute (fun P (f:forall n:nat, P n) => dep_match_at_m f 5).
-- 
Daniel Schepler