software foundations Prop.v [palindrome_converse] in Agda2

• リスト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)