1
$\begingroup$

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))
$\endgroup$
  • 1
    $\begingroup$ 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. $\endgroup$ – Gilles Feb 7 '16 at 18:54
  • $\begingroup$ 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?'. $\endgroup$ – Anton Trunov Feb 9 '16 at 14:48
1
$\begingroup$

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.

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

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.