coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Clear all unused local definitions

From: Joachim Breitner <mail AT joachim-breitner.de>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Clear all unused local definitions
Date: Mon, 30 Apr 2018 12:47:39 -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:BDkKyx9Jo5VF1/9uRHKM819IXTAuvvDOBiVQ1KB41O8cTK2v8tzYMVDF4r011RmVBd6ds6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7GMNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+55Pebx9UiDahfLh/MAi4oQLNu8cMnIBsMLwxyhzHontJf+RZ22ZlLk+Nkhj/+8m94odt/zxftPw9+cFAV776f7kjQrxDEDsmKWE169b1uhTFUACC+2ETUmQSkhpPHgjF8BT3VYr/vyfmquZw3jSRMMvrRr42RDui9b9mRhz1hikHKTA3/mPYisJsg6xcrx2svBN/z5LObYyPLvdyYqHQcNUHTmRBRMZRUClBD5u4YYsIFeUOIeZYr4j4p1ATsBa+HxejBOLzyj9OmHD2x7Ax3uMkEQ7c3QwgG8kDsHbTrNrvKKgSUeG1zKzRwTrYdfNZxzb96JTOch8/u/GAR69/ftTIxEQpCgjLgFKQqYn/MDOU0OQAq2qb7+16Wu2zi24nqgRxriG0ycc2lIbJh54Vylba+iVj2oo6OMO3RUhmatCnCJtdrzyWOol3T884R2xkojg2xqAItJKhYSQHxpoqyhjCYPKdaYeI+AjsVOOJLDd4mn1lfLW/ig6y8Ue+0O38U9e70E1QoipejNbMrG4N2ALJ6sedT/ty5F2t1iuR2AzL6+FEJ147lbbDJpI8wLM9l4AfvEDZEiPohUn7grWaelgq9+Wm8+jnZ6/ppp6YN496kAH+NaEul9S6AesiMwgOW3OW+ea71LL54UL5QLRKjvgvnqbCqpDVO8UbprK/AwBLyIYv8QuwACm+3NQCgXYHNE5FeA6Aj4XxJ17OJ+n4Ae6jjFSojTdk3OvLPqbhA5XINnjMiq3tfbd7605GyQo818pT55xOCuJJHPWmUUjo8dfcExURMgquwu+hBs8u+JkZXDetBaaSMKLX+XWS6+MzJeSWLNsQsTf5A/oi7vXujHp8k0UQfLWv0IFRZH3uTacuGFmQfXe52oRJKmwNpAdrFLW72m3HaiZaYjOJZ4x54zg6DIy8CoKZH9Kvh7WK3Ca+W5dMa2FaDF2WV3vlJd/dB6U8LRmKK8okqQQqEKC7QtV4hxOpvQT6yr8iJPDZ+zEeuIil2NUnv7SOxyF3ziR9CoGm60/IT2xwmTlRFT87xqVyugpmx02d3LJxhvUeGdEBv/4=

Hi,

Am Montag, den 30.04.2018, 16:20 +0000 schrieb Soegtrop, Michael:
> I don't think it is safe (in the sense that it doesn't influence the
> provability of the goal) to clear all defined variables which don't
> occur in the context otherwise. This is only true for types whose
> instances are trivial to construct. An extreme example is when you
> use evars for Props, you can end up with a defined variable with type
> False in a contradiction proof. I wouldn't throw away that one ...
> There are many more common counter examples, e.g. sumbools.

hmm, ok, I readily believe that I do not realize all the implications
of evars …

But without evars, if I have

x := e

in my context, I can always undo the effect of [clear x] with
[set x := e], right?

Would it be safe to clear all unused local definitions that do not
contain existential variables?

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