diff --git a/Makefile b/Makefile index 2b486f6b..5c3f85c5 100644 --- a/Makefile +++ b/Makefile @@ -13,7 +13,7 @@ out/%.md: src/%.lagda out/ .phony: serve serve: - ruby -S gem install bundler + ruby -S gem install bundler --no-ri --no-rdoc ruby -S bundle install ruby -S bundle exec jekyll serve @@ -27,6 +27,9 @@ endif .phony: clobber clobber: clean + ruby -S gem install bundler --no-ri --no-rdoc + ruby -S bundle install + ruby -S bundle exec jekyll clean ifneq ($(strip $(markdown)),) rm $(markdown) endif diff --git a/out/Stlc.md b/out/Stlc.md index d0206ece..ad4fa3d3 100644 --- a/out/Stlc.md +++ b/out/Stlc.md @@ -375,17 +375,59 @@ This chapter defines the simply-typed lambda calculus. > 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 (_∘_; _$_) @@ -398,264 +440,264 @@ Syntax of types and terms. All source terms are labeled with $ᵀ$. 
 
-infixr 100 _⇒_
-infixl 100 _·ᵀ_
-
-data Type : Set where
-  𝔹 : Type
-  _⇒_ : Type → Type → Type
-
-data Term : Set where
-  varᵀ : Id →
+infixl Term100 _·ᵀ_
-  λᵀ_∈_⇒_data : IdType →: TypeSet → Term →where
+  𝔹 Term
-  _·ᵀ_ : Term → Term → TermType
   trueᵀ_⇒_ : TermType → Type → Type
-  falseᵀdata Term : Set where : Term
   ifᵀ_then_else_varᵀ : Id → Term
+  λᵀ_∈_⇒_ : →Id → Type → Term → Term
+  _·ᵀ_ : Term → Term → Term
+  trueᵀ : Term
+  falseᵀ : Term
+  ifᵀ_then_else_ : Term → Term → Term → Term
 
@@ -664,368 +706,368 @@ Syntax of types and terms. All source terms are labeled with $ᵀ$.
 Some examples.
 
 
-f x y : 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))) ∈ 𝔹 ⇒ (varᵀ x))
 not[𝔹]I[𝔹⇒𝔹]  =  (λᵀ xf ∈ (𝔹 ⇒ 𝔹) ⇒ (ifᵀλᵀ (varᵀ x) then∈ 𝔹 ⇒ ((varᵀ falseᵀf) else·ᵀ (varᵀ x))))
+K[𝔹][𝔹]  =  (λᵀ x ∈ 𝔹 ⇒ (λᵀ y ∈ 𝔹 ⇒ (varᵀ x)))
+not[𝔹]  =  (λᵀ x ∈ 𝔹 ⇒ (ifᵀ (varᵀ x) then falseᵀ else trueᵀ))
 
@@ -1035,138 +1077,138 @@ Some examples.
 
 
 
-data value : Term → Set where
   value-λᵀ : ∀ {x A N} → value (λᵀ x ∈ A ⇒ N)
   value-trueᵀ : value (trueᵀ)
   value-falseᵀ : value (falseᵀ)
 
@@ -1176,342 +1218,175 @@ Some examples.
 
 
 
