coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Burak Ekici <ekcburak AT hotmail.com>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] on coinductive extensionality
- Date: Wed, 13 Mar 2024 12:15:11 +0000
- Arc-authentication-results: i=1; mx.microsoft.com 1; spf=none; dmarc=none; dkim=none; arc=none
- Arc-message-signature: i=1; a=rsa-sha256; c=relaxed/relaxed; d=microsoft.com; s=arcselector9901; h=From:Date:Subject:Message-ID:Content-Type:MIME-Version:X-MS-Exchange-AntiSpam-MessageData-ChunkCount:X-MS-Exchange-AntiSpam-MessageData-0:X-MS-Exchange-AntiSpam-MessageData-1; bh=NsP/+jQIDKEnkunjO0KIH3KOKiibkdWOjapG5t9pbF0=; b=TNe9sMZ6YOnCEA0ND1vJoMDmf8rPLGUZ1vjDzK2rPYzZlvUd8vpXjWCkXm9kZYeR9kuMa+Axr+xgmomqk7dwOp1S4Bt6tuSiTgkj/aaZjQvXs8J2L9t5Cs9zRPEEgeAvzQQm/ZWjmmLLYlH0L/p3lsb8BDnoydqhIGqDKL1tdC5Yy561Kod7PEd0q3pe5e8V7RMVnj/VmtCDT8DO96satErrdZgEH9MkFirjYlLwW4fXCUExYhaFSUoXKYgrTmTgNPMOFxkDJoUSN2fb/jJ9g7tcjBvwD0beSeykwuyvoYnJ9xnpMEST3XtPDvJ0KLEV1kYEybVZE3p7fxgrCzu9HQ==
- Arc-seal: i=1; a=rsa-sha256; s=arcselector9901; d=microsoft.com; cv=none; b=dCe0ouLisc4qhxagATomxzryaerpTPeRFB+MWWIZjsxLjcdSlNdEffM12eTT2vXLyn1TTqGsLoUld70uxKOycUurRNiJqWHiD0tMjvg7Q7iCK3EXauTC9NoZFB94LSpX/C9urmvqHcihi9mTX+Juc/3Sie1tbIw0BKqcaJXRh6FTby3mXCg2MidBM/hrdURX1wJJpSdva0JtF/7wsGArYS+Nb4yw7K3fMbchAn49h3l4y6Jk2Ufrzhf1vhjyU21nIuD4/JgEu/BoOsmoII8IlWamJe6Qmoxf7bQRUJQ6tJsQKEcxAgX9xjyoYysAgW2DjNcpmkdNHkvXqr8Pay0gFg==
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=ekcburak AT hotmail.com; spf=Pass smtp.mailfrom=ekcburak AT hotmail.com; spf=Pass smtp.helo=postmaster AT EUR04-DB3-obe.outbound.protection.outlook.com
- Ironport-data: A9a23:hV1So6JIqFHWc3VoFE+Ryp4lxSXFcZb7ZxGr2PjKsXjdYENS0TUAz GEYWTiPOfmJYGb0KN5xaorl9k4P6JGByYRiTAod+CA2RRqmi+KVXIXDdh+Y0wC6d5CYEho/t 63yTvGacajYm1eF/k/F3oDJ9CU6j+fSLlbFILasEjhrQgN5QzsWhxtmmuoo6qZlmtHR7zml4 LsemOWBfgf6s9JIGjhMsf7b80o05K6aVA4w5zTSW9gb5DcyqFFOVPrzFYnpR1PkT49dGPKNR uqr5NlVKUuEl/uFIorNfofTKiXmcJaKVeS9oiY+t5yZv/R3jndaPpDXmxYrQRw/Zz2hx7idw TjW3HC6YV9B0qbkwIzxX/TEes3X0GIvFLLveBCCXcKvI0LuamrQ+vpgKRENEao0/f8pJmdh9 /4+AWVYBvyDr7reLLOTZ9RW3phmAOOweYQVtzdn0C3TCusgTdbbWaLW6NRE3TA2wMdTAfLZY MlfYj1qBPjCS0EXfAZNTs1i2rr07pX8W2UwRFa9qKk86XXJxQ9Z0L/xNdPUfpqBQsA9ckOw9 jieozmpXE5y2Nq31wrG1Wuzitb2zC7cer43ToO71aZhuQjGroAUIEZNDwfkyRWjsWa1XMsaI EgJ8AI1vK0q/QqqSMP8Vlu2uha5UgU0XtNRF6g24lqA17CMvwGdBW5eFmMdLts7qMUxWDomk EeTmM/kDiBut7vTTm+B8rCTrnW5Pi19wXI+iTEsVBo52tbthdEIojXjSc89N6iajN/TMGSlq 9yVlxQWi7IWhM8N8qy0+1Hbnj6hzqQlqCZlt207uUr1v2tEiJ6ZWmC+1bTMxddtRLt1o3GEt XkA3sSUt+0TF8nRkyiORr9VQe3v4OuZOjrBh1IpB4Mm6zmm53+ke8ZX/S16I0BqdM0DfFcFg XM/WysOv/e/31PzN8ebhr5d7ex2kMAM8vy5CJjpgiJmOMQZSeN+1HgGibSs927silMwtqo0J I2Wd82hZV5DVv0/lmTmHblGj+Nwrszb+Y81bcGjp/hA+evGDEN5tZ9ebgrQBgzExP/a/1mOo 44PXyd040QDDbOiCsUozWLjBQtRdyRkbXwHg8lWffSEOQ1oBCkqDOXJqY7NiKQ095m5Ytzgp ynnMmcBkAqXrSSedW2iNCo/AJuxBs0XhSxgYkQR0aOAgSJLjXCHsP5DJvPavNAPqIRe8BKDZ 6BcJJzbWqkXEWivFvZ0RcCVkbGOvS+D3WqmVxdJqhBmF3K5b1WRpoW2TRil7yQUECu8uO03p rDqhEuRQoMOS04mRIzaYe6mhQH593UMuvNAb22RKPlqeWLo7NdLLQ71haQJOM0iE0jI6Qab8 Ae0Oi0mg9fxjbU7y/T3oJyVjpyIFrJ+F3VKHmOA4reRMzLbz1WZwoRBcbipfg7jaWHdoIGfX 85w3qjiAfg6gVwRjdJNFucyx6cH+tDPhaFW4TpmEFrPcV6qV61sEkOd15MerIlI4KFTgiqte 0e14tIBE664CMDkN18wJQQeceWI088PqATS9fgYJEbb5jd92aiuCGF+HkCrozNMCql2K6Ynz vURg9EX4AmBlRYaCNaKoSRK/WCqLHZbcaEYmrwFIY3smCw540pjZMHCNyrI/52/UdVAHU00K DuyhqCZpbB9xFLHQkUjB0r2wutRqpQfii9klGZYCQyypePEofsr0Dl60zc9FF1Vxyoa9dNDA DFgMkktKJie+zttutN4YFmtPAN8HzycxF36zgoYtW/eTnTwbFf3Ek8GBb+v8nwaokVmRRoK2 JGDyW3gbyTmQ9Gp4As2RnxeiqLCSf5fy1T8vf6JTuW/Mbs0Wz7HupOVRHEprkLnCPwhhUecq uhN+v1xWJLBNiURgvMaDomE2ZtJSBm7O3FzG6B93aIWHFPzfCO59iiOJnuQJOJMBa3u2m2pB /N+IvlgU0yF6x+PiTQAFIgwLKRRjtdwwPYjIZbvfXUntZmbpRpX6KPgzDD03jIXco8/gPQDJ ZP0XBPcN36bml9/uXLH9etAMUqGOeg0XhX2hr2Jwb9YBqA4kb9edG8p2eGJpFSTCgxs+iyUs C7lZ6P7y+9Dy5xmr7DzE5dsVhmFFtfuaNumqAyDkcxCTdfqA/f8swk4rlrGPQMPGZAzX99xt 6qGsf+p/UfjkYs1bVvkmMi6J/EU3fmxYetZCdKoDX94mSDZZtTgzSFe8E+FKLtIsuhn2O+Ze yWCZvGNKOElA+Vm+CUNagx1MQosNKDsX6Kx+QK/t6utDzYe4yzmLfSm13jjNltHRxAMILn7L BH+gNe1x9VitI8XLgQ1N/JnJJ5ZIVHYRqotcePqhwSYFmWFhlCjuKPosBgdtRXnL2aiK9nrx 4DnSjzVVgWAiIuRwP5364VN7wAqVlBjiuwOT2ch0t9RiRXhKUUZLO4YYK40OrsNngPcjJjHN SzwNk08AiDAXBNBQxX2wPLneiy9XuUuGNPIFgYFznOuSRWdJd2/WeN61yJa/X1JVCPpz7inJ fEg63TABEWN7a8zd9kDxM6QoLlB/ezb9EIq6Eqmss3VAjQiO5so+kFlPjJwUX3gL5mQumTNf GQ7fDURCgXzA0v8Ct1pdHNpCQkU9mGnhSkhaSCUhs3TocOHxelH0+fyIPz3zqZFVskROboSX jnicgNhOYxNNqA75cPFeu7FgJOYzdqmI/LicOrPb1ZXmKu9rGM6I8kFgCwDCtk4/xJSGE/ck T/q5GUiAEOCKwZa37j+JcAh5cdqSnxVZ93WpFeXmNMEuUVRIxvll9yCzAXnLJjxr+7ouEAwr PI6chOKu1PP3Nf7jWAWixnYz2BrxekREmXBWyEsCJj1l39AjYOb+K9JiykH6j6azJGIKki4u kpcPxXRNb9Lhh+y4j0=
- Ironport-hdrordr: A9a23:228kAKltzeJnygo+r9FuPleBFKLpDfMBimdD5ihNYBxZY6Wkfp +V8cjzhCWftN9OYhodcKO7Scy9qBLnlKKdhLN8AV7MZniEhILFFvAH0WKA+UycJ8SdzI5gPM 5bGsAQZuEYZWIK9voSizPIderIruP3l5xAyd2urUuEGmpRGtldxjY8LjzePlx9RQFAC5Z8PJ 2A5vBfrz7lXXgMdMy0ClQMQuCG/rTw5efbSC9DIyRixBiFjDuu5rK/Ox+E3i0GWzcK5bs562 DKnyHw+63mmfCmzR330XPV8v1t6anc4+oGIPbJptkeKz3qhArtTp9mQae+sDc8p/zqwEo2kf HXyi1Qdvhb2jf0RCWYsBHt0w7v3HIF8Hn502KVhnPlvIjQWC86McxcnohUGyGpnXbIhOsMm5 6j4ljp/aa/TCmw6xgV3uK4Hy2D2yKP0DcfeYd5tQ0ibWJRUs4ckWUlxjIlLH4xJlOE1GkZKp gRMCj93ocnTbrIVQGrgoEArebcJEjbWC32NnTrZaauokFroEw=
- Ironport-phdr: A9a23:w0F+9RLQ89hxo8fMYtmcuFVuWUAX0o4c3iYr45Yqw4hDbr6kt8y7e hCFtLMy0RSSAc2bs6sC17CG9fi4GCQp2tWojjMrSN92a1c9k8IYnggtUoauKHbQC7rUVRE8B 9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUhrwOhBoKevrB4Xck9q41/yo+53Ufg5EmCexbal9I RmoqQjdrMsbjIttJqs/xRbCv39Ed/hLyW9yKl+fgRXx6t2s8JJ/9ihbpu4s+dNHXajmcKs0S qBVAi4hP24p+sPgqAPNTRGI5nsSU2UWlgRHDg3Y5xzkXZn/rzX3uPNl1CaVIcP5Q7Y0WS+/7 6hwUx/nlD0HNz8i/27JjMF7kb9Wrwigpxx7xI7UfZ2VOf9jda7TYd8WWWxMVdtXWidcAI2zc pEPAvIdMuhboYfyqVsAowWjCwajH+7g0CNEimPs0KEmzegsEwfL1xEgEdIUt3TUqc34OboPU eCv1qbIzijIYfxV2Tf89IfIcw0qrPaSUrJzbcXe0lQvFxnfgVWTsoHlPzSV1vgIs2eB7upgU fijhHIgqwF0uzWiwNonhYbViIwP0F/E6Tl5z5gvJd2+UEN1b9CqHZlMuiyVOYV6XsIvTmJot Ss5y7AIt5C1cigKxZkkyBPSb/+KfoqV7h//SOufLjR1iXxqdb+ihRu88Umtx+vhXce3yFZHt iVInsXWun0JyRDf8MqKR/Rn8kqh1juDzx7f5+BYLU06kKfXNoItzaQxm5cWrEjPAir7lUv0g aCMc0gp//Wk5urhb777uJKcM5J0ihriMqswgMyxHOU4MwkQUGWD5eix0qDo81fjT7VQlPI2l 7HUsJDEKsQfoa60GwBb3Yg/5RqjADqqydoWkGQJIV5cfxKIlJbmN0vJIPDlEfewmFOskCptx //bJLHhGo/NLn/fkLj/Ybl9909cyA01zdxF4JJUF60BIPb0Wk/2t9zUFAM2Mwuxw+r/CdV90 J0RWX6XD6KWLK/eq1uF6vw1L+SOa4IZojbwJvc96/7rl3A5mFsdfaez3ZsQbXC1BuppI0aFb nX3n9cBC30FvgklQezqj12CTTtTaGyzX6I4/D00FIWmDYLbSoCrm7OOxD27EYFOZmBaFlCMF m/le5icV/cWdC2SOtNhkiADVbW5V4Ah0giuuBbmxLpjM+rb4TYVtYnj1dhw/+3cjws+9T1yD 8SH0mGCVXt4nm0SR2x+4Kcqqktkj1yHzKJQgvpCFNUV6ekafB09MMv20vZzCJjfWQPKf5/dR VWtSMi8CDIZTtUtxtYPZwB2HND03UOL5DajH7JAz+/DP5cz6K+JhxAZRu54wnfCj+w6ikU+B 9BILSugj7J+8A7aA8jIlV+YnuCkb/dUxzbDoUGEy2fGp0RESEhoS6yQUHMUbFbMpNfR5kTeS ravDfIsNQ4SgdWaJP5yY8byxU5DWO+lPd3fZ2yrnGLlCBWDzK6WZYnCe2IB2SzcDA4PlAVAt W2eO10GDzy663nbECQoFV/rZBb09vJirXqgUkIu5yy3VRU9kpafoVsSj/HaTO4P1LUZvitns y9zAFu2w9PRDZyHuhZle6JfJ9g65T+rzEr/sApwdtylJqFm3RsFdhhv+ljpz1NxA5lBls4jq DUryhBzIOSWygEJcTTQxp32NrDNTwu6tBmyd67b3E3f29eK6+8O7vo/sVDqoACuEAIr7Xxm1 9Bf13bU6I/NCUIeVpf4U0B/8BYfxfmSbyo27Z7O3H5EMa6otzbD35QiA+5kghesctFDMb+VQ RfoGp5SDMyvJeo23lmxO05cerEIsvFoeZ76JJ7kkOaxMe1tnSyrlzFC6YF5iQeX8jZkD/XPx 9ADyu2Z2Q2OU3H9ik2gu4b5g9MhB3laE2yhxCzjHIMUaLd1eNNBBGSlKdCtz9ZWh5nxXndZ8 BioAFZMi6rLMVKCKkfw2wFdzxFdrH+skzaixj9ckzY1q6Oe2GrFxOGoJ39lciZbAWJli1nrO 429idsXCVOpYwYenxyg/U/mxqJfqcyTNkHrSFxTN2jzJmBmCe6rs6aaJtVI8NUuuDlWV+K1Z RabTKT8ql0UyXGrE2xbzTE9Pzak3/ex1xF5g2iANn9whHreZcR5xBOZ79vZDfJcxTsJQiBkh CKfWgD6boPvoonSysuLu/v2T2+7U5xPbSTnqOHI/DC242FnG1z3nvy+nMHmDRlv1Cb609dwU iCb5B34Y4Tty+G7Kbc7Jg85Xhmjt4wnRtIb8MN4npwb1HkEi4/A+HMGlTy2KtBHwefla2JLQ zcXwtnT6Qyj2Ut5L3vPyZiqMxfVisZnedS+ZXsbnywn6MUfQqqX57ZZhyJ2ilq/sQfYYPw7l TAYg6hLijZSk6QStQwhwz/ISL0RFkNFJyXvvxSP89W3raERb2GqO+vVtgI2jZWqC7eMpRtZU XDyd8I5HCN+2c54NUrFzHz57oy3MMmVd98YsQeY1gvRl+UAYoxkjeIE3GA0XAC19W1g0eMwi gZimI23rJTSYXs457q3W1ZZLmGnOplVo2m2y/4YxoHPgMiuBskzQ21XGse3C6ruSHVL6pGFf 06PCGFu9i/dSOCZRUnHrx4453PXT8Lyby3ReCZfl40kHF7HfwRemFxGBW1m2MJmUFnylIq5N x0ig1JZrl/g9kkVkr4ua0a5DTqZ/EDyNn81UMTNdUIKqF0doRqOd5HGqbgvVyBAoM/7pVTUe DXCPlZGUTlRCB7DWwCGXPHm5MGeobKRXrPsdqKXM7vS8bcMBbDUlNquytU0pT/Ub5fWZyAwA aFjgRgTBSghSZaexm1qKWRfljqTPZSS/E7uo3Qu/M7jqK+5U1q3vdndTOYLedR3pULsiP/aZ bfJ3XR3dW4DhJ1UnSeamv9ChhZXgiVqPVFBCJw4vDXWBOLVk65TVFsAbj9rcdBP9+Q61xVMP sjSjpX00KR5h7g7EQUNWVvkk8CvLcsERgP1fEvAH1qOPa+aKCfj7vzNOf/5ZZcLyeJeulu3p CqRFFLlMnKbjT71WhuzMOZKyiaGIBhZv4L7eRFobAqrBN7rcRy0NtZrgCZ+neVy1ymMajJab GQ0elgFtrCK6CJEnvhzU3dM6HZoN6jMmiqU6fXZNodDsfZvBXcR9aoS63A7xr1JqSBcEaAt3 nqI6IEy5Qz6wYztgnJ9XRFDqyhGnteOtERmYuDC84VYHG3D5FQL5HmRDBIDo51kDMfusuZe0 Iuq9uq7JTFc/tbT5cZZCdLTLZfNPXkqOwfzET38DAwZSDeqMSfUgEkXw5TwvjWF64M3rJThg s9EUrhASFk8De8XEGxIIeZafNJbdGhhlrSWyskV+XC5sR/dAt1AuYzKXe6TBvOpLyuFib5DZ F0DxrayfuFxfsXrnkdlbFd9hoHDHUHdCMtMriNWZQgxuExR8XJ6Qz57ywf/Zwiq+nNWCe+sk 0t8lF5leep0vmSJgR9/Nh/QqSA3ikV0hdj1nWXbbmvqNKnpFYBOV3io7w5gaNWjBV4yNFD6n FQ4ZmucAesJ0P04Mzgs0VG529MHGOYAH/AeJkZInbfPIa1viAgUqz37lxYfua2ZVt060lNtK MHkrmoeiVhqNIdnfPWJdqQVlgAC1OXS7krKnqgw2FFMfU9VqTHLIXdathBQbet0YHb5tu10t 17YkmMaKjFVDqgk/qoxpBNlY7zSnWW9itshYgiwL7LNdarB4jqZzJfaTA9ojREDzxEdr+oxj J5rclLKBRomlOLDTk1QZ8SecVoHYZIKrCqBOnvU+aDExZY/V21cPs3Vd7fS8Yo+2QejFgtvG JkQ5MMcGJXqyFvfMcrsML8Cz1Mq+RjvI1KGSv9OfUDS+N/ii8G40Jp+3I0bLTYYUz0V2cqf5 rHLowYrhLyIW9JkOx8n
- Ironport-sdr: 65f198d2_22mVLD4VYyIMH+TYfWpuI37EbwA850iHMgQcVecoDHPhFMY 1+6CaFaj4qCb1r8YLRMCmFvtm6EtZqzbs2IHoxQ==
Dear all,
I have a pair of predicates — one inductively and the other coinductively defined as follows:
CoInductive ct {A: Type}: coseq A -> list A -> Prop :=
| co_nil : forall ys, ct conil ys
| co_incl: forall x xs ys, List.In x ys -> ct xs ys -> ct (cocons x xs) ys.
Inductive it {A: Type}: coseq A -> list A -> Prop :=
| ci_nil : forall ys, it conil ys
| ci_incl: forall x xs ys, List.In x ys -> it xs ys -> it (cocons x xs) ys.
Would assuming an axiom like
Axiom ext: forall {A: Type} xs ys, ct xs ys -> @it A xs ys.
introduce any unsoundness?
Thank you so much.
Best,
―
Burak
- [Coq-Club] on coinductive extensionality, Burak Ekici, 03/13/2024
- Re: [Coq-Club] on coinductive extensionality, Meven Lennon-Bertrand, 03/13/2024
- Re: [Coq-Club] on coinductive extensionality, Arthur Azevedo de Amorim, 03/13/2024
Archive powered by MHonArc 2.6.19+.