Skip to Content.
Sympa Menu

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

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[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 AT inria.fr" <coq-club AT inria.fr>
  • Subject: [Coq-Club] A well-order on lists of natural numbers
  • Date: Thu, 25 Nov 2021 07:10:01 +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=bI9GHbl6bGDTtSHkO+pdb7yH6oqpggz4sZaIM7uuCUM=; b=IRatmoKRDG8hwxwQ1B02DhRc3HgfHCkcTCPhlRKyaI88peeJ9VNekOrj9aMD6GfqwFa3DJ9hAtYm+BLDj3z0N35g9Qoy2xSQsQ1thF7tg3QMhSDJkwtzRXmaNuZqNwyir/R9qIoB4ztZ6BS4RSF0JOuDorc60q5ZsoZCSZjyZAsWrW4o4OkBoVVJ19OnY7wvmNvjbnfAv4NAHWgVoHy6MoevnAifLJg47FtBl1Tt7wx+3o3lUYIzPZad1bDN46/dkA+fF9hTef8BUL7vEvB4w/CXiYvbzYVqMb/QG9AszSd+rXG9Wg5bojRIxRmdmgcgl86B9E+SL/AIzOPPz0+zBQ==
  • Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=CbHfLoOv8lBtb1TPhkLJLeh6WKUi+Ju9xBWfbe8K2Z7PCp/MC9jawCTw/uXMnt/5zA1wUSrM6aVePKg5Zc0Q1eu0WAT2nospqUzEOwiQrAWg4jb3rTtLRbiHxbLKewQkIN5P3ktcxJ8zJZvNrsnwH8CptrsOYEZvRqXw3FiLrluvmX8fI8N7AXcgQ74QmwjOwUirSP9PjeHswPl97Wt2hgDaf8mRbTfGkPRSFQ7zkoP6I+UmdgRqMUl3D7dM5ZtRhsHY3ZsNmRMsyu1UmY262uh42Ow2g8+/1gI9N6Gr4Lvp4bWbcZQGzSEzkB1YitKkkeX18L+Wln6RG9jIQ7NQPQ==
  • 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-ME3-obe.outbound.protection.outlook.com
  • Ironport-data: A9a23:9R+qgK97jesPxoRuVjhpDrUDvH+TJUtcMsCJ2f8bfWQNrUom1GRSxmoZCGzSMvuNYTP9Lt1zbdy28xsFsZ6BzYcxSXM5pCpnJ55ogZqcVI7Bdi8cHAvLc5adFBo/hykmh2ipwPkcFhcwnT/wdOi+xZVA/fvQHOOlUbSZYnkZqTJMEU/Ntzozw4bVvaYz2bBVMyvV0T/Di5W31G2Ng1aYAUpIg063ky6Didyp0N8uUvPSUtgQ1LPWvyF94JvyvshdJVOgKmVfNrbSq+ouUNiEEm3lExcFUrtJk57ST3ZSG/v3EFPLjXBbHa+/nhJFuyo+lL4hM+YRYltWjDPPmM1tzNJKttq7TgJB0q/kxLxbCkEHVXgmbesfouKvzXuX6aR/y2Xnen2q+PVvCEU3IYow8+BqR2xC6LoRNVjhazje17LumuzgIgVrrp96d5K0VG8FgVlryiicBvI7S7jYUqDS7JlZ2i0xj4ZAB57ji2AxfWI6N1Kdd0QaYhFPHMhrxKHy2yehZ2YN8BTIsfViynb35wlX/LjJEdPzRsase8Rwih/A8zuCp3CR7goyMdWezX+A/ymlm/SXxCT9AttISfu/6+Jgh0CVyioLEhoKWFCnoP6/zEmjR9ZYLE9S8S0rxZXePXeDFrHVNyBUalbe1vLdZzZRLwH+wCiw8fKNpiO0XS0DRDMHb8E6vsgrQzBszkWOg97iGT1otvuSVG6Z8bCX6zi1PED56EccMDQcQ1JtD8bL+ekOYtDnF76P05JZSvX8Hyy2zjyX6iEj71nWpdBezL21pDgrnBr1zqUkjWcJCsH/V2S4qA51eciseuRELHCzAelodO6kc7VKgJTIdwVyIgzD4VFhWRFhmNkwIYw=
  • Ironport-hdrordr: A9a23:UDX5WKsQrARPANi/aPgUKyQO7skDuNV00zEX/kB9WHVpm6uj5riTdZUgpGbJYVMqM03I9urwX5VoLUm8yXdV2/h0AV6uZmPbUQiTQr2Kj7GP/9XgcxeOk9K1vJ0IG5SWbueAbmSS5vyKhjVQfexB/PC3tIuQr8v/8jNAXBxObad4xQFkDRvzKCBLbTgDLqMSOLqgoupBuh+nf208aNi9GxA+MNQr3Oe79q7bXQ==
  • Ironport-phdr: A9a23:RxnJ1xDwJVFsHIGWTTTLUyQU/kMY04WdBeb1wqQuh78GSKm/5ZOqZBWZua80ygOYFtWLo9t/yMPu+5j6XmIB5ZvT+FsjS7drEyE/tMMNggY7C9SEA0CoZNTjbig9AdgQHAQ9pyLzPkdaAtvxaEPPqXOu8zESBg//NQ1oLejpB4Lelcu62/6v95HJbAhFgDWxbLBxIR6rsQjfq84ajJd4JK0s0BXJuHxIe+pXxWNsO12emgv369mz8pB+7Sleouot+MFcX6r0eaQ4VqFYAy89M28p/s3rtALMQhWJ63ABT2gZiBtIAwzC7BHnQpf8tzbxu+Rh1CWGO8D9ULY5Uimg4ah2Uh/lkCcJOSAk/mHLhMJ+j75Urx26qhNl34LYfJuYOOZicq7fe94RWGpPXtxWVyxEGo6ybJEAD+wcNuhFr4n9pl8OrR+/BQmwA+Pk1zhFiHzs0q08yegvDAHG3A0kH9IKsXTUsNL1ObwIXuCz0anE1yvMYO5L2Tvn8ofIbwksrPeRVr1/bcTf01MgFx/ZjlqOs4zlOSuY2OsOvmaU4OdtSf6jhm0mpg9xpjWhydsgh5TLi48X1lzJ6yZ0zYkrKNC8RkN1bsOoHYZTui+UN4V4Qt4vTW5ntSs817YIuoa7cTAFxZg73RLTduCLfoqS7h7+SOqcIi10iG97dL+/nxq+70mtxvHyW8SxzVpGsjZKn9jJu3wQyxDe79WLR/tg8Uqk3DuDyg7e5+dZKk4uj6XbMYQuwrsom5oTr0vDGij2lV3qgaCYa0so5vWk5/3gbLvpqJKQLoh0hRrgPag0ncy/HPg4PRMJX2iG/+Szyafv/VXjQLVNkv05jLXWsIzbJcQcoK61GQhV0ps/6xa7CDem19cYkWMbI1JCfRKLl4npO1fQL/DkFfqyjEignC12y/zaPLDtGIjBImTAnbv7YLpx9U5RxBI2zd9F5pJUDr8BIOj0Wk/0rNHWDQU2Mwquz+j6CNV914ceWWaOAq+FN6PfqkWH5uQyI+WWeoAapSv9J+I/6P7zlXM5g0MSfbG13ZsLb3C1BuhpI0KAYXb1ntgBFXoKsRElQezxiFyCVCZTaGyoU6I94DE7EoOmAp3ZSoCjmrzSlBu8S9ddYXkDAVSRG1/pcZ+FUrECcmjadsRmi3kPUaWrY44nzxCn8gHgnelJNO3RrwwRs9rY1Nlx4+zPkllm1DVySf+d0mWJTn1ztmoOWnk70L05qFErmQTL6rRxn/ENTY8b3PhOSApvbfY0IMRzDc20Vw7cON6UGg/OqjSOKAwKFot05vJVJkF3FpOlkwzJ2DesD/kNjbuXCZco86XamX/sO8J6zHWA364k3QBOqi5nPGu7wKNz6k7aGtyR+3g=
  • Suggested_attachment_session_id: 329a38c3-61d1-1734-4190-3cf80d95c71a
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