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 AT inria.fr" <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] A well-order on lists of natural numbers
  • Date: Mon, 29 Nov 2021 06:17:52 +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=m3Ulz+fZpOk3AbA4410RW7DYFnUQYOxiiGoObg5k2eo=; b=Tb7CLD/0V3MxXzMYwbdJTb5jD0Xc64r4OPojD4abQ9gcP8uKQTRreDfB99EfSFjPq66Ghh3hjmKaoCgokpVcaBXV5uCqYMnMu6qBheQy0cLPtWU1xXKyvEy+uZzB8uxFcjMG+wZZTTXis8DR6wEKrG9iijx6TcLDiW4dvDLzdHZ5HlGkaGe/stOOlQmfIWNBliPhtbu2X5Ak6E5qEOnxLWkX3mZbVJlQVpRDzOrQxXar5kUyCPEdkKRloV4zc7rgdO2kpVudH6TgqAc7sFTYQ69iEIy2dtqzUZMH8HfFY/Dm4r7+wuF50TGizUdj8YSRvbMaySf5Cfw8c4YL6eOqlw==
  • Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=Hqxy4qfHwhx/GypfvzcD3C+b87eDcwBGl/++9F/C0vhJZBxSauPJcVe+5kuM2vN9kFxZ+lMLfSwuKJQwd/e553DZpgU+rFRwDbbBRBp18bjKJllJNwYHS9l/d+ZxCP98FMByZ7z0fc5nrZFnsnaEPUOwMfej2fyO5vljEz8q7oT++1ct3DPY3Nwr/A1Y8Bu96LIGHpqxkY7EIh3Dd+N9XlcdOh873Vs8r998xuF8Bm8dPrsYHV6vlSx6x9d/1a4DY4WtbpSgKB4uo6Vif7cI/forUcg7kUmhPR+IkT4h2/DjJzUgZhEwnFeQ2hVcv9Z86tQttnMFnqXwgz4E+Z5kjQ==
  • 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:LybJl6N3Osd3LIDvrR2YlsFynXyQoLVcMsFnjC/WdVLr3W930GMOzjEWCmiBbqmMZGr9cotxPoW//EMEsMXdv4NqS1BcGVNFHysb85KdbTi6Bh6tZH3KdpWroHqKXqzyU/GYRCwPZiKa9kjF3oTJ9yEmjPjRHOqkU4YoBwgoLeNaYHd54f5cs7Vh6mJYqYDR7zKl4bsekeWHULOW82Ic3lYv1k62gEgHUMIeF98vlgdWifhj5DcynpSOZX4VDfnZw3DQGuG4EgMmLtsvwo1V/kuBl/ssIvqYqe6iN2gnGfvVNwXIjWdKUa+/hBQEvjY1zqswKPsbbwFQlimNmNdyjt5KsPRcSy91ZuuVwLtbCkEIVXAgVUFF0OevzXyXkMWViXbGcn/owulpJEgwIMsV9vsxCHwmGfkwdm9XN0vY3opax5rgE7I32azPNvLDN4QG/3pk0DvxFucjWZmFQqPQ5NYe0i1YuyzkNeKGMpFfNC42OUyGOwkVbw9RUs9gwvPz0yG5LikH/XuLg4EyxUTT6C149oT3FuTUX8jTHZAK2hiMzo7d12HwAxVfMdHEwCeeqiurgLWXzH29X58OHrql8PIsmEeU2mEYFBwRUx28vOW9jUm9HdlYLiQpFuMVhfBa3CSWohPVBnVUYUJovyLwn/J5LtZisUSo5/GR5AyUQG8ZUjRGddoq8tcsQiAn3UOImNWvAiFztLqSSjSW8bL8QfaaJ30ONWFbDcMbZVJt3jUhiNhbYtHzohJLGaioyND5BHf53lhmaQAg0q4Lg5djO7qTpDj6bvHFmnQNZgcz+0PaUn/j5x4RiEuND2C3wQCz0Mus57p1grVMULboViReAC0z4UmxqRGw
  • Ironport-hdrordr: A9a23:D6e79aGhJJG7ZQ0XpLqF2JHXdLJyesId70hD6qkXc20UTiX4rbHuoB11726ItN8uYgBipTntAtj7fZsznaQFrLX4E9+ZLUbbUUGTXcpfBbKL+UytJ8UVntQtm5uICpIOQuEYbmIK/foSgjPIbOrIm+P3uJxA7N22pxwGIG0FCsEQjHYae2PrdjwQNW977LUCZdihD6F81k2dkBosH7qG7rhsZZm0mzWd/6iWECLuxCRXkTWmvHeH7Lb7Fly/xRcRUzRGxPMH/XLemwL0ooWP2svLtiM0G1Wjl6h+qZ/FwtxMGMSDhow5JijhgBulae1aKs7y+wwdkaWK4FYulNHK5z84Jt909H/dOkmpyCGdrzXI4XIL43/mzVeexVrqpsH9SClSMaV8bQ0wSGqR12MQ+Ohm1qRFxmSYsIcSIy/hsU3Glp31fiAvr1Gzp3U6l+4Vkjh4aqsxLJFsjaF3xjIQLH8ndBiKnfF/LACrNrCvlbBrmJqhHgvkglU=
  • Ironport-phdr: A9a23:JWaWGhModpbTntrhu00l6nZVChdPi9zP1u491JMrhvp0f7i5+Ny6ZQqDv6wr0Q+CBt2TwskHotKei7rnV20E7MTJm1E5W7sIaSU4j94LlRcrGs+PBB6zBvfraysnAJYKDwc9rDm0PkdPBcnxeUDZrGGs4j4OABX/Mhd+KvjoFoLIgMm7yf2+94fTbghLizawb69+JwiqoAvMscUbnZFsIbsrxBvTpXtIdeVWxWd2Kl+Wgh3x+MS+8oN9/ipJo/4u+NJOXqv8f6QjULxXFy8mPHwv5M3qrhbMUw2C7WYBX2oMkxpIBw/F7AzmXpr0ryD3uPZx1DWcMMbrS70/RDas4LpxSBLwiCkJKSM38H3ZhMJzgqJUog6uqBNkzoHOfI2ZKOBzcr/Bcd4YQ2dKQ8ZfVzZGAoO5d4YBDPAOPeBFpIfgp1sOrB++BQ2tBOPzzT9Dm3j7064g3OQnCw3IwQwgH9MKsHTQrdX1KKASXPuvw6nO0DXPde1Z1irg6ITSaB8hvOiBULRtesXe1UchDRnKjkmMqYP7JTOV0PwAvmyb4ud9Wuyii28qpgBsrjSzxskhionEipwJxl3Z9ih0w4g7KNOkRUN4f9KpEoVcujyEOoZ5TM4sTG5mtSg1xLAApJW1ci8KyJE9yB7ebfyKa4+I4g//VOaVJjd4g3FldKijiBa19Eis0vHzVs6u0FZMsCVFlt3MumoT2BPO98iKTOZ28ES52TuX2A3f9vtILV0omafZMZIt36I8m5kJvUnHHyL6gFv6ga6Kekgq/+Wk9vjrbannq5KZKoN4lgTzPrkul8OiBOk1NxUCUmad9O+hzrPs51f5T69PjvAukqnWrpTaJcMDq6OlDQBbz5ov5wumAzmh39oVk2ALLFVedx2ZlYTpPEzOIOzjAve4nlSslipky+rePr37BZXNMmbMn6v9fbZ87E5czhA/zddC55JIDrEBJ/XzWkzruNPECR85NhS4w+fhCNpjyoMTQW2CDrODPK/PrVOF5PgjL/SQaIIWojrwL/ko6+brjXAjmF8deaep3YEQaHC9BvloIF+WYXz2jtkcEWcKvw4+TOjriF2eVj5efGy9X6Qh5j0hFo2pEJrDSpq3j7ycxCu7BIFZZnhaClCQFnflb5mLW/AVaC6LPsBhliEEWqO6Ro861RCusRf6xKB9IurV/C0Yr5Pj28Jv6+3djxFhvQBzWo6W1HjIRGVplEsJQSU31eZxuwY1nlyEyO1zh+FSPd1V/fJAFAkgY83y1et/XvH7XEr6ftaNTFe6RZ3yIDg3COkxwtsKYlp6M9ykk1bO0zfsCqJDxO/DP4A97q+Jhyu5HM160XuTjMHJanEvRNYJOGG7wKdipVC772/huniiz//vUIlHmSnH+SGE0HaEu1xeXEhoS6LZUHsDZ0zQ69Pk+kfFSLzoArMiYFIpISGqI61XLNDlkBNPWaW6UOk=
  • Suggested_attachment_session_id: 45779444-c494-6445-b65b-3fb1d086bb86
