michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

lemmas in Collections and Typed renamed

Browse source
This commit is contained in:
wadler 2018-04-20 15:47:25 -03:00
parent 62219722c0
commit 10dcc7c76b
3 changed files with 213 additions and 249 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

128
src/Collections.lagda
View file

@ -24,7 +24,7 @@ open import Data.Empty using (⊥; ⊥-elim)
open import Isomorphism using (_≃_)
open import Function using (_∘_)
open import Level using (Level)
open import Data.List using (List; []; _∷_; _++_; map; foldr; filter)
open import Data.List using (List; []; _∷_; [_]; _++_; map; foldr; filter)
open import Data.List.All using (All; []; _∷_)
open import Data.List.Any using (Any; here; there)
open import Data.Maybe using (Maybe; just; nothing)
@ -49,15 +49,11 @@ module CollectionDec (A : Set) (_≟_ : ∀ (x y : A) → Dec (x ≡ y)) where
Coll : Set → Set
Coll A = List A
[_] : A → Coll A
[ x ] = x ∷ []
infix 4 _∈_
infix 4 _⊆_
infixl 5 _∪_
infixl 5 _\\_
data _∈_ : A → Coll A → Set where
data _∈_ : A → List A → Set where
here : ∀ {x xs} →
----------
@ -68,13 +64,10 @@ module CollectionDec (A : Set) (_≟_ : ∀ (x y : A) → Dec (x ≡ y)) where
----------
w ∈ x ∷ xs
_⊆_ : Coll A → Coll A → Set
_⊆_ : List A → List A → Set
xs ⊆ ys = ∀ {w} → w ∈ xs → w ∈ ys
_∪_ : Coll A → Coll A → Coll A
_∪_ = _++_
_\\_ : Coll A → A → Coll A
_\\_ : List A → A → List A
xs \\ x = filter (¬? ∘ (_≟ x)) xs
refl-⊆ : ∀ {xs} → xs ⊆ xs
@ -83,83 +76,62 @@ module CollectionDec (A : Set) (_≟_ : ∀ (x y : A) → Dec (x ≡ y)) where
trans-⊆ : ∀ {xs ys zs} → xs ⊆ ys → ys ⊆ zs → xs ⊆ zs
trans-⊆ xs⊆ ys⊆ = ys⊆ ∘ xs⊆
lemma-[_] : ∀ {w xs} → w ∈ xs ↔ [ w ] ⊆ xs
lemma-[_] = ⟨ forward , backward ⟩
where
[_]-⊆ : ∀ {x xs} → [ x ] ⊆ x ∷ xs
[_]-⊆ here = here
[_]-⊆ (there ())
forward : ∀ {w xs} → w ∈ xs → [ w ] ⊆ xs
forward ∈xs here = ∈xs
forward ∈xs (there ())
lemma₂ : ∀ {w x xs} → x ≢ w → w ∈ x ∷ xs → w ∈ xs
lemma₂ x≢ here = ⊥-elim (x≢ refl)
lemma₂ _ (there w∈) = w∈
backward : ∀ {w xs} → [ w ] ⊆ xs → w ∈ xs
backward ⊆xs = ⊆xs here
there⟨_⟩ : ∀ {w x y xs} → w ∈ xs × w ≢ x → w ∈ y ∷ xs × w ≢ x
there⟨ ⟨ w∈ , w≢ ⟩ ⟩ = ⟨ there w∈ , w≢ ⟩
lemma-\\-∈-≢ : ∀ {w x xs} → w ∈ xs \\ x ↔ w ∈ xs × w ≢ x
lemma-\\-∈-≢ = ⟨ forward , backward ⟩
where
\\-to-∈-≢ : ∀ {w x xs} → w ∈ xs \\ x → w ∈ xs × w ≢ x
\\-to-∈-≢ {_} {x} {[]} ()
\\-to-∈-≢ {_} {x} {y ∷ _} w∈ with y ≟ x
\\-to-∈-≢ {_} {x} {y ∷ _} w∈ | yes refl = there⟨ \\-to-∈-≢ w∈ ⟩
\\-to-∈-≢ {_} {x} {y ∷ _} here | no w≢ = ⟨ here , w≢ ⟩
\\-to-∈-≢ {_} {x} {y ∷ _} (there w∈) | no _ = there⟨ \\-to-∈-≢ w∈ ⟩
next : ∀ {w x y xs} → w ∈ xs × w ≢ x → w ∈ y ∷ xs × w ≢ x
next ⟨ w∈ , w≢ ⟩ = ⟨ there w∈ , w≢ ⟩
forward : ∀ {w x xs} → w ∈ xs \\ x → w ∈ xs × w ≢ x
forward {_} {x} {[]} ()
forward {_} {x} {y ∷ _} w∈ with y ≟ x
forward {_} {x} {y ∷ _} w∈ | yes refl = next (forward w∈)
forward {_} {x} {y ∷ _} here | no y≢ = ⟨ here , (λ y≡ → y≢ y≡) ⟩
forward {_} {x} {y ∷ _} (there w∈) | no _ = next (forward w∈)
backward : ∀ {w x xs} → w ∈ xs × w ≢ x → w ∈ xs \\ x
backward {_} {x} {y ∷ _} ⟨ here , w≢ ⟩
with y ≟ x
... | yes refl = ⊥-elim (w≢ refl)
... | no _ = here
backward {_} {x} {y ∷ _} ⟨ there w∈ , w≢ ⟩
with y ≟ x
... | yes refl = backward ⟨ w∈ , w≢ ⟩
... | no _ = there (backward ⟨ w∈ , w≢ ⟩)
∈-≢-to-\\ : ∀ {w x xs} → w ∈ xs → w ≢ x → w ∈ xs \\ x
∈-≢-to-\\ {_} {x} {y ∷ _} here w≢ with y ≟ x
... | yes refl = ⊥-elim (w≢ refl)
... | no _ = here
∈-≢-to-\\ {_} {x} {y ∷ _} (there w∈) w≢ with y ≟ x
... | yes refl = ∈-≢-to-\\ w∈ w≢
... | no _ = there (∈-≢-to-\\ w∈ w≢)
lemma-\\-∷ : ∀ {x xs ys} → xs \\ x ⊆ ys ↔ xs ⊆ x ∷ ys
lemma-\\-∷ = ⟨ forward , backward ⟩
where
\\-to-∷ : ∀ {x xs ys} → xs \\ x ⊆ ys → xs ⊆ x ∷ ys
\\-to-∷ {x} ⊆ys {w} ∈xs
with w ≟ x
... | yes refl = here
... | no ≢x = there (⊆ys (∈-≢-to-\\ ∈xs ≢x))
forward : ∀ {x xs ys} → xs \\ x ⊆ ys → xs ⊆ x ∷ ys
forward {x} ⊆ys {w} ∈xs
with w ≟ x
... | yes refl = here
... | no ≢x = there (⊆ys (proj₂ lemma-\\-∈-≢ ⟨ ∈xs , ≢x ⟩))
∷-to-\\ : ∀ {x xs ys} → xs ⊆ x ∷ ys → xs \\ x ⊆ ys
∷-to-\\ {x} xs⊆ {w} w∈
with \\-to-∈-≢ w∈
... | ⟨ ∈xs , ≢x ⟩ with w ≟ x
... | yes refl = ⊥-elim (≢x refl)
... | no w≢ with (xs⊆ ∈xs)
... | here = ⊥-elim (≢x refl)
... | there ∈ys = ∈ys
backward : ∀ {x xs ys} → xs ⊆ x ∷ ys → xs \\ x ⊆ ys
backward {x} xs⊆ {w} w∈
with proj₁ lemma-\\-∈-≢ w∈
... | ⟨ ∈xs , ≢x ⟩ with w ≟ x
... | yes refl = ⊥-elim (≢x refl)
... | no w≢ with (xs⊆ ∈xs)
... | here = ⊥-elim (≢x refl)
... | there ∈ys = ∈ys
⊆-++₁ : ∀ {xs ys} → xs ⊆ xs ++ ys
⊆-++₁ here = here
⊆-++₁ (there ∈xs) = there (⊆-++₁ ∈xs)
lemma-∪₁ : ∀ {xs ys} → xs ⊆ xs ∪ ys
lemma-∪₁ here = here
lemma-∪₁ (there ∈xs) = there (lemma-∪₁ ∈xs)
⊆-++₂ : ∀ {xs ys} → ys ⊆ xs ++ ys
⊆-++₂ {[]} ∈ys = ∈ys
⊆-++₂ {x ∷ xs} ∈ys = there (⊆-++₂ {xs} ∈ys)
lemma-∪₂ : ∀ {xs ys} → ys ⊆ xs ∪ ys
lemma-∪₂ {[]} ∈ys = ∈ys
lemma-∪₂ {x ∷ xs} ∈ys = there (lemma-∪₂ {xs} ∈ys)
lemma-⊎-∪ : ∀ {w xs ys} → w ∈ xs ⊎ w ∈ ys ↔ w ∈ xs ∪ ys
lemma-⊎-∪ = ⟨ forward , backward ⟩
where
forward : ∀ {w xs ys} → w ∈ xs ⊎ w ∈ ys → w ∈ xs ∪ ys
forward (inj₁ ∈xs) = lemma-∪₁ ∈xs
forward (inj₂ ∈ys) = lemma-∪₂ ∈ys
backward : ∀ {xs ys w} → w ∈ xs ∪ ys → w ∈ xs ⊎ w ∈ ys
backward {[]} ∈ys = inj₂ ∈ys
backward {x ∷ xs} here = inj₁ here
backward {x ∷ xs} (there w∈) with backward {xs} w∈
... | inj₁ ∈xs = inj₁ (there ∈xs)
... | inj₂ ∈ys = inj₂ ∈ys
++-to-⊎ : ∀ {xs ys w} → w ∈ xs ++ ys → w ∈ xs ⊎ w ∈ ys
++-to-⊎ {[]} ∈ys = inj₂ ∈ys
++-to-⊎ {x ∷ xs} here = inj₁ here
++-to-⊎ {x ∷ xs} (there w∈) with ++-to-⊎ {xs} w∈
... | inj₁ ∈xs = inj₁ (there ∈xs)
... | inj₂ ∈ys = inj₂ ∈ys
\end{code}

