Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] exact tactic vs Definition

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] exact tactic vs Definition


Chronological Thread 
  • From: Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] exact tactic vs Definition
  • Date: Wed, 28 Dec 2022 11:58:01 +0100
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=gaetan.gilbert AT skyskimmer.net; spf=Pass smtp.mailfrom=gaetan.gilbert AT skyskimmer.net; spf=None smtp.helo=postmaster AT relay10.mail.gandi.net
  • Ironport-data: A9a23:y7a5ha/s7qAD8zyVbEU4DrUDQHqTJUtcMsCJ2f8bNWPcYEJGY0x3n DNMWGmDb6qDa2v3fdwkYN62oEpUuMSDyddmHQY/+XxEQiMRo6IpJ/zJdxaqZ3v6wu7rFR88s Z1GMrEsCOhuExcwcz/0auCJQUFUjP3OHPylYAL9EngZbRd+Tys8gg5Ulec8g4p56fC0GArlV ena+qUzA3f4nW8qWo4ow/jb8kk25q6i4GpwUmEWPJingneOzxH5M7pEfcldH1OgKqFIE+izQ fr0zb3R1gs1KD9wYj8Nuu+TnnwiGtY+DyDW4pZlc/TKbix5m8AH+v1T2Mzwxqtgo27hc9hZk L2hvHErIOsjFvWkdO81C3G0H8ziVEHvFXCuzXWX6KSuI0P6n3TE/u5sImcyDLck0cEwAmIX5 OIVEAELYUXW7w626OrTpuhEnMknJdiyZMUas3Bkiz7QC/onB5bOX80m5/cChWh22ZgIRKmOI ZBCMVKDbzyYC/FLElgeBY43mqGnh331fidEgEmWtLE04m3WwRY31rXxWDbQUozXH58PxxvHz o7A12vYDk4oZeS+8xaM92OugvPNzQDpeKtHQdVU8dYw0QXMmjFLYPEMbnOwpuD8gUqjUfpEO kkM82wvq7Iz/QqlVLHAswaQunOAtw9FA5xVGuw+rg6EzKbVpQCUGgDoUwKtdvQbr80YYzgb7 GOiuJTqBmV+rrCteHSSo+L8QSyJBQAZKmoLZCkhRAQD4sX+rIxbsv4pZosyeEJSpoClcQwc0 wxmvwBi1+VO3ZRjO7GTpwuc023ESo3hF1Ztvm3qsnSZAhRRSrTNWmBFwULW6f9Rdd7fS1CAu D4Lks6S7aYIAI3leM2xrAclQ+3BCxWtamG0bbtT838Jq2vFF5mLId443d2GDB01WvvogBewC KMphStf5YVIIFyhZrJtboS6BqwClPa/T427C6CPMoceM/CdkTNrGgkwPSZ8OEizyCARfV0XY v93jO7wVCdKVcyLMhLoF7Z1PUAXKtAWnzKLGsyml3xLIJKRbXiZSP8eOUDmUwzKxP3snekhy P4Gb5Hi40wHDoXWO3CLmaZOcwxiBSVlVPje9ZYLHsbdeVAOMD96VJfsLUYJINENc1J9zbuTo RlQmyZwlDLCuJEwAV7TNi0+MuqzAsYXQLBSFXVEAGtEEkMLOe6HhJrzvbNuFVX+3LwykaxHX LMedt+eA/9CbD3C9n5PJdP+tYFuPlDjzw6HIyPvMnB1co9CVj753IbuXjLu0y0SUQuxl881+ IO72i3hHJEsegVFDeTtUsyJ8W+fh3YmtdhJbxP6GeULIETI26p2GhP1lc4ycp0tKw2c5z601 DS2IBY/pMvfqtQx4tCTgbyOkLm4N+4jGkZxPnL66IyuPnLw5VuTwo5nUceJcwvCVWjyxr6QW OVNw9z4M9wFhFxvsbcgI410zKk72cTjl4VawitgAn/PSVahUZFkHVWrwuhNsfdr6oJCmA7rR H+KxMZWCY+JNOzhDlQVAggvNcaH9PMMnwjt/eYHG1r76AB37Yi4fx1rZTfUsxNkLZxxLI8B6 sUispRP6wWA1zwbAuzfhSVQr2mxPngMVps8ja4jAajptFsP6kpDapniGCPJ8MmxS9FTAHILf B6QpoT/3op5+GSTXUY3J3b32chlua8vozFPlV8LGESIkIHKh9gxxxxgzg40RQV0kDRB9fh+C k5xPnIsOZe+3ipigfYbfmGzGjNuAA+S1VzxxmAoykzYbRiMfU7cIFItPd2i+BgizFtdWTxA7 ZekyGrBehT7TvHbhycddxZslK3+cIZX6AbHpvGCI+2EOJsLORzena6kYDszmSvNWM8eqhXOm rh3wbxWd6b+CC83pp87Aam80ZA7akiNBE5GcMFb0JI5J0PuUxDs5mHWMGG0QN1HGNLS+0zhC 8BOGNNGZy7j6Amw9AIkFYw+CJ4qus5x/9cTWKLZFUhfuZulkzdZmpbx9C//uWwVf+tTgfsNc oP/Sx/SE0i7p2dlpGvWncwVZku6eYYlYSP/7sCU8cIINYMxj/FsfH0fzZ+x5nWcDxR6zUi6o THsZLLcytI66IVznrnDFrdIKBW0JOjSCsWJ0lGXmPZfYezfNfzhs1sulWDmGABNL549as9Sh 53UlPLWhWTr5K0XVULdkLm/T5h53924BrdrA5imPUtkkjunc+6yxRk6okSTC4FDyfFZ7emZH zqIUtO6L4Mpao0M1U9uSnZsFjgGAP7KdYbmnyS2qsqMBjU70QDqKNCG92fjXVpEdx0naoHPN Qvph8mAvtxojpxAJBshNcFUB5VVJFzCW6x/eeOo5HPcRiOtj0iZs7TvqQs45HuZQjOYGcL9+ tTeSgK4aB22v7rSwcpEt5Bp+CcaF2t5nfJ6a3d1FwSaUNxmJDVuwSUh3ZQ65lV8iCH23YChP HfIZWomTyr0WzhFNxPx/LwPm+tZ6vMmYr/Eyv4Bpit4qBtawKubA6p69SZl5npsPD3u0IlL7 PkAr2boMEHZLo5BHI4uCz/SvQuj7ujZ12kL+EX4nta0BRsCaVnPOLqNAyIVPRH6/wrxeIkn6 IT7qa2ogK12dKIpLftdRg==
  • Ironport-hdrordr: A9a23:IQRMmqod/EaPrGpxQXBU2oIaV5omeYIsimQD101hICG9Afbo9P xG+85rsiMc6QxhPE3I9ursBEDtewK/yXcx2/h1AV7AZmXbUQmTRr2KhLGKq1bd8m/FltK1vp 0PT0ERMrzN5BRB4vrH3A==
  • Ironport-phdr: A9a23:Sr+bkx/Ac8QUof9uWd62ngc9DxPPW53KNwIYoqAql6hJOvz6uci4Y QqBv7431RfgZsby1bFts6LuqafuWGgNs96qkUspV9hybSIDktgchAc6AcSIWgXRJf/uaDEmT owZDAc2t360PlJIF8ngelbcvmO97SIIGhX4KAF5Ovn5FpTdgsip1+2+4ZzebxtHiDajfL95M Qm7oxjWusQKjoRuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2Q rxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v6 bpgRh31hycdLzM382/ZhcN+g6xGvhyhqRxxzIzIb4+aL/d+YqDQcMkGSWZdUMtcVSpMCZ68Y YsVCOoBOP5VoYjnqFwSsRuxHw+sD/7uxD9Jgn/5xrM10/49EQrb2wEgEMgBv2rIrNrvMqceS ++1zKjMzTrYcfxWwyv95ZPTchAiofCMRrFwccvUyUkqCQzFlE+cqYr7MDOJz+kAtXWQ4OV8W +y1kWEntx1xrSa1xscqkoTEmIwYxF/H+Chnzos4JNO2RVJlbdK4DZdeuCWXOYV4TM4hXm1mt iI3x6EbtJC0YSUG1IkryhHfZfGIcoWE/gzvWeCMKjl2g3Jlfaiwhxe08UW4xe38V9W00FZXr iVeiNXDqncN1xnL5siGTPt95Eah1iyV2wDd8OFJJ10/m6nDK5M53LI8i5gevV7BEyPqgkn6k a2be0Y+9uS25enrfrPrrYKGOYBukAHxKKEul9S/AesmNggOWHCW+f6i273n50L4QKhGguEsn qncqp/aJMAbqrS2AwBP1IYs9he/Ay2g0NsGgXkLNFNFeBSZgIj1I1zCPu30APWlj1mujDtn3 e3KM7/iD5nXMHTOnqvtca5460FGyQozyd5f54hTCrEEOP/zVVX+u8LEDhAjNQy42ennCNR51 owFR22PGLOZPbjJsV+L5uMvOOqMZI4QuDb4Nfcl/eTijXknll8BZaWp24AYZ2iiHvt6O0WZf WbsgtAZHGsXpgY+VvDliEWeUT5PYHa/R74z5jYiCI6/EYjDQp2tj6ea0SegHpxWY3hGBUqWH XfpcYWEQfYMZziILs9viDxXHYSmHoQmzFSlsBLw47thNOvdvCMC5rz5090gyORQiRg0vRN1C 86QyX3FG259k38BQXk53aR1rFZh4kyAwLN7gvldGMYV4f5VBFRpfaXAxvB3XoihEjnKec2EH Q7OqrSOBDgwSoh02NoSewNnHN7kiBnf3i2sCrtTlrqRBZVy/LiPl2PpKZNbzHDLnLIkk0FgW tFGYGKvi7J28U7cBorDnl+Fv72pZL8f3SvI+X3Fy2eS7wlDSAAlaazeRjgEY1fO69Hw50fMV birXLsuPxdIz4iNK69AZ8f1pU5FVezgOdHbbnj3nWqsVl6T3r3ZSo3sdi0G2TnFTkgJlwdG5 XGdKQ03HTusuUrEAThnBAu3JUbl8O04p3q9Qk5yyQyWB6F4/5yy/BNdxfmVSvdJm6kBpD9ks TJ/WlC0w9PRDdOE4QtnZqRVJ90nsh9B0irCugpxM4bFTegqj0MCcwlxo0Ll1glmQoRGn88wq Xo2zQ10YauG2VJFfjmc0Nj+ILrSYmX1+RmubebR1DS8mJ6Z86oT4fJ+pFTntgyzCmI58GR80 NhQ1naGoJPHEEtaUJ78VFo26wkvv6vTMUxfr8vf0XxhN7XxsyeXgYt2QrR9jE//L5EFa/vXc W26W9cXDMWvNuEwzl2gbxZeeftX6LZxJcStMf2PxK+sOu9k2jOgl2VOpo5ngSfuv2JxTPDF2 5EdzrSWxAyCAn3zhVq9u8axloFAbzwIAkKkyjn/B49UY6BoO4AGFS39Rq//jsU7nJPrV3NCo RSsDl4a0cnvdhuWZVHnwSVL1lUMon2inCaiiTp5j3t6y8jXlDyLyOPkeh0dP2dNT2Q3llbgL 7+/iNUCVVSpZQwk/Pe8zX7z3LMT5KF2Lm2JBFxNYzCzNWZpFK25qruFZcdLrpIuqyReFuqmM xiWTbv0oh1S1C2GfSMWyzk2azis/Jr4mxZ3kn61N3Vit3nYfMR931HZ6cCUSfNK3zUATTV1k nGNXwf6YIHvpIrE0c2Y6qi3TAfDHtVLfDPuzJ+cuSfz/mBsDRCl3riyltDhDQkmwHr+3thuW z/PqUWZAMGj3KC7POR7O0hwUQWltIwlQscnzdt23spIih14zt2P8HEKkHn+K4Be0KP6Nj8WQ CIThsTS607j0VFiKXSAw8T4UG+cy41vfYrfACte1yQj4sRNEKrR4qZDmH4/rVO1sQvXJ/d8m j0Q0+cG830LmOIIvQ8g1GObD6xYTiw6dWT80g+F6dyztvAda2+ibbG2kkV/mdqsFq2quQJNQ 3X4f5IvB2l249k1YzeumDXjr4rjftfXd9casBaZxgzBg+ZiI5U0jvMWhCBjNDG1rTg/xuU8l xArwYCisd3NNTB25KzgSE09VHW9d4YJ9zrql6obgsuGw9XlAMB6AjtSFJrwEaDySW1U6qyhb lneVmRt8DDBR9+9VUee8Bk09SqXSsL3PSDHdnUSkYcyFkvaehAXgRhIDm9jwdhmTkbzlJenK RYjoWpBgzyw4hpUlrAybka5DT+Z/VfyLGhuD8PFZBtOslMYvhiTbpTYt7IpWX4Eucb75FuEL mjRD+hRJUcOXEHMR1XqP730oMLF7/DdHO21af3HfbSJr+VaEfaO35OmlIV8rX6KMY2UM39uA udeuAILVG1lG8nfhzQESjAG3yPLYcmBoR6g+ypx5smh+fXvUQjr6MOBEbxXedlo/hm3h++EO YvyzG5hLi1E05oX2XLS4KIS2FcD0nkocjCsFfIPvCjBTeTWl7MWRx8XZiVvNddZuqIx2g4eX KyTwtjx17N+krs0EwIfDAOnxZnvPJNaZTvmbACiZg7DLrmNKDzVztuiZKq9TecVl+BIr1iqv j3dFUb/PzOFnj2vVha1MOgKgjvIWX4W8Iy7bBtpDnDuCdz8bRjuetB+gCE/x/s7h3fAOHQAG SN/YlhOr7iV4DkehPhjUT8kjDItPayfliCV4vONYI4RquduCz9omvhy+nk+wqoMtGdBTf1x3 iTbqNJv5VerjqPcr1gvGAoLoTFNioWRuExkMqiM7ZhMV0HP+xcV5HmRARAHzzOAIsbsqrtTy 93Kmbi1LjpeoYq8FSo0HcXQIdPeaDwkOBvtXjHdCgcECzimKTOH76SyuOqR52aWr50/p4Kqn pcSGOYzaQ==
  • Ironport-sdr: 63ac213c_sAsAkkCf94qqBKu4z3Y1WfacgXqJKf1Ay6cUf/B643bJICW mBW+Vvjx/7c2dhObfePjKEe8T06gD1RWfHqA7BQ==


