michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fixed conflicts

Browse source
This commit is contained in:
wadler 2018-06-10 21:31:37 -03:00
commit ecde68df1e
21 changed files with 207 additions and 162 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

36
index.md
View file

@ -18,38 +18,38 @@ fixes are encouraged.
## Front matter
- [Preface]({{ site.baseurl }}{% link out/Preface.md %})
- [Preface]({{ site.baseurl }}{% link out/plta/Preface.md %})
## Part 1: Logical Foundations
(This part is ready for review. Please comment!)
- [Naturals: Natural numbers]({{ site.baseurl }}{% link out/Naturals.md %})
- [Naturals: Natural numbers]({{ site.baseurl }}{% link out/plta/Naturals.md %})
- [Properties: Proof by induction](Properties)
- [Relations: Inductive definition of relations]({{ site.baseurl }}{% link out/Relations.md %})
- [Equality: Equality and equational reasoning]({{ site.baseurl }}{% link out/Equality.md %})
- [Isomorphism: Isomorphism and embedding]({{ site.baseurl }}{% link out/Isomorphism.md %})
- [Connectives: Conjunction, disjunction, and implication]({{ site.baseurl }}{% link out/Connectives.md %})
- [Negation: Negation, with intuitionistic and classical Logic]({{ site.baseurl }}{% link out/Negation.md %})
- [Quantifiers: Universals and existentials]({{ site.baseurl }}{% link out/Quantifiers.md %})
- [Lists: Lists and higher-order functions]({{ site.baseurl }}{% link out/Lists.md %})
- [Decidable: Booleans and decision procedures]({{ site.baseurl }}{% link out/Decidable.md %})
- [Relations: Inductive definition of relations]({{ site.baseurl }}{% link out/plta/Relations.md %})
- [Equality: Equality and equational reasoning]({{ site.baseurl }}{% link out/plta/Equality.md %})
- [Isomorphism: Isomorphism and embedding]({{ site.baseurl }}{% link out/plta/Isomorphism.md %})
- [Connectives: Conjunction, disjunction, and implication]({{ site.baseurl }}{% link out/plta/Connectives.md %})
- [Negation: Negation, with intuitionistic and classical Logic]({{ site.baseurl }}{% link out/plta/Negation.md %})
- [Quantifiers: Universals and existentials]({{ site.baseurl }}{% link out/plta/Quantifiers.md %})
- [Lists: Lists and higher-order functions]({{ site.baseurl }}{% link out/plta/Lists.md %})
- [Decidable: Booleans and decision procedures]({{ site.baseurl }}{% link out/plta/Decidable.md %})
## Part 2: Programming Language Foundations
(This part is not yet ready for review.)
- [Lambda: Lambda: Introduction to Lambda Calculus]({{ site.baseurl }}{% link out/Lambda.md %})
- [LambdaProp: Properties of Simply-Typed Lambda Calculus]({{ site.baseurl }}{% link out/LambdaProp.md %})
- [DeBruijn: Inherently typed De Bruijn representation]({{ site.baseurl }}{% link out/DeBruijn.md %})
- [Extensions: Extensions to simply-typed lambda calculus]({{ site.baseurl }}{% link out/Extensions.md %})
- [Inference: Bidirectional type inference]({{ site.baseurl }}{% link out/Inference.md %})
- [Untyped: Untyped lambda calculus with full normalisation]({{ site.baseurl }}{% link out/Untyped.md %})
- [Lambda: Lambda: Introduction to Lambda Calculus]({{ site.baseurl }}{% link out/plta/Lambda.md %})
- [LambdaProp: Properties of Simply-Typed Lambda Calculus]({{ site.baseurl }}{% link out/plta/LambdaProp.md %})
- [DeBruijn: Inherently typed De Bruijn representation]({{ site.baseurl }}{% link out/plta/DeBruijn.md %})
- [Extensions: Extensions to simply-typed lambda calculus]({{ site.baseurl }}{% link out/plta/Extensions.md %})
- [Inference: Bidirectional type inference]({{ site.baseurl }}{% link out/plta/Inference.md %})
- [Untyped: Untyped lambda calculus with full normalisation]({{ site.baseurl }}{% link out/plta/Untyped.md %})
## Backmatter
- [Acknowledgements]({{ site.baseurl }}{% link out/Acknowledgements.md %})
- [Fonts: Test page for fonts]({{ site.baseurl }}{% link out/Fonts.md %})
- [Acknowledgements]({{ site.baseurl }}{% link out/plta/Acknowledgements.md %})
- [Fonts: Test page for fonts]({{ site.baseurl }}{% link out/plta/Fonts.md %})
[sf]: https://softwarefoundations.cis.upenn.edu/
[wen]: https://github.com/wenkokke

4
src/Acknowledgements.lagda → src/plta/Acknowledgements.lagda
View file

@ -4,6 +4,10 @@ layout : page
permalink : /Acknowledgements/
---
\begin{code}
module plta.Acknowledgements where
\end{code}
Thank you to the following.
To the inventors of Agda, for giving us a new playground.

33
src/Connectives.lagda → src/plta/Connectives.lagda
View file

