[Agda] a puzzle about pattern matching

[Aaron Stump]

Dear Agda community,

For a while, I have wondered how to get Agda to understand that in a set 
of equations defining some function, the patterns in earlier equations 
must have failed to match, if we find ourselves in a later equation.  
This could save a lot of repetitious equations.  Below I have a small 
example.  It is completely self-contained (I have included the 
definitions I am using from our Iowa Agda Library). The puzzle is, can 
you prove lem in something closer to 3 equations, rather than the eight 
given?  Failing that, can you at least abstract out the eight equations 
in some reasonably modular way? The problem is that action is defined 
using default patterns, rather than explicit alternate patterns.  The 
proof of lem cannot just use default patterns, as partial evaluation of 
applications of action requires that the patterns be explicit.

While this is obviously an artificial example, I find this issue comes 
up rather frequently.

Cheers,
Aaron

module puzzle where

{----------- start standard definitions from IAL ---------------------}

data _≡_ {ℓ} {A : Set ℓ} (x : A) : A → Set ℓ where
   refl : x ≡ x

{-# BUILTIN EQUALITY _≡_ #-}
{-# BUILTIN REFL refl #-}

import Agda.Primitive

open Agda.Primitive public
   using    (Level ; _⊔_ ; lsuc ; lzero)

level = Level

data ⊥ : Set where

⊥-elim : ⊥ → ∀ {P : Set} → P
⊥-elim ()

¬_ : ∀{ℓ}(x : Set ℓ) → Set ℓ
¬ x = x → ⊥

_≢_ : ∀ {ℓ}{A : Set ℓ} → A → A → Set ℓ
x ≢ y = ¬ (x ≡ y)

{----------- end standard definitions from IAL ---------------------}

data A : Set where
   a : A
   d : A → A → A → A

action : A → A
action (d a a a) = (d a a a)
action (d x y z) = a
action a = a

lem : ∀(x : A) → x ≢ d a a a → action x ≡ a
lem (d a a a) p = ⊥-elim (p refl)
lem (d a a (d z z₁ z₂)) p = refl
lem (d a (d y y₁ y₂) a) p = refl
lem (d a (d y y₁ y₂) (d z z₁ z₂)) p = refl
lem (d (d x x₁ x₂) a a) p = refl
lem (d (d x x₁ x₂) a (d z z₁ z₂)) p = refl
lem (d (d x x₁ x₂) (d y y₁ y₂) a) p = refl
lem (d (d x x₁ x₂) (d y y₁ y₂) (d z z₁ z₂)) p = refl
lem a p = refl