coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Non strictly positive occurrence

From: Stefan Monnier <monnier AT iro.umontreal.ca>
To: Clément Pit-Claudel <cpitclaudel AT gmail.com>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] Non strictly positive occurrence
Date: Tue, 24 Aug 2021 10:21:30 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=monnier AT iro.umontreal.ca; spf=Pass smtp.mailfrom=monnier AT iro.umontreal.ca; spf=None smtp.helo=postmaster AT mailscanner.iro.umontreal.ca
Ironport-hdrordr: A9a23:RAUERqH6RDs3n64QpLqEMseALOsnbusQ8zAXPo5KKCC9Ffbo7/xG/c5rrCMc7Qx9ZJhOo6HkBEDtexzhHNtOkO0s1NSZLW/bUQmTXeJfBOLZqlWKcUHDH6xmpMVdmsNFaOEYY2IVsS+32njeL/8QhOO/2ITtpcDw6R5WPHpXQpAl1T5QLkK/PnJbYWB9dOAEKKY=
Ironport-phdr: A9a23:V5GpAhRUaCEYijF+cOvjcf+iNtpsosSYAWYlg6HPa5pwe6iut67vIFbYra00ygOTBcOKsrkZ1KL/iOPJYSQ4+5GPsXQPItRndiQuroEopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZvJuTyB4Xek9m72/q99pHNfwlEnj6wba59IBi2rwjaq9Ubj5ZlJqst0BXCv2FGe/5RxWNmJFKTmwjz68Kt95N98Cpepuws+ddYXar1Y6o3Q7pYDC87M28u/83kqQPDTQqU6XQCVGgdjwdFDBLE7BH+WZfxrzf6u+9g0ySUIcH6UbY5Uim54qx1VBHnljsINz8h8GHWlMNwir5boAm8rBB72oLYfZ2ZOOZ7cq7bYNgUR3dOXtxJWiJBHI2ycogBD+QPM+laoYbyqEcBoxSlCAmwHePi0CNEimPs0KEn1ekqDAHI3BYnH9ILqHnascn1O7kcUe+vyqnD0DLNb/RQ2Tf76YjHbAohquyLULJ1dsrRz08vFwLbgVWKsoHlPimV1uMXv2iG6upgUuSvi3I9qw5vuDevwt0ghZXTiY8MzF3P6Cp2zpovK9KiVE57fcCrEIFWtyyCK4Z7QMIvTWF2tSs11LEKpZq2ciYWxZg7yRPSduKLfYiU7h7/W+icJSp1iXFqdry/mRu8/kytx+LyWMS30FtHrCxImcTCuHAK0hzc8MmHSv1l80i7xTmP0hrf6uZeIUA7k6fQNp0vwqYom5YOv0nPADX6lFvqgKKZbEko5Oil5/7nb7n6vpOQKpN4hw7kPqgwlcGyA/40PhYBUmWU4+iwybPu8E3/Tb5XlPM5iLPZv4rfJckDpq62HQtV0oE75ha6FTim0dAYnWIbI11ffhKHiZbmO0vULPD5F/e/hE6gkCpux/DBOL3hHo/NIWbZn7flZ7py91RTxBIyzdBZ+Z1UFqkMLO/9V0PvrtDUEAM1PgOuz+r5CNhxzIMTVX6XDq+cKqzSsFuI5uw1I+mLYY8YoDP9K/8j5/7ojH82h0UdcLKo3ZsNb3C0BOlmI0CeYXrqntcBC3kFsRA6TODwlFKNSyZfZ2yuUKIk+jE7FIWmAJ/fSYCqmbyNxTu0HplLZm9dEV2MCnfpd4CcW/gWci6SI8lhkiYFVbe7UYMh2wuu50fGzO9MKmvR9ysE/ariyJ1e4+TOmRw2vWh/F8WB2GWEUm15mksHQjY32OZ0pkkrmXmZ1q0tuOBVG9VVr9ZOVAE7OISUm+l9DdbzVxjpf82ODkujRdO6Gzw4SpQ6yoldMA5GB9y+g0WbjGKRCLgPmunOXcRsmko593nrIIBgznHAyLMshl1gScIdbQVOZ4Z6/gnXHIXAlUOUjeCrb6NawSvK8nuZwGOK+kpRAlYYuUrtXGoYIFbTqtLl/E7LS/mlAOZ+WjY=

Clément Pit-Claudel [2021-08-21 21:59:57] wrote:
> On 8/21/21 5:01 PM, Marco Servetto wrote:
>> Dear List, I'm trying to model a problem in COQ but I got stuck. My
>> minimized problem is the following:
>>
>> Inductive Bool : Type := | T | F.
>> Inductive A : Type :=
>> | myA : (A->Bool)->A.
> You minimized the problem too far, and Coq's concern with this type is
> legitimate. The problem is that this definition would let you build
> non-terminating functions, and from there prove False.

Another way to look at it is to say that the definition is acceptable,
but that the allowable elimination rules for this type need to be more
restrictive than what we usually allow for inductive types.

E.g. https://dl.acm.org/doi/10.1145/2034773.2034807 suggests that
a catamorphism could be offered without breaking soundness.

Stefan

[Coq-Club] Non strictly positive occurrence, Marco Servetto, 08/21/2021
- Re: [Coq-Club] Non strictly positive occurrence, Clément Pit-Claudel, 08/22/2021
  - Re: [Coq-Club] Non strictly positive occurrence, Stefan Monnier, 08/24/2021