The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

Hi. You could define your ordering by lexicographically combining the order on length and the lexicographic ordering on lists of fixed length. You can find those orderings and their well-foundedness proofs in https://github.com/fblanqui/color/ (package coq-color on opam). See the files Util/Pair/PairLex.v and Util/List/ListLex.v. Best regards, Frédéric.

Le 25/11/2021 à 08:10, Ian Shillito a écrit :

        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