On palindromes

Défine the inductive predicate palindrome associated to lists that can be read the same way in both directions.

Solution

Look at this file .

Note

We added to the end of this file a proof that a list is palindromic (according to the inductive definition) if and only if it is equal to its own reverse (defined by the function rev in PolyList).

This proof is quite interesting, because we needed to build some tools to achieve it :