@ -4,6 +4,10 @@ layout : page
permalink : /Connectives/
---
\begin{code}
module plta.Connectives where
\end{code}
This chapter introduces the basic logical connectives, by observing
a correspondence between connectives of logic and data types,
a principle known as *Propositions as Types*.
@ -21,8 +25,8 @@ a principle known as *Propositions as Types*.
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong)
open Eq.≡-Reasoning
open import Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_)
open Isomorphism.≃-Reasoning
open import plta.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_)
open plta.Isomorphism.≃-Reasoning
open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
open import Data.Nat.Properties.Simple using (+-suc)
open import Function using (_∘_)
@ -53,7 +57,7 @@ the pair constructor is `_,_`, but here we rename it to
`⟨_,_⟩` so that comma is available for other notations
(in particular, lists and environments).
<!--
<!--
By convention, we parenthesise pairs, even though `M , N` is also
accepted by Agda.
-->
@ -174,10 +178,10 @@ and similarly for `to∘from`, which does the same (up to renaming).
×-comm =
record
{ to = λ{ ⟨ x , y ⟩ → ⟨ y , x ⟩ }
; from = λ{ ⟨ y , x ⟩ → ⟨ x , y ⟩ }
; from = λ{ ⟨ y , x ⟩ → ⟨ x , y ⟩ }
; from∘to = λ{ ⟨ x , y ⟩ → refl }
; to∘from = λ{ ⟨ y , x ⟩ → refl }
}
}
\end{code}
Being *commutative* is different from being *commutative up to
@ -206,7 +210,7 @@ matching against a suitable pattern to enable simplification.
; from = λ{ ⟨ x , ⟨ y , z ⟩ ⟩ → ⟨ ⟨ x , y ⟩ , z ⟩ }
; from∘to = λ{ ⟨ ⟨ x , y ⟩ , z ⟩ → refl }
; to∘from = λ{ ⟨ x , ⟨ y , z ⟩ ⟩ → refl }
}
}
\end{code}
Being *associative* is not the same as being *associative
@ -438,7 +442,7 @@ matching against a suitable pattern to enable simplification.
; to∘from = λ{ (inj₁ x) → refl
; (inj₂ (inj₁ y)) → refl
; (inj₂ (inj₂ z)) → refl
}
}
}
\end{code}
@ -527,7 +531,7 @@ isomorphism between the two types. For instance, `inj₂ true`, which is
a member of the former, corresponds to `true`, which is a member of
the latter.
Right identity follows from commutativity of sum and left identity.
Right identity follows from commutativity of sum and left identity.
\begin{code}
⊥-identityʳ : ∀ {A : Set} → (A ⊎ ⊥) ≃ A
⊥-identityʳ {A} =
@ -614,14 +618,14 @@ arguments of the type `Bool → Tri`:
→-count : (Bool → Tri) → ℕ
→-count f with f true | f false
... | aa | aa = 1
... | aa | bb = 2
... | aa | bb = 2
... | aa | cc = 3
... | bb | aa = 4
... | bb | bb = 5
... | bb | cc = 6
... | cc | aa = 7
... | cc | bb = 8
... | cc | cc = 9
... | cc | cc = 9
\end{code}
Exponential on types also share a property with exponential on
@ -719,7 +723,7 @@ this fact is similar in structure to our previous results.
×-distrib-⊎ : ∀ {A B C : Set} → (A ⊎ B) × C ≃ (A × C) ⊎ (B × C)
×-distrib-⊎ =
record
{ to = λ{ ⟨ inj₁ x , z ⟩ → (inj₁ ⟨ x , z ⟩)
{ to = λ{ ⟨ inj₁ x , z ⟩ → (inj₁ ⟨ x , z ⟩)
; ⟨ inj₂ y , z ⟩ → (inj₂ ⟨ y , z ⟩)
}
; from = λ{ (inj₁ ⟨ x , z ⟩) → ⟨ inj₁ x , z ⟩
@ -730,7 +734,7 @@ this fact is similar in structure to our previous results.
}
; to∘from = λ{ (inj₁ ⟨ x , z ⟩) → refl
; (inj₂ ⟨ y , z ⟩) → refl
}
}
}
\end{code}
@ -741,14 +745,14 @@ Sums do not distribute over products up to isomorphism, but it is an embedding.
record
{ to = λ{ (inj₁ ⟨ x , y ⟩) → ⟨ inj₁ x , inj₁ y ⟩
; (inj₂ z) → ⟨ inj₂ z , inj₂ z ⟩
}
}
; from = λ{ ⟨ inj₁ x , inj₁ y ⟩ → (inj₁ ⟨ x , y ⟩)
; ⟨ inj₁ x , inj₂ z ⟩ → (inj₂ z)
; ⟨ inj₂ z , _ ⟩ → (inj₂ z)
}
; from∘to = λ{ (inj₁ ⟨ x , y ⟩) → refl
; (inj₂ z) → refl
}
}
}
\end{code}
Note that there is a choice in how we write the `from` function.
@ -820,4 +824,3 @@ This chapter uses the following unicode.
₁ U+2081 SUBSCRIPT ONE (\_1)
₂ U+2082 SUBSCRIPT TWO (\_2)
⇔ U+21D4 LEFT RIGHT DOUBLE ARROW (\<=>)

14
src/DeBruijn.lagda → src/plta/DeBruijn.lagda
View file

@ -4,12 +4,12 @@ layout : page
permalink : /DeBruijn/
---
## Imports
\begin{code}
module DeBruijn where
module plta.DeBruijn where
\end{code}
## Imports
\begin{code}
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong)
@ -198,7 +198,7 @@ _[_] {Γ} {A} N M = subst {Γ , A} {Γ} ρ N
\begin{code}
data Value : ∀ {Γ A} → Γ ⊢ A → Set where
Zero : ∀ {Γ} →
Zero : ∀ {Γ} →
-----------------
Value (`zero {Γ})
@ -206,7 +206,7 @@ data Value : ∀ {Γ A} → Γ ⊢ A → Set where
→ Value V
--------------
→ Value (`suc V)
Fun : ∀ {Γ A B} {N : Γ , A ⊢ B}
---------------------------
→ Value (ƛ N)
@ -288,7 +288,7 @@ The second has two values of function type, both lambda abstractions and fixpoin
(μ f → μ g → N) · V
⟶ (μ f → μ g → N′) · V
⟶ (μ f → μ g → λ x → N″) · V
⟶ (μ f → μ g → λ x → N″) · V
⟶ (μ g → λ x → N″) [ f := μ f → μ g → λ x → N″ ] · V
⟶ (μ g → λ x → N″ [ f := μ f → μ g → λ x → N″ ]) · V
⟶ (λ x → N″ [ f := μ f → μ g → λ x → N″ ])
@ -476,5 +476,3 @@ normalise (suc g) L with progress L
... | step {M} L⟶M with normalise g M
... | normal h M⟶*N = normal (suc h) (L ⟶⟨ L⟶M ⟩ M⟶*N)
\end{code}

9
src/Decidable.lagda → src/plta/Decidable.lagda
View file

@ -4,6 +4,10 @@ layout : page
permalink : /Decidable/
---
\begin{code}
module plta.Decidable where
\end{code}
We have a choice as to how to represent relations:
as an inductive data type of *evidence* that the relation holds,
or as a function that *computes* whether the relation holds.
@ -115,7 +119,7 @@ and the one use of `()` when showing there can be no evidence that `4 ≤ 2`.
We would hope to be able to show these two approaches are related, and
indeed we can. First, we define a function that lets us map from the
computation world to the evidence world.
computation world to the evidence world.
\begin{code}
T : Bool → Set
T true = ⊤
@ -149,7 +153,7 @@ hence `T b` is inhabited by `tt`.
Now we can show that `T (m ≤ᵇ n)` is inhabited exactly when `m ≤ n` is inhabited.
In the forward direction, we consider the three clauses in the definition
of `_≤ᵇ_`.
of `_≤ᵇ_`.
\begin{code}
≤ᵇ→≤ : ∀ (m n : ℕ) → T (m ≤ᵇ n) → m ≤ n
≤ᵇ→≤ zero n tt = z≤n
@ -563,4 +567,3 @@ import Relation.Nullary.Sum using (_⊎-dec_)
## Unicode
ᵇ U+1D47 MODIFIER LETTER SMALL B (\^b)

6
src/Equality.lagda → src/plta/Equality.lagda
View file

