coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Théo Zimmermann <theo.zimmermann AT telecom-paris.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] exact tactic vs Definition
- Date: Wed, 28 Dec 2022 11:00:38 +0100
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=theo.zimmermann AT telecom-paris.fr; spf=Pass smtp.mailfrom=theo.zimmermann AT telecom-paris.fr; spf=None smtp.helo=postmaster AT zproxy120.enst.fr
- Dkim-filter: OpenDKIM Filter v2.10.3 zproxy120.enst.fr 8390C80D34
- Ironport-data: A9a23:o309N6ND56qGfiDvrR1yk8FynXyQoLVcMsEvi/4bfWQNrUog0GQDn zRNDT/QaPePMWukKd8la43j9U4H65DdyoNmTHM5pCpnJ55ogZqcVI7Bdi8cHAvLc5adFBo/h yk6QoOdRCzhZiaE/n9BCpC48T8mk/jgqoPUUIbsIjp2SRJvVBAvgBdin/9RqoNziLBVOSvU0 T/Ji5CZaQHNNwJcaDpOsfvZ8kM35ZwehRtB1rAATaAT1LPhvyJNZH4vDfnZB2f1RIBSAtm7S 47rpF1u1j6xE78FU7tJo56jGqE4aua60Tum1hK6b5Ofbi1q/UTe5EqU2M00Mi+7gx3R9zx4J U4kWZaYEW/FNYWU8AgRvoUx/4iT8sSq9ZeeSUVTv/B/wGWaInHz0fJyUH1pNKY7ue9YA2VW2 PgHfWVlghCr34pawZqpUvNrltV6dpGtMYUEpjdu11k1D95/Gs+FGvSWo4UehWZr7ixNNa62i 84xdTpia1LSYhhKN00SAZQ4tPulgnT0dDgdsFuPpLFx7XK7IAlZjOOya4OOI43iqcN9rlmah n37uD3AASo/Ct+05GeL2Wyoibqa9c/8cNtOReznpqECbEeo7mcUEVgdUUaxieKoj1a3HdNZM U0dvCQ0xZXe72S5VsP6Twzh+ibCsxgHR5xeCYXW9T1h1IKIsgyGFG8YEgIeYfcF98YZRzgy+ 1uWyoaB6SNUjJWZTneU97GxpDy0ODQIIWJqWcPiZVBaizUEiNpt5i8jXuqPA4bp3o2uQ2uYL ySi9nRm2Oh7Ydsjjf3TwLzRv967jrbzJuLfzj3eRGO+hu+STNH4P9XxgbQ3xV2mKIvcQlTEk mINncOThN3i4LmfjDaKUPRURunv6vCeLHvSmzaD/qXNFRzzoRZPnqgKulmSwXuF1O5eJlcFh 2eI4WtsCGd7ZifCUEOOS9vZ5z4W5abhD8/5cfvfc8BDZJN8HCfeon40PBDNjzq8yxlz+U3aB Xt9WZj1ZZr9Ifo+pAdau89HgeZDKt0WmTODG8+rk3xLL5LANSLFIVv6DLd+RrllvfLb8Fq9H yd3LcaMwglSSoXDjtr/r+YuwaQxBSFjXfje8pUPHsbae1oOMDx/V5f5nO1wE6Q7xP49vrmTo RmAtrpwkTITc1Wad17aAp2iAZu0NatCQYUTZHN0Zw70hyB4MO5CLs43LvMKQFXuz8Q7pdYcc hXPU5/o7i1nGmWfqQcOJ4LwtpJjfxmNjAeDdXjtKjsmcpIqA0SD9tb4d0G9vGMDHwimh/sY+ reA7wL8RYZcZgJACM2NVumj4WnstlcgmcVzfXDyHP9tRGvW/rJXdhPB1s0MH5lUKDHo5Cer6 AKNMBJJ+cjPu9AU9ffKt4ClrqCoMbNMIVpeLjOK8ZKGHynR+26x5YpyQceJYjHve2fm84qyZ ehu7q/dMd9WuH1oooZDA7JQ4qZm3OTWpphe1RVCIHXHS3+JG4FQCCCK8ucXv5Ic24IDnxW9X 3y+3+VzOJKLCZvDK0EQLg90Vdaz/6gYtReK5MtkPXigwjF8+YeGdkBgPxOsrih5B5ktOaMHx dYRguIn2zaduDELbOnf1jt18l6SJEMuS68k75EWILH6gzoRl21tX8buNT/U0rquNfN8alInM x2Ftprk3r58/HfPQ1A3NHrK3Ndeu6gwhQB3/AcCCWikytvhrd0r7SJV6gUyH1h0zA0Y8uddO VpLFkxSJIfQ9BdKmsVjXHCJGShcNiLE6EDall4ClUzCbkySTmeWBnYMCeWM20E48mxnYTlQ+ o+D+lvlSTrHeMLQ3DM4fFxM8djPbIZUyFXZucaFG8+lIcELUQD9iPXzWVtS+grVP8whoWbm+ 89oxb9UQo/mP3cyp6YbNdGr5Y4IQkrZGF0YEOBTx4JXL2TyYzro5COvLXq2ccZzJ/Dn10+0J shtB8BXXSSFyye8gWEHNJEIPoNLsqYl1PgadpPvAFw2gb+Vgz5qkZDXrybFlDAKRfdqmp0DM Y//TW+JPVGRonp2oFXzivd4FFC2WvQ+Xz2k7tuJqL0IM7khrNBTdVoD1+ronneNbypi0RGmn CLCQK70l95d2YBdxdrwNpVpBw6xLcHXUdaZ0QGssuZhacHEHtfOujg09HjmHVVyFpkAV+tnk Y+itIbM43rEm7ItQkblm5WlPItY1/WYBeZ4HJr+EyhHoHGkRsTp3Somx0m5Dp54yPVm+citQ lqDWvuaLNI6dY9U+yxIVnJ4DR0YNqXQa5XgrwObq9CnKEAU8S7DHeOd2U7ZV0NpXQ5WBMSmE S7xgeik2f5ApocVBBMkOeBvM6UlHHDdA5kZZ//DnhjGKFnxjl277+6o0VJq7DzQEXCLHfrr+ Z+PFFC0aB22v7qO191D9ZB7uhoMFntmnO0sZQQn9sVrjyyhRnszRQjH3U7q1rkP+sAz6H35W N0JRHk6EyLtTG0eKVPx5s//GAmFbgDL1hEVORRxl354qQ/vbG9DPFel3jtt53p9fT6m1Oi9K MpY9GeY0t2Z3MRyXehKjhCkqb4P+x4Zr07kPWjhnsj/CBEbRK0Dzn16WgRXPcAC/wchi22TT VUIqat4rI1XhKI//QuMu5KYJf3BgA7S8g==
- Ironport-hdrordr: A9a23:GlOWXqgWypymZn1nn3dBu8Pvu3BQXuYji2hC6mlwRA09TyXqrb HXoB19726PtN9xYgBapTjjUJPtfZq4z/FICOYqTNWftWXdyQyVxeJZnO7fKl/bak7DH4dmvM 8KGcUeaOEYZmIK6/oSjjPIaurIjOP3lJxAWt2x80tQ
- Ironport-phdr: A9a23:FAySuxDnAEw2rctncnJeUyQURkoY04WdBeb1wqQuh78GSKm/5ZOqZ BWZua8wygGTFt2Ko9t/yMPo8InYEVQa5piAtH1QOLdtbDQizfssogo7HcSeAlf6JvO5JwYzH cBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1JuPoEYLOksi7ze+/94PTbglShTexf7x+I AmyoA7MqsQYnIxuJ7o+xRfOvnZGYfldy3lyJVKUkRb858Ow84Bm/i9Npf8v9NNOXLvjcaggQ rNWEDopM2Yu5M32rhbDVheA5mEdUmoNjBVFBRXO4QzgUZfwtiv6sfd92DWfMMbrQ704RSiu4 qF2QxLulSwJNSM28HvPh8JzgqxUrxyuqRxizYDKfI6bO+Fzfr/Efd4AWWZNQshcWi5HD4ihb 4UPFe0BPeNAoofjp1sJtxy+DhSvC+Puzz9Ig2H53bc/0+s7FwHG2hErEtUSsHTUstr1M70eU OG0zKnNyDXMcelW2TLn54jOdBAsuu2MUqx0ccXP1UYvEAbFgkyIqYP/JTOV1/8Nv3KV7+p6T O+ijXMspA5trDa13MgslpXJiZwPylDC7Sh03Js5KNm2RUN5YtOpEIZdujyVOoZ1Tc0vXXxlt TgnxrAJpZK1fCYHxYolyhPQZfKKfJWE7xPhWeqPLzl1imxodbSijBi89kigz/fzVsiy0FtSo SpFk8XMtnAQ1xPI8MSIVvx9/kK51TaO0QDT8OBELloumarVMZ4sxKM7mJkLsUnbAyP7lkf7g LWLekgg9eWk8frrbq/7qpKYOYJ4kh/yPb4ylsCiBOk3LBQCUHKe9Om41LDu/0j0TKhXgvIrj qXUtYrVKtkFqaO5BgJZz5gv5hiwAjqjzNsVmWQLIExAdR+Ij4XlJUzBLfblBvmlmVusii1kx /XeM73hHJrNKn/Dna/gfLZl8U5czwUyzNBC655KFr0NOuz8WknqtNzEFBM5PRa0z/7mCNV7y IweRXqCDrKXPa7Qq1OE++YiLuaWaIMLojrxNvwo6vD2gX88g1AdfK2p3ZUNaHC/G/RrO1mZY XryjdcGC2sLvws+TOnviFKcSz5TYmy9X6Q65jwgFIKpE4PDSZ6xj7yG2Se3B4VWaXpcClCNC nfkbYuEW+0UZCKUOcBuiiYEWqS5S489yRGusxf3x6d/IurO5iIYrY7j1MRy5+DLiR4y8iV0A 92B3GGJUmF7hXgFRyQ23aB6uUxy0E2P0al+g/xCFNxc/elFUgkgNc2U8+svANfrHwnFY92hS VC8Q9zgDytiYMg2xooyY8d6U+ejixXOxS+jBbldw6CLCZty4KPZ2nXrIs97zV7a2a0shF4jB 9NGL2y9wKBloVuAT7XVmlmUwv75PZ8X2zTAoT/rJQumuUhZVFU1SqDZRTUEYVOQq93l50TER rvoCLI9MwIHx9TRYrBSZIjPilNLDOzmJMyYe3i4znuwCBHO1LKJaYfwfmwb2g3BBUwJmAcWu G6PLwklQCm78CrFFDI7LVv0eAv39PVm7nayT0s61QaPOlFh2r3z6B8QgPGGTvoV2JoYtSMso DJxWU60xdPNTdSa9EJ6ZKsJR9Q77R9c0H7B8QxwOpv1N6d5mlsXaBh6pWv8zw9wGpQZy5Bso XUx0Ex8M8p0yXtncDWVldD1M7zTcSzp+Qy3LrXRwhfY2cqX/aEG7LI5rU/itUenDBhq9XIvy NRT33aGg/eCRAMPTZL8VFo2/BlmtvnbZCc6/YbdyXxrN+G9rDbD39sjAOZtxAynep9TN6aNF Qm6FMN/ZYDmNOwnnB67bxcBMfpX/agyF9+rc/aN36vuJO96nSngg34GqIFx30SQ9jZtH/bS1 sVgobnQ1Q+GWjHgyVa555msxsYdNG1URCzmmHO3YewZLrd/dosKF2q0dsi+x9ElwoXoR2Yd7 1m7QVUPxM6ufxOWKV37xwxZk0oN8hnF0WO1ySJ5lzYxo++RxivLlq7+dBcAfHxKQWxvl1LlJ 46ck90eUUOvak0xnQGk/gD03eIIwcY3Z3mWWkpOcyXseit+Uqa38KiDZstC8pYhtyN/TOm4b FudT/vlqgEbyGXtBSENoVJzPyHvsZL/kRtgjWubJ3smt3vVd/Z7whLH7cDdT/pcttYfbBFxk iKfRl21Pt3yuM6Ri4+GqeemEWSoSpxUdyDvi4KGriqyo2NwU1WzmPW6m9uvFgZfs2ezy9lnU mParRP5b5Pu3qK8Gf5qekRjA1q588NgG5o4nJF4iJwL2Hccj4mY5jJeyji1aIQHn/i4NStWD TcQprydqBDowkhiMm6Ey8riW3ORz9EgL9i2b2UK2z4susVDCaOa9rtBzmN+plu1qx6UYOAox 2xCj6J/tDhAxbhY41lIrG3VGL0ZEEhGMDa5kh2J64v7t6BLfCO0dqD20kNinNenBbXEowdGW X+/dI1xeE04psh5Ll/I12X+r4/+f9yFJ84TuxrSgRbFiuVPLZs3kNIWiC5qMmX4+GUs0e8gy xJ0l8Lf3sDPOyB28aS1DwQNfCH1asRV6DDoiKtEm8+Q2aizE5FsETIOGYPhV/OzVjwI/6eCV U7GAHg3rXGVHqDaFAmU5RJ9rn7BJJusMmmeOHgTydgxDAnYPkFUhxoYGSkrhpNsXB7/39TvK Q0qg1JZrk69sBZHzfhkcgXyQnuK7hn9cS86EdCeNEYEt1odoR6EbYrEqLsiRWYDpvjD5ESMM jLJPVwQVDNXBBTWXAu7MOv0t4vLq6/BXLT2LuOSM+zV9qoHBqvOn9Tzj+4Et36NLpvdZCE6V q9lhBIRBishFZaDyWdVR2QWj36fNpXE4k7tpmst6JnkoLOwAWeNrcOOE+UAa403okLo3//Rb LXIinQje2QI39RVnyCAyaBDjgdD0GczKn/0SO9G73eUKcCY0q5PU0xCOng1aZYOtvtnmFMUY Ybako+nj+8jyKNoTQ4cDhq7w5rhMsUOJyvV2ErvIkGNOfzGIDTKx5qyeqagUfhLi/0SsRSsu DGdGkulPzKZljCvWQr9eedLxDqWOhBTouTfOl5kFHTjQdT6axa6LM4/jDs4xqcxj2/LMmhUO CZ1ckdEpLmdpS1ChfA3F2tE53tjZe6K/kTRp/HfMYoTuOB3Dz5chfpA52QrkuENqixCX+Azl jGT5t9irle6k/WenzpqVB0dz1QDzImPvEhkJeDY7swZAimCpUNRqz/WUkVR9L4HQpX1tqtdy 8bCjvf2ITZGqJfP+NcEQtPTMISBOWYgNhzgHHjVChEERHilLzK65QQVnfeM+3mStpV/pILrn c9EVr9WUxonF/YfB15gFdoECIt6Wj4vlrvelMcS5GH4ogObF6A49tjXE+mfB/niMmPTlb5fe x4B2q/1N6wBLpf8y107MAE8kYLRBwzeR5oex08pJh9xq0JL/n9kS2Q10E+wcQKh7kgYEvusl wI3gA9zCQzC3Cvh51o8IV+PvCIqkVJ3l8+32Fh5lRbtIaO9VoZTTjL9rUkqdJ3hEV4dheyaj 1R+MyfVHugJybZmbnwthhWO4fNy
- Ironport-sdr: 63ac13c8_5ibPjZdK6t4MAOauXpRQX67ABOQGgTRHqyvIzCt+ctHovW0 D1BnVXK8mvg9q0BXBqBDEY9lB8j+HO9sNpsI9nw==
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.
- [Coq-Club] exact tactic vs Definition, Frédéric Blanqui, 12/28/2022
- <Possible follow-up(s)>
- Re: [Coq-Club] exact tactic vs Definition, Théo Zimmermann, 12/28/2022
- Re: [Coq-Club] exact tactic vs Definition, Gaëtan Gilbert, 12/28/2022
Archive powered by MHonArc 2.6.19+.