The Coq mailing list

[manoury <pascal.manoury AT lip6.fr>]

Dear Ian,

 as a case of ω^ω ordering, I would be interested in the kind of application 
you have in mind.

        Pascal Manoury.

> Le 26 nov. 2021 à 08:49, Jean Goubault-Larrecq <goubault AT lsv.fr> a écrit :
> 
> 
> 
> Le 25/11/2021 à 19:27, Abhishek Anand a écrit :
>> i would define an order-preserving function rank: list N -> N and the
>> rest should be easy corollaries of the order preservation theorem
> 
> 
> Hmm, such a function does not exist, if I am not mistaken.
> The order type of Ian's ordering is ω^ω, while the order type
> of N is only ω.
> 
> -- Jean.
> 
>> 
>> -- Abhishek
>> http://www.cs.cornell.edu/~aa755/ <http://www.cs.cornell.edu/~aa755/>
>> 
>> 
>> On Wed, Nov 24, 2021 at 11:10 PM Ian Shillito <Ian.Shillito AT anu.edu.au
>> <mailto:Ian.Shillito AT anu.edu.au>> wrote:
>> 
>>    Hi all, 
>> 
>>    Consider the "less than" relation << on lists of natural numbers
>>    defined by the following clauses (where l0 l1 : list nat):
>> 
>>     1. If (length l0) < (length l1), then (l0 << l1)
>>     2. If (length l0 = length l1 = n) for some (n : nat), then follow
>>        the usual lexicographic order on n-tuples.
>> 
>>    I strongly believe that this is a well-order on lists of natural
>>    numbers. I am interested in this property as it should help reach a
>>    strong (transfinite?) induction principle like the following:
>> 
>>        Theorem listnat_strong_inductionT:
>>        forall P : list nat -> Type,
>>        (forall l0 : list nat, (forall l1 : list nat, ((l1 << l0) -> P
>>        l1)) -> P l0) ->
>>        forall l : list nat, P l.
>> 
>>    ​Has anyone ever tried to formalise such a relation? Any reference,
>>    comment, or advice is welcome. 
>> 
>>    Best,
>>    Ian Shillito
>>