# Structural induction on generic list

In preparation for an exam, I've come upon the following problem. Given the constructors :

[]: -> T LIST

[a]:T-> T LIST

cons(a,x) : T x T LIST -> T LIST ( a is added to the beginning of the list)


And the functions :

size(l) : T LIST -> N (number of elements in l)

reverse(l): T LIST -> T LIST ( reverses the order ofthe elements in the list)

unique(l) : T LIST -> T LIST - returns a list of the elements in 'l' that only appear once

repeated(l) : T LIST -> T LIST - returns a list of the elements in 'l' that appear more than once

max?(e,l) : T x T LIST -> Bool - returns true if 'e' is the maximum element in the list, false otherwise


Prove by structural induction that :

max?(e, l) -> max?(e, unique(reverse(l))) || max?(e, repeated(reverse(l)))


I've managed to simplify this to :

max?(e, l) -> max?(e, unique(l)) || max?(e, repeated(l))


But I don't see how to proceed towards proving what is asked...

Used definitions of functions:

    unique([]) = []
unique([e]) = [e]
unique(cons(e, L)) = cons(e, unique(L)), if member(e, L) = false unique(cons(e, L)) = unique(L), if member(e, L) = true

repeated([]) = []
repeated([e]) = [e]
repeated(cons(e, L)) = cons(e, repeated(L)), if member(e, L) = true unique(cons(e, L)) = unique(L), if member(e, L) = false

reverse([]) = []
reverse([e]) = [e]
reverse(cons(e, L)) = append(reverse(L), [e])

also,
member : Element x List -> Bool
member(e, []) = false
member(e, [a]) = (e == a) (true, if a is equal to e; false, if a isn't equal to e)
member(e, cons(a, L)) = (e == a) V member(e, L) (V is logical disjunction)

append : List x List -> List
append([], L) = L
append([e], L) = cons(e, L)
append(cons(e, L1), L2) = cons(e, append(L1, L2))

• Did the problem give a recursive definition for size and the other functions? It's weird to ask for a syntactic proof without syntactic definitions. – Gilles 'SO- stop being evil' Feb 7 '16 at 18:54
• Check your definition of 'repeated' -- the second case in given for 'unique'. Also it seems redundant to give special versions for lists of length one for all those functions. And you didn't give the definition of 'max?'. – Anton Trunov Feb 9 '16 at 14:48

Note: I mixed up boolean functions and propositions in what follows for brevity, and I hope it'll not cause any confusion.

I assume you have defined the function $\max?$ something like this:

max?(e, l) = ge_all?(e, l) && member(e, l),


where

ge_all?(e, []) = True
ge_all?(e, cons(x,xs)) = e >= x && ge_all? e xs.


You will need a bunch of lemmas [they can be proved using structural induction]:

Lemma 1: $\text{member}(e, l) \implies \text{member}(e, \text{unique}(l)) \vee \text{member}(e, \text{repeated}(l))$ [this one is suggested by @Alexander]. Its proof is pretty boring because of lots of subcases.

Lemma 2: $\text{ge_all?}(e, l) \implies \text{ge_all?}(e, \text{unique}(l))$.

Lemma 3: $\text{ge_all?}(e, l) \implies \text{ge_all?}(e, \text{repeated}(l))$.

Theorem: $\max?(e,l) \implies \max?(e, \text{unique}(l)) \vee \max?(e, \text{repeated}(l))$.

Proof sketch:

$\max?(e, l)$ implies $\text{member}(e,l)$, which in its turn implies $\text{member}(e, \text{unique}(l)) \vee \text{member}(e, \text{repeated}(l))$ [by lemma 1]. So we consider two cases: (1) $\text{member}(e,\text{unique}(l))$ and (2) $\text{member}(e,\text{repeated}(l))$.

In the case (1) we can prove $\text{max?}(e,\text{unique}(l))$ like this: $\max?(e, l)$ implies by definition $\text{ge_all?}(e,l)$, which [by lemma 2] implies $\text{ge_all?}(e,\text{unique}(l))$. Since $\text{ge_all?}(e,\text{unique}(l))$ and $\text{member}(e,\text{unique}(l))$ we get $\text{max?}(e,\text{unique}(l))$.

The case (2) is similar. End of proof.

• @user43389 So we have the big picture here, if you have any problems with some particular lemma feel free to ask a new question. – Anton Trunov Feb 10 '16 at 11:59

Probably you can show that

member (e, l) = member (e, unique (l)) || member (e, repeated (l))


Then maximum element it's either among unique elements or among repeated.