The Coq mailing list

[AUGER C�dric <Cedric.Auger AT lri.fr>]

Nadeem Abdul Hamid a écrit :
> No, I'm not trying to define a list indexed by its length.
It is not the case, for exemple this list is sorted with 3 elts.

Lemma _3_6_9_ : sortedlist 3.
apply scons with 6.
apply scons with 9.
apply snil.
apply le_S;apply le_S;apply le_S;apply le_n.
apply le_S;apply le_S;apply le_S;apply le_n.
Defined.
>  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
>>
>>
>>
>>     
>
> --------------------------------------------------------
> 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
>