Advertisement
Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- {-# OPTIONS --without-K #-}
- {-
- Below is an example of proving *everything* about the substitution calculus of a
- simple TT with Bool.
- The more challenging solution:
- - If substitutions are defined as lists of terms, then if you manage to
- prove that substitutions form a category, almost certainly you're done,
- since you can only prove this is you have all relevant lemmas.
- The lazy solution:
- - Copy/paste everything from below, then add/remove cases as necessary,
- depending on the definition of the syntax.
- -}
- -- Equational reasoning
- --------------------------------------------------------------------------------
- open import Relation.Binary.PropositionalEquality
- open import Function
- _◾_ : ∀ {α}{A : Set α}{x y z : A} → x ≡ y → y ≡ z → x ≡ z
- refl ◾ refl = refl
- infixr 4 _◾_
- _⁻¹ : ∀{α}{A : Set α}{x y : A} → x ≡ y → y ≡ x
- refl ⁻¹ = refl
- infix 6 _⁻¹
- coe : ∀{α}{A B : Set α} → A ≡ B → A → B
- coe refl a = a
- _&_ :
- ∀{α β}{A : Set α}{B : Set β}(f : A → B){a₀ a₁ : A}(a₂ : a₀ ≡ a₁)
- → f a₀ ≡ f a₁
- f & refl = refl
- infixl 9 _&_
- _⊗_ :
- ∀ {α β}{A : Set α}{B : Set β}{f g : A → B}(p : f ≡ g){a a' : A}(q : a ≡ a')
- → f a ≡ g a'
- refl ⊗ refl = refl
- infixl 8 _⊗_
- -- Syntax
- --------------------------------------------------------------------------------
- infixr 4 _⇒_
- infixr 5 _,_
- data Ty : Set where
- Bool : Ty
- _⇒_ : Ty → Ty → Ty
- data Con : Set where
- ∙ : Con
- _,_ : Con → Ty → Con
- data _∈_ (A : Ty) : Con → Set where
- vz : ∀ {Γ} → A ∈ (Γ , A)
- vs : ∀ {B Γ} → A ∈ Γ → A ∈ (Γ , B)
- data Tm Γ : Ty → Set where
- var : ∀ {A} → A ∈ Γ → Tm Γ A
- lam : ∀ {A B} → Tm (Γ , A) B → Tm Γ (A ⇒ B)
- app : ∀ {A B} → Tm Γ (A ⇒ B) → Tm Γ A → Tm Γ B
- true : Tm Γ Bool
- false : Tm Γ Bool
- bcase : ∀ {A} → Tm Γ Bool → Tm Γ A → Tm Γ A → Tm Γ A
- -- Order-preserving embeddings
- --------------------------------------------------------------------------------
- data OPE : Con → Con → Set where
- ∙ : OPE ∙ ∙
- drop : ∀ {A Γ Δ} → OPE Γ Δ → OPE (Γ , A) Δ
- keep : ∀ {A Γ Δ} → OPE Γ Δ → OPE (Γ , A) (Δ , A)
- -- Category operations
- idₑ : ∀ {Γ} → OPE Γ Γ
- idₑ {∙} = ∙
- idₑ {Γ , A} = keep (idₑ {Γ})
- wk : ∀ {A Γ} → OPE (Γ , A) Γ
- wk = drop idₑ
- _∘ₑ_ : ∀ {Γ Δ Σ} → OPE Δ Σ → OPE Γ Δ → OPE Γ Σ
- σ ∘ₑ ∙ = σ
- σ ∘ₑ drop δ = drop (σ ∘ₑ δ)
- drop σ ∘ₑ keep δ = drop (σ ∘ₑ δ)
- keep σ ∘ₑ keep δ = keep (σ ∘ₑ δ)
- -- Category laws
- idlₑ : ∀ {Γ Δ}(σ : OPE Γ Δ) → idₑ ∘ₑ σ ≡ σ
- idlₑ ∙ = refl
- idlₑ (drop σ) = drop & idlₑ σ
- idlₑ (keep σ) = keep & idlₑ σ
- idrₑ : ∀ {Γ Δ}(σ : OPE Γ Δ) → σ ∘ₑ idₑ ≡ σ
- idrₑ ∙ = refl
- idrₑ (drop σ) = drop & idrₑ σ
- idrₑ (keep σ) = keep & idrₑ σ
- assₑ :
- ∀ {Γ Δ Σ Ξ}(σ : OPE Σ Ξ)(δ : OPE Δ Σ)(ν : OPE Γ Δ)
- → (σ ∘ₑ δ) ∘ₑ ν ≡ σ ∘ₑ (δ ∘ₑ ν)
- assₑ σ δ ∙ = refl
- assₑ σ δ (drop ν) = drop & assₑ σ δ ν
- assₑ σ (drop δ) (keep ν) = drop & assₑ σ δ ν
- assₑ (drop σ) (keep δ) (keep ν) = drop & assₑ σ δ ν
- assₑ (keep σ) (keep δ) (keep ν) = keep & assₑ σ δ ν
- -- (A ∈ _) : PSh OPE ("PSh C" means contravariant functor from C to Set)
- ∈ₑ : ∀ {A Γ Δ} → OPE Γ Δ → A ∈ Δ → A ∈ Γ
- ∈ₑ ∙ v = v
- ∈ₑ (drop σ) v = vs (∈ₑ σ v)
- ∈ₑ (keep σ) vz = vz
- ∈ₑ (keep σ) (vs v) = vs (∈ₑ σ v)
- ∈-idₑ : ∀ {A Γ}(v : A ∈ Γ) → ∈ₑ idₑ v ≡ v
- ∈-idₑ vz = refl
- ∈-idₑ (vs v) = vs & ∈-idₑ v
- ∈-∘ₑ : ∀ {A Γ Δ Σ}(σ : OPE Δ Σ)(δ : OPE Γ Δ)(v : A ∈ Σ) → ∈ₑ (σ ∘ₑ δ) v ≡ ∈ₑ δ (∈ₑ σ v)
- ∈-∘ₑ ∙ ∙ v = refl
- ∈-∘ₑ σ (drop δ) v = vs & ∈-∘ₑ σ δ v
- ∈-∘ₑ (drop σ) (keep δ) v = vs & ∈-∘ₑ σ δ v
- ∈-∘ₑ (keep σ) (keep δ) vz = refl
- ∈-∘ₑ (keep σ) (keep δ) (vs v) = vs & ∈-∘ₑ σ δ v
- -- (Tm _ A) : PSh OPE
- Tmₑ : ∀ {A Γ Δ} → OPE Γ Δ → Tm Δ A → Tm Γ A
- Tmₑ σ (var v) = var (∈ₑ σ v)
- Tmₑ σ (lam t) = lam (Tmₑ (keep σ) t)
- Tmₑ σ (app f a) = app (Tmₑ σ f) (Tmₑ σ a)
- Tmₑ σ true = true
- Tmₑ σ false = false
- Tmₑ σ (bcase b t f) = bcase (Tmₑ σ b) (Tmₑ σ t) (Tmₑ σ f)
- Tm-idₑ : ∀ {A Γ}(t : Tm Γ A) → Tmₑ idₑ t ≡ t
- Tm-idₑ (var v) = var & ∈-idₑ v
- Tm-idₑ (lam t) = lam & Tm-idₑ t
- Tm-idₑ (app f a) = app & Tm-idₑ f ⊗ Tm-idₑ a
- Tm-idₑ true = refl
- Tm-idₑ false = refl
- Tm-idₑ (bcase b t f) = bcase & Tm-idₑ b ⊗ Tm-idₑ t ⊗ Tm-idₑ f
- Tm-∘ₑ : ∀ {A Γ Δ Σ}(σ : OPE Δ Σ)(δ : OPE Γ Δ)(t : Tm Σ A) → Tmₑ (σ ∘ₑ δ) t ≡ Tmₑ δ (Tmₑ σ t)
- Tm-∘ₑ σ δ (var v) = var & ∈-∘ₑ σ δ v
- Tm-∘ₑ σ δ (lam t) = lam & Tm-∘ₑ (keep σ) (keep δ) t
- Tm-∘ₑ σ δ (app f a) = app & Tm-∘ₑ σ δ f ⊗ Tm-∘ₑ σ δ a
- Tm-∘ₑ σ δ true = refl
- Tm-∘ₑ σ δ false = refl
- Tm-∘ₑ σ δ (bcase b t f) = bcase & Tm-∘ₑ σ δ b ⊗ Tm-∘ₑ σ δ t ⊗ Tm-∘ₑ σ δ f
- -- Substitution
- --------------------------------------------------------------------------------
- infixr 6 _ₑ∘ₛ_ _ₛ∘ₑ_ _∘ₛ_
- data Sub (Γ : Con) : Con → Set where
- ∙ : Sub Γ ∙
- _,_ : ∀ {A Δ} → Sub Γ Δ → Tm Γ A → Sub Γ (Δ , A)
- -- left and right compositions
- _ₛ∘ₑ_ : ∀ {Γ Δ Σ} → Sub Δ Σ → OPE Γ Δ → Sub Γ Σ
- ∙ ₛ∘ₑ δ = ∙
- (σ , t) ₛ∘ₑ δ = σ ₛ∘ₑ δ , Tmₑ δ t
- _ₑ∘ₛ_ : ∀ {Γ Δ Σ} → OPE Δ Σ → Sub Γ Δ → Sub Γ Σ
- ∙ ₑ∘ₛ δ = δ
- drop σ ₑ∘ₛ (δ , t) = σ ₑ∘ₛ δ
- keep σ ₑ∘ₛ (δ , t) = σ ₑ∘ₛ δ , t
- dropₛ : ∀ {A Γ Δ} → Sub Γ Δ → Sub (Γ , A) Δ
- dropₛ σ = σ ₛ∘ₑ wk
- keepₛ : ∀ {A Γ Δ} → Sub Γ Δ → Sub (Γ , A) (Δ , A)
- keepₛ σ = dropₛ σ , var vz
- ⌜_⌝ᵒᵖᵉ : ∀ {Γ Δ} → OPE Γ Δ → Sub Γ Δ
- ⌜ ∙ ⌝ᵒᵖᵉ = ∙
- ⌜ drop σ ⌝ᵒᵖᵉ = dropₛ ⌜ σ ⌝ᵒᵖᵉ
- ⌜ keep σ ⌝ᵒᵖᵉ = keepₛ ⌜ σ ⌝ᵒᵖᵉ
- ∈ₛ : ∀ {A Γ Δ} → Sub Γ Δ → A ∈ Δ → Tm Γ A
- ∈ₛ (σ , t) vz = t
- ∈ₛ (σ , t)(vs v) = ∈ₛ σ v
- Tmₛ : ∀ {A Γ Δ} → Sub Γ Δ → Tm Δ A → Tm Γ A
- Tmₛ σ (var v) = ∈ₛ σ v
- Tmₛ σ (lam t) = lam (Tmₛ (keepₛ σ) t)
- Tmₛ σ (app f a) = app (Tmₛ σ f) (Tmₛ σ a)
- Tmₛ σ true = true
- Tmₛ σ false = false
- Tmₛ σ (bcase b t f) = bcase (Tmₛ σ b) (Tmₛ σ t) (Tmₛ σ f)
- idₛ : ∀ {Γ} → Sub Γ Γ
- idₛ {∙} = ∙
- idₛ {Γ , A} = keepₛ idₛ
- _∘ₛ_ : ∀ {Γ Δ Σ} → Sub Δ Σ → Sub Γ Δ → Sub Γ Σ
- ∙ ∘ₛ δ = ∙
- (σ , t) ∘ₛ δ = σ ∘ₛ δ , Tmₛ δ t
- -- Various versions of associativity and identity
- -- with substitution/embedding differing on sides of operations.
- -- Both for category laws and Tm/∈ functor laws.
- assₛₑₑ :
- ∀ {Γ Δ Σ Ξ}(σ : Sub Σ Ξ)(δ : OPE Δ Σ)(ν : OPE Γ Δ)
- → (σ ₛ∘ₑ δ) ₛ∘ₑ ν ≡ σ ₛ∘ₑ (δ ∘ₑ ν)
- assₛₑₑ ∙ δ ν = refl
- assₛₑₑ (σ , t) δ ν = _,_ & assₛₑₑ σ δ ν ⊗ (Tm-∘ₑ δ ν t ⁻¹)
- assₑₛₑ :
- ∀ {Γ Δ Σ Ξ}(σ : OPE Σ Ξ)(δ : Sub Δ Σ)(ν : OPE Γ Δ)
- → (σ ₑ∘ₛ δ) ₛ∘ₑ ν ≡ σ ₑ∘ₛ (δ ₛ∘ₑ ν)
- assₑₛₑ ∙ δ ν = refl
- assₑₛₑ (drop σ) (δ , t) ν = assₑₛₑ σ δ ν
- assₑₛₑ (keep σ) (δ , t) ν = (_, Tmₑ ν t) & assₑₛₑ σ δ ν
- idlₑₛ : ∀ {Γ Δ}(σ : Sub Γ Δ) → idₑ ₑ∘ₛ σ ≡ σ
- idlₑₛ ∙ = refl
- idlₑₛ (σ , t) = (_, t) & idlₑₛ σ
- idlₛₑ : ∀ {Γ Δ}(σ : OPE Γ Δ) → idₛ ₛ∘ₑ σ ≡ ⌜ σ ⌝ᵒᵖᵉ
- idlₛₑ ∙ = refl
- idlₛₑ (drop σ) =
- ((idₛ ₛ∘ₑ_) ∘ drop) & idrₑ σ ⁻¹
- ◾ assₛₑₑ idₛ σ wk ⁻¹
- ◾ dropₛ & idlₛₑ σ
- idlₛₑ (keep σ) =
- (_, var vz) &
- (assₛₑₑ idₛ wk (keep σ)
- ◾ ((idₛ ₛ∘ₑ_) ∘ drop) & (idlₑ σ ◾ idrₑ σ ⁻¹)
- ◾ assₛₑₑ idₛ σ wk ⁻¹
- ◾ (_ₛ∘ₑ wk) & idlₛₑ σ )
- idrₑₛ : ∀ {Γ Δ}(σ : OPE Γ Δ) → σ ₑ∘ₛ idₛ ≡ ⌜ σ ⌝ᵒᵖᵉ
- idrₑₛ ∙ = refl
- idrₑₛ (drop σ) = assₑₛₑ σ idₛ wk ⁻¹ ◾ dropₛ & idrₑₛ σ
- idrₑₛ (keep σ) = (_, var vz) & (assₑₛₑ σ idₛ wk ⁻¹ ◾ (_ₛ∘ₑ wk) & idrₑₛ σ)
- ∈-ₑ∘ₛ : ∀ {A Γ Δ Σ}(σ : OPE Δ Σ)(δ : Sub Γ Δ)(v : A ∈ Σ) → ∈ₛ (σ ₑ∘ₛ δ) v ≡ ∈ₛ δ (∈ₑ σ v)
- ∈-ₑ∘ₛ ∙ δ v = refl
- ∈-ₑ∘ₛ (drop σ) (δ , t) v = ∈-ₑ∘ₛ σ δ v
- ∈-ₑ∘ₛ (keep σ) (δ , t) vz = refl
- ∈-ₑ∘ₛ (keep σ) (δ , t) (vs v) = ∈-ₑ∘ₛ σ δ v
- Tm-ₑ∘ₛ : ∀ {A Γ Δ Σ}(σ : OPE Δ Σ)(δ : Sub Γ Δ)(t : Tm Σ A) → Tmₛ (σ ₑ∘ₛ δ) t ≡ Tmₛ δ (Tmₑ σ t)
- Tm-ₑ∘ₛ σ δ (var v) = ∈-ₑ∘ₛ σ δ v
- Tm-ₑ∘ₛ σ δ (lam t) =
- lam & ((λ x → Tmₛ (x , var vz) t) & assₑₛₑ σ δ wk ◾ Tm-ₑ∘ₛ (keep σ) (keepₛ δ) t)
- Tm-ₑ∘ₛ σ δ (app f a) = app & Tm-ₑ∘ₛ σ δ f ⊗ Tm-ₑ∘ₛ σ δ a
- Tm-ₑ∘ₛ σ δ true = refl
- Tm-ₑ∘ₛ σ δ false = refl
- Tm-ₑ∘ₛ σ δ (bcase b t f) = bcase & Tm-ₑ∘ₛ σ δ b ⊗ Tm-ₑ∘ₛ σ δ t ⊗ Tm-ₑ∘ₛ σ δ f
- ∈-ₛ∘ₑ : ∀ {A Γ Δ Σ}(σ : Sub Δ Σ)(δ : OPE Γ Δ)(v : A ∈ Σ) → ∈ₛ (σ ₛ∘ₑ δ) v ≡ Tmₑ δ (∈ₛ σ v)
- ∈-ₛ∘ₑ (σ , _) δ vz = refl
- ∈-ₛ∘ₑ (σ , _) δ (vs v) = ∈-ₛ∘ₑ σ δ v
- Tm-ₛ∘ₑ : ∀ {A Γ Δ Σ}(σ : Sub Δ Σ)(δ : OPE Γ Δ)(t : Tm Σ A) → Tmₛ (σ ₛ∘ₑ δ) t ≡ Tmₑ δ (Tmₛ σ t)
- Tm-ₛ∘ₑ σ δ (var v) = ∈-ₛ∘ₑ σ δ v
- Tm-ₛ∘ₑ σ δ (lam t) =
- lam &
- ((λ x → Tmₛ (x , var vz) t) &
- (assₛₑₑ σ δ wk
- ◾ (σ ₛ∘ₑ_) & (drop & (idrₑ δ ◾ idlₑ δ ⁻¹))
- ◾ assₛₑₑ σ wk (keep δ) ⁻¹)
- ◾ Tm-ₛ∘ₑ (keepₛ σ) (keep δ) t)
- Tm-ₛ∘ₑ σ δ (app f a) = app & Tm-ₛ∘ₑ σ δ f ⊗ Tm-ₛ∘ₑ σ δ a
- Tm-ₛ∘ₑ σ δ true = refl
- Tm-ₛ∘ₑ σ δ false = refl
- Tm-ₛ∘ₑ σ δ (bcase b t f) = bcase & Tm-ₛ∘ₑ σ δ b ⊗ Tm-ₛ∘ₑ σ δ t ⊗ Tm-ₛ∘ₑ σ δ f
- assₛₑₛ :
- ∀ {Γ Δ Σ Ξ}(σ : Sub Σ Ξ)(δ : OPE Δ Σ)(ν : Sub Γ Δ)
- → (σ ₛ∘ₑ δ) ∘ₛ ν ≡ σ ∘ₛ (δ ₑ∘ₛ ν)
- assₛₑₛ ∙ δ ν = refl
- assₛₑₛ (σ , t) δ ν = _,_ & assₛₑₛ σ δ ν ⊗ (Tm-ₑ∘ₛ δ ν t ⁻¹)
- assₛₛₑ :
- ∀ {Γ Δ Σ Ξ}(σ : Sub Σ Ξ)(δ : Sub Δ Σ)(ν : OPE Γ Δ)
- → (σ ∘ₛ δ) ₛ∘ₑ ν ≡ σ ∘ₛ (δ ₛ∘ₑ ν)
- assₛₛₑ ∙ δ ν = refl
- assₛₛₑ (σ , t) δ ν = _,_ & assₛₛₑ σ δ ν ⊗ (Tm-ₛ∘ₑ δ ν t ⁻¹)
- ∈-idₛ : ∀ {A Γ}(v : A ∈ Γ) → ∈ₛ idₛ v ≡ var v
- ∈-idₛ vz = refl
- ∈-idₛ (vs v) = ∈-ₛ∘ₑ idₛ wk v ◾ Tmₑ wk & ∈-idₛ v ◾ (var ∘ vs) & ∈-idₑ v
- ∈-∘ₛ : ∀ {A Γ Δ Σ}(σ : Sub Δ Σ)(δ : Sub Γ Δ)(v : A ∈ Σ) → ∈ₛ (σ ∘ₛ δ) v ≡ Tmₛ δ (∈ₛ σ v)
- ∈-∘ₛ (σ , _) δ vz = refl
- ∈-∘ₛ (σ , _) δ (vs v) = ∈-∘ₛ σ δ v
- Tm-idₛ : ∀ {A Γ}(t : Tm Γ A) → Tmₛ idₛ t ≡ t
- Tm-idₛ (var v) = ∈-idₛ v
- Tm-idₛ (lam t) = lam & Tm-idₛ t
- Tm-idₛ (app f a) = app & Tm-idₛ f ⊗ Tm-idₛ a
- Tm-idₛ true = refl
- Tm-idₛ false = refl
- Tm-idₛ (bcase b t f) = bcase & Tm-idₛ b ⊗ Tm-idₛ t ⊗ Tm-idₛ f
- Tm-∘ₛ : ∀ {A Γ Δ Σ}(σ : Sub Δ Σ)(δ : Sub Γ Δ)(t : Tm Σ A) → Tmₛ (σ ∘ₛ δ) t ≡ Tmₛ δ (Tmₛ σ t)
- Tm-∘ₛ σ δ (var v) = ∈-∘ₛ σ δ v
- Tm-∘ₛ σ δ (lam t) =
- lam &
- ((λ x → Tmₛ (x , var vz) t) &
- (assₛₛₑ σ δ wk
- ◾ (σ ∘ₛ_) & (idlₑₛ (dropₛ δ) ⁻¹) ◾ assₛₑₛ σ wk (keepₛ δ) ⁻¹)
- ◾ Tm-∘ₛ (keepₛ σ) (keepₛ δ) t)
- Tm-∘ₛ σ δ (app f a) = app & Tm-∘ₛ σ δ f ⊗ Tm-∘ₛ σ δ a
- Tm-∘ₛ σ δ true = refl
- Tm-∘ₛ σ δ false = refl
- Tm-∘ₛ σ δ (bcase b t f) = bcase & Tm-∘ₛ σ δ b ⊗ Tm-∘ₛ σ δ t ⊗ Tm-∘ₛ σ δ f
- idrₛ : ∀ {Γ Δ}(σ : Sub Γ Δ) → σ ∘ₛ idₛ ≡ σ
- idrₛ ∙ = refl
- idrₛ (σ , t) = _,_ & idrₛ σ ⊗ Tm-idₛ t
- idlₛ : ∀ {Γ Δ}(σ : Sub Γ Δ) → idₛ ∘ₛ σ ≡ σ
- idlₛ ∙ = refl
- idlₛ (σ , t) = (_, t) & (assₛₑₛ idₛ wk (σ , t) ◾ (idₛ ∘ₛ_) & idlₑₛ σ ◾ idlₛ σ)
- assₛ :
- ∀ {Γ Δ Σ Ξ}(σ : Sub Σ Ξ)(δ : Sub Δ Σ)(ν : Sub Γ Δ)
- → (σ ∘ₛ δ) ∘ₛ ν ≡ σ ∘ₛ (δ ∘ₛ ν)
- assₛ ∙ δ ν = refl
- assₛ (σ , t) δ ν = _,_ & assₛ σ δ ν ⊗ (Tm-∘ₛ δ ν t ⁻¹)
Advertisement
Add Comment
Please, Sign In to add comment
Advertisement