coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Pierre-Marie Pédrot <pierre-marie.pedrot AT inria.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] function extensionality with finite domains
- Date: Tue, 11 Sep 2018 13:19:36 +0200
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=pierre-marie.pedrot AT inria.fr; spf=SoftFail smtp.mailfrom=pierre-marie.pedrot AT inria.fr; spf=None smtp.helo=postmaster AT korolev.univ-paris7.fr
- Autocrypt: addr=pierre-marie.pedrot AT inria.fr; prefer-encrypt=mutual; keydata= mQINBFOFpSQBEACyDotTWHydRK+7nzdk+ULrBszrG8Eu7J59+eogMOIOQYKw/joFiTOHnJgG vUzt//PqMURC7tZ72teZHeyLKHwr3a9oOC4W36Wrt4jVGvAnYk60hF20i921ljIN8aj41UYz t+8vgsqgpTCNbcgxhhgXSQ+9n/OZs1yoy6kgIE378HsIhGoGTQxmwdz2k0Aic/qun2Z4CO9v zjTjkUYMJxs4XwVsprMkO/a6qVBkNtEjbwVDJS5d7qzfph2DHJXFyUOPc1GudPI+VW2Abi4A 2US/ycyGMUTYRVaUDUF/GqfqmYgUj4vFvANdB3Roa3XDVxAlkYcNuUqtcpQi9yoU6t+Agobp nqcn+WrtOwrJtvEh3KaaQvI4Yudz3pEmP9KL2VYenUQLuDqVL4KgdCPcAZmpkSC7KCm8Ns2v y69zHasNsPD9YiIXCgpGNZEEUjrG8Si+ej3/3MTqTBQqpSzqTagtGhGANrjEgHj6zdh+plby k/bCYHjX4oDPJZQx6GjmtGPandUAD+SImEwS6WMyCKtUSKJtqD+DVNWiwKAK3+CNxDW/DbRS /N2ACdtItJhFmPAb9Nxs6O27xyPCse4n9fMCT5pLQpDfMmkOQsjr1kCWiOWgjIgfOG64HrxQ Vcjg6mf9EEGVi4kpMhl6RzZ7wsg+ff3w/5NR1e1HX9yj/UbsLwARAQABtFBQaWVycmUtTWFy aWUgUMOpZHJvdCAocGllcnJlLW1hcmllLnBlZHJvdEBpcmlmLmZyKSA8cGllcnJlLW1hcmll LnBlZHJvdEBpcmlmLmZyPokCVAQTAQgAPhYhBLpHqR+RBOchhNcPbXkiwB/Zujx7BQJZUDB2 AhsDBQkSzAMABQsJCAcCBhUICQoLAgQWAgMBAh4BAheAAAoJEHkiwB/Zujx73igP/RnN2JxV tZ5+Z4Rp9R2hmm/yDAj/kzdc0RyEJ/TkHsW6YLtKSiH5UkLRilUesIiRr4th3RVd8MYcTiOR AtIlyR1Z5xAtMmtw5l6pChiu/75h0KXNBoHfQlJH3IBVkEMgCVy0YwPOEpCTmxOhOApUUUPa enTPXgHViCCVijpgDA28fj4pBz7+U6OmvDk4Etouv5cM4gu9COh6h/O/79cAb5aF/5DN7bPa RSn1+Yg6j0AfF/czQLIeaaCy4cCQOFV2ikl/uViOwTcnjZQpfXwMtV7kmP5lRks8TjJcb6pp 0Iv0PJivq21BA2L0aCQCuxvtTkSZYuQANRiBtEGI6Wb+CFf6Vsf3KpxMB08/ULJISMKZR4zA cqWAW9qjx0JEeOcjiDmWNdF6VI4rZagNIA9O73FIlXd6ymht3QZH6s1zKhvwJnmUZG8HnqrS QxL/yuEDpBCjO4/XfaS7G+Y6yN9/q7Hynx365tNnpzkuZKVLGuo0o80O9qkR4jw40x69Zud9 7229HxrUuwUCgohISQyGc+BS5VqXHrT8J2t4FhEPd9JMx+XD2FV4nn9XIrxfm9U6ymSg3cBR Lfww1+ADWuMbHr6K9djtcmdkaw0nmci+Z+1ZHnQjoYbvVs5ym/8d024W9/GXfu49MGVT6Uj5 +kme9Aa1/VdBH7LTThfLET0ovZfsuQINBFOFpSQBEADMsZKO9fPtbmyMlS5YQl3B+p5E17sE JAHSNGA4rfx7Uxij1H1PnTZ0kHhngrhEG1wzv2+1aORCg31Jqrwf//XPbcv6QL4CinD7QUpb MdrZFo296AkAjuhO8J0LvB8CY3GY6n/G3njy9ISmemEH3dAzOM87Wt0En1dcSYJxdfM2fmWq 6ghlmcQA6A6g1vJ0iKnFcvh/IXHBm1/dtVSOj+2+S4/PLALMCUzugFQLVAKiv7pkdxPzKGxM MEnQuLXjoFivXV6i3q9+0FVVo2t9LfD1EzTNoKwx4866nVnVMU9myd6IS03lKAREmHhbYRKJ t+dlmJoqttVczsruFa1SRmzhpp5O2jFWzR0C+SD23s70PXaZ4wcn4TzQKL+tGMRqELLFXepq WcmKnROvX+agmeZK1UxhaIGI0JpPtZHsNGNoU1dbzUE+opzHP5Lpouc5Te+MkXe4wSM6Wrfy TRqUfVr7CeaSozkX/AfgubNnNYmi8RduUjUBjukMEsRchirbyCh1397xK90HDpiiqPy/PLaU x/sp2vp0TSxGPFtl9CmuSOPVi0HQI51SrnckMA/zQJu6AZyFkbb7fpUi/cPds7AVCLjdmNkL Oe77sZ+/D3YKXiHujrpncau+NaQ2SKMrqcRocAeogbd+VV3DFGRgHereAZwHD87ruHegjEO9 2QRw/QARAQABiQIlBBgBAgAPBQJThaUkAhsMBQkSzAMAAAoJEHkiwB/Zujx7eSsQAJnwyYs/ yiYjwzYdlmGQP1fuG0RG6DwHXZDti9etXRhjgOMvE4+TKqSeM9gXCxdGE7M2aKV+PJvitwb4 FRLBOl9YwlHTiV5UIJpcbJv+zvdNSDrlqSSln1Qfqq7HJUvDwSKcY8316pVuF5Q9gknXP/gR G4O8e/fBXuSiL08cDudnkbhSm6zb+VGaewivO0FuuCX4RpYtF4EULbCKof7SSCK3/WWlroX6 H3S6dNo/3cUGahj7FfTaQMwHH34P6wGWtJCh7vhaxQ5QdXjj8ZkJfcE03uo+GbF7/xmog5wx tsFUWhs5G0P534BmahBBKsINIyExt6JYASYL/oouC9c+AOjc3bON7Ae1jeHgx3BSSUju81x+ 5MrXAqrLhJ6xDsQpATL7qDcBEHBodo0xlAIgb71qeIU5gZUOw/43eJOnexDFs4VWMthJz2ot 6WdRzYEKt75nuCZqaaUEM+MvOGNZZRM3Dkbqw3Jik1X+lOjc/OgUs+Xn9oaIylA1nojO9E31 ulGmniydilLd+4Vd+WQn0ZEwy75EzDTl0Ne/j8nvLyzeYIWbt5/06mR2L87DIEXmXkAMmwfF XNzzX9gVX8m7owb4CPTf5DCDrguwNdvcPePy81w+fXM7c0Dq+5hzPvh5MRruEDOfqaZwHXQ4 ZkGmhsCD6dMF2cKX+EqLjopA136U
- Ironport-phdr: 9a23:tS6JNRJVn0p9PtBdANmcpTZWNBhigK39O0sv0rFitYgeLfzxwZ3uMQTl6Ol3ixeRBMOHs60C07KempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffwdFiCChbb9uMR67sRjfus4KjIV4N60/0AHJonxGe+RXwWNnO1eelAvi68mz4ZBu7T1et+ou+MBcX6r6eb84TaFDAzQ9L281/szrugLdQgaJ+3ART38ZkhtMAwjC8RH6QpL8uTb0u+ZhxCWXO9D9QLYpUjqg8qhrUgflhjoZOT438G/ZicJ+g6xUrx2juxNy2IHUbJ2POfR5Yq/Qc9EXSGxcVchRTSxBBYa8YpMVAeoAI+lYtZP9qEUXoRW5HwasHuLvxSFQiXHsx6o1zv4hEQba3Ac9GN8OqHXUo8vvNKcIT++51azIwi/Zb/NXxzjx8pDIfQ48rvGWWrJwbdHcyUgpFwPfj1Wfs5bpPz2P1ukUtWWQ8uRuVeWqi2E9qgFxpCCix8gqioXQn44V0k3L9T9+wIYpPNG3U1V7bsS+HJterSGWL4p2QsU4Q2Fpoik20LMGuYSjcCcX0pQnwALfZ+aJc4iS5B/oSeWfIS9giX54fL+yiAy+/Vagx+DzTMW50UtGojBYntTCtX0BzwHf58aDR/dn40us3SyD2x3R5+xEO0w5lKnWJpg8ybAqjJUTq17MHirulUX2kqCWckIk9/Cr6+TgeLXmoZucOJFqig3kL6QunM2/AfohPggWRWeb4+W81Kbh8EHjTrVKlOU6kqjfsJ/EOcQWvrO1Dgta34o59RqyDzir3M4ZkHUaNl5JZRyKgovxN1HLOv/4DPO/g1q2kDdswvDLJqXhApTTIXjZirfuY69x60tGxwopzNBQ+YhYCqkfL/3uQE/xs8DYAwQ4Mwyy2ebnCc9y2pkQWWKVGqOZKr/dsUeU5uIzJOmBfJMauDHkK/Q8+/HuiWI5lkQGcKmy3ZoXbWi4Ee58L0WYZ3rsmNYBHn0QsgowVuy5wGGFBDVUfjO5W782zjA9EoOvS4nZFa63h7nU5Ca2BIdbI0VPEFGBJk9pe5+DR79YcCOfONVs1zkNT7msDZcs2QupqCf7zaBmJ6za4HtL5trYyNFp6riLxlkJ/jtuApHFijDffyRPhmoNAgQO8uV6qE15xE2E1PEg0f1eD91aof1TAFxjaczsitdiAtW3YTrvO8+TQQ/+ENSgGzA4CNwrkYdXPhRNXu66hxWG5BKERr8Yk7vRWM439bjb23XvYdt7ymiDzKA7jkJ5BMVVZzWr
- Openpgp: preference=signencrypt
On 9/10/18 9:35 PM, Abhishek Anand wrote:
> Is the following provable:
> Lemma fextb: forall (f g: bool -> bool) (p: forall b, f b = g b), f =g.
>
> For CoC, the following paper (Definition 2) gives a countermodel:
> Boulier, Simon, Pierre-Marie Pédrot, and Nicolas Tabareau. “The Next 700
> Syntactical Models of Type Theory.” In CPP. Paris, 2017.
> https://www.pédrot.fr/articles/cpp2017.pdf
> <https://www.xn--pdrot-bsa.fr/articles/cpp2017.pdf>.
>
> Can this countermodel scale up to Coq?
Define precisely "Coq".
(Protip: nobody knows, and it is a moving target anyways.)
The only limitation of this model is that it doesn't satisfy
eta-expansion, but it can pretty much accomodate any other feature of Coq.
If you want to negate funext and still have eta, you can have a look at
the exceptional model: https://hal.inria.fr/hal-01840643. That one has
another limitation, namely that there is no singleton elimination from
Prop to Type (you can only eliminate empty types).
PMP
Attachment:
signature.asc
Description: OpenPGP digital signature
- [Coq-Club] function extensionality with finite domains, Abhishek Anand, 09/10/2018
- Re: [Coq-Club] function extensionality with finite domains, Pierre-Marie Pédrot, 09/11/2018
Archive powered by MHonArc 2.6.18.