The Coq mailing list

["Nadeem Abdul Hamid" <nadeem AT acm.org>]

No, I'm not trying to define a list indexed by its length. I was
trying to define a list whose elements are sorted by definition. Every
time a new element, n, is cons'ed to the beginning of an already
sorted list, l, it must be shown to be less than all the elements
already in l (thus, keeping the list sorted in ascending order). The
leq_all is not a function -- it is a property defined inductively
(necessarily mutual with sortedlist) of a number being less than all
numbers in an existing sortedlist: the definition is a bit inverted
from how you would write it as a function, which I think is what you
were thinking...

On Thu, Oct 30, 2008 at 5:59 AM, AUGER Cédric 
<Cedric.Auger AT lri.fr>
 wrote:
> Did you expected something like this:
>
> Inductive sortedlist : nat -> Set :=
>   | snil : forall n, sortedlist n
>   | scons : forall (n n':nat) (l:sortedlist n'), n <= n' -> sortedlist n.
>
> ?
>
> I am not sure why it didn't worked, so i won't try to explain it...
>
> Btw, you also ill-typed the rest of your term:
> leq_all' -> leq_all
> leq_all n nil -> leq_all n snil
> leq_all n (cons n' l') -> leq_all n (scons n' l')
>
>> I was trying to reproduce an example similar to one from the Agda
>> documentation, using dependent types to define the type of a sorted
>> list of numbers:
>>
>> Inductive sortedlist : Set :=
>>    | snil : sortedlist
>>    | scons : forall (n:nat) (l:sortedlist), leq_all' n l -> sortedlist
>> with leq_all : nat -> sortedlist -> Prop :=
>>    | srt_nil : forall n, leq_all n nil
>>    | srt_cons : forall n n' l', n <= n' -> leq_all n l' -> leq_all n
>> (cons n' l')
>> .
>>
>> but it gives an error on "sortedlist" in the type of leq_all:
>>      leq_all : nat -> sortedlist -> Prop :=
>> "Error: The reference sortedlist was not found in the current
>> environment."
>>
>> Apparently, the names of the types being defined cannot be used in the
>> types of other mutually referential definitions? Is there any way to
>> do this?
>>
>> --- nadeem
>>
>> --------------------------------------------------------
>> Bug reports: http://logical.futurs.inria.fr/coq-bugs
>> Archives: http://pauillac.inria.fr/pipermail/coq-club
>>           http://pauillac.inria.fr/bin/wilma/coq-club
>> Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
>>
>
>
> --
> Cédric AUGER
>
> Univ Paris-Sud, Laboratoire LRI, UMR 8623, F-91405, Orsay
>
>
>