Skip to content

Instantly share code, notes, and snippets.

@aljce
Last active March 21, 2023 23:28
Show Gist options
  • Save aljce/db3d03bf3d99a502d6f7e28eb8dbb389 to your computer and use it in GitHub Desktop.
Save aljce/db3d03bf3d99a502d6f7e28eb8dbb389 to your computer and use it in GitHub Desktop.
GPT4 ChurchList conversion
-- Prompt: can you prove that churchlists are isomorphic to regular lists in agda
-- Define natural numbers
data ℕ : Set where
zero : ℕ
suc : ℕ → ℕ
-- Define regular lists
data List (A : Set) : Set where
[] : List A
_∷_ : A → List A → List A
-- Define Church-encoded lists (ChurchLists)
record ChurchList (A : Set) : Set where
field
fold : ∀ {B} → (A → B → B) → B → B
open ChurchList
-- Define operations for ChurchLists
empty : ∀ {A} → ChurchList A
empty = record { fold = λ _ z → z }
cons : ∀ {A} → A → ChurchList A → ChurchList A
cons x xs = record { fold = λ f z → f x (fold xs f z) }
-- Define conversion functions between ChurchLists and Lists
toChurchList : ∀ {A} → List A → ChurchList A
toChurchList [] = empty
toChurchList (x ∷ xs) = cons x (toChurchList xs)
fromChurchList : ∀ {A} → ChurchList A → List A
fromChurchList xs = fold xs _∷_ []
-- Prove that toChurchList and fromChurchList are inverses of each other
to-from-proof : ∀ {A} → (xs : List A) → fromChurchList (toChurchList xs) ≡ xs
to-from-proof [] = refl
to-from-proof (x ∷ xs) = cong (λ y → x ∷ y) (to-from-proof xs)
from-to-proof : ∀ {A} → (xs : ChurchList A) → toChurchList (fromChurchList xs) ≡ xs
from-to-proof {A} xs = begin
record { fold = λ f z → fold (toChurchList (fromChurchList xs)) f z } ≡⟨ cong (λ y → record { fold = λ f z → fold y f z }) (fold-ext xs) ⟩
xs
where
fold-ext : ∀ (xs : ChurchList A) → fold (toChurchList (fromChurchList xs)) ≡ fold xs
fold-ext xs = funExt (λ f → funExt (λ z → begin
fold (toChurchList (fromChurchList xs)) f z ≡⟨ refl ⟩
fold (toChurchList (fold xs _∷_ [])) f z ≡⟨ cong (λ l → fold (toChurchList l) f z) (fold xs _∷_ []) ⟩
fold xs f z
∎))
funExt : ∀ {A B : Set} {f g : A → B} → (∀ x → f x ≡ g x) → f ≡ g
funExt p = λ where .funExt.step → p
-- Define the isomorphism proof
iso-proof : ∀ {A} → Iso (List A) (ChurchList A)
iso-proof = record { to = toChurchList; from = fromChurchList; to-from = to-from-proof; from-to = from-to-proof }
-- Helper functions and datatypes for the isomorphism proof
data _≡_ {A : Set} (x : A) : A → Set where
refl : x ≡ x
data Iso (A B : Set) : Set where
record
field
to : A → B
from : B →
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment