-- checked on Agda 2.5.2, standard library 0.13
-- This file is based on Abel's formalization:
-- https://github.com/andreasabel/strong-normalization/blob/master/agda/RenamingAndSubstitution.agda

module deBruijn-cbn where

open import Data.Nat
open import Data.Unit
open import Data.Empty
open import Data.List
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Function using (_∘_)

-- types
infixr 6 _⇒_

data typ : Set where
  Nat : typ
  _⇒_ : typ → typ → typ

Cxt : Set
Cxt = List typ

-- variables
data var : (Γ : Cxt) (τ : typ) → Set where
  zero : {Γ : Cxt} {τ : typ} → var (τ ∷ Γ) τ
  suc  : {Γ : Cxt} {τ σ : typ} → (x : var Γ τ) → var (σ ∷ Γ) τ

-- well-typed values and terms
mutual
  data value (Γ : Cxt) : (τ : typ) → Set where
    Num : (n : ℕ) → value Γ Nat
    Fun : (τ₂ : typ) → {τ₁ : typ} → term (τ₂ ∷ Γ) τ₁ → value Γ (τ₂ ⇒ τ₁)

  data term (Γ : Cxt) : (τ : typ) → Set where
    Val : {τ : typ} → (v : value Γ τ) → term Γ τ
    Var : {τ : typ} (x : var Γ τ) → term Γ τ
    App : {τ₂ τ₁ : typ} → term Γ (τ₂ ⇒ τ₁) → term Γ τ₂ → term Γ τ₁

-- normal forms
mutual
  data ne (Γ : Cxt) : (τ : typ) → Set where
    Var : {τ : typ} (x : var Γ τ) → ne Γ τ
    App : {τ₂ τ₁ : typ} → ne Γ (τ₂ ⇒ τ₁) → nf Γ τ₂ → ne Γ τ₁

  data nf (Γ : Cxt) : (τ : typ) → Set where
    Ne : {τ : typ} → ne Γ τ → nf Γ τ
    Num : (n : ℕ) → nf Γ Nat
    Fun : (τ₂ : typ) → {τ₁ : typ} → nf (τ₂ ∷ Γ) τ₁ → nf Γ (τ₂ ⇒ τ₁)

mutual
  embedNe : {Γ : Cxt} {τ : typ} → ne Γ τ → term Γ τ
  embedNe (Var x) = Var x
  embedNe (App ne nf) = App (embedNe ne) (embedNf nf)

  embedNf : {Γ : Cxt} {τ : typ} → nf Γ τ → term Γ τ
  embedNf (Ne ne) = embedNe ne
  embedNf (Num n) = Val (Num n)
  embedNf (Fun τ nf) = Val (Fun τ (embedNf nf))

mutual
  isNeV : {Γ : Cxt} {τ : typ} → (v : value Γ τ) → Set
  isNeV (Num n) = ⊤
  isNeV (Fun τ e) = ⊥

  isNe : {Γ : Cxt} {τ : typ} → (e : term Γ τ) → Set
  isNe (Val v) = isNeV v
  isNe (Var x) = ⊤
  isNe (App e₁ e₂) = isNe e₁ × isNf e₂

  isNfV : {Γ : Cxt} {τ : typ} → (v : value Γ τ) → Set
  isNfV (Num n) = ⊤
  isNfV (Fun τ e) = isNf e

  isNf : {Γ : Cxt} {τ : typ} → (e : term Γ τ) → Set
  isNf (Val v) = isNfV v
  isNf (Var x) = ⊤
  isNf (App e₁ e₂) = isNe e₁ × isNf e₂

-- renamings
data Ren (Γ : Cxt) : (Δ : Cxt) → Set where
  [] : Ren Γ []
  _∷_ : {Δ : Cxt} {τ : typ} →
        (x : var Γ τ) → (xs : Ren Γ Δ) → Ren Γ (τ ∷ Δ)

lookr : {Γ Δ : Cxt} → Ren Γ Δ → {τ : typ} → var Δ τ → var Γ τ
lookr (x ∷ xs) zero = x
lookr (x ∷ xs) (suc y) = lookr xs y

wkr : {Γ Δ : Cxt} → {τ : typ} → Ren Γ Δ → Ren (τ ∷ Γ) Δ
wkr [] = []
wkr (x ∷ xs) = suc x ∷ wkr xs

liftr : {Γ Δ : Cxt} → {τ : typ} → Ren Γ Δ → Ren (τ ∷ Γ) (τ ∷ Δ)
liftr xs = zero ∷ wkr xs

renId : {Γ : Cxt} → Ren Γ Γ
renId {[]} = []
renId {τ ∷ Γ} = liftr (renId {Γ})

renComp : {Γ Δ Φ : Cxt} → Ren Γ Δ → Ren Δ Φ → Ren Γ Φ
renComp xs [] = []
renComp xs (y ∷ ys) = lookr xs y ∷ renComp xs ys

lookrwkr : {Γ Δ : Cxt} {σ τ : typ} (xs : Ren Γ Δ) (y : var Δ σ) →
           lookr (wkr {τ = τ} xs) y ≡ suc (lookr xs y)
lookrwkr (x ∷ xs) zero = refl
lookrwkr (x ∷ xs) (suc y) = lookrwkr xs y

