[Agda] Associativity for free!

[James Chapman]

I should have said this follows the structure of Altenkirch and Reus' proof for untyped terms.

Also, this agda proof is described in the accepted draft paper "Relative Monads formalized" (http://www.cs.ioc.ee/~james/Publications.html)  which I should really finish, well, today.

James

On Nov 4, 2011, at 1:29 PM, James Chapman wrote:

> Dear Alan + all,
> 
> On Wed, Nov 2, 2011 at 6:26 PM, Alan Jeffrey <ajeffrey at bell-labs.com> wrote:
>> My original motivation for "associativity for free" was properties about
>> lambda-calculi. I've now worked through some of the details, and here is the
>> syntax of the simply-typed lambda-calculus.
> 
> For contrast, here's renaming and substitution for well typed lambda
> terms. Renamings are just functions from variables to variables,
> substitutions are just functions form variables to terms. No clever
> representations here, no clever getting them both as a instance of a
> more general operation, I just wanted to use the interface to
> substitution suggested by the (relative) monadic nature of well-typed
> terms. The proof is a simplification of the paper proof in Altenkirch
> and Reus' paper "Monadic presentations of lambda terms using
> generalized inductive types" and follows the approximately the same
> structure. The development goes up to proving that the substitution
> operation commutes with composition of substitutions (just composition
> of functions) -- the third monad law. It's about 170 lines in all
> including the utilities prelude.
> 
> module WellTypedTerms where
> 
> -- Utilities
> data _≅_ {A : Set} : {A' : Set} → A → A' → Set where
>  refl : {a : A} → a ≅ a
> 
> trans : ∀{A A' A''}{a : A}{a' : A'}{a'' : A''} → a ≅ a' → a' ≅ a'' → a ≅ a''
> trans refl p = p
> 
> sym : ∀{A A'}{a : A}{a' : A'} → a ≅ a' → a' ≅ a
> sym refl = refl
> 
> resp : ∀{A}{B : A → Set}(f : ∀ a → B a){a a' : A} → a ≅ a' → f a ≅ f a'
> resp f refl = refl
> 
> resp2 : ∀{A}{B : A → Set}{C : (x : A) → B x → Set}(f : (x : A)(y : B
> x) → C x y){a a' : A} → a ≅ a' → {b : B a}{b' : B a'} → b ≅ b' → f a b
> ≅ f a' b'
> resp2 f refl refl = refl
> 
> _•_ : {A : Set}{B : A → Set}{C : (a : A) → B a → Set} →
>      (∀{a} b → C a b) → (g : (∀ a → B a)) → ∀ a → C a (g a)
> f • g = λ a → f (g a)
> 
> id : {A : Set} → A → A
> id a = a
> 
> postulate iext : {A : Set}{B B' : A → Set}{f : ∀ {a} → B a}{g : ∀{a} → B' a} →
>                 (∀ a → f {a} ≅ g {a}) →
>                 _≅_ { {a : A} → B a} { {a : A} → B' a} f g
> 
> postulate ext : {A : Set}{B B' : A → Set}{f : ∀ a → B a}{g : ∀ a → B' a} →
>                (∀ a → f a ≅ g a) → f ≅ g
> 
> --Well type lambda terms
> 
> data Ty : Set where
>  ι   : Ty
>  _⇒_ : Ty → Ty → Ty
> 
> data Con : Set where
>  ε   : Con
>  _<_ : Con → Ty → Con
> 
> data Var : Con → Ty → Set where
>  vz : ∀{Γ σ} → Var (Γ < σ) σ
>  vs : ∀{Γ σ τ} → Var Γ σ → Var (Γ < τ) σ
> 
> data Tm : Con → Ty → Set where
>  var : ∀{Γ σ} → Var Γ σ → Tm Γ σ
>  app : ∀{Γ σ τ} → Tm Γ (σ ⇒ τ) → Tm Γ σ → Tm Γ τ
>  lam : ∀{Γ σ τ} → Tm (Γ < σ) τ → Tm Γ (σ ⇒ τ)
> 
> -- Renaming
> 
> Ren : Con → Con → Set
> Ren Γ Δ = ∀ {σ} → Var Γ σ → Var Δ σ
> 
> renId : ∀{Γ} → Ren Γ Γ
> renId = id
> 
> renComp : ∀{B Γ Δ} → Ren Γ Δ → Ren B Γ → Ren B Δ
> renComp f g = f • g
> 
> wk : ∀{Γ Δ σ} → Ren Γ Δ → Ren (Γ < σ) (Δ < σ)
> wk f vz     = vz
> wk f (vs i) = vs (f i)
> 
> ren : ∀{Γ Δ} → Ren Γ Δ → ∀ {σ} → Tm Γ σ → Tm Δ σ
> ren f (var x)   = var (f x)
> ren f (app t u) = app (ren f t) (ren f u)
> ren f (lam t)   = lam (ren (wk f) t)
> 
> wkid : ∀{Γ σ τ}(x : Var (Γ < τ) σ) → wk renId x ≅ renId x
> wkid vz     = refl
> wkid (vs x) = refl
> 
> renid : ∀{Γ σ}(t : Tm Γ σ) → ren renId t ≅ id t
> renid (var x)   = refl
> renid (app t u) = resp2 app (renid t) (renid u)
> renid (lam t) = resp lam (trans (resp (λ (f : Ren _ _) → ren f t)
>                                      (iext (λ _ → ext wkid)))
>                                (renid t))
> 
> wkcomp : ∀ {B Γ Δ}(f : Ren Γ Δ)(g : Ren B Γ){σ τ}(x : Var (B < σ) τ) →
>            wk (renComp f g) x ≅ renComp (wk f) (wk g) x
> wkcomp f g vz     = refl
> wkcomp f g (vs i) = refl
> 
> rencomp : ∀ {B Γ Δ}(f : Ren Γ Δ)(g : Ren B Γ){σ}(t : Tm B σ) →
>            ren (renComp f g) t ≅ (ren f • ren g) t
> rencomp f g (var x)   = refl
> rencomp f g (app t u) = resp2 app (rencomp f g t) (rencomp f g u)
> rencomp f g (lam t)   = resp lam (trans (resp (λ (f : Ren _ _) → ren f t)
>                                              (iext λ _ → ext (wkcomp f g)))
>                                        (rencomp (wk f) (wk g) t))
> 
> -- Substitutions
> 
> Sub : Con → Con → Set
> Sub Γ Δ = ∀{σ} → Var Γ σ → Tm Δ σ
> 
> lift : ∀{Γ Δ σ} → Sub Γ Δ → Sub (Γ < σ) (Δ < σ)
> lift f vz     = var vz
> lift f (vs x) = ren vs (f x)
> 
> sub : ∀{Γ Δ} → Sub Γ Δ → ∀{σ} → Tm Γ σ → Tm Δ σ
> sub f (var x)   = f x
> sub f (app t u) = app (sub f t) (sub f u)
> sub f (lam t)   = lam (sub (lift f) t)
> 
> subId : ∀{Γ} → Sub Γ Γ
> subId = var
> 
> subComp : ∀{B Γ Δ} → Sub Γ Δ → Sub B Γ → Sub B Δ
> subComp f g = sub f • g
> 
> liftid : ∀{Γ σ τ}(x : Var (Γ < σ) τ) → lift subId x ≅ subId x
> liftid vz     = refl
> liftid (vs x) = refl
> 
> -- first monad law, the second holds definitionally
> subid : ∀{Γ σ}(t : Tm Γ σ) → sub subId t ≅ id t
> subid (var x)   = refl
> subid (app t u) = resp2 app (subid t) (subid u)
> subid (lam t)   = resp lam (trans (resp (λ (f : Sub _ _) → sub f t)
>                                        (iext λ _ → ext liftid))
>                                  (subid t))
> 
> liftwk : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Ren B Γ){σ τ}(x : Var (B < σ) τ) →
>            (lift f • wk g) x ≅ lift (f • g) x
> liftwk f g vz     = refl
> liftwk f g (vs x) = refl
> 
> subren : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Ren B Γ){σ}(t : Tm B σ) →
>         (sub f • ren g) t ≅ sub (f • g) t
> subren f g (var x)   = 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) (wk g) t)
>                                       (resp (λ (f : Sub _ _) → sub f t)
>                                             (iext λ _ → ext (liftwk f g))))
> 
> renwklift : ∀{B Γ Δ}(f : Ren Γ Δ)(g : Sub B Γ){σ τ}(x : Var (B < σ) τ) →
>               (ren (wk f) • lift g) x ≅ lift (ren f • g) x
> renwklift f g vz     = refl
> renwklift f g (vs x) = trans (sym (rencomp (wk f) vs (g x)))
>                                (rencomp vs f (g x))
> 
> rensub : ∀{B Γ Δ}(f : Ren Γ Δ)(g : Sub B Γ){σ}(t : Tm B σ) →
>         (ren f •  sub g) t ≅ sub (ren f • g) t
> rensub f g (var x)   = 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 (wk f) (lift g) t)
>                                       (resp (λ (f : Sub _ _) → sub f t)
>                                             (iext λ _ →
>                                               ext (renwklift f g))))
> 
> liftcomp : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Sub B Γ){σ τ}(x : Var (B < σ) τ) →
>           lift (subComp f g) x ≅ subComp (lift f) (lift g) x
> liftcomp f g vz     = refl
> liftcomp f g (vs x) = trans (rensub vs f (g x))
>                            (sym (subren (lift f) vs (g x)))
> 
> 
> -- third monad law
> subcomp : ∀{B Γ Δ}(f : Sub Γ Δ)(g : Sub B Γ){σ}(t : Tm B σ) →
>          sub (subComp f g) t ≅ (sub f • sub g) t
> subcomp f g (var x)   = refl
> subcomp f g (app t u) = resp2 app (subcomp f g t) (subcomp f g u)
> subcomp f g (lam t)   = resp lam (trans (resp (λ (f : Sub _ _) → sub f t)
>                                              (iext λ _ → ext (liftcomp f g)))
>                                        (subcomp (lift f) (lift g) t))
> 
> Regards,
> 
> James