At

Posted on 2017-04-28 by nbloomf

Tags: arithmetic-made-difficult, literate-haskell

$\newcommand{\hyp}[2]{\stackrel{\tiny\text{hyp}}{#2}}$ $\newcommand{\let}[2]{\stackrel{\tiny\text{let}}{#2}}$ $\newcommand{\a}{a}$ $\newcommand{\b}{b}$ $\newcommand{\c}{c}$ $\newcommand{\p}{p}$ $\newcommand{\q}{q}$ $\newcommand{\r}{r}$ $\newcommand{\s}{s}$ $\newcommand{\x}{x}$ $\newcommand{\y}{y}$ $\newcommand{\z}{z}$ $\newcommand{\bool}{\mathbb{B}}$ $\newcommand{\btrue}{\mathsf{true}}$ $\newcommand{\bfalse}{\mathsf{false}}$ $\newcommand{\bnot}{\mathsf{not}}$ $\newcommand{\band}{\mathbin{\mathsf{and}}}$ $\newcommand{\bor}{\mathbin{\mathsf{or}}}$ $\newcommand{\bimpl}{\mathbin{\mathsf{impl}}}$ $\newcommand{\beq}{\mathsf{eq}}$ $\newcommand{\bif}[3]{\mathsf{if}\left(#1,#2,#3\right)}$ $\newcommand{\id}{\mathsf{id}}$ $\newcommand{\compose}{\mathsf{compose}}$ $\newcommand{\const}{\mathsf{const}}$ $\newcommand{\apply}{\mathsf{apply}}$ $\newcommand{\flip}{\mathsf{flip}}$ $\newcommand{\flipB}{\mathsf{flip2}}$ $\newcommand{\flipC}{\mathsf{flip3}}$ $\newcommand{\flipD}{\mathsf{flip4}}$ $\newcommand{\flipE}{\mathsf{flip5}}$ $\newcommand{\clone}{\mathsf{clone}}$ $\newcommand{\cloneC}{\mathsf{clone3}}$ $\newcommand{\composeAonB}{\mathsf{compose1on2}}$ $\newcommand{\composeAonC}{\mathsf{compose1on3}}$ $\newcommand{\composeAonD}{\mathsf{compose1on4}}$ $\newcommand{\composeBonA}{\mathsf{compose2on1}}$ $\newcommand{\composeBonB}{\mathsf{compose2on2}}$ $\newcommand{\composeConA}{\mathsf{compose3on1}}$ $\newcommand{\ptrue}{\mathsf{ptrue}}$ $\newcommand{\pfalse}{\mathsf{pfalse}}$ $\newcommand{\pnot}{\mathsf{pnot}}$ $\newcommand{\pand}{\mathbin{\mathsf{pand}}}$ $\newcommand{\por}{\mathbin{\mathsf{por}}}$ $\newcommand{\pimpl}{\mathbin{\mathsf{pimpl}}}$ $\newcommand{\fst}{\mathsf{first}}$ $\newcommand{\snd}{\mathsf{second}}$ $\newcommand{\dup}{\mathsf{dup}}$ $\newcommand{\tup}{\mathsf{tup}}$ $\newcommand{\tSwap}{\mathsf{swap}_{\times}}$ $\newcommand{\tPair}{\mathsf{pair}_{\times}}$ $\newcommand{\tAssocL}{\mathsf{assocL}_{\times}}$ $\newcommand{\tAssocR}{\mathsf{assocR}_{\times}}$ $\newcommand{\tupL}{\mathsf{tupL}}$ $\newcommand{\tupR}{\mathsf{tupR}}$ $\newcommand{\uncurry}{\mathsf{uncurry}}$ $\newcommand{\curry}{\mathsf{curry}}$ $\newcommand{\lft}{\mathsf{left}}$ $\newcommand{\rgt}{\mathsf{right}}$ $\newcommand{\either}{\mathsf{either}}$ $\newcommand{\uSwap}{\mathsf{swap}_{+}}$ $\newcommand{\uPair}{\mathsf{pair}_{+}}$ $\newcommand{\uAssocL}{\mathsf{assocL}_{+}}$ $\newcommand{\uAssocR}{\mathsf{assocR}_{+}}$ $\newcommand{\isLft}{\mathsf{isLeft}}$ $\newcommand{\isRgt}{\mathsf{isRight}}$ $\newcommand{\nats}{\mathbb{N}}$ $\newcommand{\zero}{\mathsf{0}}$ $\newcommand{\next}{\mathsf{next}}$ $\newcommand{\unnext}{\mathsf{unnext}}$ $\newcommand{\iszero}{\mathsf{isZero}}$ $\newcommand{\prev}{\mathsf{prev}}$ $\newcommand{\natrec}{\mathsf{natrec}}$ $\newcommand{\simprec}{\mathsf{simprec}}$ $\newcommand{\bailrec}{\mathsf{bailrec}}$ $\newcommand{\mutrec}{\mathsf{mutrec}}$ $\newcommand{\dnatrec}{\mathsf{dnatrec}}$ $\newcommand{\normrec}{\mathsf{normrec}}$ $\newcommand{\findsmallest}{\mathsf{findsmallest}}$ $\newcommand{\mnormrec}{\mathsf{mnormrec}}$ $\newcommand{\nequal}{\mathsf{eq}}$ $\newcommand{\nplus}{\mathsf{plus}}$ $\newcommand{\ntimes}{\mathsf{times}}$ $\newcommand{\nleq}{\mathsf{leq}}$ $\newcommand{\ngeq}{\mathsf{geq}}$ $\newcommand{\nminus}{\mathsf{minus}}$ $\newcommand{\nmax}{\mathsf{max}}$ $\newcommand{\nmin}{\mathsf{min}}$ $\newcommand{\ndivalg}{\mathsf{divalg}}$ $\newcommand{\nquo}{\mathsf{quo}}$ $\newcommand{\nrem}{\mathsf{rem}}$ $\newcommand{\ndiv}{\mathsf{div}}$ $\newcommand{\ngcd}{\mathsf{gcd}}$ $\newcommand{\ncoprime}{\mathsf{coprime}}$ $\newcommand{\nlcm}{\mathsf{lcm}}$ $\newcommand{\nmindiv}{\mathsf{mindiv}}$ $\newcommand{\nisprime}{\mathsf{isPrime}}$ $\newcommand{\npower}{\mathsf{power}}$ $\newcommand{\nchoose}{\mathsf{choose}}$ $\newcommand{\dom}{\mathsf{dom}}$ $\newcommand{\cod}{\mathsf{cod}}$ $\newcommand{\lists}[1]{\mathsf{List}(#1)}$ $\newcommand{\nil}{\mathsf{nil}}$ $\newcommand{\cons}{\mathsf{cons}}$ $\newcommand{\uncons}{\mathsf{uncons}}$ $\newcommand{\isnil}{\mathsf{isNil}}$ $\newcommand{\tail}{\mathsf{tail}}$ $\newcommand{\head}{\mathsf{head}}$ $\newcommand{\foldr}{\mathsf{foldr}}$ $\newcommand{\foldl}{\mathsf{foldl}}$ $\newcommand{\tacunfoldN}{\mathsf{tacunfoldN}}$ $\newcommand{\unfoldN}{\mathsf{unfoldN}}$ $\newcommand{\dfoldr}{\mathsf{dfoldr}}$ $\newcommand{\cfoldr}{\mathsf{cfoldr}}$ $\newcommand{\bfoldr}{\mathsf{bfoldr}}$ $\newcommand{\dbfoldr}{\mathsf{dbfoldr}}$ $\newcommand{\lfoldr}{\mathsf{lfoldr}}$ $\newcommand{\snoc}{\mathsf{snoc}}$ $\newcommand{\revcat}{\mathsf{revcat}}$ $\newcommand{\rev}{\mathsf{rev}}$ $\newcommand{\last}{\mathsf{last}}$ $\newcommand{\cat}{\mathsf{cat}}$ $\newcommand{\addlength}{\mathsf{addlength}}$ $\newcommand{\length}{\mathsf{length}}$ $\newcommand{\head}{\mathsf{head}}$ $\newcommand{\at}{\mathsf{at}}$ $\newcommand{\map}{\mathsf{map}}$ $\newcommand{\range}{\mathsf{range}}$ $\newcommand{\zip}{\mathsf{zip}}$ $\newcommand{\zipPad}{\mathsf{zipPad}}$ $\newcommand{\unzip}{\mathsf{unzip}}$ $\newcommand{\prefix}{\mathsf{prefix}}$ $\newcommand{\suffix}{\mathsf{suffix}}$ $\newcommand{\lcp}{\mathsf{lcp}}$ $\newcommand{\lcs}{\mathsf{lcs}}$ $\newcommand{\all}{\mathsf{all}}$ $\newcommand{\any}{\mathsf{any}}$ $\newcommand{\tails}{\mathsf{tails}}$ $\newcommand{\inits}{\mathsf{inits}}$ $\newcommand{\filter}{\mathsf{filter}}$ $\newcommand{\elt}{\mathsf{elt}}$ $\newcommand{\addcount}{\mathsf{addcount}}$ $\newcommand{\count}{\mathsf{count}}$ $\newcommand{\repeat}{\mathsf{repeat}}$ $\newcommand{\sublist}{\mathsf{sublist}}$ $\newcommand{\infix}{\mathsf{infix}}$ $\newcommand{\select}{\mathsf{select}}$ $\newcommand{\unique}{\mathsf{unique}}$ $\newcommand{\delete}{\mathsf{delete}}$ $\newcommand{\dedupeL}{\mathsf{dedupeL}}$ $\newcommand{\dedupeR}{\mathsf{dedupeR}}$ $\newcommand{\common}{\mathsf{common}}$ $\newcommand{\disjoint}{\mathsf{disjoint}}$ $\newcommand{\sublists}{\mathsf{sublists}}$ $\newcommand{\take}{\mathsf{take}}$ $\newcommand{\drop}{\mathsf{drop}}$ $\newcommand{\takeBut}{\mathsf{takeBut}}$ $\newcommand{\dropBut}{\mathsf{dropBut}}$ $\newcommand{\takeWhile}{\mathsf{takeWhile}}$ $\newcommand{\dropWhile}{\mathsf{dropWhile}}$

This page is part of a series on Arithmetic Made Difficult.

This post is literate Haskell; you can load the source into GHCi and play along.

{-# LANGUAGE NoImplicitPrelude #-}
module At
  ( at, _test_at, main_at
  ) where

import Testing
import Booleans
import DisjointUnions
import NaturalNumbers
import BailoutRecursion
import Plus
import LessThanOrEqualTo
import Lists
import HeadAndTail
import Snoc
import Reverse
import Cat
import Length

The $\head$ function attempts to extract the “first” item in a list; in this post we’ll generalize to $\at$, which extracts the element at an arbitrary position in a list.

Define $\beta : \nats \times \lists{A} \rightarrow \bool$ by \[\beta(k,x) = \isnil(x),\] $\psi : \nats \times \lists{A} \rightarrow 1 + A$ by \[\psi(k,x) = \lft(\ast),\] and $\omega : \nats \times \lists{A} \rightarrow \lists{A}$ by \[\omega(k,x) = \tail(x).\] We then define $\at : \lists{A} \times \nats \rightarrow \ast + A$ by \[\at(x,k) = \bailrec(\head)(\beta)(\psi)(\omega)(k,x).\]

In Haskell:

at :: (Natural n, Equal n, List t) => t a -> n -> Union () a
at x k = bailoutRec head beta psi omega k x
  where
    beta _ z = isNil z
    psi _ _ = lft ()
    omega _ z = tail z

Since $\at$ is defined in terms of $\bailrec$, it is the unique solution to a system of functional equations.

$\at$ is the unique map $f : \nats \times \lists{A} \rightarrow 1 + A$ such that the following hold for all $n \in \nats$, $a \in A$, and $x \in \lists{A}$. \[\left\{\begin{array}{l} f(x,\zero) = \head(x) \\ f(x,\next(n)) = \bif{\isnil(x)}{\lft(\ast)}{f(\tail(x),n)} \end{array}\right.\]

_test_at_zero
  :: (List t, Equal a, Equal (t a), Natural n, Equal n)
  => t a -> n -> Test (t a -> Bool)
_test_at_zero _ k =
  testName "at(x,zero) == head(x)" $
  \x -> eq
    (at x (zero `withTypeOf` k))
    (head x)


_test_at_next
  :: (List t, Equal a, Equal (t a), Natural n, Equal n)
  => t a -> n -> Test (n -> t a -> Bool)
_test_at_next _ k =
  testName "at(x,next(n)) == if(isNil(x),lft(*),at(tail(x),n))" $
  \n x -> eq
    (at x ((next n) `withTypeOf` k))
    (if isNil x then lft () else at (tail x) n)

$\at$ interacts with $\cons$ and $\next$.

Let $A$ be a set. For all $a \in A$, $x \in \lists{A}$, and $k \in \nats$, we have \[\at(\cons(a,x),\next(k)) = \at(x,k).\]

Note that \[\begin{eqnarray*} & & \at(\cons(a,x),\next(k)) \\ & \href{/posts/arithmetic-made-difficult/At.html#cor-at-next} = & \bif{\isnil(\cons(a,x))}{\lft(\ast)}{\at(\tail(\cons(a,x)),k)} \\ & \href{/posts/arithmetic-made-difficult/HeadAndTail.html#thm-isnil-cons} = & \bif{\bfalse}{\lft(\ast)}{\at(\tail(\cons(a,x)),k)} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & \at(\tail(\cons(a,x)),k) \\ & \href{/posts/arithmetic-made-difficult/HeadAndTail.html#thm-tail-cons} = & \at(x,k) \end{eqnarray*}\] as claimed.

_test_at_next_next_cons
  :: (List t, Equal a, Equal (t a), Natural n, Equal n)
  => t a -> n -> Test (t a -> a -> n -> Bool)
_test_at_next_next_cons _ _ =
  testName "at(cons(a,x),next(next(k))) == at(x,next(k))" $
  \x a k -> eq (at (cons a x) (next k)) (at x k)

Let’s trace some special cases.

Let $A$ be a set. The following hold for all $a,b \in A$, $x \in \lists{A}$, and $k \in \nats$.

$\at(\nil,k) = \lft(\ast)$.
$\at(\cons(a,x),\zero) = \rgt(a)$.
$\at(\cons(a,\cons(b,x)),\next(\zero)) = \rgt(b)$.

We consider two cases: $k = \zero$ and $k \neq \zero$. If $k = \zero$, we of course have \[\begin{eqnarray*} & & \at(\nil,\zero) \\ & \href{/posts/arithmetic-made-difficult/At.html#thm-at-nil} = & \lft(\ast) \end{eqnarray*}\] as claimed. If $k = \next(m)$, we have \[\begin{eqnarray*} & & \at(\nil,\next(m)) \\ & \href{/posts/arithmetic-made-difficult/At.html#cor-at-next} = & \bif{\isnil(\nil)}{\lft(\ast)}{\at(\tail(\nil),m)} \\ & \href{/posts/arithmetic-made-difficult/HeadAndTail.html#thm-isnil-nil} = & \bif{\btrue}{\lft(\ast)}{\at(\tail(\nil),m)} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & \lft(\ast) \end{eqnarray*}\] as claimed.
We have \[\begin{eqnarray*} & & \at(\cons(a,x),\zero) \\ & \href{/posts/arithmetic-made-difficult/At.html#cor-at-zero} = & \head(\cons(a,x)) \\ & \href{/posts/arithmetic-made-difficult/HeadAndTail.html#thm-head-cons} = & \rgt(a) \end{eqnarray*}\] as claimed.
We have \[\begin{eqnarray*} & & \at(\cons(a,\cons(b,x)),\next(\zero)) \\ & \href{/posts/arithmetic-made-difficult/At.html#thm-at-cons-next} = & \at(\cons(b,x),\zero) \\ & \href{/posts/arithmetic-made-difficult/At.html#thm-at-cons-zero} = & \rgt(b) \end{eqnarray*}\] as claimed.

_test_at_nil :: (List t, Equal a, Equal (t a), Natural n, Equal n)
  => t a -> n -> Test (n -> Bool)
_test_at_nil t _ =
  testName "at(nil,k) == lft(*)" $
  \n -> eq
    (at (nil `withTypeOf` t) n)
    (lft ())


_test_at_single :: (List t, Equal a, Equal (t a), Natural n, Equal n)
  => t a -> n -> Test (a -> t a -> Bool)
_test_at_single _ k =
  testName "at(cons(a,nil),next(0)) == rgt(a)" $
  \a x -> eq
    (at (cons a x) (zero `withTypeOf` k))
    (rgt a)


_test_at_double :: (List t, Equal a, Equal (t a), Natural n, Equal n)
  => t a -> n -> Test (a -> a -> t a -> Bool)
_test_at_double _ k =
  testName "at(cons(a,cons(b,nil)),next(next(0))) == rgt(b)" $
  \a b x -> eq
    (at (cons a (cons b x)) (next (zero `withTypeOf` k)))
    (rgt b)

$\at$ interacts with $\length$.

Let $A$ be a set and let $z \in \lists{A}$.

$\at(\cons(a,x),\length(x)) = \head(\rev(\cons(a,x)))$.
$\at(x,\length(x)) = \lft(\ast)$.

We proceed by list induction on $x$. For the base case $x = \nil$, we have \[\begin{eqnarray*} & & \at(\cons(a,\nil),\length(\nil)) \\ & \href{/posts/arithmetic-made-difficult/Length.html#cor-length-nil} = & \at(\cons(a,\nil),\zero) \\ & = & \rgt(a) \\ & \href{/posts/arithmetic-made-difficult/HeadAndTail.html#thm-head-cons} = & \head(\cons(a,\nil)) \\ & = & \head(\rev(\cons(a,\nil))) \end{eqnarray*}\] as needed. For the inductive step, suppose the implication holds for all $a$ for some $x$, and let $b \in A$. Now \[\begin{eqnarray*} & & \at(\cons(a,\cons(b,x)),\length(\cons(b,x))) \\ & \href{/posts/arithmetic-made-difficult/Length.html#cor-length-cons} = & \at(\cons(a,\cons(b,x)),\next(\length(x))) \\ & = & \at(\cons(b,x),length(x)) \\ & = & \head(\rev(\cons(b,x))) \\ & = & \head(\snoc(a,\rev(\cons(b,x)))) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-cons} = & \head(\rev(\cons(a,\cons(b,x)))) \end{eqnarray*}\] as needed.
We proceed by list induction on $x$. For the base case $x = \nil$, we have \[\begin{eqnarray*} & & \at(\nil,\length(\nil)) \\ & \href{/posts/arithmetic-made-difficult/At.html#thm-at-nil} = & \lft(\ast) \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for some $x$, and let $a \in A$. Now \[\begin{eqnarray*} & & \at(\cons(a,x),\length(\cons(a,x))) \\ & \href{/posts/arithmetic-made-difficult/Length.html#cor-length-cons} = & \at(\cons(a,x),\next(\length(x))) \\ & = & \at(x,\length(x)) \\ & \href{/posts/arithmetic-made-difficult/At.html#thm-at-length} = & \lft(\ast) \end{eqnarray*}\] as needed.

_test_at_length
  :: (List t, Equal a, Equal (t a), Natural n, Equal n)
  => t a -> n -> Test (a -> t a -> Bool)
_test_at_length _ k =
  testName "at(cons(a,x),length(x)) == head(rev(cons(a,x)))" $
  \a x -> eq
    (at (cons a x) ((length x) `withTypeOf` k))
    (head (rev (cons a x)))


_test_at_next_length
  :: (List t, Equal a, Equal (t a), Natural n, Equal n)
  => t a -> n -> Test (t a -> Bool)
_test_at_next_length _ k =
  testName "at(x,next(length(x))) == lft(*)" $
  \x -> eq
    (at x ((length x) `withTypeOf` k))
    (lft ())

$\at$ interacts with $\snoc$.

Let $A$ be a set. Let $a,b \in A$ and $x \in \lists{A}$.

If $\nleq(k,\length(x))$ then $\at(\snoc(a,\cons(b,x)),k) = \at(\cons(b,x),k)$.
$\at(\snoc(a,x),\length(x)) = \rgt(a)$.

We proceed by induction on $k$. For the base case $k = \zero$, note that $\nleq(k,\length(x))$, and we have \[\begin{eqnarray*} & & \at(\snoc(a,\cons(b,x)),\zero) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-cons} = & \at(\cons(b,\snoc(a,x)),\zero) \\ & \href{/posts/arithmetic-made-difficult/At.html#thm-at-cons-zero} = & \rgt(b) \\ & \href{/posts/arithmetic-made-difficult/At.html#thm-at-cons-zero} = & \at(\cons(b,x),\zero) \end{eqnarray*}\] as needed. For the inductive step, suppose the implication holds for all $x$, $a$, and $b$ for some $k$, and suppose further that $\nleq(\next(k),\length(x))$. In particular, we must have $x = \cons(c,u)$ for some $c \in A$ and $u \in \lists{A}$, and $\nleq(k,\length(u))$. Now we have \[\begin{eqnarray*} & & \at(\snoc(a,\cons(b,x)),\next(k)) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-cons} = & \at(\cons(b,\snoc(a,x)),\next(k)) \\ & \href{/posts/arithmetic-made-difficult/At.html#thm-at-cons-next} = & \at(\snoc(a,x),k) \\ & \hyp{x = \cons(c,u)} = & \at(\snoc(a,\cons(c,u)),k) \\ & = & \at(\cons(c,u),k) \\ & \hyp{x = \cons(c,u)} = & \at(x,k) \\ & \href{/posts/arithmetic-made-difficult/At.html#thm-at-cons-next} = & \at(\cons(b,x),\next(k)) \end{eqnarray*}\] as needed.
We proceed by list induction on $x$. For the base case $x = \nil$, we have \[\begin{eqnarray*} & & \at(\snoc(a,\nil),\length(\nil)) \\ & \href{/posts/arithmetic-made-difficult/Length.html#cor-length-nil} = & \at(\snoc(a,\nil),\zero) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-nil} = & \at(\cons(a,\nil),\zero) \\ & \href{/posts/arithmetic-made-difficult/At.html#thm-at-cons-zero} = & \rgt(a) \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for all $a$ for some $x$, and let $b \in A$. Now \[\begin{eqnarray*} & & \at(\snoc(a,\cons(b,x)),\length(\cons(b,x))) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-cons} = & \at(\cons(b,\snoc(a,x)),\length(\cons(b,x))) \\ & \href{/posts/arithmetic-made-difficult/Length.html#cor-length-cons} = & \at(\cons(b,\snoc(a,x)),\next(\length(x))) \\ & \href{/posts/arithmetic-made-difficult/At.html#thm-at-cons-next} = & \at(\snoc(a,x),\length(x)) \\ & \hyp{\at(\snoc(a,x),\length(x)) = \rgt(a)} = & \rgt(a) \end{eqnarray*}\] as needed.

_test_at_snoc
  :: (List t, Equal a, Equal (t a), Natural n, Equal n)
  => t a -> n -> Test (t a -> a -> a -> n -> Bool)
_test_at_snoc _ _ =
  testName "if leq(k,length(x)) then at(snoc(a,cons(b,x)),k) == at(cons(b,x),k)" $
  \x a b k -> if leq k (length x)
    then eq (at (snoc a (cons b x)) k) (at (cons b x) k)
    else true


_test_at_snoc_length
  :: (List t, Equal a, Equal (t a), Natural n, Equal n)
  => t a -> n -> Test (t a -> a -> Bool)
_test_at_snoc_length _ k =
  testName "at(snoc(a,x),length(x)) == rgt(a)" $
  \x a -> eq (at (snoc a x) ((length x) `withTypeOf` k)) (rgt a)

$\at$ interacts with $\rev$.

Let $A$ be a set. Let $x \in \lists{A}$ and $u,v \in \nats$. If $\next(\nplus(u,v)) = \length(x)$, then we have \[\at(\rev(x),v) = \at(x,u).\]

We proceed by list induction on $x$. For the base case $x = \nil$, note that $\length(x) = \zero$, so that $\next(\nplus(u,v)) = \length(x)$ is false for all $u$ and $v$, and thus the implication holds vacuously. For the inductive step, suppose the implication holds for all $u$ and $v$ for some $x$ and let $a \in A$. Suppose further that $\next(\nplus(u,v)) = \length(\cons(a,x))$. We have two possibilities for $u$. If $u = \zero$, we have $\next(v) = \length(\cons(a,x))$ and thus $v = \length(x)$. In this case, we have \[\begin{eqnarray*} & & \at(\cons(a,x),u) \\ & \let{u = \zero} = & \at(\cons(a,x),\zero) \\ & \href{/posts/arithmetic-made-difficult/At.html#thm-at-cons-zero} = & \rgt(a) \\ & \href{/posts/arithmetic-made-difficult/At.html#thm-at-snoc-length} = & \at(\snoc(a,\rev(x)),\length(\rev(x))) \\ & \href{/posts/arithmetic-made-difficult/Length.html#thm-length-rev} = & \at(\snoc(a,\rev(x)),\length(x)) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-cons} = & \at(\rev(\cons(a,x)),\length(x)) \\ & \hyp{v = \length(x)} = & \at(\rev(\cons(a,x)),v) \end{eqnarray*}\] as needed. If $u = \next(w)$, then we have $\next(\nplus(w,v)) = \length(x)$. In particular, we have $x \neq \nil$ and thus $\rev(x) \neq \nil$; say $\rev(x) = \cons(c,y)$. Now $\nleq(v,\length(y))$, and moreover \[\begin{eqnarray*} & & \at(\cons(a,x),u) \\ & \let{u = \next(w)} = & \at(\cons(a,x),\next(w)) \\ & \href{/posts/arithmetic-made-difficult/At.html#thm-at-cons-next} = & \at(x,w) \\ & = & \at(\rev(x),v) \\ & = & \at(\cons(c,y),v) \\ & = & \at(\snoc(a,\cons(c,y)),v) \\ & = & \at(\snoc(a,\rev(x)),v) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-cons} = & \at(\rev(\cons(a,x)),v) \end{eqnarray*}\] as needed.

_test_at_rev :: (List t, Equal a, Equal (t a), Natural n, Equal n)
  => t a -> n -> Test (t a -> n -> n -> Bool)
_test_at_rev _ _ =
  testName "if eq(next(plus(u,v)),length(x)) then eq(at(x,u),at(rev(x),v))" $
  \x u v -> if eq (next (plus u v)) (length x)
    then eq (at x u) (at (rev x) v)
    else true

$\at$ interacts with $\cat$.

Let $A$ be a set. For all $a \in A$, $x,y \in \lists{A}$ and $k \in \nats$, we have the following.

If $\nleq(k,\length(x))$, then $\at(\cat(\cons(a,x),y),k) = \at(\cons(a,x),k)$.
If $\at(\cat(\cons(a,x),y),\nplus(\next(\length(x)),k)) = \at(y,k)$.

We proceed by list induction on $y$. For the base case $y = \nil$, we have \[\begin{eqnarray*} & & \at(\cat(\cons(a,x),\nil),k) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#thm-cat-nil-right} = & \at(\cons(a,x),k) \end{eqnarray*}\] as claimed. For the inductive step, suppose the implication holds for all $k$, $a$, and $x$ for some $y$, and let $b \in A$, and suppose further that $\nleq(k,\length(x))$. Using the inductive hypothesis we have \[\begin{eqnarray*} & & \at(\cat(\cons(a,x),\cons(b,y)),k) \\ & \href{/posts/arithmetic-made-difficult/Cat.html#thm-cat-snoc-left} = & \at(\cat(\snoc(b,\cons(a,x)),y),k) \\ & = & \at(\snoc(b,\cons(a,x)),k) \\ & = & \at(\cons(a,x),k) \end{eqnarray*}\] as needed.
We proceed by list induction on $x$. For the base case $x = \nil$, we have \[\begin{eqnarray*} & & \at(\cat(\cons(a,\nil),y),\nplus(\next(\length(\nil)),k)) \\ & = & \at(\cons(a,\cat(\nil,y)),\next(\nplus(\zero,k))) \\ & = & \at(\cons(a,y),\next(k)) \\ & \href{/posts/arithmetic-made-difficult/At.html#thm-at-cons-next} = & \at(y,k) \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for all $a$, $y$, and $k$ for some $x$, and let $b \in A$. Note that $\snoc(b,x) = \cons(c,u)$ for some $c$ and u$, where $\length(x) = \next(\length(u))$. Now \[\begin{eqnarray*} & & \at(\cat(\cons(a,x),\cons(b,y)),\nplus(\next(\length(x)),k)) \\ & = & \at(\cat(\snoc(b,\cons(a,x)),y),\next(\nplus(\length(x),k))) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#cor-snoc-cons} = & \at(\cat(\cons(a,\snoc(b,x)),y),\next(\nplus(\length(x),k))) \\ & = & \at(\cons(a,\cat(\snoc(b,x)),y),\next(\nplus(\length(x),k))) \\ & = & \at(\cat(\snoc(b,x),y),\nplus(\length(u),k)) \\ & = & \at(\cat(\snoc(b,x),y),\nplus(\next(\length(u)),k)) \\ & = & \at(\cat(\cons(c,u),y),\nplus(\next(\length(u)),k)) \\ & = & \at(\cons(b,y),k) \end{eqnarray*}\] as needed.

_test_at_cat_left :: (List t, Equal a, Equal (t a), Natural n, Equal n)
  => t a -> n -> Test (a -> t a -> t a -> n -> Bool)
_test_at_cat_left _ _ =
  testName "if leq(k,length(x)) then eq(at(cat(cons(a,x),y),k),at(cons(a,x),k))" $
  \a x y k -> if leq k (length x)
    then eq (at (cat (cons a x) y) k) (at (cons a x) k)
    else true


_test_at_cat_right :: (List t, Equal a, Equal (t a), Natural n, Equal n)
  => t a -> n -> Test (a -> t a -> t a -> n -> Bool)
_test_at_cat_right _ _ =
  testName "eq(at(cat(cons(a,x),y),plus(next(length(x)),k)),at(y,k))" $
  \a x y k -> eq
    (at (cat (cons a x) y) (plus (next (length x)) k))
    (at y k)

We can characterize the $k$s such that $\at(x,k)$ is a $\lft$ or a $\rgt$.

Let $A$ be a set. For all $x \in \lists{A}$ and $k \in \nats$ we have the following.

If $\nleq(\length(x),k)$, then $\at(x,k) = \lft(\ast)$.
If $\nleq(k,\length(x))$, then $\at(\cons(a,x),k) = \rgt(b)$ for some $b \in A$.

We proceed by list induction on $x$. For the base case $x = \nil$, note that for any $k$ we have $\nleq(\zero,k)$ and \[\begin{eqnarray*} & & \at(\nil,k) \\ & \href{/posts/arithmetic-made-difficult/At.html#thm-at-nil} = & \lft(\ast) \end{eqnarray*}\] as needed. For the inductive step, suppose the implication holds for all $k$ for some $x$ and let $a \in A$. Suppose further that $\nleq(\length(\cons(a,x),k))$; we then have $k = \next(m)$ for some $m$, where $\nleq(\length(x),m)$. Now \[\begin{eqnarray*} & & \at(\cons(a,x),k) \\ & \hyp{k = \next(m)} = & \at(\cons(a,x),\next(m)) \\ & \href{/posts/arithmetic-made-difficult/At.html#thm-at-cons-next} = & \at(x,m) \\ & = & \lft(\ast) \end{eqnarray*}\] as needed.
We proceed by list induction on $x$. For the base case $x = \nil$, note that if $\nleq(k,\length(\nil))$ then $k = \zero$. Now \[\begin{eqnarray*} & & \at(\cons(a,\nil),\zero) \\ & \href{/posts/arithmetic-made-difficult/At.html#thm-at-cons-zero} = & \rgt(a) \end{eqnarray*}\] as needed. For the inductive step, suppose the implication holds for all $k$ and $a$ for some $x$ and let $b \in A$. Suppose further that $\nleq(k,\length(\cons(b,x)))$. We have two possibilities for $k$. If $k = \zero$, we have \[\begin{eqnarray*} & & \at(\cons(a,\cons(b,x)),\zero) \\ & \href{/posts/arithmetic-made-difficult/At.html#thm-at-cons-zero} = & \rgt(a) \end{eqnarray*}\] as needed. Suppose instead that $k = \next(m)$. Now $\nleq(m,\length(x))$, and we have \[\begin{eqnarray*} & & \at(\cons(a,\cons(b,x)),k) \\ & = & \at(\cons(a,\cons(b,x)),\next(m)) \\ & \href{/posts/arithmetic-made-difficult/At.html#thm-at-cons-next} = & \at(\cons(b,x),m) \\ & = & \rgt(c) \end{eqnarray*}\] for some $c$ by the inductive hypothesis, as needed.

_test_at_isleft :: (List t, Equal a, Equal (t a), Natural n, Equal n)
  => t a -> n -> Test (t a -> n -> Bool)
_test_at_isleft _ _ =
  testName "if leq(length(x),k) then isLft(at(x,k))" $
  \x k -> if leq (length x) k
    then isLft (at x k)
    else true


_test_at_isright :: (List t, Equal a, Equal (t a), Natural n, Equal n)
  => t a -> n -> Test (a -> t a -> n -> Bool)
_test_at_isright _ _ =
  testName "if leq(k,length(x)) then isRgt(at(cons(a,x),k))" $
  \a x k -> if leq k (length x)
    then isRgt (at (cons a x) k)
    else true

Finally, $\at$ detects equality for lists.

Let $A$ be a set, and let $x,y \in \lists{A}$. Then $x = y$ if and only if $\at(x,k) = \at(y,k)$ for all $k \in \nats$.

The “only if” direction is clear. We show the “if” part by list induction on $x$. For the base case $x = \nil$, suppose we have $\at(x,k) = \at(y,k)$ for all $k \in \nats$. If $y = \cons(a,z)$ for some $z$, then we have \[\begin{eqnarray*} & & \rgt(a) \\ & \href{/posts/arithmetic-made-difficult/At.html#thm-at-cons-zero} = & \at(\cons(a,z),\zero) \\ & = & \at(y,\zero) \\ & = & \at(x,\zero) \\ & = & \at(\nil,\zero) \\ & \href{/posts/arithmetic-made-difficult/At.html#thm-at-nil} = & \lft(\ast) \end{eqnarray*}\] a contradiction. So $y = \nil = x$ as claimed.

For the inductive step, suppose the implication holds for all $y$ for some $x$, let $a \in A$, and suppose we have $\at(\cons(a,x),k) = \at(y,k)$ for all $k \in \nats$. If $y = \nil$, then again we have \[\begin{eqnarray*} & & \rgt(a) \\ & = & \at(\cons(a,x),\next(\zero)) \\ & = & \at(y,\next(\zero)) \\ & = & \at(\nil,\next(\zero)) \\ & \href{/posts/arithmetic-made-difficult/At.html#thm-at-nil} = & \lft(\ast) \end{eqnarray*}\] a contradiction. Say $y = \cons(b,z)$. Now \[\begin{eqnarray*} & & \at(z,k) \\ & \href{/posts/arithmetic-made-difficult/At.html#thm-at-cons-next} = & \at(\cons(b,z),\next(k)) \\ & = & \at(y,\next(k)) \\ & = & \at(\cons(a,x),\next(k)) \\ & \href{/posts/arithmetic-made-difficult/At.html#thm-at-cons-next} = & \at(x,k) \end{eqnarray*}\] By the inductive hypothesis, $x = z$, so that $\cons(a,x) = y$ as needed.

_test_at_eq :: (List t, Equal a, Equal (t a), Natural n, Equal n)
  => t a -> n -> Test (t a -> t a -> n -> Bool)
_test_at_eq _ _ =
  testName "if eq(x,y) then eq(at(x,k),at(y,k))" $
  \x y k -> if eq x y
    then eq (at x k) (at y k)
    else true

Testing

Suite:

_test_at ::
  ( TypeName a, Show a, Equal a, Arbitrary a
  , TypeName n, Natural n, Equal n, Show n, Arbitrary n
  , TypeName (t a), List t, Equal (t a), Show (t a), Arbitrary (t a)
  ) => Int -> Int -> t a -> n -> IO ()
_test_at size cases t n = do
  testLabel2 "at" t n

  let args = testArgs size cases

  runTest args (_test_at_zero t n)
  runTest args (_test_at_next t n)
  runTest args (_test_at_next_next_cons t n)
  runTest args (_test_at_nil t n)
  runTest args (_test_at_single t n)
  runTest args (_test_at_double t n)
  runTest args (_test_at_length t n)
  runTest args (_test_at_next_length t n)
  runTest args (_test_at_snoc t n)
  runTest args (_test_at_snoc_length t n)
  runTest args (_test_at_rev t n)
  runTest args (_test_at_cat_left t n)
  runTest args (_test_at_cat_right t n)
  runTest args (_test_at_isleft t n)
  runTest args (_test_at_isright t n)
  runTest args (_test_at_eq t n)

Main:

main_at :: IO ()
main_at = do
  _test_at 20 100 (nil :: ConsList Bool)  (zero :: Unary)
  _test_at 20 100 (nil :: ConsList Unary) (zero :: Unary)