coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Jason Gross <jasongross9 AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] how to instantiate existential variables
Date: Mon, 3 Dec 2018 23:51:00 -0500
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jasongross9 AT gmail.com; spf=Pass smtp.mailfrom=jasongross9 AT gmail.com; spf=None smtp.helo=postmaster AT mail-ed1-f45.google.com
Ironport-phdr: 9a23:7ShI8xLvQWOkcFPIDtmcpTZWNBhigK39O0sv0rFitYgQI/nxwZ3uMQTl6Ol3ixeRBMOHs6IC07KempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffwZFiCChbb9uMR67sRjfus4KjIV4N60/0AHJonxGe+RXwWNnO1eelAvi68mz4ZBu7T1et+ou+MBcX6r6eb84TaFDAzQ9L281/szrugLdQgaJ+3ART38ZkhtMAwjC8RH6QpL8uTb0u+ZhxCWXO9D9QLYpUjqg8qhrUgflhygJNzE78G/ZhM9+gr9Frh29vBFw2ZLYbZuPOfZiYq/Qf9UXTndBUMZLUCxBB5uxYY8VAOoaOuZYqZT2qVoUrRu5HgmsH/7kxzhKhnDsxq061OIhEQ7c3AwnBNIOq3DZoc76NKcXS++1za3IwS/fYPNR3Dfw8Y7FeQ0ir/GURb98b9bdxE01Gw7Gjlics5LpMy+W2+gXvGWW7+xtXv+1hWE9sQF+uD2vy98siobXgoIVzUjJ9SBjz4Y0Id20UVB0bsO5HJdJuSGXOIt7TtktQ2FvvyY6xbkGtoChcCcWz5QnwgbTa/2Bc4eW/hLuTPidLSt8iX5/e7+yhwy+/Va8xuD/TMW531ZHojJAktbWt3AN0xLT6tKASvt45kqh2yyA1xvU6uFCLkA0j63bK4U6wrM0jZcTvkHDETX3mEXylqOZakIk+u2w5+T9frrmvoOcN5NzigzmLqsundW/Df0kPQgKQmiU4v+x1Kbj/E38WLVFlOc6kqjfsJDAJMQUvLS1AwFP0tVr1xHqBDC/ld8cgHMvLVRfeRvBgZK6FUvJJaXaBOy4hRyDijBw3LiSPLT6BZPCNH/Yi+bJcrN06koaww02m4MMr6lIA60MdaqgEnT6s8bVW0dgYl6Eht3/AdA47bswHGeGA6uXKqTX6Aba6ecmIu3Kb4gQ6m+kd6oVosX2hHp8omczOLGz1MJOOn+9F/ViZU6eZCi024pTISIxpgM7CdfSphiCXDpUPSvgWqs94nQ2BNvjA9ueAI+qh7OF0WGwGZgEPm0=

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> 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

[Coq-Club] how to instantiate existential variables, Jeremy Dawson, 12/04/2018
- Re: [Coq-Club] how to instantiate existential variables, Jason Gross, 12/04/2018
  - Re: [Coq-Club] how to instantiate existential variables, Théo Zimmermann, 12/04/2018
- Re: [Coq-Club] how to instantiate existential variables, Jean-Christophe Léchenet, 12/04/2018