coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] automated hypothesis pruning

From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: [Coq-Club] automated hypothesis pruning
Date: Wed, 28 Nov 2018 18:32:37 -0800
Authentication-results: mail2-smtp-roc.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-yb1-f173.google.com
Ironport-phdr: 9a23:eHCQqBC0El5ZTI04QTRQUyQJP3N1i/DPJgcQr6AfoPdwSPvyoMbcNUDSrc9gkEXOFd2Cra4c26yO6+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglUhzexe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Xymp4aV2Rx/ykCoIOD43/m/UhMJtkqxUvAmsqAZjz4POeoyZKOZyc6HbcNgHRWRBRMFRVylZD46gdIQPD+sBPf1Yr4bjpFsFsAezBQ+2C+Pp1zBDm3j70rch3OQhEAHGxwwgEMwNsHjOttr1Mr0dUeaow6XSzDXDbu9W2Tjm5YjHdxAuu/CMXbZqfcXNzkkvEhrIg1ONooLrODOV0/4Cs2md7+d4Se2vjHQnqwdvrTirwscgkJfGiZ8Iyl3C6C53w541KMWmREJnZdOoCphduiGAO4doX88vR3tktDs4x7AIv5OwYTIEx449xxHFbvyKa4iI7QznVOaWOTp4gWhqeLO7hxqr8Umv0fDwWtC60FpXrCdInMPAtn8K1xzU5ciHTuVy8l291jaI0gDf8uBEIUYqmqrHM5Mt3KI8m54JvUnAHiL6glv6gLKSe0k+5+Sl6erqbq3jppCGNo90jg/+Mr4pmsy6Gek3KBMBX2ia+eSn1L3s4075TK9Qgf0wiKbZto3VKd4apq64Hw9V3Z0u6xm6Dzi80dQYmWMLI05CeBKCl4TpIU3BIOjkDfejhFShiCtkx/ffPrH4HprNKmXDn6z6cLZm609czRIzwspF65JVDLEBOvPzVVXruNzWFB9qezCzlu3gEZB20p4UETaEBbbcO6fPu3eJ4PguKq+CftlGliz6Lq0M7f7vln80mhc0e6Cv0dNDYXq4H+9mLkbfaHzlhNtHEGYWsSIxSeXrjBuJVjsFNCX6ZL41+jxuUNHuNozEXI342OXQjhf+JYVfYyV9Mn7JFH7pc4ueXPJVMXCdJ8ZglnoPUr3zEtZ9hyHrjxfzzv9cFsSR4jcR7Mux29185umVnhY3p2QtUpatllqVRmQxpVsmAj872Kcl/x54w1aHlLly2rlWTIMIofxOVQg+ONjXyOkoU90=

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