halfway through tidying More
This commit is contained in:
wadler
parent
1991c84cad
commit
946ea31653
2 changed files with 97 additions and 72 deletions
|
|
@ -235,16 +235,17 @@ a separate proof.
|
|||
|
||||
We now begin our formal development.
|
||||
|
||||
First, we get all our infix declarations out of the way. For
|
||||
ease of reading, we list operators in order from least tightly
|
||||
binding to most.
|
||||
First, we get all our infix declarations out of the way.
|
||||
We list separately operators for judgements, types, and terms.
|
||||
\begin{code}
|
||||
infix 4 _⊢_
|
||||
infix 4 _∋_
|
||||
infixl 5 _,_
|
||||
|
||||
infixr 7 _⇒_
|
||||
|
||||
infix 5 ƛ_
|
||||
infix 5 μ_
|
||||
infixr 7 _⇒_
|
||||
infixl 7 _·_
|
||||
infix 8 `suc_
|
||||
infix 9 `_
|
||||
|
|
@ -264,12 +265,6 @@ data Type : Set where
|
|||
_⇒_ : Type → Type → Type
|
||||
`ℕ : Type
|
||||
\end{code}
|
||||
For example,
|
||||
\begin{code}
|
||||
_ : Type
|
||||
_ = (`ℕ ⇒ `ℕ) ⇒ `ℕ ⇒ `ℕ
|
||||
\end{code}
|
||||
is a type that can be assigned to a Church numeral.
|
||||
|
||||
### Contexts
|
||||
|
||||
|
|
@ -377,7 +372,7 @@ data _⊢_ : Context → Type → Set where
|
|||
-------
|
||||
→ Γ ⊢ `ℕ
|
||||
|
||||
`case : ∀ {Γ A}
|
||||
`caseℕ : ∀ {Γ A}
|
||||
→ Γ ⊢ `ℕ
|
||||
→ Γ ⊢ A
|
||||
→ Γ , `ℕ ⊢ A
|
||||
|
|
@ -481,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
|
||||
|
|
@ -514,15 +509,15 @@ contexts. While we are at it, we also generalise `twoᶜ` and
|
|||
|
||||
## Substitution
|
||||
|
||||
With terms in hand, we turn to substitution, the heart of
|
||||
lambda calculus. Whereas before we had to restrict our
|
||||
With terms in hand, we turn to substitution.
|
||||
Whereas before we had to restrict our
|
||||
attention to substituting only one variable at a time and
|
||||
could only substitute closed terms, here we can consider
|
||||
simultaneous subsitution of multiple open terms. The
|
||||
simultaneous subsitution of open terms. The
|
||||
definition of substitution we consider is due to Conor
|
||||
McBride. Whereas before we defined substitution in one
|
||||
chapter and showed it preserved types in the next chapter,
|
||||
here we write a single piece of code that does both at once.
|
||||
here we write code that does both at once.
|
||||
|
||||
### Renaming
|
||||
|
||||
|
|
@ -570,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 `Γ`
|
||||
|
|
@ -627,7 +622,7 @@ typing, and hence the Agda code for inherently-typed de Bruijn
|
|||
terms is inherently reliable.
|
||||
|
||||
|
||||
### Substitution
|
||||
### Simultaneous Substitution
|
||||
|
||||
Because de Bruijn indices free us of concerns with renaming,
|
||||
it becomes easy to provide a definition of substitution that
|
||||
|
|
@ -683,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 `Γ`
|
||||
|
|
@ -702,6 +697,8 @@ The remaining cases are similar, recursing on each subterm,
|
|||
and extending the map whenever the construct introduces a
|
||||
bound variable.
|
||||
|
||||
### Single substitution
|
||||
|
||||
From the general case of substitution for multiple free
|
||||
variables in is easy to define the special case of
|
||||
substitution for one free variable.
|
||||
|
|
@ -846,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}
|
||||
---------------
|
||||
|
|
@ -927,29 +924,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)))
|
||||
∎
|
||||
|
|
@ -1048,7 +1045,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)
|
||||
|
|
@ -1151,40 +1148,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) ⟩
|
||||
|
|
@ -1192,19 +1189,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
|
||||
|
|
@ -1212,23 +1209,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) ⟩
|
||||
|
|
@ -1237,7 +1234,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 (ξ-·₁ (ξ-·₁ β-μ))) ⟩
|
||||
|
|
@ -1245,12 +1242,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
|
||||
|
|
@ -1259,24 +1256,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))) ∎)
|
||||
|
|
|
|||
|
|
@ -51,6 +51,7 @@ infixl 7 _·_
|
|||
infix 8 `suc_
|
||||
infix 9 `_
|
||||
infix 9 S_
|
||||
infix 9 #_
|
||||
|
||||
data Type : Set where
|
||||
`ℕ : Type
|
||||
|
|
@ -61,11 +62,11 @@ data Type : Set where
|
|||
`⊥ : Type
|
||||
`List : Type → Type
|
||||
|
||||
data Env : Set where
|
||||
∅ : Env
|
||||
_,_ : Env → Type → Env
|
||||
data Context : Set where
|
||||
∅ : Context
|
||||
_,_ : Context → Type → Context
|
||||
|
||||
data _∋_ : Env → Type → Set where
|
||||
data _∋_ : Context → Type → Set where
|
||||
|
||||
Z : ∀ {Γ} {A}
|
||||
----------
|
||||
|
|
@ -76,7 +77,7 @@ data _∋_ : Env → Type → Set where
|
|||
---------
|
||||
→ Γ , A ∋ B
|
||||
|
||||
data _⊢_ : Env → Type → Set where
|
||||
data _⊢_ : Context → Type → Set where
|
||||
|
||||
`_ : ∀ {Γ} {A}
|
||||
→ Γ ∋ A
|
||||
|
|
@ -181,15 +182,36 @@ data _⊢_ : Env → Type → Set where
|
|||
→ Γ ⊢ B
|
||||
\end{code}
|
||||
|
||||
## Abbreviating de Bruijn indices
|
||||
|
||||
\begin{code}
|
||||
lookup : Context → ℕ → Type
|
||||
lookup (Γ , A) zero = A
|
||||
lookup (Γ , _) (suc n) = lookup Γ n
|
||||
lookup ∅ _ = ⊥-elim impossible
|
||||
where postulate impossible : ⊥
|
||||
\end{code}
|
||||
|
||||
\begin{code}
|
||||
count : ∀ {Γ} → (n : ℕ) → Γ ∋ lookup Γ n
|
||||
count {Γ , _} zero = Z
|
||||
count {Γ , _} (suc n) = S (count n)
|
||||
count {∅} _ = ⊥-elim impossible
|
||||
where postulate impossible : ⊥
|
||||
\end{code}
|
||||
|
||||
\begin{code}
|
||||
#_ : ∀ {Γ} → (n : ℕ) → Γ ⊢ lookup Γ n
|
||||
# n = ` count n
|
||||
\end{code}
|
||||
|
||||
|
||||
## Test examples
|
||||
|
||||
|
||||
## Operational semantics
|
||||
## Substitution
|
||||
|
||||
Simultaneous substitution, a la McBride
|
||||
|
||||
## Renaming
|
||||
### Renaming
|
||||
|
||||
\begin{code}
|
||||
ext : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ∋ A) → (∀ {A B} → Γ , A ∋ B → Δ , A ∋ B)
|
||||
|
|
@ -218,7 +240,7 @@ rename ρ (`caseL L M N) = `caseL (rename ρ L) (rename ρ M) (rename (ext (ex
|
|||
rename ρ (`let M N) = `let (rename ρ M) (rename (ext ρ) N)
|
||||
\end{code}
|
||||
|
||||
## Substitution
|
||||
### Simultaneous Substitution
|
||||
|
||||
\begin{code}
|
||||
exts : ∀ {Γ Δ} → (∀ {A} → Γ ∋ A → Δ ⊢ A) → (∀ {A B} → Γ , A ∋ B → Δ , A ⊢ B)
|
||||
|
|
@ -245,7 +267,11 @@ 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
|
||||
|
||||
\begin{code}
|
||||
_[_] : ∀ {Γ A B}
|
||||
→ Γ , A ⊢ B
|
||||
→ Γ ⊢ A
|
||||
|
|
@ -271,7 +297,9 @@ _[_][_] {Γ} {A} {B} N V W = subst {Γ , A , B} {Γ} σ N
|
|||
σ (S (S x)) = ` x
|
||||
\end{code}
|
||||
|
||||
## Value
|
||||
## Reductions
|
||||
|
||||
### Value
|
||||
|
||||
\begin{code}
|
||||
data Value : ∀ {Γ A} → Γ ⊢ A → Set where
|
||||
|
|
@ -295,12 +323,12 @@ data Value : ∀ {Γ A} → Γ ⊢ A → Set where
|
|||
-----------------
|
||||
→ Value `⟨ V , W ⟩
|
||||
|
||||
Inj₁ : ∀ {Γ A B} {V : Γ ⊢ A}
|
||||
V-inj₁ : ∀ {Γ A B} {V : Γ ⊢ A}
|
||||
→ Value V
|
||||
------------------------
|
||||
→ Value (`inj₁ {B = B} V)
|
||||
|
||||
Inj₂ : ∀ {Γ A B} {W : Γ ⊢ B}
|
||||
V-inj₂ : ∀ {Γ A B} {W : Γ ⊢ B}
|
||||
→ Value W
|
||||
------------------------
|
||||
→ Value (`inj₂ {A = A} W)
|
||||
|
|
@ -505,8 +533,8 @@ 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 (Inj₁ VM) (ξ-inj₁ M—→M′) = Value-lemma VM M—→M′
|
||||
Value-lemma (Inj₂ VN) (ξ-inj₂ 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′
|
||||
|
|
@ -563,14 +591,14 @@ progress (`proj₂ L) with progress L
|
|||
... | done (V-⟨ VM , VN ⟩) = step (β-×₂ VM VN)
|
||||
progress (`inj₁ M) with progress M
|
||||
... | step M—→M′ = step (ξ-inj₁ M—→M′)
|
||||
... | done VM = done (Inj₁ VM)
|
||||
... | done VM = done (V-inj₁ VM)
|
||||
progress (`inj₂ N) with progress N
|
||||
... | step N—→N′ = step (ξ-inj₂ N—→N′)
|
||||
... | done VN = done (Inj₂ VN)
|
||||
... | done VN = done (V-inj₂ VN)
|
||||
progress (`case⊎ L M N) with progress L
|
||||
... | step L—→L′ = step (ξ-case⊎ L—→L′)
|
||||
... | done (Inj₁ VV) = step (β-⊎₁ VV)
|
||||
... | done (Inj₂ VW) = step (β-⊎₂ VW)
|
||||
... | 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′)
|
||||
|
|
|
|||
Loading…
Reference in a new issue