I want to prove that unique(reverse(L)) = reverse(unique(L)) where L is a List.

List has the following constructors:
[] : -> List
[e] : Element -> List
cons(e, L) : Element x List -> List

I defined unique and reverse as follows:
unique : List -> List
reverse : List -> List

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

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

member : Element x List -> {true, false}
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))

Both base cases are easy to verify.

Induction hypothesis: I assume unique(reverse(L)) = reverse(unique(L)) is true

Inductive step: I have to prove that unique(reverse(cons(e, L))) = reverse(unique(cons(e, L))) is true

I consider two cases:

  1. member(e, L) = true, then:

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

    reverse(unique(cons(e, L))) = reverse(unique(L)) = unique(reverse(L))

    Those are obviously true, but I don't know how to formally prove it (I can explain it in words, but that's not the point).

  2. member(e, L) = false, then:

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

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

    I'm stucked here.

unique, reverse, append and member don't have to be defined that way, but they have to do the same thing.


I am not entirely sure that what you're trying to prove is right.

unique [] = []
unique (x : xs) = if x `in` xs then unique xs else x : unique xs

reverse [] = []
reverse (x : xs) = reverse xs ++ [x]

If we take xs = [a, b, a, c] then:

unique [a, b, a, c]
= { unique.2 }
if a `in` [b, a, c] then unique [b, a, c] else a : unique [b, a, c]
= { ... }
[b, a, c]

reverse [b, a, c] = [c, a, b]

reverse [a, b, a, c] = [c, a, b, a]

unique [c, a, b, a]
= { unique.2 }
c : unique [a, b, a]
= { unique . 2 }
c : [b, a]
= [c, b, a]

Hence, unique (reverse [a, b, a, c]) = [c, b, a] and reverse (unique [a, b, a, c]) = [c, a, b].


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.