lemrr : {Γ Δ Φ : Cxt} {τ : typ}
        (xs : Ren Γ Δ) (x : var Γ τ) (ys : Ren Δ Φ) →
        renComp (x ∷ xs) (wkr ys) ≡ renComp xs ys
lemrr xs x [] = refl
lemrr xs x (y ∷ ys) = cong (_∷_ (lookr xs y)) (lemrr xs x ys)

wkrcomp : {Γ Δ Φ : Cxt} {τ : typ} (xs : Ren Γ Δ) (ys : Ren Δ Φ) →
          renComp (wkr {τ = τ} xs) ys ≡ wkr {τ = τ} (renComp xs ys)
wkrcomp xs [] = refl
wkrcomp xs (y ∷ ys) = cong₂ _∷_ (lookrwkr xs y) (wkrcomp xs ys)

liftrcomp : {Γ Δ Φ : Cxt} {τ : typ} (xs : Ren Γ Δ) (ys : Ren Δ Φ) →
  renComp (liftr {τ = τ} xs) (liftr {τ = τ} ys) ≡ liftr (renComp xs ys)
liftrcomp xs ys = cong (_∷_ zero) (begin
    renComp (liftr xs) (wkr ys) ≡⟨ lemrr (wkr xs) zero ys ⟩
    renComp (wkr xs) ys         ≡⟨ wkrcomp xs ys ⟩
    wkr (renComp xs ys)         ∎)
  where open ≡-Reasoning

lookrid : {Γ : Cxt} {τ : typ} (x : var Γ τ) → lookr renId x ≡ x
lookrid zero = refl
lookrid (suc x) = begin
  lookr (wkr renId) x ≡⟨ lookrwkr renId x ⟩
  suc (lookr renId x) ≡⟨ cong suc (lookrid x) ⟩
  suc x               ∎
  where open ≡-Reasoning

lookrcomp : {Γ Δ Φ : Cxt} (f : Ren Γ Δ) (g : Ren Δ Φ)
            {τ : typ} (x : var Φ τ) →
            lookr (renComp f g) x ≡ (lookr f ∘ lookr g) x
lookrcomp f (y ∷ g) zero = refl
lookrcomp f (y ∷ g) (suc x) = lookrcomp f g x

lidr : {Γ Δ : Cxt} (xs : Ren Γ Δ) → renComp renId xs ≡ xs
lidr [] = refl
lidr (x ∷ xs) = cong₂ _∷_ (lookrid x) (lidr xs)

ridr : {Γ Δ : Cxt} (xs : Ren Γ Δ) → renComp xs renId ≡ xs
ridr [] = refl
ridr (x ∷ xs) = begin
    x ∷ renComp (x ∷ xs) (wkr renId) ≡⟨ cong (_∷_ x) (lemrr xs x renId) ⟩
    x ∷ renComp xs renId             ≡⟨ cong (_∷_ x) (ridr xs) ⟩
    x ∷ xs
  ∎
  where open ≡-Reasoning

-- renamings of terms
mutual
  renV : {Γ Δ : Cxt} → Ren Γ Δ → {τ : typ} → value Δ τ → value Γ τ
  renV xs (Num n) = Num n
  renV xs (Fun τ e) = Fun τ (ren (liftr xs) e)

  ren : {Γ Δ : Cxt} → Ren Γ Δ → {τ : typ} → term Δ τ → term Γ τ
  ren xs (Val v) = Val (renV xs v)
  ren xs (Var x) = Var (lookr xs x)
  ren xs (App e₁ e₂) = App (ren xs e₁) (ren xs e₂)

mutual
  renidV : {Γ : Cxt} {τ : typ} → (v : value Γ τ) → renV renId v ≡ v
  renidV (Num n) = refl
  renidV (Fun τ e) = cong (Fun τ) (renid e)

  renid : {Γ : Cxt} {τ : typ} → (e : term Γ τ) → ren renId e ≡ e
  renid (Val v) = cong Val (renidV v)
  renid (Var x) = cong Var (lookrid x)
  renid (App e₁ e₂) = cong₂ App (renid e₁) (renid e₂)

mutual
  rencompV : {Γ Δ Φ : Cxt} (f : Ren Γ Δ) (g : Ren Δ Φ) {σ : typ}
             (v : value Φ σ) → renV (renComp f g) v ≡ (renV f ∘ renV g) v
  rencompV f g (Num n) = cong Num refl
  rencompV f g (Fun τ e) = cong (Fun τ) (begin
      ren (liftr (renComp f g)) e
    ≡⟨ cong (λ xs → ren xs e) (sym (liftrcomp f g)) ⟩
      ren (renComp (liftr f) (liftr g)) e
    ≡⟨ rencomp (liftr f) (liftr g) e ⟩
      ren (liftr f) (ren (liftr g) e)
    ∎)
    where open ≡-Reasoning

  rencomp : {Γ Δ Φ : Cxt} (f : Ren Γ Δ) (g : Ren Δ Φ) {σ : typ}
            (e : term Φ σ) → ren (renComp f g) e ≡ (ren f ∘ ren g) e
  rencomp f g (Val v) = cong Val (rencompV f g v)
  rencomp f g (Var x) = cong Var (lookrcomp f g x)
  rencomp f g (App e₁ e₂) = cong₂ App (rencomp f g e₁) (rencomp f g e₂)

weakV : {Γ : Cxt} {τ : typ} (σ : typ) → value Γ τ → value (σ ∷ Γ) τ
weakV σ = renV (wkr renId)

