{-# OPTIONS --without-K --safe #-}

open import Level
open import Axiom.Extensionality.Propositional

-- Some consequences of fundamental theorems of completeness and soundness
module Cumulative.Consequences (fext : Extensionality 0ℓ (suc 0ℓ)) where

open import Lib

open import Cumulative.Statics.Properties
open import Cumulative.Semantics.PER
open import Cumulative.Semantics.Readback
open import Cumulative.Semantics.Properties.PER fext
open import Cumulative.Semantics.Realizability fext
open import Cumulative.Completeness fext
open import Cumulative.Completeness.LogRel
open import Cumulative.Completeness.Fundamental fext
open import Cumulative.Completeness.Consequences fext
open import Cumulative.Soundness fext
open import Cumulative.Soundness.LogRel
open import Cumulative.Soundness.Properties.LogRel fext
open import Cumulative.Soundness.Properties.Substitutions fext
open import Cumulative.Soundness.Cumulativity fext
open import Cumulative.Soundness.Realizability fext
open import Cumulative.Soundness.Fundamental fext



-- Equivalence of Π types is injective.
Π-≈-inj :  {i} 
          Γ  Π S T  Π S′ T′  Se i 
          Γ  S  S′  Se i × S  Γ  T  T′  Se i
Π-≈-inj {Γ} {S} {T} {S′} {T′} {i} Π≈
  with ⊢Γ , ⊢ΠST , ⊢ΠS′T′ , _presup-≈ Π≈
    with ⊢S  , ⊢TΠ-inv ⊢ΠST
       | ⊢S′ , ⊢T′Π-inv ⊢ΠS′T′
      with ⊨Γ , _ , relfundamental-t≈t′ Π≈
         | ⊨SΓ₁@(∷-cong ⊨Γ₁ Srel₁) , _ , rel₁fundamental-⊢t ⊢T
         | record { ⊩Γ = ⊩Γ ; krip = Skrip }fundamental-⊢t⇒⊩t ⊢S
         | record { ⊩Γ = ⊩Γ₁ ; krip = S′krip }fundamental-⊢t⇒⊩t ⊢S′
        with ρ′ , _ , ρ′init , ρ′init₁ , ρ′∈InitEnvs-related ⊨SΓ₁
          rewrite InitEnvs-det ρ′init₁ ρ′init
            with s-∷ {ρ = ρ} {A = A} ρinit S↘ρ′init
               | ρ∈ , s∈ρ′∈
            with rel (⊨-irrel ⊨Γ₁ ⊨Γ ρ∈)
               | Skrip (InitEnvs⇒s®I ⊩Γ ρinit)
               | S′krip (InitEnvs⇒s®I ⊩Γ₁ ρinit)
...            | record { ↘⟦T⟧ = ⟦Se⟧ _ ; T≈T′ = U i< _ }
               , record { ⟦t⟧ = Π ⟦S⟧ _ _ ; ⟦t′⟧ = Π ⟦S′⟧ _ _ ; ↘⟦t⟧ = ⟦Π⟧ ↘⟦S⟧ ; ↘⟦t′⟧ = ⟦Π⟧ ↘⟦S′⟧ ; t≈t′ = ΠST≈ΠS′T′ }
               | record { ↘⟦T⟧ = ⟦Se⟧ _ ; ↘⟦t⟧ = ↘⟦S⟧′ ; T∈𝕌 = U i<′ _ ; t∼⟦t⟧ = S∼⟦S⟧ }
               | record { ↘⟦T⟧ = ⟦Se⟧ _ ; ↘⟦t⟧ = ↘⟦S′⟧′ ; T∈𝕌 = U i<′₁ _ ; t∼⟦t⟧ = S′∼⟦S′⟧ }
              rewrite 𝕌-wellfounded-≡-𝕌 _ i<
                    | Glu-wellfounded-≡ i<′
                    | Glu-wellfounded-≡ i<′₁
                    | ⟦⟧-det ↘⟦S⟧′ ↘⟦S⟧
                    | ⟦⟧-det ↘⟦S′⟧′ ↘⟦S′⟧
                with Π S≈S′ TrelΠST≈ΠS′T′
                   | record { A∈𝕌 = S∈𝕌 ; rel = Srel }S∼⟦S⟧
                   | record { A∈𝕌 = S′∈𝕌 ; rel = S′rel }S′∼⟦S′⟧
                   with S≈S′′≈-sym ([I]-≈ˡ-Se (≈-sym ([I]-≈ˡ-Se (®⇒≈ S′∈𝕌 (®-transport S∈𝕌 S′∈𝕌 S≈S′ Srel) S′rel)))) = S≈S′′ , T≈T′-helper
  where
    s∈₁ : l′ A (len Γ) ∈′ El _ S≈S′
    s∈₁
      with record { ↘⟦T⟧ = ↘⟦S⟧₁ ; ↘⟦T′⟧ = ↘⟦S′⟧₁ ; T≈T′ = S≈S′₁ }Srel₁ ρ∈
        rewrite ⟦⟧-det ↘⟦S⟧₁ ↘⟦S⟧ = El-one-sided S≈S′₁ S≈S′ s∈

    T≈T′-helper : S  Γ  T  T′  Se i
    T≈T′-helper
      with record { ⊩Γ = ⊩SΓ ; krip = Tkrip }fundamental-⊢t⇒⊩t ⊢T
         | record { ⊩Γ = ⊩SΓ₁ ; krip = T′krip }fundamental-⊢t⇒⊩t (ctxeq-tm (∷-cong (⊢≈-refl ⊢Γ) (≈-sym S≈S′′)) ⊢T′)
        with record { ↘⟦T⟧ = ↘⟦T⟧ ; ↘⟦T′⟧ = ↘⟦T′⟧ ; T≈T′ = T≈T′ }Trel s∈₁
           | record { ↘⟦T⟧ = ⟦Se⟧ _ ; ↘⟦t⟧ = ↘⟦T⟧′ ; T∈𝕌 = U i<′ _ ; t∼⟦t⟧ = T∼⟦T⟧ }Tkrip (InitEnvs⇒s®I ⊩SΓ ρ′init)
           | record { ↘⟦T⟧ = ⟦Se⟧ _ ; ↘⟦t⟧ = ↘⟦T′⟧′ ; T∈𝕌 = U i<′₁ _ ; t∼⟦t⟧ = T′∼⟦T′⟧ }T′krip (InitEnvs⇒s®I ⊩SΓ₁ ρ′init)
          rewrite Glu-wellfounded-≡ i<′
                | Glu-wellfounded-≡ i<′₁
                | ⟦⟧-det ↘⟦T⟧′ ↘⟦T⟧
                | ⟦⟧-det ↘⟦T′⟧′ ↘⟦T′⟧
            with record { A∈𝕌 = T∈𝕌 ; rel = Trel }T∼⟦T⟧
               | record { A∈𝕌 = T′∈𝕌 ; rel = T′rel }T′∼⟦T′⟧ = ≈-sym ([I]-≈ˡ-Se (≈-sym ([I]-≈ˡ-Se (®⇒≈ T′∈𝕌 (®-transport T∈𝕌 T′∈𝕌 T≈T′ Trel) T′rel))))


-- If two types are equivalent and well-formed in another level, then they are
-- equivalent in that level.
adjust-Se-lvl :  {i j} 
                Γ  T  T′  Se i 
                Γ  T  Se j 
                Γ  T′  Se j 
                Γ  T  T′  Se j
adjust-Se-lvl T≈T′ ⊢T ⊢T′
  with completeness T≈T′ | soundness ⊢T | soundness ⊢T′
...  | _
     , record { init = init₁ ; nbe = record { ⟦T⟧ = .(U _) ; ↘⟦t⟧ = ↘⟦T⟧ ; ↘⟦T⟧ = ⟦Se⟧ _ ; ↓⟦t⟧ = RU ._ ↘w } }
     , record { init = init₂ ; nbe = record { ⟦T⟧ = .(U _) ; ↘⟦t⟧ = ↘⟦T′⟧ ; ↘⟦T⟧ = ⟦Se⟧ _ ; ↓⟦t⟧ = RU ._ ↘w′ } }
     | _ , record { init = init₃ ; nbe = record { ⟦T⟧ = .(U _) ; ↘⟦t⟧ = ↘⟦T⟧₁ ; ↘⟦T⟧ = ⟦Se⟧ _ ; ↓⟦t⟧ = RU ._ ↘w₁ } } , T≈w
     | _ , record { init = init ; nbe = record { ⟦T⟧ = .(U _) ; ↘⟦t⟧ = ↘⟦T′⟧₁ ; ↘⟦T⟧ = ⟦Se⟧ _ ; ↓⟦t⟧ = RU ._ ↘w′₁ } } , T′≈w
     rewrite InitEnvs-det init₁ init
           | InitEnvs-det init₂ init
           | InitEnvs-det init₃ init
           | ⟦⟧-det ↘⟦T⟧₁ ↘⟦T⟧
           | ⟦⟧-det ↘⟦T′⟧₁ ↘⟦T′⟧
           | Rty-det ↘w₁ ↘w
           | Rty-det ↘w′₁ ↘w′ = ≈-trans T≈w (≈-sym T′≈w)


-----------------------
-- canonical form of N

data IsND : D  Set where
  ze : IsND ze
  su : IsND a  IsND (su a)


data IsN : Nf  Set where
  ze : IsN ze
  su : IsN w  IsN (su w)


closed-®Nat : []  t ∶N® a ∈Nat 
              IsND a
closed-®Nat (ze _)      = ze
closed-®Nat (su _ t∼a)  = su (closed-®Nat t∼a)
closed-®Nat (ne c∈ rel)
  with ≈urel (⊢wI ⊢[])
    with _ , _ , ⊢u , _presup-≈ ≈u = ⊥-elim (no-closed-Ne ⊢u)


closed-NbE-N : []  t  N 
               NbE [] t N w 
               IsN w
closed-NbE-N ⊢t record { envs = envs ; nbe = record { ↘⟦t⟧ = ↘⟦t⟧ ; ↘⟦T⟧ = ⟦N⟧ ; ↓⟦t⟧ = ↓⟦t⟧ } }
  with record { ⊩Γ = ⊩[] ; krip = krip }fundamental-⊢t⇒⊩t ⊢t
    with record { ↘⟦T⟧ = ⟦N⟧ ; ↘⟦t⟧ = ↘⟦t⟧′ ; T∈𝕌 = N ; t∼⟦t⟧ = t∼⟦t⟧ , _ }krip {ρ = envs} (s-I ⊢[])
      rewrite ⟦⟧-det ↘⟦t⟧′ ↘⟦t⟧ = helper (closed-®Nat t∼⟦t⟧) ↓⟦t⟧
  where helper : IsND a  Rf 0 -  N a  w  IsN w
        helper ze     (Rze .0)    = ze
        helper (su a) (Rsu .0 ↘w) = su (helper a ↘w)


canonicity-N : []  t  N 
                λ w  []  t  Nf⇒Exp w  N × IsN w
canonicity-N ⊢t
  with w , nbe , ≈wsoundness ⊢t = w , ≈w , closed-NbE-N ⊢t nbe

no-neutral-Se-gen :  {i j} 
                    t  Ne⇒Exp u 
                    Γ  t  T 
                    Γ  Se i  [] 
                    Γ  T  T′  Se j 
                    T′  v 0  N  Π S S′  [] 
                    ----------------
                    
no-neutral-Se-gen {_} {v .0} {j = j} refl (vlookup ⊢Γ here) refl T≈ T′∈ = not-Se-≈-bundle (s≤s z≤n) (≈-trans (lift-⊢≈-Se-max {j = j} (≈-sym (Se-[] _ (s-wk ⊢Γ)))) (lift-⊢≈-Se-max′ T≈)) T′∈
no-neutral-Se-gen {_} {rec T z s u} refl (N-E _ _ _ ⊢t) eq T≈ T′∈       = no-neutral-Se-gen {S = N} {S′ = N} refl ⊢t eq (≈-refl (N-wf 0 (proj₁ (presup-tm ⊢t)))) (there (here refl))
no-neutral-Se-gen {_} {u $ n} refl (Λ-E ⊢t _) eq T≈ T′∈                 = no-neutral-Se-gen refl ⊢t eq (≈-refl (proj₂ (proj₂ (presup-tm ⊢t)))) (there (there (here refl)))
no-neutral-Se-gen {_} {_} refl (cumu ⊢t) refl T≈ T′∈                    = not-Se-≈-bundle (s≤s z≤n) T≈ T′∈
no-neutral-Se-gen {_} {_} refl (conv ⊢t ≈T) eq T≈ T′∈                   = no-neutral-Se-gen refl ⊢t eq (≈-trans (lift-⊢≈-Se-max ≈T) (lift-⊢≈-Se-max′ T≈)) T′∈

no-neutral-Se :  {i} 
                Se i  []  Ne⇒Exp u  v 0 
                ----------------
                
no-neutral-Se ⊢u = no-neutral-Se-gen {S = N} {S′ = N} refl ⊢u refl (≈-refl (conv (vlookup (⊢∷ ⊢[] (Se-wf _ ⊢[])) here) (Se-[] _ (s-wk (⊢∷ ⊢[] (Se-wf _ ⊢[])))))) (here refl)


consistency :  {i}  []  t  Π (Se i) (v 0)  
consistency {_} {i} ⊢t
  with fundamental-⊢t⇒⊩t ⊢t
... | record { ⊩Γ = ⊩[] ; lvl = lvl ; krip = krip }
    with krip {ρ = emp} (s-I ⊢[])
...    | record { ↘⟦T⟧ = ⟦Π⟧ (⟦Se⟧ ._) ; T∈𝕌 = T∈𝕌@(Π iA@(U 0<l _) RT) ; t∼⟦t⟧ = t∼⟦t⟧@record { IT = IT ; OT = OT ; ⊢OT = ⊢OT ; T≈ = T≈ ; krip = krip } }
        with ®Π-wf iA RT (®El⇒® T∈𝕌 t∼⟦t⟧)
           | krip (⊢wI ⊢[])
           | krip (⊢wwk (⊢∷ ⊢[] (t[σ]-Se (®Π-wf iA RT (®El⇒® T∈𝕌 t∼⟦t⟧)) (s-I ⊢[]))))
           | Bot⊆El iA (Bot-l 0)
...        | ⊢IT
           | record { IT-rel = IT-rel }
           | record { ap-rel = ap-rel }
           | l∈A
           with RT l∈A
              | ap-rel (®El-resp-T≈ iA (v0®x iA IT-rel) ([]-cong-Se′ ([I] ⊢IT) (s-wk (⊢∷ ⊢[] (t[σ]-Se ⊢IT (s-I ⊢[])))))) l∈A
...           | record { ↘⟦T⟧ = ⟦v⟧ .0 ; ↘⟦T′⟧ = ⟦v⟧ .0 ; T≈T′ = ne C≈C′ }
              | record { fa = .( _ _) ; ®fa = ne fa≈ , record { krip = krip } } = no-neutral-Se ⊢u′
  where ⊢u : IT  []  Ne⇒Exp (proj₁ (fa≈ 1))  OT
        ⊢u = conv (ctxeq-tm (∷-cong []-≈ ([I] ⊢IT)) (proj₁ (proj₂ (proj₂ (presup-≈ (proj₂ (krip (⊢wI (⊢∷ ⊢[] (t[σ]-Se ⊢IT (s-I ⊢[])))))))))))
                  (≈-trans ([]-cong-Se′ (≈-trans ([]-cong-Se″ ⊢OT (wk,v0≈I (⊢∷ ⊢[] ⊢IT))) ([I] ⊢OT)) (s-I (⊢∷ ⊢[] ⊢IT))) ([I] ⊢OT))

        ⊢[Se] = ⊢∷ ⊢[] (Se-wf i ⊢[])

        T≈′ : []  Π (Se i) (v 0)  Π IT OT  Se _
        T≈′ = ≈-trans (lift-⊢≈-Se-max {j = lvl} (≈-sym ([I] (Π-wf (Se-wf i ⊢[]) (cumu (conv (vlookup ⊢[Se] here) (Se-[] i (s-wk ⊢[Se])))))))) (lift-⊢≈-Se-max′ T≈)

        IT≈ : []  IT  Se i  Se _
        IT≈ = ≈-sym (proj₁ (Π-≈-inj T≈′))

        OT≈ : Se i  []  OT  v 0  Se _
        OT≈ = ≈-sym (proj₂ (Π-≈-inj T≈′))

        ⊢u′ : Se i  []  Ne⇒Exp (proj₁ (fa≈ 1))  v 0
        ⊢u′ = conv (ctxeq-tm (∷-cong []-≈ IT≈) ⊢u) OT≈