Stream: Is there code for X?

Topic: list.is_palindrome

Chris Wong (Apr 19 2020 at 00:00):

Is there an is_palindrome : {...} -> l = reverse l somewhere in mathlib?

My use case is proving a property of Fibonacci words. Namely: every Fibonacci word is either p01 or p10 where p is a palindrome.

Mario Carneiro (Apr 19 2020 at 00:02):

No, but reverse l = l seems pretty clear

Chris Wong (Apr 19 2020 at 00:09):

That's fair. I wonder if there'd be demand for an induction principle on palindromes, as I'll probably write that at some point. Or is that too obscure?

Kevin Buzzard (Apr 19 2020 at 00:11):

That sounds like a funky codewars project :-)

Kevin Buzzard (Apr 19 2020 at 00:11):

The word palindrome doesn't seem to appear in mathlib at all.

Scott Morrison (Apr 19 2020 at 00:11):

Perhaps in and of itself, it's too obscure. But if you need it for something else, so one will object. We're doing maths here, the standards for "obscure" are pretty generous. :-)

Last updated: May 07 2021 at 22:14 UTC