[Agda] Pattern-matching operation order

[Andreas Abel]

Thanks, Ulf, for the explanation.

Is it fair to say that pattern matching works for all pattern  
inductive families, but not for those where indices are computed by  
(recursive) functions?

In the case of a non-pattern inductive familiy, we can fall back to an  
inductive type with equality proofs in the constructors.

data D (n m : Nat) : Set where
   c : (d : Nat) -> d + n ≡ m -> D n m

f : {n m′ m : Nat} -> D n (suc m) -> Nat
f {suc n} (c zero          refl) = bla
f {n}     (c (suc zero)    refl) = bla
f {n}     (c (suc (suc d)) refl) = bla
f {zero}  (c zero          ()  )

Or, of course, use equality in the function definition, as you did.

Cheers,
Andreas

On Feb 19, 2010, at 3:10 PM, Ulf Norell wrote:

>
>
> 2010/2/19 Andreas Abel <andreas.abel at ifi.lmu.de>
>
> The connection of our problem to the one in the thread is not  
> apparent.  Here is a rephrasement of the problem, not using dot  
> patterns.
>
> f : {n m : Nat} -> D n (suc m) -> Nat
> f (c (suc i) zero) = bla              -- FAILS already
> f (c i (suc zero)) = bla
> f (c zero zero)
>
> How would I write a series of patterns for f that do type-check?
>
> Here's how you do it:
>
> f′ : {n m′ m : Nat} -> D n m′ -> m′ ≡ suc m -> Nat
> f′ (c (suc i) zero) refl = bla
> f′ (c i (suc zero)) refl = bla
> f′ (c i (suc (suc d))) refl = {!you missed this case!}
> f′ (c zero zero) ()
>
> f : {n m : Nat} -> D n (suc m) -> Nat
> f d = f′ d refl
>
> The reason your version is not accepted is that the type checking  
> algorithm requires that each function definition corresponds to a  
> (type correct) case splitting tree. Basically, if you can't C-c C-c  
> your way to the definition it won't be accepted. In your example
>
>   f (c i d) = ?
>
> is not a valid refinement of the problem f x = ? (since d + i  
> doesn't unify with suc m).
>
> / Ulf

Andreas ABEL
INRIA, Projet Pi.R2
23, avenue d'Italie
F-75013 Paris
Tel: +33.1.39.63.59.41