--- title: At author: nbloomf date: 2017-04-28 tags: arithmetic-made-difficult, literate-haskell slug: at --- > {-# 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. :::::: definition :: 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. :::::: corollary ::: []{#cor-at-zero}[]{#cor-at-next} $\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 ::::::::::: > _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$. :::::: theorem ::::: []{#thm-at-cons-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).$$ ::: proof :::::::::: Note that $$\begin{eqnarray*} & & \at(\cons(a,x),\next(k)) \\ & \href{@at@#cor-at-next} = & \bif{\isnil(\cons(a,x))}{\lft(\ast)}{\at(\tail(\cons(a,x)),k)} \\ & \href{@head-tail@#thm-isnil-cons} = & \bif{\bfalse}{\lft(\ast)}{\at(\tail(\cons(a,x)),k)} \\ & \href{@booleans@#cor-if-false} = & \at(\tail(\cons(a,x)),k) \\ & \href{@head-tail@#thm-tail-cons} = & \at(x,k) \end{eqnarray*}$$ as claimed. :::::::::::::::::::: ::: test ::::::::::: > _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. :::::: theorem ::::: []{#thm-at-nil}[]{#thm-at-cons-zero}[]{#thm-at-doubleton-one} Let$A$be a set. The following hold for all$a,b \in A$,$x \in \lists{A}$, and$k \in \nats$. 1.$\at(\nil,k) = \lft(\ast)$. 2.$\at(\cons(a,x),\zero) = \rgt(a)$. 3.$\at(\cons(a,\cons(b,x)),\next(\zero)) = \rgt(b)$. ::: proof :::::::::: 1. We consider two cases:$k = \zero$and$k \neq \zero$. If$k = \zero$, we of course have $$\begin{eqnarray*} & & \at(\nil,\zero) \\ & \href{@at@#thm-at-nil} = & \lft(\ast) \end{eqnarray*}$$ as claimed. If$k = \next(m)$, we have $$\begin{eqnarray*} & & \at(\nil,\next(m)) \\ & \href{@at@#cor-at-next} = & \bif{\isnil(\nil)}{\lft(\ast)}{\at(\tail(\nil),m)} \\ & \href{@head-tail@#thm-isnil-nil} = & \bif{\btrue}{\lft(\ast)}{\at(\tail(\nil),m)} \\ & \href{@booleans@#cor-if-true} = & \lft(\ast) \end{eqnarray*}$$ as claimed. 2. We have $$\begin{eqnarray*} & & \at(\cons(a,x),\zero) \\ & \href{@at@#cor-at-zero} = & \head(\cons(a,x)) \\ & \href{@head-tail@#thm-head-cons} = & \rgt(a) \end{eqnarray*}$$ as claimed. 3. We have $$\begin{eqnarray*} & & \at(\cons(a,\cons(b,x)),\next(\zero)) \\ & \href{@at@#thm-at-cons-next} = & \at(\cons(b,x),\zero) \\ & \href{@at@#thm-at-cons-zero} = & \rgt(b) \end{eqnarray*}$$ as claimed. :::::::::::::::::::: ::: test ::::::::::: > _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$. :::::: theorem ::::: []{#thm-at-cons-length}[]{#thm-at-length} Let $A$ be a set and let $z \in \lists{A}$. 1. $\at(\cons(a,x),\length(x)) = \head(\rev(\cons(a,x)))$. 2. $\at(x,\length(x)) = \lft(\ast)$. ::: proof :::::::::: 1. We proceed by list induction on $x$. For the base case $x = \nil$, we have $$\begin{eqnarray*} & & \at(\cons(a,\nil),\length(\nil)) \\ & \href{@length@#cor-length-nil} = & \at(\cons(a,\nil),\zero) \\ & = & \rgt(a) \\ & \href{@head-tail@#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{@length@#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{@rev@#cor-rev-cons} = & \head(\rev(\cons(a,\cons(b,x)))) \end{eqnarray*}$$ as needed. 2. We proceed by list induction on $x$. For the base case $x = \nil$, we have $$\begin{eqnarray*} & & \at(\nil,\length(\nil)) \\ & \href{@at@#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{@length@#cor-length-cons} = & \at(\cons(a,x),\next(\length(x))) \\ & = & \at(x,\length(x)) \\ & \href{@at@#thm-at-length} = & \lft(\ast) \end{eqnarray*}$$ as needed. :::::::::::::::::::: ::: test ::::::::::: > _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$. :::::: theorem ::::: []{#thm-at-snoc-cons}[]{#thm-at-snoc-length} Let $A$ be a set. Let $a,b \in A$ and $x \in \lists{A}$. 1. If $\nleq(k,\length(x))$ then $\at(\snoc(a,\cons(b,x)),k) = \at(\cons(b,x),k)$. 2. $\at(\snoc(a,x),\length(x)) = \rgt(a)$. ::: proof :::::::::: 1. 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{@snoc@#cor-snoc-cons} = & \at(\cons(b,\snoc(a,x)),\zero) \\ & \href{@at@#thm-at-cons-zero} = & \rgt(b) \\ & \href{@at@#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{@snoc@#cor-snoc-cons} = & \at(\cons(b,\snoc(a,x)),\next(k)) \\ & \href{@at@#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{@at@#thm-at-cons-next} = & \at(\cons(b,x),\next(k)) \end{eqnarray*}$$ as needed. 2. We proceed by list induction on $x$. For the base case $x = \nil$, we have $$\begin{eqnarray*} & & \at(\snoc(a,\nil),\length(\nil)) \\ & \href{@length@#cor-length-nil} = & \at(\snoc(a,\nil),\zero) \\ & \href{@snoc@#cor-snoc-nil} = & \at(\cons(a,\nil),\zero) \\ & \href{@at@#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{@snoc@#cor-snoc-cons} = & \at(\cons(b,\snoc(a,x)),\length(\cons(b,x))) \\ & \href{@length@#cor-length-cons} = & \at(\cons(b,\snoc(a,x)),\next(\length(x))) \\ & \href{@at@#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 ::::::::::: > _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$. :::::: theorem ::::: 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).$$ ::: proof :::::::::: 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{@at@#thm-at-cons-zero} = & \rgt(a) \\ & \href{@at@#thm-at-snoc-length} = & \at(\snoc(a,\rev(x)),\length(\rev(x))) \\ & \href{@length@#thm-length-rev} = & \at(\snoc(a,\rev(x)),\length(x)) \\ & \href{@rev@#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{@at@#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{@rev@#cor-rev-cons} = & \at(\rev(\cons(a,x)),v) \end{eqnarray*}$$ as needed. :::::::::::::::::::: ::: test ::::::::::: > _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$. :::::: theorem ::::: Let$A$be a set. For all$a \in A$,$x,y \in \lists{A}$and$k \in \nats$, we have the following. 1. If$\nleq(k,\length(x))$, then$\at(\cat(\cons(a,x),y),k) = \at(\cons(a,x),k)$. 2. If$\at(\cat(\cons(a,x),y),\nplus(\next(\length(x)),k)) = \at(y,k)$. ::: proof :::::::::: 1. 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{@cat@#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{@cat@#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. 2. 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{@at@#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{@snoc@#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 ::::::::::: > _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$. :::::: theorem ::::: Let $A$ be a set. For all $x \in \lists{A}$ and $k \in \nats$ we have the following. 1. If $\nleq(\length(x),k)$, then $\at(x,k) = \lft(\ast)$. 2. If $\nleq(k,\length(x))$, then $\at(\cons(a,x),k) = \rgt(b)$ for some $b \in A$. ::: proof :::::::::: 1. 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{@at@#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{@at@#thm-at-cons-next} = & \at(x,m) \\ & = & \lft(\ast) \end{eqnarray*}$$ as needed. 2. 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{@at@#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{@at@#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{@at@#thm-at-cons-next} = & \at(\cons(b,x),m) \\ & = & \rgt(c) \end{eqnarray*}$$ for some $c$ by the inductive hypothesis, as needed. :::::::::::::::::::: ::: test ::::::::::: > _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. :::::: theorem ::::: 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$. ::: proof :::::::::: 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{@at@#thm-at-cons-zero} = & \at(\cons(a,z),\zero) \\ & = & \at(y,\zero) \\ & = & \at(x,\zero) \\ & = & \at(\nil,\zero) \\ & \href{@at@#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{@at@#thm-at-nil} = & \lft(\ast) \end{eqnarray*}$$ a contradiction. Say $y = \cons(b,z)$. Now $$\begin{eqnarray*} & & \at(z,k) \\ & \href{@at@#thm-at-cons-next} = & \at(\cons(b,z),\next(k)) \\ & = & \at(y,\next(k)) \\ & = & \at(\cons(a,x),\next(k)) \\ & \href{@at@#thm-at-cons-next} = & \at(x,k) \end{eqnarray*}$$ By the inductive hypothesis, $x = z$, so that $\cons(a,x) = y$ as needed. :::::::::::::::::::: ::: test ::::::::::: > _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)