NextjournalJournal Part II
First some imports and definitions
module part2 whereopen import Level using (Level; _⊔_) renaming (zero to lzero; suc to lsuc)import Relation.Binary.PropositionalEquality as Eqopen Eq using (_≡_; refl; cong; sym)open Eq.≡-Reasoningopen import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _<_; _≤_; s≤s; z≤n)open import Data.Nat.Properties using (+-assoc; +-comm; +-identityˡ; +-identityʳ; *-assoc; *-identityˡ; *-identityʳ)Function extensionality and univalence
If two functions are equal we can show that they act the same on every element in their domain (which must necessarily be the same for the functions).
cong-app-nondep : ∀ {A B : Set} {f g : A → B} → f ≡ g → (x : A) → f x ≡ g xcong-app-nondep refl x = reflcong-app : ∀ {A : Set} {B : A → Set} {f g : (x : A) → B x} → f ≡ g → (x : A) → f x ≡ g xcong-app refl x = reflUnfortunately, we cannot go the other way around. It is impossible to show that if two functions act the same on every element in their domain then they are equal. But we can postulate it:
postulate funext-nondep : {A B : Set} {f g : A → B} → ((x : A) → f x ≡ g x) ----------------------- → f ≡ gpostulate funext : ∀ {A : Set} {B : A → Set} {f g : (x : A) → B x} → ((x : A) → f x ≡ g x) ----------------------- → f ≡ gThis is usually called function extensionality. It is an extremely useful axiom. As an example we define addition of naturals again:
_+'_ : ℕ → ℕ → ℕm +' zero = mm +' suc n = suc (m +' n)It is different from the definition _+_ in which we pattern matched on the first argument. We want to show that these are equal. For this we need funext.
+≡+' : _+_ ≡ _+'_+≡+' = funext-nondep (λ m → funext-nondep λ n → same-on-all m n) where same-on-all : ∀ m n → m + n ≡ m +' n same-on-all zero zero = refl same-on-all zero (suc n) = cong suc (same-on-all zero n) same-on-all (suc m) zero = cong suc (same-on-all m zero) same-on-all (suc m) (suc n) rewrite +-comm m (suc n) | +-comm n m = cong suc (same-on-all (suc m) n)Function extensionality follows from a more general axiom called the univalence axiom. In order to state it we need to define equivalences.
record is-equiv {i j} {A : Set i} {B : Set j} (f : A → B) : Set (i ⊔ j) where constructor constr-is-equiv field inv : B → A left-inv : (x : A) → inv (f x) ≡ x right-inv : (y : B) → f (inv y) ≡ yinfix 0 _≃_record _≃_ {i} (A B : Set i) : Set i where constructor constr-equiv field equiv : A → B is-an-equiv : is-equiv equivNote: this definition of equivalence is ok because by default, as types in agda are sets. But if you use, for example, the option --without-K, then equivalence should be defined differently because not all types are sets with this option. If interested, you can read more about equivalences in chapter 2.4 of the HoTT book.
open is-equivopen _≃_As an example of equivalences, any type is equivalent to itself.
ide : (A : Set) → A ≃ Aide A = constr-equiv (λ x → x) (constr-is-equiv (λ x → x) (λ _ → refl) (λ _ → refl))In fact, _≃_ is an equivalence relation, i.e. it is also symmetric and transitive.
_⁻¹ : {A B : Set} → A ≃ B → B ≃ A_⁻¹ e = constr-equiv (λ x → inv (is-an-equiv e) x) (constr-is-equiv (λ x → equiv e x) (λ x → right-inv (is-an-equiv e) x) (λ y → left-inv (is-an-equiv e) y))_∘≃_ : {A B C : Set} → B ≃ C → A ≃ B → A ≃ C_∘≃_ e f = constr-equiv (λ x → equiv e (equiv f x)) (constr-is-equiv (λ x → inv (is-an-equiv f) (inv (is-an-equiv e) x)) (λ x → begin (inv (is-an-equiv f) (inv (is-an-equiv e) (equiv e (equiv f x)))) ≡⟨ cong (inv (is-an-equiv f)) (left-inv (is-an-equiv e) (equiv f x)) ⟩ (inv (is-an-equiv f) (equiv f x)) ≡⟨ left-inv (is-an-equiv f) x ⟩ x ∎) (λ y → begin (equiv e (equiv f (inv (is-an-equiv f) (inv (is-an-equiv e) y)))) ≡⟨ cong (equiv e) (right-inv (is-an-equiv f) (inv (is-an-equiv e) y)) ⟩ (equiv e (inv (is-an-equiv e) y)) ≡⟨ right-inv (is-an-equiv e) y ⟩ y ∎) ) We can do equational reasoning on equivalences by mimicking the definitions of equational reasoning for equality. For details, see https://plfa.github.io/Isomorphism/#equational-reasoning-for-isomorphism
As with cong-app, we can go from equality to equivalence:
coe' : {A B : Set} → A ≡ B → A → Bcoe' refl x = xcoe!' : {A B : Set} → A ≡ B → B → Acoe!' refl x = xcoe-equiv' : {A B : Set} → A ≡ B → A ≃ Bcoe-equiv' {A} refl = ide AThe univalence axiom states that coe-equiv is itself an equivalence. In particular, we can go from an equivalence to an equality between types.
postulate ua : {A B : Set} ---------------------- → is-equiv (coe-equiv' {A} {B})The intuition is that if there is a one-to-one correspondence between the terms of types A and B then we want A and B to be considered equal.
Exercise: Try to generalize coe, coe!, coe-equiv and ua to any universe level.
-- Pending exercise!coe : {A B : Set} → A ≡ B → A → Bcoe refl x = xcoe! : {A B : Set} → A ≡ B → B → Acoe! refl x = xcoe-equiv : {A B : Set} → A ≡ B → A ≃ Bcoe-equiv {A} refl = ide AEquivalence reasoning
module ≃-Reasoning where infix 1 ≃-begin_ infixr 2 _≃⟨_⟩_ infix 3 _≃-∎ ≃-begin_ : ∀ {A B : Set} → A ≃ B ----- → A ≃ B ≃-begin A≃B = A≃B _≃⟨_⟩_ : ∀ (A : Set) {B C : Set} → A ≃ B → B ≃ C ----- → A ≃ C A ≃⟨ A≃B ⟩ B≃C = B≃C ∘≃ A≃B -- ≃-trans A≃B B≃C _≃-∎ : ∀ (A : Set) ----- → A ≃ A A ≃-∎ = ide A -- ≃-reflopen ≃-ReasoningDTT (à la Martin Löf)
Read: https://ncatlab.org/nlab/show/Martin-Löf+dependent+type+theory
module dtt where Type : (ℓ : Level) → Set (lsuc ℓ) Type ℓ = Set ℓ Basic types: inline_formula not implemented, 𝟘, 𝟙, 𝟚, ℕ, inline_formula not implemented
Type formers: ∑, ∏, → , × , ⊎
Basic types and type formers
Zero-point type
data 𝟘 (ℓ : Level) : Type ℓ whereOne-point type
record 𝟙 (ℓ : Level) : Type ℓ where constructor unitA record in Agda comes with eta-equality by default. This is the main difference respect to the definition of the unit type using the type former data.
data 𝟙' : Set where unit' : 𝟙' {- eta-fail : ∀ (w : 𝟙') → w ≡ unit' eta-fail w = refl -- So you have to prove it, by pattern-matching on w. -} eta-succeed : ∀ (w : 𝟙 lzero) → w ≡ unit eta-succeed w = reflTwo-point type
data 𝟚 (ℓ : Level) : Type ℓ where 𝟘₂ : 𝟚 ℓ 𝟙₂ : 𝟚 ℓNatural numbers type
data ℕ : Type lzero where zero : ℕ succ : ℕ → ℕIdentity type
data _≡_ {ℓ : Level}{A : Type ℓ} (a : A) : A → Type ℓ where refl : a ≡ aSigma types
record Σ {ℓ₁ ℓ₂ : Level} (A : Type ℓ₁) (B : A → Type ℓ₂) -- B is a type family over A. ------------------------------- : Type (ℓ₁ ⊔ ℓ₂) where constructor _,_ field π₁ : A π₂ : B π₁ infixr 60 _,_ open Σ public ∑ = Σ -- \Sigma and \sum syntax ∑ A (λ a → B) = ∑[ a ∶ A ] B _×_ : {ℓ₁ ℓ₂ : Level} → Type ℓ₁ → Type ℓ₂ → Type (ℓ₁ ⊔ ℓ₂) _×_ A B = ∑ A (λ _ → B) eta-× : ∀ {A B : Set} → (w : A × B) → ( π₁ w , π₂ w) ≡ w eta-× w = reflPi types
∏ : ∀ {ℓ₁ ℓ₂ : Level} → (A : Type ℓ₁) (B : A → Type ℓ₂) --------------------------------- → Type (ℓ₁ ⊔ ℓ₂) ∏ A B = ∀ (x : A) → B x Π = ∏ -- \prod vs \Pi syntax ∏ A (λ a → B) = ∏[ a ∶ A ] BCoproducts
data _⊎_ {ℓ₁ ℓ₂ : Level} -- type \u+ to get ⊎ (A : Type ℓ₁) (B : Type ℓ₂) ---------------- : Type (ℓ₁ ⊔ ℓ₂) where inl : A → A ⊎ B inr : B → A ⊎ B infixr 31 _⊎_Function type
{- p : (∏ A (λ _ → B)) ≡ (A → B) p = idp -}Finite type [n]
open dttFin : ℕ → Type _Fin n = Σ ℕ (λ m → m < n)The above definition is one of many, we discussed in the session some of these definitions. You can try to define them from the hints given below.
exfalso : ∀ {ℓ₁ ℓ₂ : Level} {A : Type ℓ₁} → (𝟘 ℓ₂ → A)exfalso ()Exercises
+-elim : ∀ {ℓ₁ ℓ₂ ℓ₃ : Level} → {A : Type ℓ₁}{B : Type ℓ₂} {C : Type ℓ₃} → (A → C) → (B → C) ------------------- → (A ⊎ B) → C +-elim f g (inl x) = f x+-elim f g (inr x) = g xvariable ℓ ℓ₁ ℓ₂ : Level A B : (ℓ : Level) → Type ℓ ex1 : 𝟘 ℓ ⊎ 𝟙 ℓ ≃ 𝟙 ℓ ex1 = constr-equiv (λ _ → unit) (constr-is-equiv (λ x → inr x) (λ {(inr x) → refl}) (λ y → refl))ex2 : 𝟘 ℓ ⊎ A ℓ ≃ A ℓ ex2 = constr-equiv (λ {(inr x) → x}) (constr-is-equiv (λ x → inr x) (λ {(inr x) → refl}) (λ _ → refl))
ex3 : 𝟙 ℓ ⊎ 𝟙 ℓ ≃ 𝟚 ℓ ex3 = constr-equiv (λ {(inl x) → 𝟘₂ ; (inr x) → 𝟙₂}) (constr-is-equiv (λ {𝟘₂ → inl unit ; 𝟙₂ → inr unit}) (λ {(inl x) → refl ; (inr x) → refl}) (λ {𝟘₂ → refl ; 𝟙₂ → refl}))ex4 : (𝟘 ℓ → 𝟙 ℓ ) ≃ 𝟙 ℓ ex4 = constr-equiv (λ _ → unit) (constr-is-equiv (λ x → λ {()}) (λ x → refl) (λ y → refl))ex5 : A ℓ₁ × B ℓ₂ ≃ B ℓ₂ × A ℓ₁ex5 = constr-equiv (λ {(π₁ , π₂) → π₂ , π₁}) (constr-is-equiv (λ {(π₃ , π₄) → π₄ , π₃}) (λ _ → refl) (λ _ → refl))-- More ex. from the book.-- ⊎-comm-- ⊎-assoc-- currying : ∀ {A B C : Set} → (A → B → C) ≃ (A × B → C)-- →-distrib-⊎ : ∀ {A B C : Set} → (A ⊎ B → C) ≃ ((A → C) × (B → C))-- →-distrib-× : ∀ {A B C : Set} → (A → B × C) ≃ (A → B) × (A → C)-- ×-distrib-⊎ : ∀ {A B C : Set} → (A ⊎ B) × C ≃ (A × C) ⊎ (B × C)-- ⊎-distrib-× : ∀ {A B C : Set} → (A × B) ⊎ C ≲ (A ⊎ C) × (B ⊎ C)-- ⊎-weak-× : ∀ {A B C : Set} → (A ⊎ B) × C → A ⊎ (B × C)-- ⊎×-implies-×⊎ : ∀ {A B C D : Set} → (A × B) ⊎ (C × D) → (A ⊎ C) × (B ⊎ D)-- ex6 : (A × B) × C ≃ A × (B × C)Propositions as types
If we view propositions as types, then the above type formers correspond to logical connectives and quantifiers as follows:
Σ corresponds to ∃: A proof that there exists an element x in A such that the proposition P x holds is a pair (a , p) where a is an element in A and p is a proof that P a holds, i.e. a : A and p : P a.
∏ corresponds to ∀: A proof that the proposition P x holds for all x in A is a function that, given an element a in A produces a proof that P a holds, i.e. a function that for every a : A returns some p : P a.
→ corresponds to implication: A proof that P implies Q is a 'function' that, given a proof of P, returns a proof of Q, i.e. a function f that maps any p : P to some f p : Q.
× corresponds to ∧: A proof of the proposition P ∧ Q is a proof of P together with a proof of Q, i.e. a pair (p , q) where p : P and q : Q.
⊎ corresponds to ∨: A proof of the proposition P ∨ Q consists either of a proof of P or a proof of Q, i.e. it is either inl p where p : P or it is inr q where q : Q.
𝟘 corresponds to ⊥: The false proposition has no proofs, i.e. it is the type with no terms; the empty type.
𝟙 corresponds to ⊤: The true proposition is true, i.e. it is a type with a term; the one-element type.
𝟚 corresponds to the booleans: The set of booleans is a set with two elements.
¬ P is defined as P → ⊥ (this definition of negation works in any system that has implication and ⊥, not just in type theory).
{- False is the empty type -}⊥ = 𝟘¬_ : {ℓ : Level} → Type ℓ → Type ℓ¬_ {ℓ} A = A → ⊥ ℓ{- True is the one-element type -}⊤ = 𝟙 {- The booleans is the two-element type -}Bool = 𝟚 lzerotrue false : Booltrue = 𝟙₂false = 𝟘₂ As an example of propositions as types, we proved that not all natural numbers are successors of some other natural number:
isSuc : (n : ℕ) → Type lzeroisSuc zero = ⊥ lzeroisSuc (suc n) = ⊤ lzero-- notice that we map n to a type, not a termall-nats-are-not-suc : ¬ (Π ℕ isSuc) -- Π ℕ isSuc → ⊥all-nats-are-not-suc f = f zeroWe can also show this using booleans instead:
false≠true : ¬ (false ≡ true)false≠true ()-- we pattern match on a term p : false lzero ≡ true lzero (C-c C-c)-- but agda realizes this is impossible, so it reduces to the absurd patternis-suc : (n : ℕ) → Boolis-suc zero = false is-suc (suc n) = true all-nats-are-not-suc' : ¬ (∏[ n ∶ ℕ ] (is-suc n ≡ true))all-nats-are-not-suc' f = false≠true (f zero)We also proved one implication of one of the de Morgan laws:
_←_ : {ℓ₁ ℓ₂ : Level} (A : Type ℓ₁) (B : Type ℓ₂) → Type (ℓ₁ ⊔ ℓ₂)A ← B = B → A-- it was convenient to add this notation¬∧←¬∨¬ : {ℓ : Level} {P Q : Type ℓ} → (¬ (P × Q)) ← ((¬ P) ⊎ (¬ Q))¬∧←¬∨¬ (inl f) w = f (π₁ w) -- this is one way to do this¬∧←¬∨¬ (inr f) (p , q) = f q -- or we can pattern match on wWe started trying to prove this, but it does not hold in constructive/intuitionistic logic (which is what is in Agda by default):
{-¬∧→¬∨¬ : {ℓ : Level} {P Q : Type ℓ} → ¬ (P × Q) → (¬ P) ⊎ (¬ Q)¬∧→¬∨¬ f = ?-}This is because in order to prove (¬ P) ⊎ (¬ Q) we need to either prove (¬ P) or (¬ Q). But we are only given ¬ (P × Q), which does not tell us which of P or Q is false, only that not both of them are true.
Exercise: Try to prove the other de Morgan laws.
-- ¬ (P ∨ Q) → ¬ P ∧ ¬ Q¬∨→¬∧¬ : {ℓ : Level} {P Q : Type ℓ} → ¬ (P ⊎ Q) → (¬ P) × (¬ Q)¬∨→¬∧¬ = ?-- ¬ (P ∨ Q) ← ¬ P ∧ ¬ Q¬∨←¬∧¬ : {ℓ : Level} {P Q : Type ℓ} → (¬ (P ⊎ Q)) ← ((¬ P) × (¬ Q))¬∨←¬∧¬ = ?An important observation is that double negation elimination does not hold in constructive logic (and thus in Agda), i.e. the implication ¬ (¬ A) → A does not hold.
With our view of propositions as types, this makes sense. A proof of ¬ (¬ A) → A would be a function f : ¬ (¬ A) → A. But if we expand the definition of negation, ¬ (¬ A) is defined as (A → ⊥) → ⊥, i.e. the set of functions that has as domain the set of functions from A to the empty type and as codomain the empty type. Then, given such a function, f would somehow be able to produce a term of type A from this. But this is impossible: no function φ : (A → ⊥) → ⊥contains any information about terms in A.
Similarly, the law of excluded middle ∀ (A : Type) → (A ∨ ¬ A), does not hold. Exercise: Try to prove it! What is the problem?
We can however prove double negation elimination for the booleans:
¬'_ : Bool → Bool¬' 𝟘₂ = 𝟙₂¬' 𝟙₂ = 𝟘₂double-neg-Bool : (b : Bool) → ¬' (¬' b) ≡ bdouble-neg-Bool 𝟘₂ = refldouble-neg-Bool 𝟙₂ = reflDecidable types
In the journal part I, we introduce relations over a type. The identity type of inline_formula not implemented is itself a (homogeneous) relation between two elements of type inline_formula not implemented. Given inline_formula not implemented, it gives rise the question whether inline_formula not implemented is equal to inline_formula not implemented, or not? But also, is there any general procedure to check the type inline_formula not implemented is inhabited or not?
x y : ℕx = suc (suc zero)y = suc (suc (suc (suc zero)))¬x≡y : ¬ (x ≡ y)¬x≡y = {! !}We say the type inline_formula not implemented has decidable equality when we are able to answer all these questions by means of a proof, a.k.a program. In general, we can talk about decidability of any binary operation on any type as it follows.
data Dec (A : Set) : Set where yes : A → Dec A no : ¬ A → Dec AWe have above an Agda view. We encode the some "knowledge" about the relation or type inline_formula not implemented:
yesstands for the case, inline_formula not implemented is inhabited, i.e., we posse a term of type inline_formula not implemented.nostands for the opposite case toyes.
Now, given a term x : Dec A , by pattern matching on it, we can determine if it was because we had a term of type inline_formula not implemented, or it if wasn't that the case.
⌊_⌋ : ∀ {A : Set} → Dec A → Bool⌊ yes x ⌋ = true⌊ no ¬x ⌋ = falseLemma. Given a decidable type inline_formula not implemented, inline_formula not implemented is also decidable.
¬? : ∀ {A : Set} → Dec A → Dec (¬ A)¬? (yes x) = no (λ f → f x)¬? (no ¬x) = yes ¬xLemma. Decidability is closed under the type formers inline_formula not implemented , and inline_formula not implemented under certain conditioninline_formula not implemented.
Naturals has decidable equality
Now, we are going to prove the natural numbers data type posses a decidable equality. To do that, we start checking when two numbers are equal. One can do this by construction.
f : (n m : ℕ) → Boolf 0 0 = truef 0 (suc m) = falsef (suc n) 0 = falsef (suc n) (suc m) = f n msuc-is-inj : ∀ {a b : ℕ } → suc a ≡ suc b → a ≡ bsuc-is-inj {a} {.a} refl = reflg : ∀ (n m : ℕ) → Dec (n ≡ m)g 0 0 = yes reflg 0 (suc m) = no (λ {()})g (suc n) 0 = no (λ ())g (suc n) (suc m) with g n m... | yes n≡m = yes (cong suc n≡m)... | no ¬n≡m = no (λ p → ¬n≡m (suc-is-inj p))So, our first approach to decide whether two natural numbers are equal or not.
method-that-decides : ∀ (n m : ℕ) → (n ≡ m) ⊎ (¬ (n ≡ m))method-that-decides 0 0 = inl reflmethod-that-decides 0 (suc m) = inr (λ ())method-that-decides (suc n) 0 = inr (λ ())method-that-decides (suc n) (suc m) with method-that-decides n m... | inl x = inl (cong suc x)... | inr n≠m = inr λ p → n≠m (suc-is-inj p)equiv-dec-m : ∀ { A : Set } → Dec A ≃ (A ⊎ (¬ A))equiv-dec-m {A} = constr-equiv f' (constr-is-equiv g' h1 h2) where f' : Dec A → A ⊎ (¬ A) f' (yes x) = inl x f' (no x) = inr x g' : A ⊎ (¬ A) → Dec A g' (inl x) = yes x g' (inr y) = no y h1 : (x : Dec A) → g' (f' x) ≡ x h1 (yes x) = refl h1 (no x) = refl h2 : (x : A ⊎ (¬ A)) → f' (g' x) ≡ x h2 (inl x) = refl h2 (inr y) = reflClassical reasoning
By classical reasoning, we refer to constructions where we use in some way any equivalent formulation of the law of excluded middle.
postulate classical-math : ∀ {A : Set} → A ⊎ (¬ A)Lists
Lists in Agda can be defined recursively as either being an empty list or an element followed by a list.
data List (A : Set) : Set where [] : List A _∷_ : A -> List A -> List Ainfixr 5 _∷__ : List ℕ_ = 0 ∷ 1 ∷ 2 ∷ [] The language pragma specifies that Agda should use Haskell lists behind the scenes.
To make (hardcoded) lists more readable, we define a pattern using the typical list notation found in other languages: [1, 2, 5, 3]. (TODO: comma is already an infix operator, so we have to use a dollar-sign for now).
pattern [_] z = z ∷ []pattern [_$_] y z = y ∷ z ∷ []pattern [_$_$_] x y z = x ∷ y ∷ z ∷ []pattern [_$_$_$_] w x y z = w ∷ x ∷ y ∷ z ∷ []pattern [_$_$_$_$_] v w x y z = v ∷ w ∷ x ∷ y ∷ z ∷ []pattern [_$_$_$_$_$_] u v w x y z = u ∷ v ∷ w ∷ x ∷ y ∷ z ∷ []Concatenating lists (++)
Next, we define an operator for concatenating two lists.
_++_ : ∀ {A : Set} -> List A -> List A -> List A[] ++ ys = ys(x ∷ xs) ++ ys = x ∷ (xs ++ ys)_ : [ 0 $ 1 $ 2 ] ++ [ 3 $ 4 ] ≡ [ 0 $ 1 $ 2 $ 3 $ 4 ]_ = begin ([ 0 $ 1 $ 2 ] ++ [ 3 $ 4 ]) -- 0 : [1, 2] ++ [3, 4] ≡⟨ refl ⟩ [ 0 $ 1 $ 2 $ 3 $ 4 ] ∎We show that the ++-operator is associative and that the empty list is neutral with respect to ++. This is a first step to showing that lists, ++ and [] together forms a monoid. More on this later.
++-assoc : ∀ {A : Set} (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) ++-identity-l : ∀ {A : Set} (xs : List A) -> [] ++ xs ≡ xs++-identity-l xs = refl++-identity-r : ∀ {A : Set} (xs : List A) -> xs ++ [] ≡ xs++-identity-r [] = refl++-identity-r (x ∷ xs) = cong (x ∷_) (++-identity-r xs)++-identityˡ = ++-identity-l++-identityʳ = ++-identity-rLength
We define a function length on lists and show that the length of two concatenated lists is the same as adding the lengths of the two lists.
length : ∀ {A : Set} -> List A -> ℕlength [] = zerolength (x ∷ xs) = suc (length xs)_ : length [ 0 $ 1 $ 2 ] ≡ 3_ = begin length (0 ∷ 1 ∷ 2 ∷ []) ≡⟨⟩ suc (length (1 ∷ 2 ∷ [])) ≡⟨⟩ suc (suc (length (2 ∷ []))) ≡⟨⟩ suc (suc (suc (length {ℕ} []))) ≡⟨⟩ suc (suc (suc zero)) ∎length-++ : ∀ {A : Set} (xs ys : List A) → length (xs ++ ys) ≡ length xs + length yslength-++ [] ys = refllength-++ (x ∷ xs) ys = cong suc (length-++ xs ys)Reverse
We define the function reverse and show that it distributes over ++, and that it is involutive - composing the function with itself gives the identity function.
-- reverse [1, 3, 5, 7] = [7, 5, 3, 1]reverse : ∀ {A : Set} → List A → List Areverse [] = []reverse (x ∷ xs) = reverse xs ++ [ x ]{- This is not working and I don't know why! J._ : List ℕ_ = reverse {ℕ} [ 1 , 3 , 5 , 7 ]_ : reverse [ 1 , 3 , 5 , 7 ] ≡ [ 7 , 5 , 3 , 1 ]_ = refl-}reverse-++-distrib : ∀ {A : Set} -> (xs ys : List A) -> reverse (xs ++ ys) ≡ reverse ys ++ reverse xsreverse-++-distrib [] ys = sym (++-identity-r (reverse ys))reverse-++-distrib (x ∷ xs) ys = begin reverse ((x ∷ xs) ++ ys) ≡⟨⟩ reverse (x ∷ (xs ++ ys)) ≡⟨⟩ reverse (xs ++ ys) ++ [ x ] ≡⟨ cong (_++ [ x ]) (reverse-++-distrib xs ys) ⟩ (reverse ys ++ reverse xs) ++ [ x ] ≡⟨ ++-assoc (reverse ys) (reverse xs) [ x ] ⟩ (reverse ys ++ ((reverse xs) ++ [ x ])) ≡⟨⟩ (reverse ys ++ reverse (x ∷ xs)) ∎ reverse-involutive : {A : Set} (xs : List A) -> reverse (reverse xs) ≡ xsreverse-involutive [] = reflreverse-involutive (x ∷ xs) = begin reverse (reverse (x ∷ xs)) ≡⟨⟩ reverse (reverse xs ++ [ x ]) ≡⟨ reverse-++-distrib (reverse xs) [ x ] ⟩ reverse [ x ] ++ reverse (reverse xs) ≡⟨⟩ x ∷ reverse (reverse xs) ≡⟨ cong (x ∷_) (reverse-involutive xs) ⟩ (x ∷ xs) ∎Because of how we defined the lists constructors and ++, the above definition of reverse is not performant (even though it is correct). The reason is that appending an element at the end of the list involves reconstructing the entire list. And reverse is doing this for each element in the list.
Therefore, we define a helper function shunt that takes a list xs and an accumulator moves the first element (x) from the list to the beginning of the accumulator and passes the lists recursively to itself. Think of this as popping all the elements from one stack and pushing them to another - the result is that we've reversed the original stack.
We prove that shunt xs acc reverses xs and concatenates it with acc. We also define a new reverse' function based on shunt, and show that it is the same as the original reverse function.
shunt : ∀ {A : Set} → List A → List A → List Ashunt [] acc = accshunt (x ∷ xs) acc = shunt xs (x ∷ acc)-- reverse [1, 3, 5, 7] = shunt [1, 3, 5, 7] [] = shunt [3, 5, 7] [1] = shunt [5, 7] [3, 1] = -- shunt [7] [5, 3, 1] = shunt [] [7, 5, 3, 1] = [7, 5, 3, 1]-- shunt [1, 3, 5, 7] [2, 4] = shunt [3, 5, 7] [1, 2, 4] = ... = [7, 5, 3, 1, 2, 4]shunt-reverse : ∀ {A : Set} (xs acc : List A) → shunt xs acc ≡ reverse xs ++ accshunt-reverse [] acc = reflshunt-reverse (x ∷ xs) acc = begin shunt (x ∷ xs) acc ≡⟨⟩ shunt xs (x ∷ acc) -- reverse xs ++ (x ∷ ys) ≡⟨ shunt-reverse xs (x ∷ acc) ⟩ (reverse xs ++ (x ∷ acc)) ≡⟨⟩ (reverse xs ++ ([ x ] ++ acc)) ≡⟨ sym (++-assoc (reverse xs) [ x ] acc) ⟩ ((reverse xs ++ [ x ]) ++ acc) ≡⟨⟩ (reverse (x ∷ xs) ++ acc) ∎reverse' : ∀ {A : Set} → List A → List Areverse' xs = shunt xs []reverses : ∀ {A : Set} (xs : List A) → reverse' xs ≡ reverse xsreverses xs = begin reverse' xs ≡⟨⟩ shunt xs [] ≡⟨ shunt-reverse xs [] ⟩ reverse xs ++ [] ≡⟨ ++-identity-r (reverse xs) ⟩ reverse xs ∎Map
We define a map over lists and show that it distributes over function composition, and that mapping the identity function over a list is itself the identity function.
map : ∀ {A B : Set} → (A → B) → List A → List Bmap f [] = []map f (x ∷ xs) = f x ∷ map f xs_ : map suc [ 0 $ 1 $ 2 ] ≡ [ 1 $ 2 $ 3 ]_ = reflsucs : List ℕ → List ℕsucs = map suc_ : sucs [ 0 $ 1 $ 2 ] ≡ [ 1 $ 2 $ 3 ]_ = reflpostulate extensionality-non-dep : {A B : Set} {f g : A -> B} -> ((x : A) -> f x ≡ g x) -> f ≡ g extensionality : {A : Set} {B : A -> Set } {f g : (x : A) -> B x} -> ((x : A) -> f x ≡ g x) -> f ≡ gh-app : {A : Set} {B : A -> Set } {f g : (x : A) -> B x} -> f ≡ g -> ((x : A) -> f x ≡ g x)h-app refl x = reflopen import Function using (_∘_)map-compose-xs :{A B C : Set} (f : A -> B) -> (g : B -> C) -> (xs : List A) -> map (g ∘ f) xs ≡ (map g ∘ map f) xsmap-compose-xs f g [] = reflmap-compose-xs f g (x ∷ xs) = begin g (f x) ∷ map (λ z → g (f z)) xs ≡⟨ cong (g (f x) ∷_ ) (map-compose-xs f g xs) ⟩ g (f x) ∷ map g (map f xs) ∎map-compose : {A B C : Set} (f : A -> B) -> (g : B -> C) -> map (g ∘ f) ≡ map g ∘ map fmap-compose f g = extensionality-non-dep (map-compose-xs f g)-- map f (xs ++ ys) ≡ map f xs ++ map f ysid : {A : Set} -> A -> Aid x = xmap-id-xs : {A : Set} (xs : List A) -> map id xs ≡ xsmap-id-xs [] = reflmap-id-xs (x ∷ xs) = cong (x ∷_) (map-id-xs xs) map-id : {A : Set} -> map id ≡ id {List A}map-id = extensionality-non-dep map-id-xsWe define a new data type Tree and give as an exercise to define a function map-tree.
data BinaryTree (A : Set) : Set where leaf : A → BinaryTree A node : BinaryTree A → BinaryTree A → BinaryTree A-- F is a functor iff we can implement such a function-- map (A -> B) (F A) -> F B-- which respects composition and identitydata Tree (A B : Set) : Set where leaf : A → Tree A B node : Tree A B → B → Tree A B → Tree A B-- map-Tree : ∀ {A B C D : Set} → (A → C) → (B → D) → Tree A B → Tree C DFolds
When defining functions on lists we often pattern match on the two constructors, the empty list and (x ∷ xs) . For the latter case, we'd do something with x and then another action, usually a recursive call, on the rest of the list xs.
Folds are examples of higher-order functions which generalises this idea. While both map and folds traverse through a list, the latter returns a single value. A fold takes an operator and a value, and uses the given operator to combine (or fold) the items of a list to a single value which is returned as the result of the empty list.
foldr : ∀ {A B : Set} → (A → B → B) → B → List A → Bfoldr _⊗_ e [] = efoldr _⊗_ e (x ∷ xs) = x ⊗ foldr _⊗_ e xsThe right fold foldr above folds the list up from the right side. Note that the starting value inline_formula not implemented is sometimes referred to as the accumulator. We will define the corresponding left fold later.
As an example we can redefine sum, which sums all the natural numbers in a list, to use foldr instead.
sum : List ℕ → ℕsum [] = 0sum (x ∷ xs) = x + sum xssum' : List ℕ → ℕsum' = foldr _+_ 0{-_ : sum [ 1 , 2 , 3 ] ≡ sum' [ 1 , 2 , 3 ]_ = refl-}Similarly, we can define the product of a list of numbers with inline_formula not implemented as the accumulator.
product : List ℕ → ℕproduct = foldr _*_ 1Lemma. foldr on ++ can be split into two consecutive folds, one for each of the lists.
foldr-++ : ∀ {A B : Set} (_⊗_ : A → B → B) → (e : B) → (xs ys : List A) →---------------------------------------------------------------- ((foldr _⊗_ e (xs ++ ys)) ≡ (foldr _⊗_ (foldr _⊗_ e ys) xs))foldr-++ _⊗_ e [] ys = reflfoldr-++ _⊗_ e (x ∷ xs) ys = begin foldr _⊗_ e ((x ∷ xs) ++ ys) ≡⟨⟩ foldr _⊗_ e (x ∷ (xs ++ ys)) ≡⟨⟩ (x ⊗ foldr _⊗_ e (xs ++ ys)) ≡⟨ cong (_⊗_ x) (foldr-++ _⊗_ e xs ys) ⟩ (x ⊗ foldr _⊗_ (foldr _⊗_ e ys) xs) ≡⟨⟩ foldr _⊗_ (foldr _⊗_ e ys) (x ∷ xs) ∎Lemma. foldr with cons and the empty list acts like an identity on lists.
foldr-∷ : ∀ {A : Set} (xs : List A) → foldr _∷_ [] xs ≡ xsfoldr-∷ [] = reflfoldr-∷ (x ∷ xs) = begin foldr _∷_ [] (x ∷ xs) ≡⟨⟩ x ∷ foldr _∷_ [] xs ≡⟨ cong (x ∷_) (foldr-∷ xs) ⟩ (x ∷ xs) ∎Corollary. ++ can be expressed as a fold.
foldr-∷++ : ∀ {A : Set} (xs ys : List A) → xs ++ ys ≡ foldr _∷_ ys xsfoldr-∷++ [] ys = reflfoldr-∷++ (x ∷ xs) ys = begin (x ∷ xs) ++ ys ≡⟨⟩ x ∷ (xs ++ ys) ≡⟨ cong (x ∷_) (foldr-∷++ xs ys) ⟩ x ∷ foldr _∷_ ys xs ≡⟨⟩ foldr _∷_ ys (x ∷ xs) ∎Lemma. map is just a fold
map-is-fold : ∀ {A B : Set} (xs : List A) → (f : A → B) → map f xs ≡ foldr (λ y ys → f y ∷ ys) [] xs map-is-fold [] f = reflmap-is-fold (x ∷ xs) f = begin map f (x ∷ xs) ≡⟨⟩ f x ∷ map f xs ≡⟨ cong ((f x ∷_)) (map-is-fold xs f) ⟩ f x ∷ foldr (λ y ys → f y ∷ ys) [] xs ≡⟨⟩ foldr (λ y ys → f y ∷ ys) [] (x ∷ xs) ∎Lemma. (Fusion-fold theorem).
fusion-fold-theorem : ∀ {A B C : Set} → (f : A → B → B) → (g : A → C → C) → (h : B → C) → {x : A} {y : B} → h (f x y) ≡ g x (h y) --------------------------------- → (e : B) → ∀ xs → (h (foldr f e xs)) ≡ foldr g (h e) xsSketch of the proof. We can work with a slightly different version, but equivalent, of our functions inline_formula not implemented and inline_formula not implemented. Now, we have inline_formula not implemented and inline_formula not implemented. This theorem states that whenever we have the diagram below commuting, we can prove the equality
formula not implementedObserve that the main assumption corresponds to the following diagrams.
We therefore can prove our goal by expanding the fold function definition to see what we really need to show. One can see the hypothesis shows up just after. In the diagram below, one can see the idea. The case is only with an input list inline_formula not implemented of two elements inline_formula not implemented, but the general case follows easily.
fusion-fold-theorem = ? -- Here it goes the proof.Just wonder now if this theorem can be helpful to prove the previous lemmas.
Monoids
We can define a monoidal structure on types as well, i.e. an associative binary operation together with a value, called unit, that acts both as a left and right identity for the given operation.
record IsMonoid {A : Set} (_⊗_ : A → A → A) (e : A) : Set where field assoc : ∀ (x y z : A) → (x ⊗ y) ⊗ z ≡ x ⊗ (y ⊗ z) identityˡ : ∀ (x : A) → e ⊗ x ≡ x identityʳ : ∀ (x : A) → x ⊗ e ≡ xopen IsMonoidSome well known examples of monoids include the natural numbers with addition or multiplication. We have also shown that ++ is associative and that the empty list acts like a unit wrt. ++, and thus, we get a monoidal structure for lists as well..
+-monoid : IsMonoid _+_ 0+-monoid = record { assoc = +-assoc ; identityˡ = +-identityˡ ; identityʳ = +-identityʳ }*-monoid : IsMonoid _*_ 1*-monoid = record { assoc = *-assoc ; identityˡ = *-identityˡ ; identityʳ = *-identityʳ }++-monoid : ∀ {A : Set} → IsMonoid {List A} _++_ []++-monoid = record { assoc = ++-assoc ; identityˡ = ++-identityˡ ; identityʳ = ++-identityʳ }Lemma. If _⊗_ and e forms a monoid, then any foldr can be re-expressed with e as the accumulator.
foldr-monoid : ∀ {A : Set} (_⊗_ : A → A → A) (e : A) → IsMonoid _⊗_ e → ∀ (xs : List A) (y : A) → ---------------------------------------- foldr _⊗_ y xs ≡ foldr _⊗_ e xs ⊗ yfoldr-monoid _⊗_ e monoid [] y = sym (identityˡ monoid y)foldr-monoid _⊗_ e monoid (x ∷ xs) y = begin foldr _⊗_ y (x ∷ xs) ≡⟨⟩ x ⊗ (foldr _⊗_ y xs) ≡⟨ cong (x ⊗_) (foldr-monoid _⊗_ e monoid xs y) ⟩ x ⊗ (foldr _⊗_ e xs ⊗ y) ≡⟨ sym (assoc monoid x (foldr _⊗_ e xs) y) ⟩ (x ⊗ foldr _⊗_ e xs) ⊗ y ≡⟨⟩ foldr _⊗_ e (x ∷ xs) ⊗ y ∎Lemma. If _⊗_ and e forms a monoid, then a foldr on ++ can be split into ⊗ of two folds, one for each of the lists.
foldr-monoid-++ : ∀ {A : Set} (_⊗_ : A → A → A) (e : A) → IsMonoid _⊗_ e → ∀ (xs ys : List A) → --------------------------------------- foldr _⊗_ e (xs ++ ys) ≡ foldr _⊗_ e xs ⊗ foldr _⊗_ e ys foldr-monoid-++ _⊗_ e monoid [] ys = sym (identityˡ monoid (foldr _⊗_ e ys))foldr-monoid-++ _⊗_ e monoid (x ∷ xs) ys = begin x ⊗ foldr _⊗_ e (xs ++ ys) ≡⟨ cong (x ⊗_) (foldr-++ _⊗_ e xs ys) ⟩ x ⊗ (foldr _⊗_ (foldr _⊗_ e ys) xs) ≡⟨ cong (x ⊗_) (foldr-monoid _⊗_ e monoid xs (foldr _⊗_ e ys)) ⟩ x ⊗ (foldr _⊗_ e xs ⊗ (foldr _⊗_ e ys)) ≡⟨ sym (assoc monoid x (foldr _⊗_ e xs) (foldr _⊗_ e ys)) ⟩ (x ⊗ foldr _⊗_ e xs) ⊗ foldr _⊗_ e ys ∎Let's define the left fold!
foldl : ∀ {A B : Set} → (B → A → B) → B → List A → Bfoldl _⊗_ e [] = efoldl _⊗_ e (x ∷ xs) = foldl _⊗_ (e ⊗ x) xsLemma. If _⊗_ and e forms a monoid, then any foldl can be re-expressed.
foldl-monoid : ∀ {A : Set} (_⊗_ : A → A → A) (e : A) → IsMonoid _⊗_ e → ∀ (xs : List A) (y : A) → ---------------------------------------- foldl _⊗_ y xs ≡ y ⊗ foldl _⊗_ e xsfoldl-monoid _⊗_ e monoid [] y = sym (identityʳ monoid y)foldl-monoid _⊗_ e monoid (x ∷ xs) y = begin foldl _⊗_ y (x ∷ xs) ≡⟨⟩ foldl _⊗_ (y ⊗ x) xs ≡⟨ foldl-monoid _⊗_ e monoid xs (y ⊗ x) ⟩ (y ⊗ x) ⊗ foldl _⊗_ e xs ≡⟨ assoc monoid y x (foldl _⊗_ e xs) ⟩ y ⊗ (x ⊗ foldl _⊗_ e xs) ≡⟨ cong (y ⊗_) (sym (foldl-monoid _⊗_ e monoid xs x)) ⟩ y ⊗ foldl _⊗_ x xs ≡⟨ cong (λ z → y ⊗ foldl _⊗_ z xs) (sym (identityˡ monoid x)) ⟩ y ⊗ foldl _⊗_ (e ⊗ x) xs ≡⟨⟩ y ⊗ foldl _⊗_ e (x ∷ xs) ∎Theorem. foldl and foldr are computationally equal for monoids.
foldr-monoid-foldl : ∀ {A : Set} (_⊗_ : A → A → A) (e : A) → IsMonoid _⊗_ e → ∀ (xs : List A) → ----------------------------------- foldr _⊗_ e xs ≡ foldl _⊗_ e xsfoldr-monoid-foldl _⊗_ e monoid [] = reflfoldr-monoid-foldl _⊗_ e monoid (x ∷ xs) = begin foldr _⊗_ e (x ∷ xs) ≡⟨⟩ x ⊗ foldr _⊗_ e xs ≡⟨ cong (x ⊗_) (foldr-monoid-foldl _⊗_ e monoid xs) ⟩ x ⊗ foldl _⊗_ e xs ≡⟨ sym (foldl-monoid _⊗_ e monoid xs x) ⟩ foldl _⊗_ x xs ≡⟨ cong (λ z → foldl _⊗_ z xs) (sym (identityˡ monoid x)) ⟩ foldl _⊗_ (e ⊗ x) xs ≡⟨⟩ foldl _⊗_ e (x ∷ xs) ∎