@ -4,6 +4,10 @@ layout : page
permalink : /Equality/
---
\begin{code}
module plta.Equality where
\end{code}
Much of our reasoning has involved equality. Given two terms `M`
and `N`, both of type `A`, we write `M ≡ N` to assert that `M` and `N`
are interchangeable. So far we have treated equality as a primitive,
@ -409,7 +413,7 @@ convenient in much of what follows.
A term of the form
λ{ P₁ → N₁; ⋯ ; Pᵢ → Nᵢ }
is equivalent to a function `f` defined by the equations
f P₁ = e₁

25
src/Extensions.lagda → src/plta/Extensions.lagda
View file

@ -4,12 +4,13 @@ layout : page
permalink : /Extensions/
---
## Imports
\begin{code}
module Extensions where
module plta.Extensions where
\end{code}
## Imports
\begin{code}
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong)
@ -144,7 +145,7 @@ data _⊢_ : Env → Type → Set where
`case⊥ : ∀ {Γ A}
→ Γ ⊢ `⊥
-------
→ Γ ⊢ A
→ Γ ⊢ A
`[] : ∀ {Γ A}
------------
@ -204,7 +205,7 @@ rename σ (`case⊥ L) = `case⊥ (rename σ L)
rename σ `[] = `[]
rename σ (M `∷ N) = (rename σ M) `∷ (rename σ N)
rename σ (`caseL L M N) = `caseL (rename σ L) (rename σ M) (rename (ext (ext σ)) N)
rename σ (`let M N) = `let (rename σ M) (rename (ext σ) N)
rename σ (`let M N) = `let (rename σ M) (rename (ext σ) N)
\end{code}
## Substitution
@ -233,7 +234,7 @@ subst ρ (`case⊥ L) = `case⊥ (subst ρ L)
subst ρ `[] = `[]
subst ρ (M `∷ N) = (subst ρ M) `∷ (subst ρ N)
subst ρ (`caseL L M N) = `caseL (subst ρ L) (subst ρ M) (subst (exts (exts ρ)) N)
subst ρ (`let M N) = `let (subst ρ M) (subst (exts ρ) N)
subst ρ (`let M N) = `let (subst ρ M) (subst (exts ρ) N)
_[_] : ∀ {Γ A B}
→ Γ , A ⊢ B
@ -265,7 +266,7 @@ _[_][_] {Γ} {A} {B} N V W = subst {Γ , A , B} {Γ} ρ N
\begin{code}
data Value : ∀ {Γ A} → Γ ⊢ A → Set where
Zero : ∀ {Γ} →
Zero : ∀ {Γ} →
-----------------
Value (`zero {Γ})
@ -273,7 +274,7 @@ data Value : ∀ {Γ A} → Γ ⊢ A → Set where
→ Value V
--------------
→ Value (`suc V)
Fun : ∀ {Γ A B} {N : Γ , A ⊢ B}
---------------------------
→ Value (ƛ N)
@ -409,7 +410,7 @@ data _⟶_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
β-⊎₁ : ∀ {Γ A B C} {V : Γ ⊢ A} {M : Γ , A ⊢ C} {N : Γ , B ⊢ C}
→ Value V
---------------------------------
→ `case⊎ (`inj₁ V) M N ⟶ M [ V ]
→ `case⊎ (`inj₁ V) M N ⟶ M [ V ]
β-⊎₂ : ∀ {Γ A B C} {W : Γ ⊢ B} {M : Γ , A ⊢ C} {N : Γ , B ⊢ C}
→ Value W
@ -447,7 +448,7 @@ data _⟶_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
→ Value W
-------------------------------------
→ `caseL (V `∷ W) M N ⟶ N [ V ][ W ]
ξ-let : ∀ {Γ A B} {M M′ : Γ ⊢ A} {N : Γ , A ⊢ B}
→ M ⟶ M′
-----------------------
@ -456,7 +457,7 @@ data _⟶_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
β-let : ∀ {Γ A B} {V : Γ ⊢ A} {N : Γ , A ⊢ B}
→ Value V
---------------------
→ `let V N ⟶ N [ V ]
→ `let V N ⟶ N [ V ]
\end{code}
## Reflexive and transitive closure
@ -600,5 +601,3 @@ normalise (suc g) L with progress L
... | step {M} L⟶M with normalise g M
... | normal h M⟶*N = normal (suc h) (L ⟶⟨ L⟶M ⟩ M⟶*N)
\end{code}

7
src/Fonts.lagda → src/plta/Fonts.lagda
View file

@ -4,6 +4,10 @@ layout : page
permalink : /Fonts/
---
\begin{code}
module plta.Fonts where
\end{code}
Test page for fonts.
Agda:
@ -31,7 +35,7 @@ ABCDEFGHIJKLMNOPQRSTUVWXYZ
⌊⌋⌈⌉
----
-}
\end{code}
\end{code}
Indented code:
@ -55,4 +59,3 @@ Indented code:
------------
⌊⌋⌈⌉
----

30
src/Inference.lagda → src/plta/Inference.lagda
View file

@ -4,12 +4,13 @@ layout : page
permalink : /Inference/
---
## Imports
\begin{code}
module Inference where
module plta.Inference where
\end{code}
## Imports
\begin{code}
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong; cong₂; _≢_)
@ -24,8 +25,7 @@ open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Function using (_∘_)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Relation.Nullary.Negation using (¬?)
open import DeBruijn using (Type; `ℕ; _⇒_)
import DeBruijn as DB
open import plta.DeBruijn as DB using (Type; `ℕ; _⇒_)
pattern [_] w = w ∷ []
pattern [_,_] w x = w ∷ x ∷ []
@ -61,7 +61,7 @@ data Ctx : Set where
Terms that synthesize `Term⁺` and inherit `Term⁻` their types.
\begin{code}
data Term⁺ : Set
data Term⁺ : Set
data Term⁻ : Set
data Term⁺ where
@ -225,7 +225,7 @@ lookup (Γ , x ⦂ A) w with w ≟ x
do ⟨ A , ⊢x ⟩ ← lookup Γ w
return ⟨ A , S w≢ ⊢x ⟩
\end{code}
## Synthesize and inherit types
\begin{code}
@ -368,15 +368,15 @@ _ = refl
_ : synthesize ε (twoCh ↓ `ℕ) ≡
error⁻ "lambda cannot be of type natural"
(ƛ "s" ⇒ (ƛ "z" ⇒ ⌊ "s" ⌋ · (⌊ "s" ⌋ · (⌊ "z" ⌋ ↑) ↑) ↑)) []
_ = refl
_ = refl
_ : synthesize ε (`zero ↓ `ℕ ⇒ `ℕ) ≡
error⁻ "zero cannot be function" `zero [ `ℕ ⇒ `ℕ ]
_ = refl
_ = refl
_ : synthesize ε (two ↓ `ℕ ⇒ `ℕ) ≡
error⁻ "suc cannot be function" (`suc (`suc `zero)) [ `ℕ ⇒ `ℕ ]
_ = refl
_ = refl
_ : synthesize ε
((`case (twoCh ↓ Ch) [zero⇒ `zero |suc "x" ⇒ ⌊ "x" ⌋ ↑ ] ↓ `ℕ) ) ≡
@ -384,11 +384,11 @@ _ : synthesize ε
`case (ƛ "s" ⇒ (ƛ "z" ⇒ ⌊ "s" ⌋ · (⌊ "s" ⌋ · (⌊ "z" ⌋ ↑) ↑) ↑))
↓ (`ℕ ⇒ `ℕ) ⇒ `ℕ ⇒ `ℕ [zero⇒ `zero |suc "x" ⇒ ⌊ "x" ⌋ ↑ ]
[ (`ℕ ⇒ `ℕ) ⇒ `ℕ ⇒ `ℕ ]
_ = refl
_ = refl
_ : synthesize ε (((ƛ "x" ⇒ ⌊ "x" ⌋ ↑) ↓ `ℕ ⇒ (`ℕ ⇒ `ℕ))) ≡
error⁺ "inheritance and synthesis conflict" ⌊ "x" ⌋ [ `ℕ , `ℕ ⇒ `ℕ ]
_ = refl
_ = refl
\end{code}
## Erasure
@ -405,8 +405,8 @@ _ = refl
∥_∥⁺ : ∀ {Γ M A} → Γ ⊢ M ↑ A → ∥ Γ ∥Γ DB.⊢ A
∥_∥⁻ : ∀ {Γ M A} → Γ ⊢ M ↓ A → ∥ Γ ∥Γ DB.⊢ A
∥ Ax ⊢x ∥⁺ = DB.⌊ ∥ ⊢x ∥∋ ⌋
∥ ⊢L · ⊢M ∥⁺ = ∥ ⊢L ∥⁺ DB.· ∥ ⊢M ∥⁻
∥ Ax ⊢x ∥⁺ = DB.⌊ ∥ ⊢x ∥∋ ⌋
∥ ⊢L · ⊢M ∥⁺ = ∥ ⊢L ∥⁺ DB.· ∥ ⊢M ∥⁻
∥ ⊢↓ ⊢M ∥⁺ = ∥ ⊢M ∥⁻
∥ ⊢λ ⊢N ∥⁻ = DB.ƛ ∥ ⊢N ∥⁻
@ -426,5 +426,3 @@ _ = refl
_ : ∥ ⊢fourCh ∥⁺ ≡ DB.fourCh′
_ = refl
\end{code}

16
src/Isomorphism.lagda → src/plta/Isomorphism.lagda
View file

@ -4,6 +4,10 @@ layout : page
permalink : /Isomorphism/
---
\begin{code}
module plta.Isomorphism where
\end{code}
This section introduces isomorphism as a way of asserting that two
types are equal, and embedding as a way of asserting that one type is
smaller than another. We apply isomorphisms in the next chapter
@ -42,7 +46,7 @@ record _≃_ (A B : Set) : Set where
from : B → A
from∘to : ∀ (x : A) → from (to x) ≡ x
to∘from : ∀ (y : B) → to (from y) ≡ y
open _≃_
open _≃_
\end{code}
Let's unpack the definition. An isomorphism between sets `A` and `B` consists
of four things:
@ -60,7 +64,7 @@ to a corresponding inductive data declaration.
\begin{code}
data _≃′_ (A B : Set): Set where
mk-≃′ : ∀ (to : A → B) →
∀ (from : B → A) →
∀ (from : B → A) →
∀ (from∘to : (∀ (x : A) → from (to x) ≡ x)) →
∀ (to∘from : (∀ (y : B) → to (from y) ≡ y)) →
A ≃′ B
@ -107,7 +111,7 @@ and `from` to be the identity function.
; from = λ{y → y}
; from∘to = λ{x → refl}
; to∘from = λ{y → refl}
}
}
\end{code}
In the above, `to` and `from` are both bound to identity functions,
and `from∘to` and `to∘from` are both bound to functions that discard
@ -142,7 +146,7 @@ equational reasoning to combine the inverses.
from A≃B (to A≃B x)
≡⟨ from∘to A≃B x ⟩
x
∎}
∎}
; to∘from = λ{y →
begin
to B≃C (to A≃B (from A≃B (from B≃C y)))
@ -214,7 +218,7 @@ right inverses.
{ to = λ{x → x}
; from = λ{y → y}
; from∘to = λ{x → refl}
}
}
≲-trans : ∀ {A B C : Set} → A ≲ B → B ≲ C → A ≲ C
≲-trans A≲B B≲C =
@ -228,7 +232,7 @@ right inverses.
from A≲B (to A≲B x)
≡⟨ from∘to A≲B x ⟩
x
∎}
∎}
}
\end{code}
It is also easy to see that if two types embed in each other,

