Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] how to instantiate existential variables

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] how to instantiate existential variables


Chronological Thread 
  • From: Théo Zimmermann <theo.zimmi AT gmail.com>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] how to instantiate existential variables
  • Date: Tue, 4 Dec 2018 16:23:00 +0100
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=theo.zimmi AT gmail.com; spf=Pass smtp.mailfrom=theo.zimmi AT gmail.com; spf=None smtp.helo=postmaster AT mail-wr1-f54.google.com
  • Autocrypt: addr=theo.zimmi AT gmail.com; prefer-encrypt=mutual; keydata= xsFNBFP+V00BEADi9eGxuXfvs0HxaYDxrOBpCJWakA4+lCi3KUGqNS5Xq0V7q+BWZZmF/pOO x4EemIickFV+DA/Yp9542XWw1vMK3uGAUpnB4sUvD+qPDnRFHDZH60p1b8rRzukHRdukW33g QsEjDdNp9iVebuBMe+IU2gdpdZxjgxzxShQMIHOX1Az65oC81eEV37XJ7b89WjArEEe0Hxcg 9+jFH3P3pNdlVaxMgEaYxeepTEfBIhWJjobr299gkgUm2a79vYnci0VONNk3crZqpNvrDK9h bqBgsEUv7t8JnIDQOJTncuoeZA+YFkceYKysO4tyDgNPgXSuI8tUfo7eU1uacNvX7LoKH1nT d4Gr26nPUyj8ntnvnT88LK+CxrrfYkUxtK5pYIQLzJSnCaCuoxOu4WJn+6PPtMhUNWC50fmA +HBt3v8YhheNEEbBZPqEGE9O1A0xB5oJJ3UCsf2VpxiEc3qCTzZHPbw5hYsS96MRysJ3gl9Z OG/u8M5r/JlyiDbVOj6WEcjgMYhuowbEX45UCCufgMWlVFDqKj685zCwhPxYSKvW2+Pkvw1K YmM4tQuF3bH2oQXe8W791N39JXQU/LHD7EHnmoJW/6ySc7Mv2f9cId/HY/DeM1U1TTTEEr1Q j6o/6PdRHGWT5PZpbNDy9+sdBieF1JWuXx24KHbhbN/OCebiewARAQABzSdUaMOpbyBaaW1t ZXJtYW5uIDx0aGVvLnppbW1pQGdtYWlsLmNvbT7CwX0EEwEIACcFAli5dBUCGyMFCQlmAYAF CwkIBwIGFQgJCgsCBBYCAwECHgECF4AACgkQ8XRKCUL1Nsf97A//QpWey31m7X20iHRRO833 BPyziP9QbIQveB8BofZfjWXBJoGExP2EZdb10UMwU0tsnD6NT5E8nKr9rRRTtnwXOcqaQHGd Y4mVLEyJYwZ8g4uZglMyTCHx6k064Ik4c5DysS/15AB72SZm+fJFayIzSY1syvTnTPxTnNx7 l697IbjS3aq3/W+vQ6MwnDgnQqggGMiA0+Tmp5VPCZX9deLmXWC1zeXe/PdCstPzeHTiIHgD wQW+0edCBELbJdhoVBKsQ3OfBK7uMJBXug7zqI3wAoywvd/E12tFzZJhLZiq8arDIimeccf4 bFZUIy17ApiFfAZJU5Rm71H29IFFMTyQxi4QFFiPjWKwtUTDB/Xv6V8nGgdhOHkNgjnRpPn4 jNxSnvr3/f1OW2yGFYyxTUlmYg72eTkSNlPAwd+WA5K3aQQtwUERzhPsK2l4Smjqr7NcI+5X 0aHBVRyRGrTmtTRz/hdyoGoxx4ts1TacquKHx88YH9GZhEng9h+Ak70oQYD9u+atp93wTyTo tghwB5Ewm3O9oruIdQtWx2H4PtP4Y3V1O/DjK42D3wKwikiHisCTKtbuIsgLTnxebWC7wN0q X9nln3KJkEnxZ/6pjLQ3XZB5YeUq58bBnr06VTZYjjYM5aZ6cQrOrnWXvrsrTh367cPKesk5 G5h/itHB0UQc+eXOwU0EU/5XTQEQAL7skL+t5KvE/j2zAzuUFtwjIA+GPBcwOJnITdT3fddN S18gCBx+EH/YPbCphKXOxRFeaD+EDuC1Ls5XK+lYu9hR7rurW7RQI+1XKO7KHQvp4i2I8J4C C+kmMw9K7fysHFG9ckiw1G5WrwiiPZHLadRIAfXwMLoDfRRNu/W8ogjm1m+UWm88DISrkIbE BYEw/fWX8QGGcFvExrFAgXyXXn4vVG90XNre+wJwIADcCqQJXCfzNF/tyetcGEwc3BZiUe/Q Ha/3xLDSm19rDkVWSpWGUr0uSziPSR9kYw6q4F1gKdvex6hnduRMEJLwFRfiHKnHZO2uN8Zj MsB1EklGvkockjkThQfFjeU3zysxfsl4tQRROpglgs1MhiMZpvCdnNTn+Gr+YHQ0sueBxpk0 6GHMmE4C4jcrLFXwfEWOnk6ISHluZS1f9qRnNZzj9ICJItT7cn1KE54jZjmVudi4kOSbihaZ 70PrXMhwphz4nVxSRMIsXdNwSkpCrcOatDS4E7EjRgHW5+CP5WON2aJPD8htAtKNej5nPbTD NFJKz6nG4jdDpxtY0PEkMHarrBpWaIdPEPgdCew5Ns5cAZC0vMkJU8uuSoEumGqzUwdVIWaV p0iZ7MTaWSZeifx7Y6x5YkYR5dMGGzKW5GeLQ7emG0I1BTcFeP+VAGewLA5xWjnhABEBAAHC wWUEGAECAA8FAlP+V00CGwwFCQlmAYAACgkQ8XRKCUL1NscXDRAAx5Y5fyDX/HvFD2Sp4E1h HbtNsPfDQ076U3qvg31e7d5560fW5hwSgZ3++3kGRO7QFTq3edo3oEEWiHuHBJxT7eXSPhXY vsM/atDyQ7Zy6fEUVuv77b3TEDHuWvn4A2kBI+ApCzXohscTuCc/PvVCoDrRQ++be2hIlxsq M7DnRr3/6FI8chCUHj3bXeXtPp8M74/3RGCiwvPZ7825NU0JP6jj1yeEuy6ts/GaZFsDj3sz TxCeZxbdARFxqmT0lf3yF2uQWj35jwqBUC/S+07fZfRRRFXwHTSSzsTTg4JKvsEpq6v0/ryc ETXqwstze+nvPvZ/bLlkiFulLFajYdIky+t5JmjmMEW0/NpK4nRo/QNuTyF1vG1/tjg/q5CZ gW++ZBoYuOR/+roFRPEKIu6Aa843e+QXvpHv4WHN1viH7ufY3D389hKkkhtnEvUu1Mv7ITDD ryw3ok6KFBrjvMQVOp0L7yZc9RYtJ0mXH9n1wWJL94q4hbUJ7fqz2rv8RbTGQoqKfDQVuVuo gH36yLP9s+RKxePuqaTn6DOOHF0/hhMCwes9pWs6ObrEPUVG1YtM6TwopIUJtuLZFWWb3X1Q 4W8EyZElzlCZhLTVhJT7p2k8xBEjpdMpsHhBMjOMljCUeRdJX55g2DVAwx3fvhdOJkuXY5Tl nCgw1L3/lCt46SU=
  • Ironport-phdr: 9a23:Atci/BX0x0/+06ddG2MN6aGrW6jV8LGtZVwlr6E/grcLSJyIuqrYYxKBt8tkgFKBZ4jH8fUM07OQ7/iwHzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba9xIRmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KptVRTmijoINyQh/W/KlMJwgqJVrhGvqRNxzIHbYp2aOeFxfq/BZ94UQnZNU8hTWiFHH4iyb5EPD+0EPetAsYf9p0EJrRymCgavBePvzzpIiWHs3a0/yeshFwfG1xEnEtISsHTbstL1OL0TUOC0yanIyDTDYuhZ2Tf48ofIcxQhreuQUrJ3dMrc0E8iHB7LgFWXrIzqJTKV1uIVvmia6epgT+OvhHQ9pwF/uDiiwNonhIrRho8N1FzI6SF0zJw2KNC4UkJ3f8CoHIZKuyyaOIZ6WsAvT3xytConzrALtoS3cDYIxZg92hLSa/+Kfo6V6Rz5TumROy13hHd9dbK/mRmy9U+gx/X5Vsau0VZKqjNJk9fWtnwQzhDT5MiKR/Rn8keu3jaP0A/T6uVaLkwuiaXbLJshzqYxlpoVr0vDAjf7lFvqgKKSbEkp+eil5/75brn4u5OQLY95hw7mPqQrgMO/AOA4MgYUX2ic/OSxzKHj/U3nT7VNlPE3k6jZsJXfJcQavaO5DApV3Zwi6xa7FTupzNMYnXwfIFJfZB2Hl5TpO03JIP3gEfi/hE2snC53yPDCI73uGY7ALmPDkbfkZbZy8VRQyAs1zdBF5pJbEKsNIPzpWhy5iNuNBRggdgew3uzPCdNn14pYV3jcLLWeNfbusd6P0dAuJuyBfoocvjC1f+Ql6vmon348nF41cqyg3J9RY3e9SKc1a36FaGbh149SWVwBuRAzGbSz2Q+yFAVLbnP3ZJoSozQyCYaoF4DGH9n/j7mI3SP9FZpTNDkfVgK8VEzwfoDBYM8iLTqIK5Y4wDMBXLmlDYQm0EP27VKo+/9cNuPRvxYgm9fj2dxyvbCBkBgz8XlrFZ3Y3TzRCW5zmWwMSnk926Ut+UE=
  • Openpgp: preference=signencrypt

