[Agda] a puzzle about pattern matching

[Matteo Acerbi]

Hello.

You can obtain shorter definitions by refinement:

module Refinement where

  actionLem : (x : A) → Σ A λ y → x ≢ d a a a → y ≡ a
  actionLem (d a a a) = d a a a , λ k → ⊥-elim $ k refl
  actionLem _         = a       , λ _ → refl

  action = proj₁ ∘ actionLem
  lem    = proj₂ ∘ actionLem

A more modular approach might be to define a view:

module View where

  data View : A → Set where
    daaa :                       View (d a a a)
    else : ∀ {x} → x ≢ d a a a → View x

  view : ∀ a → View a
  view (d a a a) = daaa
  view (d (d x y z) b c) = else (λ ())
  view (d a (d x y z) c) = else (λ ())
  view (d a b (d x y z)) = else (λ ())
  view a = else (λ ())

  action : A → A
  action x with view x
  action .(d a a a) | daaa   = d a a a
  action _          | else _ = a

  lem : ∀ x → x ≢ d a a a → action x ≡ a
  lem x p with view x
  lem .(d a a a) p | daaa   = ⊥-elim $ p refl
  lem _          p | else _ = refl

Cheers,
Matteo

On Mon, Apr 13, 2015 at 11:46 PM, Aaron Stump <aaron-stump at uiowa.edu> 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