A programming puzzle

Stream: mathlib4

[Jeremy Tan]

Since Lean is a functional programming language, certain so-called functional pearls can be implemented in it. The following is one such pearl, which checks whether a list is a palindrome. Your task is to prove the sorried lemma.

import Mathlib.Data.List.Palindrome

variable {α : Type*}

def transfer : List α × List α → List α × List α
  | ([], a) => ([], a)
  | (a :: l, b) => (l, a :: b)

def halve (l : List α) : (List α × List α) × Bool :=
  l.foldl (fun (p, b) _ ↦ (bif b then transfer p else p, !b)) ((l, []), false)

def check (l : List α) : Prop :=
  let ⟨⟨h₁, h₂⟩, b⟩ := halve l
  (bif b then h₁.tail else h₁) = h₂

theorem check_eq {l : List α} : check l ↔ l.Palindrome := by
  sorry

:slight_smile: (I don't intend to add this to mathlib or anywhere else, this puzzle stands on its own)