weak : {Γ : Cxt} {τ : typ} (σ : typ) → term Γ τ → term (σ ∷ Γ) τ
weak σ = ren (wkr renId)

mutual
  renNe : {Γ Δ : Cxt} → Ren Γ Δ → {τ : typ} → ne Δ τ → ne Γ τ
  renNe xs (Var x) = Var (lookr xs x)
  renNe xs (App ne nf) = App (renNe xs ne) (renNf xs nf)

  renNf : {Γ Δ : Cxt} → Ren Γ Δ → {τ : typ} → nf Δ τ → nf Γ τ
  renNf xs (Ne ne) = Ne (renNe xs ne)
  renNf xs (Num n) = Num n
  renNf xs (Fun τ nf) = Fun τ (renNf (liftr xs) nf)

weakNe : {Γ : Cxt} {τ : typ} (σ : typ) → ne Γ τ → ne (σ ∷ Γ) τ
weakNe σ = renNe (wkr renId)

weakNf : {Γ : Cxt} {τ : typ} (σ : typ) → nf Γ τ → nf (σ ∷ Γ) τ
weakNf σ = renNf (wkr renId)

-- (value) substitution
data Sub (Γ : Cxt) : (Δ : Cxt) → Set where
  [] : Sub Γ []
  _∷_ : {Δ : Cxt} {τ : typ} →
        (v : term Γ τ) → (es : Sub Γ Δ) → Sub Γ (τ ∷ Δ)

ren2sub : {Γ Δ : Cxt} → Ren Γ Δ → Sub Γ Δ
ren2sub [] = []
ren2sub (x ∷ xs) = Var x ∷ ren2sub xs

looks : {Γ Δ : Cxt} → Sub Γ Δ → {τ : typ} → var Δ τ → term Γ τ
looks (v ∷ vs) zero = v
looks (v ∷ vs) (suc x) = looks vs x

wks : {Γ Δ : Cxt} {τ : typ} → Sub Γ Δ → Sub (τ ∷ Γ) Δ
wks [] = []
wks (v ∷ vs) = ren (wkr renId) v ∷ wks vs

lifts : {Γ Δ : Cxt} {τ : typ} → Sub Γ Δ → Sub (τ ∷ Γ) (τ ∷ Δ)
lifts vs = Var zero ∷ wks vs

mutual
  subV : {Γ Δ : Cxt} → Sub Γ Δ → {τ : typ} → value Δ τ → value Γ τ
  subV vs (Num n) = Num n
  subV vs (Fun τ e) = Fun τ (sub (lifts vs) e)

  sub : {Γ Δ : Cxt} → Sub Γ Δ → {τ : typ} → term Δ τ → term Γ τ
  sub vs (Val v) = Val (subV vs v)
  sub vs (Var x) = looks vs x
  sub vs (App e₁ e₂) = App (sub vs e₁) (sub vs e₂)

subId : {Γ : Cxt} → Sub Γ Γ
subId {[]} = []
subId {τ ∷ Γ} = lifts (subId {Γ})

subComp : {Γ Δ Φ : Cxt} → Sub Γ Δ → Sub Δ Φ → Sub Γ Φ
subComp vs [] = []
subComp vs (w ∷ ws) = sub vs w ∷ subComp vs ws

sub0 : {Γ : Cxt} {τ σ : typ} →
       term Γ σ → term (σ ∷ Γ) τ → term Γ τ
sub0 v e = sub (v ∷ subId) e

lookswks : {Γ Δ : Cxt} {σ τ : typ} (y : var Δ σ) (xs : Sub Γ Δ) →
           looks (wks {τ = τ} xs) y ≡
           ren (wkr {τ = τ} renId) (looks xs y)
lookswks zero (x ∷ xs) = refl
lookswks (suc y) (x ∷ xs) = lookswks y xs

lemsr : {Γ Δ Φ : Cxt} {σ : typ}
        (xs : Sub Γ Δ) (v : term Γ σ) (ys : Ren Δ Φ) →
        subComp (v ∷ xs) (ren2sub (wkr ys)) ≡ subComp xs (ren2sub ys)
lemsr xs v [] = refl
lemsr xs v (x ∷ ys) = cong (_∷_ (looks xs x)) (lemsr xs v ys)

lookslookr : {Γ Δ Φ : Cxt} (f : Sub Γ Δ) (g : Ren Δ Φ) {τ : typ}
             (x : var Φ τ) →
             looks (subComp f (ren2sub g)) x ≡ looks f (lookr g x)
lookslookr f (x ∷ g) zero = refl
lookslookr f (x ∷ g) (suc y) = lookslookr f g y

wksrcomp : {Γ Δ Φ : Cxt} {τ : typ} (xs : Sub Γ Δ) (ys : Ren Δ Φ) →
           subComp (wks {τ = τ} xs) (ren2sub ys) ≡
           wks {τ = τ} (subComp xs (ren2sub ys))
wksrcomp xs [] = refl
wksrcomp xs (y ∷ ys) = cong₂ _∷_ (lookswks y xs) (wksrcomp xs ys)

liftsrcomp : {Γ Δ Φ : Cxt} {τ : typ} (xs : Sub Γ Δ) (ys : Ren Δ Φ) →
             subComp (lifts {τ = τ} xs) (ren2sub (liftr ys)) ≡
             lifts {τ = τ} (subComp xs (ren2sub ys))
