coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] automated hypothesis pruning

From: Pierre Courtieu <pierre.courtieu AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] automated hypothesis pruning
Date: Thu, 29 Nov 2018 17:54:26 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=pierre.courtieu AT gmail.com; spf=Pass smtp.mailfrom=pierre.courtieu AT gmail.com; spf=None smtp.helo=postmaster AT mail-oi1-f169.google.com
Ironport-phdr: 9a23:r8U2ABM1UxhzSf0qaAUl6mtUPXoX/o7sNwtQ0KIMzox0LfT+rarrMEGX3/hxlliBBdydt6oUzbKO+4nbGkU4qa6bt34DdJEeHzQksu4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1Ov71GonPhMiryuy+4ZLebxlLiTanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPdeRWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbYUwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0vRz+s87lkRwPpiCcfNj427mfXitBrjKlGpB6tvgFzz5LIbI2QMvd1Y6HTcs4ARWdZUclRWS5ODIOyYYUMEuQPI/pXopLhp1cStxayGRWgCP/txzJOm3T43bc60+MkEQzexgIgHswBsG7OrNrrKawfT+e1zLTSzTXfbvNZxyr945XPfxA5oPGDQ6hwcdDPxkU1CwzFiUiQqZb5PzOUyOsNrnOW7+VlVe21im4nrxt9rSSoxscpk4TEgJ8exFPc9Shh3oo5Odm1RFR4bNOkCpdcqiCXOolsTs8/QmxlvCA3waAct5GhZigF0pEnygbfa/OZd4iI5QruVOOLLjd5gHJpYbW/hxev/US5xO3wS8i53VJQoipKldnMsX8N1xjN5cSdVvR9+UKh1S6O1wDV9O5EPVg5mbTHJ5Ml2LI9lZoevV7eEiL3mkj6lrKae0Qg9+Sw7uToeLTmppuSN49ujQH+N7wjmtS+AesmKAgORXaU9f6g273k4E35WqlKjvwonanEq53aKsEbqbS4Aw9RyIos9xG/DzK+3NQCgXYHNE5FeA6Aj4XxJ17OJ+n4Ae6jjFSojTdk3OvLPqbhA5XINnjMiq3tfbd7605GyQo818pT55xOCuJJHPWmcUjo/PfcExVxZwez2qPsDMh3/oIYQ2OGRKGDZvD8q1iNs9ouLvOWacc+vyvnN/ko+ra6lX40g0UQO6KuwIELaX2lNvtjKkSdJ3Hrh4FSQi8xogMiQbmy2xW5WjlJaiP3Bvpkv2BpOMedFY7GA7uVrvmE1Sa/EIdRYzkfWF+JGHbsMY6DXqVVMX7AEopaijUBEIOZZco5zxj37V31zrNmKqzf/ShK7cu+hugw3PXakFQJzRIxD8mZ1DvTHWR9n2dNQD5vma4m/x07xVCE3qx1xfdfEI4L6g==

You can simulate this by using the section mechanism: open a section,
declare all hypothesis as "Hypothesis" or parameters, prove your lemma
foo and close the section. Only used hypothesis will be quantified in
foo.

Hope this helps.

P

[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