Discussion:
automated hypothesis pruning
(too old to reply)
Abhishek Anand
2018-11-29 02:32:37 UTC
Permalink
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/
Gregory Malecha
2018-11-29 12:15:12 UTC
Permalink
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.
Post by Abhishek Anand
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/
Pierre Courtieu
2018-11-29 16:54:26 UTC
Permalink
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

Loading...