From 77390abcc98b18ab75171c18d91727deb009da3d Mon Sep 17 00:00:00 2001 From: Philip Wadler Date: Tue, 27 Jun 2017 14:22:52 +0100 Subject: [PATCH] publish --- out/Maps.md | 9449 ++++++++++++++++++++++++++++--------------- out/Stlc.md | 9573 ++++++++++++++++++++------------------------ out/StlcProp.md | 9485 ++++++++++++++++++++++++------------------- src/StlcProp.lagda | 30 +- 4 files changed, 15911 insertions(+), 12626 deletions(-) diff --git a/out/Maps.md b/out/Maps.md index 11087b7e..db033d23 100644 --- a/out/Maps.md +++ b/out/Maps.md @@ -11,7 +11,7 @@ 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 @@ -27,216 +27,224 @@ 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 +directly from Agda's standard library. 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. -
{% raw %}
-
+
+open import import FunctionData.Nat         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.String      using (String)
+open just; nothing)
-open import Data.Nat         using (ℕ)
-open import Relation.Nullary using (¬_; Dec; yes; no)
 open import Relation.Binary.PropositionalEquality
-{% endraw %}
+ using (_≡_; refl; _≢_; trans; sym) + + Documentation for the standard library can be found at . @@ -244,341 +252,573 @@ 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 +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. +we repeat its definition here. -
{% raw %}
-
+
+data Id : Set where
   id : ℕString → Id
-{% endraw %}
-
{% raw %}
-_≟_
+
+We recall a standard fact of logic.
+
+
+
+contrapositive : (x∀ y{ℓ₁ ℓ₂} {P : Id)Set ℓ₁} {Q : Set ℓ₂} → Dec (xP ≡→ yQ)
-id x→ ≟(¬ idQ → ¬ y with x Data.Nat.≟ yP)
 idcontrapositive p→q ¬q xp ≟= id¬q (p→q p)
+
+

+
+Using the above, we can decide equality of two identifiers
+by deciding equality on the underlying strings.
+
+
+
+_≟_ : (x y |: yesId) x=y→ rewriteDec x=y(x =≡ yes refly)
 id x ≟ id y with x Data.String.≟ y
+id x ≟ id y | noyes refl  x≠y =  yes refl
+id x ≟ id y | no  x≢y   =  no (x≠ycontrapositive ∘ id-inj x≢y)
   where
     id-inj : ∀ {x y} → id x ≡ id y → x ≡ y
     id-inj refl   =   refl
-{% endraw %}

+
+
+ +We define some identifiers for future use. + +
+
+x y z : Id
+x = id "x"
+y = id "y"
+z = id "z"
+
+
+ +## Extensionality ## Total Maps @@ -599,1038 +839,1669 @@ 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. -
{% raw %}
-
+
+TotalMap : Set → Set
 TotalMap A = Id → A
-{% endraw %}
+ + Intuitively, a total map over anfi element type $$A$$ _is_ just a function that can be used to look up ids, yielding $$A$$s. -
{% raw %}
-
+
+module TotalMap where
-{% endraw %}
-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. -
{% raw %}
-  empty : ∀ {A} → A → TotalMap A
-  empty x = λ _ → x
-{% endraw %}
+
 
-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.
-
-
{% raw %}
-  update : ∀ {A} → TotalMap A -> Id -> A -> TotalMap A
-  update m x v yalways with: x∀ ≟{A} y
-  ...→ |A yes→ TotalMap x=y = vA
   ...always |v no  x≠yx = mv
+
+

+
+More interesting is the update function, which (as before) takes
+a map $$ρ$$, a key $$x$$, and a value $$v$$ and returns a new map that
+takes $$x$$ to $$v$$ and takes every other key to whatever $$ρ$$ does.
+
+
+
+  _,_↦_ : ∀ {A} → TotalMap A → Id → A → TotalMap A
+  (ρ , x ↦ v) y with x ≟ y
+  ... | yes x=y = v
+  ... | no  x≠y = ρ y
-{% endraw %}

+
+
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. +The update function takes a _function_ $$ρ$$ and yields a new +function 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: +We define handy abbreviations for updating a map two, three, or four times. -
{% raw %}
-  examplemap
_,_↦_,_↦_ : ∀ {A} → TotalMap BoolA → Id → A → Id → A → TotalMap A
   examplemapρ , x₁ ↦ v₁ , x₂ ↦ v₂  = update   (updateρ (empty, falsex₁ ↦ v₁), (idx₂ 1)↦ false) (id 3) truev₂
-{% endraw %}

+
+  _,_↦_,_↦_,_↦_ : ∀ {A} → TotalMap A → Id → A → Id → A → Id → A → TotalMap A
+  ρ , x₁ ↦ v₁ , x₂ ↦ v₂ , x₃ ↦ v₃  =  ((ρ , x₁ ↦ v₁), x₂ ↦ v₂), x₃ ↦ v₃
+
+  _,_↦_,_↦_,_↦_,_↦_ : ∀ {A} → TotalMap A → Id → A → Id → A → Id → A → Id → A → TotalMap A
+  ρ , x₁ ↦ v₁ , x₂ ↦ v₂ , x₃ ↦ v₃ , x₄ ↦ v₄ =  (((ρ , x₁ ↦ v₁), x₂ ↦ v₂), x₃ ↦ v₃), x₄ ↦ v₄
+
+
+ +For example, we can build a map taking ids to naturals, where $$x$$ +maps to 42, $$y$$ maps to 69, and every other key maps to 0, as follows: + +
+
+  ρ₀ : TotalMap ℕ
+  ρ₀ = always 0 , x ↦ 42 , y ↦ 69
+
+
This completes the definition of total maps. Note that we don't need to define a `find` operation because it is just function application! -
{% raw %}
-  test_examplemap0
+
+  test₁ : examplemapρ₀ (idx ≡ 42
+  test₁ = refl
+
+  test₂ : ρ₀ y ≡ 69
+  test₂ = refl
+
+  test₃ : ρ₀ z ≡ 0) ≡ false
   test_examplemap0test₃ = 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
-{% endraw %}
+ 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.) +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: -
{% raw %}
-  
+
+  postulate
     apply-emptyapply-always : ∀ {A x v} (v : A) (x : Id) → emptyalways {A} v x ≡ v
-{% endraw %}
+ + #### 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 +Next, if we update a map $$ρ$$ 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$$: -
{% raw %}
-  
+
+  postulate
     update-eq : ∀ {A v} (mρ : TotalMap A) (x : Id) (v : A)
               → (updateρ m, x ↦ v) x ≡ v
-{% endraw %}
+ + #### Exercise: 2 stars, optional (update-neq) @@ -1638,948 +2509,1314 @@ 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: -
{% raw %}
-  
+
+  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
-{% endraw %}
- -#### 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$$: - -
{% raw %}
-  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
-{% endraw %}
- -