coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] structural specification of where to unfold

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] structural specification of where to unfold
Date: Fri, 28 Sep 2018 13:13:58 -0700
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=abhishek.anand.iitg AT gmail.com; spf=Pass smtp.mailfrom=abhishek.anand.iitg AT gmail.com; spf=None smtp.helo=postmaster AT mail-yw1-f46.google.com
Ironport-phdr: 9a23:YEzDKBfhAl26lQpD+fw4Gz4TlGMj4u6mDksu8pMizoh2WeGdxcuzZR7h7PlgxGXEQZ/co6odzbaO7Oa4ASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTahY75+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v6bpgRh31hycdLzM2/2HZhMJzgqxGvhyuuwdyzJTIbIyPLvdyYr/RcNEcSGFcXshRTStBAoakYoYTFOUBPedYr5L9p1QQrhu1GBWhBOX1xT9Om3D9wKo33P46HgHG3QwgBNIOv2rXrNnvLqgSV/q6zK/VwjnZbvNW2Cv96IfTfxAupPGDR7Nwcc7LxUYzEAPFi0ydpIr4ND2b0eQNtnKU7+tmVe+3l2EnrBtxoj6xyccojonFnJwaxU3Z9Sh/3Y07JsW4RVZlbdK4FJZcrSKXOotsTs8/QmxkpTw2x7IHtJO9YSME0o4oxwTFZPyCa4WI4gzsVOKWITpggXJqYrO/hxKr/UmgxOzwS9C40FhFoydEiNXMuXcN1xvc6siDVPRx5Fuu2TGK1wzL6+FEJ147lbbDJpI/3rI9koAfvEfDEyPshUn7jbKael8r9+Wp8+jnZ6/ppp6YN496kAH+NaEul9SlDusjMggOXnOb+eSi273g50H2WrNKgecwkqbEqpzaJMUbprK2AwJO3YYj7gywDzai0NgCgXYHK1dFdAqdj4f1I1HOPOz4DfCnjluwlzdr3unKMaHlApXQNXfOi6zhfLZ4605E0gU/19Ff55ROCrEAOv3/QEHxtMaLRiM+Zgez2qPsDMh3ntcVXnvKCauEOovTt0WJ76QhOb/fSpUSvWPUIfgk/P7jjjcQn1YbceH91JEXaWu4E/cgKkOQZ3aqg9YdHk8FuwM/SKrhj1jUAm0bXGq7Q69pvmJzM4mhF4qWHtn80ozE5z+yG9htXk4DD1mNFXnycIDdAqUDbSuTJolqlTlWDOH9Gb9k7gmnsUrB85QiNvDdo3RKupfq1dwz7OrWx0lrqG5ESv+F2mTIdFla22MFQzhsgfJ6qE15j0aciO1236IeGttU6PdEFAw9MMyEwg==

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