coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] automated hypothesis pruning

From: Gregory Malecha <gregory AT bedrocksystems.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] automated hypothesis pruning
Date: Thu, 29 Nov 2018 07:15:12 -0500
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=gregory AT bedrocksystems.com; spf=None smtp.mailfrom=gregory AT bedrocksystems.com; spf=None smtp.helo=postmaster AT mail-pf1-f176.google.com
Ironport-phdr: 9a23:EQHsGBcwO2zvAtr5nALNJBqflGMj4u6mDksu8pMizoh2WeGdxcu9bB7h7PlgxGXEQZ/co6odzbaO4+a4ASQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTahYr5+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v6bpgRh31hycdLzM2/2/Xhc5wgqxVoxyvugJxzJLPbY6PKPZzZLnQcc8GSWdDWMtaSixPApm7b4sKF+cPPPxYoJfyp1sJtxu/BRSnCuT1xT9MmHD5wa063P48GgzB0wwgBcwBsHvTrNXvNKYfSvu6w7fVwjXZaPNZxTT96JPIcxA6vfGDQ7dwcdHLxUYzEAPFi0ydpIr4ND2b0eQNtnKU7+tmVe+3l2EnrBtxoj6xyccojonFnJwaxU3Z9Sh/3Y07JsW4RVZlbdK4FJZcrSKXOotsTs88Xm1kpDw2xqAEtJO6eiUB1Y4pyATFa/OddoiF+hLjW/iVITd/nH9lfaiwhxe28US50u38WNS43E9EriZYkNTBt2oB1xPU6siARft9+lmu1SyT2ADU7+FIOUE0lazFJJ492rM8iIYfvEDZEiL1mEj6lrGaelg49uSy9ujqYLTrqoeZN4BuiwH+Nqoumta4AeQ9KgUOUHKb9vqz1L3k5034QK5HgeYonabEqpDaItgUpq2iAw5VyYYj9wiwDzK90NgCgXYHK1dFdAqdj4f1I1HOPOz4DfCnjluwlzdr3unKMaHlApXQNXfOi6zhfLZ4605E0gU/19Ff55ROCrEAOv3/QEHxtMaLRiM+Zgez2qPsDMh3/oIYQ2OGRKGDY43ItlrdyfgiLO6WdccwsTLwIPgsr6rhl3I2nkUMVaOk0YEQY3OjD+96LkCCJ3Hrh4FSQi8xogMiQbmy2xW5WjlJaiPqBvNu1nQAEIujSLz7aMWoib2F0j28G8cONGpLBkqLGnTzZp6YVvIXLimVJ505y2BWZf2aU4YkkCqWmkri0bM9drje9yECspngz8lu++DWjlc58jkmV53AgVHIdHl9myYzfxFz3K17phYjmFKK0Kw9m/IBUNIKuK0PXQA9OprRied9DoKqVw==

I'm not aware of any work on this, but looking at the proof term it shouldn't be too difficult to compute these. Just do a dead variable/code elimination in the proof term and you should have your answer. Matching that back up to the tactic script might take some work though.

On Wed, Nov 28, 2018, 9:32 PM Abhishek Anand <abhishek.anand.iitg AT gmail.com wrote:

Has someone worked on a tool which when given a finished proof, can try to prune (`clear`) as many hypotheses as early as possible during the proof?
--
-- Abhishek
http://www.cs.cornell.edu/~aa755/

[Coq-Club] automated hypothesis pruning, Abhishek Anand, 11/29/2018
- Re: [Coq-Club] automated hypothesis pruning, Gregory Malecha, 11/29/2018
  - Re: [Coq-Club] automated hypothesis pruning, Pierre Courtieu, 11/29/2018