Skip to content

Instantly share code, notes, and snippets.

@banacorn
Last active October 13, 2015 16:24
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
Star You must be signed in to star a gist
Save banacorn/81d62806d1e6b16da123 to your computer and use it in GitHub Desktop.
open import Data.Char
open import Data.List
open import Function using (flip; _$_)
open import Relation.Nullary.Core
open import Relation.Nullary.Negation
open import Relation.Binary.PropositionalEquality renaming ([_] to [_]ev)
open ≡-Reasoning
data Pal : List Char Set where
nil : Pal []
sing : (c : Char) Pal [ c ]
cons : (s : List Char) (c : Char) Pal s Pal ([ c ] ++ s ++ [ c ])
-- examples
o : Pal [ 'o' ]
o = sing 'o'
lol : Pal ('l''o''l' ∷ [])
lol = cons ('o' ∷ []) 'l' (sing 'o')
*lol* : Pal ('*''l''o''l''*' ∷ [])
*lol* = cons ('l''o''l' ∷ []) '*'
(cons ('o' ∷ []) 'l' (sing 'o'))
-- lemmata
++-right-identity : {a} {A : Set a} (s : List A) s ++ [] ≡ s
++-right-identity [] = refl
++-right-identity (x ∷ xs) = cong (_∷_ x) (++-right-identity xs)
++-assoc : {a} {A : Set a}
(xs ys zs : List A)
xs ++ ys ++ zs ≡ (xs ++ ys) ++ zs
++-assoc [] ys zs = refl
++-assoc (x ∷ xs) ys zs = cong (_∷_ x) (++-assoc xs ys zs)
unfold-reverse : {a} {A : Set a}
(xs ys : List A)
foldl (flip _∷_) xs ys ≡ reverse ys ++ xs
unfold-reverse xs [] = refl
unfold-reverse xs (y ∷ ys) =
begin
foldl (flip _∷_) (y ∷ xs) ys
≡⟨ unfold-reverse (y ∷ xs) ys ⟩
reverse ys ++ [ y ] ++ xs
≡⟨ ++-assoc (reverse ys) [ y ] xs ⟩
(reverse ys ++ [ y ]) ++ xs
≡⟨ cong (λ w w ++ xs) (sym (unfold-reverse [ y ] ys)) ⟩
foldl (flip _∷_) [ y ] ys ++ xs
reverse-∷ : {a} {A : Set a}
(x : A)
(xs : List A)
reverse (x ∷ xs) ≡ reverse xs ++ [ x ]
reverse-∷ x xs = unfold-reverse [ x ] xs
reverse-++ : {a} {A : Set a}
(xs ys : List A)
reverse (xs ++ ys) ≡ reverse ys ++ reverse xs
reverse-++ [] ys = sym (++-right-identity (reverse ys))
reverse-++ (x ∷ xs) ys =
begin
reverse (x ∷ xs ++ ys)
≡⟨ reverse-∷ x (xs ++ ys) ⟩
reverse (xs ++ ys) ++ [ x ]
≡⟨ cong (flip _++_ [ x ]) (reverse-++ xs ys) ⟩
(reverse ys ++ reverse xs) ++ [ x ]
≡⟨ sym (++-assoc (reverse ys) (reverse xs) [ x ]) ⟩
reverse ys ++ reverse xs ++ [ x ]
≡⟨ cong (_++_ (reverse ys)) (sym (reverse-∷ x xs)) ⟩
reverse ys ++ reverse (x ∷ xs)
reverse-twice : {a} {A : Set a}
(xs : List A)
reverse (reverse xs) ≡ xs
reverse-twice [] = refl
reverse-twice (x ∷ xs) =
begin
reverse (reverse (x ∷ xs))
≡⟨ cong reverse (reverse-∷ x xs) ⟩
reverse (reverse xs ++ [ x ])
≡⟨ reverse-++ (reverse xs) [ x ] ⟩
reverse [ x ] ++ reverse (reverse xs)
≡⟨ cong (_++_ (reverse [ x ])) (reverse-twice xs) ⟩
reverse [ x ] ++ xs
≡⟨ refl ⟩
x ∷ xs
∷-right-cancellative : {a} {A : Set a}
(z : A)
(xs ys : List A)
z ∷ xs ≡ z ∷ ys
xs ≡ ys
∷-right-cancellative z [] .[] refl = refl
∷-right-cancellative z (x ∷ xs) .(x ∷ xs) refl = refl
++-left-cancellative : {a} {A : Set a}
(xs ys zs : List A)
zs ++ xs ≡ zs ++ ys
xs ≡ ys
++-left-cancellative xs ys [] rel = rel
++-left-cancellative xs ys (z ∷ zs) rel =
++-left-cancellative xs ys zs
(∷-right-cancellative z (zs ++ xs) (zs ++ ys) rel)
--
-- reverse-[] : ∀ {a} → {A : Set a}
-- → (xs : List A)
-- → reverse xs ≡ []
-- → xs ≡ []
-- reverse-[] [] rel = refl
-- reverse-[] (x ∷ xs) rel with reverse (x ∷ xs) | inspect reverse (x ∷ xs)
-- reverse-[] (x ∷ xs) refl | [] | [ eq ]ev =
-- begin
-- x ∷ xs
-- ≡⟨ sym (reverse-twice (x ∷ xs)) ⟩
-- reverse (reverse (x ∷ xs))
-- ≡⟨ cong reverse (reverse-∷ x xs) ⟩
-- reverse (reverse xs ++ [ x ])
-- ≡⟨ cong reverse (sym (unfold-reverse [ x ] xs)) ⟩
-- reverse (foldl (flip _∷_) [ x ] xs)
-- ≡⟨ cong reverse eq ⟩
-- []
-- ∎
-- reverse-[] (x ∷ xs) rel | z ∷ zs | [ eq ]ev =
-- begin
-- x ∷ xs
-- ≡⟨ sym (reverse-twice (x ∷ xs)) ⟩
-- reverse (reverse (x ∷ xs))
-- ≡⟨ cong reverse (reverse-∷ x xs) ⟩
-- reverse (reverse xs ++ [ x ])
-- ≡⟨ cong reverse (sym (unfold-reverse [ x ] xs)) ⟩
-- reverse (foldl (flip _∷_) [ x ] xs)
-- ≡⟨ cong reverse eq ⟩
-- reverse (z ∷ zs)
-- ≡⟨ cong reverse rel ⟩
-- []
-- ∎
reverse-injective : {a} {A : Set a}
(xs ys : List A)
reverse xs ≡ reverse ys
xs ≡ ys
reverse-injective xs ys rel =
begin
xs
≡⟨ sym (reverse-twice xs) ⟩
reverse (reverse xs)
≡⟨ cong reverse rel ⟩
reverse (reverse ys)
≡⟨ reverse-twice ys ⟩
ys
++-right-cancellative : {a} {A : Set a}
(xs ys zs : List A)
xs ++ zs ≡ ys ++ zs
xs ≡ ys
++-right-cancellative xs ys [] rel =
begin
xs
≡⟨ sym (++-right-identity xs) ⟩
xs ++ []
≡⟨ rel ⟩
ys ++ []
≡⟨ ++-right-identity ys ⟩
ys
++-right-cancellative xs ys (z ∷ zs) rel = reverse-injective xs ys $
∷-right-cancellative z (reverse xs) (reverse ys) $
begin
[ z ] ++ reverse xs
≡⟨ sym (reverse-++ xs (z ∷ [])) ⟩
reverse (xs ++ [ z ])
≡⟨ cong reverse (++-right-cancellative (xs ++ [ z ]) (ys ++ [ z ]) zs (
begin
(xs ++ [ z ]) ++ zs
≡⟨ sym (++-assoc xs [ z ] zs) ⟩
xs ++ z ∷ zs
≡⟨ rel ⟩
ys ++ z ∷ zs
≡⟨ ++-assoc ys [ z ] zs ⟩
(ys ++ [ z ]) ++ zs
∎)) ⟩
reverse (ys ++ [ z ])
≡⟨ reverse-++ ys [ z ] ⟩
[ z ] ++ reverse ys
prop : {xs} Pal xs reverse xs ≡ xs
prop nil = refl
prop (sing c) = refl
prop (cons s c P) =
begin
reverse (c ∷ s ++ [ c ])
≡⟨ reverse-++ (c ∷ s) [ c ] ⟩
c ∷ reverse (c ∷ s)
≡⟨ cong (_∷_ c) (reverse-∷ c s) ⟩
c ∷ reverse s ++ [ c ]
≡⟨ cong (λ x (c ∷ x) ++ [ c ]) (prop P) ⟩
c ∷ s ++ [ c ]
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment