SN of STLC

STLC_SN_pending.agda

{-# OPTIONS --no-positivity-check #-}
open import Data.Nat
open import Data.Vec as Vec
open import Data.Star
open import Data.Empty
open import Data.Product
open import Relation.Nullary
open import Relation.Binary.PropositionalEquality

module SN {ConTm ConTy : Set} {B-length} (Base : Vec (ConTm × ConTy) B-length) where

-- syntax

infixr 5 _⟶_
data Typ : Set where
  Const : ConTy → Typ
  _⟶_ : Typ → Typ → Typ

data Term : Set where
  var : ℕ → Term
  const : ConTm → Term
  lambda : Term → Term
  app : Term → Term → Term

infixl 2 _$_
_$_ : Term → Term → Term
_$_ = app

data Ctx : ∀ {n} → Vec ℕ n → Set where
  cnil : Ctx []
  ccons : ∀ {n vs} → (σ : ℕ × Typ) → (Γ : Ctx {n} vs) → Ctx (proj₁ σ ∷ vs)

append : ∀ {n} {vs : Vec ℕ n} {m} {vs' : Vec ℕ m} → Ctx vs → Ctx vs' → Ctx (vs ++ vs')
append cnil Γ' = Γ'
append (ccons σ Γ) Γ' = ccons σ (append Γ Γ')

get : ∀ {n} {vs : Vec ℕ n} → Ctx vs → (i : ℕ) → i ∈ vs → Typ
get (ccons σ Γ) .(proj₁ σ) here = proj₂ σ
get (ccons σ Γ) i (there i-in) = get Γ i i-in

-- judgement

infix 3 _⊢_∶_
data _⊢_∶_ : ∀ {n} {vs : Vec ℕ n} → Ctx vs → Term → Typ → Set where
  jvar : ∀ {v τ} → (ccons (v , τ) cnil) ⊢ var v ∶ τ
  jconst : ∀ {c ct} → (c , ct) ∈ Base → cnil ⊢ const c ∶ Const ct
  jlambda : ∀ {n vs} {Γ : Ctx {n} vs} {M σ τ} → Γ ⊢ M ∶ τ → Γ ⊢ lambda M ∶ σ ⟶ τ
  japp : ∀ {n n' vs vs'} {Γ : Ctx {n} vs} {Γ' : Ctx {n'} vs'} {M N σ τ} →
    Γ ⊢ M ∶ σ ⟶ τ → Γ' ⊢ N ∶ σ → (append Γ Γ') ⊢ app M N ∶ τ

-- reduction

shift' : Term → Term
shift' = go 0 where
  go : ℕ → Term → Term
  go c (var v) with c ≤? v
  ... | yes _ = var (suc v)
  ... | no _ = var v
  go c (const x) = const x
  go c (lambda M) = lambda (go (suc c) M)
  go c (app M₁ M₂) = app (go c M₁) (go c M₂)

unshift' : Term → Term
unshift' M = go 0 M where
  go : ℕ → Term → Term
  go c (var v) with c ≤? v
  ... | yes _ = var (pred v)
  ... | no _ = var v
  go c (const x) = const x
  go c (lambda M) = lambda (go (suc c) M)
  go c (app M₁ M₂) = app (go c M₁) (go c M₂)

_⟦_≔_⟧ : Term → ℕ → Term → Term
(var i) ⟦ j ≔ S ⟧ with i ≟ j
... | yes _ = S
... | no _ = var i
(const c) ⟦ j ≔ S ⟧ = const c
(lambda M) ⟦ j ≔ S ⟧ = lambda (M ⟦ suc j ≔ shift' S ⟧)
(app M₁ M₂) ⟦ j ≔ S ⟧ = app (M₁ ⟦ j ≔ S ⟧) (M₂ ⟦ j ≔ S ⟧)

data _⇒β_ : Term → Term → Set where
  β-subst : ∀ {M N} → (app (lambda M) N) ⇒β unshift' (M ⟦ 0 ≔ shift' N ⟧)
  β-app₁ : ∀ {M₁ M₂ N} → M₁ ⇒β M₂ → app M₁ N ⇒β app M₂ N
  β-app₂ : ∀ {M₁ M₂ N} → M₁ ⇒β M₂ → app N M₁ ⇒β app N M₂
  β-lambda : ∀ {M₁ M₂} → M₁ ⇒β M₂ → lambda M₁ ⇒β lambda M₂

_⇒*β_ : Term → Term → Set
_⇒*β_ = Star _⇒β_

-- SN

data SN : Term → Set where
  sn : ∀ {M} → (∀ {N} → M ⇒*β N → M ≡ N) → SN M

deSN : ∀ {M} → SN M → ∀ {N} → M ⇒*β N → M ≡ N
deSN (sn s) = s

-- Logical Relation

data relL : Typ → Term → Set where
  L-const : ∀ {M σ} → SN M → relL (Const σ) M
  L-arrow : ∀ {M σ τ} → (∀ {N} → relL σ N → relL τ (app M N)) → relL (σ ⟶ τ) M

module relL-SN where
  var-SN : ∀ {v} → SN (var v)
  var-SN {v} = sn lem where
    lem : ∀ {N} → var v ⇒*β N → var v ≡ N
    lem ε = refl
    lem (() ◅ red)

  const-SN : ∀ {c} → SN (const c)
  const-SN {c} = sn lem where
    lem : ∀ {N} → const c ⇒*β N → const c ≡ N
    lem ε = refl
    lem (() ◅ red)

  module var-in-rel-proof where
    data varTms : Term → Set where
      varT : ∀ {x} → varTms (var x)
      appT : ∀ {ts M} → varTms ts → SN M → varTms (app ts M)

    varTms-SN : ∀ {M} → varTms M → SN M
    varTms-SN varT = var-SN
    varTms-SN (appT {ts} {M} v snM) = sn (lem v) where
      lem : ∀ {ts N} → varTms ts → app ts M ⇒*β N → app ts M ≡ N
      lem v ε = refl
      lem () (β-subst ◅ red)
      lem v (β-app₁ b ◅ red) rewrite sym (deSN (varTms-SN v) (return b)) = lem v red
      lem v (β-app₂ b ◅ red) rewrite sym (deSN snM (return b)) = lem v red
  open var-in-rel-proof

  mutual
    varTms-in-rel : ∀ {σ M} → varTms M → relL σ M
    varTms-in-rel {Const x₁} v = L-const (varTms-SN v)
    varTms-in-rel {σ ⟶ σ₁} v = L-arrow (λ {N} relN → varTms-in-rel (appT v (relL-SN relN)))

    var-in-rel : ∀ {σ x} → relL σ (var x)
    var-in-rel {Const x} = L-const var-SN
    var-in-rel {σ₁ ⟶ σ₂} = L-arrow (λ {N} relN → varTms-in-rel (appT varT (relL-SN relN)))

    relL-SN : ∀ {τ M} → relL τ M → SN M
    relL-SN {Const c} (L-const snM) = snM
    relL-SN {σ ⟶ τ} (L-arrow rel) = sn (lem rel) where
      app-≡₁ : ∀ {M N M' N'} → app M N ≡ app M' N' → M ≡ M'
      app-≡₁ refl = refl

      β*-app₁ : ∀ {M M' N} → M ⇒*β M' → app M N ⇒*β app M' N
      β*-app₁ ε = ε
      β*-app₁ (x ◅ red) = return (β-app₁ x) ◅◅ β*-app₁ red

      lem : ∀ {M N} → (∀ {L} → relL σ L → relL τ (app M L)) → M ⇒*β N → M ≡ N
      lem rel ε = refl
      lem rel (β-subst ◅ red) rewrite sym (app-≡₁ (deSN (relL-SN (rel (var-in-rel {x = 0}))) (return (β-app₁ β-subst)))) = lem rel red
      lem rel (β-app₁ b ◅ red) = app-≡₁ (deSN (relL-SN (rel {var 0} var-in-rel)) (return (β-app₁ (β-app₁ b)) ◅◅ β*-app₁ red))
      lem rel (β-app₂ b ◅ red) = app-≡₁ (deSN (relL-SN (rel {var 0} var-in-rel)) (return (β-app₁ (β-app₂ b)) ◅◅ β*-app₁ red))
      lem rel (β-lambda b ◅ red) = app-≡₁ (deSN (relL-SN (rel {var 0} var-in-rel)) (return (β-app₁ (β-lambda b)) ◅◅ β*-app₁ red))
open relL-SN

-- subst
-- これじゃだめ
-- どうやって de Bruijn index の変数を指定して代入するか？？？

data Subst : {n : ℕ} → Vec ℕ n → Set where
  ⟨⟩ : Subst []
  _∙_ : ∀ {n} {Γ : Vec ℕ n} → (t : ℕ × Term) (γ : Subst Γ) → Subst (proj₁ t ∷ Γ)

_#_ : ∀ {n} {Γ : Vec ℕ n} → Subst Γ → Term → Term
⟨⟩ # M = M
((n , t) ∙ γ) # M = {!   !}

module fundamental-theorem where
  data relS {n} {vs : Vec ℕ n} (Γ : Ctx vs) (γ : Subst vs) : Set where
    S-rel : ∀ {i} → (i-in : i ∈ vs) → relL (get Γ i i-in) (γ # var i) → relS Γ γ

  thm : ∀ {n vs} {Γ : Ctx {n} vs} {γ M σ} → Γ ⊢ M ∶ σ → relS Γ γ → relL σ (γ # M)
  thm jvar (S-rel here rel) = rel
  thm jvar (S-rel (there ()) rel)
  thm (jconst x) (S-rel i-in rel) = {!   !}
  thm {γ = γ} {lambda M} {σ ⟶ τ} (jlambda j) (S-rel i-in rel) = {!   !} where
    lem : ∀ {N} → relL σ N → relL τ (app (lambda (γ # M)) N)
    lem {N} relN = {!   !} where

  thm (japp j j₁) (S-rel i-in rel) = {!   !}

{-
j : ⊢ M : τ ~~~> relL τ M

?show : ∀ {N} → relL σ N → relL τ (app (lambda M) N)

---

?show : relL (σ --> τ) (lam M)
L-arrow : ∀ {M σ τ} → (∀ {N} → relL σ N → relL τ (app M N)) → relL (σ ⟶ τ) M

-}