module AgdaBasics where data 𝔹 : Set where true : 𝔹 false : 𝔹 Β¬ : 𝔹 β†’ 𝔹 Β¬ true = false Β¬ false = true _∨_ : 𝔹 β†’ 𝔹 β†’ 𝔹 false ∨ x = x true ∨ _ = true infixr 20 _∨_ _∧_ : 𝔹 β†’ 𝔹 β†’ 𝔹 true ∧ x = x false ∧ _ = false infixr 30 _∧_ if_then_else : {Ξ± : Set} β†’ 𝔹 β†’ Ξ± β†’ Ξ± β†’ Ξ± if true then x else y = x if false then x else y = y infix 5 if_then_else data β„• : Set where ΞΏ : β„• ≻ : β„• β†’ β„• infixl 40 _+_ _+_ : β„• β†’ β„• β†’ β„• ΞΏ + m = m (≻ n) + m = ≻ (n + m) infixl 60 _*_ _*_ : β„• β†’ β„• β†’ β„• ΞΏ * m = ΞΏ (≻ n) * m = m + (n * m) id : {Ξ± : Set} β†’ Ξ± β†’ Ξ± id x = x _∘_ : {Ξ± : Set} {Ξ² : Ξ± β†’ Set} {Ξ³ : (x : Ξ±) β†’ Ξ² x β†’ Set} (f : {x : Ξ±} (y : Ξ² x) β†’ Ξ³ x y) (g : (x : Ξ±) β†’ Ξ² x) (x : Ξ±) β†’ Ξ³ x (g x) (f ∘ g) x = f (g x) _+2 = ≻ ∘ ≻ two = ΞΏ +2 infixr 40 _∷_ data [_] (Ξ± : Set) : Set where Ξ΅ : [ Ξ± ] _∷_ : Ξ± β†’ [ Ξ± ] β†’ [ Ξ± ] map : {Ξ± Ξ² : Set} β†’ (Ξ± β†’ Ξ²) β†’ [ Ξ± ] β†’ [ Ξ² ] map f Ξ΅ = Ξ΅ map f (x ∷ xs) = f x ∷ map f xs data ⟦_⟧ (Ξ± : Set) : β„• β†’ Set where Ξ΅ : ⟦ Ξ± ⟧ ΞΏ _◁_ : {n : β„•} β†’ Ξ± β†’ ⟦ Ξ± ⟧ n β†’ ⟦ Ξ± ⟧ (≻ n) head : {Ξ± : Set} {n : β„•} β†’ ⟦ Ξ± ⟧ (≻ n) β†’ Ξ± head (x ◁ xs) = x vmap : {Ξ± Ξ² : Set} {n : β„•} β†’ (Ξ± β†’ Ξ²) β†’ ⟦ Ξ± ⟧ n β†’ ⟦ Ξ² ⟧ n vmap f Ξ΅ = Ξ΅ vmap f (x ◁ xs) = f x ◁ vmap f xs data Im_βˆ‹_ {Ξ± Ξ² : Set} (f : Ξ± β†’ Ξ²) : Ξ² β†’ Set where im : (x : Ξ±) β†’ Im f βˆ‹ f x inv : {Ξ± Ξ² : Set} (f : Ξ± β†’ Ξ²) (y : Ξ²) β†’ Im f βˆ‹ y β†’ Ξ± inv f .(f x) (im x) = x -- Theory of finite numbers data β‹– : β„• β†’ Set where β—» : {n : β„•} β†’ β‹– (≻ n) β—Ό : {n : β„•} β†’ β‹– n β†’ β‹– (≻ n) magic : {Ξ± : Set} β†’ β‹– ΞΏ β†’ Ξ± magic () infixl 80 _!_ _!_ : {n : β„•} {Ξ± : Set} β†’ ⟦ Ξ± ⟧ n β†’ β‹– n β†’ Ξ± Ξ΅ ! () (x ◁ xs) ! β—» = x (x ◁ xs) ! (β—Ό i) = xs ! i tab : {n : β„•} {Ξ± : Set} β†’ (β‹– n β†’ Ξ±) β†’ ⟦ Ξ± ⟧ n tab {ΞΏ} f = Ξ΅ tab {≻ n} f = f β—» ◁ tab (f ∘ β—Ό) -- Programs as proofs, types as propositions data 𝔽 : Set where -- False record 𝕋 : Set where -- True tautology : 𝕋 tautology = _ isTrue : 𝔹 β†’ Set isTrue true = 𝕋 isTrue false = 𝔽 _<_ : β„• β†’ β„• β†’ 𝔹 _ < ΞΏ = false ΞΏ < ≻ n = true ≻ m < ≻ n = m < n length : {Ξ± : Set} β†’ [ Ξ± ] β†’ β„• length Ξ΅ = ΞΏ length (x ∷ xs) = ≻ (length xs) _!!_∡_ : {Ξ± : Set} β†’ (β„“ : [ Ξ± ]) β†’ (n : β„•) β†’ isTrue (n < length β„“) β†’ Ξ± Ξ΅ !! n ∡ () x ∷ xs !! ΞΏ ∡ _ = x x ∷ xs !! ≻ n ∡ p = xs !! n ∡ p data _==_ {Ξ± : Set} (x : Ξ±) : Ξ± β†’ Set where refl : x == x data _≀_ : β„• β†’ β„• β†’ Set where ≀-ze : {n : β„•} β†’ ΞΏ ≀ n ≀-su : {m n : β„•} β†’ m ≀ n β†’ (≻ m) ≀ (≻ n) ≀-trans : {l m n : β„•} β†’ l ≀ m β†’ m ≀ n β†’ l ≀ n ≀-trans ≀-ze _ = ≀-ze ≀-trans (≀-su lβ€²mβ€²) (≀-su mβ€²nβ€²) = ≀-su (≀-trans lβ€²mβ€² mβ€²nβ€²) min : β„• β†’ β„• β†’ β„• min x y with x < y ... | true = x ... | false = y filter : {Ξ± : Set} β†’ (Ξ± β†’ 𝔹) β†’ [ Ξ± ] β†’ [ Ξ± ] filter _ Ξ΅ = Ξ΅ filter p (x ∷ xs) with p x ... | true = x ∷ filter p xs ... | false = filter p xs infix 20 _βŠ†_ data _βŠ†_ {Ξ± : Set} : [ Ξ± ] β†’ [ Ξ± ] β†’ Set where βŠ†-stop : Ξ΅ βŠ† Ξ΅ βŠ†-drop : βˆ€ {z xs ys} β†’ xs βŠ† ys β†’ xs βŠ† (z ∷ ys) βŠ†-keep : βˆ€ {z xs ys} β†’ xs βŠ† ys β†’ (z ∷ xs) βŠ† (z ∷ ys) filter-lemma-βŠ† : {Ξ± : Set} (p : Ξ± β†’ 𝔹) β†’ (β„“ : [ Ξ± ]) β†’ (filter p β„“ βŠ† β„“) filter-lemma-βŠ† _ Ξ΅ = βŠ†-stop filter-lemma-βŠ† p (x ∷ xs) with p x ... | true = βŠ†-keep (filter-lemma-βŠ† p xs) ... | false = βŠ†-drop (filter-lemma-βŠ† p xs) +-lemma-id-right : (n : β„•) β†’ n + ΞΏ == n +-lemma-id-right ΞΏ = refl +-lemma-id-right (≻ mβ€²) with mβ€² + ΞΏ | +-lemma-id-right mβ€² ... | .mβ€² | refl = refl module Maybe where data _⁇ (Ξ± : Set) : Set where β—‡ : Ξ± ⁇ β—† : Ξ± β†’ Ξ± ⁇ maybe : {Ξ± Ξ² : Set} β†’ Ξ² β†’ (Ξ± β†’ Ξ²) β†’ Ξ± ⁇ β†’ Ξ² maybe z _ β—‡ = z maybe z f (β—† x) = f x open Maybe mapMaybe : {Ξ± Ξ² : Set} β†’ (Ξ± β†’ Ξ²) β†’ Ξ± ⁇ β†’ Ξ² ⁇ mapMaybe f m = maybe β—‡ (β—† ∘ f) m record _Γ—_ (Ξ± Ξ² : Set) : Set where field x : Ξ± y : Ξ² _βŠ—_ : {Ξ± Ξ² : Set} β†’ Ξ± β†’ Ξ² β†’ Ξ± Γ— Ξ² a βŠ— b = record { x = a; y = b } fst : {Ξ± Ξ² : Set} β†’ Ξ± Γ— Ξ² β†’ Ξ± fst = _Γ—_.x snd : {Ξ± Ξ² : Set} β†’ Ξ± Γ— Ξ² β†’ Ξ² snd = _Γ—_.y -- "type-class" emulation using records record Monad (Μ : Set β†’ Set) : Set1 where field return : βˆ€ {Ξ±} β†’ Ξ± β†’ Μ Ξ± _>>=_ : βˆ€ {Ξ± Ξ²} β†’ Μ Ξ± β†’ (Ξ± β†’ Μ Ξ²) β†’ Μ Ξ² mapM : βˆ€ {Ξ± Ξ²} β†’ (Ξ± β†’ Μ Ξ²) β†’ [ Ξ± ] β†’ Μ [ Ξ² ] mapM _ Ξ΅ = return Ξ΅ mapM f (x ∷ xs) = f x >>= \y β†’ mapM f xs >>= \ys β†’ return (y ∷ ys) mapMβ€² : {Μ : Set β†’ Set} β†’ Monad Μ β†’ βˆ€ {Ξ± Ξ²} β†’ (Ξ± β†’ Μ Ξ²) β†’ [ Ξ± ] β†’ Μ [ Ξ² ] mapMβ€² Mon f xs = Monad.mapM Mon f xs -- Exercises -- 1) Matrix, row-major (would be a parameterized type synonym in Haskell) 𝕄 : Set β†’ β„• β†’ β„• β†’ Set 𝕄 Ξ± n m = ⟦ ⟦ Ξ± ⟧ m ⟧ n -- a) replicate : {n : β„•} {Ξ± : Set} β†’ Ξ± β†’ ⟦ Ξ± ⟧ n replicate {ΞΏ} _ = Ξ΅ replicate {≻ m} x = x ◁ replicate {m} x -- b) infixl 90 _$*_ _$*_ : {n : β„•} {Ξ± Ξ² : Set} β†’ ⟦ (Ξ± β†’ Ξ²) ⟧ n β†’ ⟦ Ξ± ⟧ n β†’ ⟦ Ξ² ⟧ n Ξ΅ $* Ξ΅ = Ξ΅ (f ◁ fs) $* (x ◁ xs) = f x ◁ fs $* xs -- Matrix transposition transpose : βˆ€ {Ξ± n m} β†’ 𝕄 Ξ± n m β†’ 𝕄 Ξ± m n transpose Ξ΅ = replicate Ξ΅ transpose (r ◁ rs) = vmap _◁_ r $* transpose rs -- 2) Vector lookup -- a) lemma-!-inv-tab : βˆ€ {Ξ± n} (t : β‹– n β†’ Ξ±) (i : β‹– n) β†’ (tab t) ! i == t i lemma-!-inv-tab f β—» = refl lemma-!-inv-tab f (β—Ό iβ€²) = lemma-!-inv-tab (f ∘ β—Ό) iβ€² lemma-tab-inv-! : βˆ€ {Ξ± n} (Ξ½ : ⟦ Ξ± ⟧ n) β†’ tab (_!_ Ξ½) == Ξ½ lemma-tab-inv-! Ξ΅ = refl lemma-tab-inv-! (x ◁ xs) with tab (_!_ xs) | lemma-tab-inv-! xs ... | .xs | refl = refl -- 3) Sublists βŠ†-refl : {Ξ± : Set} {β„“ : [ Ξ± ]} β†’ β„“ βŠ† β„“ βŠ†-refl {Ξ±} {Ξ΅} = βŠ†-stop βŠ†-refl {Ξ±} {x ∷ xs} = βŠ†-keep βŠ†-refl βŠ†-lemma-empty : {Ξ± : Set} {β„“ : [ Ξ± ]} β†’ Ξ΅ βŠ† β„“ βŠ†-lemma-empty {Ξ±} {Ξ΅} = βŠ†-stop βŠ†-lemma-empty {Ξ±} {x ∷ xs} = βŠ†-drop βŠ†-lemma-empty βŠ†-lemma-cons : {Ξ± : Set} {ℓ₁ β„“β‚‚ : [ Ξ± ]} {e : Ξ±} β†’ (e ∷ ℓ₁) βŠ† β„“β‚‚ β†’ ℓ₁ βŠ† β„“β‚‚ βŠ†-lemma-cons {Ξ±} {Ξ΅} _ = βŠ†-lemma-empty βŠ†-lemma-cons {Ξ±} {x ∷ xs} (βŠ†-drop p) = βŠ†-drop (βŠ†-lemma-cons p) βŠ†-lemma-cons {Ξ±} {x ∷ xs} (βŠ†-keep p) = βŠ†-drop p βŠ†-trans : {Ξ± : Set} {xs ys zs : [ Ξ± ]} β†’ xs βŠ† ys β†’ ys βŠ† zs β†’ xs βŠ† zs βŠ†-trans βŠ†-stop q = βŠ†-lemma-empty βŠ†-trans (βŠ†-drop p) q = βŠ†-trans p (βŠ†-lemma-cons q) βŠ†-trans (βŠ†-keep p) q = βŠ†-trans (βŠ†-keep p) q -- b) infixr 30 _::_ data π•Š{Ξ± : Set} : [ Ξ± ] β†’ Set where [] : π•Š Ξ΅ _::_ : βˆ€ {xs} β†’ (x : Ξ±) β†’ π•Š xs β†’ π•Š (x ∷ xs) skip : βˆ€ {x xs} β†’ π•Š xs β†’ π•Š (x ∷ xs) forget : {Ξ± : Set} {β„“ : [ Ξ± ]} β†’ π•Š β„“ β†’ [ Ξ± ] forget {β„“ = l} s = l -- c) lemma-forget-βŠ† : {Ξ± : Set} {β„“ : [ Ξ± ]} (s : π•Š β„“) β†’ forget s βŠ† β„“ lemma-forget-βŠ† [] = βŠ†-stop lemma-forget-βŠ† (x :: zs) = βŠ†-keep βŠ†-refl lemma-forget-βŠ† (skip zs) = βŠ†-refl -- d) filterβ€² : {Ξ± : Set} β†’ (Ξ± β†’ 𝔹) β†’ (β„“ : [ Ξ± ]) β†’ π•Š β„“ filterβ€² _ Ξ΅ = [] filterβ€² p (x ∷ xs) with p x ... | true = x :: filterβ€² p xs ... | false = skip (filterβ€² p xs) -- e) complement : {Ξ± : Set} {β„“ : [ Ξ± ]} β†’ π•Š β„“ β†’ π•Š β„“ complement [] = [] complement (z :: zs) = skip (complement zs) complement (skip {x} {_} zs) = x :: complement zs -- f) sublists : {Ξ± : Set} (β„“ : [ Ξ± ]) β†’ [ π•Š β„“ ] sublists Ξ΅ = [] ∷ Ξ΅ sublists (x ∷ xs) = map (_::_ x) (sublists xs)