pi.agda

open import Data.Nat using (ℕ ; zero ; suc) -- ; _≤_; z≤n ; s≤s ; _≤?_)
open import Data.Product using (∃-syntax) renaming (_,_ to ⟨_,_⟩)
-- open import Relation.Nullary using (Dec ; yes ; no)
-- open import Relation.Nullary.Decidable using (True ; toWitness)
-- open import Function using (id ; _∘_)
-- open import Data.List using (List ; [] ; _∷_)
open import Relation.Binary.PropositionalEquality using (_≡_ ; refl)
-- Dependently typed lambda calculus with de Bruijn indexes

infix 19 _∋_⦂_
infix 19 _⊢_⦂_
infix 19 _-→_
infix 20 _[_]
infix 20 _,_
infixr 21 _⇒_
infix 21 ƛ_
infix 22 _∙_
infix 23 `_
infix 23 ⊢`_

-- SYNTAX ---------------------------------------------------------------------

data Term : Set where
  `_ : ℕ → Term
  ƛ_ : Term → Term
  _∙_ : Term → Term → Term
  Type : Term
  _⇒_ : Term → Term → Term

-- SUBSTITUTION ---------------------------------------------------------------

extend-renamer : (ℕ → ℕ) → ℕ → ℕ
extend-renamer ρ zero = zero
extend-renamer ρ (suc n) = suc (ρ n)

rename : (ℕ → ℕ) → Term → Term
rename ρ (` n) = ` (ρ n)
rename ρ (ƛ N) = ƛ (rename (extend-renamer ρ) N)
rename ρ (N ∙ M) = rename ρ N ∙ rename ρ M
rename ρ Type = Type
rename ρ (A ⇒ N) = rename ρ A ⇒ rename (extend-renamer ρ) N

extend-sub : (ℕ → Term) → ℕ → Term
extend-sub σ zero = ` zero
extend-sub σ (suc n) = rename suc (σ n)

substitute : (ℕ → Term) → Term → Term
substitute σ (` n) = σ n
substitute σ (ƛ N) = ƛ (substitute (extend-sub σ) N)
substitute σ (N ∙ M) = substitute σ N ∙ substitute σ M
substitute σ Type = Type
substitute σ (A ⇒ N) = substitute σ A ⇒ substitute (extend-sub σ) N

_[_] : Term → Term → Term
_[_] N M = substitute σ N
  where
    σ : ℕ → Term
    σ zero = M
    σ (suc n) = ` n

-- TYPING ---------------------------------------------------------------------

data Context : Set where

  ∅ : Context

  _,_ : Context → Term → Context

shift : Term → Term
shift = rename suc

{-
data Map (f : Term → Term) : Context → Context → Set where
  Z : Map f ∅ ∅
  S_ : ∀ { Γ Γ' A }
    → Map f Γ Γ'
    → Map f (Γ , A) (Γ' , f A)

Map-function : ∀ { f Γ }
  → ∃[ Γ' ] (Map f Γ Γ')
Map-function {_} {∅} = ⟨ ∅ , Z ⟩
Map-function {f} {Γ , A} with Map-function {f} {Γ}
... | ⟨ Γ' , p ⟩ = ⟨ (Γ' , f A) , S p ⟩
-}

data _∋_⦂_ : Context → ℕ → Term → Set where

  Z : ∀ { Γ A }
    → (Γ , A) ∋ zero ⦂ shift A

  S_ : ∀ { Γ A B i }
    → Γ ∋ i ⦂ A
    → Γ , B ∋ suc i ⦂ shift A

data _⊢_⦂_ (Γ : Context) : Term → Term → Set where

  ⊢Type : Γ ⊢ Type ⦂ Type

  ⊢`_ : ∀ { A i }
    → Γ ∋ i ⦂ A
    → Γ ⊢ ` i ⦂ A

  ⊢ƛ : ∀ { A B N }
    → Γ ⊢ A ⦂ Type
    → Γ , A ⊢ N ⦂ B
    → Γ ⊢ ƛ N ⦂ A ⇒ B

  _∙_ : ∀ { L N A B }
    → Γ ⊢ L ⦂ A ⇒ B
    → Γ ⊢ N ⦂ A
    → Γ ⊢ L ∙ N ⦂ B [ N ]

  _⇒_ : ∀ { A B }
    → Γ ⊢ A ⦂ Type
    → Γ , A ⊢ B ⦂ Type
    → Γ ⊢ A ⇒ B ⦂ Type

_ : ∅ ⊢ ƛ ƛ ` 0 ⦂ Type ⇒ ` 0 ⇒ ` 1
_ = ⊢ƛ ⊢Type (⊢ƛ (⊢` Z) (⊢` Z))

-- REDUCTION ------------------------------------------------------------------

data Value : Term → Set where

  V-ƛ : ∀ { N }
    → Value (ƛ N)

  V-Type : Value Type

  V-⇒ : ∀ { A B }
    → Value (A ⇒ B)

data _-→_ : Term → Term → Set where

  ξ-∙₁ : ∀ { L L' N }
    → L -→ L'
    → L ∙ N -→ L' ∙ N

  ξ-∙₂ : ∀ { L N N' }
    → Value L
    → N -→ N'
    → L ∙ N -→ L ∙ N'

  β-ƛ : ∀ { N M }
    → Value M
    → (ƛ N) ∙ M -→ N [ M ]

-- PROGRESS -------------------------------------------------------------------

data Progress (N : Term) : Set where

  step : ∀ { M }
    → N -→ M
    → Progress N

  done :
      Value N
    → Progress N

progress : ∀ { N A }
  → ∅ ⊢ N ⦂ A
  → Progress N
progress ⊢Type = done V-Type
progress (⊢` ())
progress (⊢ƛ _ _) = done V-ƛ
progress (⊢N ∙ ⊢M) with progress ⊢N
... | step N-→N' = step (ξ-∙₁ N-→N')
... | done V-N with progress ⊢M
...   | step M-→M' = step (ξ-∙₂ V-N M-→M')
...   | done V-M with V-N
...     | V-ƛ = step (β-ƛ V-M)
progress (⊢A ⇒ ⊢B) = done V-⇒