liftsrcomp xs ys = cong (_∷_ (Var zero)) (begin
  subComp (lifts xs) (ren2sub (wkr ys)) ≡⟨ lemsr (wks xs) (Var zero) ys ⟩
  subComp (wks xs) (ren2sub ys)         ≡⟨ wksrcomp xs ys ⟩
  wks (subComp xs (ren2sub ys))         ∎)
  where open ≡-Reasoning

mutual
  subrenV : {Γ Δ Φ : Cxt} (f : Sub Γ Δ) (g : Ren Δ Φ) {τ : typ}
            (v : value Φ τ) →
            (subV f ∘ renV g) v ≡ subV (subComp f (ren2sub g)) v
  subrenV f g (Num n) = cong Num refl
  subrenV f g (Fun τ e) = cong (Fun τ) (begin
      sub (lifts f) (ren (liftr g) e)
    ≡⟨ subren (lifts f) (liftr g) e ⟩
      sub (subComp (lifts f) (ren2sub (liftr g))) e
    ≡⟨ cong (λ f → sub f e) (liftsrcomp f g) ⟩
      sub (lifts (subComp f (ren2sub g))) e
    ∎)
    where open ≡-Reasoning

  subren : {Γ Δ Φ : Cxt} (f : Sub Γ Δ) (g : Ren Δ Φ) {τ : typ}
           (e : term Φ τ) →
           (sub f ∘ ren g) e ≡ sub (subComp f (ren2sub g)) e
  subren f g (Val v) = cong Val (subrenV f g v)
  subren f g (Var x) = sym (lookslookr f g x)
  subren f g (App e₁ e₂) = cong₂ App (subren f g e₁) (subren f g e₂)

looksid : {Γ : Cxt} {τ : typ} (x : var Γ τ) → looks subId x ≡ Var x
looksid zero = refl
looksid (suc x) = begin
  looks (wks subId) x             ≡⟨ lookswks x subId ⟩
  ren (wkr renId) (looks subId x) ≡⟨ cong (ren (wkr renId)) (looksid x) ⟩
  ren (wkr renId) (Var x)         ≡⟨ refl ⟩
  Var (lookr (wkr renId) x)       ≡⟨ cong Var (lookrwkr renId x) ⟩
  Var (suc (lookr renId x))       ≡⟨ cong (λ x → Var (suc x)) (lookrid x) ⟩
  Var (suc x) ∎
  where open ≡-Reasoning

mutual
  subidV : {Γ : Cxt} {τ : typ} (v : value Γ τ) → subV subId v ≡ v
  subidV (Num n) = cong Num refl
  subidV (Fun τ e) = cong (Fun τ) (subid e)

  subid : {Γ : Cxt} {τ : typ} (e : term Γ τ) → sub subId e ≡ e
  subid (Val v) = cong Val (subidV v)
  subid (Var x) = looksid x
  subid (App e₁ e₂) = cong₂ App (subid e₁) (subid e₂)

sidl : {Γ Δ : Cxt} (vs : Sub Γ Δ) → subComp subId vs ≡ vs
sidl [] = refl
sidl (v ∷ vs) = cong₂ _∷_ (subid v) (sidl vs)

sidr2 : {Γ Δ : Cxt} (vs : Sub Γ Δ) → subComp vs (ren2sub renId) ≡ vs
sidr2 {Δ = []} [] = refl
sidr2 {Δ = x ∷ Δ} (v ∷ vs) = cong (_∷_ v) (begin
    subComp (v ∷ vs) (ren2sub (wkr renId))
  ≡⟨ lemsr vs v renId ⟩
    subComp vs (ren2sub renId)
  ≡⟨ sidr2 vs ⟩
    vs
  ∎)
  where open ≡-Reasoning

lemss : {Γ Δ Φ : Cxt} {σ : typ}
        (vs : Sub Γ Δ) (v : term Γ σ) (ws : Sub Δ Φ) →
        subComp (v ∷ vs) (wks ws) ≡ subComp vs ws
lemss vs v [] = refl
lemss vs v (w ∷ ws) = begin
    sub (v ∷ vs) (ren (wkr renId) w) ∷ subComp (v ∷ vs) (wks ws)
  ≡⟨ cong₂ _∷_ (subren (v ∷ vs) (wkr renId) w) (lemss vs v ws) ⟩
    sub (subComp (v ∷ vs) (ren2sub (wkr renId))) w ∷ subComp vs ws
  ≡⟨ cong (λ g → sub g w ∷ subComp vs ws) (lemsr vs v renId) ⟩
    sub (subComp vs (ren2sub renId)) w ∷ subComp vs ws
  ≡⟨ cong (λ g → sub g w ∷ subComp vs ws) (sidr2 vs) ⟩
    sub vs w ∷ subComp vs ws
  ∎
  where open ≡-Reasoning

ren2sublook : {Γ Δ : Cxt} {τ : typ} (xs : Ren Γ Δ) (y : var Δ τ) →
              Var (lookr xs y) ≡ looks (ren2sub xs) y
ren2sublook (x ∷ xs) zero = refl
ren2sublook (x ∷ xs) (suc y) = ren2sublook xs y

