[Agda] direct product for list

[Andreas Abel]

Did you manage to fix this?  If not, you can send me the file with your 
example and I can have a look again...

Andreas

On 08.10.12 12:59 PM, Serge D. Mechveliani wrote:
> 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Б┌┌
>
> ?

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

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/