coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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 22:50:59 +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=ZyfjlvVOgNffxAa9b9YqZyDTPKkbTtpR8btvFDcymG8=; b=MYD+xiAwE/tJyhL7bzDGAC2LEx3Bdbi+LU+8oRJ1ViAYCPsRojkUfCNN9+DLZvsaylkmYta7qe+ViDjre45qeR/wewTM5m9W/+tJtgp4P4WAcHth39ibrZBcbESA1xFuebYYH0prXOCol5tUjiIX6Gf8obCHkQf9Up378LR9QjeSSyBmhhiBYzRJgQefaGbZnBgplPvONjIs8f9TqngZrc1AvWkdXhRJLAz5QXFtVj4y3Cd1FjQnv1AFntxI9cnNmITdbU8lPyq4LP27toXRq21rZkaC4flriYlT6LaEgWNY3fODSZR1vu5+qr26+tXvmhNGQsd6cNbJTAlojstZ3Q==
- Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=FhcV1/C6TUSAvf2PoGiAh4s8QpRJoCiXPOnvnf4HJla/DCsjc5jOnqxWDUPdZbtzlbL+03Ezmta1lpxTgpEeuNagqSgmLCCNf9IsXSWaCi1OdZx4aXD5iOEgeyoILs+QbpPne8j8QpsZjgtdWVqoN87si0JCrKAn3TrVbh/IGgWTG0He/3uk530YiWrUaxluH+m81H6lmlWb3o8DMOBJnrWa6YniXRc8XW6IXLwG1HPIC+tCvCSDyzA23TFHK/vkrs+86V9mXHL9/WDLhUOfaDXp1ttdy9HvfYd7tfE1F5PVDZOxEZkXIR39V0KcUkbpiIJsGde6dygkUC8/qhzihw==
- 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:13Hox6vxbfv5wdfxbUFcIZFAVefnVGtfMUV32f8akzHdYEJGY0x3m2sWDDzUP/qKZTOgLdB0atvj/EkOupDdydJrS1Ruq3xEQiMRo6IpJ/zJdxaqZ3v6wu7rFR88sZ1GMrEsFC2FJ5Pljk/F3oPJ8D8sislkepKmULSdY3krFFc+IMscoUsLd9AR0tYAbeeRWFvlVePa+6UzCXf9s9JGGjp8B5Gr9HuDiM/PVAYw5TTSUxzkUGj2zBH5BLpHTU24wuCRroN8RoZWTM6bpF21E/+wwvsjNj+luu6Tnkwia4PpZVHLsUsKHq+oj15FuzA41bs9OLwEc0BLhj6Vntd3jtJQqZi3TgRvNarJ8Agfe0UAVXgmYusfoOCBcCPXXc+7lyUqd1PNyvMoN0E3OYkZ5uFfCGdTs/EUNXYEc3hvgsrpmOjnFLIz7igkBJKyZ9hA0p169hnSCu9jSpTeSY3R9NpA1XExgNpPFLDQfaIkhZBHeEyVOFsSLg5CUNRmiL393j+lLmMGvAnA/exq9zeG5RJX+73LHNrxW9Wsed9zoEe9sjueqj+9WQVy2Me3zDOE9je3l7PGgDijAYUUTuXprbhtnUGZwXEVBFsOT1ynrPKli0m4HdVCN0gT/Slopq83nHFHh+LVB3WQyENodDZFMzaRLwE71O1J4oPp2F7AQ1M1EntGYtFgs9IqTzs30FPPh8nuGTFkrLySTzSa66uQqjSxfyMSKAfuoAcaGBAd7YCLTJ4b13ryohRLScZZTeEZ3Rn5xS3MoSQjwbwO5SLO/7vu5kjJ2lpAubCQJjPYJWzrsqaN5wVkIoOpesqh9DA3KN4owJmxFjG8gZTPpyRSAC3iw31AeOxhjdjhxI2U2ss=
- Ironport-hdrordr: A9a23:S4k7Ta6caLu8SCf2DQPXwZqCI+orL9Y04lQ7vn2ZFiY5TiXIraqTdaogviMc0AxhIE3I6urwQ5VoIEmsuKKdhLN8AV7MZniDhILFFuBfBM7ZskTd8k7Fh6JgPMVbAs9D4bTLZDAU4/oSojPIderIq+P3k5xA8N2uqkuFOjsaCZ2IgT0YNi+rVmlNACVWD5swE5SRouBdoSC7RHgRZsOnQlEYQunqvbTw5dzbSC9DIyRixBiFjDuu5rK/OQOfxA0iXzRGxqpn2XTZkjb++r6ov5iAu17hPi7ontRrcenau5l+7f+3+40ow/LX+0KVjbFaKv6/VfYO0aaSARgR4Z/xSlwbTr5OAjvqDxyISF3WqkbdOX8VmgDf4EWFj3Xuu9H0SQQzFtdIj4NcfhzF3VAtpst91qV832/xjesqMTrQ2C7n59LPTXhR5ziJiGtnnugJg3NFV4wCLLdXsIwE5UtQVIwNBSTg9ekcYaFT5eznlYBrmGmhHjnkV6hUsa+Rd2V2Gg3DTlkJu8ST3TQTlHdlz1EAzMhamnsb7poyR5RN+uyBa81T5ftzZ95Tabg4CPYKQMOxBGCISRXQMHiKKVCiEK0cIXrCp5P+/b1w7uC3f54Dyoc0hf36IRhlnH93f1irBdyF3ZVN/ByISGKhXS71wsUb/JR9sq2UfsudDcRCciFbryKNmYRvPiTrYYfHBHsNOY6cEYLHI/c44zHD
- Ironport-phdr: A9a23:8qAWxBNJLX8uQUaQJFkl6nZAChdPi9zP1u491JMrhvp0f7i5+Ny6ZQqDv6wr0geBdL6YwsoMs/DRvaHkVD5Iyre6m1dGTqZxUQQYg94dhQ0qDZ3NI0T6KPn3c35yR5waBxdq8H6hLEdaBtv1aUHMrX2u9z4SHQj0ORZoKujvFYPekdm72/qz9pHPfg5FmCezbbRuIRussA7frNMWgYxsKqYwzhvGvH5FcPlIyG1rOFyegQ/y6t+/85B//StQvekh99NbXqXhY6s4V71YAy84PG0z+cbmqAPMTQqL5nsbT2UWjh9FCBXL4R3mQpv8tDbxu+xg0yeYIML2V6g5VzS84al2VB/mhiQJNzA7/27LhcN9l7hUrA69qxFl34LYfJ+ZOfxjda3dZ9MaQm9BU95SWSNbBIO3cpYBD+oAPeZcq4n9pkcOrRyjDgSrB+3g0DlIimXr06060uQhFQXG3A08H9IJq3nbttP1NLoIXe+r0abI0C/PYOlL2Trk7oXDbx8ur+2WU71qbcrR1VcgFxnDjliIt4HoIzOY2OsTvmSF7+dtVO2hhmEnpQxtrTaiyMchh5fVi48WxF7J9CZ0zYk3KNO3S0N3fN6qHIVTui2HNIZ6X8UvSHxmtiY9z70Jo5+7fC4SxZQg2h7fd/iHc4+P4hLgTuqePTB4hHd9dLKwhhay7UigyvDnWcWuzFlKqS9Fn9/RvX4Ozxze8seKRudn8ku8xTqC1Rrf5vxYLU02j6bWL5AszqYumpcSrUjOECr7lFjqgKCKd0gp//Wk5/jib7n7ppKTKop5hwTjPqkgnMG0HP42PRIUX2eB/OSxzL3j8lP9QLVNlvA7jqfWvo3GKcgGv6K3Hg1a34k65xa4FDipzs4UnX4aLFJZYx2HiJXpO1fTL/ziFfe/mVOskCt1yP/aIr3hA5LNLn7ZnLfmYLZ990pcyA00zdBc/Z5bFrYBIPfrVk/wstzXEAM5PhS7zur7Etlxy58SVGCVDqOELK/fs0WE6+YhLuWUYY8aojf9K/wr5/70in85nEcQc6qz0psRcny2A/RmI0SdYXrog9cBDWAKsxEkQ+zslV2OSyBcaGuvX64m/D47FZqqDZ3fSYC1nLyBwCC7E4VKaWBBE1CACGvnd4GZW/gXcy+SOc9gkjkcVbe7UYMh1BeutBX7y7V9NObU9DcY5trf040/7OrK0Bo26DZcDsKH0mjLQXs+1jcDQCZz16Riq2R8zE2C2O52maoLO8ZU4qZoWwFyDp7dy+h7F9e6DiPIeJGySFeiRtS6Bhk4SM93ztMTJU9gTYbxxivf1janVudG34eAA4Y5p/q0N53ZLsBgjXvKye8okgt+KiOuHUSbvfYmsjPiW8vOmUjfkLu2f6MB2iKL7H2E0WeFoEBfVkh3TLnBWnccIEDRqIagjqstZ7aoFPIqPhYHwNPQc8N3
- Suggested_attachment_session_id: 7e9cdd04-ce2f-06bf-7ee4-fe1c99758b5e
Hi Daniel,
This is indeed quite similar to what I had in mind. Thanks for sharing your code!
Best,
Ian
From: coq-club-request AT inria.fr <coq-club-request AT inria.fr> on behalf of Daniel Schepler <dschepler AT gmail.com>
Sent: Tuesday, 30 November 2021 6:25 AM
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] A well-order on lists of natural numbers
Sent: Tuesday, 30 November 2021 6:25 AM
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] A well-order on lists of natural numbers
On Sun, Nov 28, 2021 at 10:18 PM Ian Shillito <Ian.Shillito AT anu.edu.au> wrote:
> Pascal: I intend to use this order to prove the termination of a proof search procedure for a sequent calculus.
If that's the use case, then I have something vaguely similar already
implemented (in a past version of Coq, but hopefully not too much
needs to be updated):
https://aus01.safelinks.protection.outlook.com/?url="https%3A%2F%2Fgithub.com%2Fdschepler%2Fcoq-sequent-calculus%2Fblob%2Fmaster%2FLJTStar.v&data=04%7C01%7Cian.shillito%40anu.edu.au%7C349c0e31acb94f4168fd08d9b36e1da2%7Ce37d725cab5c46249ae5f0533e486437%7C0%7C0%7C637738108364632152%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=mW8WfmMxUXVa%2F2OyfTZxwjWOEf0nI0WBpZxX6Zjy6fQ%3D&reserved=0
. There, I have a function context_cost that takes in a list of
propositions, and returns a list of counts of how many propositions
there are of each cost (calculated using prop_cost, result list
starting at cost 0 and going up to the maximum cost). Then, I have a
relation context_cost_lt which is reverse lexicographic order on that
list of counts, and a proposition context_cost_lt_wf which shows that
relation is well-founded. (And then, I have a series of propositions
that each manipulation in the LJT* search procedure strictly reduces
the context cost. I never actually got around to implementing the
full search procedure and using those propositions to show it
terminates, though.)
--
Daniel Schepler
> Pascal: I intend to use this order to prove the termination of a proof search procedure for a sequent calculus.
If that's the use case, then I have something vaguely similar already
implemented (in a past version of Coq, but hopefully not too much
needs to be updated):
https://aus01.safelinks.protection.outlook.com/?url="https%3A%2F%2Fgithub.com%2Fdschepler%2Fcoq-sequent-calculus%2Fblob%2Fmaster%2FLJTStar.v&data=04%7C01%7Cian.shillito%40anu.edu.au%7C349c0e31acb94f4168fd08d9b36e1da2%7Ce37d725cab5c46249ae5f0533e486437%7C0%7C0%7C637738108364632152%7CUnknown%7CTWFpbGZsb3d8eyJWIjoiMC4wLjAwMDAiLCJQIjoiV2luMzIiLCJBTiI6Ik1haWwiLCJXVCI6Mn0%3D%7C3000&sdata=mW8WfmMxUXVa%2F2OyfTZxwjWOEf0nI0WBpZxX6Zjy6fQ%3D&reserved=0
. There, I have a function context_cost that takes in a list of
propositions, and returns a list of counts of how many propositions
there are of each cost (calculated using prop_cost, result list
starting at cost 0 and going up to the maximum cost). Then, I have a
relation context_cost_lt which is reverse lexicographic order on that
list of counts, and a proposition context_cost_lt_wf which shows that
relation is well-founded. (And then, I have a series of propositions
that each manipulation in the LJT* search procedure strictly reduces
the context cost. I never actually got around to implementing the
full search procedure and using those propositions to show it
terminates, though.)
--
Daniel Schepler
- Re: [Coq-Club] A well-order on lists of natural numbers, (continued)
- Re: [Coq-Club] A well-order on lists of natural numbers, Michael Sÿfffff6gtrop, 11/25/2021
- Re: [Coq-Club] A well-order on lists of natural numbers, Dominique Larchey-Wendling, 11/25/2021
- Re: [Coq-Club] A well-order on lists of natural numbers, Vedran Čačić, 11/25/2021
- Re: [Coq-Club] A well-order on lists of natural numbers, Abhishek Anand, 11/25/2021
- Re: [Coq-Club] A well-order on lists of natural numbers, Ian Shillito, 11/26/2021
- Re: [Coq-Club] A well-order on lists of natural numbers, Dominique Larchey-Wendling, 11/26/2021
- Re: [Coq-Club] A well-order on lists of natural numbers, Jean Goubault-Larrecq, 11/26/2021
- Re: [Coq-Club] A well-order on lists of natural numbers, manoury, 11/26/2021
- Re: [Coq-Club] A well-order on lists of natural numbers, Ian Shillito, 11/29/2021
- Re: [Coq-Club] A well-order on lists of natural numbers, Daniel Schepler, 11/29/2021
- Re: [Coq-Club] A well-order on lists of natural numbers, Ian Shillito, 11/29/2021
- Re: [Coq-Club] A well-order on lists of natural numbers, Daniel Schepler, 11/29/2021
- Re: [Coq-Club] A well-order on lists of natural numbers, Ian Shillito, 11/26/2021
- Re: [Coq-Club] A well-order on lists of natural numbers, Frédéric Blanqui, 11/26/2021
Archive powered by MHonArc 2.6.19+.