ren2subwk : {Γ Δ : Cxt} {τ : typ} (xs : Ren Γ Δ) →
            ren2sub (wkr {τ = τ} xs) ≡ wks {τ = τ} (ren2sub xs)
ren2subwk [] = refl
ren2subwk (x ∷ xs) = begin
    Var (suc x) ∷ ren2sub (wkr xs)
  ≡⟨ cong₂ (λ xs x → Var (suc x) ∷ xs) (ren2subwk xs) (sym (lookrid x)) ⟩
    Var (suc (lookr renId x)) ∷ wks (ren2sub xs)
  ≡⟨ cong (λ x₁ → Var x₁ ∷ wks (ren2sub xs)) (sym (lookrwkr renId x)) ⟩
    Var (lookr (wkr renId) x) ∷ wks (ren2sub xs)
  ∎
  where open ≡-Reasoning

ren2sublift : {Γ Δ : Cxt} {τ : typ} (xs : Ren Γ Δ) →
              ren2sub (liftr {τ = τ} xs) ≡ lifts {τ = τ} (ren2sub xs)
ren2sublift xs = cong (_∷_ (Var zero)) (ren2subwk xs)

mutual
  ren2subrenV : {Γ Δ : Cxt} {τ : typ} (xs : Ren Γ Δ) (v : value Δ τ) →
                renV xs v ≡ subV (ren2sub xs) v
  ren2subrenV xs (Num n) = cong Num refl
  ren2subrenV xs (Fun τ e) = cong (Fun τ) (begin
    ren (liftr xs) e           ≡⟨ ren2subren (liftr xs) e ⟩
    sub (ren2sub (liftr xs)) e ≡⟨ cong (λ xs → sub xs e) (ren2sublift xs) ⟩
    sub (lifts (ren2sub xs)) e ∎)
    where open ≡-Reasoning

  ren2subren : {Γ Δ : Cxt} {τ : typ} (xs : Ren Γ Δ) (e : term Δ τ) →
               ren xs e ≡ sub (ren2sub xs) e
  ren2subren xs (Val v) = cong Val (ren2subrenV xs v)
  ren2subren xs (Var x) = ren2sublook xs x
  ren2subren xs (App e₁ e₂) = cong₂ App (ren2subren xs e₁) (ren2subren xs e₂)

wkrscomp : {Γ Δ Φ : Cxt} {τ : typ} (xs : Ren Γ Δ) (vs : Sub Δ Φ) →
           subComp (ren2sub (wkr {τ = τ} xs)) vs ≡
           wks {τ = τ} (subComp (ren2sub xs) vs)
wkrscomp xs [] = refl
wkrscomp xs (v ∷ vs) = begin
    sub (ren2sub (wkr xs)) v ∷ subComp (ren2sub (wkr xs)) vs
  ≡⟨ cong₂ _∷_ (sym (ren2subren (wkr xs) v)) (wkrscomp xs vs) ⟩
    ren (wkr xs) v ∷ wks (subComp (ren2sub xs) vs)
  ≡⟨ cong (λ f → ren (wkr f) v ∷ wks (subComp (ren2sub xs) vs))
          (sym (lidr xs)) ⟩
    ren (wkr (renComp renId xs)) v ∷ wks (subComp (ren2sub xs) vs)
  ≡⟨ cong (λ f → ren f v ∷ wks (subComp (ren2sub xs) vs))
          (sym (wkrcomp renId xs)) ⟩
    ren (renComp (wkr renId) xs) v ∷ wks (subComp (ren2sub xs) vs)
  ≡⟨ cong (λ f → f ∷ wks (subComp (ren2sub xs) vs))
          (rencomp (wkr renId) xs v) ⟩
    ren (wkr renId) (ren xs v) ∷ wks (subComp (ren2sub xs) vs)
  ≡⟨ cong (λ f → ren (wkr renId) f ∷ wks (subComp (ren2sub xs) vs))
          (ren2subren xs v) ⟩
    ren (wkr renId) (sub (ren2sub xs) v) ∷ wks (subComp (ren2sub xs) vs)
  ∎
  where open ≡-Reasoning

liftrscomp : {Γ Δ Φ : Cxt} {τ : typ} (xs : Ren Γ Δ) (vs : Sub Δ Φ) →
             subComp (ren2sub (liftr {τ = τ} xs)) (lifts vs) ≡
             lifts {τ = τ} (subComp (ren2sub xs) vs)
liftrscomp xs vs = cong (_∷_ (Var zero)) (begin
    subComp (Var zero ∷ ren2sub (wkr xs)) (wks vs)
  ≡⟨ lemss (ren2sub (wkr xs)) (Var zero) vs ⟩
    subComp (ren2sub (wkr xs)) vs
  ≡⟨ wkrscomp xs vs ⟩
    wks (subComp (ren2sub xs) vs)
  ∎)
  where open ≡-Reasoning

renlooks : {Γ Δ Φ : Cxt} (xs : Ren Γ Δ) (vs : Sub Δ Φ) {σ : typ}
           (x : var Φ σ) →
           (ren xs ∘ looks vs) x ≡ looks (subComp (ren2sub xs) vs) x
renlooks xs (v ∷ vs) zero = ren2subren xs v
renlooks xs (v ∷ vs) (suc x) = renlooks xs vs x

