coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Proposition for strictly positive occurrence

From: Yixuan Chen <xlk AT umich.edu>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] Proposition for strictly positive occurrence
Date: Mon, 2 Jul 2018 20:20:34 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=xlk AT umich.edu; spf=Pass smtp.mailfrom=xlk AT umich.edu; spf=None smtp.helo=postmaster AT mail-qk0-f172.google.com
Ironport-phdr: 9a23:CZqxCxcgKsUdkVImA7q1+WgslGMj4u6mDksu8pMizoh2WeGdxcu5Yx7h7PlgxGXEQZ/co6odzbaO7ea4ASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTahYL5+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v9LlgRgP2hygbNj456GDXhdJ2jKJHuxKquhhzz5fJbI2JKPZye6XQds4YS2VcRMZcTyJPDIOiYYUMEuQOMvpXopLnqFcStxazHxWgCP/txzJOm3T43bc60+MkEQze3gMgHt0PsGnOo9XzKawfT+C1w7fOzT7eaP5X1jP96IvTfxA8pPGMXK5/ccrLxUYxCgzFk0ydpIr4ND2WzuQAq3aX4/ZkWO61iGMqqxt9riaxysswkIXFm4AYxk7c+Slnz4s5P8O0RUB4bNK+DZdduTuWO5Z4T88+RWxjpTw0xaccuZGheSgH0JQnyADba/yAa4WI5wjsVOeVITthnXJle66ziw+88US9yODwSNO40FlNripCndnMsm4C2wbP5ciAT/tx5kah2TCR2ADP8uxIP1w4mK7BJ5MiwrM8jIQfvVrfEiPshUn7jrGael0h+uey6uTnZrvmpoWbN49xkgz/PaAums+kDOQlNwgOXnSU+eSm2LL94EL5Xa1GjucqnanBrJDaOcMbq7alDA9Sy4Yv8gqwDzO70NsDhnQHN1JEeBefj4fzIV3OIfb4De2+g1u2ijtryerGbfXdBcDmKWGLu7P8d/4p4ElFjQE30Np35pROC7hHLuilCWHrs9mNPx4pLgWyi83nBdM1gpMaWkqSB66SMOXfvULetbFnGPWFeIJA4GW1EPMi/fO7yCZhwQZML5ns5oMebTWDJtojJkyYZXT2hdJYSDUXuws1TKrnhEDQCGcPNUb3ZLo143QAMKzjFZ3KH9n/nbmA1yf9E5FLNDgfVwK8VEzwfoDBYM8iLSKfJsg7zG4BXLmlDpYijVSg7VCgjbVgKeXQ92sTspexjNU=

Dear Coq users,

I met a situation where I need to define an inductive type like,

Context (f: Type -> Type).

Inductive foobar: Type :=
| something_of: (f foobar) -> foobar
| nothing: foobar.

This does not pass the positive occurrence check, and it shouldn’t. However, the actual definition that would be passed as f should always guarantee to generate only legitimate types. Is there a way to write “strictly positive occurrence” as an proposition in Coq and make it as an hypothesis for f in the client and proved by the provider(s) of f? Thanks.

Best Regards,

Yixuan (Luke) Chen

[Coq-Club] Proposition for strictly positive occurrence, Yixuan Chen, 07/03/2018
- Message not available
  - Re: [Coq-Club] Proposition for strictly positive occurrence, Yixuan Chen, 07/03/2018
    - Re: [Coq-Club] Proposition for strictly positive occurrence, roux cody, 07/03/2018
      - Re: [Coq-Club] Proposition for strictly positive occurrence, Thorsten Altenkirch, 07/04/2018