The Coq mailing list

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

Thanks Pierre and Cedric,

Sorry, I figured out the definition using the minorant; however, I  
don't know if it is still completely useful. In this Agda-based paper  
"Dependent Types at Work" (http://www.cs.chalmers.se/~bove/Papers/dep_types.pdf 
) there is an example of a binary search tree, which is sorted by  
construction (around pg 34-35). I'm trying to replicate the similar  
thing with just a sorted list. So the whole point is to write an  
insert function that is also correct by specification. With Cedric's  
definition however, this does not seem pretty:

First attempt:
(* insert n' into a sorted list whose elements are all >= m *)
Definition sinsert (n':nat) (m:nat) (l:sortedlist m) : { m' &  
sortedlist m' }
- The return type is not strong enough for the induction hypothesis/ 
recursive case to go through... we need to know m' is smaller than n'  
and m...

Second attempt:
Define  min : nat -> nat -> Prop := fun x y => if (le_lt_dec x y) then  
x else y.
Definition sinsert (n':nat) (m:nat) (l:sortedlist m) : sortedlist (min  
n' m).
- This doesn't work in the nil case because suppose m is less than  
n' (for an empty list, m could be anything). Then, the cons  
constructor would need the type of the list to be indexed by its first  
element, which is now n', but this doesn't fit the return type of the  
function, which must be (sortedlist m).

It is possible to relax the definition in the scons case, so the index  
is any value less than the first element, something like:
Inductive sortedlist : nat -> Set :=
  | snil : forall m, sortedlist m
  | scons : forall (n m m':nat) (l:sortedlist m'),
            m <= n -> n <= m' -> sortedlist m.

Then, I think it is possible to get through the definition of the  
insert function, but
- it is no longer easy to make the insert function reducible using  
Eval compute... because of the use of all sorts of opaque lemmas in  
the reasoning about the indices
- it destroys the whole point of the example in the Agda paper above,  
which I think was to show a somewhat elegant definition of a sorted  
data structure and insert function that are correct by construction.

Maybe neither of these would be satisfied even with my intended  
definition, however, my original curiosity still stands, which was  
that the names of the types being defined cannot be used in the types  
of other mutually referential definitions, again, as in the following:

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')
.
==> 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."

Is there a reason why Coq doesn't support this, or just that it has  
never been useful to do so?

Thanks,
--- nadeem




On Oct 31, 2008, at 3:56 AM, Pierre Casteran wrote:

> 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