{% raw %}
-data Day : Set where
+ monday : Day
+ tuesday : Day
+ wednesday : Day
+ thursday : Day
mondayfriday : Day
tuesday saturday : Day
wednesday sunday : Day
- thursday : Day
- friday : Day
- saturday : Day
- sunday : Day
{% endraw %}
@@ -212,142 +208,142 @@ Having defined `day`, we can write functions that operate on
days.
{% raw %}
-nextWeekday : Day -> Day
nextWeekday monday = tuesday
nextWeekday tuesday = wednesday
nextWeekday wednesday = thursday
nextWeekday thursday = friday
nextWeekday friday = monday
nextWeekday saturday = monday
nextWeekday sunday = monday
{% endraw %}
@@ -374,35 +370,35 @@ Second, we can record what we *expect* the result to be in the
form of an Agda type:
{% raw %}
-test_nextWeekday : nextWeekday (nextWeekday saturday) ≡ tuesday
{% endraw %}
@@ -415,15 +411,15 @@ Having made the assertion, we must also verify it. We do this by giving
a term of the above type:
{% raw %}
-test_nextWeekday = refl
{% endraw %}
diff --git a/out/Maps.md b/out/Maps.md
index a57ad529..e9ffcf73 100644
--- a/out/Maps.md
+++ b/out/Maps.md
@@ -4,8 +4,6 @@ layout : page
permalink : /Maps
---
-# Maps: Total and Partial 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
@@ -35,207 +33,207 @@ own definitions and theorems the same as their counterparts in the
standard library, wherever they overlap.
{% raw %}
-open import Function using (_∘_)
open import Data.Bool using (Bool; true; false)
+open import (Bool; true; false)
-open import Data.Empty using (⊥; ⊥-elim)
open import Data.Maybe using (Maybe; just; nothing)
open import Data.Nat using (ℕ)
+open Data.Nat using (ℕ)
-open import Relation.Nullary using (Dec; yes; no)
open import Relation.Binary.PropositionalEquality
{% endraw %}
@@ -252,103 +250,140 @@ we repeat its definition here, together with the equality comparison
function for ids and its fundamental property.
{% raw %}
-data Id : Set where
id : ℕ → Id
{% endraw %}
{% raw %}
-_≟_ : (x y : Id) → Dec (x ≡ y)
+id x :≟ (xid y :with Id) → Dec (x ≡Data.Nat.≟ y)
id x ≟ id y with| xyes Data.Nat.≟x=y rewrite yx=y = yes refl
id x ≟ id y | yes x=y≟ rewriteid y | no x≠y x=y = yesno refl
-id x ≟ id y | no x≠y = no (x≠y ∘ id-inj)
where
id-inj : ∀ → id x ≡ id y → x ≡ y
id-inj refl = refl
{% endraw %}
@@ -590,48 +588,48 @@ _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 %}
@@ -640,15 +638,15 @@ 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 %}
@@ -658,64 +656,64 @@ default element; this map always returns the default element when
applied to any id.
{% raw %}
- empty : ∀ → A → TotalMap A
empty x = λ _ → x
{% endraw %}
@@ -725,146 +723,146 @@ 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 : ∀ → TotalMap A -> Id -> A : ∀ → TotalMap A -> IdTotalMap A
+ update m x ->v Ay ->with TotalMapx A≟ y
update... m| xyes x=y = v y with
+ ... x| ≟no x≠y y
- ...= |m yes x=y = v
- ... | no x≠y = m y
{% endraw %}
@@ -878,84 +876,84 @@ For example, we can build a map taking ids to bools, where `id
like this:
{% raw %}
- examplemap : TotalMap Bool
examplemap = update (update (empty false) (id 1) false) (id (empty false) (id 1) false) (id 3) true
{% endraw %}
@@ -965,189 +963,189 @@ need to define a `find` operation because it is just function
application!
{% raw %}
- test_examplemap0 : examplemap (id 0) ≡ false
+ test_examplemap0 = 0) ≡ false
- test_examplemap0 = refl
test_examplemap1 : examplemap (id 1) ≡ false
+ test_examplemap1 = 1) ≡ false
- test_examplemap1 = refl
test_examplemap2 : examplemap (id 2) ≡ false
+ test_examplemap2 = 2) ≡ false
- test_examplemap2 = refl
test_examplemap3 : examplemap (id 3) ≡ true
test_examplemap3 = refl
{% endraw %}
@@ -1163,96 +1161,96 @@ chapter and included in the Agda standard library.)
First, the empty map returns its default element for all keys:
{% raw %}
- postulate
apply-empty : ∀ → empty v x ≡ v
{% endraw %}
{% raw %}
- apply-empty′ : ∀ → empty v x ≡ v
apply-empty′ = refl
{% endraw %}
@@ -1264,272 +1262,272 @@ and then look up $$x$$ in the map resulting from the `update`, we get
back $$v$$:
{% raw %}
- postulate
update-eq : ∀ (m : TotalMap A) (x : : ∀ (m : TotalMap A) (x : Id)
→ (update m x v) x ≡ v
{% endraw %}
{% raw %}
- update-eq′ : ∀ (m : TotalMap A) (x : : ∀ (m : TotalMap A) (x : Id)
→ (update m x v) x ≡ v
+ update-eq′ m x with x ≟ x ≡ v
update-eq′ m x with x ≟ x
- ... | yes x=x = refl
+ ... | no x≠x = ⊥-elim = refl
- ... | no x≠x = ⊥-elim (x≠x refl)
{% endraw %}
@@ -1541,211 +1539,211 @@ then look up a _different_ key $$y$$ in the resulting map, we get
the same result that $$m$$ would have given:
{% raw %}
- update-neq : ∀ (m : TotalMap A) (x y : ∀ (m : TotalMap AId)
+ → x ≢ y (x y : Id)
- → x ≢ y → (update m x v) y ≡ m y
+ update-neq m x my xx≠y v) y ≡with mx y≟ y
update-neq... m| xyes yx=y = ⊥-elim (x≠y with x ≟ y
- ... | yes x=y = ⊥-elim (x≠y x=y)
... | no _ = refl
{% endraw %}
@@ -1758,361 +1756,361 @@ to any key) as the simpler map obtained by performing just
the second `update` on $$m$$:
{% raw %}
- postulate
update-shadow : ∀ (m : TotalMap A) (x ∀y (m : TotalMap A) (x y : Id)
→ (update (update m x v1) x v2) y (update≡ (update m x v2) x v1) x v2) y ≡ (update m x v2) y
{% endraw %}
{% raw %}
- update-shadow′ : ∀ (m : TotalMap A) (x ∀y (m : TotalMap A) (x y : Id)
→ (update (update m x v1) x v2) y (update≡ (update m x v2) xy 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
{% endraw %}
@@ -2124,301 +2122,301 @@ assign key $$x$$ the same value as it already has in $$m$$, then the
result is equal to $$m$$:
{% raw %}
- postulate
update-same : ∀ (m : TotalMap A) (x y : : ∀ (m : TotalMap A) (x y : Id)
→ (update m x (m x)) y ≡ m y
{% endraw %}
{% raw %}
- update-same′ : ∀ (m : TotalMap A) (x y : : ∀ (m : TotalMap A) (x y : Id)
→ (update m x (m x)) y ≡ m y
+ update-same′ xm (m x)) y ≡ m y
- update-same′ m x y
with x ≟ y
+ ... | yes x=y rewrite x=y ≟= y
- ... | yes x=y rewrite x=y = refl
... | no x≠y = refl
{% endraw %}
@@ -2430,664 +2428,664 @@ $$m$$ at two distinct keys, it doesn't matter in which order we do the
updates.
{% raw %}
- postulate
update-permute : ∀ (m : TotalMap A) (x1 x2 y : Id)
→ x1 ≢ x2 → (update (update m x2 v2) ≢ x2x1 v1→) (update (update m x2 v2) x1 v1) y
≡ (update (update m x1 v1) x2 v2) (update (update m x1 v1) x2 v2) y
{% endraw %}
{% raw %}
- update-permute′ : ∀ (m : TotalMap A) (x1 x2 y : Id)
→ x1 ≢ x2 → (update (update m x2 v2) ≢ x2x1 v1→) (update (update m x2 v2) x1 v1) y
≡ (update (update m x1 v1) x2 v2) (update (update m x1 v1) x2 v2) y
update-permute′ m x1 x2 y x1≠x2
+ with x1 ≟ y | x1x2 x2≟ y x1≠x2
- with... x1| yes x1=y | ≟ yyes | x2x2=y ≟= y
- ...⊥-elim | yes(x1≠x2 x1=y |(trans yes x2=y = ⊥-elim (x1≠x2 (trans x1=y (sym x2=y)))
+ ... | no x1≠y | (symyes x2=y))) rewrite x2=y = update-eq′ m y
... | no x1≠y | yes x2=y rewrite x2=y =x1=y update-eq′| no x2≠y 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 mx1 x2y y x2≠y) (sym (update-neq m x1 y x1≠y))
{% endraw %}
@@ -3100,232 +3098,232 @@ map with elements of type `A` is simply a total map with elements
of type `Maybe A` and default element `nothing`.
{% raw %}
-PartialMap : Set → Set
PartialMap A = TotalMap (Maybe A)
{% endraw %}
{% raw %}
-module PartialMap where
{% endraw %}
{% raw %}
- empty : ∀ → PartialMap A
empty = TotalMap.empty nothing
{% endraw %}
{% raw %}
- update : ∀ (m : PartialMap A) (x : : Id∀) (m : PartialMap A) (x : Id) (v : A) → PartialMap A
update m x v = TotalMap.update m x (just x v = TotalMap.update m x (just v)
{% endraw %}
@@ -3334,831 +3332,831 @@ We can now lift all of the basic lemmas about total maps to
partial maps.
{% raw %}
- update-eq : ∀ (m : PartialMap A) (x : ∀ (m : PartialMap AId)
+ → (update m x : Id)
- → (update m x v) x ≡ just v
update-eq m x = TotalMap.update-eq m x
{% endraw %}
{% raw %}
- update-neq : ∀ (m : PartialMap A) (x :y ∀: (m : PartialMap AId)
+ → x ≢ y (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 = TotalMap.update-neq m x y x≠y
{% endraw %}
{% raw %}
- update-shadow : ∀ (m : PartialMap A) (x (my : PartialMapId)
+ → A) (x yupdate :(update Idm x v1)
- → x v2) y (update≡ (update m x v2) xy v1) x v2) y ≡ (update m x v2) y
update-shadow m x y = TotalMap.update-shadow m x y
{% endraw %}
{% raw %}
- update-same : ∀ (m : PartialMap A) (x :y ∀: (Id)
+ → 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 symm x mx=v = TotalMap.update-same m x y
{% endraw %}
{% raw %}
- update-permute : ∀ (m : PartialMap A) (x1 x2 y : Id)
→ x1 ≢ x2 → (update (update m x2 v2) ≢ x2x1 v1→) (update (update m x2 v2) x1 v1) y
≡ (update (update m x1 v1) x2 v2) (update (update m x1 v1) x2 v2) y
update-permute m x1 x2 y x1≠x2 = TotalMap.update-permute x1≠x2m =x1 x2 TotalMap.update-permute m x1 x2 y x1≠x2
{% endraw %}
diff --git a/out/Stlc.md b/out/Stlc.md
index 613ffdad..515f4ccb 100644
--- a/out/Stlc.md
+++ b/out/Stlc.md
@@ -24,25 +24,25 @@ permalink : /Stlc
> (Id; id; _≟_; PartialMap;module PartialMap)
{% raw %}
-data Type : Set where
+ bool : Type
+ _⇒_ : Type → Type where
- bool : Type
- _⇒_ : Type → Type → Type
infixr 5 _⇒_
{% endraw %}
@@ -531,57 +530,102 @@ so we will STLC's function type as `_⇒_`.
### Terms
{% raw %}
-data Term : Set where
+ var : Id → Term
+ app : Term where
- var : Id → Term → Term
appabs : Id → Type → Term → Term → Term
abs : Id → Type → Term → Term
- true : Term
false : Term
if_then_else_ : Term → Term → Term → Term
{% endraw %}
{% raw %}
-infixr 8 if_then_else_
{% endraw %}
@@ -728,141 +727,141 @@ We introduce $$x, y, z$$ as names for variables. The pragmas ensure
that $$id 0, id 1, id 2$$ display as $$x, y, z$$.
{% raw %}
-x = id 0
y = id 1
z = id 2
{-# DISPLAY id zero = x #-}
{-# DISPLAY id (suc zero) = y #-}
{-# DISPLAY id (suc (suc zero)) = z #-}
{% endraw %}
@@ -872,37 +871,37 @@ Some examples...
$$\text{idB} = \lambda x:bool. x$$.
{% raw %}
-idB = (abs x bool (var x))
{% endraw %}
@@ -910,49 +909,49 @@ $$\text{idB} = \lambda x:bool. x$$.
$$\text{idBB} = \lambda x:bool\rightarrow bool. x$$.
{% raw %}
-idBB = (abs x (bool ⇒ bool) (var x))
{% endraw %}
@@ -960,69 +959,69 @@ $$\text{idBB} = \lambda x:bool\rightarrow bool. x$$.
$$\text{idBBBB} = \lambda x:(bool\rightarrow bool)\rightarrow (bool\rightarrow bool). x$$.
{% raw %}
-idBBBB = (abs x ((bool ⇒ bool) ⇒ (bool ⇒ bool)) = (abs x ((bool ⇒ bool) ⇒ (bool ⇒ bool)) (var x))
{% endraw %}
@@ -1030,51 +1029,51 @@ $$\text{idBBBB} = \lambda x:(bool\rightarrow bool)\rightarrow (bool\rightarrow b
$$\text{k} = \lambda x:bool. \lambda y:bool. x$$.
{% raw %}
-k = (abs x bool (abs y bool (var x)))
{% endraw %}
@@ -1082,68 +1081,97 @@ $$\text{k} = \lambda x:bool. \lambda y:bool. x$$.
$$\text{notB} = \lambda x:bool. \text{if }x\text{ then }false\text{ else }true$$.
{% raw %}
-notB = (abs x bool (if (var x) then false else true))
{% endraw %}
{% raw %}
-{-# DISPLAY abs 0 bool (var 0) = idB #-}
+{-# DISPLAY abs 0 bool (var 0) = idB #-}
-{-# DISPLAY abs 0 (bool ⇒ bool) (var 0) = idBB #-}
{-# DISPLAY abs 0 ((bool ⇒ bool) ⇒ (bool ⇒ bool)) (var 0) = idBBBB #-}
{-# DISPLAY abs 0 bool (abs y bool (var 0)) = k #-}
{-# DISPLAY abs 0 bool (if (var 0) then false else true) = notB #-}
{% endraw %}
@@ -1388,96 +1387,96 @@ Third, for abstractions, we have a choice:
Agda makes the first choice---for example,
{% raw %}
-test_normalizeUnderLambda : (λ (x : ℕ) → 3 + 4) ≡ (λ (x : ℕ) → 7)
test_normalizeUnderLambda = refl
{% endraw %}
@@ -1488,106 +1487,106 @@ function is actually applied to an argument. We also make the
second choice here.
{% raw %}
-data Value : Term → Set where
abs : ∀ → Value (abs x A t)
+ true : Value true
+ false (abs x A t)
- true : Value true
- false : Value false
{% endraw %}
@@ -1682,617 +1681,617 @@ $$
... and formally:
{% raw %}
-[_:=_]_ : Id -> Term -> Term -> Term
[ x := v ] (var y) with x ≟ y
+... | yes x=y = v
+... (var| no x≠y = var y) with x ≟ y
...[ |x := yesv ] x=y(app =s v
-t...) = |app no x≠y([ =x := varv ] y
-[s) x([ :=x v:= ]v (app] st)
+[ t)x =:= appv ] ([ xabs :=y vA ]t) s)with ([ x :=≟ y v ]
+... t)
-[| xyes :=x=y v= ] (abs y A t)
+... with x ≟ y
-... | yesno x≠y x=y= abs y A ([ x =:= absv y] A t)
...[ |x no:= v ] x≠y true = abs ytrue A
+[ ([ x := := v ] t)false
-[ = false
+[ x := v ] true = true
-[ x := v ] false = false
-[ x := v ] (if s then t else u) =
if [ x := v ] s then [ x := v ] t else [ x [ x := v ] v ] s then [ x := v ] t else [ x := v ] u
{% endraw %}
{% raw %}
-infix 9 [_:=_]_
{% endraw %}
@@ -2316,234 +2315,234 @@ one of the constructors; your job is to fill in the rest of the constructors
and prove that the relation you've defined coincides with the function given
above.
{% raw %}
-data [_:=_]_==>_ (x : Id) (s : Term) : Term -> Term -> Set where
+ var1 Term): [ x ::= Terms ] ->(var Termx) -> Set where
- var1 : [ x := s ] (var x) ==> s
{- FILL IN HERE -}
{% endraw %}
{% raw %}
-postulate
subst-correct : ∀ s x t t'
→ [ x := s ] t ≡ t'
+ → [ x := xs := s ] t ≡ t'
- → [ x := s ] t ==> t'
{% endraw %}
@@ -2587,708 +2586,708 @@ $$
Formally:
{% raw %}
-data _==>_ : Term → Term → Set where
red : ∀ → Value t
→ app (abs x A s) t ==> [ x := t ] s
+ app1 : ∀ → ts ] s
- app1 : ∀ → s ==> s'
→ app s t ==> app s' t
app2 : ∀ → Value s
+ → t ==> t'
+ → Valueapp s st
- → t ==> t'
- → app s t ==> app s t'
if : ∀ → s ==> s'
+ → if s then t else u ==> if s'
- → then t else if s then t else u
+ iftrue : ==>∀ if s' then→ tif true then s else ut ==> s
iftrue iffalse : ∀ → if true then s else t ==> sfalse
- iffalse :then s else ∀t → if false then s else t ==> t
{% endraw %}
{% raw %}
-data Multi (R : Term → Term → Set) : Term → Term → Set where
+ refl : Term → Term → Set)∀ :-> Term →Multi TermR →x Set wherex
reflstep : ∀ -> -> Multi R x y -> Multi xR xy
- step :z ∀-> Multi -> R x y -> Multi R y z -> Multi R x z
{% endraw %}
{% raw %}
-_==>*_ : Term → Term → Set
_==>*_ = Multi _==>_
{% endraw %}
{% raw %}
-{-# DISPLAY Multi _==>_ = _==>*_ #-}
{% endraw %}
@@ -3301,69 +3300,69 @@ Example:
$$((\lambda x:bool\rightarrow bool. x) (\lambda x:bool. x)) \Longrightarrow^* (\lambda x:bool. x)$$.
{% raw %}
-step-example1 : (app idBB idB) ==>* idB
step-example1 = step (red abs)
$ refl
{% endraw %}
@@ -3373,110 +3372,110 @@ Example:
$$(\lambda x:bool\rightarrow bool. x) \;((\lambda x:bool\rightarrow bool. x)\;(\lambda x:bool. x))) \Longrightarrow^* (\lambda x:bool. x)$$.
{% raw %}
-step-example2 : (app idBB (app idBB idB)) ==>* idB
step-example2 = step (app2 abs (red abs))
+ $ step (red abs (red abs))
- $ step (red abs)
$ refl
{% endraw %}
@@ -3486,121 +3485,121 @@ Example:
$$((\lambda x:bool\rightarrow bool. x)\;(\lambda x:bool. \text{if }x\text{ then }false\text{ else }true))\;true\Longrightarrow^* false$$.
{% raw %}
-step-example3 : (app (app idBB notB) true) ==>* false
step-example3 = step (app1 (red abs))
$ step (red true)
$ step iftrue
$ refl
{% endraw %}
@@ -3610,135 +3609,135 @@ Example:
$$((\lambda x:bool\rightarrow bool. x)\;((\lambda x:bool. \text{if }x\text{ then }false\text{ else }true)\;true))\Longrightarrow^* false$$.
{% raw %}
-step-example4 : (app idBB (app notB true)) ==>* false
step-example4 = step (app2 abs (red true))
$ step (app2 abs iftrue)
$ step (red false)
$ refl
{% endraw %}
@@ -3746,52 +3745,52 @@ $$((\lambda x:bool\rightarrow bool. x)\;((\lambda x:bool. \text{if }x\text{ then
#### Exercise: 2 stars (step-example5)
{% raw %}
-postulate
step-example5 : (app (app idBBBB idBB) idB) ==>* idB
{% endraw %}
@@ -3819,125 +3818,125 @@ $$\Gamma$$ to also map $$x$$ to $$A$$." Formally, we use the function `_,_∶_`
(or "update") to add a binding to a context.
{% raw %}
-Ctxt : Set
+Ctxt = PartialMap Type
+
+∅ : Ctxt
+∅ := Set
-Ctxt = PartialMap Type
-
-∅ : Ctxt
-∅ = PartialMap.empty
_,_∶_ : Ctxt -> Id -> Type -> Ctxt
_,_∶_ = PartialMap.update
{% endraw %}
{% raw %}
-infixl 3 _,_∶_
{% endraw %}
@@ -3963,539 +3962,539 @@ the free variables of $$t$$ the ones specified in the context
$$\Gamma$$."
{% raw %}
-data _⊢_∶_ : Ctxt -> Term -> Type -> Set where
+ var : ∀ ->x Type→ ->Γ Setx where
- var :≡ just ∀A x
+ → Γ ⊢ var x Γ∶ xA ≡ just A
- → Γ ⊢ var x ∶ A
abs : ∀ → Γ , x ∶ A ⊢ s ∶ B
→ Γ ⊢ abs x A s ∶ A ⇒ B
app : ∀ → Γ ⊢ s ∶ A ⇒ B
→ Γ ⊢ t ∶ A
→ Γ ⊢ app s t ∶ B
true : ∀ → Γ ⊢ true ∶ bool
false : ∀ → Γ ⊢ false ∶ bool
if_then_else_ : ∀ → Γ ⊢ s ∶ bool
→ Γ ⊢ t ∶ A
→ Γ ⊢ u ∶ A
+ → Γ ⊢ if s then t else A
- → Γ ⊢ if s then t else u ∶ A
{% endraw %}
{% raw %}
-infix 1 _⊢_∶_
{% endraw %}
@@ -4505,68 +4504,68 @@ $$\Gamma$$."
### Examples
{% raw %}
-typing-example1 : ∅ ⊢ idB ∶ bool ⇒ bool
typing-example1 = abs (var x refl)
{% endraw %}
@@ -4576,241 +4575,241 @@ Another example:
$$\varnothing\vdash \lambda x:A. \lambda y:A\rightarrow A. y\;(y\;x) : A\rightarrow (A\rightarrow A)\rightarrow A$$.
{% raw %}
-typing-example2 : ∅ ⊢
(abs x bool
+ (abs y (bool ⇒ bool)
+ (app bool
- (absvar y )
+ (bool ⇒ bool)
- (app (var y)
- (app (var x)))))
+ ∶ (bool ⇒ (bool ⇒ bool) y)⇒ (varbool) x)))))
- ∶ (bool ⇒ (bool ⇒ bool) ⇒ bool)
typing-example2 =
(abs
(abs
(app (var y refl)
(app (var y refl) (var x refl) ))))
{% endraw %}
@@ -4821,166 +4820,166 @@ Formally prove the following typing derivation holds:
$$\exists A, \varnothing\vdash \lambda x:bool\rightarrow B. \lambda y:bool\rightarrow bool. \lambda z:bool. y\;(x\;z) : A$$.
{% raw %}
-postulate
typing-example3 : ∃ λ A → ∅ ⊢
(abs x (bool ⇒ bool)
(abs y (bool ⇒ bool)
(abs z bool
(app (var y) (app (var x) (var z)))))) ∶ A
{% endraw %}
@@ -4993,109 +4992,109 @@ to the term $$\lambda x:bool. \lambda y:bool. x\;y$$---i.e.,
$$\nexists A, \varnothing\vdash \lambda x:bool. \lambda y:bool. x\;y : A$$.
{% raw %}
-postulate
typing-nonexample1 : ∄ λ A → ∅ ⊢
(abs x bool
(abs y bool
(app (var x) (var y)))) ∶ A
{% endraw %}
@@ -5106,109 +5105,109 @@ Another nonexample:
$$\nexists A, \exists B, \varnothing\vdash \lambda x:A. x\;x : B$$.
{% raw %}
-postulate
typing-nonexample2 : ∄ λ A → ∃ λ B → ∅ ⊢
(abs x B (app (var x) (var x))) ∶ A
{% endraw %}
diff --git a/out/StlcProp.md b/out/StlcProp.md
index 19b476b7..03e546f3 100644
--- a/out/StlcProp.md
+++ b/out/StlcProp.md
@@ -4,294 +4,292 @@ layout : page
permalink : /StlcProp
---
-# Properties of STLC
-
-In this chapter, we develop the fundamental theory of the Simply
-Typed Lambda Calculus -- in particular, the type safety
-theorem.
-
{% raw %}
-open import Function using (_∘_)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.Maybe using (Maybe; just; nothing)
open import Data.Product using (∃; ∃₂; _,_; ,_)
+open import Data.Sum using (_⊎_; inj₁; inj₂)
+open import Relation.Nullary using (¬_; Dec; yes; no)
+open import importRelation.Binary.PropositionalEquality Data.Product using (∃_≡_; ∃₂_≢_; _,_; ,_)
-open import Data.Sum using (_⊎_; inj₁; inj₂)
-open import Relation.Nullary using (¬_; Dec; yes; no)
-open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl)
open import Maps
open import Stlc
{% endraw %}
{% raw %}
-CanonicalForms : Term → Type → Set
CanonicalForms t bool = t ≡ true ⊎ t bool = t ≡ true ⊎ t ≡ false
CanonicalForms t (A ⇒ B) = ∃₂ λ x t′ → t ≡ ⇒ B) = ∃₂ λ x t′ → t ≡ abs x A t′
canonicalForms : ∀ → ∅ ⊢ t ∶ A → Value t → CanonicalForms t A
canonicalForms (abs t′) abs = _ , _ (abs t′) abs = _ , _ , refl
canonicalForms true true = inj₁ refl
canonicalForms false false = inj₂ refl
{% endraw %}
@@ -620,83 +618,83 @@ straightforward extension of the progress proof we saw in the
then the formal version.
{% raw %}
-progress : ∀ → ∅ ⊢ t ∶ A → Value t ⊎ ∃ λ t′ ∶→ At → Value t ⊎ ∃ λ t′ → t ==> t′
{% endraw %}
@@ -740,568 +738,568 @@ _Proof_: By induction on the derivation of $$\vdash t : A$$.
- Otherwise, $$t_1$$ takes a step, and therefore so does $$t$$ (by `if`).
{% raw %}
-progress (var x ())
progress true = inj₁ true
progress false = inj₁ false
progress (abs t∶A) = inj₁ abs
+progress (app inj₁ abs
-progress (app t₁∶A⇒B t₂∶B)
with progress t₁∶A⇒B
+... | inj₂ (_ , t₁∶A⇒B
-...t₁⇒t₁′) |= inj₂ (_ (_ , t₁⇒t₁′) = inj₂ (_ , app1 t₁⇒t₁′)
... | inj₁ v₁
+ with progress t₂∶B
- with progress t₂∶B
... | inj₂ (_ , t₂⇒t₂′) = inj₂ (_ (_ , t₂⇒t₂′) = inj₂ (_ , app2 v₁ t₂⇒t₂′)
... | inj₁ v₂
with canonicalForms t₁∶A⇒B v₁
+... | (_ , _ t₁∶A⇒B, v₁refl) = inj₂ (_ , red v₂)
...progress | (_ , _ , refl) = inj₂ (_(if ,t₁∶bool redthen v₂)
-progresst₂∶A (ifelse t₁∶bool then t₂∶A else t₃∶A)
with progress t₁∶bool
... | inj₂ (_ , t₁⇒t₁′) = inj₂ (_ (_ , if t₁⇒t₁′) = inj₂ (_ , if t₁⇒t₁′)
... | inj₁ v₁
with canonicalForms t₁∶bool canonicalForms t₁∶bool v₁
... | inj₁ refl = inj₂ (_ , iftrue)
... | inj₂ refl = inj₂ (_ , iffalse)
{% endraw %}
@@ -1311,88 +1309,88 @@ Show that progress can also be proved by induction on terms
instead of induction on typing derivations.
{% raw %}
-postulate
progress′ : ∀ → ∅ ⊢ t ∶ A → Value t ⊎ ∃ λ t′ ∶→ At → Value t ⊎ ∃ λ t′ → t ==> t′
{% endraw %}
@@ -1452,458 +1450,458 @@ For example:
Formally:
{% raw %}
-data _FreeIn_ (x : Id) : Term → Set where
+ var : x →FreeIn Setvar wherex
varabs : x∀ FreeIn var→ xy
- abs : ∀≢ x → x FreeIn t → x y ≢ x → x FreeIn t → x FreeIn abs y A t
+ app1 : ∀ → tx
- app1 FreeIn :t₁ ∀ → x FreeIn x FreeIn t₁ → x FreeIn app t₁ t₂
app2 : ∀ → x FreeIn :t₂ ∀ → x FreeIn x FreeIn t₂ → x FreeIn app t₁ t₂
if1 : ∀ → x FreeIn t₁ → x FreeIn x(if FreeIn t₁ then →t₂ xelse FreeIn (if t₁t₃)
+ if2 : then∀ t₂ else t₃)
- if2 : ∀ → x FreeIn t₂ → x FreeIn x(if FreeInt₁ t₂then → x FreeIn (if t₁ then t₂ else t₃)
if3 : ∀ → x FreeIn t₃ → x FreeIn x(if FreeInt₁ t₃then → x FreeIn (if t₁ then t₂ else t₃)
{% endraw %}
@@ -1911,64 +1909,64 @@ Formally:
A term in which no variables appear free is said to be _closed_.
{% raw %}
-Closed : Term → Set
+Closed t = ∀ → Set
-Closed t = ∀ → ¬ (x FreeIn t)
{% endraw %}
@@ -1989,95 +1987,95 @@ well typed in context $$\Gamma$$, then it must be the case that
$$\Gamma$$ assigns a type to $$x$$.
{% raw %}
-freeInCtxt : ∀ → x FreeIn ∀t → Γ ⊢ t ∶ A x→ FreeIn∃ tλ B → Γ ⊢x t≡ ∶just A → ∃ λ B → Γ x ≡ just B
{% endraw %}
@@ -2112,474 +2110,474 @@ _Proof_: We show, by induction on the proof that $$x$$ appears
`_≟_`, noting that $$x$$ and $$y$$ are different variables.
{% raw %}
-freeInCtxt var (var _ x∶A) = (_ , var (var _ x∶A)
+freeInCtxt =(app1 (_ , x∶Ax∈t₁)
-freeInCtxt (app1 x∈t₁) (app t₁∶A _ ) = freeInCtxt x∈t₁ t₁∶A = freeInCtxt x∈t₁ t₁∶A
freeInCtxt (app2 x∈t₂) (app _ t₂∶A) = freeInCtxt x∈t₂ t₂∶A
freeInCtxt (if1 x∈t₁) (if t₁∶A then _ else _ ) = then _ else _ ) = freeInCtxt x∈t₁ t₁∶A
freeInCtxt (if2 x∈t₂) (if _ then t₂∶A else _ ) = freeInCtxt x∈t₂ t₂∶A
freeInCtxt (if3 x∈t₃) (if _ then _ else t₃∶A) = freeInCtxt x∈t₃ t₃∶A
freeInCtxt (abs y≠x x∈t) (abs t∶B)
with freeInCtxt x∈t t∶B
+... freeInCtxt x∈t t∶B
-... | x∶A
with y ≟ x
... | yes y=x = ⊥-elim (y≠x y=x)
+... =| ⊥-elim (y≠x y=x)
-... | no _ = x∶A
{% endraw %}
@@ -2590,505 +2588,533 @@ the empty context is closed (it has no free variables).
#### Exercise: 2 stars, optional (∅⊢-closed)
{% raw %}
-postulate
∅⊢-closed : ∀ → ∅ ⊢ t ∶ A → Closed t
{% endraw %}
{% raw %}
-∅⊢-closed′ : ∀ → ∅ ⊢ t ∶ A → Closed t
∅⊢-closed′ (var x ())
∅⊢-closed′ (app t₁∶A⇒B t₂∶A) (app1 x∈t₁) = ∅⊢-closed′ t₁∶A⇒B x∈t₁
+∅⊢-closed′ t₁∶A⇒B x∈t₁
-∅⊢-closed′ (app t₁∶A⇒B t₂∶A) (app2 x∈t₂) = ∅⊢-closed′ t₂∶A x∈t₂
∅⊢-closed′ true ()
∅⊢-closed′ false ()
∅⊢-closed′ (if t₁∶bool then t₂∶A else t₁∶bool then t₂∶A else t₃∶A) (if1 x∈t₁) = ∅⊢-closed′ t₁∶bool x∈t₁
∅⊢-closed′ (if t₁∶bool then t₂∶A else t₁∶bool then t₂∶A else t₃∶A) (if2 x∈t₂) = ∅⊢-closed′ t₂∶A x∈t₂
∅⊢-closed′ (if t₁∶bool then t₂∶A else t₁∶bool then t₂∶A else t₃∶A) (if3 x∈t₃) = ∅⊢-closed′ t₃∶A x∈t₃
∅⊢-closed′ (abs {x = x} t′∶A) (abs {x = x} t′∶A) (abs x≠y y∈t′) with freeInCtxt y∈t′ t′∶A
∅⊢-closed′ (abs {x = x} t′∶A) (abs {xx≠y = x} t′∶Ay∈t′) | A (abs, x≠yy∶A with x y∈t′)≟ |y
+∅⊢-closed′ A(abs , y∶A with {x ≟= y
-∅⊢-closed′x} t′∶A) (abs {xx≠y = x} t′∶Ay∈t′) | A (abs x≠y y∈t′) | A , y∶A | yes x=y = x≠y x=y
∅⊢-closed′ (abs {x = x} t′∶A) (abs {xx≠y = x} t′∶Ay∈t′) | A (abs x≠y y∈t′) | A , () | no _
{% endraw %}
@@ -3342,115 +3340,115 @@ that appear free in $$t$$. In fact, this is the only condition that
is needed.
{% raw %}
-replaceCtxt : ∀ → (∀ → x FreeIn t → Γ x → x FreeIn t → Γ x ≡ Γ′ x)
→ Γ ⊢ t ∶ A
+ → Γ′ t⊢ ∶t A
- → Γ′ ⊢ t ∶ A
{% endraw %}
@@ -3498,550 +3496,550 @@ $$\Gamma \vdash t \in T$$.
hence the desired result follows from the induction hypotheses.
{% raw %}
-replaceCtxt f (var x x∶A) rewrite f var = xvar x x∶A)
+replaceCtxt rewrite f var = var x(app x∶A
-replaceCtxt f (app t₁∶A⇒B t₂∶A)
+ = app (replaceCtxt )
- = app (replaceCtxt (f ∘ app1) t₁∶A⇒B) (replaceCtxt (f ∘ app2) t₂∶A)
replaceCtxt f (abs t′∶B)
= abs (replaceCtxt f′ t′∶B)
+ where
+ f′ : t′∶B)
- where
- f′ : ∀ → y FreeIn t′ → (Γ →, x ∶ A) y FreeIn≡ t′ → (ΓΓ′ , x ∶ , x ∶ A) y
+ f′ ≡ (Γ′ , xy∈t′ ∶ A)with y
- f′ y∈t′ with x ≟ y
... | yes _ = refl
+ ... yes| _ =no x≠y refl
- ...= f (abs x≠y | no x≠y = f (abs x≠y y∈t′)
replaceCtxt _ true = true
replaceCtxt _ false = false
replaceCtxt f (if t₁∶bool then t₂∶A else t₁∶bool then t₂∶A else t₃∶A)
= if replaceCtxt (f ∘ if1) t₁∶bool
then replaceCtxt (f ∘ if2) t₂∶A
else replaceCtxt (f ∘ if3) t₃∶A
{% endraw %}
@@ -4063,141 +4061,141 @@ _Lemma_: If $$\Gamma,x:U \vdash t : T$$ and $$\vdash v : U$$, then
$$\Gamma \vdash [x:=v]t : T$$.
{% raw %}
-[:=]-preserves-⊢ : ∀ → ∅ ⊢ v ∶ A
+ → ∶Γ A, x ∶ A ⊢ t ∶ B
→ Γ , x ∶ A ⊢ t ∶Γ B,
- → x ∶ A ⊢ [ x := v ] Γt ,∶ x ∶ A ⊢ [ x := v ] t ∶ B
{% endraw %}
@@ -4278,322 +4276,322 @@ generalization is a little tricky. The term $$t$$, on the other
hand, _is_ completely generic.
{% raw %}
-[:=]-preserves-⊢ v∶A (var y y∈Γ) with x ≟ y
... | yes x=y = {!!}
+... | |no x≠y yes x=y= = {!!}
... | no x≠y = {!!}
-[:=]-preserves-⊢ v∶A (abs t′∶B) = {!!}
[:=]-preserves-⊢ v∶A (app t₁∶A⇒B t₂∶A) =
app ([:=]-preserves-⊢ v∶A t₁∶A⇒B) ([:=]-preserves-⊢ v∶A t₂∶A)
+[:=]-preserves-⊢ t₂∶A)
-[:=]-preserves-⊢ v∶A true = true
[:=]-preserves-⊢ v∶A false = false
+[:=]-preserves-⊢ false
-[:=]-preserves-⊢ v∶A (if t₁∶bool then t₂∶B else t₁∶bool then t₂∶B else t₃∶B) =
if [:=]-preserves-⊢ v∶A t₁∶bool
then [:=]-preserves-⊢ v∶A t₂∶B
else [:=]-preserves-⊢ v∶A t₃∶B
{% endraw %}
diff --git a/src/Basics.lagda b/src/Basics.lagda
index 5eff475c..5656704e 100644
--- a/src/Basics.lagda
+++ b/src/Basics.lagda
@@ -4,13 +4,9 @@ layout : page
permalink : /Basics
---
-