Variary Functions in Coq

The first challenge is giving such a function a type. I want the function to have T → list T when I pass it one input and T → T → T → list T when I pass it three inputs. Clearly we need to know ahead of time how many arguments to expect. If we expect n arguments, we can define the type like so:

Fixpoint narg (n : nat) (T : Set) (U : Set) : Set :=
  match n with
  | 0 => U
  | S n' => T -> (narg n' T U)
  end.

Here I've abstracted list T to U. In the heavily typed world of Coq, this sort of generality can actually be good, because it disciplines you and makes the proof search work better—I'll show you later.

Before dissecting the definition, here's some examples of it running:

Eval simpl in (narg 3). → fun T U : Set => T -> T -> T -> U

Note that narg 3 T U is a type.

That looks correct! Looking through the cases, narg takes an argument n that tells it how many T arguments a function will take before producing a U. If we expect no types, then a function that expects 0 arguments before returning a U is just a constant of type U.¹ [¹ In Racket, a function of no arguments and a constant are different things, but I think that's because of effects. I'll ignore the difference here.] If we expect n' + 1 arguments, then we expect one argument before expecting n' more before returning a U.

Coq likes this definition; it is a simple recursion on n, even though we're doing wild and wooly stuff like writing a function that returns a type.

My first attempt looked something like this:

Definition nlist (n : nat) (T : Set) : narg n T (list T) :=
  match n with
  | 0 => nil
  | S n' => fun t => cons t (nlist n' T)
  end.

This is definitely thinking in the right direction: with 0 arguments, we want to return nil, and with n + 1 arguments we want to return a function that takes one argument and then conses it on to the list. But it doesn't type check, because nlist n' T is not a list! It's a function waiting for god knows how many more arguments! We need to give that function all its arguments, and only then cons on the list.

This brought me to attempt number two:

Definition nlist (n : nat) (T : Set) : narg n T (list T) :=
  match n with
  | 0 => nil
  | S n' => fun t => compose (fun tail => cons t tail) (nlist n' T)
  end.

This is closer: since nlist n' T returns a function, and we want that function to run first and do something to the result, we want to use compose. So we say: first, run nlist n' T, which slurps up n' arguments. Then, take the list it produced, and add t to the front.

This is still not correct though, because Coq doesn't think of nlist n' T as a function that takes n' arguments; it thinks of nlist n' T as a function that takes one argument, and returns a function, which by the way you cannot cons things on to.

In other words, I need, not a normal compose, but variary composition function.

Variary composition should take a function from n T arguments to some output type U, then some function we can apply to U to get V, and return a function that takes n T arguments and produces the final output V. In Coq, this is:

Definition ncompose {n : nat} {T U V : Set} (f : U -> V) (g : narg n T U) : narg n T V.

Note that I finished this Definition with a period—that means I will do the proof in tactic mode. This is a weird, worst-practice feature of Coq that I absolutely love, because it means I can use the power of proof search to write my programs for me. The downside is that proof search usually doesn't care what proofs it finds, whereas I generally care what my functions compute. This is why I carefully specified narg to take a generic output type, instead of list T. By forcing the left hand side of the composition, g, and the result of the composition to return values of different types, I have written down a type with a single inhabitant for any given n, so whatever proof search finds, it will work correctly.

The proof is simple:

crush

Ok, that's a joke, but only sort-of, in that crush definitely finds the function. The solution without crush is:

induction n; simpl in *; auto.

The induction is clear: with 0 inputs we just want to apply f to the constant that g must be, and otherwise we want to do some other stuff that's recursive. But it turns out that simplifying the inductive hypothesis here yields a function narg n' T U → narg n' T V, where n' + 1 = n, whereas we need to produce a function (T → narg n' T U) → (T → narg n' T V). So it's just a normal composition away.

Finally, note that I've defined n, T, U, and V as implicit arguments in ncompose, since they appear in the other arguments. This means you can use ncompose like normal compose if the right hand side has an narg-based type.² [² If it has a type like T → T → U, Coq won't immediately know that that's just a reduction of narg 2 T U, so you'll need to add types or implicit arguments somewhere.]

(Since this is a tactic definition, remember to end it with Defined., not with QED, because we want the function to be something Coq can compute through.)

Now that we have variary composition nlist can be modified from the last failed attempt into a successful function:

Fixpoint nlist (n : nat) (T : Set) : narg n T (list T) :=
  match n with
  | 0 => nil
  | S n' => fun t => ncompose (fun x => cons t x) (nlist n' T)
  end.

This works!

And to show that it really does the right thing (instead of just returning nil), we can look at nlist for particular n:

Eval simpl in (nlist 3). ⇝ fun (T : Set) (t H H0 : T) => (t :: H :: H0 :: nil)%list

The syntax is as charmingly ugly as Coq usually is, but the point is that nlist 3 takes 3 T arguments (inexplicably named, in the usual Coq style, t, H, and H0)and puts them in a list in order.

If you want to write a variary function, the easiest way to do it is to build on ncompose and nlist. For example, variary addition can be decomposed into gathering the arguments into a list:

Definition add (n : nat) : narg n nat nat :=
  ncompose sum (nlist n nat).

and then summing them:

Fixpoint sum (l : list nat) : nat :=
  match l with
  | nil => 0
  | cons x rest => x + sum rest
  end.

Unfortunately, n here cannot be made implicit, preventing you from evaluating add 1 2 3 4. Instead, n is explicit, so you have to write:³ [³ I used compute instead of simpl here because, I think, add isn't notated to expand when its first argument is in WHN form. If you add that notation, using some arcane Vernacular that I don't want to look up, it would probably work with simpl as well.]

Eval compute in (add 4 1 2 3 4). ⇝ 10

The reason n can't be made implicit is that then Coq would be staring at (add ?n) 1 and it would only know that that function term had type nargs ?n nat nat. Since nargs matches on its first argument, ?n, Coq can't expand nargs, so it can't find out that it is a function type. Since it can't figure that out, it's not sure that add 1 2 3 type checks!

Once we have nlist in Coq, we can prove things about it. The easiest thing to prove would be that nlist takes n arguments and returns a list of length n. The main challenge is stating the theorem.

The first step, I think, is to get the list length idea into Prop:

Definition has_length_n (n : nat) (T : Set) (l : list T) : Prop :=
  length l = n.

Theorem nlist_length : forall n T, ncompose (has_length_n n T) (nlist n T).

However, this doesn't quite work, because the type of that theorem statement is narg n T Prop, instead of Prop. That makes sense: we don't want to say that nlist has length n for all n and T. We also want to quantify over several arguments!

I sort of thought that something like this should work:

Fixpoint nforall (n : nat) (T : Set) (P : narg n T Prop) : Prop :=
  match n with
  | 0 => P
  | S n' => forall (t : T), nforall n' T (P t)
  end.

Theorem nlist_length : forall n T, nforall n T (ncompose (has_length_n n T) (nlist n T)).

But I think I am missing some wacky motive nonsense on the definition of nforall, nonsense that doesn't get easier, sadly, in tactic mode. So I think I am a bit stuck here. I'd appreciate help!

In particular, I pose as a challenge: Find a way to implement nforall with the expected semantics, and then prove nlist_length.

Update: James has posted a solution to the challenge. The key is to allow relations on the output of two narg calls. (His solution also changes Set to Type above to allow Prop as an inhabitant.)

Update: Valentin points out that Coq's Numbers.NaryFunctions library replicates much of the functionality described here.