coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] well-founded induction on the size of the derivation tree of Prop

From: Jan Bessai <jan.bessai AT tu-dortmund.de>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] well-founded induction on the size of the derivation tree of Prop
Date: Sun, 3 Feb 2019 01:20:25 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jan.bessai AT tu-dortmund.de; spf=Pass smtp.mailfrom=jan.bessai AT tu-dortmund.de; spf=None smtp.helo=postmaster AT unimail.uni-dortmund.de
Ironport-phdr: 9a23:TT4dmRD06yZ72CYNJPtsUyQJP3N1i/DPJgcQr6AfoPdwSPvzo8bcNUDSrc9gkEXOFd2Cra4c26yO6+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglUhzexe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Xymp4aV2Rx/ykCoJOT43/n/KhMJzgqJUrw6uqAF9zIHae4yVKOZyc7nBcd8GX2dNQMBcXDFBDIOmaIsPCvIMM+JCoIn7ulADsAWxBRK3BOz1yz9Dm3j73a8g3OQnCw3JxxIvH8kVsHvOrdX4L7sSUf2swKbVyjXDde9W2TLg6IjObx8tu+yDUqxpfMfX1EIhGQTFjlCKpozkOTOYzusNs2mH7+pgSOKgkHQrpB12ojiqwMonl4rHhpoNx1zZ6yl0xJw5KcOlREN5e9KoDYVcuiKAO4Z2X88uW2JltSYgxrEYp5K3ZjUGxIgmyhLFZfGLb46F6Q/5WumLOzd3nndldaq/hxms9UigzfXxVtSy0FZLqypKiNjMtnQX2xzO7MiHS+Jx8Vqm2TaVywDT7/xEIUYpmqbBNpEu3KY8lpsVsUvdAi/7gFj6gLGSe0k+5OSk9ubqbq/7qpOCNIJ4kAHzPrk2lsy6G+s4MwwOX2aB+eS70b3u5U/5T69MjvEsiabWrovaJd8Bqa64GAJVzpsj5w+iADehytQYgXwHLE9DeB2alYTmJk/BLOjiDfijm1SsjCtrx/feM7L9BZXNN2HPn6vlfbZg8EFR0xEzzNBa55JMEL4NOvPzWknrtNzZFBA1KQK0w/y0QOl6g4gZQCeEBrKTGKLUq16BoOw1cMeWY4pAmj/7Y9Io/OXnjDdtm1YbO6OkxoAeaVikA7FqJF+FZGfqjpENHDFZ7UIFUOX2hQjaAnZobHGoUvdkv2BpOMedFY7GA7uVrvmE1Sa/EIdRYzkYWEyRVHvvbZmBRvEALi6fcJY4zm40EIO5Qopk7imA8RfgwuM5fPbJvyEfr47myd55oeHex0lrqG5ESv+F2mTIdFla22MFQzhsgfJip014w1aHl7V+grlUEsZP4u5PXkE2OMyEwg==

On Sat, Feb 02, 2019 at 09:54:42PM +0000, Jason -Zhong Sheng- Hu wrote:
> Is there any way out so that well-founded induction can be done intuitively?

Jason,

you might find the trick Larchey-Wendling and Monin presented at Types 2018
very useful:

https://github.com/DmxLarchey/ite-normalisation

Their method is to define a relation first (instead of the function) and
then show that it is a total function. This way, reasoning about size is
decoupled from the proof and often you can express the termination
certificate such that you do not need well-founded induction.

Also look into small-scale inversions, they come in very handy when
using this trick.

-- Jan

[Coq-Club] well-founded induction on the size of the derivation tree of Prop, Jason -Zhong Sheng- Hu, 02/02/2019
- Re: [Coq-Club] well-founded induction on the size of the derivation tree of Prop, Fabian Kunze, 02/02/2019
  - Re: [Coq-Club] well-founded induction on the size of the derivation tree of Prop, Jason -Zhong Sheng- Hu, 02/04/2019
- Re: [Coq-Club] well-founded induction on the size of the derivation tree of Prop, Matthieu Sozeau, 02/03/2019
- Re: [Coq-Club] well-founded induction on the size of the derivation tree of Prop, Jan Bessai, 02/03/2019