[Agda] Re: Associativity for free!

[James Chapman]

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
>