The Coq mailing list

[Pierre Casteran <pierre.casteran AT labri.fr>]

Nadeem Abdul Hamid a écrit :
> 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.
> >
> >     
Hi,
Cedric's definition doesn't characterize lists indexed by their length, 
but by a minorant
of all their elements (in fact their first element).

You can also forget this index :


Inductive SortedList : Set :=
forget_n : forall n, sortedlist n -> SortedList.



Then  leq_all is easily defined :

Definition leq_all (p:nat) (l:SortedList) :=
match l with (forget_n n l) => match n with | 0 => True
                                                                      
  | q => p <= q end end.


Definition ex1 : SortedList .
refine (forget_n _ (scons 3 _ (scons 5 _  (snil _) _) _));auto with arith.
Defined.

Goal leq_all 2  ex1.
simpl.
auto with arith.
Qed.


Definition bad_ex : SortedList .
refine (forget_n _ (scons 12 _ (scons 5 _  (snil _) _) _));auto with arith.
Abort.


> > ?
> >
> > I am not sure why it didn't worked, so i won't try to explain it...
> >     
Neither do I ...
Pierre



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