tidied More
This commit is contained in:
wadler
parent
946ea31653
commit
be11228fdd
4 changed files with 289 additions and 260 deletions
|
|
@ -123,7 +123,7 @@ the term that adds two naturals:
|
|||
|
||||
plus : Term
|
||||
plus = μ "+" ⇒ ƛ "m" ⇒ ƛ "n" ⇒
|
||||
`case ` "m"
|
||||
case ` "m"
|
||||
[zero⇒ ` "n"
|
||||
|suc "m" ⇒ `suc (` "+" · ` "m" · ` "n") ]
|
||||
|
||||
|
|
@ -149,7 +149,7 @@ addition to the previous correspondences we have
|
|||
|
||||
* `` `zero `` corresponds to `⊢zero`
|
||||
* `` `suc_ `` corresponds to `⊢suc`
|
||||
* `` `case_[zero⇒_|suc_⇒_] `` corresponds to `⊢case`
|
||||
* `` case_[zero⇒_|suc_⇒_] `` corresponds to `⊢case`
|
||||
* `μ_⇒_` corresponds to `⊢μ`
|
||||
|
||||
Note the two lookup judgements `∋m` and `∋m′` refer to two
|
||||
|
|
@ -162,7 +162,7 @@ of `"n"` but accessed in different contexts, the first where
|
|||
Here is the term and its type derivation in the notation of this chapter.
|
||||
|
||||
plus : ∀ {Γ} → Γ ⊢ `ℕ ⇒ `ℕ ⇒ `ℕ
|
||||
plus = μ ƛ ƛ `case (# 1) (# 0) (`suc (# 3 · # 0 · # 1))
|
||||
plus = μ ƛ ƛ case (# 1) (# 0) (`suc (# 3 · # 0 · # 1))
|
||||
|
||||
Reading from left to right, each de Bruijn index corresponds
|
||||
to a lookup derivation:
|
||||
|
|
@ -372,7 +372,7 @@ data _⊢_ : Context → Type → Set where
|
|||
-------
|
||||
→ Γ ⊢ `ℕ
|
||||
|
||||
`caseℕ : ∀ {Γ A}
|
||||
case : ∀ {Γ A}
|
||||
→ Γ ⊢ `ℕ
|
||||
→ Γ ⊢ A
|
||||
→ Γ , `ℕ ⊢ A
|
||||
|
|
@ -476,7 +476,7 @@ two : ∀ {Γ} → Γ ⊢ `ℕ
|
|||
two = `suc `suc `zero
|
||||
|
||||
plus : ∀ {Γ} → Γ ⊢ `ℕ ⇒ `ℕ ⇒ `ℕ
|
||||
plus = μ ƛ ƛ (`caseℕ (# 1) (# 0) (`suc (# 3 · # 0 · # 1)))
|
||||
plus = μ ƛ ƛ (case (# 1) (# 0) (`suc (# 3 · # 0 · # 1)))
|
||||
|
||||
2+2 : ∅ ⊢ `ℕ
|
||||
2+2 = plus · two · two
|
||||
|
|
@ -565,7 +565,7 @@ rename ρ (ƛ N) = ƛ (rename (ext ρ) N)
|
|||
rename ρ (L · M) = (rename ρ L) · (rename ρ M)
|
||||
rename ρ (`zero) = `zero
|
||||
rename ρ (`suc M) = `suc (rename ρ M)
|
||||
rename ρ (`caseℕ L M N) = `caseℕ (rename ρ L) (rename ρ M) (rename (ext ρ) N)
|
||||
rename ρ (case L M N) = case (rename ρ L) (rename ρ M) (rename (ext ρ) N)
|
||||
rename ρ (μ N) = μ (rename (ext ρ) N)
|
||||
\end{code}
|
||||
Let `ρ` be the name of the map that takes variables in `Γ`
|
||||
|
|
@ -678,7 +678,7 @@ subst σ (ƛ N) = ƛ (subst (exts σ) N)
|
|||
subst σ (L · M) = (subst σ L) · (subst σ M)
|
||||
subst σ (`zero) = `zero
|
||||
subst σ (`suc M) = `suc (subst σ M)
|
||||
subst σ (`caseℕ L M N) = `caseℕ (subst σ L) (subst σ M) (subst (exts σ) N)
|
||||
subst σ (case L M N) = case (subst σ L) (subst σ M) (subst (exts σ) N)
|
||||
subst σ (μ N) = μ (subst (exts σ) N)
|
||||
\end{code}
|
||||
Let `σ` be the name of the map that takes variables in `Γ`
|
||||
|
|
@ -843,16 +843,16 @@ data _—→_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
|
|||
ξ-case : ∀ {Γ A} {L L′ : Γ ⊢ `ℕ} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
|
||||
→ L —→ L′
|
||||
--------------------------
|
||||
→ `caseℕ L M N —→ `caseℕ L′ M N
|
||||
→ case L M N —→ case L′ M N
|
||||
|
||||
β-zero : ∀ {Γ A} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
|
||||
-------------------
|
||||
→ `caseℕ `zero M N —→ M
|
||||
→ case `zero M N —→ M
|
||||
|
||||
β-suc : ∀ {Γ A} {V : Γ ⊢ `ℕ} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
|
||||
→ Value V
|
||||
-----------------------------
|
||||
→ `caseℕ (`suc V) M N —→ N [ V ]
|
||||
→ case (`suc V) M N —→ N [ V ]
|
||||
|
||||
β-μ : ∀ {Γ A} {N : Γ , A ⊢ A}
|
||||
---------------
|
||||
|
|
@ -875,9 +875,9 @@ The reflexive and transitive closure is exactly as before.
|
|||
We simply cut-and-paste the previous definition.
|
||||
\begin{code}
|
||||
infix 2 _—↠_
|
||||
infix 1 begin_
|
||||
infix 1 begin_
|
||||
infixr 2 _—→⟨_⟩_
|
||||
infix 3 _∎
|
||||
infix 3 _∎
|
||||
|
||||
data _—↠_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
|
||||
|
||||
|
|
@ -891,7 +891,10 @@ data _—↠_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
|
|||
---------
|
||||
→ L —↠ N
|
||||
|
||||
begin_ : ∀ {Γ} {A} {M N : Γ ⊢ A} → (M —↠ N) → (M —↠ N)
|
||||
begin_ : ∀ {Γ} {A} {M N : Γ ⊢ A}
|
||||
→ M —↠ N
|
||||
------
|
||||
→ M —↠ N
|
||||
begin M—↠N = M—↠N
|
||||
\end{code}
|
||||
|
||||
|
|
@ -924,29 +927,29 @@ _ : plus {∅} · two · two —↠ `suc `suc `suc `suc `zero
|
|||
_ =
|
||||
plus · two · two
|
||||
—→⟨ ξ-·₁ (ξ-·₁ β-μ) ⟩
|
||||
(ƛ ƛ `caseℕ (` S Z) (` Z) (`suc (plus · ` Z · ` S Z))) · two · two
|
||||
(ƛ ƛ case (` S Z) (` Z) (`suc (plus · ` Z · ` S Z))) · two · two
|
||||
—→⟨ ξ-·₁ (β-ƛ (V-suc (V-suc V-zero))) ⟩
|
||||
(ƛ `caseℕ two (` Z) (`suc (plus · ` Z · ` S Z))) · two
|
||||
(ƛ case two (` Z) (`suc (plus · ` Z · ` S Z))) · two
|
||||
—→⟨ β-ƛ (V-suc (V-suc V-zero)) ⟩
|
||||
`caseℕ two two (`suc (plus · ` Z · two))
|
||||
case two two (`suc (plus · ` Z · two))
|
||||
—→⟨ β-suc (V-suc V-zero) ⟩
|
||||
`suc (plus · `suc `zero · two)
|
||||
—→⟨ ξ-suc (ξ-·₁ (ξ-·₁ β-μ)) ⟩
|
||||
`suc ((ƛ ƛ `caseℕ (` S Z) (` Z) (`suc (plus · ` Z · ` S Z)))
|
||||
`suc ((ƛ ƛ case (` S Z) (` Z) (`suc (plus · ` Z · ` S Z)))
|
||||
· `suc `zero · two)
|
||||
—→⟨ ξ-suc (ξ-·₁ (β-ƛ (V-suc V-zero))) ⟩
|
||||
`suc ((ƛ `caseℕ (`suc `zero) (` Z) (`suc (plus · ` Z · ` S Z))) · two)
|
||||
`suc ((ƛ case (`suc `zero) (` Z) (`suc (plus · ` Z · ` S Z))) · two)
|
||||
—→⟨ ξ-suc (β-ƛ (V-suc (V-suc V-zero))) ⟩
|
||||
`suc (`caseℕ (`suc `zero) (two) (`suc (plus · ` Z · two)))
|
||||
`suc (case (`suc `zero) (two) (`suc (plus · ` Z · two)))
|
||||
—→⟨ ξ-suc (β-suc V-zero) ⟩
|
||||
`suc (`suc (plus · `zero · two))
|
||||
—→⟨ ξ-suc (ξ-suc (ξ-·₁ (ξ-·₁ β-μ))) ⟩
|
||||
`suc (`suc ((ƛ ƛ `caseℕ (` S Z) (` Z) (`suc (plus · ` Z · ` S Z)))
|
||||
`suc (`suc ((ƛ ƛ case (` S Z) (` Z) (`suc (plus · ` Z · ` S Z)))
|
||||
· `zero · two))
|
||||
—→⟨ ξ-suc (ξ-suc (ξ-·₁ (β-ƛ V-zero))) ⟩
|
||||
`suc (`suc ((ƛ `caseℕ `zero (` Z) (`suc (plus · ` Z · ` S Z))) · two))
|
||||
`suc (`suc ((ƛ case `zero (` Z) (`suc (plus · ` Z · ` S Z))) · two))
|
||||
—→⟨ ξ-suc (ξ-suc (β-ƛ (V-suc (V-suc V-zero)))) ⟩
|
||||
`suc (`suc (`caseℕ `zero (two) (`suc (plus · ` Z · two))))
|
||||
`suc (`suc (case `zero (two) (`suc (plus · ` Z · two))))
|
||||
—→⟨ ξ-suc (ξ-suc β-zero) ⟩
|
||||
`suc (`suc (`suc (`suc `zero)))
|
||||
∎
|
||||
|
|
@ -1045,7 +1048,7 @@ progress (`zero) = done V-zero
|
|||
progress (`suc M) with progress M
|
||||
... | step M—→M′ = step (ξ-suc M—→M′)
|
||||
... | done VM = done (V-suc VM)
|
||||
progress (`caseℕ L M N) with progress L
|
||||
progress (case L M N) with progress L
|
||||
... | step L—→L′ = step (ξ-case L—→L′)
|
||||
... | done V-zero = step (β-zero)
|
||||
... | done (V-suc VL) = step (β-suc VL)
|
||||
|
|
@ -1148,40 +1151,40 @@ _ : eval (gas 100) (plus · two · two) ≡
|
|||
((μ
|
||||
(ƛ
|
||||
(ƛ
|
||||
`caseℕ (` (S Z)) (` Z) (`suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
|
||||
case (` (S Z)) (` Z) (`suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
|
||||
· `suc (`suc `zero)
|
||||
· `suc (`suc `zero)
|
||||
—→⟨ ξ-·₁ (ξ-·₁ β-μ) ⟩
|
||||
(ƛ
|
||||
(ƛ
|
||||
`caseℕ (` (S Z)) (` Z)
|
||||
case (` (S Z)) (` Z)
|
||||
(`suc
|
||||
((μ
|
||||
(ƛ
|
||||
(ƛ
|
||||
`caseℕ (` (S Z)) (` Z) (`suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
|
||||
case (` (S Z)) (` Z) (`suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
|
||||
· ` Z
|
||||
· ` (S Z)))))
|
||||
· `suc (`suc `zero)
|
||||
· `suc (`suc `zero)
|
||||
—→⟨ ξ-·₁ (β-ƛ (V-suc (V-suc V-zero))) ⟩
|
||||
(ƛ
|
||||
`caseℕ (`suc (`suc `zero)) (` Z)
|
||||
case (`suc (`suc `zero)) (` Z)
|
||||
(`suc
|
||||
((μ
|
||||
(ƛ
|
||||
(ƛ
|
||||
`caseℕ (` (S Z)) (` Z) (`suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
|
||||
case (` (S Z)) (` Z) (`suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
|
||||
· ` Z
|
||||
· ` (S Z))))
|
||||
· `suc (`suc `zero)
|
||||
—→⟨ β-ƛ (V-suc (V-suc V-zero)) ⟩
|
||||
`caseℕ (`suc (`suc `zero)) (`suc (`suc `zero))
|
||||
case (`suc (`suc `zero)) (`suc (`suc `zero))
|
||||
(`suc
|
||||
((μ
|
||||
(ƛ
|
||||
(ƛ
|
||||
`caseℕ (` (S Z)) (` Z) (`suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
|
||||
case (` (S Z)) (` Z) (`suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
|
||||
· ` Z
|
||||
· `suc (`suc `zero)))
|
||||
—→⟨ β-suc (V-suc V-zero) ⟩
|
||||
|
|
@ -1189,19 +1192,19 @@ _ : eval (gas 100) (plus · two · two) ≡
|
|||
((μ
|
||||
(ƛ
|
||||
(ƛ
|
||||
`caseℕ (` (S Z)) (` Z) (`suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
|
||||
case (` (S Z)) (` Z) (`suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
|
||||
· `suc `zero
|
||||
· `suc (`suc `zero))
|
||||
—→⟨ ξ-suc (ξ-·₁ (ξ-·₁ β-μ)) ⟩
|
||||
`suc
|
||||
((ƛ
|
||||
(ƛ
|
||||
`caseℕ (` (S Z)) (` Z)
|
||||
case (` (S Z)) (` Z)
|
||||
(`suc
|
||||
((μ
|
||||
(ƛ
|
||||
(ƛ
|
||||
`caseℕ (` (S Z)) (` Z) (`suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
|
||||
case (` (S Z)) (` Z) (`suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
|
||||
· ` Z
|
||||
· ` (S Z)))))
|
||||
· `suc `zero
|
||||
|
|
@ -1209,23 +1212,23 @@ _ : eval (gas 100) (plus · two · two) ≡
|
|||
—→⟨ ξ-suc (ξ-·₁ (β-ƛ (V-suc V-zero))) ⟩
|
||||
`suc
|
||||
((ƛ
|
||||
`caseℕ (`suc `zero) (` Z)
|
||||
case (`suc `zero) (` Z)
|
||||
(`suc
|
||||
((μ
|
||||
(ƛ
|
||||
(ƛ
|
||||
`caseℕ (` (S Z)) (` Z) (`suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
|
||||
case (` (S Z)) (` Z) (`suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
|
||||
· ` Z
|
||||
· ` (S Z))))
|
||||
· `suc (`suc `zero))
|
||||
—→⟨ ξ-suc (β-ƛ (V-suc (V-suc V-zero))) ⟩
|
||||
`suc
|
||||
`caseℕ (`suc `zero) (`suc (`suc `zero))
|
||||
case (`suc `zero) (`suc (`suc `zero))
|
||||
(`suc
|
||||
((μ
|
||||
(ƛ
|
||||
(ƛ
|
||||
`caseℕ (` (S Z)) (` Z) (`suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
|
||||
case (` (S Z)) (` Z) (`suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
|
||||
· ` Z
|
||||
· `suc (`suc `zero)))
|
||||
—→⟨ ξ-suc (β-suc V-zero) ⟩
|
||||
|
|
@ -1234,7 +1237,7 @@ _ : eval (gas 100) (plus · two · two) ≡
|
|||
((μ
|
||||
(ƛ
|
||||
(ƛ
|
||||
`caseℕ (` (S Z)) (` Z) (`suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
|
||||
case (` (S Z)) (` Z) (`suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
|
||||
· `zero
|
||||
· `suc (`suc `zero)))
|
||||
—→⟨ ξ-suc (ξ-suc (ξ-·₁ (ξ-·₁ β-μ))) ⟩
|
||||
|
|
@ -1242,12 +1245,12 @@ _ : eval (gas 100) (plus · two · two) ≡
|
|||
(`suc
|
||||
((ƛ
|
||||
(ƛ
|
||||
`caseℕ (` (S Z)) (` Z)
|
||||
case (` (S Z)) (` Z)
|
||||
(`suc
|
||||
((μ
|
||||
(ƛ
|
||||
(ƛ
|
||||
`caseℕ (` (S Z)) (` Z) (`suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
|
||||
case (` (S Z)) (` Z) (`suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
|
||||
· ` Z
|
||||
· ` (S Z)))))
|
||||
· `zero
|
||||
|
|
@ -1256,24 +1259,24 @@ _ : eval (gas 100) (plus · two · two) ≡
|
|||
`suc
|
||||
(`suc
|
||||
((ƛ
|
||||
`caseℕ `zero (` Z)
|
||||
case `zero (` Z)
|
||||
(`suc
|
||||
((μ
|
||||
(ƛ
|
||||
(ƛ
|
||||
`caseℕ (` (S Z)) (` Z) (`suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
|
||||
case (` (S Z)) (` Z) (`suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
|
||||
· ` Z
|
||||
· ` (S Z))))
|
||||
· `suc (`suc `zero)))
|
||||
—→⟨ ξ-suc (ξ-suc (β-ƛ (V-suc (V-suc V-zero)))) ⟩
|
||||
`suc
|
||||
(`suc
|
||||
`caseℕ `zero (`suc (`suc `zero))
|
||||
case `zero (`suc (`suc `zero))
|
||||
(`suc
|
||||
((μ
|
||||
(ƛ
|
||||
(ƛ
|
||||
`caseℕ (` (S Z)) (` Z) (`suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
|
||||
case (` (S Z)) (` Z) (`suc (` (S (S (S Z))) · ` Z · ` (S Z))))))
|
||||
· ` Z
|
||||
· `suc (`suc `zero))))
|
||||
—→⟨ ξ-suc (ξ-suc β-zero) ⟩ `suc (`suc (`suc (`suc `zero))) ∎)
|
||||
|
|
|
|||
|
|
@ -79,7 +79,7 @@ Three are for the naturals:
|
|||
|
||||
* Zero `` `zero ``
|
||||
* Successor `` `suc ``
|
||||
* Case `` `case L [zero⇒ M |suc x ⇒ N ] ``
|
||||
* Case `` case L [zero⇒ M |suc x ⇒ N ] ``
|
||||
|
||||
And one is for recursion:
|
||||
|
||||
|
|
@ -99,7 +99,7 @@ Here is the syntax of terms in BNF.
|
|||
|
||||
L, M, N ::=
|
||||
` x | ƛ x ⇒ N | L · M |
|
||||
`zero | `suc M | `case L [zero⇒ M |suc x ⇒ N] |
|
||||
`zero | `suc M | case L [zero⇒ M |suc x ⇒ N] |
|
||||
μ x ⇒ M
|
||||
|
||||
And here it is formalised in Agda.
|
||||
|
|
@ -119,7 +119,7 @@ data Term : Set where
|
|||
_·_ : Term → Term → Term
|
||||
`zero : Term
|
||||
`suc_ : Term → Term
|
||||
`case_[zero⇒_|suc_⇒_] : Term → Term → Id → Term → Term
|
||||
case_[zero⇒_|suc_⇒_] : Term → Term → Id → Term → Term
|
||||
μ_⇒_ : Id → Term → Term
|
||||
\end{code}
|
||||
We represent identifiers by strings. We choose precedence so that
|
||||
|
|
@ -139,7 +139,7 @@ two = `suc `suc `zero
|
|||
|
||||
plus : Term
|
||||
plus = μ "+" ⇒ ƛ "m" ⇒ ƛ "n" ⇒
|
||||
`case ` "m"
|
||||
case ` "m"
|
||||
[zero⇒ ` "n"
|
||||
|suc "m" ⇒ `suc (` "+" · ` "m" · ` "n") ]
|
||||
|
||||
|
|
@ -273,7 +273,7 @@ Case and recursion also introduce bound variables, which are also subject
|
|||
to alpha renaming. In the term
|
||||
|
||||
μ "+" ⇒ ƛ "m" ⇒ ƛ "n" ⇒
|
||||
`case ` "m"
|
||||
case ` "m"
|
||||
[zero⇒ ` "n"
|
||||
|suc "m" ⇒ `suc (` "+" · ` "m" · ` "n") ]
|
||||
|
||||
|
|
@ -281,7 +281,7 @@ notice that there are two binding occurrences of `m`, one in the first
|
|||
line and one in the last line. It is equivalent to the following term,
|
||||
|
||||
μ "plus" ⇒ ƛ "x" ⇒ ƛ "y" ⇒
|
||||
`case ` "x"
|
||||
case ` "x"
|
||||
[zero⇒ ` "y"
|
||||
|suc "x′" ⇒ `suc (` "plus" · ` "x′" · ` "y") ]
|
||||
|
||||
|
|
@ -416,9 +416,9 @@ N ⟨ x ⟩[ y := V ] with x ≟ y
|
|||
(L · M) [ y := V ] = (L [ y := V ]) · (M [ y := V ])
|
||||
(`zero) [ y := V ] = `zero
|
||||
(`suc M) [ y := V ] = `suc (M [ y := V ])
|
||||
(`case L
|
||||
(case L
|
||||
[zero⇒ M
|
||||
|suc x ⇒ N ]) [ y := V ] = `case L [ y := V ]
|
||||
|suc x ⇒ N ]) [ y := V ] = case L [ y := V ]
|
||||
[zero⇒ M [ y := V ]
|
||||
|suc x ⇒ N ⟨ x ⟩[ y := V ] ]
|
||||
(μ x ⇒ N) [ y := V ] = μ x ⇒ (N ⟨ x ⟩[ y := V ])
|
||||
|
|
@ -551,16 +551,16 @@ data _—→_ : Term → Term → Set where
|
|||
ξ-case : ∀ {x L L′ M N}
|
||||
→ L —→ L′
|
||||
-----------------------------------------------------------------
|
||||
→ `case L [zero⇒ M |suc x ⇒ N ] —→ `case L′ [zero⇒ M |suc x ⇒ N ]
|
||||
→ case L [zero⇒ M |suc x ⇒ N ] —→ case L′ [zero⇒ M |suc x ⇒ N ]
|
||||
|
||||
β-zero : ∀ {x M N}
|
||||
----------------------------------------
|
||||
→ `case `zero [zero⇒ M |suc x ⇒ N ] —→ M
|
||||
→ case `zero [zero⇒ M |suc x ⇒ N ] —→ M
|
||||
|
||||
β-suc : ∀ {x V M N}
|
||||
→ Value V
|
||||
---------------------------------------------------
|
||||
→ `case `suc V [zero⇒ M |suc x ⇒ N ] —→ N [ x := V ]
|
||||
→ case `suc V [zero⇒ M |suc x ⇒ N ] —→ N [ x := V ]
|
||||
|
||||
β-μ : ∀ {x M}
|
||||
------------------------------
|
||||
|
|
@ -631,7 +631,10 @@ data _—↠_ : Term → Term → Set where
|
|||
---------
|
||||
→ L —↠ N
|
||||
|
||||
begin_ : ∀ {M N} → (M —↠ N) → (M —↠ N)
|
||||
begin_ : ∀ {M N}
|
||||
→ M —↠ N
|
||||
------
|
||||
→ M —↠ N
|
||||
begin M—↠N = M—↠N
|
||||
\end{code}
|
||||
We can read this as follows.
|
||||
|
|
@ -655,17 +658,17 @@ data _—↠′_ : Term → Term → Set where
|
|||
|
||||
step : ∀ {M N}
|
||||
→ M —→ N
|
||||
------
|
||||
-------
|
||||
→ M —↠′ N
|
||||
|
||||
refl : ∀ {M}
|
||||
------
|
||||
-------
|
||||
→ M —↠′ M
|
||||
|
||||
trans : ∀ {L M N}
|
||||
→ L —↠′ M
|
||||
→ M —↠′ N
|
||||
------
|
||||
-------
|
||||
→ L —↠′ N
|
||||
\end{code}
|
||||
The three constructors specify, respectively, that `—↠` includes `—→`
|
||||
|
|
@ -752,38 +755,38 @@ _ =
|
|||
plus · two · two
|
||||
—→⟨ ξ-·₁ (ξ-·₁ β-μ) ⟩
|
||||
(ƛ "m" ⇒ ƛ "n" ⇒
|
||||
`case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ])
|
||||
case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ])
|
||||
· two · two
|
||||
—→⟨ ξ-·₁ (β-ƛ (V-suc (V-suc V-zero))) ⟩
|
||||
(ƛ "n" ⇒
|
||||
`case two [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ])
|
||||
case two [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ])
|
||||
· two
|
||||
—→⟨ β-ƛ (V-suc (V-suc V-zero)) ⟩
|
||||
`case two [zero⇒ two |suc "m" ⇒ `suc (plus · ` "m" · two) ]
|
||||
case two [zero⇒ two |suc "m" ⇒ `suc (plus · ` "m" · two) ]
|
||||
—→⟨ β-suc (V-suc V-zero) ⟩
|
||||
`suc (plus · `suc `zero · two)
|
||||
—→⟨ ξ-suc (ξ-·₁ (ξ-·₁ β-μ)) ⟩
|
||||
`suc ((ƛ "m" ⇒ ƛ "n" ⇒
|
||||
`case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ])
|
||||
case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ])
|
||||
· `suc `zero · two)
|
||||
—→⟨ ξ-suc (ξ-·₁ (β-ƛ (V-suc V-zero))) ⟩
|
||||
`suc ((ƛ "n" ⇒
|
||||
`case `suc `zero [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ])
|
||||
case `suc `zero [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ])
|
||||
· two)
|
||||
—→⟨ ξ-suc (β-ƛ (V-suc (V-suc V-zero))) ⟩
|
||||
`suc (`case `suc `zero [zero⇒ two |suc "m" ⇒ `suc (plus · ` "m" · two) ])
|
||||
`suc (case `suc `zero [zero⇒ two |suc "m" ⇒ `suc (plus · ` "m" · two) ])
|
||||
—→⟨ ξ-suc (β-suc V-zero) ⟩
|
||||
`suc `suc (plus · `zero · two)
|
||||
—→⟨ ξ-suc (ξ-suc (ξ-·₁ (ξ-·₁ β-μ))) ⟩
|
||||
`suc `suc ((ƛ "m" ⇒ ƛ "n" ⇒
|
||||
`case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ])
|
||||
case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ])
|
||||
· `zero · two)
|
||||
—→⟨ ξ-suc (ξ-suc (ξ-·₁ (β-ƛ V-zero))) ⟩
|
||||
`suc `suc ((ƛ "n" ⇒
|
||||
`case `zero [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ])
|
||||
case `zero [zero⇒ ` "n" |suc "m" ⇒ `suc (plus · ` "m" · ` "n") ])
|
||||
· two)
|
||||
—→⟨ ξ-suc (ξ-suc (β-ƛ (V-suc (V-suc V-zero)))) ⟩
|
||||
`suc `suc (`case `zero [zero⇒ two |suc "m" ⇒ `suc (plus · ` "m" · two) ])
|
||||
`suc `suc (case `zero [zero⇒ two |suc "m" ⇒ `suc (plus · ` "m" · two) ])
|
||||
—→⟨ ξ-suc (ξ-suc β-zero) ⟩
|
||||
`suc (`suc (`suc (`suc `zero)))
|
||||
∎
|
||||
|
|
@ -1032,7 +1035,7 @@ data _⊢_⦂_ : Context → Term → Type → Set where
|
|||
→ Γ ⊢ M ⦂ A
|
||||
→ Γ , x ⦂ `ℕ ⊢ N ⦂ A
|
||||
-------------------------------------
|
||||
→ Γ ⊢ `case L [zero⇒ M |suc x ⇒ N ] ⦂ A
|
||||
→ Γ ⊢ case L [zero⇒ M |suc x ⇒ N ] ⦂ A
|
||||
|
||||
⊢μ : ∀ {Γ x M A}
|
||||
→ Γ , x ⦂ A ⊢ M ⦂ A
|
||||
|
|
|
|||
|
|
@ -15,7 +15,7 @@ more datatypes, including products, sums, unit type, empty
|
|||
type, and lists, all of which will be familiar from Part I of
|
||||
this textbook. We also describe _let_ bindings. Most of the
|
||||
description will be informal. We show how to formalise a few
|
||||
of the constructs, but leave the rest as an exercise for the
|
||||
of the constructs, and leave the rest as an exercise for the
|
||||
reader.
|
||||
|
||||
## Imports
|
||||
|
|
@ -46,13 +46,16 @@ infixr 9 _`×_
|
|||
|
||||
infix 5 ƛ_
|
||||
infix 5 μ_
|
||||
infix 6 _`∷_
|
||||
infixr 6 _`∷_
|
||||
infixl 7 _·_
|
||||
infix 8 `suc_
|
||||
infix 9 `_
|
||||
infix 9 S_
|
||||
infix 9 #_
|
||||
|
||||
infixr 6 _V-∷_
|
||||
infix 8 V-suc_
|
||||
|
||||
data Type : Set where
|
||||
`ℕ : Type
|
||||
_⇒_ : Type → Type → Type
|
||||
|
|
@ -68,47 +71,47 @@ data Context : Set where
|
|||
|
||||
data _∋_ : Context → Type → Set where
|
||||
|
||||
Z : ∀ {Γ} {A}
|
||||
----------
|
||||
Z : ∀ {Γ A}
|
||||
---------
|
||||
→ Γ , A ∋ A
|
||||
|
||||
S_ : ∀ {Γ} {A B}
|
||||
S_ : ∀ {Γ A B}
|
||||
→ Γ ∋ B
|
||||
---------
|
||||
→ Γ , A ∋ B
|
||||
|
||||
data _⊢_ : Context → Type → Set where
|
||||
|
||||
`_ : ∀ {Γ} {A}
|
||||
`_ : ∀ {Γ A}
|
||||
→ Γ ∋ A
|
||||
------
|
||||
-----
|
||||
→ Γ ⊢ A
|
||||
|
||||
ƛ_ : ∀ {Γ} {A B}
|
||||
ƛ_ : ∀ {Γ A B}
|
||||
→ Γ , A ⊢ B
|
||||
----------
|
||||
---------
|
||||
→ Γ ⊢ A ⇒ B
|
||||
|
||||
_·_ : ∀ {Γ} {A B}
|
||||
_·_ : ∀ {Γ A B}
|
||||
→ Γ ⊢ A ⇒ B
|
||||
→ Γ ⊢ A
|
||||
----------
|
||||
---------
|
||||
→ Γ ⊢ B
|
||||
|
||||
`zero : ∀ {Γ}
|
||||
----------
|
||||
------
|
||||
→ Γ ⊢ `ℕ
|
||||
|
||||
`suc_ : ∀ {Γ}
|
||||
→ Γ ⊢ `ℕ
|
||||
-------
|
||||
------
|
||||
→ Γ ⊢ `ℕ
|
||||
|
||||
`caseℕ : ∀ {Γ A}
|
||||
case : ∀ {Γ A}
|
||||
→ Γ ⊢ `ℕ
|
||||
→ Γ ⊢ A
|
||||
→ Γ , `ℕ ⊢ A
|
||||
-----------
|
||||
-----
|
||||
→ Γ ⊢ A
|
||||
|
||||
μ_ : ∀ {Γ A}
|
||||
|
|
@ -142,7 +145,7 @@ data _⊢_ : Context → Type → Set where
|
|||
-----------
|
||||
→ Γ ⊢ A `⊎ B
|
||||
|
||||
`case⊎ : ∀ {Γ A B C}
|
||||
case⊎ : ∀ {Γ A B C}
|
||||
→ Γ ⊢ A `⊎ B
|
||||
→ Γ , A ⊢ C
|
||||
→ Γ , B ⊢ C
|
||||
|
|
@ -153,7 +156,7 @@ data _⊢_ : Context → Type → Set where
|
|||
------
|
||||
→ Γ ⊢ `⊤
|
||||
|
||||
`case⊥ : ∀ {Γ A}
|
||||
case⊥ : ∀ {Γ A}
|
||||
→ Γ ⊢ `⊥
|
||||
-------
|
||||
→ Γ ⊢ A
|
||||
|
|
@ -168,7 +171,7 @@ data _⊢_ : Context → Type → Set where
|
|||
------------
|
||||
→ Γ ⊢ `List A
|
||||
|
||||
`caseL : ∀ {Γ A B}
|
||||
caseL : ∀ {Γ A B}
|
||||
→ Γ ⊢ `List A
|
||||
→ Γ ⊢ B
|
||||
→ Γ , A , `List A ⊢ B
|
||||
|
|
@ -219,25 +222,25 @@ ext ρ Z = Z
|
|||
ext ρ (S x) = S (ρ x)
|
||||
|
||||
rename : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ∋ A) → (∀ {A} → Γ ⊢ A → Δ ⊢ A)
|
||||
rename ρ (` x) = ` (ρ x)
|
||||
rename ρ (ƛ N) = ƛ (rename (ext ρ) N)
|
||||
rename ρ (L · M) = (rename ρ L) · (rename ρ M)
|
||||
rename ρ (`zero) = `zero
|
||||
rename ρ (`suc M) = `suc (rename ρ M)
|
||||
rename ρ (`caseℕ L M N) = `caseℕ (rename ρ L) (rename ρ M) (rename (ext ρ) N)
|
||||
rename ρ (μ N) = μ (rename (ext ρ) N)
|
||||
rename ρ `⟨ M , N ⟩ = `⟨ rename ρ M , rename ρ N ⟩
|
||||
rename ρ (`proj₁ L) = `proj₁ (rename ρ L)
|
||||
rename ρ (`proj₂ L) = `proj₂ (rename ρ L)
|
||||
rename ρ (`inj₁ M) = `inj₁ (rename ρ M)
|
||||
rename ρ (`inj₂ N) = `inj₂ (rename ρ N)
|
||||
rename ρ (`case⊎ L M N) = `case⊎ (rename ρ L) (rename (ext ρ) M) (rename (ext ρ) N)
|
||||
rename ρ `tt = `tt
|
||||
rename ρ (`case⊥ L) = `case⊥ (rename ρ L)
|
||||
rename ρ `[] = `[]
|
||||
rename ρ (M `∷ N) = (rename ρ M) `∷ (rename ρ N)
|
||||
rename ρ (`caseL L M N) = `caseL (rename ρ L) (rename ρ M) (rename (ext (ext ρ)) N)
|
||||
rename ρ (`let M N) = `let (rename ρ M) (rename (ext ρ) N)
|
||||
rename ρ (` x) = ` (ρ x)
|
||||
rename ρ (ƛ N) = ƛ (rename (ext ρ) N)
|
||||
rename ρ (L · M) = (rename ρ L) · (rename ρ M)
|
||||
rename ρ (`zero) = `zero
|
||||
rename ρ (`suc M) = `suc (rename ρ M)
|
||||
rename ρ (case L M N) = case (rename ρ L) (rename ρ M) (rename (ext ρ) N)
|
||||
rename ρ (μ N) = μ (rename (ext ρ) N)
|
||||
rename ρ `⟨ M , N ⟩ = `⟨ rename ρ M , rename ρ N ⟩
|
||||
rename ρ (`proj₁ L) = `proj₁ (rename ρ L)
|
||||
rename ρ (`proj₂ L) = `proj₂ (rename ρ L)
|
||||
rename ρ (`inj₁ M) = `inj₁ (rename ρ M)
|
||||
rename ρ (`inj₂ N) = `inj₂ (rename ρ N)
|
||||
rename ρ (case⊎ L M N) = case⊎ (rename ρ L) (rename (ext ρ) M) (rename (ext ρ) N)
|
||||
rename ρ `tt = `tt
|
||||
rename ρ (case⊥ L) = case⊥ (rename ρ L)
|
||||
rename ρ `[] = `[]
|
||||
rename ρ (M `∷ N) = (rename ρ M) `∷ (rename ρ N)
|
||||
rename ρ (caseL L M N) = caseL (rename ρ L) (rename ρ M) (rename (ext (ext ρ)) N)
|
||||
rename ρ (`let M N) = `let (rename ρ M) (rename (ext ρ) N)
|
||||
\end{code}
|
||||
|
||||
### Simultaneous Substitution
|
||||
|
|
@ -248,25 +251,25 @@ exts σ Z = ` Z
|
|||
exts σ (S x) = rename S_ (σ x)
|
||||
|
||||
subst : ∀ {Γ Δ} → (∀ {C} → Γ ∋ C → Δ ⊢ C) → (∀ {C} → Γ ⊢ C → Δ ⊢ C)
|
||||
subst σ (` k) = σ k
|
||||
subst σ (ƛ N) = ƛ (subst (exts σ) N)
|
||||
subst σ (L · M) = (subst σ L) · (subst σ M)
|
||||
subst σ (`zero) = `zero
|
||||
subst σ (`suc M) = `suc (subst σ M)
|
||||
subst σ (`caseℕ L M N) = `caseℕ (subst σ L) (subst σ M) (subst (exts σ) N)
|
||||
subst σ (μ N) = μ (subst (exts σ) N)
|
||||
subst σ `⟨ M , N ⟩ = `⟨ subst σ M , subst σ N ⟩
|
||||
subst σ (`proj₁ L) = `proj₁ (subst σ L)
|
||||
subst σ (`proj₂ L) = `proj₂ (subst σ L)
|
||||
subst σ (`inj₁ M) = `inj₁ (subst σ M)
|
||||
subst σ (`inj₂ N) = `inj₂ (subst σ N)
|
||||
subst σ (`case⊎ L M N) = `case⊎ (subst σ L) (subst (exts σ) M) (subst (exts σ) N)
|
||||
subst σ `tt = `tt
|
||||
subst σ (`case⊥ L) = `case⊥ (subst σ L)
|
||||
subst σ `[] = `[]
|
||||
subst σ (M `∷ N) = (subst σ M) `∷ (subst σ N)
|
||||
subst σ (`caseL L M N) = `caseL (subst σ L) (subst σ M) (subst (exts (exts σ)) N)
|
||||
subst σ (`let M N) = `let (subst σ M) (subst (exts σ) N)
|
||||
subst σ (` k) = σ k
|
||||
subst σ (ƛ N) = ƛ (subst (exts σ) N)
|
||||
subst σ (L · M) = (subst σ L) · (subst σ M)
|
||||
subst σ (`zero) = `zero
|
||||
subst σ (`suc M) = `suc (subst σ M)
|
||||
subst σ (case L M N) = case (subst σ L) (subst σ M) (subst (exts σ) N)
|
||||
subst σ (μ N) = μ (subst (exts σ) N)
|
||||
subst σ `⟨ M , N ⟩ = `⟨ subst σ M , subst σ N ⟩
|
||||
subst σ (`proj₁ L) = `proj₁ (subst σ L)
|
||||
subst σ (`proj₂ L) = `proj₂ (subst σ L)
|
||||
subst σ (`inj₁ M) = `inj₁ (subst σ M)
|
||||
subst σ (`inj₂ N) = `inj₂ (subst σ N)
|
||||
subst σ (case⊎ L M N) = case⊎ (subst σ L) (subst (exts σ) M) (subst (exts σ) N)
|
||||
subst σ `tt = `tt
|
||||
subst σ (case⊥ L) = case⊥ (subst σ L)
|
||||
subst σ `[] = `[]
|
||||
subst σ (M `∷ N) = (subst σ M) `∷ (subst σ N)
|
||||
subst σ (caseL L M N) = caseL (subst σ L) (subst σ M) (subst (exts (exts σ)) N)
|
||||
subst σ (`let M N) = `let (subst σ M) (subst (exts σ) N)
|
||||
\end{code}
|
||||
|
||||
### Single and double substitution
|
||||
|
|
@ -312,7 +315,7 @@ data Value : ∀ {Γ A} → Γ ⊢ A → Set where
|
|||
-----------------
|
||||
Value (`zero {Γ})
|
||||
|
||||
V-suc : ∀ {Γ} {V : Γ ⊢ `ℕ}
|
||||
V-suc_ : ∀ {Γ} {V : Γ ⊢ `ℕ}
|
||||
→ Value V
|
||||
--------------
|
||||
→ Value (`suc V)
|
||||
|
|
@ -320,31 +323,31 @@ data Value : ∀ {Γ A} → Γ ⊢ A → Set where
|
|||
V-⟨_,_⟩ : ∀ {Γ A B} {V : Γ ⊢ A} {W : Γ ⊢ B}
|
||||
→ Value V
|
||||
→ Value W
|
||||
-----------------
|
||||
----------------
|
||||
→ Value `⟨ V , W ⟩
|
||||
|
||||
V-inj₁ : ∀ {Γ A B} {V : Γ ⊢ A}
|
||||
→ Value V
|
||||
------------------------
|
||||
-----------------------
|
||||
→ Value (`inj₁ {B = B} V)
|
||||
|
||||
V-inj₂ : ∀ {Γ A B} {W : Γ ⊢ B}
|
||||
→ Value W
|
||||
------------------------
|
||||
-----------------------
|
||||
→ Value (`inj₂ {A = A} W)
|
||||
|
||||
TT : ∀ {Γ}
|
||||
V-tt : ∀ {Γ}
|
||||
-------------------
|
||||
→ Value (`tt {Γ = Γ})
|
||||
|
||||
Nil : ∀ {Γ A}
|
||||
----------------------------
|
||||
V-[] : ∀ {Γ A}
|
||||
---------------------------
|
||||
→ Value (`[] {Γ = Γ} {A = A})
|
||||
|
||||
Cons : ∀ {Γ A} {V : Γ ⊢ A} {W : Γ ⊢ `List A}
|
||||
_V-∷_ : ∀ {Γ A} {V : Γ ⊢ A} {W : Γ ⊢ `List A}
|
||||
→ Value V
|
||||
→ Value W
|
||||
---------------
|
||||
--------------
|
||||
→ Value (V `∷ W)
|
||||
\end{code}
|
||||
|
||||
|
|
@ -360,141 +363,141 @@ data _—→_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
|
|||
|
||||
ξ-·₁ : ∀ {Γ A B} {L L′ : Γ ⊢ A ⇒ B} {M : Γ ⊢ A}
|
||||
→ L —→ L′
|
||||
-----------------
|
||||
---------------
|
||||
→ L · M —→ L′ · M
|
||||
|
||||
ξ-·₂ : ∀ {Γ A B} {V : Γ ⊢ A ⇒ B} {M M′ : Γ ⊢ A}
|
||||
→ Value V
|
||||
→ M —→ M′
|
||||
-----------------
|
||||
---------------
|
||||
→ V · M —→ V · M′
|
||||
|
||||
β-ƛ : ∀ {Γ A B} {N : Γ , A ⊢ B} {W : Γ ⊢ A}
|
||||
→ Value W
|
||||
---------------------
|
||||
→ (ƛ N) · W —→ N [ W ]
|
||||
β-ƛ : ∀ {Γ A B} {N : Γ , A ⊢ B} {V : Γ ⊢ A}
|
||||
→ Value V
|
||||
--------------------
|
||||
→ (ƛ N) · V —→ N [ V ]
|
||||
|
||||
ξ-suc : ∀ {Γ} {M M′ : Γ ⊢ `ℕ}
|
||||
→ M —→ M′
|
||||
-------------------
|
||||
-----------------
|
||||
→ `suc M —→ `suc M′
|
||||
|
||||
ξ-caseℕ : ∀ {Γ A} {L L′ : Γ ⊢ `ℕ} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
|
||||
ξ-case : ∀ {Γ A} {L L′ : Γ ⊢ `ℕ} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
|
||||
→ L —→ L′
|
||||
-------------------------------
|
||||
→ `caseℕ L M N —→ `caseℕ L′ M N
|
||||
-------------------------
|
||||
→ case L M N —→ case L′ M N
|
||||
|
||||
β-ℕ₁ : ∀ {Γ A} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
|
||||
-----------------------
|
||||
→ `caseℕ `zero M N —→ M
|
||||
-------------------
|
||||
→ case `zero M N —→ M
|
||||
|
||||
β-ℕ₂ : ∀ {Γ A} {V : Γ ⊢ `ℕ} {M : Γ ⊢ A} {N : Γ , `ℕ ⊢ A}
|
||||
→ Value V
|
||||
--------------------------------
|
||||
→ `caseℕ (`suc V) M N —→ N [ V ]
|
||||
----------------------------
|
||||
→ case (`suc V) M N —→ N [ V ]
|
||||
|
||||
β-μ : ∀ {Γ A} {N : Γ , A ⊢ A}
|
||||
------------------
|
||||
----------------
|
||||
→ μ N —→ N [ μ N ]
|
||||
|
||||
ξ-⟨,⟩₁ : ∀ {Γ A B} {M M′ : Γ ⊢ A} {N : Γ ⊢ B}
|
||||
→ M —→ M′
|
||||
--------------------------
|
||||
-------------------------
|
||||
→ `⟨ M , N ⟩ —→ `⟨ M′ , N ⟩
|
||||
|
||||
ξ-⟨,⟩₂ : ∀ {Γ A B} {V : Γ ⊢ A} {N N′ : Γ ⊢ B}
|
||||
→ Value V
|
||||
→ N —→ N′
|
||||
--------------------------
|
||||
-------------------------
|
||||
→ `⟨ V , N ⟩ —→ `⟨ V , N′ ⟩
|
||||
|
||||
ξ-proj₁ : ∀ {Γ A B} {L L′ : Γ ⊢ A `× B}
|
||||
→ L —→ L′
|
||||
-----------------------
|
||||
---------------------
|
||||
→ `proj₁ L —→ `proj₁ L′
|
||||
|
||||
ξ-proj₂ : ∀ {Γ A B} {L L′ : Γ ⊢ A `× B}
|
||||
→ L —→ L′
|
||||
-----------------------
|
||||
---------------------
|
||||
→ `proj₂ L —→ `proj₂ L′
|
||||
|
||||
β-×₁ : ∀ {Γ A B} {V : Γ ⊢ A} {W : Γ ⊢ B}
|
||||
→ Value V
|
||||
→ Value W
|
||||
------------------------
|
||||
----------------------
|
||||
→ `proj₁ `⟨ V , W ⟩ —→ V
|
||||
|
||||
β-×₂ : ∀ {Γ A B} {V : Γ ⊢ A} {W : Γ ⊢ B}
|
||||
→ Value V
|
||||
→ Value W
|
||||
------------------------
|
||||
----------------------
|
||||
→ `proj₂ `⟨ V , W ⟩ —→ W
|
||||
|
||||
ξ-inj₁ : ∀ {Γ A B} {M M′ : Γ ⊢ A}
|
||||
→ M —→ M′
|
||||
-----------------------------
|
||||
---------------------------
|
||||
→ `inj₁ {B = B} M —→ `inj₁ M′
|
||||
|
||||
ξ-inj₂ : ∀ {Γ A B} {N N′ : Γ ⊢ B}
|
||||
→ N —→ N′
|
||||
-----------------------------
|
||||
---------------------------
|
||||
→ `inj₂ {A = A} N —→ `inj₂ N′
|
||||
|
||||
ξ-case⊎ : ∀ {Γ A B C} {L L′ : Γ ⊢ A `⊎ B} {M : Γ , A ⊢ C} {N : Γ , B ⊢ C}
|
||||
→ L —→ L′
|
||||
-------------------------------
|
||||
→ `case⊎ L M N —→ `case⊎ L′ M N
|
||||
---------------------------
|
||||
→ case⊎ L M N —→ case⊎ L′ M N
|
||||
|
||||
β-⊎₁ : ∀ {Γ A B C} {V : Γ ⊢ A} {M : Γ , A ⊢ C} {N : Γ , B ⊢ C}
|
||||
→ Value V
|
||||
---------------------------------
|
||||
→ `case⊎ (`inj₁ V) M N —→ M [ V ]
|
||||
------------------------------
|
||||
→ case⊎ (`inj₁ V) M N —→ M [ V ]
|
||||
|
||||
β-⊎₂ : ∀ {Γ A B C} {W : Γ ⊢ B} {M : Γ , A ⊢ C} {N : Γ , B ⊢ C}
|
||||
→ Value W
|
||||
---------------------------------
|
||||
→ `case⊎ (`inj₂ W) M N —→ N [ W ]
|
||||
------------------------------
|
||||
→ case⊎ (`inj₂ W) M N —→ N [ W ]
|
||||
|
||||
ξ-case⊥ : ∀ {Γ A} {L L′ : Γ ⊢ `⊥}
|
||||
→ L —→ L′
|
||||
-------------------------------
|
||||
→ `case⊥ {A = A} L —→ `case⊥ L′
|
||||
---------------------------
|
||||
→ case⊥ {A = A} L —→ case⊥ L′
|
||||
|
||||
ξ-∷₁ : ∀ {Γ A} {M M′ : Γ ⊢ A} {N : Γ ⊢ `List A}
|
||||
→ M —→ M′
|
||||
-------------------
|
||||
-----------------
|
||||
→ M `∷ N —→ M′ `∷ N
|
||||
|
||||
ξ-∷₂ : ∀ {Γ A} {V : Γ ⊢ A} {N N′ : Γ ⊢ `List A}
|
||||
→ Value V
|
||||
→ N —→ N′
|
||||
-------------------
|
||||
-----------------
|
||||
→ V `∷ N —→ V `∷ N′
|
||||
|
||||
ξ-caseL : ∀ {Γ A B} {L L′ : Γ ⊢ `List A} {M : Γ ⊢ B} {N : Γ , A , `List A ⊢ B}
|
||||
→ L —→ L′
|
||||
-------------------------------
|
||||
→ `caseL L M N —→ `caseL L′ M N
|
||||
---------------------------
|
||||
→ caseL L M N —→ caseL L′ M N
|
||||
|
||||
β-List₁ : ∀ {Γ A B} {M : Γ ⊢ B} {N : Γ , A , `List A ⊢ B}
|
||||
---------------------
|
||||
→ `caseL `[] M N —→ M
|
||||
------------------
|
||||
→ caseL `[] M N —→ M
|
||||
|
||||
β-List₂ : ∀ {Γ A B} {V : Γ ⊢ A} {W : Γ ⊢ `List A}
|
||||
{M : Γ ⊢ B} {N : Γ , A , `List A ⊢ B}
|
||||
→ Value V
|
||||
→ Value W
|
||||
-------------------------------------
|
||||
→ `caseL (V `∷ W) M N —→ N [ V ][ W ]
|
||||
----------------------------------
|
||||
→ caseL (V `∷ W) M N —→ N [ V ][ W ]
|
||||
|
||||
ξ-let : ∀ {Γ A B} {M M′ : Γ ⊢ A} {N : Γ , A ⊢ B}
|
||||
→ M —→ M′
|
||||
-----------------------
|
||||
---------------------
|
||||
→ `let M N —→ `let M′ N
|
||||
|
||||
β-let : ∀ {Γ A B} {V : Γ ⊢ A} {N : Γ , A ⊢ B}
|
||||
→ Value V
|
||||
---------------------
|
||||
-------------------
|
||||
→ `let V N —→ N [ V ]
|
||||
\end{code}
|
||||
|
||||
|
|
@ -502,9 +505,9 @@ data _—→_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
|
|||
|
||||
\begin{code}
|
||||
infix 2 _—↠_
|
||||
infix 1 begin_
|
||||
infix 1 begin_
|
||||
infixr 2 _—→⟨_⟩_
|
||||
infix 3 _∎
|
||||
infix 3 _∎
|
||||
|
||||
data _—↠_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
|
||||
|
||||
|
|
@ -515,10 +518,13 @@ data _—↠_ : ∀ {Γ A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
|
|||
_—→⟨_⟩_ : ∀ {Γ A} (L : Γ ⊢ A) {M N : Γ ⊢ A}
|
||||
→ L —→ M
|
||||
→ M —↠ N
|
||||
---------
|
||||
------
|
||||
→ L —↠ N
|
||||
|
||||
begin_ : ∀ {Γ} {A} {M N : Γ ⊢ A} → (M —↠ N) → (M —↠ N)
|
||||
begin_ : ∀ {Γ} {A} {M N : Γ ⊢ A}
|
||||
→ M —↠ N
|
||||
------
|
||||
→ M —↠ N
|
||||
begin M—↠N = M—↠N
|
||||
\end{code}
|
||||
|
||||
|
|
@ -527,24 +533,30 @@ begin M—↠N = M—↠N
|
|||
|
||||
Values do not reduce.
|
||||
\begin{code}
|
||||
Value-lemma : ∀ {Γ A} {M N : Γ ⊢ A} → Value M → ¬ (M —→ N)
|
||||
Value-lemma V-ƛ ()
|
||||
Value-lemma V-zero ()
|
||||
Value-lemma (V-suc VM) (ξ-suc M—→M′) = Value-lemma VM M—→M′
|
||||
Value-lemma (V-⟨_,_⟩ VM _) (ξ-⟨,⟩₁ M—→M′) = Value-lemma VM M—→M′
|
||||
Value-lemma (V-⟨_,_⟩ _ VN) (ξ-⟨,⟩₂ _ N—→N′) = Value-lemma VN N—→N′
|
||||
Value-lemma (V-inj₁ VM) (ξ-inj₁ M—→M′) = Value-lemma VM M—→M′
|
||||
Value-lemma (V-inj₂ VN) (ξ-inj₂ N—→N′) = Value-lemma VN N—→N′
|
||||
Value-lemma TT ()
|
||||
Value-lemma Nil ()
|
||||
Value-lemma (Cons VM _) (ξ-∷₁ M—→M′) = Value-lemma VM M—→M′
|
||||
Value-lemma (Cons _ VN) (ξ-∷₂ _ N—→N′) = Value-lemma VN N—→N′
|
||||
V¬—→ : ∀ {Γ A} {M N : Γ ⊢ A}
|
||||
→ Value M
|
||||
----------
|
||||
→ ¬ (M —→ N)
|
||||
V¬—→ V-ƛ ()
|
||||
V¬—→ V-zero ()
|
||||
V¬—→ (V-suc VM) (ξ-suc M—→M′) = V¬—→ VM M—→M′
|
||||
V¬—→ V-⟨ VM , _ ⟩ (ξ-⟨,⟩₁ M—→M′) = V¬—→ VM M—→M′
|
||||
V¬—→ V-⟨ _ , VN ⟩ (ξ-⟨,⟩₂ _ N—→N′) = V¬—→ VN N—→N′
|
||||
V¬—→ (V-inj₁ VM) (ξ-inj₁ M—→M′) = V¬—→ VM M—→M′
|
||||
V¬—→ (V-inj₂ VN) (ξ-inj₂ N—→N′) = V¬—→ VN N—→N′
|
||||
V¬—→ V-tt ()
|
||||
V¬—→ V-[] ()
|
||||
V¬—→ (VM V-∷ _) (ξ-∷₁ M—→M′) = V¬—→ VM M—→M′
|
||||
V¬—→ (_ V-∷ VN) (ξ-∷₂ _ N—→N′) = V¬—→ VN N—→N′
|
||||
\end{code}
|
||||
|
||||
As a corollary, terms that reduce are not values.
|
||||
\begin{code}
|
||||
—→-corollary : ∀ {Γ A} {M N : Γ ⊢ A} → (M —→ N) → ¬ Value M
|
||||
—→-corollary M—→N VM = Value-lemma VM M—→N
|
||||
—→¬V : ∀ {Γ A} {M N : Γ ⊢ A}
|
||||
→ M —→ N
|
||||
---------
|
||||
→ ¬ Value M
|
||||
—→¬V M—→N VM = V¬—→ VM M—→N
|
||||
\end{code}
|
||||
|
||||
|
||||
|
|
@ -552,74 +564,79 @@ As a corollary, terms that reduce are not values.
|
|||
|
||||
\begin{code}
|
||||
data Progress {A} (M : ∅ ⊢ A) : Set where
|
||||
|
||||
step : ∀ {N : ∅ ⊢ A}
|
||||
→ M —→ N
|
||||
-------------
|
||||
----------
|
||||
→ Progress M
|
||||
|
||||
done :
|
||||
Value M
|
||||
----------
|
||||
→ Progress M
|
||||
|
||||
progress : ∀ {A} → (M : ∅ ⊢ A) → Progress M
|
||||
progress : ∀ {A}
|
||||
→ (M : ∅ ⊢ A)
|
||||
-----------
|
||||
→ Progress M
|
||||
progress (` ())
|
||||
progress (ƛ N) = done V-ƛ
|
||||
progress (ƛ N) = done V-ƛ
|
||||
progress (L · M) with progress L
|
||||
... | step L—→L′ = step (ξ-·₁ L—→L′)
|
||||
... | step L—→L′ = step (ξ-·₁ L—→L′)
|
||||
... | done V-ƛ with progress M
|
||||
... | step M—→M′ = step (ξ-·₂ V-ƛ M—→M′)
|
||||
... | done VM = step (β-ƛ VM)
|
||||
progress (`zero) = done V-zero
|
||||
... | step M—→M′ = step (ξ-·₂ V-ƛ M—→M′)
|
||||
... | done VM = step (β-ƛ VM)
|
||||
progress (`zero) = done V-zero
|
||||
progress (`suc M) with progress M
|
||||
... | step M—→M′ = step (ξ-suc M—→M′)
|
||||
... | done VM = done (V-suc VM)
|
||||
progress (`caseℕ L M N) with progress L
|
||||
... | step L—→L′ = step (ξ-caseℕ L—→L′)
|
||||
... | done V-zero = step β-ℕ₁
|
||||
... | done (V-suc VL) = step (β-ℕ₂ VL)
|
||||
progress (μ N) = step β-μ
|
||||
... | step M—→M′ = step (ξ-suc M—→M′)
|
||||
... | done VM = done (V-suc VM)
|
||||
progress (case L M N) with progress L
|
||||
... | step L—→L′ = step (ξ-case L—→L′)
|
||||
... | done V-zero = step β-ℕ₁
|
||||
... | done (V-suc VL) = step (β-ℕ₂ VL)
|
||||
progress (μ N) = step β-μ
|
||||
progress `⟨ M , N ⟩ with progress M
|
||||
... | step M—→M′ = step (ξ-⟨,⟩₁ M—→M′)
|
||||
... | step M—→M′ = step (ξ-⟨,⟩₁ M—→M′)
|
||||
... | done VM with progress N
|
||||
... | step N—→N′ = step (ξ-⟨,⟩₂ VM N—→N′)
|
||||
... | done VN = done (V-⟨ VM , VN ⟩)
|
||||
... | step N—→N′ = step (ξ-⟨,⟩₂ VM N—→N′)
|
||||
... | done VN = done (V-⟨ VM , VN ⟩)
|
||||
progress (`proj₁ L) with progress L
|
||||
... | step L—→L′ = step (ξ-proj₁ L—→L′)
|
||||
... | done (V-⟨ VM , VN ⟩) = step (β-×₁ VM VN)
|
||||
... | step L—→L′ = step (ξ-proj₁ L—→L′)
|
||||
... | done (V-⟨ VM , VN ⟩) = step (β-×₁ VM VN)
|
||||
progress (`proj₂ L) with progress L
|
||||
... | step L—→L′ = step (ξ-proj₂ L—→L′)
|
||||
... | done (V-⟨ VM , VN ⟩) = step (β-×₂ VM VN)
|
||||
... | step L—→L′ = step (ξ-proj₂ L—→L′)
|
||||
... | done (V-⟨ VM , VN ⟩) = step (β-×₂ VM VN)
|
||||
progress (`inj₁ M) with progress M
|
||||
... | step M—→M′ = step (ξ-inj₁ M—→M′)
|
||||
... | done VM = done (V-inj₁ VM)
|
||||
... | step M—→M′ = step (ξ-inj₁ M—→M′)
|
||||
... | done VM = done (V-inj₁ VM)
|
||||
progress (`inj₂ N) with progress N
|
||||
... | step N—→N′ = step (ξ-inj₂ N—→N′)
|
||||
... | done VN = done (V-inj₂ VN)
|
||||
progress (`case⊎ L M N) with progress L
|
||||
... | step L—→L′ = step (ξ-case⊎ L—→L′)
|
||||
... | done (V-inj₁ VV) = step (β-⊎₁ VV)
|
||||
... | done (V-inj₂ VW) = step (β-⊎₂ VW)
|
||||
progress (`tt) = done TT
|
||||
progress (`case⊥ {A = A} L) with progress L
|
||||
... | step L—→L′ = step (ξ-case⊥ {A = A} L—→L′)
|
||||
... | step N—→N′ = step (ξ-inj₂ N—→N′)
|
||||
... | done VN = done (V-inj₂ VN)
|
||||
progress (case⊎ L M N) with progress L
|
||||
... | step L—→L′ = step (ξ-case⊎ L—→L′)
|
||||
... | done (V-inj₁ VV) = step (β-⊎₁ VV)
|
||||
... | done (V-inj₂ VW) = step (β-⊎₂ VW)
|
||||
progress (`tt) = done V-tt
|
||||
progress (case⊥ {A = A} L) with progress L
|
||||
... | step L—→L′ = step (ξ-case⊥ {A = A} L—→L′)
|
||||
... | done ()
|
||||
progress (`[]) = done Nil
|
||||
progress (`[]) = done V-[]
|
||||
progress (M `∷ N) with progress M
|
||||
... | step M—→M′ = step (ξ-∷₁ M—→M′)
|
||||
... | step M—→M′ = step (ξ-∷₁ M—→M′)
|
||||
... | done VM with progress N
|
||||
... | step N—→N′ = step (ξ-∷₂ VM N—→N′)
|
||||
... | done VN = done (Cons VM VN)
|
||||
progress (`caseL L M N) with progress L
|
||||
... | step L—→L′ = step (ξ-caseL L—→L′)
|
||||
... | done Nil = step β-List₁
|
||||
... | done (Cons VV VW) = step (β-List₂ VV VW)
|
||||
... | step N—→N′ = step (ξ-∷₂ VM N—→N′)
|
||||
... | done VN = done (_V-∷_ VM VN)
|
||||
progress (caseL L M N) with progress L
|
||||
... | step L—→L′ = step (ξ-caseL L—→L′)
|
||||
... | done V-[] = step β-List₁
|
||||
... | done (_V-∷_ VV VW) = step (β-List₂ VV VW)
|
||||
progress (`let M N) with progress M
|
||||
... | step M—→M′ = step (ξ-let M—→M′)
|
||||
... | done VM = step (β-let VM)
|
||||
... | step M—→M′ = step (ξ-let M—→M′)
|
||||
... | done VM = step (β-let VM)
|
||||
\end{code}
|
||||
|
||||
|
||||
## Normalise
|
||||
## Evaluation
|
||||
|
||||
\begin{code}
|
||||
data Gas : Set where
|
||||
|
|
|
|||
|
|
@ -93,7 +93,10 @@ types without needing to develop a separate inductive definition of the
|
|||
|
||||
We start with any easy observation. Values do not reduce.
|
||||
\begin{code}
|
||||
V¬—→ : ∀ {M N} → Value M → ¬ (M —→ N)
|
||||
V¬—→ : ∀ {M N}
|
||||
→ Value M
|
||||
----------
|
||||
→ ¬ (M —→ N)
|
||||
V¬—→ V-ƛ ()
|
||||
V¬—→ V-zero ()
|
||||
V¬—→ (V-suc VM) (ξ-suc M—→N) = V¬—→ VM M—→N
|
||||
|
|
@ -110,7 +113,10 @@ We consider the three possibilities for values.
|
|||
|
||||
As a corollary, terms that reduce are not values.
|
||||
\begin{code}
|
||||
—→¬V : ∀ {M N} → (M —→ N) → ¬ Value M
|
||||
—→¬V : ∀ {M N}
|
||||
→ M —→ N
|
||||
---------
|
||||
→ ¬ Value M
|
||||
—→¬V M—→N VM = V¬—→ VM M—→N
|
||||
\end{code}
|
||||
If we expand out the negations, we have
|
||||
|
|
@ -1015,19 +1021,19 @@ _ : eval (gas 100) ⊢2+2 ≡
|
|||
((μ "+" ⇒
|
||||
(ƛ "m" ⇒
|
||||
(ƛ "n" ⇒
|
||||
`case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
|
||||
case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
|
||||
])))
|
||||
· `suc (`suc `zero)
|
||||
· `suc (`suc `zero)
|
||||
—→⟨ ξ-·₁ (ξ-·₁ β-μ) ⟩
|
||||
(ƛ "m" ⇒
|
||||
(ƛ "n" ⇒
|
||||
`case ` "m" [zero⇒ ` "n" |suc "m" ⇒
|
||||
case ` "m" [zero⇒ ` "n" |suc "m" ⇒
|
||||
`suc
|
||||
((μ "+" ⇒
|
||||
(ƛ "m" ⇒
|
||||
(ƛ "n" ⇒
|
||||
`case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
|
||||
case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
|
||||
])))
|
||||
· ` "m"
|
||||
· ` "n")
|
||||
|
|
@ -1036,24 +1042,24 @@ _ : eval (gas 100) ⊢2+2 ≡
|
|||
· `suc (`suc `zero)
|
||||
—→⟨ ξ-·₁ (β-ƛ (V-suc (V-suc V-zero))) ⟩
|
||||
(ƛ "n" ⇒
|
||||
`case `suc (`suc `zero) [zero⇒ ` "n" |suc "m" ⇒
|
||||
case `suc (`suc `zero) [zero⇒ ` "n" |suc "m" ⇒
|
||||
`suc
|
||||
((μ "+" ⇒
|
||||
(ƛ "m" ⇒
|
||||
(ƛ "n" ⇒
|
||||
`case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
|
||||
case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
|
||||
])))
|
||||
· ` "m"
|
||||
· ` "n")
|
||||
])
|
||||
· `suc (`suc `zero)
|
||||
—→⟨ β-ƛ (V-suc (V-suc V-zero)) ⟩
|
||||
`case `suc (`suc `zero) [zero⇒ `suc (`suc `zero) |suc "m" ⇒
|
||||
case `suc (`suc `zero) [zero⇒ `suc (`suc `zero) |suc "m" ⇒
|
||||
`suc
|
||||
((μ "+" ⇒
|
||||
(ƛ "m" ⇒
|
||||
(ƛ "n" ⇒
|
||||
`case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
|
||||
case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
|
||||
])))
|
||||
· ` "m"
|
||||
· `suc (`suc `zero))
|
||||
|
|
@ -1063,7 +1069,7 @@ _ : eval (gas 100) ⊢2+2 ≡
|
|||
((μ "+" ⇒
|
||||
(ƛ "m" ⇒
|
||||
(ƛ "n" ⇒
|
||||
`case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
|
||||
case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
|
||||
])))
|
||||
· `suc `zero
|
||||
· `suc (`suc `zero))
|
||||
|
|
@ -1071,12 +1077,12 @@ _ : eval (gas 100) ⊢2+2 ≡
|
|||
`suc
|
||||
((ƛ "m" ⇒
|
||||
(ƛ "n" ⇒
|
||||
`case ` "m" [zero⇒ ` "n" |suc "m" ⇒
|
||||
case ` "m" [zero⇒ ` "n" |suc "m" ⇒
|
||||
`suc
|
||||
((μ "+" ⇒
|
||||
(ƛ "m" ⇒
|
||||
(ƛ "n" ⇒
|
||||
`case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
|
||||
case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
|
||||
])))
|
||||
· ` "m"
|
||||
· ` "n")
|
||||
|
|
@ -1086,12 +1092,12 @@ _ : eval (gas 100) ⊢2+2 ≡
|
|||
—→⟨ ξ-suc (ξ-·₁ (β-ƛ (V-suc V-zero))) ⟩
|
||||
`suc
|
||||
((ƛ "n" ⇒
|
||||
`case `suc `zero [zero⇒ ` "n" |suc "m" ⇒
|
||||
case `suc `zero [zero⇒ ` "n" |suc "m" ⇒
|
||||
`suc
|
||||
((μ "+" ⇒
|
||||
(ƛ "m" ⇒
|
||||
(ƛ "n" ⇒
|
||||
`case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
|
||||
case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
|
||||
])))
|
||||
· ` "m"
|
||||
· ` "n")
|
||||
|
|
@ -1099,12 +1105,12 @@ _ : eval (gas 100) ⊢2+2 ≡
|
|||
· `suc (`suc `zero))
|
||||
—→⟨ ξ-suc (β-ƛ (V-suc (V-suc V-zero))) ⟩
|
||||
`suc
|
||||
`case `suc `zero [zero⇒ `suc (`suc `zero) |suc "m" ⇒
|
||||
case `suc `zero [zero⇒ `suc (`suc `zero) |suc "m" ⇒
|
||||
`suc
|
||||
((μ "+" ⇒
|
||||
(ƛ "m" ⇒
|
||||
(ƛ "n" ⇒
|
||||
`case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
|
||||
case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
|
||||
])))
|
||||
· ` "m"
|
||||
· `suc (`suc `zero))
|
||||
|
|
@ -1115,7 +1121,7 @@ _ : eval (gas 100) ⊢2+2 ≡
|
|||
((μ "+" ⇒
|
||||
(ƛ "m" ⇒
|
||||
(ƛ "n" ⇒
|
||||
`case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
|
||||
case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
|
||||
])))
|
||||
· `zero
|
||||
· `suc (`suc `zero)))
|
||||
|
|
@ -1124,12 +1130,12 @@ _ : eval (gas 100) ⊢2+2 ≡
|
|||
(`suc
|
||||
((ƛ "m" ⇒
|
||||
(ƛ "n" ⇒
|
||||
`case ` "m" [zero⇒ ` "n" |suc "m" ⇒
|
||||
case ` "m" [zero⇒ ` "n" |suc "m" ⇒
|
||||
`suc
|
||||
((μ "+" ⇒
|
||||
(ƛ "m" ⇒
|
||||
(ƛ "n" ⇒
|
||||
`case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
|
||||
case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
|
||||
])))
|
||||
· ` "m"
|
||||
· ` "n")
|
||||
|
|
@ -1140,12 +1146,12 @@ _ : eval (gas 100) ⊢2+2 ≡
|
|||
`suc
|
||||
(`suc
|
||||
((ƛ "n" ⇒
|
||||
`case `zero [zero⇒ ` "n" |suc "m" ⇒
|
||||
case `zero [zero⇒ ` "n" |suc "m" ⇒
|
||||
`suc
|
||||
((μ "+" ⇒
|
||||
(ƛ "m" ⇒
|
||||
(ƛ "n" ⇒
|
||||
`case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
|
||||
case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
|
||||
])))
|
||||
· ` "m"
|
||||
· ` "n")
|
||||
|
|
@ -1154,12 +1160,12 @@ _ : eval (gas 100) ⊢2+2 ≡
|
|||
—→⟨ ξ-suc (ξ-suc (β-ƛ (V-suc (V-suc V-zero)))) ⟩
|
||||
`suc
|
||||
(`suc
|
||||
`case `zero [zero⇒ `suc (`suc `zero) |suc "m" ⇒
|
||||
case `zero [zero⇒ `suc (`suc `zero) |suc "m" ⇒
|
||||
`suc
|
||||
((μ "+" ⇒
|
||||
(ƛ "m" ⇒
|
||||
(ƛ "n" ⇒
|
||||
`case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
|
||||
case ` "m" [zero⇒ ` "n" |suc "m" ⇒ `suc (` "+" · ` "m" · ` "n")
|
||||
])))
|
||||
· ` "m"
|
||||
· `suc (`suc `zero))
|
||||
|
|
@ -1360,7 +1366,7 @@ det (β-ƛ _) (ξ-·₁ L—→L″) = ⊥-elim (V¬—→ V-ƛ L—
|
|||
det (β-ƛ VM) (ξ-·₂ _ M—→M″) = ⊥-elim (V¬—→ VM M—→M″)
|
||||
det (β-ƛ _) (β-ƛ _) = refl
|
||||
det (ξ-suc M—→M′) (ξ-suc M—→M″) = cong `suc_ (det M—→M′ M—→M″)
|
||||
det (ξ-case L—→L′) (ξ-case L—→L″) = cong₄ `case_[zero⇒_|suc_⇒_]
|
||||
det (ξ-case L—→L′) (ξ-case L—→L″) = cong₄ case_[zero⇒_|suc_⇒_]
|
||||
(det L—→L′ L—→L″) refl refl refl
|
||||
det (ξ-case L—→L′) β-zero = ⊥-elim (V¬—→ V-zero L—→L′)
|
||||
det (ξ-case L—→L′) (β-suc VL) = ⊥-elim (V¬—→ (V-suc VL) L—→L′)
|
||||
|
|
|
|||
Loading…
Reference in a new issue