1143 lines
33 KiB
Text
1143 lines
33 KiB
Text
---
|
||
title : "Quantitative: Counting Resources in Types"
|
||
layout : page
|
||
permalink : /Quantitative/
|
||
---
|
||
|
||
In previous chapters, we introduced the lambda calculus, with [a formalisation based on named variables][plfa.Lambda] and [an inherently-typed version][plfa.DeBruijn]. This chapter presents a refinement of those approaches, in which we not only care about the types of variables, but also about *how often they're used*.
|
||
|
||
|
||
# Imports & Module declaration
|
||
|
||
\begin{code}
|
||
open import Relation.Nullary using (Dec)
|
||
open import Relation.Binary.PropositionalEquality as Eq using (_≡_)
|
||
open import Algebra.Structures using (module IsSemiring; IsSemiring)
|
||
\end{code}
|
||
|
||
\begin{code}
|
||
module qtt.Quantitative
|
||
{Mult : Set}
|
||
(_+_ _*_ : Mult → Mult → Mult)
|
||
(0# 1# : Mult)
|
||
(*-+-isSemiring : IsSemiring _≡_ _+_ _*_ 0# 1#)
|
||
where
|
||
\end{code}
|
||
|
||
\begin{code}
|
||
open import Function using (_∘_; _|>_)
|
||
open Eq using (refl; sym; trans; cong)
|
||
open Eq.≡-Reasoning using (begin_; _≡⟨_⟩_; _≡⟨⟩_; _∎)
|
||
open IsSemiring *-+-isSemiring hiding (refl; sym; trans)
|
||
\end{code}
|
||
|
||
|
||
# Syntax
|
||
|
||
\begin{code}
|
||
infix 1 _⊢_
|
||
infix 1 _∋_
|
||
infixl 5 _,_
|
||
infixl 5 _,_∙_
|
||
infixr 6 [_∙_]⊸_
|
||
infixl 7 _+̇_
|
||
infixl 8 _*̇_
|
||
infixl 8 _*⟩_
|
||
\end{code}
|
||
|
||
|
||
# Types
|
||
|
||
\begin{code}
|
||
data Type : Set where
|
||
`0 : Type
|
||
[_∙_]⊸_ : Mult → Type → Type → Type
|
||
`1 : Type
|
||
_⊗_ : Type → Type → Type
|
||
_⊕_ : Type → Type → Type
|
||
\end{code}
|
||
|
||
\begin{code}
|
||
_⊸_ : Type → Type → Type
|
||
A ⊸ B = [ 1# ∙ A ]⊸ B
|
||
\end{code}
|
||
|
||
# Precontexts
|
||
|
||
\begin{code}
|
||
data Precontext : Set where
|
||
∅ : Precontext
|
||
_,_ : Precontext → Type → Precontext
|
||
|
||
variable γ δ : Precontext
|
||
\end{code}
|
||
|
||
\begin{code}
|
||
_ : Precontext
|
||
_ = ∅ , `0 ⊸ `0 , `0
|
||
\end{code}
|
||
|
||
|
||
# Variables and the lookup judgment
|
||
|
||
\begin{code}
|
||
data _∋_ : Precontext → Type → Set where
|
||
|
||
Z : ∀ {γ} {A}
|
||
|
||
---------
|
||
→ γ , A ∋ A
|
||
|
||
S_ : ∀ {γ} {A B}
|
||
|
||
→ γ ∋ A
|
||
---------
|
||
→ γ , B ∋ A
|
||
\end{code}
|
||
|
||
|
||
# Contexts
|
||
|
||
\begin{code}
|
||
data Context : Precontext → Set where
|
||
∅ : Context ∅
|
||
_,_∙_ : ∀ {Γ} → Context Γ → Mult → (A : Type) → Context (Γ , A)
|
||
|
||
variable Γ Δ Θ : Context γ
|
||
\end{code}
|
||
|
||
\begin{code}
|
||
_ : Context (∅ , `0 ⊸ `0 , `0)
|
||
_ = ∅ , 1# ∙ `0 ⊸ `0 , 0# ∙ `0
|
||
\end{code}
|
||
|
||
|
||
# Resources and linear algebra
|
||
|
||
Scaling.
|
||
|
||
\begin{code}
|
||
_*̇_ : ∀ {γ} → Mult → Context γ → Context γ
|
||
π *̇ ∅ = ∅
|
||
π *̇ (Γ , ρ ∙ A) = π *̇ Γ , π * ρ ∙ A
|
||
\end{code}
|
||
|
||
The 0-vector.
|
||
|
||
\begin{code}
|
||
0s : ∀ {γ} → Context γ
|
||
0s {∅} = ∅
|
||
0s {γ , A} = 0s , 0# ∙ A
|
||
\end{code}
|
||
|
||
Vector addition.
|
||
|
||
\begin{code}
|
||
_+̇_ : ∀ {γ} → Context γ → Context γ → Context γ
|
||
∅ +̇ ∅ = ∅
|
||
(Γ₁ , π₁ ∙ A) +̇ (Γ₂ , π₂ ∙ .A) = Γ₁ +̇ Γ₂ , π₁ + π₂ ∙ A
|
||
\end{code}
|
||
|
||
Matrices.
|
||
|
||
See [this sidenote][plfa.Quantitative.LinAlg].
|
||
|
||
\begin{code}
|
||
Matrix : Precontext → Precontext → Set
|
||
Matrix γ δ = ∀ {A} → γ ∋ A → Context δ
|
||
|
||
variable Ξ : Matrix γ δ
|
||
\end{code}
|
||
|
||
The identity matrix.
|
||
|
||
"x" "y" "z"
|
||
"x" 1 ∙ A , 0 ∙ B , 0 ∙ C
|
||
"y" 0 ∙ A , 1 ∙ B , 0 ∙ C
|
||
"z" 0 ∙ A , 0 ∙ B , 1 ∙ C
|
||
|
||
\begin{code}
|
||
identity : ∀ {γ} → Matrix γ γ
|
||
identity {γ , A} Z = 0s , 1# ∙ A
|
||
identity {γ , B} (S x) = identity x , 0# ∙ B
|
||
\end{code}
|
||
|
||
|
||
# Terms and the typing judgment
|
||
|
||
\begin{code}
|
||
data _⊢_ : ∀ {γ} (Γ : Context γ) (A : Type) → Set where
|
||
|
||
`_ : ∀ {γ} {A}
|
||
|
||
→ (x : γ ∋ A)
|
||
--------------
|
||
→ identity x ⊢ A
|
||
|
||
ƛ_ : ∀ {γ} {Γ : Context γ} {A B} {π}
|
||
|
||
→ Γ , π ∙ A ⊢ B
|
||
----------------
|
||
→ Γ ⊢ [ π ∙ A ]⊸ B
|
||
|
||
_·_ : ∀ {γ} {Γ Δ : Context γ} {A B} {π}
|
||
|
||
→ Γ ⊢ [ π ∙ A ]⊸ B
|
||
→ Δ ⊢ A
|
||
----------------
|
||
→ Γ +̇ π *̇ Δ ⊢ B
|
||
|
||
⟨⟩ : ∀ {γ}
|
||
|
||
-----------
|
||
→ 0s {γ} ⊢ `1
|
||
|
||
case1 : ∀ {γ} {Γ Δ : Context γ} {A}
|
||
|
||
→ Γ ⊢ `1
|
||
→ Δ ⊢ A
|
||
---------
|
||
→ Γ +̇ Δ ⊢ A
|
||
|
||
⟨_,_⟩ : ∀ {γ} {Γ Δ : Context γ} {A B}
|
||
|
||
→ Γ ⊢ A
|
||
→ Δ ⊢ B
|
||
-------------
|
||
→ Γ +̇ Δ ⊢ A ⊗ B
|
||
|
||
case⊗ : ∀ {γ} {Γ Δ : Context γ} {A B C}
|
||
|
||
→ Γ ⊢ A ⊗ B
|
||
→ Δ , 1# ∙ A , 1# ∙ B ⊢ C
|
||
-----------------------
|
||
→ Γ +̇ Δ ⊢ C
|
||
|
||
inj₁ : ∀ {γ} {Γ : Context γ} {A B}
|
||
|
||
→ Γ ⊢ A
|
||
---------
|
||
→ Γ ⊢ A ⊕ B
|
||
|
||
inj₂ : ∀ {γ} {Γ : Context γ} {A B}
|
||
|
||
→ Γ ⊢ B
|
||
---------
|
||
→ Γ ⊢ A ⊕ B
|
||
|
||
case⊕ : ∀ {γ} {Γ Δ : Context γ} {A B C}
|
||
|
||
→ Γ ⊢ A ⊕ B
|
||
→ Δ , 1# ∙ A ⊢ C
|
||
→ Δ , 1# ∙ B ⊢ C
|
||
--------------
|
||
→ Γ +̇ Δ ⊢ C
|
||
\end{code}
|
||
|
||
|
||
# Properties of vector operations
|
||
|
||
Unit scaling does nothing.
|
||
|
||
\begin{code}
|
||
*̇-identityˡ : ∀ {γ} (Γ : Context γ)
|
||
|
||
-----------
|
||
→ 1# *̇ Γ ≡ Γ
|
||
|
||
*̇-identityˡ ∅ = refl
|
||
*̇-identityˡ (Γ , π ∙ A) =
|
||
begin
|
||
1# *̇ Γ , 1# * π ∙ A
|
||
≡⟨ *-identityˡ π |> cong (1# *̇ Γ ,_∙ A) ⟩
|
||
1# *̇ Γ , π ∙ A
|
||
≡⟨ *̇-identityˡ Γ |> cong (_, π ∙ A) ⟩
|
||
Γ , π ∙ A
|
||
∎
|
||
\end{code}
|
||
|
||
Scaling by a product is the composition of scalings.
|
||
|
||
\begin{code}
|
||
*̇-assoc : ∀ {γ} (Γ : Context γ) {π π′}
|
||
|
||
------------------------------
|
||
→ (π * π′) *̇ Γ ≡ π *̇ (π′ *̇ Γ)
|
||
|
||
*̇-assoc ∅ = refl
|
||
*̇-assoc (Γ , π″ ∙ A) {π} {π′} =
|
||
begin
|
||
(π * π′) *̇ Γ , (π * π′) * π″ ∙ A
|
||
≡⟨ *-assoc π π′ π″ |> cong ((π * π′) *̇ Γ ,_∙ A) ⟩
|
||
(π * π′) *̇ Γ , π * (π′ * π″) ∙ A
|
||
≡⟨ *̇-assoc Γ |> cong (_, π * (π′ * π″) ∙ A) ⟩
|
||
π *̇ (π′ *̇ Γ) , π * (π′ * π″) ∙ A
|
||
∎
|
||
\end{code}
|
||
|
||
Scaling the 0-vector gives the 0-vector.
|
||
|
||
\begin{code}
|
||
*̇-zeroʳ : ∀ {γ} π
|
||
|
||
----------------
|
||
→ 0s {γ} ≡ π *̇ 0s
|
||
|
||
*̇-zeroʳ {∅} π = refl
|
||
*̇-zeroʳ {γ , A} π =
|
||
begin
|
||
0s , 0# ∙ A
|
||
≡⟨ zeroʳ π |> sym ∘ cong (0s ,_∙ A) ⟩
|
||
0s , π * 0# ∙ A
|
||
≡⟨ *̇-zeroʳ π |> cong (_, π * 0# ∙ A) ⟩
|
||
π *̇ 0s , π * 0# ∙ A
|
||
∎
|
||
\end{code}
|
||
|
||
Scaling by 0 gives the 0-vector.
|
||
|
||
\begin{code}
|
||
*̇-zeroˡ : ∀ {γ} (Γ : Context γ)
|
||
|
||
------------
|
||
→ 0# *̇ Γ ≡ 0s
|
||
|
||
*̇-zeroˡ ∅ = refl
|
||
*̇-zeroˡ (Γ , π ∙ A) =
|
||
begin
|
||
0# *̇ Γ , 0# * π ∙ A
|
||
≡⟨ zeroˡ π |> cong (0# *̇ Γ ,_∙ A) ⟩
|
||
0# *̇ Γ , 0# ∙ A
|
||
≡⟨ *̇-zeroˡ Γ |> cong (_, 0# ∙ A) ⟩
|
||
0s , 0# ∙ A
|
||
∎
|
||
\end{code}
|
||
|
||
Adding the 0-vector does nothing.
|
||
|
||
\begin{code}
|
||
+̇-identityˡ : ∀ {γ} (Γ : Context γ)
|
||
|
||
----------
|
||
→ 0s +̇ Γ ≡ Γ
|
||
|
||
+̇-identityˡ ∅ = refl
|
||
+̇-identityˡ (Γ , π ∙ A) =
|
||
begin
|
||
0s +̇ Γ , 0# + π ∙ A
|
||
≡⟨ +-identityˡ π |> cong (0s +̇ Γ ,_∙ A) ⟩
|
||
0s +̇ Γ , π ∙ A
|
||
≡⟨ +̇-identityˡ Γ |> cong (_, π ∙ A) ⟩
|
||
Γ , π ∙ A
|
||
∎
|
||
\end{code}
|
||
|
||
\begin{code}
|
||
+̇-identityʳ : ∀ {γ} (Γ : Context γ)
|
||
|
||
----------
|
||
→ Γ +̇ 0s ≡ Γ
|
||
|
||
+̇-identityʳ ∅ = refl
|
||
+̇-identityʳ (Γ , π ∙ A) =
|
||
begin
|
||
Γ +̇ 0s , π + 0# ∙ A
|
||
≡⟨ +-identityʳ π |> cong (Γ +̇ 0s ,_∙ A) ⟩
|
||
Γ +̇ 0s , π ∙ A
|
||
≡⟨ +̇-identityʳ Γ |> cong (_, π ∙ A) ⟩
|
||
Γ , π ∙ A
|
||
∎
|
||
\end{code}
|
||
|
||
Vector addition is commutative.
|
||
|
||
\begin{code}
|
||
+̇-comm : ∀ {γ} (Γ₁ Γ₂ : Context γ)
|
||
|
||
-----------------
|
||
→ Γ₁ +̇ Γ₂ ≡ Γ₂ +̇ Γ₁
|
||
|
||
+̇-comm ∅ ∅ = refl
|
||
+̇-comm (Γ₁ , π₁ ∙ A) (Γ₂ , π₂ ∙ .A) =
|
||
begin
|
||
Γ₁ +̇ Γ₂ , π₁ + π₂ ∙ A
|
||
≡⟨ +-comm π₁ π₂ |> cong (Γ₁ +̇ Γ₂ ,_∙ A) ⟩
|
||
Γ₁ +̇ Γ₂ , π₂ + π₁ ∙ A
|
||
≡⟨ +̇-comm Γ₁ Γ₂ |> cong (_, π₂ + π₁ ∙ A) ⟩
|
||
Γ₂ +̇ Γ₁ , π₂ + π₁ ∙ A
|
||
∎
|
||
\end{code}
|
||
|
||
Vector addition is associative.
|
||
|
||
\begin{code}
|
||
+̇-assoc : ∀ {γ} (Γ₁ Γ₂ Γ₃ : Context γ)
|
||
|
||
-------------------------------------
|
||
→ (Γ₁ +̇ Γ₂) +̇ Γ₃ ≡ Γ₁ +̇ (Γ₂ +̇ Γ₃)
|
||
|
||
+̇-assoc ∅ ∅ ∅ = refl
|
||
+̇-assoc (Γ₁ , π₁ ∙ A) (Γ₂ , π₂ ∙ .A) (Γ₃ , π₃ ∙ .A) =
|
||
begin
|
||
(Γ₁ +̇ Γ₂) +̇ Γ₃ , (π₁ + π₂) + π₃ ∙ A
|
||
≡⟨ +-assoc π₁ π₂ π₃ |> cong ((Γ₁ +̇ Γ₂) +̇ Γ₃ ,_∙ A) ⟩
|
||
(Γ₁ +̇ Γ₂) +̇ Γ₃ , π₁ + (π₂ + π₃) ∙ A
|
||
≡⟨ +̇-assoc Γ₁ Γ₂ Γ₃ |> cong (_, π₁ + (π₂ + π₃) ∙ A) ⟩
|
||
Γ₁ +̇ (Γ₂ +̇ Γ₃) , π₁ + (π₂ + π₃) ∙ A
|
||
∎
|
||
\end{code}
|
||
|
||
Scaling by a sum gives the sum of the scalings.
|
||
|
||
\begin{code}
|
||
*̇-distribʳ-+̇ : ∀ {γ} (Γ : Context γ) (π₁ π₂ : Mult)
|
||
|
||
-----------------------------------
|
||
→ (π₁ + π₂) *̇ Γ ≡ π₁ *̇ Γ +̇ π₂ *̇ Γ
|
||
|
||
*̇-distribʳ-+̇ ∅ π₁ π₂ = refl
|
||
*̇-distribʳ-+̇ (Γ , π ∙ A) π₁ π₂ =
|
||
begin
|
||
(π₁ + π₂) *̇ Γ , (π₁ + π₂) * π ∙ A
|
||
≡⟨ distribʳ π π₁ π₂ |> cong ((π₁ + π₂) *̇ Γ ,_∙ A) ⟩
|
||
(π₁ + π₂) *̇ Γ , (π₁ * π) + (π₂ * π) ∙ A
|
||
≡⟨ *̇-distribʳ-+̇ Γ π₁ π₂ |> cong (_, (π₁ * π) + (π₂ * π) ∙ A) ⟩
|
||
π₁ *̇ Γ +̇ π₂ *̇ Γ , (π₁ * π) + (π₂ * π) ∙ A
|
||
∎
|
||
\end{code}
|
||
|
||
Scaling a sum gives the sum of the scalings.
|
||
|
||
\begin{code}
|
||
*̇-distribˡ-+̇ : ∀ {γ} (Γ₁ Γ₂ : Context γ) (π : Mult)
|
||
|
||
--------------------------------------
|
||
→ π *̇ (Γ₁ +̇ Γ₂) ≡ π *̇ Γ₁ +̇ π *̇ Γ₂
|
||
|
||
*̇-distribˡ-+̇ ∅ ∅ π = refl
|
||
*̇-distribˡ-+̇ (Γ₁ , π₁ ∙ A) (Γ₂ , π₂ ∙ .A) π =
|
||
begin
|
||
π *̇ (Γ₁ +̇ Γ₂) , π * (π₁ + π₂) ∙ A
|
||
≡⟨ distribˡ π π₁ π₂ |> cong (π *̇ (Γ₁ +̇ Γ₂) ,_∙ A) ⟩
|
||
π *̇ (Γ₁ +̇ Γ₂) , (π * π₁) + (π * π₂) ∙ A
|
||
≡⟨ *̇-distribˡ-+̇ Γ₁ Γ₂ π |> cong (_, (π * π₁) + (π * π₂) ∙ A) ⟩
|
||
π *̇ Γ₁ +̇ π *̇ Γ₂ , (π * π₁) + (π * π₂) ∙ A
|
||
∎
|
||
\end{code}
|
||
|
||
|
||
|
||
# Vector-matrix multiplication
|
||
|
||
Vector-matrix multiplication.
|
||
|
||
\begin{code}
|
||
_*⟩_ : ∀ {γ δ} → Context γ → Matrix γ δ → Context δ
|
||
∅ *⟩ Ξ = 0s
|
||
(Γ , π ∙ A) *⟩ Ξ = (π *̇ Ξ Z) +̇ Γ *⟩ (Ξ ∘ S_)
|
||
\end{code}
|
||
|
||
Linear maps preserve the 0-vector.
|
||
|
||
\begin{code}
|
||
*⟩-zeroˡ : ∀ {γ δ} (Ξ : Matrix γ δ)
|
||
|
||
--------------
|
||
→ 0s *⟩ Ξ ≡ 0s
|
||
|
||
*⟩-zeroˡ {∅} {δ} Ξ = refl
|
||
*⟩-zeroˡ {γ , A} {δ} Ξ =
|
||
begin
|
||
0s *⟩ Ξ
|
||
≡⟨⟩
|
||
0# *̇ Ξ Z +̇ 0s *⟩ (Ξ ∘ S_)
|
||
≡⟨ *⟩-zeroˡ (Ξ ∘ S_) |> cong (0# *̇ Ξ Z +̇_) ⟩
|
||
0# *̇ Ξ Z +̇ 0s
|
||
≡⟨ *̇-zeroˡ (Ξ Z) |> cong (_+̇ 0s) ⟩
|
||
0s +̇ 0s
|
||
≡⟨ +̇-identityʳ 0s ⟩
|
||
0s
|
||
∎
|
||
\end{code}
|
||
|
||
Adding a row of 0s to the end of the matrix and then multiplying by a vector produces a vector with a 0 at the bottom.
|
||
|
||
\begin{code}
|
||
*⟩-zeroʳ : ∀ {γ δ} (Γ : Context γ) (Ξ : Matrix γ δ) {B}
|
||
|
||
---------------------------------------------
|
||
→ Γ *⟩ (λ x → Ξ x , 0# ∙ B) ≡ Γ *⟩ Ξ , 0# ∙ B
|
||
|
||
*⟩-zeroʳ {γ} {δ} ∅ Ξ {B} = refl
|
||
*⟩-zeroʳ {γ} {δ} (Γ , π ∙ C) Ξ {B} =
|
||
begin
|
||
(π *̇ Ξ Z , π * 0# ∙ B) +̇ (Γ *⟩ (λ x → Ξ (S x) , 0# ∙ B))
|
||
≡⟨ *⟩-zeroʳ Γ (Ξ ∘ S_) |> cong ((π *̇ Ξ Z , π * 0# ∙ B) +̇_) ⟩
|
||
(π *̇ Ξ Z , π * 0# ∙ B) +̇ (Γ *⟩ (λ x → Ξ (S x)) , 0# ∙ B)
|
||
≡⟨⟩
|
||
(π *̇ Ξ Z , π * 0# ∙ B) +̇ (Γ *⟩ (Ξ ∘ S_) , 0# ∙ B)
|
||
≡⟨⟩
|
||
(π *̇ Ξ Z +̇ Γ *⟩ (Ξ ∘ S_)) , (π * 0#) + 0# ∙ B
|
||
≡⟨ +-identityʳ (π * 0#) |> cong ((π *̇ Ξ Z +̇ Γ *⟩ (Ξ ∘ S_)) ,_∙ B) ⟩
|
||
(π *̇ Ξ Z +̇ Γ *⟩ (Ξ ∘ S_)) , π * 0# ∙ B
|
||
≡⟨ zeroʳ π |> cong ((π *̇ Ξ Z +̇ Γ *⟩ (Ξ ∘ S_)) ,_∙ B) ⟩
|
||
(π *̇ Ξ Z +̇ Γ *⟩ (Ξ ∘ S_)) , 0# ∙ B
|
||
∎
|
||
\end{code}
|
||
|
||
Linear maps preserve scaling.
|
||
|
||
\begin{code}
|
||
*⟩-assoc : ∀ {γ δ} (Γ : Context γ) (Ξ : Matrix γ δ) (π : Mult)
|
||
|
||
-----------------------------------
|
||
→ (π *̇ Γ) *⟩ Ξ ≡ π *̇ (Γ *⟩ Ξ)
|
||
|
||
*⟩-assoc {γ} {δ} ∅ Ξ π =
|
||
begin
|
||
0s
|
||
≡⟨ *̇-zeroʳ π ⟩
|
||
π *̇ 0s
|
||
∎
|
||
|
||
*⟩-assoc {γ} {δ} (Γ , π′ ∙ A) Ξ π =
|
||
begin
|
||
((π * π′) *̇ Ξ Z) +̇ ((π *̇ Γ) *⟩ (Ξ ∘ S_))
|
||
≡⟨ *⟩-assoc Γ (Ξ ∘ S_) π |> cong ((π * π′) *̇ Ξ Z +̇_) ⟩
|
||
((π * π′) *̇ Ξ Z) +̇ (π *̇ (Γ *⟩ (Ξ ∘ S_)))
|
||
≡⟨ *̇-assoc (Ξ Z) |> cong (_+̇ (π *̇ (Γ *⟩ (Ξ ∘ S_)))) ⟩
|
||
(π *̇ (π′ *̇ Ξ Z)) +̇ (π *̇ (Γ *⟩ (Ξ ∘ S_)))
|
||
≡⟨ *̇-distribˡ-+̇ (π′ *̇ Ξ Z) (Γ *⟩ (Ξ ∘ S_)) π |> sym ⟩
|
||
π *̇ (π′ *̇ Ξ Z +̇ Γ *⟩ (Ξ ∘ S_))
|
||
∎
|
||
\end{code}
|
||
|
||
Linear maps distribute over sums.
|
||
|
||
\begin{code}
|
||
*⟩-distribʳ-+̇ : ∀ {γ} {δ} (Γ₁ Γ₂ : Context γ) (Ξ : Matrix γ δ)
|
||
|
||
----------------------------------
|
||
→ (Γ₁ +̇ Γ₂) *⟩ Ξ ≡ Γ₁ *⟩ Ξ +̇ Γ₂ *⟩ Ξ
|
||
|
||
*⟩-distribʳ-+̇ ∅ ∅ Ξ =
|
||
begin
|
||
0s
|
||
≡⟨ sym (+̇-identityʳ 0s) ⟩
|
||
0s +̇ 0s
|
||
∎
|
||
|
||
*⟩-distribʳ-+̇ (Γ₁ , π₁ ∙ A) (Γ₂ , π₂ ∙ .A) Ξ =
|
||
begin
|
||
(π₁ + π₂) *̇ Ξ Z +̇ (Γ₁ +̇ Γ₂) *⟩ (Ξ ∘ S_)
|
||
≡⟨ *⟩-distribʳ-+̇ Γ₁ Γ₂ (Ξ ∘ S_) |> cong ((π₁ + π₂) *̇ Ξ Z +̇_) ⟩
|
||
(π₁ + π₂) *̇ Ξ Z +̇ (Γ₁ *⟩ (Ξ ∘ S_) +̇ Γ₂ *⟩ (Ξ ∘ S_))
|
||
≡⟨ *̇-distribʳ-+̇ (Ξ Z) π₁ π₂ |> cong (_+̇ (Γ₁ *⟩ (Ξ ∘ S_) +̇ Γ₂ *⟩ (Ξ ∘ S_))) ⟩
|
||
(π₁ *̇ Ξ Z +̇ π₂ *̇ Ξ Z) +̇ (Γ₁ *⟩ (Ξ ∘ S_) +̇ Γ₂ *⟩ (Ξ ∘ S_))
|
||
≡⟨ +̇-assoc (π₁ *̇ Ξ Z +̇ π₂ *̇ Ξ Z) (Γ₁ *⟩ (Ξ ∘ S_)) (Γ₂ *⟩ (Ξ ∘ S_)) |> sym ⟩
|
||
((π₁ *̇ Ξ Z +̇ π₂ *̇ Ξ Z) +̇ Γ₁ *⟩ (Ξ ∘ S_)) +̇ Γ₂ *⟩ (Ξ ∘ S_)
|
||
≡⟨ +̇-assoc (π₁ *̇ Ξ Z) (π₂ *̇ Ξ Z) (Γ₁ *⟩ (Ξ ∘ S_)) |> cong (_+̇ Γ₂ *⟩ (Ξ ∘ S_)) ⟩
|
||
(π₁ *̇ Ξ Z +̇ (π₂ *̇ Ξ Z +̇ Γ₁ *⟩ (Ξ ∘ S_))) +̇ Γ₂ *⟩ (Ξ ∘ S_)
|
||
≡⟨ +̇-comm (π₂ *̇ Ξ Z) (Γ₁ *⟩ (Ξ ∘ S_)) |> cong ((_+̇ Γ₂ *⟩ (Ξ ∘ S_)) ∘ (π₁ *̇ Ξ Z +̇_)) ⟩
|
||
(π₁ *̇ Ξ Z +̇ (Γ₁ *⟩ (Ξ ∘ S_) +̇ π₂ *̇ Ξ Z)) +̇ Γ₂ *⟩ (Ξ ∘ S_)
|
||
≡⟨ +̇-assoc (π₁ *̇ Ξ Z) (Γ₁ *⟩ (Ξ ∘ S_)) (π₂ *̇ Ξ Z) |> sym ∘ cong (_+̇ Γ₂ *⟩ (Ξ ∘ S_)) ⟩
|
||
((π₁ *̇ Ξ Z +̇ Γ₁ *⟩ (Ξ ∘ S_)) +̇ π₂ *̇ Ξ Z) +̇ Γ₂ *⟩ (Ξ ∘ S_)
|
||
≡⟨ +̇-assoc (π₁ *̇ Ξ Z +̇ Γ₁ *⟩ (Ξ ∘ S_)) (π₂ *̇ Ξ Z) (Γ₂ *⟩ (Ξ ∘ S_)) ⟩
|
||
(π₁ *̇ Ξ Z +̇ Γ₁ *⟩ (Ξ ∘ S_)) +̇ (π₂ *̇ Ξ Z +̇ Γ₂ *⟩ (Ξ ∘ S_))
|
||
∎
|
||
\end{code}
|
||
|
||
Multiplying by a standard basis vector projects out the corresponding column of the matrix.
|
||
|
||
\begin{code}
|
||
*⟩-identityˡ : ∀ {γ δ} {A} (Ξ : Matrix γ δ)
|
||
|
||
→ (x : γ ∋ A)
|
||
-----------------------
|
||
→ identity x *⟩ Ξ ≡ Ξ x
|
||
|
||
*⟩-identityˡ {γ , A} {δ} {A} Ξ Z =
|
||
begin
|
||
identity Z *⟩ Ξ
|
||
≡⟨⟩
|
||
1# *̇ Ξ Z +̇ 0s *⟩ (Ξ ∘ S_)
|
||
≡⟨ *⟩-zeroˡ (Ξ ∘ S_) |> cong ((1# *̇ Ξ Z) +̇_) ⟩
|
||
1# *̇ Ξ Z +̇ 0s
|
||
≡⟨ +̇-identityʳ (1# *̇ Ξ Z) ⟩
|
||
1# *̇ Ξ Z
|
||
≡⟨ *̇-identityˡ (Ξ Z) ⟩
|
||
Ξ Z
|
||
∎
|
||
|
||
*⟩-identityˡ {γ , B} {δ} {A} Ξ (S x) =
|
||
begin
|
||
identity (S x) *⟩ Ξ
|
||
≡⟨⟩
|
||
0# *̇ Ξ Z +̇ identity x *⟩ (Ξ ∘ S_)
|
||
≡⟨ *⟩-identityˡ (Ξ ∘ S_) x |> cong (0# *̇ Ξ Z +̇_) ⟩
|
||
0# *̇ Ξ Z +̇ Ξ (S x)
|
||
≡⟨ *̇-zeroˡ (Ξ Z) |> cong (_+̇ Ξ (S x)) ⟩
|
||
0s +̇ Ξ (S x)
|
||
≡⟨ +̇-identityˡ (Ξ (S x)) ⟩
|
||
Ξ (S x)
|
||
∎
|
||
\end{code}
|
||
|
||
The standard basis vectors put together give the identity matrix.
|
||
|
||
\begin{code}
|
||
*⟩-identityʳ : ∀ {γ} (Γ : Context γ)
|
||
|
||
-------------------
|
||
→ Γ *⟩ identity ≡ Γ
|
||
|
||
*⟩-identityʳ {γ} ∅ = refl
|
||
*⟩-identityʳ {γ , .A} (Γ , π ∙ A) =
|
||
begin
|
||
(π *̇ 0s , π * 1# ∙ A) +̇ (Γ *⟩ (λ x → identity x , 0# ∙ A))
|
||
≡⟨ *⟩-zeroʳ Γ identity |> cong ((π *̇ 0s , π * 1# ∙ A) +̇_) ⟩
|
||
(π *̇ 0s , π * 1# ∙ A) +̇ (Γ *⟩ identity , 0# ∙ A)
|
||
≡⟨ *⟩-identityʳ Γ |> cong (((π *̇ 0s , π * 1# ∙ A) +̇_) ∘ (_, 0# ∙ A)) ⟩
|
||
(π *̇ 0s , π * 1# ∙ A) +̇ (Γ , 0# ∙ A)
|
||
≡⟨⟩
|
||
π *̇ 0s +̇ Γ , (π * 1#) + 0# ∙ A
|
||
≡⟨ +-identityʳ (π * 1#) |> cong ((π *̇ 0s +̇ Γ) ,_∙ A) ⟩
|
||
π *̇ 0s +̇ Γ , π * 1# ∙ A
|
||
≡⟨ *-identityʳ π |> cong ((π *̇ 0s +̇ Γ) ,_∙ A) ⟩
|
||
π *̇ 0s +̇ Γ , π ∙ A
|
||
≡⟨ *̇-zeroʳ π |> cong ((_, π ∙ A) ∘ (_+̇ Γ)) ∘ sym ⟩
|
||
0s +̇ Γ , π ∙ A
|
||
≡⟨ +̇-identityˡ Γ |> cong (_, π ∙ A) ⟩
|
||
Γ , π ∙ A
|
||
∎
|
||
\end{code}
|
||
|
||
|
||
# Renaming
|
||
|
||
\begin{code}
|
||
ext : ∀ {γ δ}
|
||
|
||
→ (∀ {A} → γ ∋ A → δ ∋ A)
|
||
---------------------------------
|
||
→ (∀ {A B} → γ , B ∋ A → δ , B ∋ A)
|
||
|
||
ext ρ Z = Z
|
||
ext ρ (S x) = S (ρ x)
|
||
\end{code}
|
||
|
||
\begin{code}
|
||
lem-` : ∀ {γ δ} {A} {Ξ : Matrix γ δ} (x : γ ∋ A) → _
|
||
lem-` {γ} {δ} {A} {Ξ} x =
|
||
begin
|
||
Ξ x
|
||
≡⟨ *⟩-identityˡ Ξ x |> sym ⟩
|
||
identity x *⟩ Ξ
|
||
∎
|
||
\end{code}
|
||
|
||
\begin{code}
|
||
lem-ƛ : ∀ {γ δ} (Γ : Context γ) {A} {π} {Ξ : Matrix γ δ} → _
|
||
lem-ƛ {γ} {δ} Γ {A} {π} {Ξ} =
|
||
begin
|
||
(π *̇ 0s , π * 1# ∙ A) +̇ (Γ *⟩ (λ x → Ξ x , 0# ∙ A))
|
||
≡⟨ *⟩-zeroʳ Γ Ξ |> cong ((π *̇ 0s , π * 1# ∙ A) +̇_) ⟩
|
||
(π *̇ 0s , π * 1# ∙ A) +̇ (Γ *⟩ Ξ , 0# ∙ A)
|
||
≡⟨⟩
|
||
π *̇ 0s +̇ Γ *⟩ Ξ , (π * 1#) + 0# ∙ A
|
||
≡⟨ *̇-zeroʳ π |> cong ((_, (π * 1#) + 0# ∙ A) ∘ (_+̇ Γ *⟩ Ξ)) ∘ sym ⟩
|
||
0s +̇ Γ *⟩ Ξ , (π * 1#) + 0# ∙ A
|
||
≡⟨ +̇-identityˡ (Γ *⟩ Ξ) |> cong (_, (π * 1#) + 0# ∙ A) ⟩
|
||
Γ *⟩ Ξ , (π * 1#) + 0# ∙ A
|
||
≡⟨ +-identityʳ (π * 1#) |> cong (Γ *⟩ Ξ ,_∙ A) ⟩
|
||
Γ *⟩ Ξ , π * 1# ∙ A
|
||
≡⟨ *-identityʳ π |> cong (Γ *⟩ Ξ ,_∙ A) ⟩
|
||
Γ *⟩ Ξ , π ∙ A
|
||
∎
|
||
\end{code}
|
||
|
||
\begin{code}
|
||
lem-· : ∀ {γ δ} (Γ Δ : Context γ) {π} {Ξ : Matrix γ δ} → _
|
||
lem-· {γ} {δ} Γ Δ {π} {Ξ} =
|
||
begin
|
||
Γ *⟩ Ξ +̇ π *̇ (Δ *⟩ Ξ)
|
||
≡⟨ *⟩-assoc Δ Ξ π |> cong (Γ *⟩ Ξ +̇_) ∘ sym ⟩
|
||
Γ *⟩ Ξ +̇ (π *̇ Δ) *⟩ Ξ
|
||
≡⟨ *⟩-distribʳ-+̇ Γ (π *̇ Δ) Ξ |> sym ⟩
|
||
(Γ +̇ π *̇ Δ) *⟩ Ξ ∎
|
||
\end{code}
|
||
|
||
\begin{code}
|
||
lem-, : ∀ {γ δ} (Γ Δ : Context γ) {Ξ : Matrix γ δ} → _
|
||
lem-, {γ} {δ} Γ Δ {Ξ} =
|
||
begin
|
||
Γ *⟩ Ξ +̇ Δ *⟩ Ξ
|
||
≡⟨ *⟩-distribʳ-+̇ Γ Δ Ξ |> sym ⟩
|
||
(Γ +̇ Δ) *⟩ Ξ
|
||
∎
|
||
\end{code}
|
||
|
||
\begin{code}
|
||
lem-case⊗ : ∀ {γ δ} (Γ : Context γ) {A B} {Ξ : Matrix γ δ} → _
|
||
lem-case⊗ {γ} {δ} Γ {A} {B} {Ξ} =
|
||
let
|
||
lem1 : ∀ {γ} (Γ : Context γ) → _
|
||
lem1 {γ} Γ =
|
||
begin
|
||
(1# *̇ 0s) +̇ Γ
|
||
≡⟨ *̇-identityˡ 0s |> cong (_+̇ Γ) ⟩
|
||
0s +̇ Γ
|
||
≡⟨ +̇-identityˡ Γ ⟩
|
||
Γ
|
||
∎
|
||
in
|
||
begin
|
||
|
||
(1# *̇ 0s , 1# * 0# ∙ A , 1# * 1# ∙ B) +̇ ((1# *̇ 0s , 1# * 1# ∙ A , 1# * 0# ∙ B) +̇ Γ *⟩ (λ x → Ξ x , 0# ∙ A , 0# ∙ B))
|
||
|
||
-- Step 1. Move the three occurrences of A and B to the top-level.
|
||
≡⟨ trans (*⟩-zeroʳ Γ (λ x → Ξ x , 0# ∙ A)) (*⟩-zeroʳ Γ Ξ |> cong (_, 0# ∙ B))
|
||
|> cong (((1# *̇ 0s , 1# * 0# ∙ A , 1# * 1# ∙ B) +̇_) ∘ ((1# *̇ 0s , 1# * 1# ∙ A , 1# * 0# ∙ B) +̇_)) ⟩
|
||
|
||
(1# *̇ 0s) +̇ ((1# *̇ 0s) +̇ (Γ *⟩ Ξ)) , (1# * 0#) + ((1# * 1#) + 0#) ∙ A , (1# * 1#) + ((1# * 0#) + 0#) ∙ B
|
||
|
||
-- Step 2. Remove the empty environments (1# *̇ 0s).
|
||
≡⟨ trans (lem1 (Γ *⟩ Ξ) |> cong (1# *̇ 0s +̇_)) (lem1 (Γ *⟩ Ξ))
|
||
|> cong ((_, (1# * 1#) + ((1# * 0#) + 0#) ∙ B) ∘ (_, (1# * 0#) + ((1# * 1#) + 0#) ∙ A)) ⟩
|
||
|
||
Γ *⟩ Ξ , (1# * 0#) + ((1# * 1#) + 0#) ∙ A , (1# * 1#) + ((1# * 0#) + 0#) ∙ B
|
||
|
||
-- Step 3. Reduce the complex sum for the usage of B to 1#.
|
||
≡⟨ trans (trans (+-identityʳ (1# * 0#)) (*-identityˡ 0#) |> cong ((1# * 1#) +_)) (trans (+-identityʳ (1# * 1#)) (*-identityˡ 1#))
|
||
|> cong (Γ *⟩ Ξ , (1# * 0#) + ((1# * 1#) + 0#) ∙ A ,_∙ B) ⟩
|
||
|
||
Γ *⟩ Ξ , (1# * 0#) + ((1# * 1#) + 0#) ∙ A , 1# ∙ B
|
||
|
||
-- Step 4. Reduce the complex sum for the usage of A to 1#.
|
||
≡⟨ trans (*-identityˡ 0# |> cong (_+ ((1# * 1#) + 0#))) (trans (+-identityˡ ((1# * 1#) + 0#)) (trans (+-identityʳ (1# * 1#)) (*-identityʳ 1#)))
|
||
|> cong ((_, 1# ∙ B) ∘ (Γ *⟩ Ξ ,_∙ A)) ⟩
|
||
|
||
Γ *⟩ Ξ , 1# ∙ A , 1# ∙ B
|
||
|
||
∎
|
||
\end{code}
|
||
|
||
\begin{code}
|
||
lem-⟨⟩ : ∀ {γ δ} {Ξ : Matrix δ γ} → _
|
||
lem-⟨⟩ {γ} {δ} {Ξ} =
|
||
begin
|
||
0s {γ}
|
||
≡⟨ *⟩-zeroˡ Ξ |> sym ⟩
|
||
0s {δ} *⟩ Ξ
|
||
∎
|
||
\end{code}
|
||
|
||
\begin{code}
|
||
lem-case⊕ : ∀ {γ δ} (Γ : Context γ) {A : Type} {Ξ : Matrix γ δ} → _
|
||
lem-case⊕ {γ} {δ} Γ {A} {Ξ} =
|
||
begin
|
||
(1# *̇ 0s , 1# * 1# ∙ A) +̇ Γ *⟩ (λ x → Ξ x , 0# ∙ A)
|
||
≡⟨ *̇-identityˡ 0s |> cong ((_+̇ Γ *⟩ (λ x → Ξ x , 0# ∙ A)) ∘ (_, 1# * 1# ∙ A)) ⟩
|
||
(0s , 1# * 1# ∙ A) +̇ Γ *⟩ (λ x → Ξ x , 0# ∙ A)
|
||
≡⟨ *-identityˡ 1# |> cong ((_+̇ Γ *⟩ (λ x → Ξ x , 0# ∙ A)) ∘ (0s ,_∙ A)) ⟩
|
||
(0s , 1# ∙ A) +̇ Γ *⟩ (λ x → Ξ x , 0# ∙ A)
|
||
≡⟨ *⟩-zeroʳ Γ Ξ |> cong (( 0s , 1# ∙ A) +̇_) ⟩
|
||
(0s , 1# ∙ A) +̇ (Γ *⟩ Ξ , 0# ∙ A)
|
||
≡⟨⟩
|
||
(0s +̇ Γ *⟩ Ξ) , 1# + 0# ∙ A
|
||
≡⟨ +̇-identityˡ (Γ *⟩ Ξ) |> cong (_, 1# + 0# ∙ A) ⟩
|
||
Γ *⟩ Ξ , 1# + 0# ∙ A
|
||
≡⟨ +-identityʳ 1# |> cong (Γ *⟩ Ξ ,_∙ A) ⟩
|
||
Γ *⟩ Ξ , 1# ∙ A
|
||
∎
|
||
\end{code}
|
||
|
||
\begin{code}
|
||
rename : ∀ {γ δ} {Γ : Context γ} {B}
|
||
|
||
→ (ρ : ∀ {A} → γ ∋ A → δ ∋ A)
|
||
→ Γ ⊢ B
|
||
---------------------------
|
||
→ Γ *⟩ (identity ∘ ρ) ⊢ B
|
||
|
||
rename ρ (` x) =
|
||
Eq.subst (_⊢ _) (lem-` x) (` ρ x)
|
||
rename ρ (ƛ_ {Γ = Γ} N) =
|
||
ƛ (Eq.subst (_⊢ _) (lem-ƛ Γ) (rename (ext ρ) N))
|
||
rename ρ (_·_ {Γ = Γ} {Δ = Δ} L M) =
|
||
Eq.subst (_⊢ _) (lem-· Γ Δ) (rename ρ L · rename ρ M)
|
||
rename ρ ⟨⟩ =
|
||
Eq.subst (_⊢ _) (lem-⟨⟩ {Ξ = identity ∘ ρ}) ⟨⟩
|
||
rename ρ (case1 {Γ = Γ} {Δ = Δ} L N) =
|
||
Eq.subst (_⊢ _) (lem-, Γ Δ) (case1 (rename ρ L) (rename ρ N))
|
||
rename ρ (⟨_,_⟩ {Γ = Γ} {Δ = Δ} L M) =
|
||
Eq.subst (_⊢ _) (lem-, Γ Δ) ⟨ rename ρ L , rename ρ M ⟩
|
||
rename ρ (case⊗ {Γ = Γ} {Δ = Δ} L N) =
|
||
Eq.subst (_⊢ _) (lem-, Γ Δ) (case⊗ (rename ρ L) (Eq.subst (_⊢ _) (lem-case⊗ Δ) (rename (ext (ext ρ)) N)))
|
||
rename ρ (inj₁ {Γ = Γ} L) =
|
||
inj₁ (rename ρ L)
|
||
rename ρ (inj₂ {Γ = Γ} L) =
|
||
inj₂ (rename ρ L)
|
||
rename ρ (case⊕ {Γ = Γ} {Δ = Δ} L M N) =
|
||
Eq.subst (_⊢ _) (lem-, Γ Δ) (case⊕ (rename ρ L) (Eq.subst (_⊢ _) (lem-case⊕ Δ) (rename (ext ρ) M)) (Eq.subst (_⊢ _) (lem-case⊕ Δ) (rename (ext ρ) N)))
|
||
\end{code}
|
||
|
||
|
||
# Simultaneous Substitution
|
||
|
||
Extend a matrix as the identity matrix -- add a zero to the end of every row, and add a new row with a 1 and the rest 0s.
|
||
|
||
\begin{code}
|
||
extm : ∀ {γ δ}
|
||
|
||
→ Matrix γ δ
|
||
--------------------------------
|
||
→ (∀ {B} → Matrix (γ , B) (δ , B))
|
||
|
||
extm Ξ {B} {A} Z = identity Z
|
||
extm Ξ {B} {A} (S x) = Ξ x , 0# ∙ B
|
||
\end{code}
|
||
|
||
\begin{code}
|
||
exts : ∀ {γ δ} {Ξ : Matrix γ δ}
|
||
|
||
→ (∀ {A} → (x : γ ∋ A) → Ξ x ⊢ A)
|
||
------------------------------------------
|
||
→ (∀ {A B} → (x : γ , B ∋ A) → extm Ξ x ⊢ A)
|
||
|
||
exts {Ξ = Ξ} σ {A} {B} Z = ` Z
|
||
exts {Ξ = Ξ} σ {A} {B} (S x) = Eq.subst (_⊢ A) lem (rename S_ (σ x))
|
||
where
|
||
lem =
|
||
begin
|
||
Ξ x *⟩ (identity ∘ S_)
|
||
≡⟨⟩
|
||
Ξ x *⟩ (λ x → identity x , 0# ∙ B)
|
||
≡⟨ *⟩-zeroʳ (Ξ x) identity ⟩
|
||
(Ξ x *⟩ identity) , 0# ∙ B
|
||
≡⟨ *⟩-identityʳ (Ξ x) |> cong (_, 0# ∙ B) ⟩
|
||
Ξ x , 0# ∙ B
|
||
∎
|
||
\end{code}
|
||
|
||
\begin{code}
|
||
subst : ∀ {γ δ} {Γ : Context γ} {Ξ : Matrix γ δ} {B}
|
||
|
||
→ (σ : ∀ {A} → (x : γ ∋ A) → Ξ x ⊢ A)
|
||
→ Γ ⊢ B
|
||
--------------------------------------
|
||
→ Γ *⟩ Ξ ⊢ B
|
||
|
||
subst {Ξ = Ξ} σ (` x) =
|
||
Eq.subst (_⊢ _) (lem-` x) (σ x)
|
||
subst {Ξ = Ξ} σ (ƛ_ {Γ = Γ} N) =
|
||
ƛ (Eq.subst (_⊢ _) (lem-ƛ Γ) (subst (exts σ) N))
|
||
subst {Ξ = Ξ} σ (_·_ {Γ = Γ} {Δ = Δ} L M) =
|
||
Eq.subst (_⊢ _) (lem-· Γ Δ)(subst σ L · subst σ M)
|
||
subst {Ξ = Ξ} σ ⟨⟩ =
|
||
Eq.subst (_⊢ _) (lem-⟨⟩ {Ξ = Ξ}) ⟨⟩
|
||
subst {Ξ = Ξ} σ (case1 {Γ = Γ} {Δ = Δ} L N) =
|
||
Eq.subst (_⊢ _) (lem-, Γ Δ) (case1 (subst σ L) (subst σ N))
|
||
subst {Ξ = Ξ} σ (⟨_,_⟩ {Γ = Γ} {Δ = Δ} L M) =
|
||
Eq.subst (_⊢ _) (lem-, Γ Δ) ⟨ subst σ L , subst σ M ⟩
|
||
subst {Ξ = Ξ} σ (case⊗ {Γ = Γ} {Δ = Δ} L N) =
|
||
Eq.subst (_⊢ _) (lem-, Γ Δ) (case⊗ (subst σ L) (Eq.subst (_⊢ _) (lem-case⊗ Δ) (subst (exts (exts σ)) N)))
|
||
subst {Ξ = Ξ} σ (inj₁ {Γ = Γ} L) =
|
||
inj₁ (subst σ L)
|
||
subst {Ξ = Ξ} σ (inj₂ {Γ = Γ} L) =
|
||
inj₂ (subst σ L)
|
||
subst {Ξ = Ξ} σ (case⊕ {Γ = Γ} {Δ = Δ} L M N) =
|
||
Eq.subst (_⊢ _) (lem-, Γ Δ) (case⊕ (subst σ L) (Eq.subst (_⊢ _) (lem-case⊕ Δ) (subst (exts σ) M)) (Eq.subst (_⊢ _) (lem-case⊕ Δ) (subst (exts σ) N)))
|
||
\end{code}
|
||
|
||
|
||
# Values
|
||
|
||
\begin{code}
|
||
data Value : ∀ {γ} {Γ : Context γ} {A} → Γ ⊢ A → Set where
|
||
|
||
V-ƛ : ∀ {γ} {Γ : Context γ} {A B} {π} {N : Γ , π ∙ A ⊢ B}
|
||
|
||
-----------
|
||
→ Value (ƛ N)
|
||
|
||
V-⟨⟩ : ∀ {γ}
|
||
|
||
--------------
|
||
→ Value (⟨⟩ {γ})
|
||
|
||
V-, : ∀ {γ} {Γ Δ : Context γ} {A B} {L : Γ ⊢ A} {M : Δ ⊢ B}
|
||
|
||
→ Value L
|
||
→ Value M
|
||
---------------
|
||
→ Value ⟨ L , M ⟩
|
||
|
||
V-inj₁ : ∀ {γ} {Γ : Context γ} {A B} {L : Γ ⊢ A}
|
||
|
||
→ Value L
|
||
--------------
|
||
→ Value (inj₁ {B = B} L)
|
||
|
||
V-inj₂ : ∀ {γ} {Γ : Context γ} {A B} {L : Γ ⊢ B}
|
||
|
||
→ Value L
|
||
--------------
|
||
→ Value (inj₂ {A = A} L)
|
||
\end{code}
|
||
|
||
|
||
# Single Substitution
|
||
|
||
\begin{code}
|
||
_⊸[_] : ∀ {γ} {Γ Δ : Context γ} {A B} {π}
|
||
|
||
→ Γ , π ∙ B ⊢ A
|
||
→ Δ ⊢ B
|
||
--------------
|
||
→ Γ +̇ π *̇ Δ ⊢ A
|
||
|
||
_⊸[_] {γ} {Γ} {Δ} {A} {B} {π} N M = Eq.subst (_⊢ _) lem (subst σ′ N)
|
||
where
|
||
Ξ′ : Matrix (γ , B) γ
|
||
Ξ′ Z = Δ
|
||
Ξ′ (S x) = identity x
|
||
σ′ : ∀ {A} → (x : γ , B ∋ A) → Ξ′ x ⊢ A
|
||
σ′ Z = M
|
||
σ′ (S x) = ` x
|
||
|
||
lem =
|
||
begin
|
||
π *̇ Δ +̇ Γ *⟩ identity
|
||
≡⟨ +̇-comm (π *̇ Δ) (Γ *⟩ identity) ⟩
|
||
Γ *⟩ identity +̇ π *̇ Δ
|
||
≡⟨ *⟩-identityʳ Γ |> cong (_+̇ π *̇ Δ) ⟩
|
||
Γ +̇ π *̇ Δ
|
||
∎
|
||
\end{code}
|
||
|
||
\begin{code}
|
||
_1[_] : ∀ {γ} {Γ Δ : Context γ} {A} {V : Γ ⊢ `1}
|
||
|
||
→ Δ ⊢ A
|
||
→ Value V
|
||
---------
|
||
→ Γ +̇ Δ ⊢ A
|
||
|
||
_1[_] {Δ = Δ} N V-⟨⟩ = Eq.subst (_⊢ _) lem N
|
||
where
|
||
lem =
|
||
begin
|
||
Δ
|
||
≡⟨ +̇-identityˡ Δ |> sym ⟩
|
||
0s +̇ Δ
|
||
∎
|
||
\end{code}
|
||
|
||
\begin{code}
|
||
_⊗[_][_] : ∀ {γ} {Γ Δ Θ : Context γ} {A B C}
|
||
|
||
→ Θ , 1# ∙ A , 1# ∙ B ⊢ C
|
||
→ Γ ⊢ A
|
||
→ Δ ⊢ B
|
||
---------------
|
||
→ Γ +̇ Δ +̇ Θ ⊢ C
|
||
|
||
_⊗[_][_] {γ} {Γ} {Δ} {Θ} {A} {B} {C} N L M = Eq.subst (_⊢ _) lem (subst σ′ N)
|
||
where
|
||
Ξ′ : Matrix (γ , A , B) γ
|
||
Ξ′ Z = Δ
|
||
Ξ′ (S Z) = Γ
|
||
Ξ′ (S (S x)) = identity x
|
||
σ′ : ∀ {D} → (x : γ , A , B ∋ D) → Ξ′ x ⊢ D
|
||
σ′ Z = M
|
||
σ′ (S Z) = L
|
||
σ′ (S (S x)) = ` x
|
||
|
||
lem =
|
||
begin
|
||
1# *̇ Δ +̇ (1# *̇ Γ +̇ Θ *⟩ identity)
|
||
≡⟨ *⟩-identityʳ Θ |> cong ((1# *̇ Δ +̇_) ∘ (1# *̇ Γ +̇_)) ⟩
|
||
1# *̇ Δ +̇ (1# *̇ Γ +̇ Θ)
|
||
≡⟨ *̇-identityˡ Γ |> cong ((1# *̇ Δ +̇_) ∘ (_+̇ Θ)) ⟩
|
||
1# *̇ Δ +̇ (Γ +̇ Θ)
|
||
≡⟨ *̇-identityˡ Δ |> cong (_+̇ (Γ +̇ Θ)) ⟩
|
||
Δ +̇ (Γ +̇ Θ)
|
||
≡⟨ +̇-assoc Δ Γ Θ |> sym ⟩
|
||
(Δ +̇ Γ) +̇ Θ
|
||
≡⟨ +̇-comm Δ Γ |> cong (_+̇ Θ) ⟩
|
||
(Γ +̇ Δ) +̇ Θ
|
||
∎
|
||
\end{code}
|
||
|
||
\begin{code}
|
||
_⊕[_] : ∀ {γ} {Γ Δ : Context γ} {A B}
|
||
|
||
→ Δ , 1# ∙ B ⊢ A
|
||
→ Γ ⊢ B
|
||
--------------
|
||
→ Γ +̇ Δ ⊢ A
|
||
|
||
_⊕[_] {γ} {Γ} {Δ} {A} {B} N M = Eq.subst (_⊢ _) lem (N ⊸[ M ])
|
||
where
|
||
lem =
|
||
begin
|
||
Δ +̇ 1# *̇ Γ
|
||
≡⟨ *̇-identityˡ Γ |> cong (Δ +̇_) ⟩
|
||
Δ +̇ Γ
|
||
≡⟨ +̇-comm Δ Γ ⟩
|
||
Γ +̇ Δ
|
||
∎
|
||
\end{code}
|
||
|
||
|
||
# Reduction
|
||
|
||
\begin{code}
|
||
infix 2 _—→_
|
||
|
||
data _—→_ : ∀ {γ} {Γ : Context γ} {A} → (Γ ⊢ A) → (Γ ⊢ A) → Set where
|
||
|
||
ξ-·₁ : ∀ {γ} {Γ Δ : Context γ} {A B} {π} {L L′ : Γ ⊢ [ π ∙ A ]⊸ B} {M : Δ ⊢ A}
|
||
|
||
→ L —→ L′
|
||
-----------------
|
||
→ L · M —→ L′ · M
|
||
|
||
ξ-·₂ : ∀ {γ} {Γ Δ : Context γ} {A B} {π} {V : Γ ⊢ [ π ∙ A ]⊸ B} {M M′ : Δ ⊢ A}
|
||
|
||
→ Value V
|
||
→ M —→ M′
|
||
--------------
|
||
→ V · M —→ V · M′
|
||
|
||
ξ-case1 : ∀ {γ} {Γ Δ : Context γ} {A} {L L′ : Γ ⊢ `1} {M : Δ ⊢ A}
|
||
|
||
→ L —→ L′
|
||
-----------------------
|
||
→ case1 L M —→ case1 L′ M
|
||
|
||
ξ-,₁ : ∀ {γ} {Γ Δ : Context γ} {A B} {L L′ : Γ ⊢ A} {M : Δ ⊢ B}
|
||
|
||
→ L —→ L′
|
||
-----------------------
|
||
→ ⟨ L , M ⟩ —→ ⟨ L′ , M ⟩
|
||
|
||
ξ-,₂ : ∀ {γ} {Γ Δ : Context γ} {A B} {V : Γ ⊢ A} {M M′ : Δ ⊢ B}
|
||
|
||
→ Value V
|
||
→ M —→ M′
|
||
-----------------------
|
||
→ ⟨ V , M ⟩ —→ ⟨ V , M′ ⟩
|
||
|
||
ξ-case⊗ : ∀ {γ} {Γ Δ : Context γ} {A B C} {L L′ : Γ ⊢ A ⊗ B} {N : Δ , 1# ∙ A , 1# ∙ B ⊢ C}
|
||
|
||
→ L —→ L′
|
||
------------------------
|
||
→ case⊗ L N —→ case⊗ L′ N
|
||
|
||
ξ-inj₁ : ∀ {γ} {Γ : Context γ} {A B} {L L′ : Γ ⊢ A}
|
||
|
||
→ L —→ L′
|
||
---------------------------------
|
||
→ inj₁ {B = B} L —→ inj₁ {B = B} L′
|
||
|
||
ξ-inj₂ : ∀ {γ} {Γ : Context γ} {A B} {L L′ : Γ ⊢ B}
|
||
|
||
→ L —→ L′
|
||
---------------------------------
|
||
→ inj₂ {A = A} L —→ inj₂ {A = A} L′
|
||
|
||
ξ-case⊕ : ∀ {γ} {Γ Δ : Context γ} {A B C} {L L′ : Γ ⊢ A ⊕ B} {M : Δ , 1# ∙ A ⊢ C} {N : Δ , 1# ∙ B ⊢ C}
|
||
|
||
→ L —→ L′
|
||
---------------------------
|
||
→ case⊕ L M N —→ case⊕ L′ M N
|
||
|
||
β-⊸ : ∀ {γ} {Γ Δ : Context γ} {A B} {π} {N : Γ , π ∙ A ⊢ B} {W : Δ ⊢ A}
|
||
|
||
→ (VW : Value W)
|
||
--------------------
|
||
→ (ƛ N) · W —→ N ⊸[ W ]
|
||
|
||
β-1 : ∀ {γ} {Γ Δ : Context γ} {A} {V : Γ ⊢ `1} {N : Δ ⊢ A}
|
||
|
||
→ (VV : Value V)
|
||
----------------------
|
||
→ case1 V N —→ N 1[ VV ]
|
||
|
||
β-⊗ : ∀ {γ} {Γ Δ Θ : Context γ} {A B C} {V : Γ ⊢ A} {W : Δ ⊢ B} {N : Θ , 1# ∙ A , 1# ∙ B ⊢ C}
|
||
|
||
→ (VV : Value V)
|
||
→ (VW : Value W)
|
||
---------------------------------
|
||
→ case⊗ ⟨ V , W ⟩ N —→ N ⊗[ V ][ W ]
|
||
|
||
β-⊕₁ : ∀ {γ} {Γ Δ : Context γ} {A B C} {V : Γ ⊢ A} {M : Δ , 1# ∙ A ⊢ C} {N : Δ , 1# ∙ B ⊢ C}
|
||
|
||
→ (VV : Value V)
|
||
-----------------------------
|
||
→ case⊕ (inj₁ V) M N —→ M ⊕[ V ]
|
||
|
||
|
||
β-⊕₂ : ∀ {γ} {Γ Δ : Context γ} {A B C} {V : Γ ⊢ B} {M : Δ , 1# ∙ A ⊢ C} {N : Δ , 1# ∙ B ⊢ C}
|
||
|
||
→ (VV : Value V)
|
||
-----------------------------
|
||
→ case⊕ (inj₂ V) M N —→ N ⊕[ V ]
|
||
\end{code}
|
||
|
||
|
||
# Progress
|
||
|
||
\begin{code}
|
||
data Progress {γ} {Γ : Context γ} {A} (M : Γ ⊢ A) : Set where
|
||
|
||
step : {N : Γ ⊢ A}
|
||
|
||
→ M —→ N
|
||
----------
|
||
→ Progress M
|
||
|
||
done :
|
||
|
||
Value M
|
||
----------
|
||
→ Progress M
|
||
\end{code}
|
||
|
||
\begin{code}
|
||
progress : ∀ {A} → (M : ∅ ⊢ A) → Progress M
|
||
progress M = go refl M
|
||
where
|
||
go : ∀ {γ} {Γ : Context γ} {A} → γ ≡ ∅ → (M : Γ ⊢ A) → Progress M
|
||
go refl (` ())
|
||
go refl (ƛ N) = done V-ƛ
|
||
go refl (L · M) with go refl L
|
||
... | step L—→L′ = step (ξ-·₁ L—→L′)
|
||
... | done V-ƛ with go refl M
|
||
... | step M—→M′ = step (ξ-·₂ V-ƛ M—→M′)
|
||
... | done V-M = step (β-⊸ V-M)
|
||
go refl ⟨⟩ = done V-⟨⟩
|
||
go refl (case1 L N) with go refl L
|
||
... | step L—→L′ = step (ξ-case1 L—→L′)
|
||
... | done V-L = step (β-1 V-L)
|
||
go refl ⟨ L , M ⟩ with go refl L
|
||
... | step L—→L′ = step (ξ-,₁ L—→L′)
|
||
... | done V-L with go refl M
|
||
... | step M—→M′ = step (ξ-,₂ V-L M—→M′)
|
||
... | done V-M = done (V-, V-L V-M)
|
||
go refl (case⊗ L N) with go refl L
|
||
... | step L—→L′ = step (ξ-case⊗ L—→L′)
|
||
... | done (V-, V-L V-M) = step (β-⊗ V-L V-M)
|
||
go refl (inj₁ L) with go refl L
|
||
... | step L—→L′ = step (ξ-inj₁ L—→L′)
|
||
... | done V-L = done (V-inj₁ V-L)
|
||
go refl (inj₂ L) with go refl L
|
||
... | step L—→L′ = step (ξ-inj₂ L—→L′)
|
||
... | done V-L = done (V-inj₂ V-L)
|
||
go refl (case⊕ L M N) with go refl L
|
||
... | step L—→L′ = step (ξ-case⊕ L—→L′)
|
||
... | done (V-inj₁ V-L) = step (β-⊕₁ V-L)
|
||
... | done (V-inj₂ V-L) = step (β-⊕₂ V-L)
|
||
\end{code}
|