The Coq mailing list

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

And now is it what you expected?

Require Import Arith.

Inductive sortedlist : nat -> Set :=
   | snil : forall n, sortedlist n
   | scons : forall (n n':nat) (l:sortedlist n'), n <= n' -> sortedlist n.

Lemma dec : forall m n, {m<=n}+{n<=m}.
induction m;intro n;destruct n.
  intuition.

  left;apply le_O_n.

  right;apply le_O_n.

  destruct (IHm n).
    left;apply le_n_S;assumption.

    right;apply le_n_S;assumption.
Defined.

Definition min m n := if dec m n then m else n.
Definition max m n := if dec m n then n else m.
Lemma comp : forall m n, min m n <= max m n.
intros.
unfold min.
unfold max.
destruct (dec m n); intuition.
Defined.

Definition sinsert (n:nat) (m:nat) (l:sortedlist m) : sortedlist (min n m).
intros.
revert n.
induction l.
intro.
apply (scons (min n0 n) (max n0 n) (snil (max n0 n))).
apply comp.
intro.
unfold min.
destruct (dec n0 n).
exact (scons n0 n (scons n n' l l0) l1).
apply (scons n (min n0 n') (IHl n0)).
unfold min.
destruct (dec n0 n');assumption.
Defined.

(* For empty lists, you cannot use this inductive but rather: *)
Inductive sortedlist2 : nat -> Set :=
   | snil2 : sortedlist2 0 (* unicity empty list *)
   | scons2 : forall (n n':nat) (l:sortedlist2 n'), n' <= n ->
sortedlist2 n.
(* because snil 5 is not equal to snil 6, see snil 5 equal as [5]
i take youur relaxed version as pure masochism *)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.
>>
>> ?
>>
>> 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
>