{-# OPTIONS --without-K --safe #-}
open import Axiom.Extensionality.Propositional
module Mints.Soundness.Box (fext : ∀ {ℓ ℓ′} → Extensionality ℓ ℓ′) where
open import Lib
open import Data.Nat.Properties as ℕₚ
open import Mints.Statics.Properties
open import Mints.Semantics.Properties.Domain fext
open import Mints.Semantics.Properties.Evaluation fext
open import Mints.Semantics.Properties.PER fext
open import Mints.Completeness.Consequences fext
open import Mints.Soundness.Realizability fext
open import Mints.Soundness.Cumulativity fext
open import Mints.Soundness.LogRel
open import Mints.Soundness.ToSyntax fext
open import Mints.Soundness.Properties.LogRel fext
open import Mints.Soundness.Properties.Substitutions fext
σ；1∼extρ : (⊩Γ : ⊩ Γ) → Δ ⊢s σ ∶ ⊩Γ ® ρ → [] ∷⁺ Δ ⊢s σ ； 1 ∶ ⊩κ ⊩Γ ® (ext ρ 1)
σ；1∼extρ ⊩Γ σ∼ρ = record
{ ⊢σ = s-； L.[ [] ] ⊢σ (⊢κ ⊢Δ) refl
; Ψs⁻ = L.[ [] ]
; Γ≡ = refl
; ≈σ∥ = s-≈-refl ⊢σ
; O≡ = refl
; len≡ = refl
; step = σ∼ρ
}
where
⊢σ = s®⇒⊢s ⊩Γ σ∼ρ
⊢Δ = proj₁ (presup-s ⊢σ)
□-wf′ : ∀ {i} →
[] ∷⁺ Γ ⊩ T ∶ Se i →
Γ ⊩ □ T ∶ Se i
□-wf′ {Γ} {T} {i} ⊩T
with ⊩T
... | record { ⊩Γ = ⊩κ ⊩Γ ; lvl = lvl ; krip = Tkrip } = record { ⊩Γ = ⊩Γ ; krip = krip }
where
⊢T = ⊩⇒⊢-tm ⊩T
⊢Γ = ⊩⇒⊢ ⊩Γ
krip : ∀ {Δ σ ρ} →
Δ ⊢s σ ∶ ⊩Γ ® ρ →
GluExp _ Δ (□ T) (Se i) σ ρ
krip {Δ} {σ} {ρ} σ∼ρ
with Tkrip (σ；1∼extρ ⊩Γ σ∼ρ)
... | record { ↘⟦T⟧ = ⟦Se⟧ _ ; ↘⟦t⟧ = ↘⟦T⟧ ; T∈𝕌 = U i<lvl _ ; t∼⟦t⟧ = T∼⟦T⟧ }
with T∼⟦T⟧
... | record { t∶T = t∶T ; T≈ = T≈ ; A∈𝕌 = A∈𝕌 ; rel = Trel } = record
{ ↘⟦T⟧ = ⟦Se⟧ _
; ↘⟦t⟧ = ⟦□⟧ ↘⟦T⟧
; T∈𝕌 = U′ i<lvl
; t∼⟦t⟧ = record
{ t∶T = t[σ] (□-wf ⊢T) ⊢σ
; T≈ = lift-⊢≈-Se (Se-[] _ ⊢σ) i<lvl
; A∈𝕌 = □ λ κ → 𝕌-mon κ A∈𝕌
; rel = rel
}
}
where
⊢σ = s®⇒⊢s ⊩Γ σ∼ρ
rel : Glu-wellfounded lvl i<lvl Δ (sub (□ T) σ) (□ (λ κ → 𝕌-mon κ A∈𝕌))
rel
rewrite Glu-wellfounded-≡ i<lvl = record
{ T≈ = □-[] ⊢σ ⊢T
; krip = λ {_} {δ} Ψs ⊢ΨsΔ ⊢δ → ®-mon′ A∈𝕌 Trel (r-； Ψs ⊢δ (s-≈-refl (s-； Ψs (⊢r⇒⊢s ⊢δ) ⊢ΨsΔ refl)) refl)
}
□-I′ : [] ∷⁺ Γ ⊩ t ∶ T →
Γ ⊩ box t ∶ □ T
□-I′ {_} {t} {T} ⊩t
with ⊩⇒⊢-both ⊩t
... | ⊢T , ⊢t
with ⊩t
... | record { ⊩Γ = ⊩κ ⊩Γ ; lvl = lvl ; krip = tkrip } = record { ⊩Γ = ⊩Γ ; krip = krip }
where
krip : ∀ {Δ σ ρ} →
Δ ⊢s σ ∶ ⊩Γ ® ρ →
GluExp _ Δ (box t) (□ T) σ ρ
krip {Δ} {σ} {ρ} σ∼ρ
with tkrip (σ；1∼extρ ⊩Γ σ∼ρ)
... | record { ⟦t⟧ = ⟦t⟧ ; ↘⟦T⟧ = ↘⟦T⟧ ; ↘⟦t⟧ = ↘⟦t⟧ ; T∈𝕌 = T∈𝕌 ; t∼⟦t⟧ = t∼⟦t⟧ } = record
{ ↘⟦T⟧ = ⟦□⟧ ↘⟦T⟧
; ↘⟦t⟧ = ⟦box⟧ ↘⟦t⟧
; T∈𝕌 = □ λ κ → 𝕌-mon κ T∈𝕌
; t∼⟦t⟧ = record
{ t∶T = t[σ] (□-I ⊢t) ⊢σ
; a∈El = λ m κ → record
{ ↘ua = box↘ _
; ↘ub = box↘ _
; ua≈ub = subst
(λ a → a ≈ a ∈ El _ (𝕌-mon (ins κ m) T∈𝕌))
(sym (D-ins-ins ⟦t⟧ κ m))
(El-mon T∈𝕌 (ins κ m) (𝕌-mon (ins κ m) T∈𝕌) (®El⇒∈El T∈𝕌 t∼⟦t⟧))
}
; T≈ = □-[] ⊢σ ⊢T
; krip = helper
}
}
where
⊢σ = s®⇒⊢s ⊩Γ σ∼ρ
⊢Δ = proj₁ (presup-s ⊢σ)
⊢σ；1 = s-； L.[ [] ] ⊢σ (⊢κ ⊢Δ) refl
⊢t[σ；1] = t[σ] ⊢t ⊢σ；1
⊢T[σ；1] = t[σ]-Se ⊢T ⊢σ；1
helper : ∀ {Δ′ δ} (Ψs : L.List Ctx) →
⊢ Ψs ++⁺ Δ′ →
Δ′ ⊢r δ ∶ Δ →
□Krip Ψs Δ′ (box t [ σ ]) (T [ σ ； 1 ]) δ (box ⟦t⟧)
(λ σ₁ n → _⊢_∶_®[ lvl ]_∈El (𝕌-mon (ins (mt σ₁) n) T∈𝕌))
helper {Δ′} {δ} Ψs ⊢ΨsΔ′ ⊢δ = record
{ ↘ua = box↘ _
; rel = subst
(_ ⊢ _ ∶ _ ®[ _ ]_∈El _)
(sym (D-ins-ins ⟦t⟧ (mt δ) (len Ψs)))
(®El-resp-≈
_
(®El-mon′
_
t∼⟦t⟧
(r-； Ψs ⊢δ (；-cong Ψs (s-≈-refl ⊢δ′) ⊢ΨsΔ′ refl) refl))
helper′)
}
where
⊢δ′ = ⊢r⇒⊢s ⊢δ
δ；Ψs≈ = ；-cong Ψs (s-≈-refl ⊢δ′) ⊢ΨsΔ′ refl
helper′ : Ψs ++⁺ Δ′ ⊢ t [ σ ； 1 ] [ δ ； len Ψs ] ≈ unbox (len Ψs) (box t [ σ ] [ δ ]) ∶ T [ σ ； 1 ] [ δ ； len Ψs ]
helper′
with unbox-[] L.[ [] ] (conv (t[σ] (□-I ⊢t) ⊢σ) (□-[] ⊢σ ⊢T)) (s-； Ψs ⊢δ′ ⊢ΨsΔ′ refl) refl
... | eq rewrite +-identityʳ (len Ψs) =
begin t [ σ ； 1 ] [ δ ； len Ψs ] ≈˘⟨ []-cong ([I] ⊢t[σ；1]) δ；Ψs≈ ⟩
t [ σ ； 1 ] [ I ] [ δ ； len Ψs ] ≈⟨ []-cong (≈-conv ([]-cong (≈-refl ⊢t[σ；1]) (s-≈-sym (I；1≈I ⊢Δ))) ([I] ⊢T[σ；1])) δ；Ψs≈ ⟩
t [ σ ； 1 ] [ I ； 1 ] [ δ ； len Ψs ] ≈˘⟨ []-cong (≈-conv (□-β L.[ [] ] ⊢t[σ；1] (⊢κ ⊢Δ) refl) ([I；1] ⊢T[σ；1])) δ；Ψs≈ ⟩
unbox 1 (box (t [ σ ； 1 ])) [ δ ； len Ψs ] ≈˘⟨ []-cong (≈-conv (unbox-cong L.[ [] ] (≈-conv (box-[] ⊢σ ⊢t) (□-[] ⊢σ ⊢T)) (⊢κ ⊢Δ) refl) ([I；1] ⊢T[σ；1])) δ；Ψs≈ ⟩
unbox 1 (box t [ σ ]) [ δ ； len Ψs ] ≈⟨ eq ⟩
unbox (len Ψs) (box t [ σ ] [ δ ]) ∎
where
open ER
□-E′ : ∀ {i n} Ψs →
[] ∷⁺ Γ ⊩ T ∶ Se i →
Γ ⊩ t ∶ □ T →
⊩ Ψs ++⁺ Γ →
len Ψs ≡ n →
Ψs ++⁺ Γ ⊩ unbox n t ∶ T [ I ； n ]
□-E′ {Γ = Γ@(_ ∷ _)} {T} {t} {i} {n} Ψs ⊩T ⊩t ⊩ΨsΓ refl
with ⊩T | ⊩t | ⊩⇒⊢-both ⊩t
... | record { ⊩Γ = ⊩κ ⊩Γ ; lvl = lvl ; krip = Tkrip }
| record { ⊩Γ = ⊩Γ₁ ; lvl = lvl₁ ; krip = tkrip₁ }
| ⊢□T , ⊢t = record { ⊩Γ = ⊩ΨsΓ ; krip = krip }
where
⊢T : [] ∷⁺ Γ ⊢ T ∶ Se lvl₁
⊢T = □-inv ⊢□T
⊢Γ₁ = ⊩⇒⊢ ⊩Γ₁
Ψs<ΨsΓ = subst (len Ψs <_) (sym (length-++⁺ Ψs Γ)) (m<m+n _ {len Γ} 0<1+n)
krip : ∀ {Δ σ ρ} →
Δ ⊢s σ ∶ ⊩ΨsΓ ® ρ →
GluExp _ Δ (unbox n t) (T [ I ； n ]) σ ρ
krip {Δ} {σ} {ρ} σ∼ρ
with s®⇒⊢s ⊩ΨsΓ σ∼ρ | ∥-s®′ Ψs ⊩ΨsΓ σ∼ρ | s®-resp-O _ ⊩ΨsΓ σ∼ρ Ψs<ΨsΓ
... | ⊢σ
| Ψs′ , Δ′ , refl , Ψs′≡Oσ , ⊩Γ₂ , σ∥∼ρ∥
| Oσ≡Oρ
with presup-s ⊢σ | tkrip₁ (s®-irrel ⊩Γ₂ ⊩Γ₁ σ∥∼ρ∥)
... | ⊢Δ , _
| record { ⟦T⟧ = □ ⟦T⟧ ; ⟦t⟧ = ⟦t⟧ ; ↘⟦T⟧ = ⟦□⟧ ↘⟦T⟧ ; ↘⟦t⟧ = ↘⟦t⟧ ; T∈𝕌 = □ T∈𝕌 ; t∼⟦t⟧ = t∼⟦t⟧ }
with t∼⟦t⟧
... | record { GT = GT ; t∶T = t∶T ; a∈El = a∈El ; T≈ = T≈ ; krip = □krip }
with □krip Ψs′ ⊢Δ (⊢rI (proj₁ (presup-s (s®⇒⊢s ⊩Γ₂ σ∥∼ρ∥))))
... | record { ↘ua = ↘ua ; rel = ∼ua }
rewrite D-ap-vone ⟦t⟧ = record
{ ↘⟦T⟧ = ⟦[]⟧ (⟦；⟧ ⟦I⟧) (subst (⟦ T ⟧_↘ ⟦T⟧ [ Ψs′vone ]) (trans (cong (λ n → (ext (ρ ∥ len Ψs) 1) [ ins vone n ]) Ψs′≡Oρ) (ext1-mon (ρ ∥ len Ψs) Oρ)) (⟦⟧-mon Ψs′vone ↘⟦T⟧))
; ↘⟦t⟧ = ⟦unbox⟧ (len Ψs) ↘⟦t⟧ (subst (unbox∙_, _ ↘ _) Ψs′≡Oρ ↘ua)
; t∼⟦t⟧ = ®El-resp-≈
_
(®El-resp-T≈ _ (®El-cumu _ ∼ua (m≤n⊔m _ _)) GT[I；Ψs′]≈T[I；Ψs][σ])
(subst (λ n → _ ⊢ unbox n _ ≈ _ ∶ _) (sym Ψs′≡Oσ) unbox[t[σ∥][I]]≈unbox[t][σ])
}
where
Ψs′vone = ins vone (len Ψs′)
Oσ = O σ (len Ψs)
Oρ = O ρ (len Ψs)
Ψs′≡Oρ = trans Ψs′≡Oσ Oσ≡Oρ
⊢σ∥ = ∥-⊢s″ Ψs′ Ψs ⊢σ Ψs′≡Oσ
⊢Δ′ = ⊢⇒∥⊢ Ψs′ ⊢Δ
unbox[t[σ∥][I]]≈unbox[t][σ] : Δ ⊢ unbox Oσ (t [ σ ∥ len Ψs ] [ I ]) ≈ unbox (len Ψs) t [ σ ] ∶ T [ I ； len Ψs ] [ σ ]
unbox[t[σ∥][I]]≈unbox[t][σ] =
begin unbox Oσ (t [ σ ∥ len Ψs ] [ I ]) ≈⟨ ≈-conv
(unbox-cong Ψs′ ([I] (conv (t[σ] ⊢t ⊢σ∥) (□-[] ⊢σ∥ ⊢T))) ⊢Δ Ψs′≡Oσ)
(begin
_ ≈˘⟨ subst (λ x → _ ⊢ _ [ _ ； x ] ≈ _ [ _ ； x ] ∶ _) Ψs′≡Oσ ([]-∘-；′ Ψs′ ⊢Δ ⊢T ⊢σ∥) ⟩
_ ≈⟨ []-cong-Se″ ⊢T (；-cong Ψs′ (s-≈-sym (I-∘ ⊢σ∥)) ⊢Δ Ψs′≡Oσ) ⟩
_ ≈⟨ []-；-∘ Ψs ⊢T (s-I ⊢Γ₁) ⊢σ ⟩
_ ∎) ⟩
unbox Oσ (t [ σ ∥ len Ψs ]) ≈˘⟨ ≈-conv
(unbox-[] Ψs ⊢t ⊢σ refl)
(≈-trans
([]-cong-Se″ ⊢T (；-cong Ψs′ (s-≈-sym (I-∘ ⊢σ∥)) ⊢Δ Ψs′≡Oσ))
([]-；-∘ Ψs ⊢T (s-I ⊢Γ₁) ⊢σ)) ⟩
unbox (len Ψs) t [ σ ] ∎
where
open ER
GT[I；Ψs′]≈T[σ∥；1][I；Ψs′] : Δ ⊢ GT [ I ； len Ψs′ ] ≈ T [ σ ∥ len Ψs ； 1 ] [ I ； len Ψs′ ] ∶ Se (max lvl lvl₁)
GT[I；Ψs′]≈T[σ∥；1][I；Ψs′]
with Tkrip (s®-irrel (⊩κ ⊩Γ₂) (⊩κ ⊩Γ) (s®； L.[ [] ] (⊢κ ⊢Δ′) ⊩Γ₂ σ∥∼ρ∥ refl))
... | record { ↘⟦T⟧ = ⟦Se⟧ _ ; ↘⟦t⟧ = ↘⟦T⟧₁ ; T∈𝕌 = U i<lvl _ ; t∼⟦t⟧ = T∼⟦T⟧₁ }
rewrite ⟦⟧-det ↘⟦T⟧₁ ↘⟦T⟧
| Glu-wellfounded-≡ i<lvl
with T∼⟦T⟧₁
... | record { A∈𝕌 = ⟦T⟧∈𝕌₁ ; rel = T∼⟦T⟧₁ } = ®⇒≈
_
(®-cumu _ (®El⇒® _ ∼ua) (m≤n⊔m _ _))
(®-one-sided
_
_
(®-cumu
_
(®-mon′
_
(®-cumu _ T∼⟦T⟧₁ (<⇒≤ i<lvl))
(r-； Ψs′ (⊢rI ⊢Δ′) (；-cong Ψs′ (I-≈ ⊢Δ′) ⊢Δ refl) refl))
(m≤m⊔n _ lvl₁)))
GT[I；Ψs′]≈T[I；Ψs][σ] : Δ ⊢ GT [ I ； len Ψs′ ] ≈ T [ I ； len Ψs ] [ σ ] ∶ Se (max lvl lvl₁)
GT[I；Ψs′]≈T[I；Ψs][σ] =
begin GT [ I ； len Ψs′ ] ≈⟨ GT[I；Ψs′]≈T[σ∥；1][I；Ψs′] ⟩
T [ σ ∥ len Ψs ； 1 ] [ I ； len Ψs′ ] ≈˘⟨ lift-⊢≈-Se-max′ ([]-∘-；′ Ψs′ ⊢Δ ⊢T ⊢σ∥) ⟩
T [ σ ∥ len Ψs ； len Ψs′ ] ≈˘⟨ lift-⊢≈-Se-max′ ([]-cong-Se″ ⊢T (；-cong Ψs′ (I-∘ ⊢σ∥) ⊢Δ refl)) ⟩
T [ (I ∘ σ ∥ len Ψs) ； len Ψs′ ] ≈⟨ subst (λ n → _ ⊢ _ [ _ ； n ] ≈ _ ∶ _) (sym Ψs′≡Oσ) (lift-⊢≈-Se-max′ ([]-；-∘ Ψs ⊢T (s-I ⊢Γ₁) ⊢σ)) ⟩
T [ I ； len Ψs ] [ σ ] ∎
where
open ER