open import Definition.Typed.EqualityRelation
import Definition.Typed
open import Definition.Typed.Restrictions
import Definition.Untyped
open import Graded.Modality
open import Tools.Nullary
import Tools.PropositionalEquality as PE
module Graded.Erasure.LogicalRelation.Conversion
{a} {M : Set a}
(open Definition.Untyped M)
(𝕄 : Modality M)
(open Modality 𝕄)
(R : Type-restrictions M)
(open Definition.Typed R)
(is-𝟘? : (p : M) → Dec (p PE.≡ 𝟘))
{{eqrel : EqRelSet R}}
{k} {Δ : Con Term k} (⊢Δ : ⊢ Δ)
where
open EqRelSet {{...}}
open import Graded.Erasure.LogicalRelation 𝕄 R is-𝟘? ⊢Δ
import Graded.Erasure.Target as T
open import Definition.LogicalRelation R
open import Definition.LogicalRelation.Irrelevance R
open import Definition.LogicalRelation.Fundamental.Reducibility R
open import Definition.LogicalRelation.ShapeView R
open import Definition.LogicalRelation.Properties.Conversion R
open import Definition.LogicalRelation.Properties.Escape R
open import Definition.LogicalRelation.Substitution R
open import Definition.LogicalRelation.Substitution.Properties R
import Definition.LogicalRelation.Substitution.Irrelevance R as IS
open import Graded.Mode 𝕄
open import Definition.Untyped.Properties M
open import Definition.Typed.Consequences.Injectivity R
open import Definition.Typed.Consequences.Substitution R
open import Definition.Typed.Reduction R
open import Definition.Typed.RedSteps R
open import Definition.Typed.Weakening R hiding (wk)
open import Tools.Level
open import Tools.Nat
open import Tools.Product
open import Tools.Unit
private
variable
n : Nat
Γ : Con Term n
A B t : Term n
v : T.Term n
p : M
m : Mode
convTermʳ′ : ∀ {l l′}
→ ([A] : Δ ⊩⟨ l ⟩ A)
([B] : Δ ⊩⟨ l′ ⟩ B)
→ Δ ⊢ A ≡ B
→ ShapeView Δ l l′ A B [A] [B]
→ t ®⟨ l ⟩ v ∷ A / [A]
→ t ®⟨ l′ ⟩ v ∷ B / [B]
convTermʳ′ _ _ A≡B (Uᵥ UA UB) t®v = t®v
convTermʳ′ _ _ A≡B (ℕᵥ ℕA ℕB) t®v = t®v
convTermʳ′ _ _ A≡B (Unitᵥ UnitA UnitB) t®v = t®v
convTermʳ′
[A] [B] A≡B
(Bᵥ (BΠ p q) (Bᵣ F G [ _ , _ , A⇒Π ] ⊢F ⊢G A≡A [F] [G] G-ext _)
(Bᵣ F₁ G₁ [ _ , _ , B⇒Π₁ ] ⊢F₁ ⊢G₁ A≡A₁ [F]₁ [G]₁ G-ext₁ _))
t®v
with is-𝟘? p
... | yes PE.refl = λ [a]′ →
let Π≡Π₁ = reduction′ A⇒Π B⇒Π₁ ΠΣₙ ΠΣₙ A≡B
F≡F₁ , G≡G₁ , _ , _ = injectivity Π≡Π₁
[F₁]′ , [F]′ , [F₁≡F]′ = reducibleEq (sym F≡F₁)
[F₁≡F] = irrelevanceEq″ (PE.sym (wk-id F₁)) (PE.sym (wk-id F))
[F₁]′ ([F]₁ id ⊢Δ) [F₁≡F]′
[a] = convTerm₁ ([F]₁ id ⊢Δ) ([F] id ⊢Δ) [F₁≡F] [a]′
G≡G₁′ = wkEq (lift id) (⊢Δ ∙ escape ([F] id ⊢Δ)) G≡G₁
G[a]≡G₁[a] = substTypeEq G≡G₁′ (refl (escapeTerm ([F] id ⊢Δ) [a]))
[Ga]′ , [G₁a]′ , [Ga≡G₁a]′ = reducibleEq G[a]≡G₁[a]
[Ga≡G₁a] = irrelevanceEq [Ga]′ ([G] id ⊢Δ [a]) [Ga≡G₁a]′
t®v′ = t®v [a]
SV = goodCases ([G] id ⊢Δ [a]) ([G]₁ id ⊢Δ [a]′) [Ga≡G₁a]
in convTermʳ′ ([G] id ⊢Δ [a]) ([G]₁ id ⊢Δ [a]′) G[a]≡G₁[a] SV t®v′
... | no p≢𝟘 = λ [a]′ a®w′ →
let Π≡Π₁ = reduction′ A⇒Π B⇒Π₁ ΠΣₙ ΠΣₙ A≡B
F≡F₁ , G≡G₁ , _ , _ = injectivity Π≡Π₁
[F₁]′ , [F]′ , [F₁≡F]′ = reducibleEq (sym F≡F₁)
[F₁≡F] = irrelevanceEq″ (PE.sym (wk-id F₁)) (PE.sym (wk-id F))
[F₁]′ ([F]₁ id ⊢Δ) [F₁≡F]′
[a] = convTerm₁ ([F]₁ id ⊢Δ) ([F] id ⊢Δ) [F₁≡F] [a]′
G≡G₁′ = wkEq (lift id) (⊢Δ ∙ escape ([F] id ⊢Δ)) G≡G₁
G[a]≡G₁[a] = substTypeEq G≡G₁′ (refl (escapeTerm ([F] id ⊢Δ) [a]))
[Ga]′ , [G₁a]′ , [Ga≡G₁a]′ = reducibleEq G[a]≡G₁[a]
[Ga≡G₁a] = irrelevanceEq [Ga]′ ([G] id ⊢Δ [a]) [Ga≡G₁a]′
SV = goodCases ([F]₁ id ⊢Δ) ([F] id ⊢Δ) [F₁≡F]
F₁≡F = PE.subst₂ (Δ ⊢_≡_) (PE.sym (wk-id F₁)) (PE.sym (wk-id F)) (sym F≡F₁)
a®w = convTermʳ′ ([F]₁ id ⊢Δ) ([F] id ⊢Δ) F₁≡F SV a®w′
t®v′ = t®v [a] a®w
SV′ = goodCases ([G] id ⊢Δ [a]) ([G]₁ id ⊢Δ [a]′) [Ga≡G₁a]
in convTermʳ′ ([G] id ⊢Δ [a]) ([G]₁ id ⊢Δ [a]′) G[a]≡G₁[a] SV′ t®v′
convTermʳ′ {v = v}
[A] [B] A≡B
(Bᵥ (BΣ _ p _) (Bᵣ F G [ _ , _ , A⇒Σ ] ⊢F ⊢G A≡A [F] [G] G-ext _)
(Bᵣ F₁ G₁ [ _ , _ , B⇒Σ₁ ] ⊢F₁ ⊢G₁ A≡A₁ [F]₁ [G]₁ G-ext₁ _))
(t₁ , t₂ , t⇒t′ , [t₁] , v₂ , t₂®v₂ , extra) =
let Σ≡Σ₁ = reduction′ A⇒Σ B⇒Σ₁ ΠΣₙ ΠΣₙ A≡B
F≡F₁ , G≡G₁ , _ = Σ-injectivity Σ≡Σ₁
[F]′ = [F] id ⊢Δ
[F]₁′ = [F]₁ id ⊢Δ
[F]″ , [F₁]″ , [F≡F₁]′ = reducibleEq F≡F₁
[F≡F₁] = irrelevanceEq″ (PE.sym (wk-id F)) (PE.sym (wk-id F₁))
[F]″ [F]′ [F≡F₁]′
F≡F₁′ = PE.subst₂ (Δ ⊢_≡_) (PE.sym (wk-id F)) (PE.sym (wk-id F₁)) F≡F₁
[t₁]′ = convTerm₁ [F]′ [F]₁′ [F≡F₁] [t₁]
G≡G₁′ = wkEq (lift id) (⊢Δ ∙ escape [F]′) G≡G₁
G[t₁]≡G₁[t₁] = substTypeEq G≡G₁′ (refl (escapeTerm [F]′ [t₁]))
[Gt₁] = [G] id ⊢Δ [t₁]
[Gt₁]₁ = [G]₁ id ⊢Δ [t₁]′
[Gt₁]′ , [G₁t₁]′ , [Gt₁≡G₁t₁]′ = reducibleEq G[t₁]≡G₁[t₁]
[Gt₁≡G₁t₁] = irrelevanceEq [Gt₁]′ [Gt₁] [Gt₁≡G₁t₁]′
t⇒t″ = conv* t⇒t′ Σ≡Σ₁
SV₂ = goodCases [Gt₁] [Gt₁]₁ [Gt₁≡G₁t₁]
t₂®v₂′ = convTermʳ′ [Gt₁] [Gt₁]₁ G[t₁]≡G₁[t₁] SV₂ t₂®v₂
SV₁ = goodCases [F]′ [F]₁′ [F≡F₁]
extra′ =
Σ-®-elim (λ _ → Σ-® _ _ [F]₁′ t₁ v v₂ p) extra
Σ-®-intro-𝟘
λ v₁ v⇒p t₁®v₁ →
let t₁®v₁′ = convTermʳ′ [F]′ [F]₁′ F≡F₁′ SV₁ t₁®v₁
in Σ-®-intro-ω v₁ v⇒p t₁®v₁′
in t₁ , t₂ , t⇒t″ , [t₁]′ , v₂ , t₂®v₂′ , extra′
convTermʳ′ (emb 0<1 [A]) [B] A≡B (emb⁰¹ SV) t®v =
convTermʳ′ [A] [B] A≡B SV t®v
convTermʳ′ [A] (emb 0<1 [B]) A≡B (emb¹⁰ SV) t®v =
convTermʳ′ [A] [B] A≡B SV t®v
convTermʳ′ _ _ _ (Emptyᵥ _ _) ()
convTermʳ′ _ _ _ (ne _ _) ()
convTermʳ : ∀ {l l′ A B t v}
→ ([A] : Δ ⊩⟨ l ⟩ A)
([B] : Δ ⊩⟨ l′ ⟩ B)
→ Δ ⊢ A ≡ B
→ t ®⟨ l ⟩ v ∷ A / [A]
→ t ®⟨ l′ ⟩ v ∷ B / [B]
convTermʳ [A] [B] A≡B t®v =
let [A]′ , [B]′ , [A≡B]′ = reducibleEq A≡B
[A≡B] = irrelevanceEq [A]′ [A] [A≡B]′
in convTermʳ′ [A] [B] A≡B (goodCases [A] [B] [A≡B]) t®v
convTermQuantʳ : ∀ {l l′ A B t v} p
→ ([A] : Δ ⊩⟨ l ⟩ A)
([B] : Δ ⊩⟨ l′ ⟩ B)
→ Δ ⊢ A ≡ B
→ t ®⟨ l ⟩ v ∷ A ◂ p / [A]
→ t ®⟨ l′ ⟩ v ∷ B ◂ p / [B]
convTermQuantʳ p [A] [B] A≡B t®v with is-𝟘? p
... | yes PE.refl = lift tt
... | no p≢𝟘 = convTermʳ [A] [B] A≡B t®v
convʳ : ∀ {l l′ A B t γ}
→ ([Γ] : ⊩ᵛ Γ)
([A] : Γ ⊩ᵛ⟨ l ⟩ A / [Γ])
([B] : Γ ⊩ᵛ⟨ l′ ⟩ B / [Γ])
(A≡B : Γ ⊢ A ≡ B)
(⊩ʳt : γ ▸ Γ ⊩ʳ⟨ l ⟩ t ∷[ m ] A / [Γ] / [A])
→ (γ ▸ Γ ⊩ʳ⟨ l′ ⟩ t ∷[ m ] B / [Γ] / [B])
convʳ {m = m} {A = A} {B = B} [Γ] [A] [B] A≡B ⊩ʳt [σ] σ®σ′ =
let t®v = ⊩ʳt [σ] σ®σ′
[σA] = proj₁ (unwrap [A] ⊢Δ [σ])
[σB] = proj₁ (unwrap [B] ⊢Δ [σ])
σA≡σB = substitutionEq A≡B (wellformedSubstEq [Γ] ⊢Δ [σ] (reflSubst [Γ] ⊢Δ [σ])) ⊢Δ
in convTermQuantʳ ⌜ m ⌝ [σA] [σB] σA≡σB t®v