diff --git a/index.md b/index.md
index 468dfb80..13e9d65a 100644
--- a/index.md
+++ b/index.md
@@ -7,4 +7,3 @@ layout : page
- [Maps: Total and Partial Maps]({{ "/Maps" | relative_url }})
- [Stlc: The Simply Typed Lambda-Calculus]({{ "/Stlc" | relative_url }})
- [StlcProp: Properties of STLC]({{ "/StlcProp" | relative_url }})
- - [StlcPhil: The Simply Typed Lambda Calculus (Phil's version)]({{ "/StlcPhil | relative_url }})
diff --git a/src/Maps.lagda b/src/Maps.lagda
index d92bef88..a965e53d 100644
--- a/src/Maps.lagda
+++ b/src/Maps.lagda
@@ -117,13 +117,13 @@ function that can be used to look up ids, yielding $$A$$s.
module TotalMap where
\end{code}
-The function `empty` yields an empty total map, given a
+The function `always` yields a total map given a
default element; this map always returns the default element when
applied to any id.
\begin{code}
- empty : ∀ {A} → A → TotalMap A
- empty v x = v
+ always : ∀ {A} → A → TotalMap A
+ always v x = v
\end{code}
More interesting is the update function, which (as before) takes
@@ -165,7 +165,7 @@ maps to 42, $$y$$ maps to 69, and every other key maps to 0, as follows:
\begin{code}
ρ₀ : TotalMap ℕ
- ρ₀ = empty 0 , x ↦ 42 , y ↦ 69
+ ρ₀ = always 0 , x ↦ 42 , y ↦ 69
\end{code}
This completes the definition of total maps. Note that we don't
@@ -188,18 +188,18 @@ facts about how they behave. Even if you don't work the following
exercises, make sure you understand the statements of
the lemmas!
-#### Exercise: 1 star, optional (apply-empty)
-First, the empty map returns its default element for all keys:
+#### Exercise: 1 star, optional (apply-always)
+The `always` map returns its default element for all keys:
\begin{code}
postulate
- apply-empty : ∀ {A} (v : A) (x : Id) → empty v x ≡ v
+ apply-always : ∀ {A} (v : A) (x : Id) → always v x ≡ v
\end{code}
\begin{code}
- apply-empty′ : ∀ {A} (v : A) (x : Id) → empty v x ≡ v
- apply-empty′ v x = refl
+ apply-always′ : ∀ {A} (v : A) (x : Id) → always v x ≡ v
+ apply-always′ v x = refl
\end{code}
@@ -296,65 +296,26 @@ updates.
\begin{code}
update-permute′ : ∀ {A} (ρ : TotalMap A) (x : Id) (v : A) (y : Id) (w : A) (z : Id)
→ x ≢ y → (ρ , x ↦ v , y ↦ w) z ≡ (ρ , y ↦ w , x ↦ v) z
- update-permute′ {A} ρ x v y w z x≢y
- with x ≟ z | y ≟ z
- update-permute′ {A} ρ x v y w z x≢y
- | yes x≡z | yes y≡z = ⊥-elim (x≢y (trans x≡z (sym y≡z)))
- update-permute′ {A} ρ x v y w z x≢y
- | no x≢z | yes y≡z rewrite y≡z
- with z ≟ z
- update-permute′ {A} ρ x v y w z x≢y
- | no x≢z | yes y≡z | yes z≡z = refl
- update-permute′ {A} ρ x v y w z x≢y
- | no x≢z | yes y≡z | no z≢z = ⊥-elim (z≢z refl)
- update-permute′ {A} ρ x v y w z x≢y
- | yes x≡z | no y≢z rewrite x≡z
- with z ≟ z
- update-permute′ {A} ρ x v y w z x≢y
- | yes x≡z | no y≢z | yes z≡z = refl
- update-permute′ {A} ρ x v y w z x≢y
- | yes x≡z | no y≢z | no z≢z = ⊥-elim (z≢z refl)
- update-permute′ {A} ρ x v y w z x≢y
- | no x≢z | no y≢z
- with x ≟ z | y ≟ z
- update-permute′ {A} ρ x v y w z x≢y
- | no _ | no _ | no x≢z | no y≢z
- = refl
- update-permute′ {A} ρ x v y w z x≢y
- | no x≢z | no y≢z | yes x≡z | _
- = ⊥-elim (x≢z x≡z)
- update-permute′ {A} ρ x v y w z x≢y
- | no x≢z | no y≢z | _ | yes y≡z
- = ⊥-elim (y≢z y≡z)
+ update-permute′ {A} ρ x v y w z x≢y with x ≟ z | y ≟ z
+ ... | yes refl | yes refl = ⊥-elim (x≢y refl)
+ ... | no x≢z | yes refl = sym (update-eq′ ρ z w)
+ ... | yes refl | no y≢z = update-eq′ ρ z v
+ ... | no x≢z | no y≢z = trans (update-neq ρ x v z x≢z) (sym (update-neq ρ y w z y≢z))
+\end{code}
+
+And a slightly different version of the same proof.
+
+\begin{code}
+ update-permute′′ : ∀ {A} (ρ : TotalMap A) (x : Id) (v : A) (y : Id) (w : A) (z : Id)
+ → x ≢ y → (ρ , x ↦ v , y ↦ w) z ≡ (ρ , y ↦ w , x ↦ v) z
+ update-permute′′ {A} ρ x v y w z x≢y with x ≟ z | y ≟ z
+ ... | yes x≡z | yes y≡z = ⊥-elim (x≢y (trans x≡z (sym y≡z)))
+ ... | no x≢z | yes y≡z rewrite y≡z = sym (update-eq′ ρ z w)
+ ... | yes x≡z | no y≢z rewrite x≡z = update-eq′ ρ z v
+ ... | no x≢z | no y≢z = trans (update-neq ρ x v z x≢z) (sym (update-neq ρ y w z y≢z))
\end{code}
-
-Phil:
- Holes are typed as follows. What do the "| z ≟ z" mean, and how can I deal
- with them? Why does "λ y₁" appear in the final hole?
-
- ?0 : w ≡ ((ρ , z ↦ w) z | z ≟ z)
- ?1 : ((ρ , z ↦ v) z | z ≟ z) ≡ v
- ?2 : (((λ y₁ → (ρ , x ↦ v) y₁ | x ≟ y₁) , y ↦ w) z | no y≢z) ≡
- (((λ y₁ → (ρ , y ↦ w) y₁ | y ≟ y₁) , x ↦ v) z | no x≢z)
-
-Wen:
- The "| z ≟ z" term appears because there is a comparison on the two strings z
- and z somewhere in the code. Because the decidable equality (and in fact all
- functions on strings) are postulate, they do not reduce during type checking.
- In order to stop this, you would have to insert a with clause at the location
- where you want the term to reduce, i.e. "with z ≟ z", so that you can cover
- both possible outputs, even if you already know that "z ≡ z", e.g. due to
- reflexivity. You can cover the other case with a ⊥-elim fairly easily, but
- it's not pretty. This is why I used naturals, because their equality test is
- implemented in Agda and therefore can reduce. However, I'm not sure if
- switching would in fact solve this problem, due to the fact that we're dealing
- with variables, but I think so. See the completed code above for the
- not-so-pretty way of actually implementing update-permute'.
-
-
-
## Partial maps
Finally, we define _partial maps_ on top of total maps. A partial
@@ -371,15 +332,14 @@ module PartialMap where
\end{code}
\begin{code}
- empty : ∀ {A} → PartialMap A
- empty = TotalMap.empty nothing
+ ∅ : ∀ {A} → PartialMap A
+ ∅ = TotalMap.always nothing
\end{code}
\begin{code}
_,_↦_ : ∀ {A} (ρ : PartialMap A) (x : Id) (v : A) → PartialMap A
ρ , x ↦ v = TotalMap._,_↦_ ρ x (just v)
\end{code}
-
As before, we define handy abbreviations for updating a map two, three, or four times.
\begin{code}
diff --git a/src/MapsOld.lagda b/src/MapsOld.lagda
new file mode 100644
index 00000000..673b6959
--- /dev/null
+++ b/src/MapsOld.lagda
@@ -0,0 +1,340 @@
+---
+title : "Maps: Total and Partial Maps"
+layout : page
+permalink : /Maps
+---
+
+Maps (or dictionaries) are ubiquitous data structures, both in software
+construction generally and in the theory of programming languages in particular;
+we're going to need them in many places in the coming chapters. They also make
+a nice case study using ideas we've seen in previous chapters, including
+building data structures out of higher-order functions (from [Basics]({{
+"Basics" | relative_url }}) and [Poly]({{ "Poly" | relative_url }}) and the use
+of reflection to streamline proofs (from [IndProp]({{ "IndProp" | relative_url
+}})).
+
+We'll define two flavors of maps: _total_ maps, which include a
+"default" element to be returned when a key being looked up
+doesn't exist, and _partial_ maps, which return an `Maybe` to
+indicate success or failure. The latter is defined in terms of
+the former, using `nothing` as the default element.
+
+## The Agda Standard Library
+
+One small digression before we start.
+
+Unlike the chapters we have seen so far, this one does not
+import the chapter before it (and, transitively, all the
+earlier chapters). Instead, in this chapter and from now, on
+we're going to import the definitions and theorems we need
+directly from Agda's standard library stuff. You should not notice
+much difference, though, because we've been careful to name our
+own definitions and theorems the same as their counterparts in the
+standard library, wherever they overlap.
+
+\begin{code}
+open import Function using (_∘_)
+open import Data.Bool using (Bool; true; false)
+open import Data.Empty using (⊥; ⊥-elim)
+open import Data.Maybe using (Maybe; just; nothing)
+open import Data.Nat using (ℕ)
+open import Relation.Nullary using (Dec; yes; no)
+open import Relation.Binary.PropositionalEquality
+\end{code}
+
+Documentation for the standard library can be found at
+.
+
+## Identifiers
+
+First, we need a type for the keys that we use to index into our
+maps. For this purpose, we again use the type Id` from the
+[Lists](sf/Lists.html) chapter. To make this chapter self contained,
+we repeat its definition here, together with the equality comparison
+function for ids and its fundamental property.
+
+\begin{code}
+data Id : Set where
+ id : ℕ → Id
+\end{code}
+
+\begin{code}
+_≟_ : (x y : Id) → Dec (x ≡ y)
+id x ≟ id y with x Data.Nat.≟ y
+id x ≟ id y | yes x=y rewrite x=y = yes refl
+id x ≟ id y | no x≠y = no (x≠y ∘ id-inj)
+ where
+ id-inj : ∀ {x y} → id x ≡ id y → x ≡ y
+ id-inj refl = refl
+\end{code}
+
+## Total Maps
+
+Our main job in this chapter will be to build a definition of
+partial maps that is similar in behavior to the one we saw in the
+[Lists](sf/Lists.html) chapter, plus accompanying lemmas about their
+behavior.
+
+This time around, though, we're going to use _functions_, rather
+than lists of key-value pairs, to build maps. The advantage of
+this representation is that it offers a more _extensional_ view of
+maps, where two maps that respond to queries in the same way will
+be represented as literally the same thing (the same function),
+rather than just "equivalent" data structures. This, in turn,
+simplifies proofs that use maps.
+
+We build partial maps in two steps. First, we define a type of
+_total maps_ that return a default value when we look up a key
+that is not present in the map.
+
+\begin{code}
+TotalMap : Set → Set
+TotalMap A = Id → A
+\end{code}
+
+Intuitively, a total map over anfi element type $$A$$ _is_ just a
+function that can be used to look up ids, yielding $$A$$s.
+
+\begin{code}
+module TotalMap where
+\end{code}
+
+The function `empty` yields an empty total map, given a
+default element; this map always returns the default element when
+applied to any id.
+
+\begin{code}
+ empty : ∀ {A} → A → TotalMap A
+ empty x = λ _ → x
+\end{code}
+
+More interesting is the `update` function, which (as before) takes
+a map $$m$$, a key $$x$$, and a value $$v$$ and returns a new map that
+takes $$x$$ to $$v$$ and takes every other key to whatever $$m$$ does.
+
+\begin{code}
+ update : ∀ {A} → TotalMap A -> Id -> A -> TotalMap A
+ update m x v y with x ≟ y
+ ... | yes x=y = v
+ ... | no x≠y = m y
+\end{code}
+
+This definition is a nice example of higher-order programming.
+The `update` function takes a _function_ $$m$$ and yields a new
+function $$\lambda x'.\vdots$$ that behaves like the desired map.
+
+For example, we can build a map taking ids to bools, where `id
+3` is mapped to `true` and every other key is mapped to `false`,
+like this:
+
+\begin{code}
+ examplemap : TotalMap Bool
+ examplemap = update (update (empty false) (id 1) false) (id 3) true
+\end{code}
+
+This completes the definition of total maps. Note that we don't
+need to define a `find` operation because it is just function
+application!
+
+\begin{code}
+ test_examplemap0 : examplemap (id 0) ≡ false
+ test_examplemap0 = refl
+
+ test_examplemap1 : examplemap (id 1) ≡ false
+ test_examplemap1 = refl
+
+ test_examplemap2 : examplemap (id 2) ≡ false
+ test_examplemap2 = refl
+
+ test_examplemap3 : examplemap (id 3) ≡ true
+ test_examplemap3 = refl
+\end{code}
+
+To use maps in later chapters, we'll need several fundamental
+facts about how they behave. Even if you don't work the following
+exercises, make sure you thoroughly understand the statements of
+the lemmas! (Some of the proofs require the functional
+extensionality axiom, which is discussed in the [Logic]
+chapter and included in the Agda standard library.)
+
+#### Exercise: 1 star, optional (apply-empty)
+First, the empty map returns its default element for all keys:
+
+\begin{code}
+ postulate
+ apply-empty : ∀ {A x v} → empty {A} v x ≡ v
+\end{code}
+
+
+\begin{code}
+ apply-empty′ : ∀ {A x v} → empty {A} v x ≡ v
+ apply-empty′ = refl
+\end{code}
+
+
+#### Exercise: 2 stars, optional (update-eq)
+Next, if we update a map $$m$$ at a key $$x$$ with a new value $$v$$
+and then look up $$x$$ in the map resulting from the `update`, we get
+back $$v$$:
+
+\begin{code}
+ postulate
+ update-eq : ∀ {A v} (m : TotalMap A) (x : Id)
+ → (update m x v) x ≡ v
+\end{code}
+
+
+\begin{code}
+ update-eq′ : ∀ {A v} (m : TotalMap A) (x : Id)
+ → (update m x v) x ≡ v
+ update-eq′ m x with x ≟ x
+ ... | yes x=x = refl
+ ... | no x≠x = ⊥-elim (x≠x refl)
+\end{code}
+
+
+#### Exercise: 2 stars, optional (update-neq)
+On the other hand, if we update a map $$m$$ at a key $$x$$ and
+then look up a _different_ key $$y$$ in the resulting map, we get
+the same result that $$m$$ would have given:
+
+\begin{code}
+ update-neq : ∀ {A v} (m : TotalMap A) (x y : Id)
+ → x ≢ y → (update m x v) y ≡ m y
+ update-neq m x y x≠y with x ≟ y
+ ... | yes x=y = ⊥-elim (x≠y x=y)
+ ... | no _ = refl
+\end{code}
+
+#### Exercise: 2 stars, optional (update-shadow)
+If we update a map $$m$$ at a key $$x$$ with a value $$v_1$$ and then
+update again with the same key $$x$$ and another value $$v_2$$, the
+resulting map behaves the same (gives the same result when applied
+to any key) as the simpler map obtained by performing just
+the second `update` on $$m$$:
+
+\begin{code}
+ postulate
+ update-shadow : ∀ {A v1 v2} (m : TotalMap A) (x y : Id)
+ → (update (update m x v1) x v2) y ≡ (update m x v2) y
+\end{code}
+
+
+\begin{code}
+ update-shadow′ : ∀ {A v1 v2} (m : TotalMap A) (x y : Id)
+ → (update (update m x v1) x v2) y ≡ (update m x v2) y
+ update-shadow′ m x y
+ with x ≟ y
+ ... | yes x=y = refl
+ ... | no x≠y = update-neq m x y x≠y
+\end{code}
+
+
+#### Exercise: 2 stars (update-same)
+Prove the following theorem, which states that if we update a map to
+assign key $$x$$ the same value as it already has in $$m$$, then the
+result is equal to $$m$$:
+
+\begin{code}
+ postulate
+ update-same : ∀ {A} (m : TotalMap A) (x y : Id)
+ → (update m x (m x)) y ≡ m y
+\end{code}
+
+
+\begin{code}
+ update-same′ : ∀ {A} (m : TotalMap A) (x y : Id)
+ → (update m x (m x)) y ≡ m y
+ update-same′ m x y
+ with x ≟ y
+ ... | yes x=y rewrite x=y = refl
+ ... | no x≠y = refl
+\end{code}
+
+
+#### Exercise: 3 stars, recommended (update-permute)
+Prove one final property of the `update` function: If we update a map
+$$m$$ at two distinct keys, it doesn't matter in which order we do the
+updates.
+
+\begin{code}
+ postulate
+ update-permute : ∀ {A v1 v2} (m : TotalMap A) (x1 x2 y : Id)
+ → x1 ≢ x2 → (update (update m x2 v2) x1 v1) y
+ ≡ (update (update m x1 v1) x2 v2) y
+\end{code}
+
+
+\begin{code}
+ update-permute′ : ∀ {A v1 v2} (m : TotalMap A) (x1 x2 y : Id)
+ → x1 ≢ x2 → (update (update m x2 v2) x1 v1) y
+ ≡ (update (update m x1 v1) x2 v2) y
+ update-permute′ {A} {v1} {v2} m x1 x2 y x1≠x2
+ with x1 ≟ y | x2 ≟ y
+ ... | yes x1=y | yes x2=y = ⊥-elim (x1≠x2 (trans x1=y (sym x2=y)))
+ ... | no x1≠y | yes x2=y rewrite x2=y = update-eq′ m y
+ ... | yes x1=y | no x2≠y rewrite x1=y = sym (update-eq′ m y)
+ ... | no x1≠y | no x2≠y =
+ trans (update-neq m x2 y x2≠y) (sym (update-neq m x1 y x1≠y))
+\end{code}
+
+
+## Partial maps
+
+Finally, we define _partial maps_ on top of total maps. A partial
+map with elements of type `A` is simply a total map with elements
+of type `Maybe A` and default element `nothing`.
+
+\begin{code}
+PartialMap : Set → Set
+PartialMap A = TotalMap (Maybe A)
+\end{code}
+
+\begin{code}
+module PartialMap where
+\end{code}
+
+\begin{code}
+ empty : ∀ {A} → PartialMap A
+ empty = TotalMap.empty nothing
+\end{code}
+
+\begin{code}
+ update : ∀ {A} (m : PartialMap A) (x : Id) (v : A) → PartialMap A
+ update m x v = TotalMap.update m x (just v)
+\end{code}
+
+We can now lift all of the basic lemmas about total maps to
+partial maps.
+
+\begin{code}
+ update-eq : ∀ {A v} (m : PartialMap A) (x : Id)
+ → (update m x v) x ≡ just v
+ update-eq m x = TotalMap.update-eq m x
+\end{code}
+
+\begin{code}
+ update-neq : ∀ {A v} (m : PartialMap A) (x y : Id)
+ → x ≢ y → (update m x v) y ≡ m y
+ update-neq m x y x≠y = TotalMap.update-neq m x y x≠y
+\end{code}
+
+\begin{code}
+ update-shadow : ∀ {A v1 v2} (m : PartialMap A) (x y : Id)
+ → (update (update m x v1) x v2) y ≡ (update m x v2) y
+ update-shadow m x y = TotalMap.update-shadow m x y
+\end{code}
+
+\begin{code}
+ update-same : ∀ {A v} (m : PartialMap A) (x y : Id)
+ → m x ≡ just v
+ → (update m x v) y ≡ m y
+ update-same m x y mx=v rewrite sym mx=v = TotalMap.update-same m x y
+\end{code}
+
+\begin{code}
+ update-permute : ∀ {A v1 v2} (m : PartialMap A) (x1 x2 y : Id)
+ → x1 ≢ x2 → (update (update m x2 v2) x1 v1) y
+ ≡ (update (update m x1 v1) x2 v2) y
+ update-permute m x1 x2 y x1≠x2 = TotalMap.update-permute m x1 x2 y x1≠x2
+\end{code}
diff --git a/src/Stlc.lagda b/src/Stlc.lagda
index 67cefd6a..dcfa86bc 100644
--- a/src/Stlc.lagda
+++ b/src/Stlc.lagda
@@ -7,30 +7,22 @@ permalink : /Stlc
This chapter defines the simply-typed lambda calculus.
## Imports
-
\begin{code}
--- open import Data.Sum renaming (_⊎_ to _+_)
--- open import Data.Sum
--- open import Data.Product
--- open import Data.Nat
--- open import Data.List
-open import Data.String
--- open import Data.Bool
--- open import Relation.Binary.PropositionalEquality
--- open import Relation.Nullary.Decidable
+open import Maps using (Id; id; _≟_; PartialMap; module PartialMap)
+open PartialMap using (∅; _,_↦_)
+open import Data.String using (String)
+open import Data.Empty using (⊥; ⊥-elim)
+open import Data.Maybe using (Maybe; just; nothing)
+open import Data.Nat using (ℕ; suc; zero; _+_)
+open import Data.Bool using (Bool; true; false; if_then_else_)
+open import Relation.Nullary using (Dec; yes; no)
+open import Relation.Nullary.Decidable using (⌊_⌋)
+open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)
+-- open import Relation.Binary.Core using (Rel)
+-- open import Data.Product using (∃; ∄; _,_)
+-- open import Function using (_∘_; _$_)
\end{code}
-## Identifiers
-
-[Replace this by $Id$ from $Map$]
-
-\begin{code}
-data Id : Set where
- id : String → Id
-
-_===_ : Id → Id → Bool
-(id s) === (id t) = s == t
-\end{code}
## Syntax
@@ -39,11 +31,11 @@ Syntax of types and terms. All source terms are labeled with $ᵀ$.
\begin{code}
data Type : Set where
𝔹 : Type
- _⟶_ : Type → Type → Type
+ _⇒_ : Type → Type → Type
data Term : Set where
varᵀ : Id → Term
- λᵀ_∷_⟶_ : Id → Type → Term → Term
+ λᵀ_∈_⇒_ : Id → Type → Term → Term
_·ᵀ_ : Term → Term → Term
trueᵀ : Term
falseᵀ : Term
@@ -57,18 +49,18 @@ f = id "f"
x = id "x"
y = id "y"
-I[𝔹] I[𝔹⟶𝔹] K[𝔹][𝔹] not[𝔹] : Term
-I[𝔹] = (λᵀ x ∷ 𝔹 ⟶ (varᵀ x))
-I[𝔹⟶𝔹] = (λᵀ f ∷ (𝔹 ⟶ 𝔹) ⟶ (λᵀ x ∷ 𝔹 ⟶ ((varᵀ f) ·ᵀ (varᵀ x))))
-K[𝔹][𝔹] = (λᵀ x ∷ 𝔹 ⟶ (λᵀ y ∷ 𝔹 ⟶ (varᵀ x)))
-not[𝔹] = (λᵀ x ∷ 𝔹 ⟶ (ifᵀ (varᵀ x) then falseᵀ else trueᵀ))
+I[𝔹] I[𝔹⇒𝔹] K[𝔹][𝔹] not[𝔹] : Term
+I[𝔹] = (λᵀ x ∈ 𝔹 ⇒ (varᵀ x))
+I[𝔹⇒𝔹] = (λᵀ f ∈ (𝔹 ⇒ 𝔹) ⇒ (λᵀ x ∈ 𝔹 ⇒ ((varᵀ f) ·ᵀ (varᵀ x))))
+K[𝔹][𝔹] = (λᵀ x ∈ 𝔹 ⇒ (λᵀ y ∈ 𝔹 ⇒ (varᵀ x)))
+not[𝔹] = (λᵀ x ∈ 𝔹 ⇒ (ifᵀ (varᵀ x) then falseᵀ else trueᵀ))
\end{code}
## Values
\begin{code}
data value : Term → Set where
- value-λᵀ : ∀ x A N → value (λᵀ x ∷ A ⟶ N)
+ value-λᵀ : ∀ x A N → value (λᵀ x ∈ A ⇒ N)
value-trueᵀ : value (trueᵀ)
value-falseᵀ : value (falseᵀ)
\end{code}
@@ -77,8 +69,8 @@ data value : Term → Set where
\begin{code}
_[_:=_] : Term → Id → Term → Term
-(varᵀ x) [ y := P ] = if x === y then P else (varᵀ x)
-(λᵀ x ∷ A ⟶ N) [ y := P ] = λᵀ x ∷ A ⟶ (if x === y then N else (N [ y := P ]))
+(varᵀ x) [ y := P ] = if ⌊ x ≟ y ⌋ then P else (varᵀ x)
+(λᵀ x ∈ A ⇒ N) [ y := P ] = λᵀ x ∈ A ⇒ (if ⌊ x ≟ y ⌋ then N else (N [ y := P ]))
(L ·ᵀ M) [ y := P ] = (L [ y := P ]) ·ᵀ (M [ y := P ])
(trueᵀ) [ y := P ] = trueᵀ
(falseᵀ) [ y := P ] = falseᵀ
@@ -89,29 +81,64 @@ _[_:=_] : Term → Id → Term → Term
\begin{code}
data _⟹_ : Term → Term → Set where
- β⟶ᵀ : ∀ {x A N V} → value V →
- ((λᵀ x ∷ A ⟶ N) ·ᵀ V) ⟹ (N [ x := V ])
- κ·ᵀ₁ : ∀ {L L' M} →
+ β⇒ : ∀ {x A N V} → value V →
+ ((λᵀ x ∈ A ⇒ N) ·ᵀ V) ⟹ (N [ x := V ])
+ γ·₁ : ∀ {L L' M} →
L ⟹ L' →
(L ·ᵀ M) ⟹ (L' ·ᵀ M)
- κ·ᵀ₂ : ∀ {V M M'} → value V →
+ γ·₂ : ∀ {V M M'} → value V →
M ⟹ M' →
(V ·ᵀ M) ⟹ (V ·ᵀ M)
- βifᵀ₁ : ∀ {M N} →
+ βif₁ : ∀ {M N} →
(ifᵀ trueᵀ then M else N) ⟹ M
- βifᵀ₂ : ∀ {M N} →
+ βif₂ : ∀ {M N} →
(ifᵀ falseᵀ then M else N) ⟹ N
- κifᵀ : ∀ {L L' M N} →
+ γif : ∀ {L L' M N} →
L ⟹ L' →
(ifᵀ L then M else N) ⟹ (ifᵀ L' then M else N)
\end{code}
-## Type rules
-
-Environment : Set
-Environment = Map Type
+## Reflexive and transitive closure of a relation
\begin{code}
-data _⊢_∈_ : Environment → Term → Set where
+Rel : Set → Set₁
+Rel A = A → A → Set
+data _* {A : Set} (R : Rel A) : Rel A where
+ refl* : ∀ {x : A} → (R *) x x
+ step* : ∀ {x y : A} → R x y → (R *) x y
+ tran* : ∀ {x y z : A} → (R *) x y → (R *) y z → (R *) x z
+\end{code}
+
+\begin{code}
+_⟹*_ : Term → Term → Set
+_⟹*_ = (_⟹_) *
+\end{code}
+
+## Type rules
+
+\begin{code}
+Env : Set
+Env = PartialMap Type
+
+data _⊢_∈_ : Env → Term → Type → Set where
+ Ax : ∀ {Γ x A} →
+ Γ x ≡ just A →
+ Γ ⊢ varᵀ x ∈ A
+ ⇒-I : ∀ {Γ x N A B} →
+ (Γ , x ↦ A) ⊢ N ∈ B →
+ Γ ⊢ (λᵀ x ∈ A ⇒ N) ∈ (A ⇒ B)
+ ⇒-E : ∀ {Γ L M A B} →
+ Γ ⊢ L ∈ (A ⇒ B) →
+ Γ ⊢ M ∈ A →
+ Γ ⊢ L ·ᵀ M ∈ B
+ 𝔹-I₁ : ∀ {Γ} →
+ Γ ⊢ trueᵀ ∈ 𝔹
+ 𝔹-I₂ : ∀ {Γ} →
+ Γ ⊢ falseᵀ ∈ 𝔹
+ 𝔹-E : ∀ {Γ L M N A} →
+ Γ ⊢ L ∈ 𝔹 →
+ Γ ⊢ M ∈ A →
+ Γ ⊢ N ∈ A →
+ Γ ⊢ (ifᵀ L then M else N) ∈ A
\end{code}