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: Vedran Čačić <veky AT math.hr>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] A well-order on lists of natural numbers
  • Date: Thu, 25 Nov 2021 13:04:11 +0100
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=veky AT math.hr; spf=Pass smtp.mailfrom=veky AT math.hr; spf=None smtp.helo=postmaster AT mail.math.hr
  • Ironport-data: A9a23:fKLRqK0yvWeMEfo2jPbD5Shzkn2cJEfYwER7XOPLsXnJ0mgl32QGxjYZXmGFO/fbNDaje9sgOYSw8h9QvZWEx9cSHQtv/xmBbVoa8JufXYzxwmTYZn7JcJWbFCqL1yivAzX5BJhcokT0+1H9bdANkVEmjfvRH+OmVbaeUsxMbVYMpBkJ2UoLd9ER2dYAbeiRW2thiPuqyyHtEAfNNw1cbgr435m+RCZH55wejt+3UmsWPpintHeG/5Uc4Ql2yauZdxMUSaEMdgK2qnqq8V23wo/Z109F5tKNl7/6dgsPS6LSewiU4pZUc/H8214f/WpilP9mXBYfQR8/ZzGhgd1y2f1IvICwDwczVkHJsLpFC0MITnwW0apuqe6ZfyXXXdao50bBaj7nx+hkJFonOJURvOdxG2BHs/ICQA3hxDjra/mexbu6Tq9pj9gjasnxVL7zc0pIlVnxZcvKi7iaK0kL2TNZ4Nv0rsVHHPKYYsMFaXxvdnwspjUn1kg/UPoDcCWA3xETsAG0bHqQrLY3pWjJpOC0+Ka4K8LbI7RmWu0M9nt1ZQv6E6DRBxgGNJqf01JpN1rEavDnxUvGZW7ZKFF0GjOGTrFeKqz/xSD6jWeGnMQ=
  • Ironport-hdrordr: A9a23:x7Hxk6BFW5cIa7DlHem855DYdb4zR+YMi2TDtnoBKyC9Hfbo9PxG8M576faWskd1ZJhfo6HlBEDoexq1nvQZ3WB2B9eftWLd11dAQrsP0WM1qwePJxHD
  • Ironport-phdr: A9a23:xQ9fqB86BLp1L/9uWUW8ngc9DxPPW53KNwIYoqAql6hJOvz6uci4ZQqCvb421xfgZsby07p8ke3YsqTtCyQrwK2qlzQ8SqFKTAIPks4MngYtU4avAEz/K+P2PWRhRJwRHFBq8GumPkdLBc3we0PdomGo7T4VBx7zKRd5Kv76F4LMksi7zeC/94HcbwhGije2fK9/IgixoQjNrMcdnJFsKrw2yhvHo3tIf/pZyGZ1Ll+NnBjy+9m98od7/ytfp/wu+chAUb7nf6sjVrxXEC4mM2Eu68L1sxTIUBaC6WEdUmUSlRpIHhTF4RTnVZr/rif2quxw0zScMMbrT747RC6i4r9kRx/miigJNzA3/mLKhMJukK1WuwiuqwBlzoPOfI2ZKPhzc6XAdt0aX2pBWcNRWjRODYyicoQPFfAOPeBFpITjvVQBsRq+ChWxD+7o1D9HmHz23K0h3uQkCw7GwAwgE8gOsHTOtdj4MroZXu+pwqfS1zrDc+9W1inn6IjOah0tvf6BULx+fMfe10UiEw3IgkiUpILlMD6Y1+cAvmaG4+Z8Wuyhi3MqpxxtrzWuxsoihJfFip4Wx13Z+it3wII4KNulQ0B4ed6pCIZcuiCHO4dsQs4vTXtktSUgxrEbuZO2ejUBxo49yB7FcfOHdpCF4hL9W+aVJjd1nHdld6i+hxa260Sgz/fzVtW00FpQripFiMHAtnEL1xPN9siKUuZx80a81TqV1w3e5PtILEMumabGK5Mt2rswmYASsUTHEC/2gkL2jKqOe0U65Oeo6OTmb67jppCGK490ihvyMqQ0msCnG+Q3LhAOX3SH+eS7zLDs4Ur5QKxTgvIqlqnZrYvVKN8Apq+5Bg9Vypws5wy+DzegytQYnGMIIEhLeBKd3MDVPATFJ+m9BvOiiXytli1qzrbIJO7PGJLIe0bOnK3oe/5W4kVdw0Jn091c9rpRA60BZvLpDByi/OfEBwM0ZlTni93sD89wg9t2sYenB6aFMOXSqw3QjgrOC+yFZYtTvT/hK74l/ay25ZfWsVoUYanv3YFFMRiF
It's usually called "shortlex" ordering (or "lengthicographic", but that's more tongue-in-cheek:).

čet, 25. stu 2021. u 08:11 Ian Shillito <Ian.Shillito AT anu.edu.au> napisao je:
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


--
Vedran Čačić

Archive powered by MHonArc 2.6.19+.

Top of Page