I want to prove that unique(reverse(L)) = reverse(unique(L)) where L is a List.List has the following constructors:[] : -> List[e] : Element -> Listcons(e, L) : Element x List -> ListI defined unique and reverse as follows:unique : List -> Listreverse : List -> Listunique([]) = []unique([e]) = [e]unique(cons(e, L)) = cons(e, unique(L)), if member(e, L) = falseunique(cons(e, L)) = unique(L), if member(e, L) = truereverse([]) = []reverse([e]) = [e]reverse(cons(e, L)) = append(reverse(L), [e])also,member : Element x List -> {true, false}member(e, []) = falsemember(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 -> Listappend([], L) = Lappend([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 trueInductive step: I have to prove that unique(reverse(cons(e, L))) = reverse(unique(cons(e, L))) is trueI consider two cases: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).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.
Structural induction over list
discrete mathematics;induction;lists
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 xsreverse [] = []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].