Finite list induction principle and the tail eliminator

Question

In Dybjer's Inductive Families the author present a method to derive an eliminator/induction principle for every inductive family of types.

In particular for the type of finite lists, namely $$List' \colon (A \colon set) (n \colon N) set$$ we get the eliminator $$\begin{align*} listrec' \colon &(A \colon set)\\ & (C \colon (a \colon N)(c \colon List'_A n)set) \\ & (e_1 \colon C(0,nil'_A)\\ & (e_2 \colon (b_1 \colon N)(b_2 \colon A)(u \colon List'_A(b_1))(v \colon C(b_1,u))C(s(b_1),cons'_A(b_1,b_2,u)))\\ & (a \colon N) \\ & (c \colon List'_A(a)) \\ & C(a,c)\ . \end{align*}$$

From what I get from this eliminator we should be able to provide any possible operation using finite lists.

Now my question is

how do we get the classical destructor $$tail \colon (A \colon set)(n \colon N)(List'_A(s(n))) List'_A n$$ that from any finite list gets its tail?

I am totally lost on how to approach this problem since the eliminator seems to be able to provide just function defined on the whole family $List'_A(n)$ and not on the sub-family $List'_A(s(n))$.

Thanks in advance.

Answer 1

I am totally lost on how to approach this problem since the eliminator seems to be able to provide just function defined on the whole family List′A(n) and not on the sub-family List′A(s(n)).

The typical trick in this situation is to pick a C such that you can pretend you are defining a function on the whole family when, in fact, you're only focusing on the sub-family you care about thanks to equality constraints.

Let me be more concrete:

If you pick C(n, xs) = (m:N) -> n = s(m) -> List'_A(m) then you can define a generalised gtail by using listrec', and derive tail as a corollary.

gtail : (A:set) (n:N) (xs : List'_A(n)) -> C(n, xs)
gtail A = listrec' A C
          contradiction -- of type: (m:N) -> 0 = s(m) -> List'_A(m)
          (\ _ _ u _ -> u)

tail : (A:set) (n:N) -> List′A (s(n)) -> List′An
tail A n xs = gtailn A (s(n)) xs n refl

Answer 2

What follows is just a little modification of the idea proposed in the accepted answer, nevertheless I think it can be of interest to other readers.

Here's a way to build tail

We can consider the predicate $P \colon (A\colon set)(n \colon N)(l \colon List'_A n)set$ defined (by recursion on natural numbers) as the only type family such that $$\begin{align*} P(A,0,l)&= 1\\ P(A, s(n),l) &= List'_A (n) \end{align*}$$ where $1$ is the unit type with only term $()$.

If we let $$e_1 = () \colon 1= P(A,0,nil')$$ and $$e_2=\lambda n \colon N.\lambda x \colon A.\lambda xs \colon List'_A n. \lambda p \colon P(A,n,xs). xs \colon (n \colon N)(x\colon A)(xs \colon List'_A n)(p \colon P(A,n,xs))\underbrace{List'_A(n)}_{=P(A,s(n),cons'_A(n,x,xs))}$$ we get $almostTail = (\lambda A \colon set) listrec'(A,P(A),e_1,e_2) \colon (A \colon set)(n \colon N)(l \colon List'_A(n))P(A,n,l)$ which by the reduction principle is such that $$almostTail(A,s(n),cons'_A(n,x,xs))=e_2(n,x,xs,almostTail(A,n,xs))=xs\ .$$

So we get $$tail' \colon (A\colon set)(n\colon N)(l \colon List'_A(s(n)))\underbrace{P(A,s(n),l)}_{List'_A(n)}$$ by letting $$tail'(A,n,l) = almostTile(A,s(n),l)\ .$$

Note: the only difference between gallais' example and mine is that instead of adding an hypothesis in the predicate to pass to $listrec'$ I have used a predicate with a don't care value for the case $n=0$.

In this case too we basically build a function defined on all the lists, with the desired behaviour in the case of interest (i.e. not empty lists), and then consider the specialized/restricted function for the sub-family of types we are interested in.