Hi all, 

Frédéric: Thank you for the reference, I will have a look.

Pascal: I intend to use this order to prove the termination of a proof search procedure for a sequent calculus. 

Best,
Ian
From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Jean Goubault-Larrecq <goubault AT lsv.fr>
Sent: Friday, 26 November 2021 6:49 PM
To: coq-club AT inria.fr <coq-club AT inria.fr>
Subject: Re: [Coq-Club] A well-order on lists of natural numbers
 


Le 25/11/2021 à 19:27, Abhishek Anand a écrit :
> i would define an order-preserving function rank: list N -> N and the
> rest should be easy corollaries of the order preservation theorem


Hmm, such a function does not exist, if I am not mistaken.
The order type of Ian's ordering is ω^ω, while the order type
of N is only ω.

-- Jean.

>
> -- Abhishek
> https://aus01.safelinks.protection.outlook.com/?url="http%3A%2F%2Fwww.cs.cornell.edu%2F~aa755%2F&amp;data=04%7C01%7Cian.shillito%40anu.edu.au%7Cbce92dcfe21e457853f808d9b0b259c9%7Ce37d725cab5c46249ae5f0533e486437%7C0%7C0%7C637735717794656076%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&amp;sdata=2sm2YjkYwjvmKqK%2BRqAXFlcS%2BRMTiOfQbbsGA5HEjaI%3D&amp;reserved=0 <https://aus01.safelinks.protection.outlook.com/?url="http%3A%2F%2Fwww.cs.cornell.edu%2F~aa755%2F&amp;data=04%7C01%7Cian.shillito%40anu.edu.au%7Cbce92dcfe21e457853f808d9b0b259c9%7Ce37d725cab5c46249ae5f0533e486437%7C0%7C0%7C637735717794656076%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&amp;sdata=2sm2YjkYwjvmKqK%2BRqAXFlcS%2BRMTiOfQbbsGA5HEjaI%3D&amp;reserved=0>
>
>
> On Wed, Nov 24, 2021 at 11:10 PM Ian Shillito <Ian.Shillito AT anu.edu.au
> <mailto: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