mutual
  rensubV : {Γ Δ Φ : Cxt} (xs : Ren Γ Δ) (vs : Sub Δ Φ) {τ : typ}
            (v : value Φ τ) →
            (renV xs ∘ subV vs) v ≡ subV (subComp (ren2sub xs) vs) v
  rensubV xs vs (Num n) = cong Num refl
  rensubV xs vs (Fun τ e) = cong (Fun τ) (begin
      ren (liftr xs) (sub (lifts vs) e)
    ≡⟨ rensub (liftr xs) (lifts vs) e ⟩
      sub (subComp (ren2sub (liftr xs)) (lifts vs)) e
    ≡⟨ cong (λ xs₁ → sub xs₁ e) (liftrscomp xs vs) ⟩
      sub (lifts (subComp (ren2sub xs) vs)) e
    ∎)
    where open ≡-Reasoning

  rensub : {Γ Δ Φ : Cxt} (xs : Ren Γ Δ) (vs : Sub Δ Φ) {τ : typ}
           (e : term Φ τ) →
           (ren xs ∘ sub vs) e ≡ sub (subComp (ren2sub xs) vs) e
  rensub xs vs (Val v) = cong Val (rensubV xs vs v)
  rensub xs vs (Var x) = renlooks xs vs x
  rensub xs vs (App e₁ e₂) = cong₂ App (rensub xs vs e₁) (rensub xs vs e₂)

lookscomp : {Γ Δ Φ : Cxt} (f : Sub Γ Δ) (g : Sub Δ Φ) {τ : typ}
            (x : var Φ τ) → looks (subComp f g) x ≡ sub f (looks g x)
lookscomp f (v ∷ g) zero = refl
lookscomp f (v ∷ g) (suc x) = lookscomp f g x

ren2subid : {Γ : Cxt} → subId {Γ} ≡ ren2sub renId
ren2subid {[]} = refl
ren2subid {x ∷ Γ} = cong (_∷_ (Var zero)) (begin
  wks subId           ≡⟨ cong wks (ren2subid {Γ}) ⟩
  wks (ren2sub renId) ≡⟨ sym (ren2subwk renId) ⟩
  ren2sub (wkr renId) ∎)
  where open ≡-Reasoning

wksscomp : {Γ Δ Φ : Cxt} {τ : typ} (xs : Sub Γ Δ) (ys : Sub Δ Φ) →
  subComp (wks {τ = τ} xs) ys ≡ wks {τ = τ} (subComp xs ys)
wksscomp xs [] = refl
wksscomp xs (v ∷ ys) = begin
    sub (wks xs) v ∷ subComp (wks xs) ys
  ≡⟨ cong (λ f → sub (wks f) v ∷ subComp (wks xs) ys) (sym (sidl xs)) ⟩
    sub (wks (subComp subId xs)) v ∷ subComp (wks xs) ys
  ≡⟨ cong₂ _∷_ (cong (λ f → sub (wks (subComp f xs)) v) ren2subid)
               (wksscomp xs ys) ⟩
    sub (wks (subComp (ren2sub renId) xs)) v ∷ wks (subComp xs ys)
  ≡⟨ cong (λ f → sub f v ∷ wks (subComp xs ys)) (sym (wkrscomp renId xs)) ⟩
    sub (subComp (ren2sub (wkr renId)) xs) v ∷ wks (subComp xs ys)
  ≡⟨ cong (λ f → f ∷ wks (subComp xs ys)) (sym (rensub (wkr renId) xs v)) ⟩
    (ren (wkr renId) (sub xs v) ∷ wks (subComp xs ys))
  ∎
  where open ≡-Reasoning

sidr : {Γ Φ : Cxt} (xs : Sub Γ Φ) → subComp xs subId ≡ xs
sidr xs = begin
  subComp xs subId           ≡⟨ cong (subComp xs) ren2subid ⟩
  subComp xs (ren2sub renId) ≡⟨ sidr2 xs ⟩
  xs                         ∎
  where open ≡-Reasoning

liftscomp : {Γ Δ Φ : Cxt} {τ : typ} (xs : Sub Γ Δ) (ys : Sub Δ Φ) →
  subComp (lifts {τ = τ} xs) (lifts ys) ≡ lifts {τ = τ} (subComp xs ys)
liftscomp xs ys = cong (_∷_ (Var zero)) (begin
  subComp (lifts xs) (wks ys) ≡⟨ lemss (wks xs) (Var zero) ys ⟩
  subComp (wks xs) ys         ≡⟨ wksscomp xs ys ⟩
  wks (subComp xs ys)         ∎)
  where open ≡-Reasoning

mutual
  subcompV : {Γ Δ Φ : Cxt} (vs : Sub Γ Δ) (ws : Sub Δ Φ) {τ : typ}
             (v : value Φ τ) → subV (subComp vs ws) v ≡ (subV vs ∘ subV ws) v
  subcompV vs ws (Num n) = cong Num refl
  subcompV vs ws (Fun τ e) = cong (Fun τ) (begin
      sub (lifts (subComp vs ws)) e
    ≡⟨ cong (λ xs → sub xs e) (sym (liftscomp vs ws)) ⟩
      sub (subComp (lifts vs) (lifts ws)) e
    ≡⟨ subcomp (lifts vs) (lifts ws) e ⟩
      sub (lifts vs) (sub (lifts ws) e)
    ∎)
    where open ≡-Reasoning

  subcomp : {Γ Δ Φ : Cxt} (vs : Sub Γ Δ) (ws : Sub Δ Φ) {σ : typ}
            (e : term Φ σ) → sub (subComp vs ws) e ≡ (sub vs ∘ sub ws) e
  subcomp vs ws (Val v) = cong Val (subcompV vs ws v)
  subcomp vs ws (Var x) = lookscomp vs ws x
  subcomp vs ws (App e₁ e₂) = cong₂ App (subcomp vs ws e₁) (subcomp vs ws e₂)

