updated derivations in Stlc

src/Stlc.lagda

@@ -11,17 +11,9 @@ This chapter defines the simply-typed lambda calculus.
 open import Maps using (Id; id; _≟_; PartialMap; module PartialMap)
 open PartialMap using (∅) renaming (_,_↦_ to _,_∶_)
 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 Relation.Nullary using (Dec; yes; no)
-open import Relation.Nullary.Decidable using (⌊_⌋)
-open import Relation.Binary.PropositionalEquality as P using (_≡_; _≢_; refl)
-open import Relation.Binary using (Preorder)
-import Relation.Binary.PreorderReasoning as PreorderReasoning
--- open import Relation.Binary.Core using (Rel)
--- open import Data.Product using (∃; ∄; _,_)
--- open import Function using (_∘_; _$_)
+open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)
 \end{code}
 
 
@@ -49,21 +41,15 @@ data Term : Set where
   if_then_else_ : Term → Term → Term → Term
 \end{code}
 
-Some examples.
+Example terms.
 \begin{code}
-f x y : Id
+f x : Id
 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 two : Term 
 not =  λ[ x ∶ 𝔹 ] (if var x then false else true)
-
-check : not ≡ λ[ x ∶ 𝔹 ] (if var x then false else true)
-check = refl
+two =  λ[ f ∶ 𝔹 ⇒ 𝔹 ] λ[ x ∶ 𝔹 ] var f · (var f · var x)
 \end{code}
 
 ## Values
@@ -99,23 +85,23 @@ infix 10 _⟹_
 data _⟹_ : Term → Term → Set where
   β⇒ : ∀ {x A N V} → Value V →
     (λ[ x ∶ A ] N) · V ⟹ N [ x ∶= V ]
