[Agda] Associativity for free!

[James Chapman]

Hi Alan, 

I too have encountered this problem, rather than tackling it head on here are two ways of tiptoeing around it.

1. A trivial solution for your example is simply to make _++_ associate to the left:

data List (X : Set) : Set where
 []   : List X
 _::_ : X → List X → List X

_++_ : ∀{X} → List X → List X → List X
[]        ++ xs' = xs'
(x :: xs) ++ xs' = x :: (xs ++ xs')

infixl 5 _++_

postulate P : ∀{X} → List X → Set

postulate weakening : ∀ {A} (as bs cs : List A) →
                      P (as ++ cs) → P (as ++ bs ++ cs)

weaken2 : ∀ {A} (as bs cs ds : List A) →
   P (as ++ bs ++ ds) → P (as ++ bs ++ cs ++ ds)
weaken2 as bs cs ds p = weakening (as ++ bs) cs ds p

This may sound silly and perhaps you might somewhere else need append to associate to the right. Nisse told me that in a recent implementation of a dependently typed lambda calculus he defined both versions and didn't end up needing them both at the same time. Do you need both at the same time?

2. I guess you run into the this problem where ++ is an operation on contexts right? Another solution I learnt from Conor (exercise 15, his AFP notes http://www.strictlypositive.org/epigram-notes.ps.gz) is simply to avoid it. Instead of giving weakening this type, give a first order presentation of weakenings (functions from a context to the same context with more stuff chucked in arbitrary places). For  lists this function space would be the following inductively defined sublist relation:

data _≤_ {X : Set} : List X → List X → Set where
  done : [] ≤ []
  keep : ∀{x}{xs xs'} → xs ≤ xs' → (x :: xs) ≤ (x :: xs')
  skip : ∀{x}{xs xs'} → xs ≤ xs' → xs ≤ (x :: xs')

Then, weakening would be something like:

weakening : ∀{X}{xs xs' : List X} → P xs → xs ≤ xs' → P xs'

By doing this ++ never appears in the types, so we don't have to use subst. I used this technique (called order preserving embeddings) in chapter 4 of my thesis (http://www.cs.ioc.ee/~james/papers/thesis.pdf ) and it was much more pleasant than using ++ as we did in our Big-step normalization paper (http://www.cs.ioc.ee/~james/papers/tait2.pdf) on which this chapter was based.

Best wishes,

James