60
src/Typed.lagda
View file

@ -15,7 +15,7 @@ module Typed where
import Relation.Binary.PropositionalEquality as Eq
open Eq using (_≡_; refl; sym; trans; cong; cong₂; _≢_)
open import Data.Empty using (⊥; ⊥-elim)
open import Data.List using (List; []; _∷_; _++_; map; foldr; filter)
open import Data.List using (List; []; _∷_; [_]; _++_; map; foldr; filter)
open import Data.List.Any using (Any; here; there)
open import Data.Nat using (ℕ; zero; suc; _+_; _∸_; _≤_; _⊔_; _≟_)
open import Data.Nat.Properties using (≤-refl; ≤-trans; m≤m⊔n; n≤m⊔n; 1+n≰n)
@ -228,7 +228,7 @@ open Collections.CollectionDec (Id) (_≟_)
free : Term → List Id
free (` x) = [ x ]
free (`λ x ⇒ N) = free N \\ x
free (L · M) = free L ∪ free M
free (L · M) = free L ++ free M
\end{code}
### Fresh identifier
@ -238,9 +238,8 @@ fresh : List Id → Id
fresh = foldr _⊔_ 0 ∘ map suc
⊔-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))
⊔-lemma {_} {_ ∷ xs} here = m≤m⊔n _ (fresh xs)
⊔-lemma {_} {_ ∷ xs} (there x∈) = ≤-trans (⊔-lemma x∈) (n≤m⊔n _ (fresh xs))
fresh-lemma : ∀ {x xs} → x ∈ xs → fresh xs ≢ x
fresh-lemma x∈ refl = 1+n≰n (⊔-lemma x∈)
@ -271,7 +270,7 @@ subst ys ρ (`λ x ⇒ N) = `λ y ⇒ subst (y ∷ ys) (ρ , x ↦ ` y) N
subst ys ρ (L · M) = subst ys ρ L · subst ys ρ M
_[_:=_] : Term → Id → Term → Term
N [ x := M ] = subst (free M ∪ (free N \\ x)) (∅ , x ↦ M) N
N [ x := M ] = subst (free M ++ (free N \\ x)) (∅ , x ↦ M) N
\end{code}
@ -374,8 +373,8 @@ free-lemma : ∀ {Γ M A} → Γ ⊢ M ⦂ A → free M ⊆ dom Γ
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 (⊢L · ⊢M) w∈ with proj₂ lemma-⊎-∪ w∈
free-lemma {Γ} (`λ_ {x = x} {N = N} ⊢N) = ∷-to-\\ (free-lemma ⊢N)
free-lemma (⊢L · ⊢M) w∈ with ++-to-⊎ w∈
... | inj₁ ∈L = free-lemma ⊢L ∈L
... | inj₂ ∈M = free-lemma ⊢M ∈M
\end{code}
@ -387,11 +386,11 @@ free-lemma (⊢L · ⊢M) w∈ with proj₂ lemma-⊎-∪ w∈
→ (∀ {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) = ` ⊢σ ∈xs ⊢x
where
∈xs = proj₂ lemma-[_] ⊆xs
∈xs = ⊆xs here
⊢rename {Γ} {Δ} {xs} ⊢σ ⊆xs (`λ_ {x = x} {A = A} {N = N} ⊢N)
= `λ (⊢rename {Γ′} {Δ′} {xs′} ⊢σ′ ⊆xs′ ⊢N)
= `λ (⊢rename {Γ′} {Δ′} {xs′} ⊢σ′ ⊆xs′ ⊢N)
where
Γ′ = Γ , x ⦂ A
Δ′ = Δ , x ⦂ A
@ -404,25 +403,17 @@ free-lemma (⊢L · ⊢M) w∈ with proj₂ lemma-⊎-∪ w∈
... | there ∈xs = S x≢y (⊢σ ∈xs ⊢y)
⊆xs′ : free N ⊆ xs′
⊆xs′ = proj₁ lemma-\\-∷ ⊆xs
⊢rename {xs = xs} ⊢σ {L · M} ⊆xs (⊢L · ⊢M)
= ⊢rename ⊢σ L⊆ ⊢L · ⊢rename ⊢σ M⊆ ⊢M
⊆xs′ = \\-to-∷ ⊆xs
⊢rename ⊢σ ⊆xs (⊢L · ⊢M) = ⊢rename ⊢σ L⊆ ⊢L · ⊢rename ⊢σ M⊆ ⊢M
where
L⊆ = trans-⊆ (proj₁ lemma-⊎-∪ ∘ inj₁) ⊆xs
M⊆ = trans-⊆ (proj₁ lemma-⊎-∪ ∘ inj₂) ⊆xs
L⊆ = trans-⊆ ⊆-++₁ ⊆xs
M⊆ = trans-⊆ ⊆-++₂ ⊆xs
\end{code}
### Substitution preserves types
\begin{code}
lemma₁ : ∀ {y ys} → [ y ] ⊆ y ∷ ys
lemma₁ = proj₁ lemma-[_] here
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)
@ -442,33 +433,33 @@ lemma₂ _ (there w∈) = w∈
Σ′ : ∀ {w} → w ∈ xs′ → free (ρ′ w) ⊆ ys′
Σ′ {w} here with w ≟ x
... | yes refl = lemma₁
... | yes refl = [_]-⊆
... | no w≢ = ⊥-elim (w≢ refl)
Σ′ {w} (there w∈) with w ≟ x
... | yes refl = lemma₁
... | yes refl = [_]-⊆
... | no _ = there ∘ (Σ w∈)
⊆xs′ : free N ⊆ xs′
⊆xs′ = proj₁ lemma-\\-∷ ⊆xs
⊆xs′ = \\-to-∷ ⊆xs
⊢σ : ∀ {w C} → w ∈ ys → Δ ∋ w ⦂ C → Δ′ ∋ w ⦂ C
⊢σ w∈ ⊢w = S (fresh-lemma w∈) ⊢w
⊢ρ′ : ∀ {w C} → w ∈ xs′ → Γ′ ∋ w ⦂ C → Δ′ ⊢ ρ′ w ⦂ C
⊢ρ′ _ Z with x ≟ x
⊢ρ′ {w} Z with w ≟ x
... | yes _ = ` Z
... | no x≢x = ⊥-elim (x≢x refl)
... | no w≢x = ⊥-elim (w≢x refl)
⊢ρ′ {w} w∈′ (S x≢w ⊢w) with w ≟ x
... | yes refl = ⊥-elim (x≢w refl)
... | no _ = ⊢rename {Δ} {Δ′} {ys} ⊢σ (Σ w∈) (⊢ρ w∈ ⊢w)
where
w∈ = lemma₂ x≢w w∈′
⊢subst {xs = xs} Σ ⊢ρ {L · M} ⊆xs (⊢L · ⊢M)
⊢subst Σ ⊢ρ ⊆xs (⊢L · ⊢M)
= ⊢subst Σ ⊢ρ L⊆ ⊢L · ⊢subst Σ ⊢ρ M⊆ ⊢M
where
L⊆ = trans-⊆ lemma-∪₁ ⊆xs
M⊆ = trans-⊆ lemma-∪₂ ⊆xs
L⊆ = trans-⊆ ⊆-++₁ ⊆xs
M⊆ = trans-⊆ ⊆-++₂ ⊆xs
⊢substitution : ∀ {Γ x A N B M} →
Γ , x ⦂ A ⊢ N ⦂ B →
@ -480,15 +471,14 @@ lemma₂ _ (there w∈) = w∈
where
Γ′ = Γ , x ⦂ A
xs = free N
ys = free M ∪ (free N \\ x)
ys = free M ++ (free N \\ x)
ρ = ∅ , x ↦ M
Σ : ∀ {w} → w ∈ xs → free (ρ w) ⊆ ys
Σ {w} w∈ y∈ with w ≟ x
... | yes _ = lemma-∪₁ y∈
... | yes _ = ⊆-++₁ y∈
... | no w≢ with y∈
... | here = lemma-∪₂
(proj₂ lemma-\\-∈-≢ ⟨ w∈ , w≢ ⟩)
... | here = ⊆-++₂ (∈-≢-to-\\ w∈ w≢)
... | there ()
⊢ρ : ∀ {z C} → z ∈ xs → Γ′ ∋ z ⦂ C → Γ ⊢ ρ z ⦂ C

274
src/extra/Typed-backup.lagda
View file

@ -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}