91 lines
7.0 KiB
Agda
91 lines
7.0 KiB
Agda
module univTypes.SubjectReduction.SubjectReduction where
|
||
|
||
open import Data.Product renaming (_,_ to ⟨_,_⟩)
|
||
open import Data.Sum
|
||
open import Data.Nat using (ℕ; zero; suc; _+_)
|
||
open import Function using (_∘_)
|
||
open import Relation.Binary.PropositionalEquality using (_≡_; refl; sym; subst; cong; cong₂; module ≡-Reasoning)
|
||
open import Data.Fin using (zero; suc) renaming (Fin to 𝔽)
|
||
open import Relation.Nullary using (¬_)
|
||
open import Data.Empty using (⊥; ⊥-elim)
|
||
|
||
open import univTypes.Util.Fin using (zero; suc)
|
||
open import univTypes.SubjectReduction.Specification
|
||
open import univTypes.SubjectReduction.Inversion using (invert-⊢λ; invert-⊢,; invert-⊢refl)
|
||
open import univTypes.SubjectReduction.SubstitutionPreservesTyping using (⊢sub; ⊢sub₁)
|
||
open import univTypes.SubjectReduction.ConversionProperties using (≈-sym; ≈σ-sub; ≈σ-sub₁; ≈→≈σ; ↪→≈; ≈-Γ-⊢₁; ≈-trans; ≈-sub; ≈-ren; ≈-refl)
|
||
|
||
-- Subject Reduction
|
||
|
||
type-two : ∀ {n} {Γ : Context n} {e : Term n} {x t}
|
||
→ Γ ⊢ e ⦂ ∀[x⦂ x ] t
|
||
→ Term _
|
||
type-two {t = t} _ = t
|
||
|
||
subject-reduction : ∀ {n} {Γ : Context n} {e e' t : Term n}
|
||
→ Γ ⊢ e ⦂ t
|
||
→ e ↪ e'
|
||
----------
|
||
→ Γ ⊢ e' ⦂ t
|
||
subject-reduction (⊢-≈ t≈t₁ ⊢e) β-λ = ⊢-≈ t≈t₁ (subject-reduction ⊢e β-λ)
|
||
subject-reduction (⊢-≈ t≈t₁ ⊢e) (ξ-λ e↪e') = ⊢-≈ t≈t₁ (subject-reduction ⊢e (ξ-λ e↪e'))
|
||
subject-reduction (⊢-≈ t≈t₁ ⊢e) (ξ-·₁ e↪e') = ⊢-≈ t≈t₁ (subject-reduction ⊢e (ξ-·₁ e↪e'))
|
||
subject-reduction (⊢-≈ t≈t₁ ⊢e) (ξ-·₂ e↪e') = ⊢-≈ t≈t₁ (subject-reduction ⊢e (ξ-·₂ e↪e'))
|
||
subject-reduction (⊢-≈ t≈t₁ ⊢e) (ξ-∀₁ e↪e') = ⊢-≈ t≈t₁ (subject-reduction ⊢e (ξ-∀₁ e↪e'))
|
||
subject-reduction (⊢-≈ t≈t₁ ⊢e) (ξ-∀₂ e↪e') = ⊢-≈ t≈t₁ (subject-reduction ⊢e (ξ-∀₂ e↪e'))
|
||
subject-reduction (⊢-λ ⊢e₁ ⊢e₂) (ξ-λ e₁↪e₁') = ⊢-λ ⊢e₁ (subject-reduction ⊢e₂ e₁↪e₁')
|
||
subject-reduction (⊢-· ⊢e₁ ⊢e₂) (ξ-·₁ e₁↪e₁') = ⊢-· (subject-reduction ⊢e₁ e₁↪e₁') ⊢e₂
|
||
subject-reduction (⊢-· ⊢e₁ ⊢e₂) (ξ-·₂ e₂↪e₂') =
|
||
⊢-≈ (≈-sym (≈σ-sub {e = type-two ⊢e₁} (≈→≈σ (↪→≈ e₂↪e₂')))) (⊢-· ⊢e₁ (subject-reduction ⊢e₂ e₂↪e₂'))
|
||
subject-reduction (⊢-∀ ⊢t ⊢e) (ξ-∀₁ t↪t') =
|
||
⊢-∀ (subject-reduction ⊢t t↪t') (≈-Γ-⊢₁ (↪→≈ t↪t') ⊢e)
|
||
subject-reduction (⊢-∀ ⊢e₁ ⊢e₂) (ξ-∀₂ e₁↪e₁') = ⊢-∀ ⊢e₁ (subject-reduction ⊢e₂ e₁↪e₁')
|
||
subject-reduction (⊢-· ⊢e₁ ⊢e₂) β-λ with invert-⊢λ ⊢e₁
|
||
... | ⟨ t₁' , ⟨ t₂' , ⟨ t₁≈t₁' , ⟨ t₂≈t₂' , ⟨ ⊢t₁' , Γ,t₁'⊢e₁⦂t₂' ⟩ ⟩ ⟩ ⟩ ⟩
|
||
= ⊢sub (⊢sub₁ (⊢-≈ t₁≈t₁' ⊢e₂)) ⊢e₁⦂t₂
|
||
where
|
||
⊢e₁⦂t₂ = ⊢-≈ (≈-sym t₂≈t₂') Γ,t₁'⊢e₁⦂t₂'
|
||
subject-reduction (⊢-` x x₁) ()
|
||
subject-reduction ⊢-Set ()
|
||
subject-reduction (⊢-≈ x ⊢e) β-proj₁ = ⊢-≈ x (subject-reduction ⊢e β-proj₁)
|
||
subject-reduction (⊢-≈ x ⊢e) β-proj₂ = ⊢-≈ x (subject-reduction ⊢e β-proj₂)
|
||
subject-reduction (⊢-≈ x ⊢e) β-subst = ⊢-≈ x (subject-reduction ⊢e β-subst)
|
||
subject-reduction (⊢-≈ x ⊢e) (ξ-∃₁ e↪e') = ⊢-≈ x (subject-reduction ⊢e (ξ-∃₁ e↪e'))
|
||
subject-reduction (⊢-≈ x ⊢e) (ξ-∃₂ e↪e') = ⊢-≈ x (subject-reduction ⊢e (ξ-∃₂ e↪e'))
|
||
subject-reduction (⊢-≈ x ⊢e) (ξ-proj₁ e↪e') = ⊢-≈ x (subject-reduction ⊢e (ξ-proj₁ e↪e'))
|
||
subject-reduction (⊢-≈ x ⊢e) (ξ-proj₂ e↪e') = ⊢-≈ x (subject-reduction ⊢e (ξ-proj₂ e↪e'))
|
||
subject-reduction (⊢-≈ x ⊢e) (ξ-,₁ e↪e') = ⊢-≈ x (subject-reduction ⊢e (ξ-,₁ e↪e'))
|
||
subject-reduction (⊢-≈ x ⊢e) (ξ-,₂ e↪e') = ⊢-≈ x (subject-reduction ⊢e (ξ-,₂ e↪e'))
|
||
subject-reduction (⊢-≈ x ⊢e) (ξ-≡₁ e↪e') = ⊢-≈ x (subject-reduction ⊢e (ξ-≡₁ e↪e'))
|
||
subject-reduction (⊢-≈ x ⊢e) (ξ-≡₂ e↪e') = ⊢-≈ x (subject-reduction ⊢e (ξ-≡₂ e↪e'))
|
||
subject-reduction (⊢-≈ t₁≈t ⊢e) (ξ-subst₁ t₂↪t') = ⊢-≈ t₁≈t (subject-reduction ⊢e (ξ-subst₁ t₂↪t'))
|
||
subject-reduction (⊢-≈ x ⊢e) (ξ-subst₂ e↪e') = ⊢-≈ x (subject-reduction ⊢e (ξ-subst₂ e↪e'))
|
||
subject-reduction (⊢-≈ x ⊢e) (ξ-subst₃ e↪e') = ⊢-≈ x (subject-reduction ⊢e (ξ-subst₃ e↪e'))
|
||
subject-reduction (⊢-∃ ⊢t₁ t₁⊢t₂) (ξ-∃₁ t₁↪t₁')
|
||
= ⊢-∃ (subject-reduction ⊢t₁ t₁↪t₁') (≈-Γ-⊢₁ (↪→≈ t₁↪t₁') t₁⊢t₂)
|
||
subject-reduction (⊢-∃ ⊢e ⊢e₁) (ξ-∃₂ e↪e') = ⊢-∃ ⊢e (subject-reduction ⊢e₁ e↪e')
|
||
subject-reduction (⊢-, {t₂ = t₂} ⊢l ⊢r) (ξ-,₁ l↪l')
|
||
= ⊢-, (subject-reduction ⊢l l↪l')
|
||
(⊢-≈ (≈σ-sub₁ {e = t₂} (↪→≈ l↪l')) ⊢r)
|
||
-- t₂ [ e₁ ] ≈ t₂ [ e₁' ]
|
||
subject-reduction (⊢-, ⊢l ⊢r) (ξ-,₂ r↪r') = ⊢-, ⊢l (subject-reduction ⊢r r↪r')
|
||
subject-reduction (⊢-proj₁ ⊢e) β-proj₁ with invert-⊢, ⊢e
|
||
... | ⟨ t₁ , ⟨ t₂ , ⟨ t≈t₁ , ⟨ t₃≈t₂ , ⟨ ⊢e' , ⊢e₂ ⟩ ⟩ ⟩ ⟩ ⟩
|
||
= ⊢e'
|
||
subject-reduction (⊢-proj₁ ⊢e) (ξ-proj₁ e↪e') = ⊢-proj₁ (subject-reduction ⊢e e↪e')
|
||
subject-reduction (⊢-proj₂ {t₂ = t'} ⊢e) β-proj₂ with invert-⊢, ⊢e
|
||
... | ⟨ t₁ , ⟨ t₂ , ⟨ t≈t₁ , ⟨ t₃≈t₂ , ⟨ ⊢e' , ⊢e₂ ⟩ ⟩ ⟩ ⟩ ⟩
|
||
= ⊢-≈ (≈σ-sub₁ {e = t'} (mk-≈ _ ↪*-refl (↪*-step β-proj₁ ↪*-refl))) ⊢e₂
|
||
subject-reduction (⊢-proj₂ {e = e} {t₂ = t₂} ⊢e) (ξ-proj₂ e↪e')
|
||
= ⊢-≈ (≈-sym (≈σ-sub {e = t₂} (≈→≈σ (↪→≈ (ξ-proj₁ e↪e'))))) (⊢-proj₂ (subject-reduction ⊢e e↪e'))
|
||
subject-reduction (⊢-≡ ⊢e ⊢e₁) (ξ-≡₁ e↪e') = ⊢-≡ (subject-reduction ⊢e e↪e') ⊢e₁
|
||
subject-reduction (⊢-≡ ⊢e ⊢e₁) (ξ-≡₂ e↪e') = ⊢-≡ ⊢e (subject-reduction ⊢e₁ e↪e')
|
||
subject-reduction (⊢-refl ⊢e) ()
|
||
subject-reduction (⊢-subst {t = t} ⊢t ⊢u₁ ⊢u₂ ⊢≈ ⊢t[u₁]) β-subst with invert-⊢refl ⊢≈
|
||
... | u₁≈u₂
|
||
= ⊢-≈ (≈σ-sub₁ {e = t} u₁≈u₂) ⊢t[u₁]
|
||
subject-reduction (⊢-subst {u₁ = u₁} {u₂ = u₂} ⊢t ⊢u₁ ⊢u₂ ⊢≈ ⊢t[u₁]) (ξ-subst₁ t↪t')
|
||
= ⊢-≈ (≈-sym (≈-sub (0↦ u₂) (↪→≈ t↪t'))) (⊢-subst (subject-reduction ⊢t t↪t') ⊢u₁ ⊢u₂ ⊢≈ (⊢-≈ (≈-sub (0↦ u₁) (↪→≈ t↪t')) ⊢t[u₁]))
|
||
subject-reduction (⊢-subst ⊢e ⊢e₁ ⊢e₂ ⊢e₃ ⊢e₄) (ξ-subst₂ e↪e') = ⊢-subst ⊢e ⊢e₁ ⊢e₂ (subject-reduction ⊢e₃ e↪e') ⊢e₄
|
||
subject-reduction (⊢-subst ⊢e ⊢e₁ ⊢e₂ ⊢e₃ ⊢e₄) (ξ-subst₃ e↪e') = ⊢-subst ⊢e ⊢e₁ ⊢e₂ ⊢e₃ (subject-reduction ⊢e₄ e↪e')
|