49
src/Lambda.lagda → src/plta/Lambda.lagda
View file

@ -4,6 +4,11 @@ layout : page
permalink : /Lambda/
---
\begin{code}
module plta.Lambda where
\end{code}
[Parts of this chapter take their text from chapter _Stlc_
of _Software Foundations_ (_Programming Language Foundations_).
Those parts will be revised.]
@ -48,8 +53,6 @@ four.
## Imports
\begin{code}
module Lambda where
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)
open import Data.String using (String; _≟_)
open import Data.Nat using (ℕ; zero; suc)
@ -76,7 +79,7 @@ And one is for recursion:
* Fixpoint, `μ x ⇒ M`
Abstraction is also called lambda abstraction, and is the construct
from which the calculus takes its name.
from which the calculus takes its name.
With the exception of variables and fixpoints, each term
form either constructs a value of a given type (abstractions yield functions,
@ -212,7 +215,7 @@ leaves the meaning of a term unchanged. Thus the five terms
* `` ƛ "s" ⇒ ƛ "z" ⇒ # "s" · (# "s" · # "z") ``
* `` ƛ "f" ⇒ ƛ "x" ⇒ # "f" · (# "f" · # "x") ``
* `` ƛ "fred" ⇒ ƛ "xander" ⇒ # "fred" · (# "fred" · # "xander") ``
* `` λ[ 😇 ∶ 𝔹 ⇒ 𝔹 ] λ[ 😈 ∶ 𝔹 ] ` 😇 · (` 😇 · ` 😈 ) ``
* `` λ[ 😇 ∶ 𝔹 ⇒ 𝔹 ] λ[ 😈 ∶ 𝔹 ] ` 😇 · (` 😇 · ` 😈 ) ``
* `` ƛ "z" ⇒ ƛ "s" ⇒ # "z" · (# "z" · # "s") ``
are all considered equivalent. Following the convention introduced
@ -235,7 +238,7 @@ _open_. Of the three terms above, the first is closed and the other
two are open.
Different occurrences of a variable may be bound and free.
In the term
In the term
(ƛ "x" ⇒ # "x") · # "x"
@ -260,7 +263,7 @@ to alpha renaming. In the term
notice that there are two binding occurrences of `m`, one in the first
line and one in the last line. It is equivalent to the following term,
μ "plus" ⇒ ƛ "x" ⇒ ƛ "y" ⇒
`case # "x"
[zero⇒ # "y"
@ -268,7 +271,7 @@ line and one in the last line. It is equivalent to the following term,
where the two binding occurrences corresponding to `m` now have distinct
names, `x` and `x′`.
## Values
@ -457,7 +460,7 @@ conditional, we first reduce the condition until it becomes a value;
if the condition is true the conditional reduces to the first
branch and if false it reduces to the second branch.
In an informal presentation of the formal semantics,
In an informal presentation of the formal semantics,
the rules for reduction are written as follows.
L ⟹ L′
@ -499,7 +502,7 @@ and indeed such rules are traditionally called beta rules.
Here are the above rules formalised in Agda.
\begin{code}
infix 4 _⟹_
infix 4 _⟹_
data _⟹_ : Term → Term → Set where
@ -525,7 +528,7 @@ data _⟹_ : Term → Term → Set where
→ `suc M ⟹ `suc M′
ξ-case : ∀ {x L L′ M N}
→ L ⟹ L′
→ L ⟹ L′
-----------------------------------------------------------------
→ `case L [zero⇒ M |suc x ⇒ N ] ⟹ `case L′ [zero⇒ M |suc x ⇒ N ]
@ -600,7 +603,7 @@ Here it is formalised in Agda, along similar lines to what
we used for reasoning about [Equality](Equality).
\begin{code}
infix 2 _⟹*_
infix 2 _⟹*_
infix 1 begin_
infixr 2 _⟹⟨_⟩_
infix 3 _∎
@ -614,7 +617,7 @@ data _⟹*_ : Term → Term → Set where
→ L ⟹ M
→ M ⟹* N
---------
→ L ⟹* N
→ L ⟹* N
begin_ : ∀ {M N} → (M ⟹* N) → (M ⟹* N)
begin M⟹*N = M⟹*N
@ -637,7 +640,7 @@ _ =
begin
plus · two · two
⟹⟨ ξ-·₁ (ξ-·₁ β-μ) ⟩
(ƛ "m" ⇒ ƛ "n" ⇒
(ƛ "m" ⇒ ƛ "n" ⇒
`case # "m" [zero⇒ # "n" |suc "m" ⇒ `suc (plus · # "m" · # "n") ])
· two · two
⟹⟨ ξ-·₁ (β-ƛ· (V-suc (V-suc V-zero))) ⟩
@ -649,11 +652,11 @@ _ =
⟹⟨ β-case-suc (V-suc V-zero) ⟩
`suc (plus · `suc `zero · two)
⟹⟨ ξ-suc (ξ-·₁ (ξ-·₁ β-μ)) ⟩
`suc ((ƛ "m" ⇒ ƛ "n" ⇒
`suc ((ƛ "m" ⇒ ƛ "n" ⇒
`case # "m" [zero⇒ # "n" |suc "m" ⇒ `suc (plus · # "m" · # "n") ])
· `suc `zero · two)
⟹⟨ ξ-suc (ξ-·₁ (β-ƛ· (V-suc V-zero))) ⟩
`suc ((ƛ "n" ⇒
`suc ((ƛ "n" ⇒
`case `suc `zero [zero⇒ # "n" |suc "m" ⇒ `suc (plus · # "m" · # "n") ])
· two)
⟹⟨ ξ-suc (β-ƛ· (V-suc (V-suc V-zero))) ⟩
@ -661,11 +664,11 @@ _ =
⟹⟨ ξ-suc (β-case-suc V-zero) ⟩
`suc `suc (plus · `zero · two)
⟹⟨ ξ-suc (ξ-suc (ξ-·₁ (ξ-·₁ β-μ))) ⟩
`suc `suc ((ƛ "m" ⇒ ƛ "n" ⇒
`suc `suc ((ƛ "m" ⇒ ƛ "n" ⇒
`case # "m" [zero⇒ # "n" |suc "m" ⇒ `suc (plus · # "m" · # "n") ])
· `zero · two)
⟹⟨ ξ-suc (ξ-suc (ξ-·₁ (β-ƛ· V-zero))) ⟩
`suc `suc ((ƛ "n" ⇒
`suc `suc ((ƛ "n" ⇒
`case `zero [zero⇒ # "n" |suc "m" ⇒ `suc (plus · # "m" · # "n") ])
· two)
⟹⟨ ξ-suc (ξ-suc (β-ƛ· (V-suc (V-suc V-zero)))) ⟩
@ -786,7 +789,7 @@ In general, we use typing _judgements_ of the form
to assert in type environment `Γ` that term `M` has type `A`.
Environment `Γ` provides types for all the free variables in `M`.
Here are three examples.
Here are three examples.
* `` ∅ , "f" ⦂ `ℕ ⇒ `ℕ , "x" ⦂ `ℕ ⊢ # "f" · (# "f" · # "x") ⦂ `ℕ ``
* `` ∅ , "f" ⦂ `ℕ ⇒ `ℕ ⊢ (ƛ "x" ⇒ # "f" · (# "f" · # "x")) ⦂ `ℕ ⇒ `ℕ ``
@ -800,7 +803,7 @@ environment `Γ` by mapping variable `x` to type `A`.
*(((Need text to explain `Γ ∋ x ⦂ A`)))*
In an informal presentation of the formal semantics,
In an informal presentation of the formal semantics,
the rules for typing are written as follows.
Γ x ≡ A
@ -829,7 +832,7 @@ the rules for typing are written as follows.
Γ ⊢ if L then M else N ⦂ A
As we will show later, the rules are deterministic, in that
at most one rule applies to every term.
at most one rule applies to every term.
The proof rules come in pairs, with rules to introduce and to
eliminate each connective, labeled `-I` and `-E`, respectively. As we
@ -851,7 +854,7 @@ infix 4 _⊢_⦂_
infixl 5 _,_⦂_
data Context : Set where
∅ : Context
∅ : Context
_,_⦂_ : Context → Id → Type → Context
data _∋_⦂_ : Context → Id → Type → Set where
@ -929,9 +932,9 @@ Derivation of for the Church numeral two:
Where `∋s` and `∋z` abbreviate the two derivations:
---------------- Z
---------------- Z
"s" ≢ "z" Γ₁ ∋ "s" ⦂ A ⇒ A
----------------------------- S ------------- Z
----------------------------- S ------------- Z
Γ₂ ∋ "s" ⦂ A ⇒ A Γ₂ ∋ "z" ⦂ A
where `Γ₁ = ∅ , s ⦂ A ⇒ A` and `Γ₂ = ∅ , s ⦂ A ⇒ A , z ⦂ A`.

19
src/LambdaProp.lagda → src/plta/LambdaProp.lagda
View file

@ -4,6 +4,11 @@ layout : page
permalink : /LambdaProp/
---
\begin{code}
module plta.LambdaProp where
\end{code}
[Parts of this chapter take their text from chapter _Stlc_
of _Software Foundations_ (_Programming Language Foundations_).
Those parts will be revised.]
@ -25,8 +30,6 @@ types without needing to develop a separate inductive definition of the
## Imports
\begin{code}
module LambdaProp where
open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)
open import Data.String using (String; _≟_)
open import Data.Nat using (ℕ; zero; suc)
@ -37,7 +40,7 @@ open import Data.Product
open import Data.Sum using (_⊎_; inj₁; inj₂)
open import Relation.Nullary using (¬_; Dec; yes; no)
open import Function using (_∘_)
open import Lambda
open import plta.Lambda
\end{code}
@ -46,7 +49,7 @@ open import Lambda
The first step in establishing basic properties of reduction and typing
is to identify the possible _canonical forms_ (i.e., well-typed closed values)
belonging to each type. For function types the canonical forms are lambda-abstractions,
while for boolean types they are values `true` and `false`.
while for boolean types they are values `true` and `false`.
\begin{code}
infix 4 Canonical_⦂_
@ -157,7 +160,7 @@ technical lemmas), the story goes like this:
- The _preservation theorem_ is proved by induction on a typing derivation.
The definition of `β-ƛ· uses substitution. To see that
this step preserves typing, we need to know that the substitution itself
does. So we prove a ...
does. So we prove a ...
- _substitution lemma_, stating that substituting a (closed) term
`V` for a variable `x` in a term `N` preserves the type of `N`.
@ -202,7 +205,7 @@ rename : ∀ {Γ Δ}
→ (∀ {M A} → Γ ⊢ M ⦂ A → Δ ⊢ M ⦂ A)
rename σ (Ax ∋w) = Ax (σ ∋w)
rename σ (⇒-I ⊢N) = ⇒-I (rename (ext σ) ⊢N)
rename σ (⇒-E ⊢L ⊢M) = ⇒-E (rename σ ⊢L) (rename σ ⊢M)
rename σ (⇒-E ⊢L ⊢M) = ⇒-E (rename σ ⊢L) (rename σ ⊢M)
rename σ ℕ-I₁ = ℕ-I₁
rename σ (ℕ-I₂ ⊢M) = ℕ-I₂ (rename σ ⊢M)
rename σ (ℕ-E ⊢L ⊢M ⊢N) = ℕ-E (rename σ ⊢L) (rename σ ⊢M) (rename (ext σ) ⊢N)
@ -340,7 +343,7 @@ preserve : ∀ {M N A}
→ M ⟹ N
----------
→ ∅ ⊢ N ⦂ A
preserve (Ax ())
preserve (Ax ())
preserve (⇒-I ⊢N) ()
preserve (⇒-E ⊢L ⊢M) (ξ-·₁ L⟹L′) = ⇒-E (preserve ⊢L L⟹L′) ⊢M
preserve (⇒-E ⊢L ⊢M) (ξ-·₂ VL M⟹M′) = ⇒-E ⊢L (preserve ⊢M M⟹M′)
@ -822,5 +825,3 @@ false, give a counterexample.
- Progress
- Preservation

22
src/Lists.lagda → src/plta/Lists.lagda
View file

@ -4,6 +4,10 @@ layout : page
permalink : /Lists/
---
\begin{code}
module plta.Lists where
\end{code}
This chapter discusses the list data type. It gives further examples
of many of the techniques we have developed so far, and provides
examples of polymorphic types and higher-order functions.
@ -19,7 +23,7 @@ open import Data.Nat.Properties using
(+-assoc; +-identityˡ; +-identityʳ; *-assoc; *-identityˡ; *-identityʳ)
open import Relation.Nullary using (¬_)
open import Data.Product using (_×_) renaming (_,_ to ⟨_,_⟩)
open import Isomorphism using (_≃_)
open import plta.Isomorphism using (_≃_)
open import Function using (_∘_)
open import Level using (Level)
\end{code}
@ -59,7 +63,7 @@ denotes the list of the first three natural numbers. Since `_::_`
associates to the right, the term parses as `0 ∷ (1 ∷ (2 ∷ []))`.
Here `0` is the first element of the list, called the *head*,
and `1 ∷ (2 ∷ [])` is a list of the remaining elements, called the
*tail*. Lists are a rather strange beast: they have a head and a tail,
*tail*. Lists are a rather strange beast: they have a head and a tail,
nothing in between, and the tail is itself another list!
As we've seen, parameterised types can be translated to
@ -107,7 +111,7 @@ on the right-hand side of an equation.
## Append
Our first function on lists is written `_++_` and pronounced
*append*.
*append*.
\begin{code}
infixr 5 _++_
@ -265,7 +269,7 @@ The length of one list appended to another is the
sum of the lengths of the lists.
\begin{code}
length-++ : ∀ {A : Set} (xs ys : List A) → length (xs ++ ys) ≡ length xs + length ys
length-++ {A} [] ys =
length-++ {A} [] ys =
begin
length ([] ++ ys)
≡⟨⟩
@ -449,7 +453,7 @@ _ =
shunt (2 ∷ []) (1 ∷ 0 ∷ [])
≡⟨⟩
shunt [] (2 ∷ 1 ∷ 0 ∷ [])
≡⟨⟩
≡⟨⟩
2 ∷ 1 ∷ 0 ∷ []
∎
\end{code}
@ -533,7 +537,7 @@ Prove the following relationship between map and append.
Fold takes an operator and a value, and uses the operator to combine
each of the elements of the list, taking the given value as the result
for the empty list.
for the empty list.
\begin{code}
foldr : ∀ {A B : Set} → (A → B → B) → B → List A → B
foldr _⊗_ e [] = e
@ -559,7 +563,7 @@ _ =
1 + (2 + (3 + (4 + foldr _+_ 0 [])))
≡⟨⟩
1 + (2 + (3 + (4 + 0)))
∎
∎
\end{code}
Fold requires time linear in the length of the list.
@ -603,7 +607,7 @@ postulate
\end{code}
### Exercise (`map-is-foldr`)
### Exercise (`map-is-foldr`)
Show that map can be defined using fold.
\begin{code}
@ -728,7 +732,7 @@ foldr-monoid-++ _⊗_ e monoid-⊗ xs ys =
foldr _⊗_ e xs ⊗ foldr _⊗_ e ys
∎
\end{code}
## All {#All}
We can also define predicates over lists. Two of the most important

11
src/Modules.lagda → src/plta/Modules.lagda
View file

@ -7,6 +7,10 @@ permalink : /Modules/
** Turn this into a Setoid example. Copy equivalence relation and setoid
from the standard library. **
\begin{code}
module plta.Modules where
\end{code}
This chapter introduces modules as a way of structuring proofs,
and proves some general results which will be useful later.
@ -17,18 +21,15 @@ import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong)
open Eq.≡-Reasoning
open import Data.Nat using (ℕ; zero; suc; _+_; _*_; _∸_; _≤_; s≤s; z≤n)
-- open import Data.Nat.Properties using
-- (+-assoc; +-identityˡ; +-identityʳ; *-assoc; *-identityˡ; *-identityʳ)
open import Relation.Nullary using (¬_)
open import Data.Product using (_×_) renaming (_,_ to ⟨_,_⟩)
open import Isomorphism using (_≃_)
open import plta.Isomorphism using (_≃_)
open import Function using (_∘_)
open import Level using (Level)
open import Data.Maybe using (Maybe; just; nothing)
open import Data.List using (List; []; _∷_; _++_; map; foldr; downFrom)
open import Data.List.All using (All; []; _∷_)
open import Data.List.Any using (Any; here; there)
-- open import Data.List.Any.Membership.Propositional using (_∈_)
\end{code}
We assume [extensionality][extensionality].
@ -101,7 +102,7 @@ Say I want to define a type of stacks, with operations push and pop.
I can define stacks in terms of lists, but hide the definitions from
the rest of the program.
\begin{code}
abstract
abstract
Stack : Set → Set
Stack A = List A

20
src/Naturals.lagda → src/plta/Naturals.lagda
View file

@ -4,6 +4,10 @@ layout : page
permalink : /Naturals/
---
\begin{code}
module plta.Naturals where
\end{code}
The night sky holds more stars than I can count, though fewer than five
thousand are visible to the naked eye. The observable universe
contains about seventy sextillion stars.
@ -144,7 +148,7 @@ natural number (on the day before today) then `suc m` is also a
natural number (today). We didn't know about any natural numbers
before today, so the inductive case doesn't apply.
-- on the first day, there is one natural number
-- on the first day, there is one natural number
zero : ℕ
Then we repeat the process. On the next day we know about all the
@ -265,7 +269,7 @@ specifies operators to support reasoning about equivalence, and adds
all the names specified in the `using` clause into the current scope.
In this case, the names added are `begin_`, `_≡⟨⟩_`, and `_∎`. We
will see how these are used below. We take all these as givens for now,
but will see how they are defined in Chapter [Equality]({{ site.baseurl }}{% link out/Equality.md %}).
but will see how they are defined in Chapter [Equality](Equality).
Agda uses underbars to indicate where terms appear in infix or mixfix
operators. Thus, `_≡_` and `_≡⟨⟩_` are infix (each operator is written
@ -301,7 +305,7 @@ written with underbars where the argument go, hence its name is
`_+_`. The first line is a signature specifying the type of the operator.
The type `ℕ → ℕ → ℕ`, indicates that addition accepts two naturals
and returns a natural. Infix notation is just a shorthand for application;
the terms `m + n` and `_+_ m n` are equivalent.
the terms `m + n` and `_+_ m n` are equivalent.
The definition has a base case and an inductive case, corresponding to
those for the natural numbers. The base case says that adding zero to
@ -423,7 +427,7 @@ Once we have defined addition, we can define multiplication
as repeated addition.
\begin{code}
_*_ : ℕ → ℕ → ℕ
zero * n = zero
zero * n = zero
(suc m) * n = n + (m * n)
\end{code}
@ -445,7 +449,7 @@ identity for multiplication, so `1 * n = n`.
Again, the definition is well-founded in that multiplication of
larger numbers is defined in terms of multiplication of smaller numbers.
For example, let's multiply two and three.
\begin{code}
_ =
@ -650,7 +654,7 @@ more equations.
0 + 0 = 0 0 + 1 = 1 0 + 2 = 2 0 + 3 = 3 ...
1 + 0 = 1 1 + 1 = 2 1 + 2 = 3 1 + 3 = 4 ...
And we repeat the process again.
And we repeat the process again.
-- on the third day, we know about addition of 0, 1, and 2
0 + 0 = 0 0 + 1 = 1 0 + 2 = 2 0 + 3 = 3 ...
@ -867,7 +871,7 @@ Information on pragmas can be found in the Agda documentation.
This chapter uses the following unicode.
ℕ U+2115 DOUBLE-STRUCK CAPITAL N (\bN)
ℕ U+2115 DOUBLE-STRUCK CAPITAL N (\bN)
→ U+2192 RIGHTWARDS ARROW (\to, \r)
∸ U+2238 DOT MINUS (\.-)
≡ U+2261 IDENTICAL TO (\==) =
@ -894,5 +898,3 @@ In place of left, right, up, and down keys, one may also use control characters.
We write `^B` to stand for control-B, and similarly. One can also navigate
left and write by typing the digits that appear in the displayed list.

14
src/Negation.lagda → src/plta/Negation.lagda
View file

@ -4,13 +4,17 @@ layout : page
permalink : /Negation/
---
\begin{code}
module plta.Negation where
\end{code}
This chapter introduces negation, and discusses intuitionistic
and classical logic.
## Imports
\begin{code}
open import Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_)
open import plta.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_)
open import Relation.Binary.PropositionalEquality using (_≡_; refl)
open import Data.Nat using (ℕ; zero; suc)
open import Data.Empty using (⊥; ⊥-elim)
@ -24,7 +28,7 @@ open import Function using (_∘_)
Given a proposition `A`, the negation `¬ A` holds if `A` cannot hold.
We formalise this idea by declaring negation to be the same
as implication of false.
as implication of false.
\begin{code}
¬_ : Set → Set
¬ A = A → ⊥
@ -117,7 +121,7 @@ peano : ∀ {m : ℕ} → zero ≢ suc m
peano = λ()
\end{code}
The evidence is essentially the same, as the absurd pattern matches
all possible evidence of type `zero ≡ suc m`.
all possible evidence of type `zero ≡ suc m`.
Given the correspondence of implication to exponentiation and
false to the type with no members, we can view negation as
@ -264,7 +268,7 @@ pick the first disjunct.
em-irrefutable k = k (inj₂ λ{ x → k (inj₁ x) })
There are no holes left! This completes the proof.
There are no holes left! This completes the proof.
The following story illustrates the behaviour of the term we have created.
(With apologies to Peter Selinger, who tells a similar story
@ -319,7 +323,7 @@ Implication = ∀ {A B : Set} → (A → B) → ¬ A ⊎ B
×-Implies-⊎ = ∀ {A B : Set} → ¬ (A × B) → (¬ A) ⊎ (¬ B)
\end{code}
### Exercise (`¬-stable`, `×-stable`)
Say that a formula is *stable* if double negation elimination holds for it.

5
src/Preface.lagda → src/plta/Preface.lagda
View file

@ -4,6 +4,10 @@ layout : page
permalink : /Preface/
---
\begin{code}
module plta.Preface where
\end{code}
This book is an introduction to programming language theory, written
in Agda. The authors are [Wen Kokke][wen] and [Philip Wadler][phil].
@ -88,4 +92,3 @@ preparing an Agda file that solves the exercise. Sometimes it is up to you to
work out the type of the identifier, but sometimes we give it in the exercise.
In some cases the type is bound to an identifier with a capital in its
name, where the identifier you are to define has a small letter instead.

12
src/Properties.lagda → src/plta/Properties.lagda
View file

@ -4,6 +4,10 @@ layout : page
permalink : /Properties/
---
\begin{code}
module plta.Properties where
\end{code}
Now that we've defined the naturals and operations upon them, our next
step is to learn how to prove properties that they satisfy. As hinted
by their name, properties of *inductive datatypes* are proved by
@ -140,7 +144,7 @@ You've got the hang of it by now.
The process continues. On the *n*th day there will be *n* distinct
properties that hold. The property of every natural number will appear
on some given day. In particular, the property `P n` first appears on
day *n+1*.
day *n+1*.
## Our first proof: associativity
@ -185,7 +189,7 @@ Here is the proposition's statement and proof.
suc (m + (n + p))
≡⟨⟩
suc m + (n + p)
∎
∎
\end{code}
We have named the proof `+-assoc`. In Agda, identifiers can consist of
any sequence of characters not including spaces or the characters `@.(){};_`.
@ -424,7 +428,7 @@ Finally, here is our proposition's statement and proof.
suc (n + m)
≡⟨⟩
suc n + m
∎
∎
\end{code}
The first line states that we are defining the identifier
`+-comm` which provides evidence for the proposition:
@ -495,7 +499,7 @@ before today, so that rule doesn't give us any new judgments.
-- on the first day, we know about associativity of 0
(0 + 0) + 0 ≡ 0 + (0 + 0) ... (0 + 4) + 5 ≡ 0 + (4 + 5) ...
Then we repeat the process, so on the next day we know about all the
judgements from the day before, plus any judgements added by the rules.
The base case tells us nothing new, but now the inductive case adds

16
src/Quantifiers.lagda → src/plta/Quantifiers.lagda
View file

@ -4,6 +4,10 @@ layout : page
permalink : /Quantifiers/
---
\begin{code}
module plta.Quantifiers where
\end{code}
This chapter introduces universal and existential quantification.
## Imports
@ -12,8 +16,8 @@ This chapter introduces universal and existential quantification.
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong)
open Eq.≡-Reasoning
open import Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_)
open Isomorphism.≃-Reasoning
open import plta.Isomorphism using (_≃_; ≃-sym; ≃-trans; _≲_)
open plta.Isomorphism.≃-Reasoning
open import Data.Nat using (ℕ; zero; suc; _+_; _*_)
open import Data.Nat.Properties.Simple using (+-suc)
open import Relation.Nullary using (¬_)
@ -74,7 +78,7 @@ evidence of a proposition are indistinguishable.
Dependent function types are sometimes referred to as dependent products,
because if `A` is a finite type with values `x₁ , ⋯ , xᵢ`, and if
each of the types `B x₁ , ⋯ , B xᵢ` has `m₁ , ⋯ , mᵢ` distinct members,
then `∀ (x : A) → B x` has `m₁ * ⋯ * mᵢ` members.
then `∀ (x : A) → B x` has `m₁ * ⋯ * mᵢ` members.
Indeed, sometimes the notation `∀ (x : A) → B x`
is replaced by a notation such as `Π[ x ∈ A ] (B x)`,
where `Π` stands for product. However, we will stick with the name
@ -236,7 +240,7 @@ Does the converse hold? If so, prove; if not, explain why.
## An existential example
Recall the definitions of `even` and `odd` from Chapter [Relations](Relations).
Recall the definitions of `even` and `odd` from Chapter [Relations](Relations).
\begin{code}
data even : ℕ → Set
data odd : ℕ → Set
@ -350,8 +354,8 @@ of a disjunction is isomorphic to a conjunction of negations.
record
{ to = λ{ ¬∃xy x y → ¬∃xy ⟨ x , y ⟩ }
; from = λ{ ∀¬xy ⟨ x , y ⟩ → ∀¬xy x y }
; from∘to = λ{ ¬∃xy → extensionality λ{ ⟨ x , y ⟩ → refl } }
; to∘from = λ{ ∀¬xy → refl }
; from∘to = λ{ ¬∃xy → extensionality λ{ ⟨ x , y ⟩ → refl } }
; to∘from = λ{ ∀¬xy → refl }
}
\end{code}
In the `to` direction, we are given a value `¬∃xy` of type

11
src/Relations.lagda → src/plta/Relations.lagda
View file

@ -4,10 +4,13 @@ layout : page
permalink : /Relations/
---
\begin{code}
module plta.Relations where
\end{code}
After having defined operations such as addition and multiplication,
the next step is to define relations, such as *less than or equal*.
## Imports
\begin{code}
@ -59,7 +62,7 @@ Both definitions above tell us the same two things:
In fact, they each give us a bit more detail:
+ *Base case*: for all naturals `n`, the constructor `z≤n`
+ *Base case*: for all naturals `n`, the constructor `z≤n`
produces evidence that `zero ≤ n` holds.
+ *Inductive case*: for all naturals `m` and `n`, the constructor
`s≤s` takes evidence that `m ≤ n` holds into evidence that
@ -306,7 +309,7 @@ In this case the proof is by induction over both the first
and second arguments. We perform a case analysis:
+ *First base case*: If the first argument is `zero` and the
second argument is `n` then the forward case holds,
second argument is `n` then the forward case holds,
with `z≤n` as evidence that `zero ≤ n`.
+ *Second base case*: If the first argument is `suc m` and the
@ -379,7 +382,7 @@ addition is monotonic on the right.
\begin{code}
+-monoʳ-≤ : ∀ (m p q : ℕ) → p ≤ q → m + p ≤ m + q
+-monoʳ-≤ zero p q p≤q = p≤q
+-monoʳ-≤ (suc m) p q p≤q = s≤s (+-monoʳ-≤ m p q p≤q)
+-monoʳ-≤ (suc m) p q p≤q = s≤s (+-monoʳ-≤ m p q p≤q)
\end{code}
The proof is by induction on the first argument.

10
src/Untyped.lagda → src/plta/Untyped.lagda
View file

@ -4,6 +4,10 @@ layout : page
permalink : /Untyped/
---
\begin{code}
module plta.Untyped where
\end{code}
This chapter considers a system that varies, in interesting ways,
what has gone earlier. The lambda calculus in this section is
untyped rather than simply-typed; uses terms that are inherently-scoped
@ -13,10 +17,6 @@ call-by-value order of reduction.
## Imports
\begin{code}
module Untyped where
\end{code}
\begin{code}
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong)
@ -301,7 +301,7 @@ normalise (suc g) L with progress L
\end{code}
\begin{code}
_ : normalise 100 (plus {zero} · two · two) ≡
_ : normalise 100 (plus {zero} · two · two) ≡
normal 94
((ƛ
(ƛ