Also see Lists for newer material
.

This section presents a few
basic objects from list theory and array theory.
We start with the idea of a * discrete* type,
which is a type for which equality is decidable. Discreteness is
required for the element comparisons that are needed,
for example, in searching a list
for a given element.
Also, we need the idea that a proposition is
* decidable* , i.e., that it is either true or false.

discrete(<T:type>) == all x,y:<T>. (x=y in <T>) | ~(x=y in <T>)

< P: T->prop > is decidable on <T:type> == all x:<T>. P(x) | ~P(x)Figure gives two versions of the list

The definition of the * tail* function is straightforward.

tl(<l:list>) == list_ind( <l>; nil; h,t,v. t )Given a function of the appropriate type, the first theorem (named ``

**Figure:** Defining the Sum of a List of Integers

The definition of the membership predicate for lists uses a recursive proposition .

<e:element> on <l:list> over <T:type> == list_ind( <l>; void; h,t,v. (<e>=h in <T>) | v )

>> all A:U1. all x:A. all l:A list. (x on L over A) in U1The above type of use of

this type (proposition) is inhabited (true) exactly when one of the is true.

The following is another example of a recursively defined proposition;
it defines a predicate over lists of a certain type which is true
of list **l** exactly when **l** has no repeated elements.

<l:list> is nonrepetitious over <T:type> == list_ind( <l>; one; h,t,v. ~(h on t over <T>) and v )Given this definition, the following theorems are provable.

>> all A:U1. nil is nonrepetitious over A

>> all A:U1. all x:A. all l:A list. ~(x on l over A) & l is nonrepetitious over A => x.l is nonrepetitious over A

The next theorem defines a function which searches an array for the first occurrence of an element with a given property. (Arrays are taken to be functions on segments of the integers.)

search: >> all A:U1. all n:int. all f:{1,...,n}->A. all P:A->prop. P is decidable on A => all k:int. 1<=k<=n => all x:{1,...,k}. ~P(f(x)) | some x:{1,...,k}. P(f(x)) & all y:{1,...,x-1}. ~P(f(y))

Thu Sep 14 08:45:18 EDT 1995