coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] [Coq-club] return annotation on a match clause leads to missing information

From: Merlin Göttlinger <megoettlinger AT gmail.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] [Coq-club] return annotation on a match clause leads to missing information
Date: Tue, 30 Jan 2018 12:58:11 +0000
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=megoettlinger AT gmail.com; spf=Pass smtp.mailfrom=megoettlinger AT gmail.com; spf=None smtp.helo=postmaster AT mail-it0-f41.google.com
Ironport-phdr: 9a23:EMS05RNcO1NtFTRz3fQl6mtUPXoX/o7sNwtQ0KIMzox0LfvyrarrMEGX3/hxlliBBdydt6odzbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxlViDanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0yRD+s7bpkSAXwhSgINzA3/mLZhNFugq1Hux+uvQBzzpTObY2JKPZzfKXQds4aS2pbWcZRUjRMDISiYIsVC+oBPOBYoJH8qUMIsRu+GQ2sBOLpyj9HmHD2x7Ax3uMkEQ7Y0wwgGMwBsGjIrNXxNacSV++1w7fSzTjYYPNW3C3y6InMchw7vf6MWrdwfNPXxEIyGQ3FiVCQppbkPzOTzukNvGmb7/ZgVeKykGErsR1+oj+qxsoql4LHhZoVx0ja+SllxIs5P961RU5hbdK6DZdduDuWOoRrTs4kXmpmojw1yqcctp6+ZCUKyIooxxrYa/GfdoiH+BPjVOKILTd5mHJpZKuzhxi9/ES90OH8Wc600FFFripBjNbArGwC1xvW6sSfS/t9+Fmu2SqX2gzN9u1JJVo4mKnbJpI73LI8i5UevV7MEyPrgEn2ibWZdkQg+uim8eTnZbDmq4eZN4BqhQH+NbohmtCjAeQ8MwgOWWeb9vqm1LD48k35Ra9FjvwykqXDrJ/aIsEbqrajAwBJyoYj9wq/DzC+3dsEmnkHNUtJdw6Dj4j0IF7DO+v4DPe6g1S0ijhn3fHGPrv7ApXMNHfPirnhfawuo3JbnUA4yska7JZJAJkAJujyUwn/rpaQWhQ+Kkm/x/vtINR7zIIXH2yVVPy3KqTX5HqF/OYuJd6j+pMJvDf7JPU/r6rrgHA+lEMBeaiv0pYNQH+9F/ViZU6eZCy/0Z86DW4Ws19mH6TRg1qYXGsLPifgb+cH/jg+TbmeI8LGT4GpjqaG2X7iTJJTb2FCTFuLFCWxLtnWa7I3cCuXZ/RZvHkcT7H4Et0u0BivsEnxzL81drOJqB1djorq0Z1O38OWlRw28mYpXcGU0mXITn0s221UHnk526dwpUE7wVCGg/B1

Hi,

it took me quite a while to figure out why my Program Fixpoint (and refine with Fix as well) generates missing contextual witnesses in the proof obligations making the goal unprovable. I had that happening previously when the recursive calls were made inside a higher order function (which did no longer seem to be unfolded when a measure function was involved) but that could be resolved by specialising that higher order function to pass the necessary proof along as well. But here the recursive call is "direct" and not nested in some other fuzz that could confuse Coq.

Self contained example showing this behaviour: https://gist.github.com/mgttlinger/ea0654dcf71b8937a7c67231e0c625f9

Can someone explain why this is happening?

Cheers,

Merlin

[Coq-Club] [Coq-club] return annotation on a match clause leads to missing information, Merlin Göttlinger, 01/30/2018
- Re: [Coq-Club] [Coq-club] return annotation on a match clause leads to missing information, Ralf Jung, 01/30/2018