-- PRESERVATION ---------------------------------------------------------------

-- FIX type equality
⊢extend-renamer : ∀ { Γ Δ }
  → (∀ { a A }   → Γ     ∋ a ⦂ A → Δ     ∋ a ⦂ A)
  → (∀ { a A B } → Γ , B ∋ a ⦂ A → Δ , B ∋ a ⦂ A)
⊢extend-renamer ρ Z = Z
⊢extend-renamer ρ (S n) = S (ρ n)

⊢rename : ∀ { Γ Δ }
  → (∀ { a A } → Γ ∋ a ⦂ A → Δ ∋ a ⦂ A)
  → (∀ { N A } → Γ ⊢ N ⦂ A → Δ ⊢ N ⦂ A)
⊢rename ρ (⊢` ∋n) = ⊢` (ρ ∋n)
⊢rename ρ (⊢ƛ ⊢A ⊢N) = ⊢ƛ (⊢rename ρ ⊢A) (⊢rename (⊢extend-renamer ρ) ⊢N)
⊢rename ρ (⊢N ∙ ⊢M) = ⊢rename ρ ⊢N ∙ ⊢rename ρ ⊢M
⊢rename ρ ⊢Type = ⊢Type
⊢rename ρ (⊢A ⇒ ⊢N) = ⊢rename ρ ⊢A ⇒ ⊢rename (⊢extend-renamer ρ) ⊢N

⊢extend-sub : ∀ { Γ Δ }
  → (∀ { a A }   → Γ     ∋ a ⦂ A → ∃[ N ] (Δ     ⊢ N ⦂ A))
  → (∀ { a A B } → Γ , B ∋ a ⦂ A → ∃[ N ] (Δ , B ⊢ N ⦂ A))
⊢extend-sub σ Z = ⟨ ` 0 , ⊢` Z ⟩
⊢extend-sub σ (S n) with σ n
... | ⟨ N , ⊢N ⟩ = ⟨ shift N , {!!} ⟩

-- Goal:
-- ρ : Γ ∋ n ⦂ A → ∃[ B ] (∃[ N ] (Δ ⊢ N ⦂ B)) × ρ ⊢A ≡ ⊢B
-- Γ ⊢ N

preserve : ∀ { M M' A }
  → ∅ ⊢ M ⦂ A
  → M -→ M'
  → ∅ ⊢ M' ⦂ A
preserve ⊢Type ()
preserve (⊢` ())
preserve (⊢ƛ _ _) ()
preserve (⊢L ∙ ⊢N) (ξ-∙₁ L-→L') = preserve ⊢L L-→L' ∙ ⊢N
preserve (⊢L ∙ ⊢N) (ξ-∙₂ V-L N-→N') = {!!}
preserve (⊢L ∙ ⊢N) (β-ƛ V-N) = {!!}
preserve (_ ⇒ _) ()

-- INFERRENCE -----------------------------------------------------------------

mutual

  data Term↑ : Set where

    `_ : ℕ → Term↑

    _∙_ : Term↑ → Term↓ → Term↑

    Type : Term↑

    _⇒_ : Term↓ → Term↓ → Term↑

    _↓_ : Term↓ → Term↑

  data Term↓ : Set where

    ƛ_ : Term↓ → Term↓

    _↑ : Term↑ → Term↓

mutual

  data Context' : Set where

    ∅ : Context'

    _,_ : Context' → Term↑ → Context

  data _⊢_↑_ (Γ : Context') : Term↑ → Term↑ where

    ⊢`_ : ∀ { A i }
      → Γ ∋ i ⦂ A
      → Γ ⊢ ` i ↑ A

    _∙_ : ∀ { L N A B }
      → Γ ⊢ L ↑ A ⇒ B
      → Γ ⊢ N ↓ A
      → Γ ⊢ L ∙ N ↑ B [ N ]

    ⊢Type : Γ ⊢ Type ↑ Type

    _⇒_ : ∀ { A B }
      → Γ ⊢ A ↓ Type
      → Γ , A ⊢ B ↓ Type
      → Γ ⊢ A ⇒ B ↑ Type

    ⊢↓ : ∀ { N A }
      → Γ ⊢ N ↓ A
      → Γ ⊢ (N ↓ A) ↑ A

  data _⊢_↓_ (Γ : Context') : Term↓ → Term↑ where

    ⊢ƛ : ∀ { A B N }
      → Γ ⊢ A ↓ Type
      → Γ , A ⊢ N ↓ B
      → Γ ⊢ ƛ N ↓ A ⇒ B

    ⊢↑ : ∀ { N A }
      → Γ ⊢ N ↑ A
      → Γ ⊢ N ↓ A

{-

length : Context → ℕ
length ∅ = 0
length (rest , _) = suc (length rest)

lookup : ∀ { Γ i } → suc i ≤ length Γ → Term
lookup {_ , p} {zero} (s≤s z≤n) = p
lookup {rest , _} {suc i} (s≤s i≤l) = lookup i≤l

scoped : ∀ { Γ i } → (p : suc i ≤ length Γ) → Γ ∋ (lookup p)
scoped {_ , p} {zero} (s≤s z≤n) = Z
scoped {rest , _} {suc _} (s≤s s≤l) = S (scoped s≤l)

-}