coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
- To: coq-club <coq-club AT inria.fr>
- Subject: [Coq-Club] function extensionality with finite domains
- Date: Mon, 10 Sep 2018 15:35:01 -0400
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-yw1-f53.google.com
- Ironport-phdr: 9a23:6filWRwZgqBI/bHXCy+O+j09IxM/srCxBDY+r6Qd2+4XIJqq85mqBkHD//Il1AaPAd2Eraocw8Pt8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94HRbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeuBWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbOSxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDwULs6Wymt771zRRDniCkJOT03/nzJhMNsl69Uug6tqgZlzoLIfI2YNvxzdb7dc9MAQmpBW95cWjBaDYO8bosPFOoBMvhbr4Lgu1YOqwGxBQ+xC+jyzTJHnGT53a070+Q6EQHJwg8gE8gUv3TSttr1MrodXfq0zKnJ0TXDYOhb2Tj46IfScxAhpeuAUq53ccrU0EQiER7OgFuXqYzgJTyV1+INvnCU7upmTO6jknYnpBxrojio2scgk5LGhpkPxVze+yV52p45KsG/SE5hZ96rDp9QtyWAO4RoX8wiXnlktzsgyr0BpZ63ZiYKyI4hyhXCaPKHa5CF7gz/WOuVOzt1h3JodKiiixuz7ESs0O3xW8ey3V1XtCRKiMPMuWoI1xHL6siIVP99/kC51DaKzQ/T6+VELVk0lKvVNpIt27Awm5odvEjZES/2n0L2jKCSdko64OSn9+PnYrD+qp+dMY97lB3+P7wwlsCjBek0KAsDUmiB9eih1bDv4Ff1TbVEg/Eul6nWqpHaJcAVpq6jBA9V154u5AykADem0dQYhnkHI0xGeB6dlYfpPUvBIPblAvulglSskStrx//dM73uB5XCNHnDkLP7cblh7E5czRI/zcpD6JJMFrEBPPXzV1ftu9zfFx81KhC7w+L6CNpmzY4eQmKOAqqBMKzIq1OI5+QvI/ONZIAPojr9JeIltLbSiioynkZYdq2019NDY3ehW/9iPk+xYHz2g95HH31c7SQkS+m/oVeCUCVTanX6dqQ14D1zXIusDYbYRo2uxrWH1SG3WJxXem9uBVWFEHOufIKBDaRfIBmOK9Nsx2RXHYOqTJUsgEn35V3KjoF/J++RwRU28Jfq1dx7/erWzEhg+jl9DsDb2GaIHTgtwjE4AgQu1aU6mnRTj0+Z2PEh0fNdHN1XofhOV1VibMOO/6lBE9n3Hzn5UJKJRVKhGIj0BDgwSpcg3IZLbRsmXdqliR/H0myhBLpHz7E=
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.
Can this countermodel scale up to Coq?
- [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.