Structural induction over list

Question

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

also,
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.

Answer 1

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].