-_[_:=_] : Term → Id → Term → Term
-(varᵀ x′) [ x := V ] with x ≟ x′
-... | yes _ = V
-... | no  _ = varᵀ x′
-(λᵀ x′ ∈ A′ ⇒Term N′)→ [ xId :=→ V ]Term with→ xTerm ≟ x′
 ...(varᵀ |x′) yes[ _x := =V λᵀ] x′with ∈x A′≟ ⇒ N′x′
 ... | |yes no  _ = = λᵀ x′ ∈ A′ ⇒ (N′ [ x := V ])
 (L′... ·ᵀ| no  _ = varᵀ x′
+(λᵀ x′ ∈ A′ ⇒ M′N′) [ x := V ] =  (L′with x [≟ x := Vx′
+... ])| ·ᵀyes (M′_ = [λᵀ xx′ :=∈ VA′ ])⇒ N′
 (trueᵀ)... [| xno  _ := V ] = λᵀ trueᵀ
-(falseᵀ)x′ ∈ A′ ⇒ (N′ [ x := V ]) = falseᵀ
 (ifᵀ L′ then·ᵀ M′) [ x := V ] M′=  (L′ else N′) [ x := xV :=]) V·ᵀ ] = ifᵀ (L′M′ [ x := [V x := V ])
+(trueᵀ) then[ x (M′ [ x := V ] = trueᵀ
+(falseᵀ) else (N′ [ x := V ] = falseᵀ
+(ifᵀ L′ then M′ else N′) [ x := V ] = ifᵀ (L′ [ x := V ]) then (M′ [ x := V ]) else (N′ [ x := V ])
 
@@ -1824,593 +1866,593 @@ Some examples.
 
 
 
-data _⟹_ : Term → Term → Set where
-  β⇒ : ∀ {x A N V} → value V →
-    ((λᵀ x ∈ A ⇒ N) ·ᵀ V) ⟹ (N [ x := V ])
-  γ⇒₁ : ∀ {L L' M} →Term
-    L → Set ⟹ L' →
-    (L ·ᵀ M) ⟹ (L' ·ᵀ M)where
   γ⇒₂β⇒ : ∀ {x A N V M M'} → value V →
     value((λᵀ x ∈ A ⇒ N) ·ᵀ V) V⟹ →
-    M(N ⟹[ x := M'V ]→)
-    (Vγ⇒₁ ·ᵀ: ∀ M){L ⟹L' (V ·ᵀ M')
-  β𝔹₁ : ∀ {M N} →
+    L ⟹ L' →
+    (L →
-    (ifᵀ·ᵀ trueᵀ then M) ⟹ (L' ·ᵀ M)
+  γ⇒₂ else N) ⟹ M
-  β𝔹₂ : ∀ {V M NM'} →
     (ifᵀvalue falseᵀV then →
+    M else N) ⟹ M' →
+    (V ·ᵀ M) ⟹ (V ·ᵀ NM')
   γ𝔹β𝔹₁ : ∀ {L L'{M M N} →
     L ⟹ L' →    
-    (ifᵀ Ltrueᵀ then M else N) then⟹ M
+  β𝔹₂ else: N)∀ ⟹{M (ifᵀ L' then M else 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)
 
@@ -2420,367 +2462,367 @@ Some examples.
 
 
 
-Rel : Set → Set₁
-Rel A = A → A → Set
-
-infixl 100 _>>_
-
-data _* {A : Set} (R : Rel A) : Rel A where
-  ⟨⟩ : ∀ {x : A}Set → (R *)Set₁ x x
-  ⟨_⟩Rel A = A :→ ∀A {x y : A} → RSet
+
+infixl x y100 → (R *) x y
-  _>>_
+
+data _* {A : : ∀ {x y z : ASet} → (R *: Rel A) x: yRel →A (R *)where
+  ⟨⟩ y: z∀ →{x (R: *A)} x→ (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
 
@@ -2788,66 +2830,66 @@ Some examples.
 
 
 
-infix 80 _⟹*_
 
 _⟹*_ : Term → Term → Set
 _⟹*_ = (_⟹_) *
 
@@ -2855,270 +2897,240 @@ Some examples.
 
 
 
-open import Relation.Binary using (Preorder)
-
-⟹*-Preorder : Preorder _ _ _
 ⟹*-Preorder = record
   { Carrier    = Term
-  ; _≈_        = _≡_
-  ; _∼_        = _⟹*_ Carrier    = Term
   ; _≈_        = _≡_
+  ; _∼_        = _⟹*_
+  ; isPreorder = record
-    { isEquivalence = P.isEquivalence
-    ; reflexive     = λ record
+    {refl →isEquivalence ⟨⟩}
-    ; trans         = _>>_P.isEquivalence
     ; reflexive     = λ {refl → ⟨⟩}
+    ; trans         = _>>_
+    }
   }
 
 open importPreorderReasoning Relation.Binary.PreorderReasoning ⟹*-Preorder
      using (begin_; _∎) renaming (_≈⟨_⟩_ to _≡⟨_⟩_; _∼⟨_⟩_ to renaming (_≈⟨_⟩_ to _≡⟨_⟩_; _∼⟨_⟩_ to _⟹*⟨_⟩_)
 
@@ -3128,1064 +3140,1064 @@ Example evaluation.
 
 
 
-example₀′ : not[𝔹] ·ᵀ trueᵀ ⟹* falseᵀ
-example₀′ =:
-  begin
-     not[𝔹] ·ᵀ trueᵀ ⟹* ·ᵀ trueᵀfalseᵀ
-  ⟹*⟨ ⟨example₀′ β⇒ value-trueᵀ ⟩ ⟩=
+  begin
     ifᵀnot[𝔹] ·ᵀ trueᵀ
+  ⟹*⟨ then⟨ falseᵀβ⇒ elsevalue-trueᵀ trueᵀ
-  ⟹*⟨ ⟨ β𝔹₁ ⟩ ⟩
     ifᵀ trueᵀ then falseᵀ else trueᵀ
   ⟹*⟨ ⟨ β𝔹₁ ⟩ ⟩
+    falseᵀ
+  ∎
 
 example₀ : (not[𝔹] ·ᵀ trueᵀ) ⟹* falseᵀ
-example₀ = ⟨ step₀ ⟩ >>trueᵀ) ⟨⟹* step₁ ⟩falseᵀ
-  where
-  M₀example₀ M₁= M₂⟨ :step₀ Term⟩ >> ⟨ step₁ ⟩
   where
+  M₀ = (not[𝔹] ·ᵀ trueᵀ) M₁ M₂ : Term
   M₁ = (ifᵀ trueᵀM₀ then= falseᵀ(not[𝔹] else·ᵀ trueᵀ)
   M₂ = falseᵀ
-  step₀ : M₀ ⟹ M₁ = (ifᵀ trueᵀ then falseᵀ else trueᵀ)
   step₀M₂ = β⇒ value-trueᵀfalseᵀ
   step₁step₀ : M₀ :⟹ M₁ ⟹ M₂
   step₁step₀ = β⇒ =value-trueᵀ
+  step₁ : M₁ ⟹ M₂
+  step₁ = β𝔹₁
 
 example₁ : (I[𝔹⇒𝔹] ·ᵀ I[𝔹] ·ᵀ (not[𝔹] ·ᵀ falseᵀ)): ⟹*(I[𝔹⇒𝔹] trueᵀ
-example₁·ᵀ I[𝔹] ·ᵀ =(not[𝔹] ⟨·ᵀ step₀falseᵀ)) ⟩ >> ⟨ step₁⟹* ⟩ >> ⟨ step₂ ⟩trueᵀ
+example₁ >>= ⟨ step₀ ⟩ >> ⟨ step₁ ⟩ >> ⟨ step₂ ⟩ >> ⟨ step₃ ⟩ >> ⟨ step₄ ⟩
-  where
-  M₀ M₁ M₂ M₃ M₄ M₅>> :⟨ Termstep₄ ⟩
   where
+  M₀ =M₁ (I[𝔹⇒𝔹]M₂ ·ᵀM₃ I[𝔹]M₄ ·ᵀM₅ (not[𝔹]: ·ᵀ falseᵀ))Term
   M₁M₀ = (I[𝔹⇒𝔹] ((λᵀ·ᵀ xI[𝔹] ∈ 𝔹·ᵀ ⇒ (I[𝔹]not[𝔹] ·ᵀ varᵀ xfalseᵀ)) ·ᵀ (not[𝔹] ·ᵀ falseᵀ))
   M₂M₁ = ((λᵀ x ∈ 𝔹 ⇒ (I[𝔹] ·ᵀ varᵀ x)) ·ᵀ ⇒ (I[𝔹]not[𝔹] ·ᵀ varᵀ xfalseᵀ)) ·ᵀ (ifᵀ falseᵀ then falseᵀ else trueᵀ))
   M₃M₂ = ((λᵀ x ∈ 𝔹 ⇒ (I[𝔹] ·ᵀ varᵀ x)) ·ᵀ (ifᵀ falseᵀ then ⇒falseᵀ (I[𝔹]else ·ᵀ varᵀ xtrueᵀ)) ·ᵀ trueᵀ)
   M₄M₃ = ((λᵀ x ∈ 𝔹 ⇒ (I[𝔹] ·ᵀ trueᵀ
-  M₅varᵀ =x)) ·ᵀ trueᵀ)
   step₀M₄ : M₀ ⟹ M₁
-  step₀ = γ⇒₁I[𝔹] ·ᵀ trueᵀ
+  M₅ = (β⇒ value-λᵀ)trueᵀ
+  step₀
-  step₁ : M₁M₀ ⟹ M₂M₁
   step₁step₀ = γ⇒₁ (β⇒ γ⇒₂ value-λᵀ (β⇒ value-falseᵀ)
   step₂step₁ : M₂M₁ ⟹ M₃M₂
   step₂step₁ = γ⇒₂ value-λᵀ β𝔹₂(β⇒ value-falseᵀ)
   step₃step₂ : M₂ ⟹ : M₃ ⟹ M₄
   step₃step₂ = γ⇒₂ value-λᵀ β𝔹₂
+  step₃ : M₃ ⟹ M₄
+  step₃ = β⇒ value-trueᵀ         
   step₄ : M₄ ⟹ M₅
   step₄ = β⇒ value-trueᵀ
 
@@ -4195,418 +4207,356 @@ Example evaluation.
 
 
 
-Context : Set
 Context = PartialMap Type
-
-infix 50 _⊢_∈_
-
-data _⊢_∈_PartialMap : ContextType → Term
+
+infix →50 Type →_⊢_∈_ Set where
-  Axdata _⊢_∈_ : ∀ {ΓContext x→ A} →Term
-    Γ x ≡ just A → Type → Set where
-    Ax : ∀ {Γ ⊢ varᵀ x ∈A} A→
-  ⇒-IΓ :x ∀≡ {Γ xjust NA A B} →
     (Γ , x ↦ A) ⊢ Nvarᵀ x ∈ A
+  ⇒-I ∈: B∀ {Γ x N A B} →
     Γ ⊢ (λᵀΓ , x ∈ A ⇒ N) ∈↦ (A) ⇒⊢ N ∈ B)
-  ⇒-E : ∀ {Γ L M A B} →
     Γ ⊢ (λᵀ x ∈ A ⇒ N) ∈ ⊢ L ∈ (A ⇒ B)
+  ⇒-E →:
-     ∀ {Γ ⊢L M ∈ A B} 
     Γ ⊢ L ·ᵀ∈ M(A ∈⇒ B
-  𝔹-I₁) :→
+    Γ ∀⊢ {Γ}M ∈ →A →
     Γ ⊢ trueᵀ⊢ L ·ᵀ M ∈ 𝔹B
   𝔹-I₂𝔹-I₁ : ∀ {Γ} →
     Γ ⊢ falseᵀ ∈trueᵀ 𝔹∈ 𝔹
   𝔹-E𝔹-I₂ : ∀ {Γ L M{Γ} N A} →
     Γ ⊢ Lfalseᵀ ∈ 𝔹 →
-    Γ𝔹-E : ⊢∀ {Γ L M ∈N A} →
     Γ ⊢ N ∈ A⊢ →L ∈ 𝔹 →
     Γ ⊢ (ifᵀM L∈ thenA M→
+    Γ else N)⊢ ∈N ∈ A →
+    Γ ⊢ (ifᵀ L then M else N) ∈ A
 
diff --git a/out/StlcProp.md b/out/StlcProp.md
index f7365f74..45a6b18f 100644
--- a/out/StlcProp.md
+++ b/out/StlcProp.md
@@ -373,7 +373,7 @@ belonging to each type.  For `bool`, these are the boolean values `true` and
       >: Term → Type  (λᵀ x ∈ A ⇒ A ⇒ canonical trueᵀ for 𝔹
@@ -524,7 +524,7 @@ belonging to each type.  For `bool`, these are the boolean values `true` and
       >canonical falseᵀ for 𝔹
@@ -586,7 +586,7 @@ belonging to each type.  For `bool`, these are the boolean values `true` and
       >∅ ⊢ L ∈ → value  (Ax  (⇒-I ) value-λᵀ  (⇒-E canonicalFormsLemma 𝔹-I₁ value-trueᵀ canonicalFormsLemma 𝔹-I₂ value-falseᵀ  (𝔹-E ∅ ⊢ M ∈ → value M ⟹  (Ax  (⇒-I inj₁ value-λᵀ
@@ -989,7 +989,7 @@ _Proof_: By induction on the derivation of `\vdash t : A`.
       > (⇒-E L′ ·ᵀ , γ⇒₁ L ·ᵀ , γ⇒₂ N [ x := M ]), β⇒ progress 𝔹-I₁ inj₁ value-trueᵀ
@@ -1376,7 +1376,7 @@ _Proof_: By induction on the derivation of `\vdash t : A`.
       >progress 𝔹-I₂ inj₁ value-falseᵀ
@@ -1399,7 +1399,7 @@ _Proof_: By induction on the derivation of `\vdash t : A`.
       > (𝔹-E  ((ifᵀ L′ then M else , γ𝔹 , β𝔹₁), β𝔹₂)∅ ⊢ M ∈ → value M ⟹ → Term  (varᵀ  (λᵀ y ∈ A ⇒ L ·ᵀ L ·ᵀ  (ifᵀ L then M else  (ifᵀ L then M else  (ifᵀ L then M else : Term Γ ⊢ M ∈  (Ax  (⇒-E  (⇒-E  (𝔹-E  (𝔹-E  (𝔹-E  (⇒-I ∅ ⊢ M ∈ ∅ ⊢ M ∈ Γ  ⊢ M ∈ Γ′ ⊢ M ∈  (Ax = Ax  {λᵀ x ∈ A ⇒  (⇒-I = ⇒-I  (⇒-E = ⇒-E Γ~Γ′ 𝔹-I₁ = 𝔹-I₁
@@ -4141,7 +4141,7 @@ _Proof_: By induction on the derivation of
       >Γ~Γ′ 𝔹-I₂ = 𝔹-I₂
@@ -4164,7 +4164,7 @@ _Proof_: By induction on the derivation of
       > (𝔹-E = 𝔹-E ) ⊢ N ∈ ∅ ⊢ V ∈ Γ ⊢ N [ x := V ]) ∈ ∅ ⊢ V ∈ Γ ⊢ V ∈  (Ax =  Ax  {λᵀ x′ ∈ A′ ⇒ A′ ⇒  (⇒-I  (⇒-I  (λᵀ x′ ∈ A′ ⇒ = ⇒-I A ⊢ N′ ∈ ) ⊢ N′ [ x := V ] ∈  (⇒-E = ⇒-E preservation-[:=] 𝔹-I₁ = 𝔹-I₁
@@ -5781,7 +5781,7 @@ We need a couple of lemmas. A closed term can be weakened to any context, and ju
       >preservation-[:=] 𝔹-I₂ = 𝔹-I₂
@@ -5804,7 +5804,7 @@ We need a couple of lemmas. A closed term can be weakened to any context, and ju
       > (𝔹-E 
   𝔹-E ∅ ⊢ M ∈ M ⟹ ∅ ⊢ N ∈  (Ax  (⇒-I  (⇒-E (⇒-I  (β⇒  (⇒-E  (γ⇒₁ = ⇒-E  (⇒-E  (γ⇒₂ = ⇒-E preservation 𝔹-I₁ preservation 𝔹-I₂  (𝔹-E 𝔹-I₁ ) β𝔹₁  (𝔹-E 𝔹-I₂ ) β𝔹₂  (𝔹-E  (γ𝔹 = 𝔹-E