coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] structural specification of where to unfold

From: Matthieu Sozeau <mattam AT mattam.org>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] structural specification of where to unfold
Date: Fri, 28 Sep 2018 21:58:35 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mattam AT mattam.org; spf=Pass smtp.mailfrom=matthieu.sozeau AT gmail.com; spf=None smtp.helo=postmaster AT mail-wm1-f54.google.com
Ironport-phdr: 9a23:gsGxcxFDBlPSuvGkpvmKEp1GYnF86YWxBRYc798ds5kLTJ78o8+wAkXT6L1XgUPTWs2DsrQY07WQ6/iocFdDyK7JiGoFfp1IWk1NouQttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZrKeTpAI7SiNm82/yv95HJbAhEmDiwbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VDK/5KlpVRDokj8KODE38G7VisJ+gqFVrg+/qRNj2IPbep2ZOeBkc6/BYd8XR2xMVdtRWSxbBYO8apMCAe0bMuZEs4n9p1oOogWjBQKxGe3vzT5JiWHs0q0nzu8sFgTG0xY8H9ISqnvUqc74NKIIXuCp0KnH1zDDY+lR2Tfn54jFaxYsquyCU7J3dMre00gvFwXdg1qMrozlJTWV2foJs2if9eZvS/+gi3MhpgpsoTav3t8hhpfVio8R0FzJ9iV0zJwoKdGmS0N3e96pHZRWuiqHLYV5WNkiTHttuCsiyr0Jp5q7fC8SxZQi3RHfaviHf5GG4xLmSeqdODl4iXJqdb6liBay9k+gyuL4VsaqylpFsi1FktzUunAM0Rzc9NSHR+Nj8ku93TuDzQPe5+FeLUwpi6bWKIQtz74/m5YLtETMBC72mEH4jK+McUUk//Cl6+H9bbX6up+cN450hR/jMqg0gcy/BuU5PRYUUGiG4um827jj8lf4QLVOlPE5jq7ZsJXCKcQBuqG5GxNV0pok6xunEzim180YkWAbI1JBZRKIlJPkO0rOIfD9FfewmU6gkDZtx/DcP73uGI/BLnbZkOSpQbEo4ElFjQE30Np35pROC7hHLuigdFX2sYn9BwMlMw253q7cD8dw355WDWeGHrOQNYvXuEOU7+dpJPODMtxG8A3hIuQosqa9xUQynkUQKPHwjMknLUugF/EjGH23JH/lg9MPC2AP51NsQ+njiVnEWjlWNS/rA/AMowojAYfjNr/tA5i3ieXbjiKyAoFfYyZBEF/eSS61JbXBYO8FbWepGuEkkjEAUuL8GYoo1BXrqwqjjrQ6cqzb/SoXsZ+l399wtbXe

Hi Abishek, ssreflect’s rewrite supports contextual patterns and unfolding with “/“. Maybe with `pattern` and `eval unfold in` and `change` you could program this in Ltac as well.

Best,
— Matthieu

Le ven. 28 sept. 2018 à 15:14, Abhishek Anand <abhishek.anand.iitg AT gmail.com> a écrit :

Many times, we wish to unfold only certain occurrences of a definition.
The unfold tactic takes the occurrence number as an integer.
However, using an integer to refer to occurrence seems less robust and the integer provides less useful information when proofs break.

Is there a way to more structurally specify where to unfold?
For example, is there a way to specify where to unfold as follows:

match goal with
[|- context[?x+978]] => unfold foo in ?x
end

Thanks,
-- Abhishek
http://www.cs.cornell.edu/~aa755/

[Coq-Club] structural specification of where to unfold, Abhishek Anand, 09/28/2018
- Re: [Coq-Club] structural specification of where to unfold, Matthieu Sozeau, 09/29/2018
  - Re: [Coq-Club] structural specification of where to unfold, Enrico Tassi, 09/29/2018