[Agda] direct product for list

[Andreas Abel]

Sorry, I was a bit quick.  You need to split on xs to fire the 
reductions for OrderedList?.  This works:

tailOrdered {xs = []}     = proj_2
tailOrdered {xs = _ :: _} = proj_2

(I was under the errorneous assumption that if you split in one clause 
{xs = []}, then the following clauses would split on xs as well; but you 
have to do it manually.)

Cheers,
Andreas

On 10.10.12 12:53 PM, Serge D. Mechveliani wrote:
> On Wed, Oct 10, 2012 at 10:44:16AM +0200, Andreas Abel wrote:
>> Did you manage to fix this?  If not, you can send me the file with your
>> example and I can have a look again...
>
> Please, replace respectively  Nat, ::,  <=,  _2
> to their math symbols         \bn, \::, \<=, \_2
> :
> ---------------------------------------------------
> module Main where
> open import Foreign.Haskell
> open import IO.Primitive
> open import Data.Unit using ( \top )
> open import Data.Nat
> open import Data.Product
> open import Data.List
> open import Prelude using ( toCostring )  -- by F. Kettelhoit
>
> OrderedList? : List Nat -> Set
> OrderedList? []             =  \top
> OrderedList? (x :: [])      =  \top \times \top
> OrderedList? (x :: y :: xs) =  x <= y \times (OrderedList? (y :: xs))
>
> tailOrdered : {x : Nat} {xs : List Nat} -> OrderedList? (x :: xs) ->
>                                                          OrderedList? xs
> tailOrdered {xs = []} = proj_2
> tailOrdered           = proj_2
>
> main : IO Unit
> main = putStrLn (toCostring "done")
> ---------------------------------------------------
>
> The checker report is
>
> /home/mechvel/haskell/agda/myPrograms/Main.agda:18,25-30
> OrderedList? (.x Б┬╥ .xs) !=< нё _21 _22 of type Set
> when checking that the expression projБ┌┌ has type
> OrderedList? (.x Б┬╥ .xs) Б├▓ OrderedList? .xs
>
> This is for  Agda-2.3.0.1, MAlonzo, lib-0.6.
>
> Thanks,
> Sergei
>
>
>
>> 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:
> [..]
>

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