syntax changes to Typed
This commit is contained in:
wadler
parent
76d8d6bcbf
commit
62219722c0
1 changed files with 138 additions and 136 deletions
274
src/Typed.lagda
274
src/Typed.lagda
|
|
@ -4,6 +4,7 @@ layout : page
|
|||
permalink : /Typed
|
||||
---
|
||||
|
||||
|
||||
## Imports
|
||||
|
||||
\begin{code}
|
||||
|
|
@ -35,59 +36,60 @@ open import Collections using (_↔_)
|
|||
## Syntax
|
||||
|
||||
\begin{code}
|
||||
infixr 6 _⇒_
|
||||
infixr 5 _⟹_
|
||||
infixl 5 _,_⦂_
|
||||
infix 4 _∋_⦂_
|
||||
infix 4 _⊢_⦂_
|
||||
infix 5 ƛ_⦂_⇒_
|
||||
infix 5 ƛ_
|
||||
infix 5 `λ_⇒_
|
||||
infix 5 `λ_
|
||||
infixl 6 _·_
|
||||
infix 7 `_
|
||||
|
||||
Id : Set
|
||||
Id = ℕ
|
||||
|
||||
data Type : Set where
|
||||
o : Type
|
||||
_⇒_ : Type → Type → Type
|
||||
`ℕ : Type
|
||||
_⟹_ : Type → Type → Type
|
||||
|
||||
data Env : Set where
|
||||
ε : Env
|
||||
_,_⦂_ : Env → Id → Type → Env
|
||||
|
||||
data Term : Set where
|
||||
⌊_⌋ : Id → Term
|
||||
ƛ_⦂_⇒_ : Id → Type → Term → Term
|
||||
_·_ : Term → Term → Term
|
||||
`_ : Id → Term
|
||||
`λ_⇒_ : Id → Term → Term
|
||||
_·_ : Term → Term → Term
|
||||
|
||||
data _∋_⦂_ : Env → Id → Type → Set where
|
||||
|
||||
Z : ∀ {Γ A x} →
|
||||
-----------------
|
||||
Γ , x ⦂ A ∋ x ⦂ A
|
||||
Z : ∀ {Γ A x}
|
||||
-----------------
|
||||
→ Γ , x ⦂ A ∋ x ⦂ A
|
||||
|
||||
S : ∀ {Γ A B x y} →
|
||||
x ≢ y →
|
||||
Γ ∋ y ⦂ B →
|
||||
-----------------
|
||||
Γ , x ⦂ A ∋ y ⦂ B
|
||||
S : ∀ {Γ A B x y}
|
||||
→ x ≢ y
|
||||
→ Γ ∋ y ⦂ B
|
||||
-----------------
|
||||
→ Γ , x ⦂ A ∋ y ⦂ B
|
||||
|
||||
data _⊢_⦂_ : Env → Term → Type → Set where
|
||||
|
||||
⌊_⌋ : ∀ {Γ A x} →
|
||||
Γ ∋ x ⦂ A →
|
||||
---------------------
|
||||
Γ ⊢ ⌊ x ⌋ ⦂ A
|
||||
`_ : ∀ {Γ A x}
|
||||
→ Γ ∋ x ⦂ A
|
||||
---------------------
|
||||
→ Γ ⊢ ` x ⦂ A
|
||||
|
||||
ƛ_ : ∀ {Γ x A N B} →
|
||||
Γ , x ⦂ A ⊢ N ⦂ B →
|
||||
--------------------------
|
||||
Γ ⊢ (ƛ x ⦂ A ⇒ N) ⦂ A ⇒ B
|
||||
`λ_ : ∀ {Γ x A N B}
|
||||
→ Γ , x ⦂ A ⊢ N ⦂ B
|
||||
------------------------
|
||||
→ Γ ⊢ (`λ x ⇒ N) ⦂ A ⟹ B
|
||||
|
||||
_·_ : ∀ {Γ L M A B} →
|
||||
Γ ⊢ L ⦂ A ⇒ B →
|
||||
Γ ⊢ M ⦂ A →
|
||||
--------------
|
||||
Γ ⊢ L · M ⦂ B
|
||||
_·_ : ∀ {Γ L M A B}
|
||||
→ Γ ⊢ L ⦂ A ⟹ B
|
||||
→ Γ ⊢ M ⦂ A
|
||||
--------------
|
||||
→ Γ ⊢ L · M ⦂ B
|
||||
\end{code}
|
||||
|
||||
## Test examples
|
||||
|
|
@ -118,32 +120,31 @@ n≢m : n ≢ m
|
|||
n≢m ()
|
||||
|
||||
Ch : Type
|
||||
Ch = (o ⇒ o) ⇒ o ⇒ o
|
||||
Ch = (`ℕ ⟹ `ℕ) ⟹ `ℕ ⟹ `ℕ
|
||||
|
||||
two : Term
|
||||
two = ƛ s ⦂ (o ⇒ o) ⇒ ƛ z ⦂ o ⇒ (⌊ s ⌋ · (⌊ s ⌋ · ⌊ z ⌋))
|
||||
two = `λ s ⇒ `λ z ⇒ (` s · (` s · ` z))
|
||||
|
||||
⊢two : ε ⊢ two ⦂ Ch
|
||||
⊢two = ƛ ƛ ⌊ ⊢s ⌋ · (⌊ ⊢s ⌋ · ⌊ ⊢z ⌋)
|
||||
⊢two = `λ `λ ` ⊢s · (` ⊢s · ` ⊢z)
|
||||
where
|
||||
⊢s = S z≢s Z
|
||||
⊢z = Z
|
||||
|
||||
four : Term
|
||||
four = ƛ s ⦂ (o ⇒ o) ⇒ ƛ z ⦂ o ⇒ ⌊ s ⌋ · (⌊ s ⌋ · (⌊ s ⌋ · (⌊ s ⌋ · ⌊ z ⌋)))
|
||||
four = `λ s ⇒ `λ z ⇒ ` s · (` s · (` s · (` s · ` z)))
|
||||
|
||||
⊢four : ε ⊢ four ⦂ Ch
|
||||
⊢four = ƛ ƛ ⌊ ⊢s ⌋ · (⌊ ⊢s ⌋ · (⌊ ⊢s ⌋ · (⌊ ⊢s ⌋ · ⌊ ⊢z ⌋)))
|
||||
⊢four = `λ `λ ` ⊢s · (` ⊢s · (` ⊢s · (` ⊢s · ` ⊢z)))
|
||||
where
|
||||
⊢s = S z≢s Z
|
||||
⊢z = Z
|
||||
|
||||
plus : Term
|
||||
plus = ƛ m ⦂ Ch ⇒ ƛ n ⦂ Ch ⇒ ƛ s ⦂ (o ⇒ o) ⇒ ƛ z ⦂ o ⇒
|
||||
⌊ m ⌋ · ⌊ s ⌋ · (⌊ n ⌋ · ⌊ s ⌋ · ⌊ z ⌋)
|
||||
plus = `λ m ⇒ `λ n ⇒ `λ s ⇒ `λ z ⇒ ` m · ` s · (` n · ` s · ` z)
|
||||
|
||||
⊢plus : ε ⊢ plus ⦂ Ch ⇒ Ch ⇒ Ch
|
||||
⊢plus = ƛ ƛ ƛ ƛ ⌊ ⊢m ⌋ · ⌊ ⊢s ⌋ · (⌊ ⊢n ⌋ · ⌊ ⊢s ⌋ · ⌊ ⊢z ⌋)
|
||||
⊢plus : ε ⊢ plus ⦂ Ch ⟹ Ch ⟹ Ch
|
||||
⊢plus = `λ `λ `λ `λ ` ⊢m · ` ⊢s · (` ⊢n · ` ⊢s · ` ⊢z)
|
||||
where
|
||||
⊢z = Z
|
||||
⊢s = S z≢s Z
|
||||
|
|
@ -162,8 +163,8 @@ four′ = plus · two · two
|
|||
|
||||
\begin{code}
|
||||
⟦_⟧ᵀ : Type → Set
|
||||
⟦ o ⟧ᵀ = ℕ
|
||||
⟦ A ⇒ B ⟧ᵀ = ⟦ A ⟧ᵀ → ⟦ B ⟧ᵀ
|
||||
⟦ `ℕ ⟧ᵀ = ℕ
|
||||
⟦ A ⟹ B ⟧ᵀ = ⟦ A ⟧ᵀ → ⟦ B ⟧ᵀ
|
||||
|
||||
⟦_⟧ᴱ : Env → Set
|
||||
⟦ ε ⟧ᴱ = ⊤
|
||||
|
|
@ -174,8 +175,8 @@ four′ = plus · two · two
|
|||
⟦ S _ x ⟧ⱽ ⟨ ρ , v ⟩ = ⟦ x ⟧ⱽ ρ
|
||||
|
||||
⟦_⟧ : ∀ {Γ M A} → Γ ⊢ M ⦂ A → ⟦ Γ ⟧ᴱ → ⟦ A ⟧ᵀ
|
||||
⟦ ⌊ x ⌋ ⟧ ρ = ⟦ x ⟧ⱽ ρ
|
||||
⟦ ƛ ⊢N ⟧ ρ = λ{ v → ⟦ ⊢N ⟧ ⟨ ρ , v ⟩ }
|
||||
⟦ ` x ⟧ ρ = ⟦ x ⟧ⱽ ρ
|
||||
⟦ `λ ⊢N ⟧ ρ = λ{ v → ⟦ ⊢N ⟧ ⟨ ρ , v ⟩ }
|
||||
⟦ ⊢L · ⊢M ⟧ ρ = (⟦ ⊢L ⟧ ρ) (⟦ ⊢M ⟧ ρ)
|
||||
|
||||
_ : ⟦ ⊢four′ ⟧ tt ≡ ⟦ ⊢four ⟧ tt
|
||||
|
|
@ -194,22 +195,22 @@ lookup {Γ , x ⦂ A} Z = x
|
|||
lookup {Γ , x ⦂ A} (S _ k) = lookup {Γ} k
|
||||
|
||||
erase : ∀ {Γ M A} → Γ ⊢ M ⦂ A → Term
|
||||
erase ⌊ k ⌋ = ⌊ lookup k ⌋
|
||||
erase (ƛ_ {x = x} {A = A} ⊢N) = ƛ x ⦂ A ⇒ erase ⊢N
|
||||
erase (⊢L · ⊢M) = erase ⊢L · erase ⊢M
|
||||
erase (` k) = ` lookup k
|
||||
erase (`λ_ {x = x} ⊢N) = `λ x ⇒ erase ⊢N
|
||||
erase (⊢L · ⊢M) = erase ⊢L · erase ⊢M
|
||||
\end{code}
|
||||
|
||||
### Properties of erasure
|
||||
|
||||
\begin{code}
|
||||
lookup-lemma : ∀ {Γ x A} → (k : Γ ∋ x ⦂ A) → lookup k ≡ x
|
||||
lookup-lemma : ∀ {Γ x A} → (⊢x : Γ ∋ x ⦂ A) → lookup ⊢x ≡ x
|
||||
lookup-lemma Z = refl
|
||||
lookup-lemma (S _ k) = lookup-lemma k
|
||||
|
||||
erase-lemma : ∀ {Γ M A} → (⊢M : Γ ⊢ M ⦂ A) → erase ⊢M ≡ M
|
||||
erase-lemma ⌊ k ⌋ = cong ⌊_⌋ (lookup-lemma k)
|
||||
erase-lemma (ƛ_ {x = x} {A = A} ⊢N) = cong (ƛ x ⦂ A ⇒_) (erase-lemma ⊢N)
|
||||
erase-lemma (⊢L · ⊢M) = cong₂ _·_ (erase-lemma ⊢L) (erase-lemma ⊢M)
|
||||
erase-lemma (` ⊢x) = cong `_ (lookup-lemma ⊢x)
|
||||
erase-lemma (`λ_ {x = x} ⊢N) = cong (`λ x ⇒_) (erase-lemma ⊢N)
|
||||
erase-lemma (⊢L · ⊢M) = cong₂ _·_ (erase-lemma ⊢L) (erase-lemma ⊢M)
|
||||
\end{code}
|
||||
|
||||
|
||||
|
|
@ -221,39 +222,25 @@ erase-lemma (⊢L · ⊢M) = cong₂ _·_ (erase-lemma ⊢L) (er
|
|||
open Collections.CollectionDec (Id) (_≟_)
|
||||
\end{code}
|
||||
|
||||
### Properties of sets
|
||||
|
||||
\begin{code}
|
||||
-- ⊆∷ : ∀ {y xs ys} → xs ⊆ ys → xs ⊆ y ∷ ys
|
||||
-- ∷⊆∷ : ∀ {x xs ys} → xs ⊆ ys → (x ∷ xs) ⊆ (x ∷ ys)
|
||||
-- []⊆ : ∀ {x xs} → [ x ] ⊆ xs → x ∈ xs
|
||||
-- ⊆[] : ∀ {x xs} → x ∈ xs → [ x ] ⊆ xs
|
||||
-- bind : ∀ {x xs} → xs \\ x ⊆ xs
|
||||
-- left : ∀ {xs ys} → xs ⊆ xs ∪ ys
|
||||
-- right : ∀ {xs ys} → ys ⊆ xs ∪ ys
|
||||
-- prev : ∀ {z y xs} → y ≢ z → z ∈ y ∷ xs → z ∈ xs
|
||||
\end{code}
|
||||
|
||||
### Free variables
|
||||
|
||||
\begin{code}
|
||||
free : Term → List Id
|
||||
free ⌊ x ⌋ = [ x ]
|
||||
free (ƛ x ⦂ A ⇒ N) = free N \\ x
|
||||
free (L · M) = free L ∪ free M
|
||||
free (` x) = [ x ]
|
||||
free (`λ x ⇒ N) = free N \\ x
|
||||
free (L · M) = free L ∪ free M
|
||||
\end{code}
|
||||
|
||||
|
||||
### Fresh identifier
|
||||
|
||||
\begin{code}
|
||||
fresh : List Id → Id
|
||||
fresh = foldr _⊔_ 0 ∘ map suc
|
||||
|
||||
⊔-lemma : ∀ {x xs} → x ∈ xs → suc x ≤ fresh xs
|
||||
⊔-lemma {x} {.x ∷ xs} here = m≤m⊔n (suc x) (fresh xs)
|
||||
⊔-lemma {x} {y ∷ xs} (there x∈) = ≤-trans (⊔-lemma {x} {xs} x∈)
|
||||
(n≤m⊔n (suc y) (fresh xs))
|
||||
⊔-lemma : ∀ {w xs} → w ∈ xs → suc w ≤ fresh xs
|
||||
⊔-lemma {w} {x ∷ xs} here = m≤m⊔n (suc w) (fresh xs)
|
||||
⊔-lemma {w} {x ∷ xs} (there x∈) = ≤-trans (⊔-lemma {w} {xs} x∈)
|
||||
(n≤m⊔n (suc x) (fresh xs))
|
||||
|
||||
fresh-lemma : ∀ {x xs} → x ∈ xs → fresh xs ≢ x
|
||||
fresh-lemma x∈ refl = 1+n≰n (⊔-lemma x∈)
|
||||
|
|
@ -263,7 +250,9 @@ fresh-lemma x∈ refl = 1+n≰n (⊔-lemma x∈)
|
|||
|
||||
\begin{code}
|
||||
∅ : Id → Term
|
||||
∅ x = ⌊ x ⌋
|
||||
∅ x = ` x
|
||||
|
||||
infixl 5 _,_↦_
|
||||
|
||||
_,_↦_ : (Id → Term) → Id → Term → (Id → Term)
|
||||
(ρ , x ↦ M) w with w ≟ x
|
||||
|
|
@ -275,8 +264,8 @@ _,_↦_ : (Id → Term) → Id → Term → (Id → Term)
|
|||
|
||||
\begin{code}
|
||||
subst : List Id → (Id → Term) → Term → Term
|
||||
subst ys ρ ⌊ x ⌋ = ρ x
|
||||
subst ys ρ (ƛ x ⦂ A ⇒ N) = ƛ y ⦂ A ⇒ subst (y ∷ ys) (ρ , x ↦ ⌊ y ⌋) N
|
||||
subst ys ρ (` x) = ρ x
|
||||
subst ys ρ (`λ x ⇒ N) = `λ y ⇒ subst (y ∷ ys) (ρ , x ↦ ` y) N
|
||||
where
|
||||
y = fresh ys
|
||||
subst ys ρ (L · M) = subst ys ρ L · subst ys ρ M
|
||||
|
|
@ -291,74 +280,80 @@ N [ x := M ] = subst (free M ∪ (free N \\ x)) (∅ , x ↦ M) N
|
|||
\begin{code}
|
||||
data Value : Term → Set where
|
||||
|
||||
Fun : ∀ {x A N} →
|
||||
--------------------
|
||||
Value (ƛ x ⦂ A ⇒ N)
|
||||
Fun : ∀ {x N}
|
||||
---------------
|
||||
→ Value (`λ x ⇒ N)
|
||||
\end{code}
|
||||
|
||||
## Reduction
|
||||
|
||||
\begin{code}
|
||||
infix 4 _⟹_
|
||||
infix 4 _⟶_
|
||||
|
||||
data _⟹_ : Term → Term → Set where
|
||||
data _⟶_ : Term → Term → Set where
|
||||
|
||||
β-⇒ : ∀ {x A N V} →
|
||||
β-⟹ : ∀ {x N V}
|
||||
→ Value V
|
||||
------------------------------
|
||||
→ (`λ x ⇒ N) · V ⟶ N [ x := V ]
|
||||
|
||||
ξ-⟹₁ : ∀ {L L′ M}
|
||||
→ L ⟶ L′
|
||||
----------------
|
||||
→ L · M ⟶ L′ · M
|
||||
|
||||
ξ-⟹₂ : ∀ {V M M′} →
|
||||
Value V →
|
||||
----------------------------------
|
||||
(ƛ x ⦂ A ⇒ N) · V ⟹ N [ x := V ]
|
||||
|
||||
ξ-⇒₁ : ∀ {L L′ M} →
|
||||
L ⟹ L′ →
|
||||
M ⟶ M′ →
|
||||
----------------
|
||||
L · M ⟹ L′ · M
|
||||
|
||||
ξ-⇒₂ : ∀ {V M M′} →
|
||||
Value V →
|
||||
M ⟹ M′ →
|
||||
----------------
|
||||
V · M ⟹ V · M′
|
||||
V · M ⟶ V · M′
|
||||
\end{code}
|
||||
|
||||
## Reflexive and transitive closure
|
||||
|
||||
\begin{code}
|
||||
infix 2 _⟹*_
|
||||
infix 2 _⟶*_
|
||||
infix 1 begin_
|
||||
infixr 2 _⟹⟨_⟩_
|
||||
infixr 2 _⟶⟨_⟩_
|
||||
infix 3 _∎
|
||||
|
||||
data _⟹*_ : Term → Term → Set where
|
||||
data _⟶*_ : Term → Term → Set where
|
||||
|
||||
_∎ : ∀ {M} →
|
||||
-------------
|
||||
M ⟹* M
|
||||
_∎ : ∀ {M}
|
||||
-------------
|
||||
→ M ⟶* M
|
||||
|
||||
_⟹⟨_⟩_ : ∀ (L : Term) {M N} →
|
||||
L ⟹ M →
|
||||
M ⟹* N →
|
||||
---------
|
||||
L ⟹* N
|
||||
_⟶⟨_⟩_ : ∀ (L : Term) {M N}
|
||||
→ L ⟶ M
|
||||
→ M ⟶* N
|
||||
---------
|
||||
→ L ⟶* N
|
||||
|
||||
begin_ : ∀ {M N} → (M ⟹* N) → (M ⟹* N)
|
||||
begin M⟹*N = M⟹*N
|
||||
begin_ : ∀ {M N} → (M ⟶* N) → (M ⟶* N)
|
||||
begin M⟶*N = M⟶*N
|
||||
\end{code}
|
||||
|
||||
## Progress
|
||||
|
||||
\begin{code}
|
||||
data Progress (M : Term) : Set where
|
||||
step : ∀ {N} → M ⟹ N → Progress M
|
||||
done : Value M → Progress M
|
||||
step : ∀ {N}
|
||||
→ M ⟶ N
|
||||
----------
|
||||
→ Progress M
|
||||
done :
|
||||
Value M
|
||||
----------
|
||||
→ Progress M
|
||||
|
||||
progress : ∀ {M A} → ε ⊢ M ⦂ A → Progress M
|
||||
progress ⌊ () ⌋
|
||||
progress (ƛ_ ⊢N) = done Fun
|
||||
progress (` ())
|
||||
progress (`λ_ ⊢N) = done Fun
|
||||
progress (⊢L · ⊢M) with progress ⊢L
|
||||
... | step L⟹L′ = step (ξ-⇒₁ L⟹L′)
|
||||
... | step L⟶L′ = step (ξ-⟹₁ L⟶L′)
|
||||
... | done Fun with progress ⊢M
|
||||
... | step M⟹M′ = step (ξ-⇒₂ Fun M⟹M′)
|
||||
... | done valM = step (β-⇒ valM)
|
||||
... | step M⟶M′ = step (ξ-⟹₂ Fun M⟶M′)
|
||||
... | done valM = step (β-⟹ valM)
|
||||
\end{code}
|
||||
|
||||
|
||||
|
|
@ -376,10 +371,10 @@ dom-lemma Z = here
|
|||
dom-lemma (S x≢y ⊢y) = there (dom-lemma ⊢y)
|
||||
|
||||
free-lemma : ∀ {Γ M A} → Γ ⊢ M ⦂ A → free M ⊆ dom Γ
|
||||
free-lemma ⌊ ⊢x ⌋ w∈ with w∈
|
||||
... | here = dom-lemma ⊢x
|
||||
free-lemma (` ⊢x) w∈ with w∈
|
||||
... | here = dom-lemma ⊢x
|
||||
... | there ()
|
||||
free-lemma {Γ} (ƛ_ {x = x} {N = N} ⊢N) = proj₂ lemma-\\-∷ (free-lemma ⊢N)
|
||||
free-lemma {Γ} (`λ_ {x = x} {N = N} ⊢N) = proj₂ lemma-\\-∷ (free-lemma ⊢N)
|
||||
free-lemma (⊢L · ⊢M) w∈ with proj₂ lemma-⊎-∪ w∈
|
||||
... | inj₁ ∈L = free-lemma ⊢L ∈L
|
||||
... | inj₂ ∈M = free-lemma ⊢M ∈M
|
||||
|
|
@ -388,13 +383,15 @@ free-lemma (⊢L · ⊢M) w∈ with proj₂ lemma-⊎-∪ w∈
|
|||
### Renaming
|
||||
|
||||
\begin{code}
|
||||
⊢rename : ∀ {Γ Δ xs} → (∀ {x A} → x ∈ xs → Γ ∋ x ⦂ A → Δ ∋ x ⦂ A) →
|
||||
(∀ {M A} → free M ⊆ xs → Γ ⊢ M ⦂ A → Δ ⊢ M ⦂ A)
|
||||
⊢rename ⊢σ ⊆xs (⌊ ⊢x ⌋) = ⌊ ⊢σ ∈xs ⊢x ⌋
|
||||
⊢rename : ∀ {Γ Δ xs}
|
||||
→ (∀ {x A} → x ∈ xs → Γ ∋ x ⦂ A → Δ ∋ x ⦂ A)
|
||||
--------------------------------------------------
|
||||
→ (∀ {M A} → free M ⊆ xs → Γ ⊢ M ⦂ A → Δ ⊢ M ⦂ A)
|
||||
⊢rename ⊢σ ⊆xs (` ⊢x) = ` ⊢σ ∈xs ⊢x
|
||||
where
|
||||
∈xs = proj₂ lemma-[_] ⊆xs
|
||||
⊢rename {Γ} {Δ} {xs} ⊢σ ⊆xs (ƛ_ {x = x} {A = A} {N = N} ⊢N)
|
||||
= ƛ (⊢rename {Γ′} {Δ′} {xs′} ⊢σ′ ⊆xs′ ⊢N)
|
||||
⊢rename {Γ} {Δ} {xs} ⊢σ ⊆xs (`λ_ {x = x} {A = A} {N = N} ⊢N)
|
||||
= `λ (⊢rename {Γ′} {Δ′} {xs′} ⊢σ′ ⊆xs′ ⊢N)
|
||||
where
|
||||
Γ′ = Γ , x ⦂ A
|
||||
Δ′ = Δ , x ⦂ A
|
||||
|
|
@ -407,7 +404,7 @@ free-lemma (⊢L · ⊢M) w∈ with proj₂ lemma-⊎-∪ w∈
|
|||
... | there ∈xs = S x≢y (⊢σ ∈xs ⊢y)
|
||||
|
||||
⊆xs′ : free N ⊆ xs′
|
||||
⊆xs′ = proj₁ lemma-\\-∷ ⊆xs
|
||||
⊆xs′ = proj₁ lemma-\\-∷ ⊆xs
|
||||
⊢rename {xs = xs} ⊢σ {L · M} ⊆xs (⊢L · ⊢M)
|
||||
= ⊢rename ⊢σ L⊆ ⊢L · ⊢rename ⊢σ M⊆ ⊢M
|
||||
where
|
||||
|
|
@ -426,21 +423,22 @@ lemma₂ : ∀ {w x xs} → x ≢ w → w ∈ x ∷ xs → w ∈ xs
|
|||
lemma₂ x≢ here = ⊥-elim (x≢ refl)
|
||||
lemma₂ _ (there w∈) = w∈
|
||||
|
||||
⊢subst : ∀ {Γ Δ xs ys ρ} →
|
||||
(∀ {x} → x ∈ xs → free (ρ x) ⊆ ys) →
|
||||
(∀ {x A} → x ∈ xs → Γ ∋ x ⦂ A → Δ ⊢ ρ x ⦂ A) →
|
||||
(∀ {M A} → free M ⊆ xs → Γ ⊢ M ⦂ A → Δ ⊢ subst ys ρ M ⦂ A)
|
||||
⊢subst Σ ⊢ρ ⊆xs ⌊ ⊢x ⌋
|
||||
⊢subst : ∀ {Γ Δ xs ys ρ}
|
||||
→ (∀ {x} → x ∈ xs → free (ρ x) ⊆ ys)
|
||||
→ (∀ {x A} → x ∈ xs → Γ ∋ x ⦂ A → Δ ⊢ ρ x ⦂ A)
|
||||
-------------------------------------------------------------
|
||||
→ (∀ {M A} → free M ⊆ xs → Γ ⊢ M ⦂ A → Δ ⊢ subst ys ρ M ⦂ A)
|
||||
⊢subst Σ ⊢ρ ⊆xs (` ⊢x)
|
||||
= ⊢ρ (⊆xs here) ⊢x
|
||||
⊢subst {Γ} {Δ} {xs} {ys} {ρ} Σ ⊢ρ ⊆xs (ƛ_ {x = x} {A = A} {N = N} ⊢N)
|
||||
= ƛ_ {x = y} {A = A} (⊢subst {Γ′} {Δ′} {xs′} {ys′} {ρ′} Σ′ ⊢ρ′ ⊆xs′ ⊢N)
|
||||
⊢subst {Γ} {Δ} {xs} {ys} {ρ} Σ ⊢ρ ⊆xs (`λ_ {x = x} {A = A} {N = N} ⊢N)
|
||||
= `λ_ {x = y} {A = A} (⊢subst {Γ′} {Δ′} {xs′} {ys′} {ρ′} Σ′ ⊢ρ′ ⊆xs′ ⊢N)
|
||||
where
|
||||
y = fresh ys
|
||||
Γ′ = Γ , x ⦂ A
|
||||
Δ′ = Δ , y ⦂ A
|
||||
xs′ = x ∷ xs
|
||||
ys′ = y ∷ ys
|
||||
ρ′ = ρ , x ↦ ⌊ y ⌋
|
||||
ρ′ = ρ , x ↦ ` y
|
||||
|
||||
Σ′ : ∀ {w} → w ∈ xs′ → free (ρ′ w) ⊆ ys′
|
||||
Σ′ {w} here with w ≟ x
|
||||
|
|
@ -458,7 +456,7 @@ lemma₂ _ (there w∈) = w∈
|
|||
|
||||
⊢ρ′ : ∀ {w C} → w ∈ xs′ → Γ′ ∋ w ⦂ C → Δ′ ⊢ ρ′ w ⦂ C
|
||||
⊢ρ′ _ Z with x ≟ x
|
||||
... | yes _ = ⌊ Z ⌋
|
||||
... | yes _ = ` Z
|
||||
... | no x≢x = ⊥-elim (x≢x refl)
|
||||
⊢ρ′ {w} w∈′ (S x≢w ⊢w) with w ≟ x
|
||||
... | yes refl = ⊥-elim (x≢w refl)
|
||||
|
|
@ -499,7 +497,7 @@ lemma₂ _ (there w∈) = w∈
|
|||
... | no x≢x = ⊥-elim (x≢x refl)
|
||||
⊢ρ {z} z∈ (S x≢z ⊢z) with z ≟ x
|
||||
... | yes refl = ⊥-elim (x≢z refl)
|
||||
... | no _ = ⌊ ⊢z ⌋
|
||||
... | no _ = ` ⊢z
|
||||
|
||||
⊆xs : free N ⊆ xs
|
||||
⊆xs x∈ = x∈
|
||||
|
|
@ -508,12 +506,16 @@ lemma₂ _ (there w∈) = w∈
|
|||
### Preservation
|
||||
|
||||
\begin{code}
|
||||
preservation : ∀ {Γ M N A} → Γ ⊢ M ⦂ A → M ⟹ N → Γ ⊢ N ⦂ A
|
||||
preservation ⌊ ⊢x ⌋ ()
|
||||
preservation (ƛ ⊢N) ()
|
||||
preservation (⊢L · ⊢M) (ξ-⇒₁ L⟹L′) = preservation ⊢L L⟹L′ · ⊢M
|
||||
preservation (⊢V · ⊢M) (ξ-⇒₂ valV M⟹M′) = ⊢V · preservation ⊢M M⟹M′
|
||||
preservation ((ƛ ⊢N) · ⊢W) (β-⇒ valW) = ⊢substitution ⊢N ⊢W
|
||||
preservation : ∀ {Γ M N A}
|
||||
→ Γ ⊢ M ⦂ A
|
||||
→ M ⟶ N
|
||||
---------
|
||||
→ Γ ⊢ N ⦂ A
|
||||
preservation (` ⊢x) ()
|
||||
preservation (`λ ⊢N) ()
|
||||
preservation (⊢L · ⊢M) (ξ-⟹₁ L⟶L′) = preservation ⊢L L⟶L′ · ⊢M
|
||||
preservation (⊢V · ⊢M) (ξ-⟹₂ valV M⟶M′) = ⊢V · preservation ⊢M M⟶M′
|
||||
preservation ((`λ ⊢N) · ⊢W) (β-⟹ valW) = ⊢substitution ⊢N ⊢W
|
||||
\end{code}
|
||||
|
||||
|
||||
|
|
|
|||
Loading…
Reference in a new issue