[Agda] a puzzle about pattern matching

[Jacques Carette]

It can be done in 5 lines:
lem : ∀(x : A) → x ≢ d a a a → action x ≡ a
lem a p = refl
lem (d a a a) p = ⊥-elim (p refl)
lem (d a a (d x₂ x₃ x₄)) p = refl
lem (d a (d x₁ x₂ x₃) x₄) p = refl
lem (d (d x x₁ x₂) x₃ x₄) p = refl

Jacques

On 2015-04-13, 17:46 , Aaron Stump wrote:
> 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
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda