The Coq mailing list

[Jean Goubault-Larrecq <goubault AT lsv.fr>]

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
>