completed first draft of Stlc

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
@@ -159,7 +159,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
@@ -182,18 +182,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}
 
 <div class="hidden">
 \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}
 </div>
 
@@ -288,6 +288,7 @@ updates.
 
 <div class="hidden">
 \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
@@ -295,6 +296,7 @@ updates.
   ... | 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 ρ y w z y≢z) (sym (update-neq ρ x v z x≢z))!}
+-}
 
 {-
 Holes are typed as follows. What do the "| z ≟ z" mean, and how can I deal with them?
@@ -325,15 +327,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}

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}