coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: "Soegtrop, Michael" <michael.soegtrop AT intel.com>
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: RE: [Coq-Club] Clear all unused local definitions
Date: Mon, 30 Apr 2018 16:20:07 +0000
Accept-language: de-DE, en-US
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=michael.soegtrop AT intel.com; spf=Pass smtp.mailfrom=michael.soegtrop AT intel.com; spf=None smtp.helo=postmaster AT mga06.intel.com
Dlp-product: dlpe-windows
Dlp-reaction: no-action
Dlp-version: 11.0.200.100
Ironport-phdr: 9a23:CY9lcBWVgrC+YFrZnoSMfRI3k8vV8LGtZVwlr6E/grcLSJyIuqrYbBGFt8tkgFKBZ4jH8fUM07OQ7/i7HzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjWwba98IRmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KptVRTmijoINyQh/W/XlMJ+kb5brhyiqRxxwYHUYZ2aO/VxcK7GYdMVXm5MUtpNWyBdAI6xaZYEAeobPeZfqonwv1UCowa5BQayC+Pv1iVIhnju3aEizu8vFgDG0xAgH90UrnvUqNv5P7oVXOCwzanH0TXDYOlI1jf58oTIaRchru+DXbJsa8rRzlEvGhjEjlWWtYzqITeV2v4RvGic6uptTOSigHMppQF2pzig3MYsio/Ri4IUzFDE6Tt2wIIvKdKlVkF2Z8OvHphItyyCKod7TMwvT3t1tCs0xbAKo4O3cSYLxZg9yRPTduSLf5WJ7x/tTuqcLzl1iGh7dL+xgxu+61Wsx+7hWsWszVpHry5InsPSun0N2BHf8NaLRuFj8kqu3TuC0R3Y5PteLkAuj6XbLoYswr4umZoXtkTOBir2mErsg6OKd0go4Omo6+L7Yrr4op+QLZN7igb7Mqg2m8y/B/o3MhQWUmSG9+mx26fv8VD3TbhFlPE6j6fUvZHAKckVu6K1GwpV3Zwi6xa7ATemytMYnXwfIVJAeRKIk4jpNEvQL/D8F/u/mFOsnylkx/DaJL3hBY3NI2PCkLfnYbZy9UpcxBAvwtBY4pJYEqsBL+7rWk/tqNzYCQc0PBCzw+b+EdlyyoceWX+UDaKCK6PTsVqI5vo1LOWWZY8Vviz9K/k/6PL0g385gwxVQa78l5AQcTWzGulsC0Sfe3vlxNkbWy9etQ0nCefulVeqUDhJZn/0UbhqtR8hD4fzR7zES4+xmruZmG+eH5ZWb21CQBjYFHbjd4yJX7EXby+dPtVmihQFU6SsT8kq0hT451yy8KZuMueBon5QjpnkztUgv7SCxyF3ziR9CoGm60/ISmh1mm0SQDpvhfJ+p1BwzhGI1q0q2qUER+wW3OtAV0IBDbCZ1/ZzUomgWwTdc9PPQ1GjEI3/XGMBC+kpytpLWH5TXtWviheagHivDLZNyfqKAoA59uTX2H2jf8s=

Dear Joachim,

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.

So I wouldn't call it "clearsafe".

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928

[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