open import Graded.Modality
open import Graded.Usage.Restrictions
open import Definition.Typed.EqualityRelation
import Definition.Typed
open import Definition.Typed.Restrictions
import Definition.Untyped hiding (_∷_)
open import Tools.Empty
open import Tools.Sum hiding (id)
import Tools.PropositionalEquality as PE
module Graded.Erasure.LogicalRelation.Fundamental
{a} {M : Set a}
(𝕄 : Modality M)
(open Modality 𝕄)
(TR : Type-restrictions M)
(UR : Usage-restrictions M)
(𝟘-well-behaved : Has-well-behaved-zero M semiring-with-meet)
{{eqrel : EqRelSet TR}}
where
open Definition.Untyped M
open Definition.Typed TR
open EqRelSet {{...}}
open import Definition.LogicalRelation TR
open import Definition.LogicalRelation.Properties.Escape TR
open import Definition.LogicalRelation.Substitution TR
open import Definition.LogicalRelation.Substitution.MaybeEmbed TR
open import Definition.LogicalRelation.Substitution.Properties TR
open import Definition.LogicalRelation.Substitution.Weakening TR
open import Definition.LogicalRelation.Substitution.Introductions.Pi TR
open import Definition.LogicalRelation.Substitution.Introductions.Nat TR
import Definition.LogicalRelation.Fundamental TR as F
import Definition.LogicalRelation.Irrelevance TR as I
import Definition.LogicalRelation.Substitution.Irrelevance TR as IS
open import Graded.Context 𝕄
open import Graded.Context.Properties 𝕄
open import Graded.Modality.Dedicated-star.Instance
open import Graded.Modality.Properties.PartialOrder semiring-with-meet
open import Graded.Modality.Properties.Has-well-behaved-zero
semiring-with-meet 𝟘-well-behaved
open import Graded.Usage 𝕄 UR
open import Graded.Usage.Inversion 𝕄 UR
open import Graded.Usage.Properties 𝕄 UR
open import Graded.Mode 𝕄
open import Definition.Untyped.Properties M
open import Definition.Typed.Consequences.Syntactic TR
import Graded.Erasure.LogicalRelation 𝕄 TR is-𝟘? as LR
open import Graded.Erasure.LogicalRelation.Fundamental.Assumptions 𝕄 TR UR
import Graded.Erasure.LogicalRelation.Fundamental.Application
import Graded.Erasure.LogicalRelation.Fundamental.Empty
import Graded.Erasure.LogicalRelation.Fundamental.Lambda
import Graded.Erasure.LogicalRelation.Fundamental.Nat
import Graded.Erasure.LogicalRelation.Fundamental.Natrec
import Graded.Erasure.LogicalRelation.Fundamental.Prodrec
import Graded.Erasure.LogicalRelation.Fundamental.Product
import Graded.Erasure.LogicalRelation.Fundamental.Unit
import Graded.Erasure.LogicalRelation.Conversion
import Graded.Erasure.LogicalRelation.Irrelevance
import Graded.Erasure.LogicalRelation.Subsumption
import Graded.Erasure.Target as T
open import Graded.Erasure.Extraction 𝕄 is-𝟘?
import Graded.Erasure.Target.Properties as TP
open import Tools.Fin
open import Tools.Function
open import Tools.Nat
open import Tools.Nullary
open import Tools.Product
import Tools.PropositionalEquality as PE
import Tools.Reasoning.PartialOrder
import Tools.PropositionalEquality as PE
private
variable
l n : Nat
Γ Δ : Con Term n
t u A B : Term n
γ δ : Conₘ n
p q : M
σ : Subst l n
x : Fin n
σ′ : T.Subst l n
m : Mode
module _ (⊢Δ : ⊢ Δ) where
open LR ⊢Δ
open Graded.Erasure.LogicalRelation.Conversion 𝕄 TR is-𝟘? ⊢Δ
open Graded.Erasure.LogicalRelation.Irrelevance 𝕄 TR is-𝟘? ⊢Δ
open Graded.Erasure.LogicalRelation.Subsumption 𝕄 TR is-𝟘? ⊢Δ
subsumption-≤ : ∀ {l}
→ ([Γ] : ⊩ᵛ Γ) ([A] : Γ ⊩ᵛ⟨ l ⟩ A / [Γ])
→ γ ▸ Γ ⊩ʳ⟨ l ⟩ t ∷[ m ] A / [Γ] / [A]
→ δ ≤ᶜ γ
→ δ ▸ Γ ⊩ʳ⟨ l ⟩ t ∷[ m ] A / [Γ] / [A]
subsumption-≤ {t = t} [Γ] [A] γ⊩ʳt δ≤γ =
subsumption {t = t} [Γ] [A] γ⊩ʳt λ x δx≡𝟘 → lemma x δx≡𝟘 δ≤γ
where
lemma : (x : Fin n) → δ ⟨ x ⟩ PE.≡ 𝟘 → δ ≤ᶜ γ
→ γ ⟨ x ⟩ PE.≡ 𝟘
lemma {δ = δ ∙ p} {γ ∙ q} x0 PE.refl (δ≤γ ∙ p≤q) = 𝟘≮ p≤q
lemma {δ = δ ∙ p} {γ ∙ q} (x +1) δx≡𝟘 (δ≤γ ∙ _) = lemma x δx≡𝟘 δ≤γ
fundamentalVar′ :
([Γ] : ⊩ᵛ Γ) →
x ∷ A ∈ Γ →
γ ≤ᶜ 𝟘ᶜ , x ≔ 𝟙 →
([σ] : Δ ⊩ˢ σ ∷ Γ / [Γ] / ⊢Δ) →
(σ®σ′ : σ ®⟨ ¹ ⟩ σ′ ∷[ 𝟙ᵐ ] Γ ◂ γ / [Γ] / [σ]) →
∃ λ ([A] : Γ ⊩ᵛ⟨ ¹ ⟩ A / [Γ]) →
σ x ®⟨ ¹ ⟩ σ′ x ∷ A [ σ ] / proj₁ (unwrap [A] ⊢Δ [σ])
fundamentalVar′ ε ()
fundamentalVar′ {σ = σ} (_∙_ {A = A} [Γ] [A]) here (_ ∙ p≤𝟙)
([tailσ] , [headσ]) (σ®σ′ , σ0®σ′0) =
let [A]′ = proj₁ (unwrap [A] ⊢Δ [tailσ])
[↑A] = wk1ᵛ {A = A} {F = A} [Γ] [A] [A]
[↑A]′ = maybeEmbᵛ {A = wk1 A} (_∙_ {A = A} [Γ] [A]) [↑A]
[σ↑A] = proj₁ (unwrap [↑A]′ {σ = σ} ⊢Δ ([tailσ] , [headσ]))
A≡A : Δ ⊢ A [ tail σ ] ≡ A [ tail σ ]
A≡A = refl (escape [A]′)
A≡A′ = PE.subst (Δ ⊢ A [ tail σ ] ≡_)
(PE.sym (wk1-tail A)) A≡A
σ0®σ′0′ = σ0®σ′0 ◀≢𝟘 λ 𝟙p≡𝟘 →
𝟙≢𝟘 (𝟘≮ (≤-trans (≤-reflexive (PE.trans (PE.sym 𝟙p≡𝟘) (·-identityˡ _))) p≤𝟙))
in [↑A]′ , convTermʳ [A]′ [σ↑A] A≡A′ σ0®σ′0′
fundamentalVar′ (_∙_ {A = A} [Γ] [A]) (there {A = B} x) (γ≤eᵢ ∙ _)
([tailσ] , [headσ]) (σ®σ′ , σ0®σ′0) =
let [σA] = proj₁ (unwrap [A] ⊢Δ [tailσ])
[A]′ = maybeEmbᵛ {A = A} [Γ] [A]
[B] , t®v = fundamentalVar′ [Γ] x γ≤eᵢ [tailσ] σ®σ′
[↑B] = wk1ᵛ {A = B} {F = A} [Γ] [A]′ [B]
[↑B]′ = maybeEmbᵛ {A = wk1 B} (_∙_ {A = A} [Γ] [A]′) [↑B]
[↑B]″ = IS.irrelevance {A = wk1 B} (_∙_ {A = A} [Γ] [A]′) ([Γ] ∙ [A]) [↑B]′
t®v′ = irrelevanceTerm′ (PE.sym (wk1-tail B)) (proj₁ (unwrap [B] ⊢Δ [tailσ]))
(proj₁ (unwrap [↑B]″ ⊢Δ ([tailσ] , [headσ]))) t®v
in [↑B]″ , t®v′
fundamentalVar : ([Γ] : ⊩ᵛ Γ)
→ x ∷ A ∈ Γ
→ γ ▸[ m ] var x
→ ∃ λ ([A] : Γ ⊩ᵛ⟨ ¹ ⟩ A / [Γ])
→ γ ▸ Γ ⊩ʳ⟨ ¹ ⟩ var x ∷[ m ] A / [Γ] / [A]
fundamentalVar {Γ = Γ} {x = x} {A = A} {γ = γ} {m = m} [Γ] x∷A∈Γ γ▸x =
[A] , lemma m γ▸x
where
[A] = proj₁ (F.fundamentalVar x∷A∈Γ [Γ])
lemma :
∀ m →
γ ▸[ m ] var x →
γ ▸ Γ ⊩ʳ⟨ ¹ ⟩ var x ∷[ m ] A / [Γ] / [A]
lemma 𝟘ᵐ with is-𝟘? 𝟘
... | yes 𝟘≡𝟘 = _
... | no 𝟘≢𝟘 = PE.⊥-elim (𝟘≢𝟘 PE.refl)
lemma 𝟙ᵐ γ▸x [σ] σ®σ′ with is-𝟘? 𝟙
... | yes 𝟙≡𝟘 = PE.⊥-elim (𝟙≢𝟘 𝟙≡𝟘)
... | no 𝟙≢𝟘 =
let [A]′ , t®v =
fundamentalVar′ [Γ] x∷A∈Γ (inv-usage-var γ▸x) [σ] σ®σ′
in irrelevanceTerm (proj₁ (unwrap [A]′ ⊢Δ [σ]))
(proj₁ (unwrap [A] ⊢Δ [σ])) t®v
module Fundamental (FA : Fundamental-assumptions Δ) where
open Fundamental-assumptions FA
open Graded.Erasure.LogicalRelation.Fundamental.Application
𝕄 TR 𝟘-well-behaved well-formed
open Graded.Erasure.LogicalRelation.Fundamental.Empty
𝕄 TR is-𝟘? well-formed consistent
open Graded.Erasure.LogicalRelation.Fundamental.Lambda
𝕄 TR is-𝟘? 𝟙≢𝟘 well-formed
open Graded.Erasure.LogicalRelation.Fundamental.Nat
𝕄 TR is-𝟘? well-formed
open Graded.Erasure.LogicalRelation.Fundamental.Natrec
𝕄 TR 𝟘-well-behaved well-formed
open Graded.Erasure.LogicalRelation.Fundamental.Prodrec
𝕄 TR 𝟘-well-behaved well-formed
open Graded.Erasure.LogicalRelation.Fundamental.Product
𝕄 TR UR 𝟘-well-behaved well-formed
open Graded.Erasure.LogicalRelation.Fundamental.Unit
𝕄 TR is-𝟘? well-formed
open Graded.Erasure.LogicalRelation.Conversion 𝕄 TR is-𝟘? well-formed
open Graded.Erasure.LogicalRelation.Irrelevance 𝕄 TR is-𝟘? well-formed
open Graded.Erasure.LogicalRelation.Subsumption 𝕄 TR is-𝟘? well-formed
open LR well-formed
fundamental :
Γ ⊢ t ∷ A → γ ▸[ m ] t →
∃₂ λ ([Γ] : ⊩ᵛ Γ) ([A] : Γ ⊩ᵛ⟨ ¹ ⟩ A / [Γ]) →
γ ▸ Γ ⊩ʳ⟨ ¹ ⟩ t ∷[ m ] A / [Γ] / [A]
fundamental {m = 𝟘ᵐ} ⊢t _ with is-𝟘? 𝟘
... | yes 𝟘≡𝟘 =
case F.fundamental (syntacticTerm ⊢t) of λ ([Γ] , [A]) →
[Γ] , [A] , _
... | no 𝟘≢𝟘 = PE.⊥-elim (𝟘≢𝟘 PE.refl)
fundamental Γ⊢ΠΣ@(ΠΣⱼ Γ⊢F:U _ _) γ▸t =
let invUsageΠΣ δ▸F _ _ = inv-usage-ΠΣ γ▸t
[Γ] , _ , _ = fundamental Γ⊢F:U δ▸F
[U] , ⊩ʳΠΣ = ΠΣʳ [Γ] Γ⊢ΠΣ
in [Γ] , [U] , ⊩ʳΠΣ
fundamental (ℕⱼ ⊢Γ) γ▸t = ℕʳ ⊢Γ
fundamental (Emptyⱼ ⊢Γ) γ▸t = Emptyʳ ⊢Γ
fundamental (Unitⱼ ⊢Γ ok) _ = Unitʳ ⊢Γ ok
fundamental (var ⊢Γ x∷A∈Γ) γ▸t =
let [Γ] = F.valid ⊢Γ
[A] , ⊩ʳx = fundamentalVar well-formed [Γ] x∷A∈Γ γ▸t
in [Γ] , [A] , ⊩ʳx
fundamental
(lamⱼ {F = F} {t = t} {G = G} {p = p} {q = q} Γ⊢F Γ⊢t:G ok) γ▸t =
let invUsageLam {δ = δ} δ▸t δ≤γ = inv-usage-lam γ▸t
[ΓF] , [G]′ , ⊩ʳt = fundamental Γ⊢t:G δ▸t
[Γ] , [F] = F.fundamental Γ⊢F
[G] = IS.irrelevance {A = G} [ΓF] ([Γ] ∙ [F]) [G]′
[Γ]′ , [G]″ , [t]′ = F.fundamentalTerm Γ⊢t:G
[t] = IS.irrelevanceTerm {A = G} {t = t}
[Γ]′ ([Γ] ∙ [F]) [G]″ [G] [t]′
⊩ʳt′ = irrelevance {A = G} {t = t}
[ΓF] ([Γ] ∙ [F]) [G]′ [G] ⊩ʳt
⊩ʳλt = lamʳ {t = t} [Γ] [F] [G] [t] ⊩ʳt′ ok
[Π] = Πᵛ [Γ] [F] [G] ok
in [Γ] , [Π] ,
subsumption-≤ well-formed {A = Π p , q ▷ F ▹ G} {t = lam p t}
[Γ] [Π] ⊩ʳλt δ≤γ
fundamental
(_∘ⱼ_ {t = t} {p = p} {q = q} {F = F} {G = G} {u = u} Γ⊢t:Π Γ⊢u:F)
γ▸t =
let invUsageApp δ▸t η▸u γ≤δ+pη = inv-usage-app γ▸t
[Γ]′ , [Π]′ , ⊩ʳt′ = fundamental Γ⊢t:Π δ▸t
[Γ] , [F] , ⊩ʳu = fundamental Γ⊢u:F η▸u
[Π] = IS.irrelevance {A = Π p , q ▷ F ▹ G} [Γ]′ [Γ] [Π]′
⊩ʳt = irrelevance {A = Π p , q ▷ F ▹ G} {t = t}
[Γ]′ [Γ] [Π]′ [Π] ⊩ʳt′
[Γ]″ , [F]′ , [u]′ = F.fundamentalTerm Γ⊢u:F
[u] = IS.irrelevanceTerm {A = F} {t = u}
[Γ]″ [Γ] [F]′ [F] [u]′
[G[u]] , ⊩ʳt∘u = appʳ {F = F} {G = G} {u = u} {t = t}
[Γ] [F] [Π] [u] ⊩ʳt ⊩ʳu
in [Γ] , [G[u]] ,
subsumption-≤ well-formed {A = G [ u ]₀} {t = t ∘⟨ p ⟩ u}
[Γ] [G[u]] ⊩ʳt∘u γ≤δ+pη
fundamental
(prodⱼ {F = F} {G = G} {t = t} {u = u} {k = Σₚ}
Γ⊢F Γ⊢G Γ⊢t:F Γ⊢u:G ok)
γ▸t =
let invUsageProdₚ δ▸t η▸u γ≤pδ∧η = inv-usage-prodₚ γ▸t
[Γ]₁ , [F] , ⊩ʳt = fundamental Γ⊢t:F δ▸t
[Γ]₂ , [G[t]]′ , ⊩ʳu = fundamental Γ⊢u:G η▸u
[Γ] = [Γ]₁
[Γ]₃ , [G]′ = F.fundamental Γ⊢G
[G] = IS.irrelevance {A = G} [Γ]₃ ([Γ] ∙ [F]) [G]′
[G[t]] = IS.irrelevance {A = G [ t ]₀} [Γ]₂ [Γ] [G[t]]′
[Γ]₄ , [F]₄ , [t]′ = F.fundamentalTerm Γ⊢t:F
[t] = IS.irrelevanceTerm {A = F} {t = t}
[Γ]₄ [Γ] [F]₄ [F] [t]′
[Γ]₅ , [G]₅ , [u]′ = F.fundamentalTerm Γ⊢u:G
[u] = IS.irrelevanceTerm {A = G [ t ]₀} {t = u}
[Γ]₅ [Γ] [G]₅ [G[t]] [u]′
[Σ] , ⊩ʳp =
prodʳ
{F = F} {G = G} {t = t} {u = u} {_⊕ᶜ_ = _∧ᶜ_}
[Γ] [F] [G] [G[t]] [t] [u] ⊩ʳt
(irrelevance {A = G [ t ]₀} {t = u}
[Γ]₂ [Γ] [G[t]]′ [G[t]] ⊩ʳu)
(λ {x} {γ} {δ} γ∧δ≡𝟘 →
∧-positiveˡ
(PE.trans (PE.sym (lookup-distrib-∧ᶜ γ δ x)) γ∧δ≡𝟘))
(λ {x} {γ} {δ} γ∧δ≡𝟘 →
∧-positiveʳ
(PE.trans (PE.sym (lookup-distrib-∧ᶜ γ δ x)) γ∧δ≡𝟘))
ok
in [Γ] , [Σ] ,
subsumption-≤ well-formed {t = prod! t u} [Γ] [Σ] ⊩ʳp γ≤pδ∧η
fundamental
(prodⱼ {F = F} {G = G} {t = t} {u = u} {k = Σᵣ}
Γ⊢F Γ⊢G Γ⊢t:F Γ⊢u:G ok)
γ▸t =
let invUsageProdᵣ δ▸t η▸u γ≤pδ+η = inv-usage-prodᵣ γ▸t
[Γ]₁ , [F] , ⊩ʳt = fundamental Γ⊢t:F δ▸t
[Γ]₂ , [G[t]]′ , ⊩ʳu = fundamental Γ⊢u:G η▸u
[Γ] = [Γ]₁
[Γ]₃ , [G]′ = F.fundamental Γ⊢G
[G] = IS.irrelevance {A = G} [Γ]₃ ([Γ] ∙ [F]) [G]′
[G[t]] = IS.irrelevance {A = G [ t ]₀} [Γ]₂ [Γ] [G[t]]′
[Γ]₄ , [F]₄ , [t]′ = F.fundamentalTerm Γ⊢t:F
[t] = IS.irrelevanceTerm {A = F} {t = t}
[Γ]₄ [Γ] [F]₄ [F] [t]′
[Γ]₅ , [G]₅ , [u]′ = F.fundamentalTerm Γ⊢u:G
[u] = IS.irrelevanceTerm {A = G [ t ]₀} {t = u}
[Γ]₅ [Γ] [G]₅ [G[t]] [u]′
[Σ] , ⊩ʳp =
prodʳ
{F = F} {G = G} {t = t} {u = u} {_⊕ᶜ_ = _+ᶜ_}
[Γ] [F] [G] [G[t]] [t] [u] ⊩ʳt
(irrelevance {A = G [ t ]₀} {t = u}
[Γ]₂ [Γ] [G[t]]′ [G[t]] ⊩ʳu)
(λ {x} {γ} {δ} γ∧δ≡𝟘 →
+-positiveˡ $
PE.trans (PE.sym (lookup-distrib-+ᶜ γ δ x)) γ∧δ≡𝟘)
(λ {x} {γ} {δ} γ∧δ≡𝟘 →
+-positiveʳ $
PE.trans (PE.sym (lookup-distrib-+ᶜ γ δ x)) γ∧δ≡𝟘)
ok
in [Γ] , [Σ] ,
subsumption-≤ well-formed {t = prod! t u} [Γ] [Σ] ⊩ʳp γ≤pδ+η
fundamental (fstⱼ {F = F} {t = t} Γ⊢F Γ⊢G Γ⊢t:Σ) γ▸t =
let invUsageFst m′ m≡m′ᵐ·p δ▸t γ≤δ ok = inv-usage-fst γ▸t
[Γ] , [Σ] , ⊩ʳt = fundamental Γ⊢t:Σ δ▸t
[F] , ⊩ʳt₁ =
fstʳ Γ⊢F Γ⊢G Γ⊢t:Σ [Γ] [Σ] ⊩ʳt
(fstₘ m′ (▸-cong m≡m′ᵐ·p δ▸t) (PE.sym m≡m′ᵐ·p) ok)
in [Γ] , [F] ,
subsumption-≤ well-formed {t = fst _ t} [Γ] [F] ⊩ʳt₁ γ≤δ
fundamental (sndⱼ {G = G} {t = t} Γ⊢F Γ⊢G Γ⊢t:Σ) γ▸t =
let invUsageSnd δ▸t γ≤δ = inv-usage-snd γ▸t
[Γ] , [Σ] , ⊩ʳt = fundamental Γ⊢t:Σ δ▸t
[G] , ⊩ʳt₂ = sndʳ Γ⊢F Γ⊢G Γ⊢t:Σ [Γ] [Σ] ⊩ʳt
in [Γ] , [G] ,
subsumption-≤ well-formed {t = snd _ t} [Γ] [G] ⊩ʳt₂ γ≤δ
fundamental
(prodrecⱼ {F = F} {G} {A = A} {t = t} {u} {r = r}
Γ⊢F Γ⊢G Γ⊢A Γ⊢t Γ⊢u _)
γ▸prodrec =
let invUsageProdrec {δ = δ} δ▸t η▸u _ ok γ≤pδ+η =
inv-usage-prodrec γ▸prodrec
[Γ] , [Σ] , ⊩ʳt = fundamental Γ⊢t δ▸t
[Γ]₂ , [A₊]₂ , ⊩ʳu = fundamental Γ⊢u η▸u
[Γ]₃ , [F]₃ = F.fundamental Γ⊢F
[Γ]₄ , [G]₄ = F.fundamental Γ⊢G
[Γ]₅ , [A]₅ = F.fundamental Γ⊢A
[Γ]₆ , [Σ]₆ , [t]₆ = F.fundamentalTerm Γ⊢t
[Γ]₇ , [A₊]₇ , [u]₇ = F.fundamentalTerm Γ⊢u
A₊ = A [ prodᵣ _ (var (x0 +1)) (var x0) ]↑²
[F] = IS.irrelevance {A = F} [Γ]₃ [Γ] [F]₃
[G] = IS.irrelevance {A = G} [Γ]₄ ([Γ] ∙ [F]) [G]₄
[A₊] = IS.irrelevance {A = A₊} [Γ]₂ ([Γ] ∙ [F] ∙ [G]) [A₊]₂
[A] = IS.irrelevance {A = A} [Γ]₅ ([Γ] ∙ [Σ]) [A]₅
[t] = IS.irrelevanceTerm {t = t} [Γ]₆ [Γ] [Σ]₆ [Σ] [t]₆
[u] = IS.irrelevanceTerm {A = A₊} {u}
[Γ]₇ ([Γ] ∙ [F] ∙ [G]) [A₊]₇ [A₊] [u]₇
⊩ʳu′ = irrelevance {t = u}
[Γ]₂ ([Γ] ∙ [F] ∙ [G]) [A₊]₂ [A₊] ⊩ʳu
r≡𝟘→k≡0 = case closed-or-no-erased-matches of λ where
(inj₁ nem) → λ r≡𝟘 → PE.⊥-elim (nem 𝟙≢𝟘 ok r≡𝟘)
(inj₂ k≡0) → λ _ → k≡0
[At] , ⊩ʳprodrec =
prodrecʳ
[Γ] [F] [G] [Σ] [A] [A₊] [t] [u]
(λ r≢𝟘 →
PE.subst (δ ▸ _ ⊩ʳ⟨ _ ⟩ t ∷[_] _ / _ / [Σ])
(≢𝟘→ᵐ·≡ r≢𝟘) ⊩ʳt)
⊩ʳu′ r≡𝟘→k≡0
in [Γ] , [At] ,
subsumption-≤ well-formed {t = prodrec _ _ _ A t u}
[Γ] [At] ⊩ʳprodrec γ≤pδ+η
fundamental (zeroⱼ ⊢Γ) γ▸t = zeroʳ ⊢Γ
fundamental (sucⱼ {n = t} Γ⊢t:ℕ) γ▸t =
let invUsageSuc δ▸t γ≤δ = inv-usage-suc γ▸t
[Γ] , [ℕ] , ⊩ʳt = fundamental Γ⊢t:ℕ δ▸t
δ⊩ʳsuct = sucʳ [Γ] [ℕ] ⊩ʳt Γ⊢t:ℕ
γ⊩ʳsuct =
subsumption-≤ well-formed {A = ℕ} {t = suc t}
[Γ] [ℕ] δ⊩ʳsuct γ≤δ
in [Γ] , [ℕ] , γ⊩ʳsuct
fundamental
(natrecⱼ {A = A} {z = z} {s = s} {p = p} {q = q} {r = r} {n = n}
Γ⊢A Γ⊢z:A Γ⊢s:A Γ⊢n:ℕ)
γ▸t =
case inv-usage-natrec γ▸t of λ {
(invUsageNatrec {δ = δ} δ▸z η▸s θ▸n _ γ≤γ′ extra) →
let [Γ] , [A₀] , ⊩ʳz = fundamental Γ⊢z:A δ▸z
[ΓℕA] , [A₊]′ , ⊩ʳs′ = fundamental Γ⊢s:A η▸s
[Γ]′ , [ℕ]′ , ⊩ʳn′ = fundamental Γ⊢n:ℕ θ▸n
[ℕ] = ℕᵛ {l = ¹} [Γ]
[Γℕ] = [Γ] ∙ [ℕ]
[Γℕ]′ , [A]′ = F.fundamental Γ⊢A
[A] = IS.irrelevance {A = A} [Γℕ]′ [Γℕ] [A]′
[A₊] = IS.irrelevance {A = A [ suc (var x1) ]↑²}
[ΓℕA] ([Γℕ] ∙ [A]) [A₊]′
[Γ]ᶻ , [A]ᶻ , [z]′ = F.fundamentalTerm Γ⊢z:A
[z] = IS.irrelevanceTerm {A = A [ zero ]₀} {t = z}
[Γ]ᶻ [Γ] [A]ᶻ [A₀] [z]′
[Γ]ˢ , [A]ˢ , [s]′ = F.fundamentalTerm Γ⊢s:A
[s] = IS.irrelevanceTerm
{A = A [ suc (var x1) ]↑²} {t = s}
[Γ]ˢ ([Γℕ] ∙ [A]) [A]ˢ [A₊] [s]′
[Γ]ⁿ , [ℕ]ⁿ , [n]′ = F.fundamentalTerm Γ⊢n:ℕ
[n] = IS.irrelevanceTerm {A = ℕ} {t = n}
[Γ]ⁿ [Γ] [ℕ]ⁿ [ℕ] [n]′
⊩ʳs = irrelevance
{A = A [ suc (var x1) ]↑²} {t = s}
[ΓℕA] ([Γℕ] ∙ [A]) [A₊]′ [A₊] ⊩ʳs′
⊩ʳn = irrelevance {A = ℕ} {t = n} [Γ]′ [Γ] [ℕ]′ [ℕ] ⊩ʳn′
[A[n]] , ⊩ʳnatrec =
natrecʳ {A = A} {z = z} {s = s} {m = n}
[Γ] [A] [A₊] [A₀] [z] [s] [n] ⊩ʳz ⊩ʳs ⊩ʳn
(case extra of λ where
invUsageNatrecStar → ⟨⟩≡𝟘→⟨⟩≡𝟘-⊛ 𝟘-well-behaved δ
(invUsageNatrecNoStar fix) →
⟨⟩≡𝟘→⟨⟩≡𝟘-fixpoint 𝟘-well-behaved fix)
in [Γ] , [A[n]] ,
λ {_ _} →
subsumption-≤ well-formed
{A = A [ n ]₀} {t = natrec p q r A z s n}
[Γ] [A[n]] ⊩ʳnatrec γ≤γ′ }
fundamental
{Γ = Γ} {γ = γ}
(emptyrecⱼ {A = A} {t = t} {p = p} ⊢A Γ⊢t:Empty) γ▸t =
let invUsageemptyrec δ▸t _ γ≤δ = inv-usage-emptyrec γ▸t
[Γ] , [Empty] , ⊩ʳt = fundamental Γ⊢t:Empty δ▸t
[Γ]′ , [A]′ = F.fundamental ⊢A
[A] = IS.irrelevance {A = A} [Γ]′ [Γ] [A]′
[Γ]″ , [Empty]′ , [t]′ = F.fundamentalTerm Γ⊢t:Empty
[t] = IS.irrelevanceTerm {A = Empty} {t = t}
[Γ]″ [Γ] [Empty]′ [Empty] [t]′
γ⊩ʳemptyrec = emptyrecʳ {A = A} {t = t} {p = p}
[Γ] [Empty] [A] [t]
in [Γ] , [A] , γ⊩ʳemptyrec
fundamental (starⱼ ⊢Γ ok) _ = starʳ ⊢Γ ok
fundamental (conv {t = t} {A = A} {B = B} Γ⊢t:A A≡B) γ▸t =
let [Γ] , [A] , ⊩ʳt = fundamental Γ⊢t:A γ▸t
Γ⊢B = syntacticTerm (conv Γ⊢t:A A≡B)
[Γ]′ , [B]′ = F.fundamental Γ⊢B
[B] = IS.irrelevance {A = B} [Γ]′ [Γ] [B]′
in [Γ] , [B] ,
convʳ {A = A} {B = B} {t = t} [Γ] [A] [B] A≡B ⊩ʳt
fundamentalErased :
Δ ⊢ t ∷ A → 𝟘ᶜ ▸[ m ] t →
∃ λ ([A] : Δ ⊩⟨ ¹ ⟩ A) → t ®⟨ ¹ ⟩ erase t ∷ A ◂ ⌜ m ⌝ / [A]
fundamentalErased {t = t} {A = A} {m = m} ⊢t 𝟘▸t =
[A]′ , lemma m ⊩ʳt
where
[Δ]-[A]-⊩ʳt = fundamental ⊢t 𝟘▸t
[Δ] = [Δ]-[A]-⊩ʳt .proj₁
[A] = [Δ]-[A]-⊩ʳt .proj₂ .proj₁
⊩ʳt = [Δ]-[A]-⊩ʳt .proj₂ .proj₂
[id]′ = idSubstS [Δ]
⊢Δ′ = soundContext [Δ]
[id] = IS.irrelevanceSubst [Δ] [Δ] ⊢Δ′ well-formed [id]′
[idA] = proj₁ (unwrap [A] {σ = idSubst} well-formed [id])
[A]′ = I.irrelevance′ (subst-id A) [idA]
lemma :
∀ m →
𝟘ᶜ ▸ Δ ⊩ʳ⟨ ¹ ⟩ t ∷[ m ] A / [Δ] / [A] →
t ®⟨ ¹ ⟩ erase t ∷ A ◂ ⌜ m ⌝ / [A]′
lemma 𝟘ᵐ with is-𝟘? 𝟘
... | yes 𝟘≡𝟘 = _
... | no 𝟘≢𝟘 = PE.⊥-elim (𝟘≢𝟘 PE.refl)
lemma 𝟙ᵐ ⊩ʳt with is-𝟘? 𝟙
... | yes 𝟙≡𝟘 = ⊥-elim (𝟙≢𝟘 𝟙≡𝟘)
... | no 𝟙≢𝟘 =
PE.subst₂ (λ x y → x ®⟨ ¹ ⟩ y ∷ A / [A]′)
(subst-id t) (TP.subst-id (erase t)) t®t″
where
id®id′ = erasedSubst {l = ¹} {σ′ = T.idSubst} [Δ] [id]
t®t′ = ⊩ʳt [id] id®id′
t®t″ = irrelevanceTerm′ (subst-id A) [idA] [A]′ t®t′