Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] A well-order on lists of natural numbers

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] A well-order on lists of natural numbers


Chronological Thread 
    < Chronological >      < Thread >
  • From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] A well-order on lists of natural numbers
  • Date: Thu, 25 Nov 2021 10:27:48 -0800
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-ed1-f54.google.com
  • Ironport-data: A9a23:KLkSxagHjVe3Kw6Osfi1rNsTX161CxEKZh0ujC45NGQNrF6WrkUCnGVMWm6EbP+Ca2vzfdt1b4+1oxgP65Xdz4drGlNopVhgHilAwSbnLYTAfx2oZ0t+DeWaERk5t51GAjX4wXFdokb0/n9BCZC86ykjvU20buCkUredY3osHVUMpBoJ0HqPpcZp2uaEvvDiW2thifuqyyHuEAfNNwxcagr42IrfwP9bh8kejRtD1rAIiV+ni3eF/5UdJMp3yahctBIUSKEMdgKxb76rIL1UYgrkExkR5tONyt4Xc2UPS7/WeAWC0z9YBvTkjR9FqSg/lK08MZLwa28N02TPz403ko0d88HsIesqFvWkdOA1WhNYEjp+MK4A8bnOJ3T5sM2PwGXJdnLtx7NlC0Re0YgwpL8sWTAfr5T0LxhUNkzZ7w6s+5qwTfApjcA+JuHwLYYHszdhyyvYBLAoW/j+rw/i8YcNhnFvkpkbRbCGc5BMMXw1PUWZd0YaYhFKHM1rtfmMrXzbXz18iVuzmbAT3Wn22FUpheG2dILBEjCRbcBcn0Ldq26fumqkXlcVM9uQzTfD+XWp7tIjVBjTAOo6fIBUPNYz6LFS+oASNPHSfV6yoP38h0LnHtwCdwob/S0hqaV0/0uuJjU4d3VUv1bc1iPwmfIJewH51O1J4qXR6gedQGMDS1atrfQ44dQuS2VCOkChxrvU6P8GjFFRYX2Y/7aQ6zi1PED56EdqiTAsFWM43jUonG3/Yt8jgDqu/G5ZQ+AZwQ3N/g0=
  • Ironport-hdrordr: A9a23:0DFiw6+X1XCtd+tajDtuk+DhI+orL9Y04lQ7vn2ZKCYlC/Bw8vrFoB11726QtN98YgBDpTnEAtjifZq+z/9ICOsqTNOftWDd0QPCEGgh1+vfKlbbakrDH4BmpMFdmmtFZOEYz2IWsS832maF+h8bruW6zA==
  • Ironport-phdr: A9a23:6q33VhLcIg5uqh4W3tmcuMNmWUAX0o4c3iYr45Yqw4hDbr6kt8y7ehCFvLMw1BSQBN2TwskHotKei7rnV20E7MTJm1E5W7sIaSU4j94LlRcrGs+PBB6zBvfraysnAJYKDwc9rDm0PkdPBcnxeUDZrGGs4j4OABX/Mhd+KvjoFoLIgMm7yf2+94fTbglUizaxfK5+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Xymp4aV2Rx/ykCoIODA5/2PXhMJ+j6xVvQyvqABkzoHOfI2YLuBzcr/Bcd4YQ2dKQ8ZfVzZGAoO5d4YCE/EOPeZZr4nmp1sBsxi+DhSwCePp0DBIgGL51rA93us7Cg7G3A0gH8kOsHvKr9X5Lr0dUeavw6nO0DrPdfJW2Tbh6IjHaR0hrvSMUqhxccrV00UgCwTFjlCJpIHjIjia2fgDvXKB4Op8SeKglXQnqwdprzWrxsoglpfEipwbxF3K9St0wZg5KcGlREB7YdCqEIVcui+GOoZqTM4uXnxltDg4x7AapZO2fScExZsnyhPCavGKdZWD7BzkVOaUOzh4hXRldaqjiBa160igzPPzVs2w0FpQsCVKj8TMu3YQ3BLQ8siKUuVx8lul1DqV1A3e6vtILV4omafYMZIswrE9m5wOukrZBCD2gl/5jKqOe0Uk5Oeo7+Pnb63jppCGNo90jhjyPbozlcCiGOg4PAgDUmeB9eSz073j+kL5QLFUgfEsjqbZt5XaKdwapq6/HQBVzp4u5wijAzqiytgVnnkKIEhbdB6bjIXlIVHDLf/gAfe6mVuskTNrx/7cPr3mB5XANmLMn6zhfbZ88E5cyBQ8zdNF651ODLEOOvTzVVLruNzZDx85LwO0zv3oCNV4zIweWGaPDrWFP6PVtF+E/vgvLPWUZI8JpDb9LOAo6OLpjX8ggFMSYa2p3YYMZ32jBfRnI0CZYWL2jdsbEGcKuBA+TO3wh1GYXz5TfSX6Y6Vp7TYiTYmiEI2LEouqmfmK2DqxNpxQfGFPTF6WRyTGbYKBDt4GaCOJIsJi2hUCXL6tA9so3xGvrw/3yPxuKOPS9msZtI7s/Ndw7uzX0xo18GonXIymz2iRQjQszSszTDgs0fUnyaSS4liG2Kl8xfdfEI4Kjxusegg/PJ/Yied9DoKqMuogVtKASVLjT9n/RD9sEpQ+xNgBZ0s7ENKn3Eir4g==
i would define an order-preserving function rank: list N -> N and the rest should be easy corollaries of the order preservation theorem



On Wed, Nov 24, 2021 at 11:10 PM Ian Shillito <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

Archive powered by MHonArc 2.6.19+.

Top of Page