[Agda] Re: Associativity for free!

[Alan Jeffrey]

OK, that's pretty cool. The nasty case which hit me was proving 
properties like "weakening of weakening is weakening":

   weaken* A (weaken* B M) ≡ weaken* (A ++ B) M

which you can't even state without putting in some explicit associators.

This came up in the context of normalization by evaluation, which needs 
a Kripke-like structure which extends the context on every function 
application. Associators were really getting in the way, as I was 
needing to prove a bunch of coherence properties. Have you tried getting 
an NBE proof to go through in your setting?

A.

On 11/04/2011 06:29 AM, 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