module LamRenSub where

-- first we define some equality machinery to use later

-- Homogeneous equality will suffice for this.

data _≅_ {A : Set} : A → A → Set where
  refl : {a : A} → a ≅ a

-- we will be reasoning about functos and hence extensionality is useful

postulate ext : {A B : Set}{f g : A → B} → (∀ a → f a ≅ g a) → f ≅ g 

-- it is useful to be able to peal off functions if the same one
-- appears on the outside of both sides of the equation we are trying
-- to prove.

resp : {A B : Set}(f : A → B){a a' : A} → a ≅ a' → f a ≅ f a'
resp f refl = refl 

resp2 : {A B C : Set}(f : A → B → C){a a' : A} → a ≅ a' → {b b' : B} → b ≅ b' → f a b ≅ f a' b'
resp2 f refl refl = refl

-- transitity and symmetry are derivable

trans : {A : Set}{a a' a'' : A} → a ≅ a' → a' ≅ a'' → a ≅ a''
trans refl refl = refl

sym : {A : Set}{a a' : A} → a ≅ a' → a' ≅ a
sym refl = refl

-- The language of well-scoped lambda terms

data Nat : Set where
  z : Nat
  s : Nat → Nat

data Fin : Nat → Set where
  z : ∀{n} → Fin (s n)
  s : ∀{n} → Fin n → Fin (s n)

data Lam : Nat → Set where
  var : ∀{n} → Fin n → Lam n
  app : ∀{n} → Lam n → Lam n → Lam n
  lam : ∀{n} → Lam (s n) → Lam n

-- Renamings

Ren : Nat → Nat → Set
Ren m n = Fin m → Fin n

-- Weakening a renaming (to push it under a lambda)

intro : ∀{m n} → Ren m n → Ren (s m) (s n)
intro f z     = z
intro f (s i) = s (f i)

-- Performing a renaming on an expression

ren : ∀{m n} → Ren m n → Lam m → Lam n
ren f (var i)   = var (f i)
ren f (app t u) = app (ren f t) (ren f u)
ren f (lam t)   = lam (ren (intro f) t)

-- Identity renaming

renId : ∀{n} → Ren n n
renId i = i

-- Composition of renamings

renComp : ∀{m n o} → Ren n o → Ren m n → Ren m o
renComp f g i = f (g i)

-- we prove that intro is an endofunctor

introid : ∀{n}(i : Fin (s n)) → intro renId i ≅ i
introid z     = refl
introid (s i) = refl

introcomp : ∀{m n o}(i : Fin (s m))(f : Ren n o)(g : Ren m n) → intro (renComp f g) i ≅ intro f (intro g i)
introcomp z     f g = refl
introcomp (s i) f g = refl

-- we prove that renamings is a functor

renid : ∀{n}(t : Lam n) → ren renId t ≅ t
renid (var i)   = refl
renid (app t u) = resp2 app (renid t) (renid u)
renid (lam t)   = resp lam (trans (resp (λ f → ren f t) (ext introid)) (renid t))

rencomp : ∀{m n o}(t : Lam m)(f : Ren n o)(g : Ren m n) → ren (renComp f g) t ≅ ren f (ren g t)
rencomp (var i)   f g = refl
rencomp (app t u) f g = resp2 app (rencomp t f g) (rencomp u f g)
rencomp (lam t)   f g = resp lam (trans (resp (λ f → ren f t) (ext (λ i → introcomp i f g))) 
                                        (rencomp t (intro f) (intro g)))

-- Substitutions

Sub : Nat → Nat → Set
Sub m n = Fin m → Lam n

-- Weaken a substitution to push it under a lambda

lift : ∀{m n} → Sub m n → Sub (s m) (s n)
lift f z     = var z
lift f (s i) = ren s (f i)

-- Perform substitution on an expression

sub : ∀{m n} → Sub m n → Lam m → Lam n
sub f (var i)   = f i
sub f (app t u) = app (sub f t) (sub f u)
sub f (lam t)   = lam (sub (lift f) t)

-- Identity substitution

subId : ∀{n} → Sub n n
subId = var

-- Composition of substitutions 

subComp : ∀{m n o} → Sub n o → Sub m n → Sub m o
subComp f g i = sub f (g i)

-- lift is an endofunctor on substitutions and sub is a functor, we
-- need some auxilary lemmas for the composition cases

-- the conditions for identity are easy

liftid : ∀{n}(i : Fin (s n)) → lift var i ≅ var i
liftid z     = refl
liftid (s i) = refl

subid : ∀{n}(t : Lam n) → sub var t ≅ t
subid (var i)   = refl
subid (app t u) = resp2 app (subid t) (subid u)
subid (lam t)   = resp lam (trans (resp (λ f → sub f t) (ext liftid)) (subid t))  

_•_ : {A B C : Set} → (B → C) → (A → B) → A → C
f • g = λ a → f (g a)

-- for composition of subs (subcomp) and lifts (liftcomp) we need two
-- lemmas about how renaming and subs interact for these two lemmas we
-- need two lemmas about how lift and intro interact.

liftintro : ∀{m n o}(f : Fin n → Lam o)(g : Fin m → Fin n)(i : Fin (s m)) → 
       lift f (intro g i) ≅ lift (f • g) i
liftintro f g z     = refl
liftintro f g (s i) = refl

subren : ∀{m n o}(f : Fin n → Lam o)(g : Fin m → Fin n)(t : Lam m) → 
                 sub f (ren g t) ≅ sub (f • g) t
subren f g (var i)   = refl
subren f g (app t u) = resp2 app (subren f g t) (subren f g u)
subren f g (lam t)   = resp lam (trans (subren (lift f) (intro g) t)
                                       (resp (λ f → sub f t) (ext (liftintro f g))))

renintrolift : ∀{m n o}(f : Fin n → Fin o)(g : Fin m → Lam n)(i : Fin (s m)) → 
 ren (intro f) (lift g i) ≅ lift (ren f • g) i
renintrolift f g z     = refl
renintrolift f g (s i) = trans (sym (rencomp (g i) (intro f) s)) (rencomp (g i) s f)

rensub : ∀{m n o}(f : Fin n → Fin o)(g : Fin m → Lam n)(t : Lam m) →
                 ren f (sub g t) ≅ sub (ren f • g) t
rensub f g (var i)   = refl
rensub f g (app t u) = resp2 app (rensub f g t) (rensub f g u)
rensub f g (lam t)   = resp lam (trans (rensub (intro f) (lift g) t)
                                       (resp (λ f → sub f t) 
                                             (ext (renintrolift f g))))

liftcomp : ∀{m n o}(i : Fin (s m))(f : Sub n o)(g : Sub m n) → lift (subComp f g) i ≅ sub (lift f) (lift g i)
liftcomp z     f g = refl
liftcomp (s i) f g = trans (rensub s f (g i))
                           (sym (subren (lift f) s (g i)))

subcomp : ∀{m n o}(t : Lam m)(f : Sub n o)(g : Sub m n) → sub (subComp f g) t ≅ sub f (sub g t)
subcomp (var i)   f g = refl
subcomp (app t u) f g = resp2 app (subcomp t f g) (subcomp u f g)
subcomp (lam t)   f g = resp lam (trans (resp (λ f → sub f t) (ext (λ i → liftcomp i f g))) (subcomp t (lift f) (lift g)))