coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] how to instantiate existential variables

From: Jeremy Dawson <Jeremy.Dawson AT anu.edu.au>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: [Coq-Club] how to instantiate existential variables
Date: Tue, 4 Dec 2018 04:06:16 +0000
Accept-language: en-US
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.mailfrom=Jeremy.Dawson AT anu.edu.au; spf=Pass smtp.helo=postmaster AT AUS01-SY3-obe.outbound.protection.outlook.com
Ironport-phdr: 9a23:e+M/+hFl+NhRImU6KRXzF51GYnF86YWxBRYc798ds5kLTJ7zoM6wAkXT6L1XgUPTWs2DsrQY07qQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmDmwbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj8KOT4n/m/Klsx+gqFVoBO9qBJwzIHZe52VO+Fkc6/BYd8WWWhMU8BMXCJBGIO8aI4PAvIFM+lGtYnyuV4OrBujDgeiHuzuxCRIhnjw3aYn1OkvFR/J3BY+ENILsHXYttv7O70cUOCuy6nIyy7OYOlQ2Tfg8oTHbA0uoeyWUb1qbMrc0E8iHB7GgFWIsYHoMC+Z2v4Qv2SH7edsT/+jhmAlpg1rvzSj2MMhhpHUio8V1lzI7zt1zJo7KNGiVkJ3fMKoHIFNuyyUM4Z6Ws0iTH9rtSomz7ALvJ+2czQIxZknwhPQcf+KfoqV7R/mSemePTl1iXZgdb2knRm//kutx+vhXceuyllKtDBKktzUu3ANyRPT7s+HR+Nh80ivxDiDyx3f5vhZL082m6fXMpkhzaUumZYJtkTDAzP2l17xjK+LcEUr5/Kk6/z9YrXhup+TKZN7ih3/MqQpnMyzG+M4MhUSX2if/uS8077j8VflT7VNi/06iqjZsJbEKsQHvqO0DBNZ3pw+5xqjDTqqyskUkHcFIV5fZR6LkYzkN0nLIP/iDPe/h1qskC1sx/DDJrDvBovCLmLdn7fkfbdx8UBSxxA9zNBE4JJUDKoML+j1Wk/srtDXEAI2MxGuz+n9FdVxzpkeVn6XAq+FLKPStkeF6f4oI+mVfYMapDL9K+U+6PP1ln84mVodfbGz0pcNaXC4GO5mI0SDbnb2jNcBCzRCgg1rBuftkRiJVSNZT3e0RaM1oD8hQsryBoDaA4upnbap3SGhH5QQaHoQWX6WFnK9VYieVvIdIA6bPdRmlHRQd7W7Roowkz2nqxT9zZJuKPeS9yEF85v+gosmr9bPnA0/oGQnR/+W1HuAGjktzzE4AgQu1aU6mnRTj1KK0Kx2mftdTIYB7vVUFAo2KNjV0r4jUoygakf6Zt6MDW2ebJC+GzhoFIA4xcJIbkpgXdy/3EiagniaRoQNnrnOP6Qat6LR23+teJRU9k2ejewavgJjRcFCc2q7mqR46g7fQZbTlFmUnLqrcqJa2zPR8GCEziyFu0QKCQM=
Spamdiagnosticmetadata: NSPM
Spamdiagnosticoutput: 1:99

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