# Finite list induction principle and the tail eliminator

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))$.

• There must be an answer in the Coq standard library. Coq calls the type of lists of a given length “vector”. I don't know if the code would be comprehensible though. – Gilles 'SO- stop being evil' Aug 23 '18 at 16:24
• @Gilles I have give a lookbat Coq stdlib, it seems that they use a form of pattern matching not eliminators. – Giorgio Mossa Aug 25 '18 at 11:32

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

• Thanks for the answer. I have doubt, It is not clear to me how you can provide the term contradiction which by its very definition should not exist. – Giorgio Mossa Aug 27 '18 at 7:55
• Contradiction can exist just fine as long as you have large elimination. Cf. hal.archives-ouvertes.fr/inria-00489412 You're not asked to prove False, you're asked to prove anything given an (absurd) proof of 0 = s(m). – gallais Aug 27 '18 at 8:40
• I'm not following, you provide a $0 = s(m)$ which is a constant (or did I miss a lambda lurking around) and should not be derivable (or did I miss something). Anyway I think I got the idea. I just need some time to digest it. Thanks again. – Giorgio Mossa Aug 27 '18 at 13:37
• You don't provide a 0 = s(m), you are given one in the nil case. – gallais Aug 27 '18 at 13:40
• I got it, silly me, I had misread the type of contradiction. Perfect. Thank you so much. – Giorgio Mossa Aug 27 '18 at 14:21

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.

• Nice one! We have the same dichotomy in Agda's standard library between e.g. from-just : (x : Maybe A) → From-just x which computes the return type and only does something interesting if x has the right shape and to-witness : (m : Maybe P) → Is-just m → P which uses a constraint to ensure the argument has the right shape to begin with. Both are useful! Link to the module in question: agda.github.io/agda-stdlib/Data.Maybe.Base.html – gallais Aug 27 '18 at 18:44