[Agda] Re: Associativity for free!

[Alan Jeffrey]

Fair enough, if you phrase the Kripke structure in terms of subcontext 
inclusion rather than context extension, then I can see how it goes 
through without worrying about associativity.

A.

On 11/05/2011 05:47 AM, James Chapman wrote:
> I haven't tried an NBE proof with the version of renaming and
> substitution I posted yesterday. I have done something similar during
> my PhD. I used OPEs in the end (which I described early in this thread
> and Randy pointed to copious prior art).
>
> data OPE : Con ->  Con ->  Set where
>    done : OPE ε ε
>    keep : forall {Γ Δ} σ ->  OPE Γ Δ ->  OPE (Γ<  σ) (Δ<  σ)
>    skip : forall {Γ Δ} σ ->  OPE Γ Δ ->  OPE (Γ<  σ) Δ
>
> I had exactly this problem as you, for me it was with kripke logical
> predicates. Instead of defining the kripke-like part as saying:
>
> /a strongly computable function is one that given an strongly
> computable  argument in an extended context, and after weakening the
> function so that it is in the same context, will give a strongly
> computable result./
>
> I defined it using the kripke like bit of strong computability roughly
> as follows:
>
> SCV : forall {Γ σ} ->  Val Γ σ ->  Set
> SCV {Γ} {σ ⇒ τ} v       = forall {B}(f : OPE B Γ)(a : Val B σ) ->  SCV a ->
>    SCV  {B} {τ} (oapp f v $$ a)
> SCV ...
>
> i.e. /a strongly computable function is one that given a strongly
> computable argument in an arbitrary context B, and a order preserving
> embedding from the functions context Γ into B, and after applying the
> embedding to the function, we get a strongly computable result./
>
> The context B is arbitrary but OPE Γ B is only inhabited if B is
> 'larger'. applying oapp twice (composing them) doesn't lead to the
> same problem as your weaken as the source and target contexts are just
> variables, just like composing functions. OPEs are exactly the
> renamings which don't shrink the context and hence useful here.
>
> Regards,
>
> James
>
> On Fri, Nov 4, 2011 at 7:55 PM, Alan Jeffrey<ajeffrey at bell-labs.com>  wrote:
>> 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
>>