ssreflect - [ssreflect] Finfun and positivity requirements

Subject: Ssreflect Users Discussion List

List archive

[ssreflect] Finfun and positivity requirements

From: Joshua Gancher <>
To:
Subject: [ssreflect] Finfun and positivity requirements
Date: Fri, 15 Feb 2019 14:00:24 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None ; spf=Pass ; spf=None
Ironport-phdr: 9a23:kd473hKaKyreLRzg4NmcpTZWNBhigK39O0sv0rFitYgRKvjxwZ3uMQTl6Ol3ixeRBMOHs6IC07KempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffwZFiCChbb9uMR67sRjfus4KjIV4N60/0AHJonxGe+RXwWNnO1eelAvi68mz4ZBu7T1et+ou+MBcX6r6eb84TaFDAzQ9L281/szrugLdQgaJ+3ART38ZkhtMAwjC8RH6QpL8uTb0u+ZhxCWXO9D9QLYpUjqg8qhrUgflhygHOTA382/Zl9J+g75ArR27uxBy2ZTZbJ2JOPd8eK7WYNMURXBGXsZUTyFPBoS8b5APD+ocJ+lTsojzqEEIrRSiBQmjGvnvwSJPi3/0x6063OosHAHF0QE7A90Ot27UrNPrO6cWVeC51rfHwijeb/5P3zr29YvGcgg5rP2SQb59ddDdxEovGg/fk1mdqI3oMymI2ukPsmWW6fdrW/i1hG49sQ5xpyCixscyhYnNgYIY0lXE+j94wIYxPNG4SVJ7bcO9HJteqi2XNYp7TtktQ2FvvyY6xbkGtoChcCcWz5QnwgbTa/2Bc4eW/hLuTPidLSt8iX5/e7+yhwy+/VWhx+D9TMW4zVRHoytdntnJrH8N1hjT6sadSvt6+0eswTSP1xrc6uxKIU05lrHWJIImwr4qkJocr0DDHivslErokaCWa10o+vK05OT/frXmupicOpdvigHlKKQhhMK/AeAmPQcSQ2iW4v+81b3m/U3hWrpGlPw2kq/DsJDbP8sXvKC5AxUGmrokvg2kFTqo1NkTgVECN0gAeRSdjoGvOlfUIfm+A+3srU6rlWJJwOvGI7SpLZzLJXjOiv+1f6xysBMM4AE019ZS45YSB70cdqGgEnTtvcDVW0dqeze/xPzqXY0kh9EuHFmXC6rcC5v89FqB5+YhOe6JPdRHszHnLfUh47jjgWJrwAZBL5ns5oMebTWDJtojO1+QOCG+idAbF2oOukwzQPG40ATfAw4WXG67WucH3h9+CI+iCt2dFIWkgbjE3TviW5MPOT4ABVeLHnPlMY6DXqVUZQ==

Hi all,

Consider the below datatype, where T is a finType:

Inductive TstF :=

| TBase : nat -> TstF

| TF : (T -> TstF) -> TstF.

I would like to leverage the finType structure of T in order to give a choiceType structure to TstF (up to extensionality of the function in TF). Thus I want to do something like:

Inductive TstF' :=

| TBase' : nat -> TstF'

| TF' : {ffun T -> TstF'} -> TstF'.

However, the above does not go through, since it violates the strict positivity requirement in Coq. (Indeed, replacing {ffun T -> TstF'} with something like {xs : list TstF' | P xs} where P is a pred also violates the same requirement.)

Has anybody thought of a workaround for this issue?

Thanks,

Joshua Gancher

[ssreflect] Finfun and positivity requirements, Joshua Gancher, 02/15/2019
- Re: [ssreflect] Finfun and positivity requirements, Assia Mahboubi, 02/21/2019
  - Re: [ssreflect] Finfun and positivity requirements, georges gonthier, 02/27/2019
    - Re: [ssreflect] Finfun and positivity requirements, Joshua Gancher, 02/27/2019
    - Re: [ssreflect] Finfun and positivity requirements, Erik Martin-Dorel, 02/27/2019

List archive

[ssreflect] Finfun and positivity requirements