Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Why `ex2`?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Why `ex2`?


Chronological Thread 
  • From: Maximilian Wuttke <s8mawutt AT stud.uni-saarland.de>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] Why `ex2`?
  • Date: Sat, 18 Apr 2020 15:26:41 +0200
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=s8mawutt AT stud.uni-saarland.de; spf=Pass smtp.mailfrom=s8mawutt AT stud.uni-saarland.de; spf=None smtp.helo=postmaster AT triton.rz.uni-saarland.de
  • Autocrypt: addr=s8mawutt AT stud.uni-saarland.de; keydata= mQINBFWVkZsBEADmp2Mq5XZcOg38F91SMR5uF8cqC7LaODrnF+xh3TNKgbK301sPwcSKA4gr +TKV73e4VQoWihiWaYfPJYHsudXrp644dqYvWuxNWlkh4S2HIOmcopuTEd063TL5hRvhkg0V ZOMq000ucKo0yBsUux7+TdZdDAX3WP1whF7jY8OTe5xnEO3yv4xydAZhbT/gMO/IW6BVE2xO eElXEwC8Tnssar8cM0wZcnxgKXq4dhjDO6sSkeaf81a6FPlpy+VuCIHFYoFIAquX6T6V+Zbi UXJyDSUSUVVmechLA8vXmiRgOTyVMdTejXQb5niLGjb/Upvy9uSlO7eR0aSkCs3vqeXIppmS PDTKVwPso/PmJHEJnZLrbXKqqh589pbDAdYfJvP3Sg0fncL5bzxV0gdSqWH0t0e7c9AMiHs5 5bxEHBXuVtNs1srF52gT0KlE84R2UOmZ9Kst7P3XgJtIGzuS5uSHqFmtknh9tj+/G/Kg3qDz njxM6xTGExNPHQuskwbvYDqA6/5Hslqis6D6EpMPGhRuUhPuE5Eb+PsxpV26UccZt51FqIIc Mwv+3AUPbF7v7s7rAE1BkbmClUGuYUGfqfndGT4V6fLpQH5F9kRdxmIm9FcMURUDvX4CBKZz gmwIZ4jgZ2jZ1VTy+MWIXRpgJIt5aim4liycyDoPk+fyYfdmQwARAQABtB1zOG1hd3V0dEBz dHVkLnVuaS1zYWFybGFuZC5kZYkCUAQTAQgAOwIbAQULCQgHAgYVCgkICwIEFgIDAQIeAQIX gBYhBD64TDV8welurJxMM+1Xu2bbvfzeBQJd7qlVAhkBAAoJEO1Xu2bbvfze9NkP92DvzDUh VM5IzQC+aK2M7Yo2NE5j3ELhZH1m+RZsU1Ek5evoBVX71WfIrBDHb92c5AUBPy3uzG9Rno2Y x6eE59BFr0CpGZ52G+JWjVxL2voBV8zuvI720lqHONv3zONK9OvaI0nE0XxV56NktzW6X018 8h4woo1amXu8jBxJcSdrwiS//T6ZqzrHAv00JWwmhbg57uwgvu07PcHDUSB93j8hx7RxP3UG bnTE1/3QRdwq4YDa/TO7v+EqEO8RCAlRtTCXnLlgRpIWPEx4+g4w9EGaBdc94YRgkEFh2U1z QuJt/3797P2iTiR3LqIXfSxTZUy/znMcy6q5Jl6A3+dms2JQRVjeA0yppajmxLDlz6zjZj91 BKIIXQbo5A8UiKDHWEgxq7Atyg/Bloc3njvaZ0+bGIKyciDT2Noyd8SHD4H390O/cD8LVjBt H6k/1wUFkX3h24dEFXASjA3vZCsmR/FI9wok9fyfpE/iqVXkUpmX20FNWJl9f9eLNSDKx7N7 foJSzwPVSGFSNhEY5BAjUkJrHOyHZ8tAShBJovxnIGfD2OtTqKLAEWHvm7+CYXeR91DjalPp /6iRd/xvRw6yisS+Nqi8X9gEBaq8vJemCV0psbU30brVs7dqKqaOf+N0PyCp/FDlCvYaAhEe kFgo4TeEqMe92xM49tzenY6I2vq5Ag0EVZWRmwEQALwwnvtVw/zFec+MNKgBwKt1MIG6EMBK c+OTIYM2tN4jcWlaAbEcIZGkBSeoPJeTi4m3GQXhifGZK29VoDIUQjYYDWNtp6U8y0hLRnqS VY/YvcTDnK929n5rqMqO0wYf1fzhmPshIyD1jj96tqu0ppX7zE++VQ/VJgVIA8IGcNXUN21A /+rJKCJFAvBp+6u2gNaUDfnqvPfTGtkq7A/D40Lo6y0KVu20R3W76iFWl6FEQzOe28VBnOjU /NbyzAzVUSgYCSfkYxhDiKfJRJvQd+VKUCAa+BSNoEPvDMKakvhApWUOncnNUbfXiH04fYSV iu2NH2Ls3HLm+6xaAaf9eUIU75A02xXUa6m+AccJQzCEJySeYJFVhJLSgZEbGwDZVdrRALol gYiIrwOHTitC2PLRej8HeywQrn3PUGBwiYdOa19KTHZykbO0s0SHb6bvm3vgpAPPdZp+QWPO Xx3aZz6dw4D867lisGVKMcKBcX9QCekVL7CW6lvvevUP5tBBYCshMvSTaN0BymBBwYrz8UB4 RYJ4cUs5apd1mMfD5Vm8EZf1DT15Q+K9+HsRQr3y/+AtHm0gd0DpXGfBH4H+54vyB9Aj3DVb yPMeFYv9UhyKALEomprFM0tr0+SPh275xXlIxUvoC+3PlFM0swoLSmi2Tu9edjU6GuyL91w/ 9WTjABEBAAGJBD4EGAEIAAkFglWVkZsCmwICKQkQ7Ve7Ztu9/N7BXaAEGQEIAAYFAlWVkZsA CgkQIA5mg0qOKkAoDhAAnms7o654V2uZWBsiiR2oEykGs/sIzxYcKrOi2RnkL6RAwhJgBr+W VpjQ2IS9IQ5Bxy8GOWhzyit2XvFYTWxGamrmyXol7IynGcl2U3WpmSQEPJx/QeyQ5lWLYzjn 5bbdzNdY0mhUnRZ+ke2tcttmvLsUKn2J/8lSyqBF4i4Yaj4p4LQ8n/K/eW9lIY+J/gVGDcrl ZqOozXV9aClYDtgxL/c6/TPuDi0vgkhIaojwsSu38YmhmbYP03ntiLTrLbjnJXr0pYIlMRqU mNvPsphOR8cVGFnZ50dVoWHSSJhoIESpu8Qz1qwvA9uNTDhe/nnr092diP78FWo4SENiKjrX A2fOjk0YoZA1uSL0RbcRKAttPC88iBWUyBwYrhMBFKzJeDG+lvBID8gED205Jy7Mk8v7R9Nq HpjJXST1avVMF7TXCH8OK7rgI9ATGLqJ31WoYZkCSFkYKYRbyarZnVKxMsQ1zhpjoEfuQlWa q2NgwS2cijWmKAmFV4Qv3FA5zAoEdzB9HCbT2DafITEUqjf111+WjNcfJvtfQcO7hghhMwFt W9Or9KqVKpEDrakuuHUr6nVnBNYCliY80m/X5DXOZsKzehxfHht4t+CydGE2xRzIwzpos2Ze bhkjWmghGS7G1JHADgEk7zBKyVxJm/nwwNGk5MdY9sckx8XMiaA5lV2oDw/+K7mXo2qbEPng hGjN2bAqYbZd/Wdh5SUwa5YvnfqWcSY7G8OA5pexnIV/5RRIdcc+RtrxADmfTYGVIvSfAS4u wALIgEd5LYdYBIajxWLCyNghoQowLqZbIQQ4eOWd2xCF6srcTsIou2kJ97iiFtXgX3PthKn+ fhdFYWktEDabDhgYSdqJVvs+Sk3lO41aJu5MSIsqWq+G0ZGumTtO/yR9x5RzA/qKn56S6Da8 WjRF6iq/oyemifyC74HXmmi6gd8HCWD+eEXNWVAVL/FlfYhL420olMcBgP+cMGJTpmWK5jCy axHH4RFYg8AAdzn0/Lc/Xr47IZBntCaLy3V1LSKvDSZackKOreBmxQrd2Qn5/seLYFWWl/rP vqib6hmoE17SjBI2szi/t37JGXTl0ZkhSUp6FSC4YmoFrKJgxuX0q7CONZzdZ9G7mNOkUdg3 QAaN6/EZQceGC/Dvi28jB57Y50OoOAcyJnSkS95lPobHcGbBDDIQVvcEBwhSir/coGXHk8tq MXCdhxDo9Tq1cSvANeRYuJdrTdJM2FMll7QEtBcto0DNCNEecvZ+D/uqOU+InyJHpD4qDpQR 8bqNJ3Fmehd54LYiZK2G5/gRwF+8vnaeoy9fSs/CAw3icKPTcSSmy9bOk3I0fgAyb63xLF/s GHAOq5gkPg+9o79dHcbtD425Ag0EVZWRmwEQAKYFa3Y6d5D34YkaNBYvjU3mUlaS2uq7khoV xhnPiad496PzpxpF76rwpAbh7+V+aqxFDldmydjV3REPgJKk5hnhJ2ndltaoy0CtzFOjUV2K kzzvG2YXADSKCqvLrtVx3wfAxOVxjPOlFzG57mvZd3MUlxOGJPvNbFJJY98OzjQGeCukITMO 4mivublSlJy8hNkwbMgkAfBkuITNXllrLfTxch6wikunYlDrtI2X1/h6ygXn/m8dYWzDGv80 PyzVHWNMz7JS5UuD7PkkazkqLzH9HQ+xj2x7KOWIHs9BQp99OrZfUMcD54EfoM0JUG5kq0Xs 099Z4UEFA2Pl+8mnn7z7NNZ1JSN0xjUuxhMu5deIkKEj8XGwB+6OXYEhF3mdh5T29C4LHDpp 3fpa9LU+8Dlpq0HJlwBx5ngXOfAmZrKAJhiy8kT3AfNskiVWxgYga2Kk2ku8vV4DkMai7kzK 45t0/cDwdgugeck83x/7yR9XIrBwlt8N4bdJ3URbOtnuGuYjM5RTtqpadjVLLr+ZdhKPdM7q tPfnHotjRq+ban1TdA/zlCOW+s4g955kvafY29qnhx54y+DQJUwELAZCTA0fT/eHs0n6M/gI LepMleBR7STA+XqnI5aWlWn3Pp6nI8t3bz0T6sFEocD++YJNEr/J7yduvcNaI84j03iRMfPj ABEBAAGJAh8EGAEIAAkFglWVkZsCmwwACgkQ7Ve7Ztu9/N4GJA//f21oF6/XClyTnbsNSBKL vbtb9CjKx+9c6B6k1qHePSylFf+BsrKFMEdtyn40bfVnQqQ1GzNFFbzGiFkUlwM1BZMR0ogl 6ahtJL3M4Tf7RkV6FUhkov5HwYIXDjx9WdboLPPz4NQkomgcWyc0vAndtL1vYFizVLkxIdWo nnv11M4MoQybCjv9lm+UwmoqLkSvrWn3F6RMPwsc4HWDRHiBYNkCxYGlfVfQax1u3ENH7KfE nZAEEoxSBkaha1Tv/06wHjQ9w+7ZwueiB48MCQleDM4xP+Geom/VIhExdySrAtGZEP7DjCpc XTYL6491G1gDdStpzSU0odKKxp3xUgB7gFuegBsM4dXm02Q6tzr+oVLkCeTGWld3/DfyIVVi 3f2w+g+JEE8W71GxuIw4IwuxXr0sGo1gHnH8CD5ky0/dGYfW644oZ6DQRzDqp+7sJNGoSOmE bJ5k7IgkPlwb41jNEz1miq/AIleDjVgM6ZP1g4eVAWgjATFqfv9y/WR1t1BvrcogGKdVLfRr 6kDYwP2GzzCGz2KiVtlPaPv52UYPa9zX6IT5hEOq4GSAVo2IHwtukyG10l7sanq7J6s5CumN ukDzuJxJ+EgNYIxaEtdujUPJxlRQcFwqjbLEt2LQBJivwzRhRmQfQz5tt3c797Tsto875TRg vFHu+ezStimb9ew=
  • Ironport-phdr: 9a23:zSUa5RTV0oO9AK5cn5VKoIA8iNpsv+yvbD5Q0YIujvd0So/mwa6yZxGN2/xhgRfzUJnB7Loc0qyK6v2mAj1Lv8vJ8ChbNsAVC1ld0YRetjdjKfDGIHWzFOTtYS0+EZYKf35e1Fb/D3JoHt3jbUbZuHy44G1aMBz+MQ1oOra9QdaK3Iy42O+o5pLcfRhDiiajbrNuNhW2qhjautULjYd4Jas91xvErmFGdulSym9lJFKelAv46sus4ZJv6Stdt+8u+sJaTan2Y6E0RqFEATo7NGw4+MLkuR7fQAWV+3ASSH8Wkh1GAwjE6BH1QJL8uTbku+R+xSeXI9T4Qag7Vjq+4ahrTgToiDocOD4i7G7XkM1wg7lFrx+nuhdy3pTbYICRNPp5Y6PdYdYXTndPU8pNSyBMBJ63Yo0SBOQDIOlYtZHwqUUArRW+GAeiB+3hxTFHiXD0waI3yOshHR3c0QInA94DvnbZodPoP6kSS+C1y6zIwC3EYfxM1jb96Y3IchElofGNR71wd9faxkkyFwPZklWQqpLqNC6S2+QWsGWb6vBvVOyyi247twF8uSOvxtsxiobUnI4V11bE9SRgzIYuP9K3UlR7Ydq+H5tWqi6WLZZ5Td07TmxupS00yaUGtIamcCUEx5kr3RrSZv2df4WK+B7vSuacLS9liH9rd7+znRK//Em6xuHhUsS50UxGojRLn9TPsH0Gygbd5dKdSvRn+0eswTaP2B7X6uFDOU00ibDbK589wr43kJofq17DHy7slEXriq+Wd1wo+vOy5Ov9eLXmooWTN4lphQ3kL6shhNSzAeU+MgcQQ2iW4fmw2bPs8EHjRLhHj+c6n6vDvJzEJckXvqu5DBVU0oYn5Ra/FTCm0NEAkHkcL19FfQiIjob0O1HSPPD1Fuy/g0ixkDh23fzGI7vhApTUInjYirjuZ6x960pGxwo10N9T/Y9bBa8ZLPLpRkDxrMDYDgM+MwGs3+nnD8x92poCVmKLH6+WK7jfsUSI5+IqO+mDfpUZuDf7K/g/5v7hl2U1mVEHffrh4ZxCY3ehW/9iPk+xYHz2g95HH31ZkBA5SbnPgU2DVD9XZn+0F50h+i04BcryFtfGT5+wnKCpxzumEttLYGEDEVmFC3PhcYnCV/paO3HaGdNojjFRDevpcIQmzxz77FanmYoiFfLd/2gjjbym1NVx4LeMxw0o9CBzCYKHwSeQSWAxhWoBXTs/2qw5rUEvkg7Sg5g9uORREJlo390MVw47MZDGyOkgUYLpRh/NOMqPSRO9S9y8BTg3QpQ9zo1XOhovK5CZlhnGmhGSLfoNjbXRXs4v7r/QmWX3JoNmwn/c0KAngx8qT5kXOA==

Hi all,

On 17/04/2020 20:57, Christian Doczkal wrote:
> I guess the main difference is that is saves a "destruct" whenever
> eliminating an exisist2-hypothesis and a "split" whenever proving one.

This looks like a valid point for `ex2`! Indeed, I sometimes find those
long 'destruct chains' a bit annoying, e.g:


pose proof my_lemma _ H as (x&L1&L2&L3).


(Of course, I know that you can write an ltac that does this destructing
for you, and I sometimes use this kind of ltac.)

Having n-ary conjunctions is also a nice alternative.

* * * *

I had a quick look into the git history of Coq. It was first committed
quite a while ago, in December 1997, just after the redesign of Coq's
kernel by Jean-Christophe Filliâtre. [1] However, I think it's likely
that `ex2` is even much older, predating the old SVN repo.


[1]: Commit 2b62054dcccae08fdb5b61145e4b84d746e6faf1 (imported from SVN)

Attachment: signature.asc
Description: OpenPGP digital signature




Archive powered by MHonArc 2.6.18.

Top of Page