# [Agda] direct product for list

Serge D. Mechveliani mechvel at botik.ru
Sun Oct 7 16:49:40 CEST 2012

Can you, please, answer a beginner question about the type for an
ordered-list proof?

First, I define of what is a  natural list ordered by <= :
(for this letter I change  \bn -> Nat,  \<= to <=,  \_2 -> -2 )

data OrderedList? : List Nat -> Set
where
nil    : OrderedList? []
single : (x : Nat)  -> OrderedList? (x :: [])
prep2  : (x y : Nat) -> (xs : List Nat) -> x <= y ->
OrderedList? (y :: xs) -> OrderedList? (x :: y :: xs)

And I manage to use this definition in practice. For example,

-- x :: xs  is ordered  ==>  xs  is ordered
tailOrdered : {x : Nat} {xs : List Nat} -> OrderedList? (x :: xs) ->
OrderedList? xs
tailOrdered (single _)                = nil
tailOrdered (prep2 x y xs _ ord-y:xs) = ord-y:xs

-- xs  is ordered  ==>  0 :: xs  is ordered
prep0Ordered : {xs : List Nat} -> OrderedList? xs ->
OrderedList? (0 :: xs)
prep0Ordered nil                        = single 0
prep0Ordered (single x)                 = prep2 0 x [] z<=n \$ single x
prep0Ordered (prep2 x y xs x<=y ord-y-xs) =
prep2 0 x (y :: xs) z<=n
(prep2 x y xs x<=y ord-y-xs)

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:
OrderedList'? (.x :: .xs) !=< \Sigma _154 _155 of type Set
when checking that the expression proj-2 has type
OrderedList'? (.x :: .xs) -> OrderedList'? .xs

The expression   tailOrdered' ( _ , tl ) = tl

also is not compiled, it reports of a wrong pattern.

Is not  OrderedList'? (x :: xs)  a direct product of two types
(so that its member is a pair  ( _ , tl ) )
?
How to fix this?

Which definition of an  ordered natural list  is better to use?

Thank you in advance for explanation,

------
Sergei