coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] rewriting without instantiating

From: Emilio Jesús Gallego Arias <e AT x80.org>
To: Robbert Krebbers <mailinglists AT robbertkrebbers.nl>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] rewriting without instantiating
Date: Mon, 03 Dec 2018 11:48:58 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=e AT x80.org; spf=Pass smtp.mailfrom=e AT x80.org; spf=Pass smtp.helo=postmaster AT x80.org
Ironport-phdr: 9a23:MujT2hEagxC9ilYTYZt4dJ1GYnF86YWxBRYc798ds5kLTJ78osuwAkXT6L1XgUPTWs2DsrQY07qQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmDmwbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj8KOT4n/m/KjcxwgqxVrxCiqRNxzIHbfJqYNOZicq7HYd8WWXBMU8RXWidcAo28dYwPD+8ZMOhXqon9pl8OrRq5BQa0AO3g1CRInmXt3aIi0uouCwXG3Ag+ENIBt3TbtMn4NL0TUe+v16nD0DLOYO1N1Dby64XEbgotofaWXbJ/aMfcz1QkGQ3CjlWVs4PlPjWV2/wMs2id9epgVPigh3QpqwFrpDWk28QiipHRi44IyV3J9j91zJgrKdC5UkJ3fNypHIZKuy2HOYZ6XNsuTmNqtSog17ELuZ22cDIXxJkk2xLTceKLfoaL7x/lSe2fOy13hGh/d7K6nxuy8Vavyun7VsSs31dHrTZJnsPLtnAX2Bzf8smHSv1j8Ue9wTuDygPe5+JeLUwqi6bWKoQtzqMym5YOq0jPAyH7lFvugK+TbEok++yo6+r9YrXho5+RL5F7hxrxM6kthsCzG+M4MhIBX2SD4+SzyKXj/VHlQLVNlvA5jq7ZsInDKcsHoq65HhRa35046xe/CjemyM4XkWMGLFJDYhKHjpLmN0vAIPDiXr+DhAGWlz1hyuradp77D5/HI2LY2OPkdLd56khTzAso0ct3/ZVeALwbPPHpV0X7ucbDSBk9ZV+a2eHiXfh414cfXlWtD7QLK5T9uFuM6+0oFMCWZYYO8GLwA+h1v7jpl3BvygxVRrWgwZZCMCPwJf9hOUjMOSO90OdEKn8Du08FdMKvjVSDVTBJYHPjDbJsvnc8Eo30VN6fFLDou6SI2WKAJrMTfnpPWwKcQS+ucJ+LCa9VNXCiZ/R5mzlBboCPDo8s0Rb/5h+qk/xgNOWGoyA=
Organization: X80 Heavy Industries

Robbert Krebbers
<mailinglists AT robbertkrebbers.nl>
writes:

> For this concrete example, it appears that the ssreflect rewrite
> tactic is doing what you want (i.e. it does _not_ instantiate the evar
> with []). I have no idea if this is coincidental, or an explicit
> feature of the ssreflect rewrite tactic.
>
> Maybe some of the ssr developers around here could tell more.

See p. 44, Sec 7.2 of https://hal.inria.fr/inria-00258384v17:

,----
| Existential metavariables and rewriting
|
| The rewrite tactic will not instantiate existing existential
| metavariables when matching a redex pattern
`----

Cheers,
E.

[Coq-Club] rewriting without instantiating, Jeremy Dawson, 12/03/2018
- Re: [Coq-Club] rewriting without instantiating, Dominique Larchey-Wendling, 12/03/2018
  - Re: [Coq-Club] rewriting without instantiating, Jeremy Dawson, 12/03/2018
    - Re: [Coq-Club] rewriting without instantiating, Robbert Krebbers, 12/03/2018
      - Re: [Coq-Club] rewriting without instantiating, Emilio Jesús Gallego Arias, 12/03/2018
        
        Re: [Coq-Club] rewriting without instantiating, Jason Gross, 12/04/2018
    - Re: [Coq-Club] rewriting without instantiating, Armaël Guéneau, 12/03/2018
- RE: [Coq-Club] rewriting without instantiating, Soegtrop, Michael, 12/03/2018