[Agda] direct product for list

[Andreas Abel]

On 07.10.12 4:49 PM, Serge D. Mechveliani wrote:
> 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:

Here, it would be better if you say "does not type-check", because you 
are talking about a type error message.  Under compilation we understand 
usually the code generation phase: compilation to Haskell (MALonzo) or 
Epic or JavaScript.  You could help avoiding misunderstandings.

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.  However, forcing a 
match on xs with two clauses

   tailOrdered' {xs = []} = proj-2
   tailOrdered'           = proj-2

should remove the error.

>     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?

That is a bit of an open question, you have to decide from case to case. 
  Agda supports data types like OrderedList? a bit better than 
recursively defined types like OrderedList'? because matching on data 
types is easier.

Cheers,
Andreas

-- 
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/