coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Clear all unused local definitions

From: Joachim Breitner <mail AT joachim-breitner.de>
To: coq-club AT inria.fr
Subject: [Coq-Club] Clear all unused local definitions
Date: Mon, 30 Apr 2018 11:19:49 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mail AT joachim-breitner.de; spf=Neutral smtp.mailfrom=mail AT joachim-breitner.de; spf=None smtp.helo=postmaster AT hermes.serverama.de
Ironport-phdr: 9a23:ES0yRRXOigLXFkphHP6pm8r5JFDV8LGtZVwlr6E/grcLSJyIuqrYYxOGt8tkgFKBZ4jH8fUM07OQ7/i7HzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba98IRmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KptVRTmijoINyQh/W/Ul8J+jLxVrhy9qBJ4zIHZe46VOOZkc67HZ94WWWhMU8BMXCJBGIO8aI4PAvIFM+ZftYbyu1sOrRq7BQKxGe7v0CFHhn7q3a08zeshCxzN0QslH90UsXTUqM74NKUVUe+v0KbIzTTDb/ZP1Tjm8ojHbBEhoe2KXb1ua8rd01QgGB3cg1iWtIfrMTSV1uEXvGia6eptTeCvi2k9pA5tojivx8IshpDSiYIP1F/E9Dl5wIArKt2iUkJ0fMCrHZ1NvC+ZL4t7Wt4uTmNptSogzrAKo4C3cDUExZg92hLSZfKKfo6V6Rz5TumROy13hHd9dbK/mRmy9U+gx/X8VsaqylZKqzRKksLWunAWyRPT8NaHReVn/ki73DaAzRrf5fxaLkwslKrbLYAuwqIom5YOs0nOHzX6lUHsgKOIa0kp9PKk5/npb7jovpOcMpV7igD6MqQggMy/BuE4PxALX2eB+OS80Kbu/U/+QLpQkvI2kqjZsJXDKcsAvK62HQ5V0pol6xmhFTeqyskXkmcfIFJfZB2Hl5TpO03JIP3gEfi/hE2snC53yPDCI73uGY7ALmPDkbfkZbZy8VRQyAs1zdBF5pJbEKsNIPzpWhy5iNuNBRggdgew3uzPCdNn14pYV3jcLLWeNfbwtlaD5uMqa8OWaY4JvjvnY6wg7v/qpX0+kFQdfKzs14EaaWy+E+4gL0jPMimkucsIDWpf5ll2d+ftklDXCWcCNUb3ZLo143QAMKzjCI7CQo63h7nbhXW5GZRdZmFDT1qWHHb0cYieHfsBOnjLfp1R1wccXL3kcLcPkAm0vVWjmbhgJ+HU+yhdv4ju1cRz6veVmRxgrWUpXfTY6HmESiRPpk1NRzIy2/om80xw0FKOyu5jjuZGGMZa4voPXgpobZM=

Hi,

the `clear` tactic is often not a good idea, as it may remove
assumptions that are needed to conclude the goal. But the context may
also contain local definitions (… := …), and clearing a local
definition that is no longer mentioned in the goal or any assumption is
always safe (and almost always useful).

It seems that this tactic clears all unused local definitions:

multimatch goal with [ x := _ |- _ ] => clear x end.

Would it be useful to have that as one of the clear variants?
“clearsafe” or “cleardefs” or something like this?

Cheers,
Joachim
--
Joachim Breitner

mail AT joachim-breitner.de
http://www.joachim-breitner.de/

Attachment: signature.asc
Description: This is a digitally signed message part

[Coq-Club] Clear all unused local definitions, Joachim Breitner, 04/30/2018
- RE: [Coq-Club] Clear all unused local definitions, Soegtrop, Michael, 04/30/2018
  - Re: [Coq-Club] Clear all unused local definitions, Joachim Breitner, 04/30/2018