[Agda] Pattern-matching operation order

[Andreas Abel]

Nils Anders Danielsson a écrit :
> On 2010-02-17 15:11, Pierre Boutillier wrote:
>> data _<_ : Nat → Nat → Set where
>>    LE : ∀ {i} → (d : Nat) → i < (d + i)
> 
>> minusSS : ∀ {m n} → m < (ss n) → Nat
>> minusSS .{ss n}{n} (LE {ss .n} zz) = {!zz!}
>> minusSS a = ?
> 
> Agda does not make use of the pattern {ss .n} when checking whether (LE
> <whatever>) has type m < ss n. See
> http://thread.gmane.org/gmane.comp.lang.agda/1161/focus=1165.

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.

data Nat : Set where
   zero : Nat
   suc  : Nat -> Nat

_+_ : Nat -> Nat -> Nat
zero    + m = m
(suc n) + m = suc (n + m)

data D : Nat -> Nat -> Set where
   c : (i : Nat) -> (d : Nat) -> D i (d + i)

bla : Nat
bla = zero

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)

Here  c (suc i) zero  has type  D (suc i) (zero + suc i)  simplifying to 
  D (suc i) (suc i) which can be unified with D n (suc m), yielding n = 
suc i and m = i.  So I do not see why the match fails.

How would I write a series of patterns for f that do type-check?

Cheers,
Andreas



-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
http://www.tcs.informatik.uni-muenchen.de/~abel/
-------------- next part --------------
module PierreBoutillierMatch where

data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

_+_ : Nat -> Nat -> Nat
zero    + m = m
(suc n) + m = suc (n + m)

data D : Nat -> Nat -> Set where
  c : (i : Nat) -> (d : Nat) -> D i (d + i)

bla : Nat
bla = zero

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