-  γ⇒₁ : ∀ {L L' M} →
+  γ⇒₀ : ∀ {L L' M} →
     L ⟹ L' →
     L · M ⟹ L' · M
-  γ⇒₂ : ∀ {V M M'} →
+  γ⇒₁ : ∀ {V M M'} →
     Value V →
     M ⟹ M' →
     V · M ⟹ V · M'
-  β𝔹₁ : ∀ {M N} →
+  β𝔹₀ : ∀ {M N} →
     if true then M else N ⟹ M
-  β𝔹₂ : ∀ {M N} →
+  β𝔹₁ : ∀ {M N} →
     if false then M else N ⟹ N
   γ𝔹 : ∀ {L L' M N} →
     L ⟹ L' →    
     if L then M else N ⟹ if L' then M else N
 \end{code}
 
-## Reflexive and transitive closure of a relation
+## Reflexive and transitive closure
 
 \begin{code}
 Rel : Set → Set₁
@@ -127,63 +113,52 @@ data _* {A : Set} (R : Rel A) : Rel A where
   ⟨⟩ : ∀ {x : A} → (R *) x x
   ⟨_⟩ : ∀ {x y : A} → R x y → (R *) x y
   _>>_ : ∀ {x y z : A} → (R *) x y → (R *) y z → (R *) x z
-\end{code}
 
-\begin{code}
 infix 10 _⟹*_
 
 _⟹*_ : Rel Term
 _⟹*_ = (_⟹_) *
 \end{code}
 
+## Notation for setting out reductions
+
 \begin{code}
-⟹*-Preorder : Preorder _ _ _
-⟹*-Preorder = record
-  { Carrier    = Term
-  ; _≈_        = _≡_
-  ; _∼_        = _⟹*_
-  ; isPreorder = record
-    { isEquivalence = P.isEquivalence
-    ; reflexive     = λ {refl → ⟨⟩}
-    ; trans         = _>>_
-    }
-  }
+infixr 2 _⟹⟨_⟩_
+infix  3 _∎
 
-open PreorderReasoning ⟹*-Preorder
-     using (_IsRelatedTo_; begin_; _∎) renaming (_≈⟨_⟩_ to _≡⟨_⟩_; _∼⟨_⟩_ to _⟹*⟨_⟩_)
+_⟹⟨_⟩_ : ∀ L {M N} → L ⟹ M → M ⟹* N → L ⟹* N
+L ⟹⟨ L⟹M ⟩ M⟹*N  =  ⟨ L⟹M ⟩ >> M⟹*N
 
-infixr 2 _⟹*⟪_⟫_
-
-_⟹*⟪_⟫_ : ∀ x {y z} → x ⟹ y → y IsRelatedTo z → x IsRelatedTo z
-x ⟹*⟪ x⟹y ⟫ yz  =  x ⟹*⟨ ⟨ x⟹y ⟩ ⟩ yz
+_∎ : ∀ M → M ⟹* M
+M ∎  =  ⟨⟩
 \end{code}
 
-Example evaluation.
+## Example reductions
 
 \begin{code}
 example₀ : not · true ⟹* false
 example₀ =
-  begin
     not · true
-  ⟹*⟪ β⇒ value-true ⟫
+  ⟹⟨ β⇒ value-true ⟩
     if true then false else true
-  ⟹*⟪ β𝔹₁ ⟫
+  ⟹⟨ β𝔹₀ ⟩
     false
   ∎
 
-example₁ : I² · I · (not · false) ⟹* true
+example₁ : two · not · true ⟹* true
 example₁ =
-  begin
-    I² · I · (not · false)
-  ⟹*⟪ γ⇒₁ (β⇒ value-λ) ⟫
-    (λ[ x ∶ 𝔹 ] I · var x) · (not · false)                  
-  ⟹*⟪ γ⇒₂ value-λ (β⇒ value-false) ⟫
-    (λ[ x ∶ 𝔹 ] I · var x) · (if false then false else true)
-  ⟹*⟪ γ⇒₂ value-λ β𝔹₂ ⟫
-    (λ[ x ∶ 𝔹 ] I · var x) · true
-  ⟹*⟪ β⇒ value-true ⟫
-    I · true
-  ⟹*⟪ β⇒ value-true ⟫
+    two · not · true
+  ⟹⟨ γ⇒₀ (β⇒ value-λ) ⟩
+    (λ[ x ∶ 𝔹 ] not · (not · var x)) · true
+  ⟹⟨ β⇒ value-true ⟩
+    not · (not · true)
+  ⟹⟨ γ⇒₁ value-λ (β⇒ value-true) ⟩
+    not · (if true then false else true)
+  ⟹⟨ γ⇒₁ value-λ β𝔹₀ ⟩
+    not · false
+  ⟹⟨ β⇒ value-false ⟩
+    if false then false else true
+  ⟹⟨ β𝔹₁ ⟩
     true
   ∎
 \end{code}
@@ -207,9 +182,9 @@ data _⊢_∶_ : Context → Term → Type → Set where
     Γ ⊢ L ∶ A ⇒ B →
     Γ ⊢ M ∶ A →
     Γ ⊢ L · M ∶ B
-  𝔹-I₁ : ∀ {Γ} →
+  𝔹-I₀ : ∀ {Γ} →
     Γ ⊢ true ∶ 𝔹
-  𝔹-I₂ : ∀ {Γ} →
+  𝔹-I₁ : ∀ {Γ} →
     Γ ⊢ false ∶ 𝔹
   𝔹-E : ∀ {Γ L M N A} →
     Γ ⊢ L ∶ 𝔹 →
@@ -217,3 +192,45 @@ data _⊢_∶_ : Context → Term → Type → Set where
     Γ ⊢ N ∶ A →
     Γ ⊢ if L then M else N ∶ A    
 \end{code}
+
+## Example type derivations
+
+\begin{code}
+example₂ : ∅ ⊢ not ∶ 𝔹 ⇒ 𝔹
+example₂ = ⇒-I (𝔹-E (Ax refl) 𝔹-I₁ 𝔹-I₀)
+
+example₃ : ∅ ⊢ two ∶ (𝔹 ⇒ 𝔹) ⇒ 𝔹 ⇒ 𝔹
+example₃ = ⇒-I (⇒-I (⇒-E (Ax refl) (⇒-E (Ax refl) (Ax refl))))
+\end{code}
+
+Construction of a type derivation is best done interactively.
+We start with the declaration:
+
+  `example₂ : ∅ ⊢ not ∶ 𝔹 ⇒ 𝔹`
+  `example₂ = ?`
+
+Typing control-L causes Agda to create a hole and tell us its expected type.
+
+  `example₂ = { }0`
+  `?0 : ∅ ⊢ not ∶ 𝔹 ⇒ 𝔹`
+
+Now we fill in the hole, observing that the outermost term in `not` in a `λ`,
+which is typed using `⇒-I`. The `⇒-I` rule in turn takes one argument, which
+we again specify with a hole.
+
+  `example₂ = ⇒-I { }0`
+  `?0 : ∅ , x ∶ 𝔹 ⊢ if var x then false else true ∶ 𝔹`
+
+Again we fill in the hole, observing that the outermost term is now
+`if_then_else_`, which is typed using `𝔹-E`. The `𝔹-E` rule in turn takes
+three arguments, which we again specify with holes.
+
+  `example₂ = ⇒-I (𝔹-E { }0 { }1 { }2)`
+  `?0 : ∅ , x ∶ 𝔹 ⊢ var x ∶ 𝔹`
+  `?1 : ∅ , x ∶ 𝔹 ⊢ false ∶ 𝔹`
+  `?2 : ∅ , x ∶ 𝔹 ⊢ true ∶ 𝔹`
+
+Filling in the three holes gives the derivation above.
+
+
+