renrenwkr : {Γ Δ : Cxt} (xs : Ren Γ Δ) {τ σ : typ}
            (e : term Δ τ) (x : var Γ σ) →
            ren (x ∷ xs) (ren (wkr renId) e) ≡ ren xs e
renrenwkr xs e x = begin
    ren (x ∷ xs) (ren (wkr renId) e)
  ≡⟨ sym (rencomp (x ∷ xs) (wkr renId) e) ⟩
    ren (renComp (x ∷ xs) (wkr renId)) e
  ≡⟨ cong (λ l → ren l e) (lemrr xs x renId) ⟩
    ren (renComp xs renId) e
  ≡⟨ cong (λ l → ren l e) (ridr xs) ⟩
    ren xs e
  ∎
  where open ≡-Reasoning

sub0sub : {Γ Δ : Cxt} {τ₁ τ₂ : typ}
          (v : term Δ τ₂) (vs : Sub Δ Γ) (e : term (τ₂ ∷ Γ) τ₁) →
          sub0 v (sub (Var zero ∷ wks vs) e) ≡ sub (v ∷ vs) e
sub0sub v vs e = begin
    sub0 v (sub (Var zero ∷ wks vs) e)
  ≡⟨ refl ⟩
    sub0 v (sub (lifts vs) e)
  ≡⟨ refl ⟩
    sub (v ∷ subId) (sub (lifts vs) e)
  ≡⟨ sym (subcomp (v ∷ subId) (lifts vs) e) ⟩
    sub (subComp (v ∷ subId) (lifts vs)) e
  ≡⟨ refl ⟩
    sub (v ∷ subComp (v ∷ subId) (wks vs)) e
  ≡⟨ cong (λ vs₁ → sub (v ∷ vs₁) e) (lemss subId v vs) ⟩
    sub (v ∷ subComp subId vs) e
  ≡⟨ cong (λ vs → sub (v ∷ vs) e) (sidl vs) ⟩
    sub (v ∷ vs) e
  ∎
  where open ≡-Reasoning

rensub0 : {Γ Δ : Cxt} (xs : Ren Γ Δ) {τ₁ τ₂ : typ}
          (u : term Δ τ₂) (e : term (τ₂ ∷ Δ) τ₁) →
          ren xs (sub (u ∷ subId) e) ≡
          sub (ren xs u ∷ subId) (ren (liftr xs) e)
rensub0 xs u e = begin
    ren xs (sub (u ∷ subId) e)
  ≡⟨ ren2subren xs (sub (u ∷ subId) e) ⟩
    sub (ren2sub xs) (sub (u ∷ subId) e)
  ≡⟨ sym (subcomp (ren2sub xs) (u ∷ subId) e) ⟩
    sub (subComp (ren2sub xs) (u ∷ subId)) e
  ≡⟨ refl ⟩
    sub (sub (ren2sub xs) u ∷ subComp (ren2sub xs) subId) e
  ≡⟨ cong (λ l → sub (sub (ren2sub xs) u ∷ l) e) (sidr (ren2sub xs)) ⟩
    sub (sub (ren2sub xs) u ∷ ren2sub xs) e
  ≡⟨ cong (λ v → sub (v ∷ ren2sub xs) e) (sym (ren2subren xs u)) ⟩
    sub (ren xs u ∷ ren2sub xs) e
  ≡⟨ cong (λ l → sub (ren xs u ∷ l) e) (sym (sidl (ren2sub xs))) ⟩
    sub (ren xs u ∷ subComp subId (ren2sub xs)) e
  ≡⟨ cong (λ l → sub (ren xs u ∷ l) e)
          (sym (lemsr subId (ren xs u) xs)) ⟩
    sub (ren xs u ∷ subComp (ren xs u ∷ subId) (ren2sub (wkr xs))) e
  ≡⟨ cong (λ l → sub (ren xs u ∷ subComp (ren xs u ∷ subId) l) e)
          (ren2subwk xs) ⟩
    sub (ren xs u ∷ subComp (ren xs u ∷ subId) (wks (ren2sub xs))) e
  ≡⟨ refl ⟩
    sub (subComp (ren xs u ∷ subId) (lifts (ren2sub xs))) e
  ≡⟨ subcomp (ren xs u ∷ subId) (lifts (ren2sub xs)) e ⟩
    sub (ren xs u ∷ subId) (sub (lifts (ren2sub xs)) e)
  ≡⟨ cong (λ l → sub (ren xs u ∷ subId) (sub l e)) (sym (ren2sublift xs)) ⟩
    sub (ren xs u ∷ subId) (sub (ren2sub (liftr xs)) e)
  ≡⟨ cong (sub (ren xs u ∷ subId)) (sym (ren2subren (liftr xs) e)) ⟩
    sub (ren xs u ∷ subId) (ren (liftr xs) e)
  ∎
  where open ≡-Reasoning

