is-palindrome l <-> l = rev l

Palindromes.agda

{-# OPTIONS --safe #-}

open import Agda.Primitive
open import Agda.Builtin.Sigma
open import Agda.Builtin.Equality

variable
  ℓ : Level
  A : Set ℓ

-- Polymorphic versions to save "Lift"
record ⊤ {ℓ} : Set ℓ where
  constructor tt
data ⊥ {ℓ} : Set ℓ where

infixr 2 _×_
_×_ : ∀ {ℓ₁ ℓ₂} → Set ℓ₁ → Set ℓ₂ → Set (ℓ₁ ⊔ ℓ₂)
A × B = Σ A (λ _ → B)

infixr 6 _∙_
_∙_ : ∀ {x y z : A} → x ≡ y → y ≡ z → x ≡ z
refl ∙ p = p

-- Combinators stolen from the Agda stdlib
infix  3 _∎
infixr 2 _≡⟨⟩_ step-≡

_≡⟨⟩_ : ∀ (x {y} : A) → x ≡ y → x ≡ y
_ ≡⟨⟩ x≡y = x≡y

step-≡ : ∀ (x {y z} : A) → y ≡ z → x ≡ y → x ≡ z
step-≡ _ y≡z x≡y = x≡y ∙ y≡z

_∎ : ∀ (x : A) → x ≡ x
_∎ _ = refl

syntax step-≡ x y≡z x≡y = x ≡⟨  x≡y ⟩ y≡z

ap : ∀ {ℓ₁ ℓ₂} {A : Set ℓ₁} {B : Set ℓ₂} (f : A → B) {x y : A} → x ≡ y → f x ≡ f y
ap f refl = refl

infixr 4 !_

!_ : ∀ {x y : A} → x ≡ y → y ≡ x
!_ refl = refl

subst : ∀ {ℓ₁ ℓ₂} {A : Set ℓ₁} (B : A → Set ℓ₂) {x y : A} → x ≡ y → B x → B y
subst B refl bx = bx

module D where

  data List {ℓ} (A : Set ℓ) : Set ℓ where
    [] : List A
    [_] : A → List A
    _∷[_]∷_ : A → List A → A → List A

  rev : List A → List A
  rev [] = []
  rev [ x ] = [ x ]
  rev (x ∷[ l ]∷ y) = y ∷[ rev l ]∷ x

  _∷_ : A → List A → List A
  x ∷ [] = [ x ]
  x ∷ [ y ] = x ∷[ [] ]∷ y
  x ∷ (y ∷[ l ]∷ z) = x ∷[ y ∷ l ]∷ z
  infixr 5 _∷_

  _∷ʳ_ : List A → A → List A
  [] ∷ʳ x = [ x ]
  [ x ] ∷ʳ y = x ∷[ [] ]∷ y
  (x ∷[ l ]∷ y) ∷ʳ z = x ∷[ l ∷ʳ y ]∷ z
  infixr 6 _∷ʳ_

  data IsPal {ℓ} {A : Set ℓ} : List A → Set ℓ where
    []ᵖ : IsPal []
    [_]ᵖ : ∀ x → IsPal [ x ]
    _∷ᵖ_ : ∀ x {l} → IsPal l → IsPal (x ∷[ l ]∷ x)

  ∷ʳ-∷ : ∀ x (l : List A) y → (x ∷ l) ∷ʳ y ≡ x ∷[ l ]∷ y
  ∷ʳ-∷ x [] y = refl
  ∷ʳ-∷ x [ y ] z = refl
  ∷ʳ-∷ x (y ∷[ l ]∷ z) w = ap (x ∷[_]∷ w) (∷ʳ-∷ y l z)

  ∷-∷ʳ : ∀ x (l : List A) y → x ∷ l ∷ʳ y ≡ x ∷[ l ]∷ y
  ∷-∷ʳ x [] y = refl
  ∷-∷ʳ x [ y ] z = refl
  ∷-∷ʳ x (y ∷[ l ]∷ z) w = ap (x ∷[_]∷ w) (∷-∷ʳ y l z)

  rev-∷ : ∀ x (l : List A) → rev (x ∷ l) ≡ rev l ∷ʳ x
  rev-∷ x [] = refl
  rev-∷ x [ y ] = refl
  rev-∷ x (y ∷[ l ]∷ z) = ap (z ∷[_]∷ x) (rev-∷ y l)

  Code : ∀ {ℓ} {A : Set ℓ} (l₁ l₂ : List A) → Set ℓ
  Code [] [] = ⊤
  Code [ x₁ ] [ x₂ ] = x₁ ≡ x₂
  Code (x₁ ∷[ l₁ ]∷ y₁) (x₂ ∷[ l₂ ]∷ y₂) = (x₁ ≡ x₂) × (l₁ ≡ l₂) × (y₁ ≡ y₂)
  Code _ _ = ⊥

  encode : ∀ {l₁ l₂ : List A} → l₁ ≡ l₂ → Code l₁ l₂
  encode {l₁ = []} refl = tt
  encode {l₁ = [ _ ]} refl = refl
  encode {l₁ = _ ∷[ _ ]∷ _} refl = refl , refl , refl

  rev-pal : ∀ {l : List A} → l ≡ rev l → IsPal l
  rev-pal {l = []} _ = []ᵖ
  rev-pal {l = [ x ]} _ = [ x ]ᵖ
  rev-pal {l = x ∷[ l ]∷ y} p with encode p
  ... | x≡y , revl≡l , _ = subst (λ y → IsPal (x ∷[ l ]∷ y)) x≡y (x ∷ᵖ rev-pal revl≡l)

module L where

  open import Agda.Builtin.List

  [_] : A → List A
  [ x ] = x ∷ []

  _∷ʳ_ : List A → A → List A
  [] ∷ʳ x = [ x ]
  (x ∷ l) ∷ʳ y = x ∷ (l ∷ʳ y)
  infixl 6 _∷ʳ_

  _∷[_]∷_ : A → List A → A → List A
  x ∷[ l ]∷ y = x ∷ l ∷ʳ y

  rev : List A → List A
  rev [] = []
  rev (x ∷ l) = rev l ∷ʳ x

  data IsPal {ℓ} {A : Set ℓ} : List A → Set ℓ where
    []ᵖ : IsPal []
    [_]ᵖ : ∀ x → IsPal [ x ]
    _∷ᵖ_ : ∀ x {l} → IsPal l → IsPal (x ∷[ l ]∷ x)

  rev-∷ʳ : (l : List A) (x : A) → rev (l ∷ʳ x) ≡ x ∷ rev l
  rev-∷ʳ [] x = refl
  rev-∷ʳ (x ∷ l) y =
    rev (l ∷ʳ y) ∷ʳ x
      ≡⟨ ap (_∷ʳ x) (rev-∷ʳ l y) ⟩
    y ∷[ rev l ]∷ x
      ∎

  pal-rev : {l : List A} → IsPal l → l ≡ rev l
  pal-rev []ᵖ = refl
  pal-rev [ _ ]ᵖ = refl
  pal-rev (_∷ᵖ_ x {l} lip) =
    x ∷[ l ]∷ x
      ≡⟨ ap (x ∷[_]∷ x) (pal-rev lip) ⟩
    x ∷[ rev l ]∷ x
      ≡⟨⟩
    x ∷ rev (x ∷ l)
      ≡⟨ ! rev-∷ʳ (x ∷ l) x ⟩
    rev (x ∷[ l ]∷ x)
      ∎

  toDList : List A → D.List A
  toDList [] = D.[]
  toDList (x ∷ l) = x D.∷ toDList l

  toDList-∷ʳ : ∀ (l : List A) x → toDList (l ∷ʳ x) ≡ toDList l D.∷ʳ x
  toDList-∷ʳ [] x = refl
  toDList-∷ʳ (x ∷ l) y =
    x D.∷ toDList (l ∷ʳ y)
      ≡⟨ ap (x D.∷_) (toDList-∷ʳ l y) ⟩
    x D.∷ (toDList l D.∷ʳ y)
      ≡⟨ D.∷-∷ʳ x (toDList l) y ⟩
    x D.∷[ toDList l ]∷ y
      ≡⟨ ! D.∷ʳ-∷ x (toDList l) y ⟩
    (x D.∷ toDList l) D.∷ʳ y
      ∎

  toDList-rev : ∀ (l : List A) → toDList (rev l) ≡ D.rev (toDList l)
  toDList-rev [] = refl
  toDList-rev (x ∷ l) =
    toDList (rev l ∷ʳ x)
      ≡⟨ toDList-∷ʳ (rev l) x ⟩
    toDList (rev l) D.∷ʳ x
      ≡⟨ ap (D._∷ʳ x) (toDList-rev l) ⟩
    D.rev (toDList l) D.∷ʳ x
      ≡⟨ ! D.rev-∷ x (toDList l) ⟩
    D.rev (x D.∷ toDList l)
      ∎

  fromDList : D.List A → List A
  fromDList D.[] = []
  fromDList D.[ x ] = [ x ]
  fromDList (x D.∷[ l ]∷ y) = x ∷[ fromDList l ]∷ y

  fromDList-∷ : ∀ x (l : D.List A) → fromDList (x D.∷ l) ≡ x ∷ fromDList l
  fromDList-∷ x D.[] = refl
  fromDList-∷ x D.[ y ] = refl
  fromDList-∷ x (y D.∷[ l ]∷ z) =
    fromDList (x D.∷ (y D.∷[ l ]∷ z))
      ≡⟨⟩
    fromDList (x D.∷[ y D.∷ l ]∷ z)
      ≡⟨⟩
    x ∷[ fromDList (y D.∷ l) ]∷ z
      ≡⟨ ap (x ∷[_]∷ z) (fromDList-∷ y l) ⟩
    x ∷[ y ∷ fromDList l ]∷ z
      ≡⟨⟩
    x ∷ y ∷[ fromDList l ]∷ z
      ≡⟨⟩
    x ∷ fromDList (y D.∷[ l ]∷ z)
      ∎

  fromDList-toDList : ∀ (l : List A) → fromDList (toDList l) ≡ l
  fromDList-toDList [] = refl
  fromDList-toDList (x ∷ l) =
    fromDList (x D.∷ toDList l)
      ≡⟨ fromDList-∷ x (toDList l) ⟩
    x ∷ fromDList (toDList l)
      ≡⟨ ap (x ∷_) (fromDList-toDList l) ⟩
    x ∷ l
      ∎

  fromDIsPal : ∀ {l : D.List A} → D.IsPal l → IsPal (fromDList l)
  fromDIsPal D.[]ᵖ = []ᵖ
  fromDIsPal D.[ x ]ᵖ = [ x ]ᵖ
  fromDIsPal (x D.∷ᵖ lip) = x ∷ᵖ fromDIsPal lip

  rev-pal : {l : List A} → l ≡ rev l → IsPal l
  rev-pal {l = l} p = subst IsPal (fromDList-toDList l) (fromDIsPal (D.rev-pal (ap toDList p ∙ toDList-rev l)))

  toDList-fromDList : ∀ (l : D.List A) → toDList (fromDList l) ≡ l
  toDList-fromDList D.[] = refl
  toDList-fromDList D.[ x ] = refl
  toDList-fromDList (x D.∷[ l ]∷ y) =
    toDList (x ∷[ fromDList l ]∷ y)
      ≡⟨⟩
    x D.∷ toDList (fromDList l ∷ʳ y)
      ≡⟨ ap (x D.∷_) (toDList-∷ʳ (fromDList l) y) ⟩
    x D.∷ toDList (fromDList l) D.∷ʳ y
      ≡⟨ D.∷-∷ʳ x (toDList (fromDList l)) y ⟩
    x D.∷[ toDList (fromDList l) ]∷ y
      ≡⟨ ap (x D.∷[_]∷ y) (toDList-fromDList l) ⟩
    x D.∷[ l ]∷ y
      ∎