Structural induction on generic list

Question

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))

Answer 1

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.

Answer 2

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.