mutual
  embedNe-ren : {Γ Δ : Cxt} (xs : Ren Γ Δ) {τ : typ} (ne : ne Δ τ) → 
                embedNe (renNe xs ne) ≡ ren xs (embedNe ne)
  embedNe-ren xs (Var x) = refl
  embedNe-ren xs (App ne nf) =
    cong₂ App (embedNe-ren xs ne) (embedNf-ren xs nf)

  embedNf-ren : {Γ Δ : Cxt} (xs : Ren Γ Δ) {τ : typ} (nf : nf Δ τ) → 
                embedNf (renNf xs nf) ≡ ren xs (embedNf nf)
  embedNf-ren xs (Ne ne) = embedNe-ren xs ne
  embedNf-ren xs (Num n) = refl
  embedNf-ren xs (Fun τ nf) =
    cong Val (cong (Fun τ) (embedNf-ren (liftr xs) nf))

embedNe-weak : {Γ : Cxt} {τ : typ} (σ : typ) (ne : ne Γ τ) → 
               embedNe (weakNe σ ne) ≡ weak σ (embedNe ne)
embedNe-weak σ ne = embedNe-ren (wkr renId) ne

embedNf-weak : {Γ : Cxt} {τ : typ} (σ : typ) (nf : nf Γ τ) → 
               embedNf (weakNf σ nf) ≡ weak σ (embedNf nf)
embedNf-weak σ nf = embedNf-ren (wkr renId) nf

mutual
  isNe-renV : {Γ Δ : Cxt} (xs : Ren Γ Δ) {τ : typ} (v : value Δ τ) → 
             isNeV v → isNeV (renV xs v)
  isNe-renV xs (Num n) p = tt
  isNe-renV xs (Fun τ e) ()

  isNe-ren : {Γ Δ : Cxt} (xs : Ren Γ Δ) {τ : typ} (e : term Δ τ) → 
             isNe e → isNe (ren xs e)
  isNe-ren xs (Val v) p = isNe-renV xs v p
  isNe-ren xs (Var x) p = tt
  isNe-ren xs (App e₁ e₂) (p₁ , p₂) =
    (isNe-ren xs e₁ p₁ , isNf-ren xs e₂ p₂)

  isNf-renV : {Γ Δ : Cxt} (xs : Ren Γ Δ) {τ : typ} (v : value Δ τ) → 
             isNfV v → isNfV (renV xs v)
  isNf-renV xs (Num n) p = tt
  isNf-renV xs (Fun τ e) p = isNf-ren (liftr xs) e p

  isNf-ren : {Γ Δ : Cxt} (xs : Ren Γ Δ) {τ : typ} (e : term Δ τ) → 
             isNf e → isNf (ren xs e)
  isNf-ren xs (Val v) p = isNf-renV xs v p
  isNf-ren xs (Var x) p = tt
  isNf-ren xs (App e₁ e₂) (p₁ , p₂) =
    (isNe-ren xs e₁ p₁ , isNf-ren xs e₂ p₂)

isNe-weak : {Γ : Cxt} {τ : typ} {σ : typ} (e : term Γ τ) → 
            isNe e → isNe (weak σ e)
isNe-weak e p = isNe-ren (wkr renId) e p

isNf-weak : {Γ : Cxt} {τ : typ} {σ : typ} (e : term Γ τ) → 
            isNf e → isNf (weak σ e)
isNf-weak e p = isNf-ren (wkr renId) e p

{-
wkr-Δ : {Γ : Cxt} → (Δ : Cxt) → Ren (Δ ++ Γ) Δ
wkr-Δ [] = []
wkr-Δ (_ ∷ Δ) = liftr (wkr-Δ Δ)

wks-Δ : {Γ : Cxt} → (Δ : Cxt) → Sub (Δ ++ Γ) Δ
wks-Δ [] = []
wks-Δ (_ ∷ Δ) = lifts (wks-Δ Δ)

looksr-wksr : ∀ {τ Δ} (x : var Δ τ) {Γ} →
              looks (wks-Δ {Γ} Δ) x ≡ Var (lookr (wkr-Δ Δ) x)
looksr-wksr {Δ = []} ()
looksr-wksr {Δ = τ ∷ Δ} zero = refl
looksr-wksr {Δ = τ ∷ Δ} (suc x) = begin
    looks (wks (wks-Δ Δ)) x
  ≡⟨ lookswks x (wks-Δ Δ) ⟩
    ren (wkr renId) (looks (wks-Δ Δ) x)
  ≡⟨ cong (ren (wkr renId)) (looksr-wksr x) ⟩
    ren (wkr renId) (Var (lookr (wkr-Δ Δ) x))
  ≡⟨ refl ⟩
    Var (lookr (wkr renId) (lookr (wkr-Δ Δ) x))
  ≡⟨ cong Var (lookrwkr renId (lookr (wkr-Δ Δ) x) ) ⟩
    Var (suc (lookr renId (lookr (wkr-Δ Δ) x)))
  ≡⟨ cong (λ x → Var (suc x)) (lookrid (lookr (wkr-Δ Δ) x)) ⟩
    Var (suc (lookr (wkr-Δ Δ) x))
  ≡⟨ cong Var (sym (lookrwkr (wkr-Δ Δ) x)) ⟩
    Var (lookr (wkr (wkr-Δ Δ)) x)
  ∎
  where open ≡-Reasoning
-}