Using contextual information in Coq pattern matching

2
votes

I want to define a function app_1 which converts an n-ary function f : X ^^ n --> Y into a new function f' : (Z -> X) ^^ n --> Y, provided that there is a z : Z to apply once to all of its arguments. For instance, 

Example ex1 : app_1 plus 2 S pred = 4.
trivial. Qed.

app_1 plus 2 is able to take the unary functions S and pred as arguments because it applies both of them to 2 first, and then apply the results to plus.

Here's my attempted definition of app_1:

Fixpoint app_1 {X Y Z : Type} {n : nat} 
(f : X ^^ n --> Y) (z : Z) :
(Z -> X) ^^ n --> Y :=
match n return ((Z -> X) ^^ n --> Y) with
| O    => f
| S n' => fun g => app_1 (f (g z)) z
end.

Which doesn't work, because Coq doesn't like the clause | O => f, and says:

The term "f" has type "X ^^ n --> Y" while it is expected to have type "(Z -> X) ^^ 0 --> Y".

But if n = O, X ^^ n --> Y = X ^^ 0 --> Y = Y = (Z -> X) ^^ 0 --> Y, so it's not a type mismatch. The problem is that Coq can't use the contextual information n = O to figure out the equivalence.

Some preliminary searches show that this is a well-known problem, but it's a little confusing how to apply those discussions to this case. For instance, an almost identical question on SO is solved using return, which is what I (sort of) tried above as well, to no avail.

Is there a way to make this pattern match work?

2
pattern-matchingcoq

2 Answers

3
votes

As usual, you must apply the convoy pattern (cf. Adam Chlipala's CPDT book) and make the pattern-matching return a function:

Require Import Coq.Numbers.NaryFunctions.

Fixpoint app_1 {X Y Z : Type} {n : nat}
(f : X ^^ n --> Y) (z : Z) :
(Z -> X) ^^ n --> Y :=
match n return (X ^^ n --> Y) -> ((Z -> X) ^^ n --> Y) with
| O    => fun f => f
| S n' => fun f g => app_1 (f (g z)) z
end f.

In order to use the information about f's type, it needs to be re-abstracted: in each branch, it'll have the right type.

2
votes

You can just delay getting your arguments until after n has been refined:

Fixpoint app_1 {X Y Z : Type} {n : nat}
  : (X ^^ n --> Y) -> Z -> (Z -> X) ^^ n --> Y :=
  match n return (X ^^ n --> Y) -> Z -> (Z -> X) ^^ n --> Y with
    | O    => fun f _ => f
    | S n' => fun f z g => app_1 (f (g z)) z
  end.

By the time f is bound, its type has already been changed into X ^^ 0 --> Y, and so it works out.

EDIT: Ah, I was going to add this, but Arthur beat me to it!

Fixpoint app_1 {X Y Z : Type} {n : nat} (f: X ^^ n --> Y) (z: Z)
  : (Z -> X) ^^ n --> Y :=
  match n return X ^^ n --> Y -> ((Z -> X) ^^ n --> Y) with
    | O    => fun f => f
    | S n' => fun f' g => app_1 (f' (g z)) z
  end f.