The Coq mailing list

[Bernard Hurley <bernard AT marcade.biz>]

Thanks, I was attempting to do something like this but couldn't get it right!
I can see where I went wrong now!

Bernard

On Mon, Apr 30, 2012 at 08:57:50AM -0700, Daniel Schepler wrote:
> 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