- リストxsを要素数に応じて分割する
- 要素数が偶数のとき: xs = ys ++ zs (※ length ys = length zs)
- 奇数個のとき: xs = ys ++ [ x ] ++ zs (※ length ys = length zs)
- どちらの場合でも∃ zs ∈ pal. xs = ys ++ zs ++ reverse ysの形に変形できる
- ys ++ reverse ysと∀ x. ys ++ [ x ] ++ reverse ysは回文になる
以上よりリストを反転したものが元と等しい場合は回文であることが証明できる
palindrome.agda
module palindrome where
open import Data.List
import Relation.Binary.PropositionalEquality as Eq
open Eq hiding ([_] ; setoid)
import Data.List.Properties as ListProps
open import Relation.Binary
open import Data.Product
open import Data.Sum
open import Algebra
import list as ListProps'
data IsPalindrome {ℓ} {A : Set ℓ} : List A → Set ℓ where
[]-pal : IsPalindrome []
[_]-pal : ∀ x → IsPalindrome [ x ]
pal-step : ∀ x {xs} → IsPalindrome xs → IsPalindrome (x ∷ xs ∷ʳ x)
module Helper {ℓ}{A : Set ℓ} where
open ≡-Reasoning
open ListProps' A public
.pal-[]-rev : ∀ (xs : List A) → IsPalindrome (xs ++ reverse xs)
pal-[]-rev [] = []-pal
pal-[]-rev (x ∷ xs) = subst IsPalindrome (sym h) (pal-step x (pal-[]-rev xs))
where h : (x ∷ xs) ++ reverse (x ∷ xs) ≡ x ∷ (xs ++ reverse xs) ∷ʳ x
h = begin
(x ∷ xs) ++ reverse (x ∷ xs)
≡⟨ cong (λ z → x ∷ xs ++ z) (ListProps.unfold-reverse x xs) ⟩
x ∷ (xs ++ (reverse xs ∷ʳ x))
≡⟨ cong (_∷_ x) (sym (App.assoc xs (reverse xs) [ x ])) ⟩
x ∷ (xs ++ reverse xs) ++ [ x ] ∎
.pal-[_]-rev : ∀ (y : A) xs → IsPalindrome (xs ++ [ y ] ++ reverse xs)
pal-[_]-rev y [] = [ y ]-pal
pal-[_]-rev y (x ∷ xs) = subst IsPalindrome (sym h) (pal-step x (pal-[ y ]-rev xs))
where h : (x ∷ xs) ++ (y ∷ []) ++ reverse (x ∷ xs) ≡
x ∷ (xs ++ [ y ] ++ reverse xs) ∷ʳ x
h = begin
(x ∷ xs) ++ [ y ] ++ reverse (x ∷ xs)
≡⟨ cong (λ z → (x ∷ xs) ++ [ y ] ++ z) (ListProps.unfold-reverse x xs) ⟩
x ∷ xs ++ [ y ] ++ (reverse xs ++ [ x ])
≡⟨ cong (_∷_ x) (begin
xs ++ [ y ] ++ (reverse xs ++ [ x ])
≡⟨ cong (_++_ xs) (sym (App.assoc [ y ] (reverse xs) [ x ])) ⟩
xs ++ ([ y ] ++ reverse xs ++ [ x ])
≡⟨ sym (App.assoc xs (y ∷ reverse xs) [ x ]) ⟩
(xs ++ [ y ] ++ reverse xs) ∷ʳ x
∎) ⟩
x ∷ (xs ++ [ y ] ++ reverse xs) ∷ʳ x ∎
module Properties {ℓ} {A : Set ℓ} where
open ≡-Reasoning
open Helper {A = A}
.reverse-++-lem : ∀ (y : A) ys zs →
reverse (ys ++ [ y ] ++ zs) ≡ reverse zs ++ [ y ] ++ reverse ys
reverse-++-lem y ys zs = begin
reverse (ys ++ [ y ] ++ zs)
≡⟨ ListProps.reverse-++-commute ys (y ∷ zs) ⟩
reverse ([ y ] ++ zs) ++ reverse ys
≡⟨ cong (λ z → z ++ reverse ys) (ListProps.reverse-++-commute [ y ] zs) ⟩
(reverse zs ++ [ y ]) ++ reverse ys
≡⟨ App.assoc (reverse zs) [ y ] (reverse ys) ⟩
reverse zs ++ [ y ] ++ reverse ys
∎
-- palindrome_converse
.reverse-id-pal : ∀ (xs : List A) → xs ≡ reverse xs → IsPalindrome xs
reverse-id-pal xs with split xs
... | inj₁ (y , ys , zs , hlen , heq) rewrite heq = λ h →
let h1 = begin
ys ++ [ y ] ++ zs ≡⟨ h ⟩
reverse (ys ++ [ y ] ++ zs) ≡⟨ reverse-++-lem y ys zs ⟩
reverse zs ++ [ y ] ++ reverse ys
∎
hlen' : SameLength ys (reverse zs)
hlen' = SL.trans hlen (reverse-SameLen zs)
h2 = ++-SameLen-injectiveʳ hlen' h1
h2' : [ y ] SL.≈ [ y ]
h2' = ListProps'.∷-samelen ListProps'.[]-samelen
h3 : zs ≡ reverse ys
h3 = ++-SameLen-injectiveʳ h2' h2
in subst (λ z → IsPalindrome (ys ++ [ y ] ++ z)) (sym h3) (pal-[ y ]-rev ys)
... | inj₂ (ys , zs , hlen , heq) rewrite heq = λ h →
let h1 : ys ++ zs ≡ reverse zs ++ reverse ys
h1 = trans h (ListProps.reverse-++-commute ys zs)
h2 : ys SL.≈ reverse zs
h2 = SL.trans hlen (reverse-SameLen zs)
in subst (λ z → IsPalindrome (ys ++ z))
(sym (++-SameLen-injectiveʳ h2 h1)) (pal-[]-rev ys)
list.agda
open import Level
module list {o} (A : Set o) where
open import Data.List
open import Data.List.Properties
open import Relation.Binary.PropositionalEquality hiding (setoid ; [_])
open import Relation.Binary
open import Algebra
open import Data.Product
open import Data.Sum
data SameLength : Rel (List A) o where
[]-samelen : SameLength [] []
∷-samelen : ∀ {xs ys} → SameLength xs ys → ∀ {x y} → SameLength (x ∷ xs) (y ∷ ys)
setoid : Setoid o o
setoid = record { Carrier = List A; _≈_ = SameLength; isEquivalence = record {
refl = refl'; sym = sym'; trans = trans' }
}
where refl' : {x : List A} → SameLength x x
refl' {[]} = []-samelen
refl' {x ∷ x₁} = ∷-samelen refl'
sym' : {i j : List A} → SameLength i j → SameLength j i
sym' []-samelen = []-samelen
sym' (∷-samelen h) = ∷-samelen (sym' h)
trans' : {i j k : List A} → SameLength i j → SameLength j k → SameLength i k
trans' []-samelen i = i
trans' (∷-samelen h) (∷-samelen i) = ∷-samelen (trans' h i)
module SL = Setoid setoid
module App = Monoid (monoid A)
∷-∷ʳ-SameLen : ∀ {x y} xs → SameLength (x ∷ xs) (xs ∷ʳ y)
∷-∷ʳ-SameLen {x} {y} [] = ∷-samelen []-samelen
∷-∷ʳ-SameLen {x} {y} (z ∷ zs) = ∷-samelen (∷-∷ʳ-SameLen zs)
reverse-SameLen : ∀ xs → SameLength xs (reverse xs)
reverse-SameLen [] = []-samelen
reverse-SameLen (x ∷ xs) = (subst (λ z → SameLength (x ∷ xs) z)
(sym (unfold-reverse x xs))
(SL.trans (∷-samelen (reverse-SameLen xs) {y = x})
(∷-∷ʳ-SameLen (reverse xs))))
++-SameLen-injectiveˡ : ∀ {xs ys zs ws} → xs SL.≈ zs → xs ++ ys ≡ zs ++ ws → xs ≡ zs
++-SameLen-injectiveˡ []-samelen h = refl
++-SameLen-injectiveˡ (∷-samelen sl) h with ∷-injective h
... | (h1 , h2) = cong₂ _∷_ h1 (++-SameLen-injectiveˡ sl h2)
++-SameLen-injectiveʳ : ∀ {xs ys zs ws} → xs SL.≈ zs → xs ++ ys ≡ zs ++ ws → ys ≡ ws
++-SameLen-injectiveʳ []-samelen h = h
++-SameLen-injectiveʳ (∷-samelen hlen) h = ++-SameLen-injectiveʳ hlen (proj₂ (∷-injective h))
open ≡-Reasoning
∷-inv : ∀ (xs : List A) → ∃₂ (λ y ys → xs ≡ y ∷ ys) ⊎ xs ≡ []
∷-inv [] = inj₂ refl
∷-inv (x ∷ xs) = inj₁ (x , xs , refl)
init-last : ∀ (xs : List A) → ∃₂ (λ ys y → xs ≡ ys ∷ʳ y) ⊎ xs ≡ []
init-last [] = inj₂ refl
init-last (x ∷ xs) with init-last xs
... | inj₁ (zs , z , h) = inj₁ (x ∷ zs , z , cong (_∷_ x) h)
... | inj₂ h = inj₁ ([] , x , cong (_∷_ x) h)
split : ∀ (xs : List A) →
∃ (λ y → ∃₂ (λ (ys zs : List A) →
SameLength ys zs × xs ≡ ys ++ [ y ] ++ zs)) ⊎
∃₂ (λ (ys zs : List A) → SameLength ys zs × xs ≡ ys ++ zs)
split [] = inj₂ ([] , [] , []-samelen , refl)
split (x ∷ xs) with split xs
... | inj₁ (y , ys , zs , hlen , heq) = inj₂ (x ∷ ys , y ∷ zs , ∷-samelen hlen , cong (_∷_ x) heq)
... | inj₂ (ys , zs , hlen , heq) with init-last ys
... | inj₁ (vs , v , h) = inj₁ (v , x ∷ vs , zs ,
SL.trans (∷-∷ʳ-SameLen _) (subst (λ a → SameLength a zs) h hlen) ,
cong (_∷_ x) (trans heq (trans (cong (λ a → a ++ zs) h) (Monoid.assoc (monoid A) vs [ v ] zs))))
... | inj₂ h with subst (λ a → SameLength a zs) h hlen | hlen | heq
split (x ∷ .[]) | inj₂ (.[] , .[] , hlen , heq) | inj₂ h | []-samelen | []-samelen | refl =
inj₁ (x , [] , [] , []-samelen , refl)
++[] : ∀ (xs : List A) → xs ++ [] ≡ xs
++[] [] = refl
++[] (x ∷ xs) = cong (_∷_ x) (++[] xs)