158 lines
9.2 KiB
Agda
158 lines
9.2 KiB
Agda
module univTypes.SubjectReduction.Inversion 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.SubjectReduction.Specification
|
||
open import univTypes.SubjectReduction.ConversionProperties using (≈-refl; ≈-trans; ≈-sym; ≈-sub)
|
||
|
||
--------------------------------------------------------------------------------
|
||
|
||
-- Inversion for lambda terms
|
||
|
||
↪-∀-shape : ∀ {n} {t t₁ : Term n} {t₂ : Term (suc n)} →
|
||
∀[x⦂ t₁ ] t₂ ↪ t →
|
||
∃[ t₁' ] ∃[ t₂' ] t ≡ ∀[x⦂ t₁' ] t₂' × (t₁ ↪* t₁') × (t₂ ↪* t₂')
|
||
↪-∀-shape (ξ-∀₁ ↪₁) = ⟨ _ , ⟨ _ , ⟨ refl , ⟨ ↪*-step ↪₁ ↪*-refl , ↪*-refl ⟩ ⟩ ⟩ ⟩
|
||
↪-∀-shape (ξ-∀₂ ↪₂) = ⟨ _ , ⟨ _ , ⟨ refl , ⟨ ↪*-refl , ↪*-step ↪₂ ↪*-refl ⟩ ⟩ ⟩ ⟩
|
||
|
||
↪*-∀-shape : ∀ {n} {t t₁ : Term n} {t₂ : Term (suc n)} →
|
||
(∀[x⦂ t₁ ] t₂) ↪* t →
|
||
∃[ t₁' ] ∃[ t₂' ] t ≡ ∀[x⦂ t₁' ] t₂' × (t₁ ↪* t₁') × (t₂ ↪* t₂')
|
||
↪*-∀-shape ↪*-refl = ⟨ _ , ⟨ _ , ⟨ refl , ⟨ ↪*-refl , ↪*-refl ⟩ ⟩ ⟩ ⟩
|
||
↪*-∀-shape (↪*-step ∀↪z z↪*t) with ↪-∀-shape ∀↪z
|
||
... | ⟨ x₁ , ⟨ x₂ , ⟨ refl , ⟨ t₁↪*x₁ , t₂↪*x₂ ⟩ ⟩ ⟩ ⟩ with ↪*-∀-shape z↪*t
|
||
... | ⟨ y₁ , ⟨ y₂ , ⟨ refl , ⟨ x₁↪*y₁ , x₂↪*y₂ ⟩ ⟩ ⟩ ⟩
|
||
= ⟨ y₁ , ⟨ y₂ , ⟨ refl , ⟨ ↪*-trans t₁↪*x₁ x₁↪*y₁ , ↪*-trans t₂↪*x₂ x₂↪*y₂ ⟩ ⟩ ⟩ ⟩
|
||
|
||
invert-≈-∀ : ∀ {n} {t₁ t₁' : Term n} {t₂ t₂' : Term (suc n)} →
|
||
(∀[x⦂ t₁ ] t₂) ≈ (∀[x⦂ t₁' ] t₂') →
|
||
t₁ ≈ t₁' × t₂ ≈ t₂'
|
||
invert-≈-∀ (mk-≈ x ∀₁↪*x ∀₂↪*x) with ↪*-∀-shape ∀₁↪*x | ↪*-∀-shape ∀₂↪*x
|
||
... | ⟨ a₁ , ⟨ a₂ , ⟨ refl , ⟨ t₁↪*a₁ , t₂↪*a₁ ⟩ ⟩ ⟩ ⟩
|
||
| ⟨ b₁ , ⟨ b₂ , ⟨ refl , ⟨ t₁'↪*b₁ , t₂'↪*b₂ ⟩ ⟩ ⟩ ⟩
|
||
= ⟨ mk-≈ a₁ t₁↪*a₁ t₁'↪*b₁ , mk-≈ a₂ t₂↪*a₁ t₂'↪*b₂ ⟩
|
||
|
||
invert-⊢λ' : ∀ {n} {Γ : Context n} {e : Term (suc n)} {t : Term n} →
|
||
Γ ⊢ `λ e ⦂ t →
|
||
∃[ t₁ ] ∃[ t₂ ]
|
||
t ≈ (∀[x⦂ t₁ ] t₂) ×
|
||
Γ ⊢ t₁ ⦂ `Set ×
|
||
Γ , t₁ ⊢ e ⦂ t₂
|
||
invert-⊢λ' (⊢-λ ⊢λ ⊢e) = ⟨ _ , ⟨ _ , ⟨ ≈-refl , ⟨ ⊢λ , ⊢e ⟩ ⟩ ⟩ ⟩
|
||
invert-⊢λ' (⊢-≈ t₁≈t ⊢λ⦂t₁) with invert-⊢λ' ⊢λ⦂t₁
|
||
... | ⟨ X , ⟨ E , ⟨ t₁≈∀[X]E , ⟨ X⦂Set , Γ,X⊢e⦂E ⟩ ⟩ ⟩ ⟩
|
||
= ⟨ X , ⟨ E , ⟨ ≈-trans (≈-sym t₁≈t) t₁≈∀[X]E , ⟨ X⦂Set , Γ,X⊢e⦂E ⟩ ⟩ ⟩ ⟩
|
||
|
||
invert-⊢λ : ∀ {n} {Γ : Context n} {e : Term (suc n)} {t₁ : Term n} {t₂ : Term (suc n)}
|
||
→ Γ ⊢ `λ e ⦂ ∀[x⦂ t₁ ] t₂
|
||
→ ∃[ t₁' ] ∃[ t₂' ]
|
||
t₁ ≈ t₁' ×
|
||
t₂ ≈ t₂' ×
|
||
Γ ⊢ t₁' ⦂ `Set ×
|
||
Γ , t₁' ⊢ e ⦂ t₂'
|
||
invert-⊢λ (⊢-λ ⊢λ ⊢λ₁) = ⟨ _ , ⟨ _ , ⟨ mk-≈ _ ↪*-refl ↪*-refl , ⟨ mk-≈ _ ↪*-refl ↪*-refl , ⟨ ⊢λ , ⊢λ₁ ⟩ ⟩ ⟩ ⟩ ⟩
|
||
invert-⊢λ (⊢-≈ t≈∀ ⊢λ) with invert-⊢λ' ⊢λ
|
||
... | ⟨ X , ⟨ E , ⟨ t≈∀' , ⟨ X⦂Set , Γ,X⊢e⦂E ⟩ ⟩ ⟩ ⟩ with invert-≈-∀ (≈-trans (≈-sym t≈∀) t≈∀')
|
||
... | ⟨ ≈₁ , ≈₂ ⟩
|
||
= ⟨ X , ⟨ E , ⟨ ≈₁ , ⟨ ≈₂ , ⟨ X⦂Set , Γ,X⊢e⦂E ⟩ ⟩ ⟩ ⟩ ⟩
|
||
|
||
|
||
-- Inversion for pairs
|
||
|
||
↪-∃-shape : ∀ {n} {t t₁ : Term n} {t₂ : Term (suc n)} →
|
||
∃[x⦂ t₁ ] t₂ ↪ t →
|
||
∃[ t₁' ] ∃[ t₂' ] t ≡ ∃[x⦂ t₁' ] t₂' × (t₁ ↪* t₁') × (t₂ ↪* t₂')
|
||
↪-∃-shape (ξ-∃₁ ↪₁) = ⟨ _ , ⟨ _ , ⟨ refl , ⟨ ↪*-step ↪₁ ↪*-refl , ↪*-refl ⟩ ⟩ ⟩ ⟩
|
||
↪-∃-shape (ξ-∃₂ ↪₂) = ⟨ _ , ⟨ _ , ⟨ refl , ⟨ ↪*-refl , ↪*-step ↪₂ ↪*-refl ⟩ ⟩ ⟩ ⟩
|
||
|
||
↪*-∃-shape : ∀ {n} {t t₁ : Term n} {t₂ : Term (suc n)} →
|
||
(∃[x⦂ t₁ ] t₂) ↪* t →
|
||
∃[ t₁' ] ∃[ t₂' ] t ≡ ∃[x⦂ t₁' ] t₂' × (t₁ ↪* t₁') × (t₂ ↪* t₂')
|
||
↪*-∃-shape ↪*-refl = ⟨ _ , ⟨ _ , ⟨ refl , ⟨ ↪*-refl , ↪*-refl ⟩ ⟩ ⟩ ⟩
|
||
↪*-∃-shape (↪*-step ∀↪z z↪*t) with ↪-∃-shape ∀↪z
|
||
... | ⟨ x₁ , ⟨ x₂ , ⟨ refl , ⟨ t₁↪*x₁ , t₂↪*x₂ ⟩ ⟩ ⟩ ⟩ with ↪*-∃-shape z↪*t
|
||
... | ⟨ y₁ , ⟨ y₂ , ⟨ refl , ⟨ x₁↪*y₁ , x₂↪*y₂ ⟩ ⟩ ⟩ ⟩
|
||
= ⟨ y₁ , ⟨ y₂ , ⟨ refl , ⟨ ↪*-trans t₁↪*x₁ x₁↪*y₁ , ↪*-trans t₂↪*x₂ x₂↪*y₂ ⟩ ⟩ ⟩ ⟩
|
||
|
||
invert-≈-∃ : ∀ {n} {t₁ t₁' : Term n} {t₂ t₂' : Term (suc n)} →
|
||
(∃[x⦂ t₁ ] t₂) ≈ (∃[x⦂ t₁' ] t₂') →
|
||
t₁ ≈ t₁' × t₂ ≈ t₂'
|
||
invert-≈-∃ (mk-≈ x ∃₁↪*x ∃₂↪*x) with ↪*-∃-shape ∃₁↪*x | ↪*-∃-shape ∃₂↪*x
|
||
... | ⟨ a₁ , ⟨ a₂ , ⟨ refl , ⟨ t₁↪*a₁ , t₂↪*a₁ ⟩ ⟩ ⟩ ⟩
|
||
| ⟨ b₁ , ⟨ b₂ , ⟨ refl , ⟨ t₁'↪*b₁ , t₂'↪*b₂ ⟩ ⟩ ⟩ ⟩
|
||
= ⟨ mk-≈ a₁ t₁↪*a₁ t₁'↪*b₁ , mk-≈ a₂ t₂↪*a₁ t₂'↪*b₂ ⟩
|
||
|
||
invert-⊢,' : ∀ {n} {Γ : Context n} {l r t : Term n} →
|
||
Γ ⊢ l `, r ⦂ t →
|
||
∃[ t₁ ] ∃[ t₂ ]
|
||
t ≈ (∃[x⦂ t₁ ] t₂) ×
|
||
Γ ⊢ l ⦂ t₁ ×
|
||
Γ ⊢ r ⦂ t₂ [ l ]
|
||
invert-⊢,' (⊢-≈ t₁≈t ⊢lr) with invert-⊢,' ⊢lr
|
||
... | ⟨ x₁ , ⟨ x₂ , ⟨ t≈∃ , ⟨ ⊢l , ⊢r ⟩ ⟩ ⟩ ⟩
|
||
= ⟨ x₁ , ⟨ x₂ , ⟨ ≈-sym (≈-trans (≈-sym t≈∃) t₁≈t) , ⟨ ⊢l , ⊢r ⟩ ⟩ ⟩ ⟩
|
||
invert-⊢,' (⊢-, {n} {Γ} {e₁} {e₂} {t₁} {t₂} ⊢l ⊢r) = ⟨ t₁ , ⟨ t₂ , ⟨ ≈-refl , ⟨ ⊢l , ⊢r ⟩ ⟩ ⟩ ⟩
|
||
|
||
invert-⊢, : ∀ {n} {Γ : Context n} {l r : Term n} {t₁ : Term n} {t₂ : Term (suc n)}
|
||
→ Γ ⊢ l `, r ⦂ ∃[x⦂ t₁ ] t₂
|
||
→ ∃[ t₁' ] ∃[ t₂' ]
|
||
t₁ ≈ t₁' ×
|
||
t₂ ≈ t₂' ×
|
||
Γ ⊢ l ⦂ t₁ ×
|
||
Γ ⊢ r ⦂ t₂ [ l ]
|
||
invert-⊢, (⊢-≈ t≈∃ ⊢lr) with invert-⊢,' ⊢lr
|
||
... | ⟨ x₁ , ⟨ x₂ , ⟨ t≈∃' , ⟨ ⊢l , ⊢r ⟩ ⟩ ⟩ ⟩ with invert-≈-∃ (≈-trans (≈-sym t≈∃) t≈∃')
|
||
... | ⟨ ≈₁ , ≈₂ ⟩
|
||
= ⟨ x₁ , ⟨ x₂ , ⟨ ≈₁ , ⟨ ≈₂ , ⟨ ⊢-≈ (≈-sym ≈₁) ⊢l , ⊢-≈ (≈-sub _ (≈-sym ≈₂)) ⊢r ⟩ ⟩ ⟩ ⟩ ⟩
|
||
invert-⊢, (⊢-, ⊢l ⊢r)
|
||
= ⟨ _ , ⟨ _ , ⟨ ≈-refl , ⟨ ≈-refl , ⟨ ⊢l , ⊢r ⟩ ⟩ ⟩ ⟩ ⟩
|
||
|
||
↪-≡-shape : ∀ {n} {t u₁ u₂ : Term n} →
|
||
u₁ `≡ u₂ ↪ t →
|
||
∃[ u₁' ] ∃[ u₂' ] t ≡ u₁' `≡ u₂' × (u₁ ↪* u₁') × (u₂ ↪* u₂')
|
||
↪-≡-shape (ξ-≡₁ ↪₁) = ⟨ _ , ⟨ _ , ⟨ refl , ⟨ ↪*-step ↪₁ ↪*-refl , ↪*-refl ⟩ ⟩ ⟩ ⟩
|
||
↪-≡-shape (ξ-≡₂ ↪₂) = ⟨ _ , ⟨ _ , ⟨ refl , ⟨ ↪*-refl , ↪*-step ↪₂ ↪*-refl ⟩ ⟩ ⟩ ⟩
|
||
|
||
↪*-≡-shape : ∀ {n} {t u₁ u₂ : Term n} →
|
||
(u₁ `≡ u₂) ↪* t →
|
||
∃[ u₁' ] ∃[ u₂' ] t ≡ u₁' `≡ u₂' × (u₁ ↪* u₁') × (u₂ ↪* u₂')
|
||
↪*-≡-shape ↪*-refl = ⟨ _ , ⟨ _ , ⟨ refl , ⟨ ↪*-refl , ↪*-refl ⟩ ⟩ ⟩ ⟩
|
||
↪*-≡-shape (↪*-step ≡↪x x↪*t) with ↪-≡-shape ≡↪x
|
||
... | ⟨ a , ⟨ b , ⟨ refl , ⟨ u₁↪*a , u₂↪*b ⟩ ⟩ ⟩ ⟩ with ↪*-≡-shape x↪*t
|
||
... | ⟨ x , ⟨ y , ⟨ refl , ⟨ a↪*x , b↪*y ⟩ ⟩ ⟩ ⟩
|
||
= ⟨ x , ⟨ y , ⟨ refl , ⟨ ↪*-trans u₁↪*a a↪*x , ↪*-trans u₂↪*b b↪*y ⟩ ⟩ ⟩ ⟩
|
||
|
||
invert-≈-≡ : ∀ {n} {u₁ u₁' u₂ u₂' : Term n} →
|
||
(u₁ `≡ u₂) ≈ (u₁' `≡ u₂') →
|
||
u₁ ≈ u₁' × u₂ ≈ u₂'
|
||
invert-≈-≡ (mk-≈ x ≡↪*x ≡'↪*x) with ↪*-≡-shape ≡↪*x
|
||
... | ⟨ a , ⟨ b , ⟨ refl , ⟨ u₁↪*a , u₂↪*b ⟩ ⟩ ⟩ ⟩ with ↪*-≡-shape ≡'↪*x
|
||
... | ⟨ _ , ⟨ _ , ⟨ refl , ⟨ u₁'↪*a , u₂'↪*b ⟩ ⟩ ⟩ ⟩
|
||
= ⟨ mk-≈ a u₁↪*a u₁'↪*a , mk-≈ b u₂↪*b u₂'↪*b ⟩
|
||
|
||
invert-⊢refl' : ∀ {n} {Γ : Context n} {t : Term n}
|
||
→ Γ ⊢ `refl ⦂ t
|
||
→ ∃[ u₁ ] ∃[ u₂ ]
|
||
t ≈ u₁ `≡ u₂ ×
|
||
u₁ ≈ u₂
|
||
invert-⊢refl' (⊢-≈ t₁≈t ⊢refl) with invert-⊢refl' ⊢refl
|
||
... | ⟨ u₁ , ⟨ u₂ , ⟨ t₁≈≡ , u₁≈u₂ ⟩ ⟩ ⟩
|
||
= ⟨ _ , ⟨ _ , ⟨ ≈-trans (≈-sym t₁≈t) t₁≈≡ , u₁≈u₂ ⟩ ⟩ ⟩
|
||
invert-⊢refl' (⊢-refl ⊢refl) = ⟨ _ , ⟨ _ , ⟨ ≈-refl , ≈-refl ⟩ ⟩ ⟩
|
||
|
||
invert-⊢refl : ∀ {n} {Γ : Context n} {u₁ u₂ : Term n}
|
||
→ Γ ⊢ `refl ⦂ u₁ `≡ u₂
|
||
→ u₁ ≈ u₂
|
||
invert-⊢refl (⊢-refl ⊢refl) = ≈-refl
|
||
invert-⊢refl (⊢-≈ t≈≡ ⊢refl) with invert-⊢refl' ⊢refl
|
||
... | ⟨ u₁' , ⟨ u₂' , ⟨ t≈≡' , ≈' ⟩ ⟩ ⟩ with invert-≈-≡ (≈-trans (≈-sym t≈≡') t≈≡)
|
||
... | ⟨ ≈₁ , ≈₂ ⟩
|
||
= ≈-trans (≈-trans (≈-sym ≈₁) ≈') ≈₂
|