[Agda] direct product for list

[Serge D. Mechveliani]

On Sun, Oct 07, 2012 at 11:49:36PM +0200, Andreas Abel wrote:
> On 07.10.12 4:49 PM, Serge D. Mechveliani wrote:
[..]
>> But then, I thought of the definition via the direct product (\times):
>>
>>    OrderedList'? : List Nat -> Set
>>    OrderedList'? []             =  \top
>>    OrderedList'? (x :: [])      =  \top \times \top
>>    OrderedList'? (x :: y :: xs) =  x <= y \times (OrderedList'? (y :: xs))
>>
>> It looks simpler, it does not introduce new constructors.
>> But I fail to process its data, so far. For example,
>>
>>    tailOrdered' : {x : Nat} {xs : List Nat} -> OrderedList'? (x :: xs) ->
>>                                                          OrderedList'? xs
>>    tailOrdered' = proj-2
>>
>> is not compiled:

> Here, it would be better if you say "does not type-check"
> [..]

> The problem with tailOrdered' is that it does not match deeply enough.
>
>   OrderedList? (x :: xs)
>
> does not reduce, you need to match on xs first.  

How cannot it reduce when the type checker sees the explicit rules
  OrderedList'? (x :: [])      =  \top \times \top
  OrderedList'? (x :: y :: xs) =  x <= y \times (OrderedList'? (y :: xs))
?

> However, forcing a match on xs with two clauses
>
>   tailOrdered' {xs = []} = proj-2
>   tailOrdered'           = proj-2
>
> should remove the error.

It does not!
(try to apply Agda). Neither it does 
  tailOrdered' {xs = []     } = projБ┌┌
  tailOrdered' {xs = _ :: []} = projБ┌┌
  tailOrdered'                = projБ┌┌

?

Cheers,
Sergei