You need to explicitly name existential variables (with the `?[x]`
syntax, e.g. `refine (?[A] ?[B])` if you want to be able to refer to
them by name later on, with instantiate, or with the named goal selector
`[x]: ` (see
https://coq.inria.fr/refman/proof-engine/ltac.html#goal-selectors and,
in 8.9,
https://coq.inria.fr/distrib/V8.9+beta1/refman/proof-engine/proof-handling.html#navigation-in-the-proof-tree).

Théo

On 04/12/2018 05:51, Jason Gross wrote:
> You can instantiate them by number
>
> instantiate (4 := B).  instantiate (2 := A).  This is not very
> satisfying, but it works.
>
> On Mon, Dec 3, 2018, 23:07 Jeremy Dawson
> <Jeremy.Dawson AT anu.edu.au
> <mailto:Jeremy.Dawson AT anu.edu.au>>
> wrote:
>
> Hi,
>
> thanks for all the answers to my previous question.
>
> FWIW, actually simpl seems to rewrite a goal without instantiating evars
>
> Another question about evars:
> given a goal
>
>   Γ1 ++ l ++ A :: Γ2 ++ B :: Γ3 = ?Γ1 ++ ?A :: ?Γ2 ++ ?B :: ?Γ3
>
> how do I instantiate ?A to A and ?B to B?
>
> I've tried
> instantiate (?A := A).
> and
> instantiate (A := A).
> but both those produce error messages.
>
> thanks
>
> Jeremy
>

Attachment: signature.asc
Description: OpenPGP digital signature




Archive powered by MHonArc 2.6.18.

Top of Page