4
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ 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. $\endgroup$ – Gilles 'SO- stop being evil' Aug 23 '18 at 16:24
  • $\begingroup$ @Gilles I have give a lookbat Coq stdlib, it seems that they use a form of pattern matching not eliminators. $\endgroup$ – Giorgio Mossa Aug 25 '18 at 11:32
3
$\begingroup$

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
$\endgroup$
  • $\begingroup$ 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. $\endgroup$ – Giorgio Mossa Aug 27 '18 at 7:55
  • $\begingroup$ 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). $\endgroup$ – gallais Aug 27 '18 at 8:40
  • $\begingroup$ 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. $\endgroup$ – Giorgio Mossa Aug 27 '18 at 13:37
  • $\begingroup$ You don't provide a 0 = s(m), you are given one in the nil case. $\endgroup$ – gallais Aug 27 '18 at 13:40
  • $\begingroup$ I got it, silly me, I had misread the type of contradiction. Perfect. Thank you so much. $\endgroup$ – Giorgio Mossa Aug 27 '18 at 14:21
1
$\begingroup$

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.

$\endgroup$
  • 1
    $\begingroup$ 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 $\endgroup$ – gallais Aug 27 '18 at 18:44

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.