> As for why Lemma f : A. Proof. exact (t). Qed. is slower, part of the
explanation might be that t is type checked twice in this script (one during the
call to the exact tactic and one during the call to Qed).

I don't think so. They both get elaborated then sent to the kernel.

Gaëtan Gilbert

On 28/12/2022 11:00, Théo Zimmermann wrote:
Hi Frédéric,

There is a proposal for making a Lemma := command available, but there was no
progress on this in the last few years. See:
https://github.com/coq/ceps/pull/42

As for why Lemma f : A. Proof. exact (t). Qed. is slower, part of the
explanation might be that t is type checked twice in this script (one during
the call to the exact tactic and one during the call to Qed). To speed things
up, you could consider replacing the call to exact by a call to
exact_no_check
(https://coq.inria.fr/refman/proof-engine/tactics.html#coq:tacn.exact_no_check).

Théo

----- Original Message -----
From: "Frédéric Blanqui" <frederic.blanqui AT inria.fr>
To: coq-club AT inria.fr
Sent: Wednesday, December 28, 2022 10:26:22 AM
Subject: [Coq-Club] exact tactic vs Definition

Hello.

It seems that

(1) Definition f : A := t.

is faster to check than

(2) Lemma f : A. Proof. exact (t). Qed.

Is there a variant of the Definition command which is semantically equivalent
to (2), that is, with f considered as a constant by the reduction/conversion
engine of the Coq kernel?

Frédéric.



Archive powered by MHonArc 2.6.19+.

Top of Page