coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Théo Zimmermann <theo AT irif.fr>
- To: Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] Definition as opaque as Qed
- Date: Thu, 2 Jun 2022 15:40:14 +0200
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=theo AT irif.fr; spf=Pass smtp.mailfrom=theo AT irif.fr; spf=None smtp.helo=postmaster AT korolev.univ-paris7.fr
- Ironport-data: A9a23:UPdwHqvViUAlCBRvDI39ByVMPOfnVJVYMUV32f8akzHdYApBsoF/q tZmKWuFaf/ZZGv3L9h1Odi/pE8B6JCAztIxQQpp+yg1QSwTgMeUXt7xwmXYb3rDdJWbJK5Ex 5xDMYeYdJhcolv0/ErF3m3J9CEkvU2wbuOgTraCYEidfCc8IMsboUsLd9UR38g52LBVPyvX4 Ymo+5OHYgf8s9JJGjt8B5yr+EsHUMva42twUmwWPZina3eD/5W9JMt3yZCZdxMUcKEMdgKJb 7qrIIWCw4/s10xF5uVJPVrMWhZirrb6ZWBig5fNMkSoqkAqSicais7XOBeAAKtao23hojx/9 DlCndu8Zzd2HIHvo7sYcjIFLgxxfqF4oqCSdBBTseTLp6HHW3jr2fJqAV9wIIsZ5KNvCHtP7 qNeJiplghKr3rPqhujmFq8y34J6d5mD0IA34hmMyRnFDfshaZHZQquM68UwMDIY350RQK+DP 5BxhTxHaD3dZR1FN3stLqkwt9zxiyCiYgBpkQfAzUYwyzGPnV0ugOeF3MDuUteNXIBemluSj nnX+nzwRBAcLt2WjzSfmk9AncfMmjn8XI8MUqC+9+AvmFSJx3dMThMMPbemnRWnogmydeIAC WA3wXUrjINvyWGkDdXDBQLt9RZooSUgc9ZXFuQ77iSExazV/xuVCwA4othpNIBOWCgeGWFC6 7OZoz/6LWA/4ObPExpx4p/O8WvtZED5OEdYPXdscOcT3zX0iK8J5v4lZu5qCq+u5jEeMW6tm 2nWxMTSrx71icNO26j+00rOhTmhzqUlrzLZBC2JAApJDSsgNOZJgrBED3CHtp6sy67FEjG8U IAswZT20Qz3JcjleNaxaOsMBqq1wP2OLSfRh1Vid7F4qWnxoibzJ9sIsW4gTKuMDiriUWG1C KM0kV0KjKK/wFPxN/Efj3+ZV5VznPKxS7wJqNiNNIATM/CdizNrDAk3OR/BgDCy+KTdubsyP 56HfNzEMJrpIfoP8dZCfM9EieVD7nlnnQv7HMmnpzz6j+b2TCPLGN8tbQvfBshkvf3siFiEo 753aZHXoz0BC7eWSneMruYuwaUiaCFibXwAg5MJKbHrz8sPMDpJNsI9Npt6J9c0xP4Nyr+Zl px/M2cBoGfCabT8AV3iQhhehHnHB/6TdFo3Yn4hO0iGwX8mbdr95asTbcRlfKMm+qpt16csH fUCfsyBBNVJSyjGomhGNMSn/NA7JRn71xiTOyeFYSQke8IyTQL+/NK5LBDk8zMDD3bquMZn+ ++g2wrXTIAtXQNnCMqKOvujw0nu73kHmew0UVGReotff0Dl8Y5LLS3tj6ZreJhRc0Wfn2qXj l/EDw0ZqO/Bp54O3OPI3a3U/Z20F+ZeH1ZBGzWJ57iBMySHrHGoxpVNUbrVcD3QCDH09aGla bkHxv3wKqddzlVNqY14Hqgt0KQ/+Z73rqVb1VsiEm+SNwanDbZpI3+n28hTt/QVn+UJ51DoA hqCqotAJLGEGML5C1pPdgArWeS0yq1GkDfl6/locl7x4zV6/efZXBwKbQWMkiFUMJB8LJghn bU6oMcT5gHj2AAmNM2K0nJd+2iWdCZSUKI9sZUXHsn2jAs1j0lLe53HVWn4+sjXOdlLN0ArJ B6ShbbD3uwFnBqcKCRrTXWdj/BAgZkuuQxRyAFQLVq+mu3a2q090ipX/GllVQ9S1BhGjrx+Y zA5K01vKKyS1D50n8wfDXu0EgRMCRDxFpYdELfVeLk1jnVEV1Ah6EU+PvyK+E0HtX9afyYe5 LiCyX26FzjwFC00Mu3eRmY9w8EPj/QonuEBpCxjN8WfHpd8byCNbmqGez8TsxW+aS8urBSvm ASpldqcrYX6Ly8e5aMhY2VfOXL8VzjcTFF/rTpdEG/l0I0SlPxeGdRDFqxpRv5wGg==
- Ironport-hdrordr: A9a23:8EsYX6s4phdzisoZxvB7IM9m7skD09V00zEX/kB9WHVpm6uj5r 6TdZUgpGDJYVMqNE3I9urwQJVoLUmsjKKdpLNhW4tKPzOW3FdATrsSl7cKqgeIc0aVm4A9tZ uIMZIOb+EYZmIK8PoSjjPIb+rIA+P3k5yAtKPxy39sSEVNcKFv7wBwD0K+HldtTAdLQboVfa DsnfavawDQG0j+4amAdwh1L9TrlpnulJf6bQULCnccmXr+/w9AIYSKdiRwAS1wbxp/hbRn+2 nGlwT44+GOtO62zxnEzmO71eUi6a/c4+oGB4iHi8oQIjXozjyjYp9sMofyy0FCnMifrFVvmt jPpx8hOoBI9nvNYnvdm2qlqkHd7Ao=
- Ironport-phdr: A9a23:MeVcmh3cq0aLpHbwsmDOpA8yDhhOgF0UFjAc5pdvsb9SaKPrp82kY BaEo6Q3xwGSFazgqNt8w9LMtK7hXWFSqb2gi1slNKJ2ahkelM8NlBYhCsPWQWfyLfrtcjBoV J8aDAwt8H60K1VaF9jjbFPOvHKy8SQSGhLiPgZpO+j5AIHfg9q52uyo/5DffQpEiTuzbLhvM Bi4sALdu9UMj4B/MKgx0BzJonVJe+RS22xlIE+Ykgj/6Mmt4pNt6jxctP09+cFOV6X6ZLk4Q qdDDDs6KWA15dbkugfFQACS+3YTSGQWkh5PAwjY8BH3W4r6vyXmuuZh3iSRINb7Rq4oVzu88 6hrSQfoiCYZOD4/7GHXkdF7gKZCrB68uxBz34vYbYeIP/R8Y6zdZ8sXSmVPXslTVyJPDICyY ZYRAeUdMuhVtJX9p0IUoBeiGQWgGOHixzlVjXH2x6061OEhHBnY0gwgBdUOt2zbo9b0NKcXV OC60rPIzTDZYPNQ3zf29Y/Fcgwhof6SWrJ9asvRyVMuFwPLlFmQp5blMiqT2+8QvGeV8/BuW vizi247tQ5xuD6vy98wh4fHm48YxEzI+Ct5zoorKtO1VFJ3bN25HJZfqSyXKpd6T8A+T2xru Cs21L0ItIOlcSUFzJkqxBzSZvyJfYWW5B/oSeifITB9hH1/ebK/gQ6/8Uehyu3gVsm0zU1Fo jBZndnLs3ABzx3T6s6dSvt85EitwziP1xrV5+pZIk40jbLWJ4Mlz7M/jJYfr0TOEyDslEj3k aOabFgo9+ar5uj/fLnqupuRO5V3hwz+KKgihNCzDOciPgQTXGWX5+Kx36D580LjWrVFlPg2n 7HZsJ/EIcQboba0AwxS0oY57Ba/Cymp0MoCkXkaKlJFeQyHg5HxO17UOvD4DOy/jla2nDdl3 fDKJrzhApPTIXjfiLrtYLJw5kFGxAYtzd1S6IhYB7AcLP7pR0P8ut/VAgc8MwOuwubnDNt91 pkZWWKKGqKZLKPSvkGP5u80IumMfo4VuDjnJ/gr/f7ilXk5lkQFcqmzwZQXcGy4HuhhI0iBf Hbgms0BHnsSvgoiUOzqj0WPXiJUZ3arRq4z+jU7CJ+9AorYXYCsgLmB3D+hEZFMZ2BGDEqME XbyeImeVfcMcnHaHsg0uTsdHZOlVoVpgRqprUrxz6dtBuvS4CwR85z5gotb/erWwC0ydDtDP cWY1myXSmhymCtcWz8724h+u01zjFmZh/sry8dEHMBesqsaGjwxMoTRmqkjU4iasmPpe96IT A3jWdC6GXQqScp3xdYSYkF7EtHkjxbZ3iPsDaVG36eTCskS9aTRl2P0O94702zPgbUhgl4OQ 9FOOyuonP037BDdUrbAiF7RjKO2beIZ1S/J+n2EyD+SvExfeA9qUKuDU2pMLlDOo4Hf4UXPB 6SrFaxhMgZFzpuaLbBWb9TykVhcbPTkItPabnz3hmGxG1OQz6mNd9WsdX91MDz1Lk8CnkhT+ H+HMVN7HSK9uyfFCyQoE1vzYkTq+O04qXWhT0ZywRvYJ0tmn6G4/BIYn5n+A7saw64EtSE9q j51AEf13tTYDMCFrhZge6MUaM004VNO32bU/wJnOZnoI6dnj18YOwN52iGmnwl3B4JokNIro jUk1ks6KK6V1k9AayLNxYr5afXcLmj/+gzqaraDgwCClozLpuFRsbJh8AWw2WPhXlAv+Hhmz dRPhn6V55GRSREXTYq0SUEvsR5zu7DdZCA5oYLSz3xld6eu4Vqgk5okAvUozhG4cpJRKqSBQ UXuE8AdL8m0KeJslULjPVoUeftf8qI5JZbsa/uL34aqJudu2jy8xzcigsg1wgeH8CxyTfTN1 pAOzqSD3weJYDz7iU+orsH9nY0siSg6JmOk0mCkAYdQYvY3ZoMXESK1JNXxwNxihpnrUnoe9 Vi5BlpA1tX7MRaValX820VX2yF16TS7mSa/5z1ukj9voLDX0CHVwuvkfQYKISYSFTUk1wqwZ 9btyYlBDAChdEAxmQGg5FrmyqQTv6l5I2TJACIqN2D3I2xkTqqsp++Has9L5okvtHYfW+C9b FaGD7/l9kJLj2W5QjcYmml9Lmr66fCb11RghWmQLWh+ti/ccMB0nlLE4cDEAOVWxnwATTV5j j/eAh69OcOo9JOajcSm0Kj2WmS/W5lUaSSuw5mHsX7x+W1nBjW+hfG93NP9W1tywWrg2t9mW D+d5gr8b47D1r67P6RpZAM7YT20o9o/EYZ4nIwqgZgW0nVPnZSZ800MlmLrOMla06bzPzIdA CQGyNnP7E35yVVueziXkpnhWCzXka4DL5GqJ3kb0SUn44VWBbeIufZayDBtrAPwqBKZNvF5m n11JeIGznkcjqlJvQMsyn7YGbUOBQxDOjSqkR2U7te4paERZWC1cLH22lAs1damRKqPpA1RQ hObMt8rADNw48NjMVnNzGy764fqf8PVZM4SsRvcmgnJjuxcIpY83vQQgi8vNWX4tHwjg+k16 H4mlYm9p5SCIn5x8biRARlCMTn4eYUO/DDzyL5XhMeNgMahBNQpGzkGWofpUeP9ED8WsqeCV U7GGzk9p3GHXLvHSFbOtAE88i6JTcntbirHdxx7hZ14SRKQJVJSmlURVTQ+xdsiExyygdfma AF/7ywQ4Vjxrl1NzPhpPl/xSDS6xk/gZzEqRZyYNBcT4BtF4hKfLcyT6cpyBSBWuJO75l/oS CTTd0FTAGcFV1bRTUjkJaWr7MLc/vKwBe2kKP/Df/OTr+1AEu+B35O0jc1o5XzfU6fHdmknB Po91E1ZWHl/EMmMgDQDRRsckCfVZtKarhOxksWWhsO46vPvVRyp+I2OFf5KOM9u4E/wj73Rb 4Z4aw54MzdWkJ0WlyagIF033UQThWdgbWv1eYk=
- Ironport-sdr: 6uxtq4aEF2ld12yyWwnfp0HjmLqkm8qyiMFvH8qlgBSJwPiGAjWenqyLbrdefyWiaX6D/y++gu AfB90XhqDSvhn7xXhL4ewt0I/eQlc5WkhmaPwP40E3hFPFbco+Y9IFQ6hCAqmb/HMIxMSoPA2x LJqCJPtRVjm7NFe0+GWLBtmI5U+HouFsEEE8pN1OGy+2EBtlIk2PvyR6L9S3x8zUiXBGmicBQC 8oJc8lBpKwEnj+RwwcYTPksq0XVWIBVE2/QRRMZVG0EgoexJitZ9AbwIrbqgi14gal5GQBSocT l4yg+C2AP8zLuBcsoEBwKyNe
This is a known limitation of the current vernacular. There is a
proposal to extend it with a Lemma := feature. See
https://github.com/coq/ceps/pull/42. But implementation of this
proposal has not started.
Le jeu. 2 juin 2022 à 15:38, Li-yao Xia <lysxia AT gmail.com> a écrit :
>
> There could be an attribute for this.
>
> One hacky solution is to start from the normal, transparent definition, and
> use it in a separate Qed-ed Definition which also extracts the type from
> it. The initial definition can be erased by making it local to a section:
>
>
> Notation type_of x := ltac:(let t := type of x in exact t) (only parsing).
>
> Section FOO.
> Let foo_ := 3.
> Definition foo : type_of foo_.
> Proof. exact foo_. Qed.
> End FOO.
>
>
> Cheers,
> Li-yao
>
> On 2022-06-02 1:19 AM, mukesh tiwari wrote:
>
> Hi Qinshi,
>
> I am not sure if it's exactly going to solve your problem, but have a look
> at the locking and unlocking mechanism in math-comp [1, 2, 3].
>
> Best,
> Mukesh
>
> [1] https://github.com/math-comp/hierarchy-builder/wiki/Locking
> [2]
> https://github.com/math-comp/math-comp/blob/master/mathcomp/algebra/matrix.v#L282-L283
> [3]
> https://coq.inria.fr/distrib/V8.14.0/stdlib//Coq.ssr.ssreflect.html#locked_with
>
> On Wed, 1 Jun 2022 at 22:11, Qinshi Wang <qinshiw AT cs.princeton.edu> wrote:
>>
>> Hi everyone,
>>
>> Is there any way to make a "Definition" as opaque as a proof ended with
>> "Qed"? My use case is I want to specialize a lemma and define
>>>
>>> Definition foo := lem (* a lot of paramters *).
>>
>> I want to omit its type, which is long. So I cannot start a "Proof." in a
>> normal way.
>>
>> Thanks,
>> Qinshi
- [Coq-Club] Definition as opaque as Qed, Qinshi Wang, 06/01/2022
- Re: [Coq-Club] Definition as opaque as Qed, mukesh tiwari, 06/02/2022
- Re: [Coq-Club] Definition as opaque as Qed, Li-yao Xia, 06/02/2022
- Re: [Coq-Club] Definition as opaque as Qed, Théo Zimmermann, 06/02/2022
- Re: [Coq-Club] Definition as opaque as Qed, Li-yao Xia, 06/02/2022
- Re: [Coq-Club] Definition as opaque as Qed, mukesh tiwari, 06/02/2022
Archive powered by MHonArc 2.6.19+.