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: Ian Shillito <Ian.Shillito AT anu.edu.au>
  • 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 23:08:46 +0000
  • Accept-language: en-AU, en-US
  • Arc-authentication-results: i=1; mx.microsoft.com 1; spf=pass smtp.mailfrom=anu.edu.au; dmarc=pass action=none header.from=anu.edu.au; dkim=pass header.d=anu.edu.au; arc=none
  • Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-AntiSpam-MessageData-ChunkCount:X-MS-Exchange-AntiSpam-MessageData-0:X-MS-Exchange-AntiSpam-MessageData-1; bh=XeIgmm4C6+7ps2GgfVF/Td6B/XRukO5C/+w6lHCIeaI=; b=hbF7anIn/usfNUorXgQZkZ0aXOBdcAW2bJZ5LGg6+Q8Zy/fvWyCNfTgobKM5lBvI0gz5ohkBuMqxvQyy4IxDFb75cjPGSCwhbuWCF5UJOhqvcDUQcgI6Cj8BYe8evpTHRClII4J1D7Z3mida6bs8gDfNkZ+hS/ebtg5IVI/tI+vcmVD0JwuV11UsZPxqGAS/QNKhbYvkSYskBf67oFL5vo/xGJLRcXVNXrjMUWZGFl8khXS4RZXc9T4b1NYnccNSXrpgI6Esm72XwfRFNc32Y9Sk8itFdpEili7tXgfkPIlAwJb5o6iDvCuRutWHZROLG0NRbhNQD7Bc85fUAWUL5g==
  • Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=ZZjQNgbuoG7nba5RkWBQjGyOmqxfbLFIGkgf8koz+mYahzMQuKxyESi0+W+WRWZzBqkbgEIMW58nybhqGdm9251Dy7th5pv4n/GOJNEHJWqvpIIyRaXYwNv22kK0gJHaLibjrXL0ZyoHQNCIR1mHPhdkJ72Tlwnw2oxPt/BWud+R9RJaWOXSUogjE/uVdj4OLKW3i5yab2bBkTOswoDdMyG4CM0DQeqOb8o0JIW24UY/gCT4xznTeQYx+/KOcEtjkVGmoNJQFRABm5k7Ky/U1alYyYUdTSDC49K02UJjHu/nTJp9XAk7zInu9vhtBIglAchq9COLwKUJFWZguav5jA==
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=Ian.Shillito AT anu.edu.au; spf=Pass smtp.mailfrom=Ian.Shillito AT anu.edu.au; spf=Pass smtp.helo=postmaster AT AUS01-SY4-obe.outbound.protection.outlook.com
  • Ironport-data: A9a23:VOU7B6I8ffqhmaJpFE+R7ZQlxSXFcZb7ZxGrkP8bfHC93D4j12ECnWAfWDyOMvvZZGGmfNAgaYS0px8HvcOGy6c2QQE+nZ1PZyIT+JCdXbx1DW+pYnjMdpWbJK5fAnR3huDodKjYdVeB4EfyWlTdhSMkj/jRH+ChULWs1h1ZHGeIdg9x0XqPpMZi2uaEsfDha++8kYuaT//3YDdJ6BYoWo4g0J9vnTs01BjEVJz0iXRlDRxDlAe2e3D4l/vzL4npR5fzatE88uJX24/+IL+FEmPxp3/BC/uMr42jKwgxc+KXOgKDzH1LR6Klnx5O4DQo1bo2P+YdbkERjCiVm9d2y5NGspnYpQUBYvWKwbxCFUAATGcnZ/cuFLzveRBTteSyxkuASHvtx/FvEEYeNIsFvOt7HCdH6JT0LRhTN07f2L3oqF68YrI13Z98RCXxB6sUvWglxjXEB949UJXbSuPL48VZ1XE+nKhz8Vz2c5JMMnwyeE2VO1sXLg1CUNRkwbn2kiKqK3sFvA3AjLQTyG314AxV8bHLDMDzRN2vUZwNyxjc/nauE3/RBxgbMJmE2GaM72n03+jJx3qhAsQVCaGy8eNsjBuL3GsPBRYKVFy95/6klkq5XNEZIEsRkhfCZJMarCSDJuQRlTXhyJJFgvIdZzaUO8QH01nUj5Hlv0OeDGVCSSNdYts7ssNwXSYtylKCg9LuA3poraGRTnWesLyTqFte/AALeHQaa3ZsoRQturHeTEMb13ojjeqP1Ia8iMCzFD3thTmXxMT7r6tGltYFjs1X4nie6w9BZfH1osod7wPKGG+p80VweeZJoqTABUfztZ59EWpScrVNULXoVSRTACDiwKxhTBCwfdg=
  • Ironport-hdrordr: A9a23:MM9oVa7O4lDrIPv8mAPXwQqCI+orL9Y04lQ7vn2ZKCY6TiX2ra2TdZggviMc+Qx/ZJhIo7npBEDqex/hHPBOi7X5RY3CYCDW/EylMYl69M/r2SH4XyX5+6pc0qd8c6BiBNCYNykOse/KpC61Dt442Z2O6rywwe3a021xQRpnZshbnnZEIzfeNUFqTBBeQZIiCIPZ7MxBqH6reHgcbN6mAhA+Lpf+juyOs576aQceQxY89BDLhzWu5/rkHwOD3hEYOgk/vYsKwCzjnxHw/7zmu+um01vX0Wjd75lbn8bgwt5CGdzksKgoAwSprQq0bJ15H7WZoClwquep9VosjbD30nUdFvU2zH/Ndnit5RP2xxCl3y0p7xbZuCGlqEqmhsDlTCsiT8JamZscfBff51Epod1wlKRNtljpzqZ/PFfmkDn0/sGNXwt3jw60p2A+luYWgxVkIO0jQY4UioAD9FpNVJ8bADu/7IYrHOwrC8nZ6J9tAC6nRkGcmWVzyMW0GnwoAg7DRFJHpcCPyThRmxlCviwl7f1auXsc/IslD5Ff+/2BK6xyibZDVYsWa7hhA+8ETaKMexbwaCOJF26OKU3/UKkcJ2uIspbt/bI4/6WxaIYUwJ93mJmpaiIiiUcCP2XjFMWWxdlC6AzVBHy0TTHqwswb7Zl0sL/nWL6DC1zxdHke1+ytvv0HG4nSQeqrfIlbHuTqKnHrGZsh5XyNZ7BibV4TTcUNo5IyQU6W5tjGMpHnsebWGcyjVIbFIHICVn72G2JGVCLuPYFb4luqUnq9hwTUMkmdAnDXzNZWHLXT5vFWwJIQL8lXrgMXhV6lj/v7TAFqg+gQcFZ3OaqimrmmvC2t7XzU42EsOhc1NDcw3JzQF1RHuAcSKgf9a6ob/8qSYnpT2nzvHG4dc//r
  • Ironport-phdr: A9a23:PNutvheKH63Pw/ypsyfHSn/clGM++tnLVj580XLHo4xHfqnrxZn+JkuXvawr0AWQG9iCoKofw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94PObwlShDexfLx+IAm4oA7MqsQYnIxuJ7orxBDUuHVIYeNWxW1pJVKXgRnx49q78YBg/SpNpf8v7tZMXqrmcas2S7xYFykmPHsu5ML3rxnDTBCA6WUaX24LjxdHGQnF7BX9Xpfsriv3s/d21SeGMcHqS70/RDKv5LppRhD1kicKLz43/n/KhMxsgqxVoxyhqB5jzIHbe4yaLuZycr/HcN8GWWZMXMBcXDFBDIOmaIsPCvIMM+VCoIn7ulAAsBu+BQioBOPryz9Imnj21rA93uoiCw7G2hYsEc8OsHTVqNX1MKYSUfyyzKTT1zrDae5W1S3j54fVbxAtu+uDXa9pfMfX1EIgGB/LgE+Kpoz5IzOayP4Ns26D4uRgSe+iiG8qpQFwrzSy28sglJfEi40Jx13a6Sh03IQ4KcO2RkB1fdKpH4Zcui6UOoV5Rs4vR25ltDs7x7AEpJO2ejUBxpogxx7acfOHco6I7wr/W+aWOzd4gmxqeLa7hxqo70ev1/D8WtGz0FZXsipFlt7MtncO1xDJ9seHTf5980G80jiMzwDe8u5JLVwumabGN5IswKQ8mocPvUnBBCP6hVv6gLGOekk6++Wk9+rqb7D7qpOAK4B5iwTzPrkylsG6HOg1MhUBUm2e9Oih2rDu+1DyTq9Qgf0siKbZtYjXJcQFqa69BA9Yypou5BiiATu6zdgUhGQJI1BKdR6eiIjmIE/BLOr/Dfein1SjizBrx+3APrL8GJnNNmLDkLD9fblj90Fc1AszzddZ555ODbEBPe7zWkv2tNzfDR81KRC7w+HiCNll14MeX3yAArOBPa7drVOE/P8jL/WOaYMPpTrxN/oo6+TzgXMnh1MRZayp0oEWaHC8EPRmOUKZYX/0j9kCC2gKuBAyQvHqiF2DVT5TY3eyX7475jwgEo2mC5rDSpqzj7OcwSe3BIdZZn1eBlCWDXjob5mEW+sLaC+KPsBhlSUEWaG9RI8lyBGhrxT3y6FnL+rR4i0Xr4jv1Nlz5+3JlBE97yZ4D8qH0zLFc2YhlWQRAjQywao39Ud60xKI1bVyq/1eD91aof1TBFQUL5nZms1zDZjJWgPFetaVTx7yY9ygRwoxT9Y1wsMJS097BpOvgg2F1jf8UOxdrKCCGJFhqvGU5HP2Pcsokx4uNYEIsmJ+G450BDHjgaRysQ/OG4TOjkOV0b6wcrgR1zLM82HFyneSuEZfU0h7VqCXBBj3iWPfq8m/60/fCbazW+1P2u5pwMifbKZGd5vgkAceLMo=
  • Suggested_attachment_session_id: fdde5156-43a7-ebfb-f35d-1c8e1866d2e1
Hi all, 

Thanks to all of you for your answers. They are very helpful! 

Michael: I should have been more precise in my email, as I am particularly interested in getting the strong induction theorem for the specific order I described. I do not directly see how I can use your result for the order I have in mind. 

Dominique: My initial thought was to first ask the community to see if this work had been done before, and if not then try to find a solution myself. But well, I don't think I can blame you for giving the solution straight away! 🙂 Thanks a lot for that, it is exactly what I was looking for.

Vedran: I will definitely go for shortlex too! 🙂

Abhishek: I will also investigate in this direction and think about what the rank function might be in this case.

Best,
Ian
From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Abhishek Anand <abhishek.anand.iitg AT gmail.com>
Sent: Friday, 26 November 2021 5:27 AM
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] A well-order on lists of natural numbers
 
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