Nearly-complete inductive-recursive encoding of LF in Agda

LF.agda

open import Data.Nat
open import Data.Fin
open import Level
open import Relation.Binary.PropositionalEquality

module LF where

  {- Semantic model primitives -}
  Rℕ : {C : ℕ -> Set} -> (x : ℕ) -> C ℕ.zero -> ((n : ℕ) -> C n -> C (ℕ.suc n)) -> C x
  Rℕ ℕ.zero z s = z
  Rℕ (ℕ.suc n) z s = s n (Rℕ n z s)
  
  -- Operator J!
  J : ∀ {σ : Set}{a b} -> (C : (a : σ) -> (b : σ) -> a ≡ b -> Set) ->
                        (P : a ≡ b) ->
                        (D : C a a (refl)) ->
                        C a b P
  J C refl D = D

  {- Now a syntactic model that we can interpret into the semantic model -}

  mutual
    data U : Set where
      ⋆ : U
      □ : U
    -- I'm going to try to use this to avoid level-polymorphism-hell
    El : U -> Level
    El ⋆ = Level.zero
    El □ = Level.suc (Level.zero)
    data Type : U -> Set where
      `ℕ : Type ⋆
      `Πp : (σ : Type ⋆) -> ([[ σ ]] -> Type ⋆) -> Type ⋆
      `Πpt : (σ : Type ⋆) -> ([[ σ ]] -> Type □) -> Type □
      I[_,_,_] : {u : U} -> (σ : Type u) -> Tm u σ -> Tm u σ -> Type u 
      {- Can't write a □ -> □ version, since the interpretation of the argument type makes
         the second component too large to fit in Set.  And of course, □ -> ⋆ is impredicative,
         so there are two reasons it won't embed.
         This is unfortunate, but at least we have ℝ={(⋆,⋆),(⋆,□)} is λP=LF.
      -}
    [[_]] : {u : U} -> (Type u) -> Set (El u)
    [[_]] {⋆} (`Πp σ y) = (x : [[ σ ]]) -> [[ y x ]]
    [[_]] {⋆} `ℕ = ℕ
    [[_]] {□} (`Πpt σ y) = (x : [[ σ ]]) -> [[ y x ]]
    [[_]] {⋆} (I[ σ , x , y ]) =  _≡_ {El ⋆} (⇓ x ⇓) (⇓ y ⇓) --⇓ x ⇓ ≡ ⇓ y ⇓
    [[_]] {□} (I[ σ , x , y ]) =  _≡_ {El □} (⇓ x ⇓) (⇓ y ⇓) --⇓ x ⇓ ≡ ⇓ y ⇓
    data Tm : (u : U) -> Type u -> Set where
      -- This is only part of the conversion relation we'd like to have
      -- Note that it's only needed for the reification attempt below
      --conv-tm : ∀ {σ} (ρ : [[ σ ]] -> Type ⋆) -> 
      --                (x : Tm ⋆ σ) -> (y : Tm ⋆ σ) -> 
      --                ⇓ x ⇓ ≡ ⇓ y ⇓ ->
      --                Tm ⋆ (ρ ⇓ x ⇓) -> Tm ⋆ (ρ ⇓ y ⇓)
      `λp : ∀ {σ τ} (e : (ρ : [[ σ ]]) -> Tm ⋆ (τ ρ)) -> Tm ⋆ (`Πp σ τ)
      `λpt : ∀ {σ}{τ : [[ σ ]] -> Type □} (e : (ρ : [[ σ ]]) -> Tm □ (τ ρ)) -> Tm □ (`Πpt σ τ)
      `refl : ∀ {u : U} {σ : Type u} -> (x : Tm u σ) -> Tm u (I[ σ , x , x ])
      `Jp : ∀ {σ : Type ⋆} {a : Tm ⋆ σ} { b} -> 
             (C : (a : [[ σ ]]) -> (b : [[ σ ]]) -> _≡_ {El ⋆} a b -> Type ⋆) ->
             (P : Tm ⋆ (I[ σ , a , b ])) ->
             -- Should be (D : Tm ⋆ (C (⇓ a ⇓) (⇓ a ⇓) ⇓ (`refl a) ⇓)) -> 
             -- but Agda claims ⇓ `refl a ⇓ /≡ refl...
             (D : Tm ⋆ (C (⇓ a ⇓) (⇓ a ⇓) refl)) -> 
             Tm ⋆ (C (⇓ a ⇓) (⇓ b ⇓) ⇓ P ⇓)
      pApp : ∀ {τ}{σ} -> Tm ⋆ (`Πp τ σ) -> (e : Tm ⋆ τ) -> Tm ⋆ (σ (⇓ e ⇓))
      ptApp : ∀ {τ}{σ} -> Tm □ (`Πpt τ σ) -> (e : Tm ⋆ τ) -> Tm □ (σ (⇓ e ⇓))
      `0 : Tm ⋆ `ℕ
      `S : Tm ⋆ (`Πp `ℕ (λ _ → `ℕ))
      `Rℕ : ∀  {τ : [[ `ℕ ]] -> Type ⋆} -> 
                     (t : Tm ⋆ `ℕ) -> 
                     (z : Tm ⋆ (τ ℕ.zero)) -> --(z : Tm ⋆ (τ ⇓ `0 ⇓)) ->, but Agda doesn't do the conversion right...
                     -- Should be (s : Tm ⋆ (`Πp `ℕ (λ n → `Πp (τ n) (λ r → τ (⇓ `S ⇓ n))))) ->
                     -- but Agda claims ⇓ `S ⇓ n /≡ ℕ.suc n...
                     (s : Tm ⋆ (`Πp `ℕ (λ n → `Πp (τ n) (λ r → τ (ℕ.suc n))))) ->
                     Tm ⋆ (τ ⇓ t ⇓)
    ⇓_⇓ : {u : U} -> {τ : Type u} -> Tm u τ -> [[ τ ]]
    ⇓ `0 ⇓ = ℕ.zero
    ⇓ `S ⇓ = ℕ.suc
    ⇓ pApp y e ⇓ = ⇓ y ⇓ ⇓ e ⇓
    ⇓ ptApp y e ⇓ = (⇓ y ⇓) ⇓ e ⇓
    ⇓ `λp e ⇓ = λ x → ⇓ e x ⇓
    ⇓ `λpt e ⇓ = λ x → ⇓ e x ⇓
    ⇓ `refl {⋆} {σ} a ⇓ = refl
    ⇓ `refl {□} {σ} a ⇓ = refl
    ⇓ `Jp {σ} {a} {b} C P D ⇓ = J (λ a' b' x → [[ C a' b' x ]]) (⇓ P ⇓) ⇓ D ⇓
    ⇓ `Rℕ {τ} t z s ⇓ = Rℕ {λ x → [[ τ x ]]} ⇓ t ⇓ (⇓ z ⇓) (λ n x → ⇓ s ⇓ n x)
    --⇓ conv-tm {σ} ρ x y x≡y y0 ⇓ = subst (λ x' → [[ ρ x' ]]) x≡y ⇓ y0 ⇓ -- x and y interpret to the same value, so...
    
  {- This terrible hack is sound within the LF encoding, but obviously
     not with raw Agda semantics since e.g. `Jp, `Rℕ, and pApp can all
     produce a result type in ⋆.
     Maybe if I extended the LF variant above to use an observational
     equality instead of vanilla propositional equality this would work,
     since the LF terms can't actually distinguish any terms whose
     denotations are equal. -}
  postulate
    inject-equality : ∀ {u σ} (x : Tm u σ) (y : Tm u σ) -> ⇓ x ⇓ ≡ ⇓ y ⇓ -> x ≡ y
    
  {- We'd also really like to be able to implement these functions from
     native Agda types into the LF encoding, which means we need to be
     able to reify Agda values of a type with an LF embedding equivalent
     into the LF term representations.
  -}
  reify : {u : U} -> (t : Type u) -> [[ t ]] -> Tm u t
  reify {⋆} `ℕ ℕ.zero = `0
  reify {⋆} `ℕ (ℕ.suc n) = pApp `S (reify `ℕ n)
  reify {⋆} (`Πp σ y) a = `λp (λ ρ → reify (y ρ) (a ρ))
  reify {□} (`Πpt σ y) a = `λpt (λ ρ → reify (y ρ) (a ρ))
  {- I think we need to lift some notion of conversion into the LF typing,
     since Agda (reasonably) refuses to unify y and y' directly -}
  -- This might be too large to encode computationally, though I can't even make the small one compute
  reify {□} I[ σ , y , y' ] a = subst (λ x → Tm □ I[ σ , y , x ]) (inject-equality y y' a) (`refl y) 
  reify {⋆} I[ σ , y , y' ] a = subst (λ x → Tm ⋆ I[ σ , y , x ]) (inject-equality y y' a) (`refl y) 
  -- Note that Agda doesn't complain about missing terms since we're
  -- reifying normal forms of Agda values

  {- I had to hack around the fact that Agda's typechecker fails to
     notice a couple definitional equalities -}
  lemma-interp-`0 : ⇓ `0 ⇓ ≡ ℕ.zero 
  lemma-interp-`0 = refl

  lemma-interp-`S : (n : ℕ) -> ⇓ `S ⇓ n ≡ ℕ.suc n
  lemma-interp-`S n = refl
  

  {- Now we can actually implement things! -}
  inc : Tm ⋆ (`Πp `ℕ (λ n → `ℕ))
  inc = `λp (λ ρ → pApp `S (reify `ℕ ρ))
  
  ⇑_ : {u : U} -> {t : Type u} -> [[ t ]] -> Tm u t
  ⇑_ {u} {t} tm = reify t tm

  ℕeq : Tm ⋆ (`Πp `ℕ (λ n -> (I[ `ℕ , ⇑ n , ⇑ n ])))
  ℕeq = `λp (λ n → `refl (⇑ n))
  

  -- Need to prove ∀ v:[[σ]], v ≡ ⇓ (⇑ v) ⇓ and do some subst'ing
  Itrans : Tm ⋆ (`Πp `ℕ (λ x → 
                (`Πp `ℕ (λ y → 
                (`Πp `ℕ (λ z → 
                     `Πp I[ `ℕ , ⇑ x , ⇑ y ] (λ xy →
                     `Πp I[ `ℕ , ⇑ y , ⇑ z ] (λ yz →
                     I[ `ℕ , ⇑ x , ⇑ z ]))))))))
  Itrans = `λp (λ x → `λp (λ y → `λp (λ z → 
               `λp (λ xy → `λp (λ yz → 
               `Jp {`ℕ} {⇑ ⇓ reify `ℕ {!!} ⇓} {⇑ {!!}} (λ a b e → I[ `ℕ , ⇑ x , ⇑ b ]) (⇑ yz) (⇑ xy))))))