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)))