The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 06/25/2014 02:29 AM, Guillaume Melquiond wrote:
> On 24/06/2014 23:53, Jonathan wrote:
>
> > Could someone describe in more detail what is supposed to go on at the
> > end of a section with regard to this dependency analysis?  I might be
> > seeing a bug, or I might just not understand what is involved in a
> > dependency according to this analysis.  Is it perhaps that some tactics
> > involved in the proof of the definition create "false" dependencies that
> > aren't really needed, but are still honored with respect to
> > end-of-section dependency analysis?
>
> As long as the hypotheses appear in the constructed proof terms, they 
> are actual dependencies. You can Print the proved theorems to see 
> where they come from. Do you happen to use any automatic tactic (auto, 
> omega, assumption, etc)? Such tactics don't try to find the minimal 
> subset of hypotheses needed for proving a goal. And even if they were 
> doing this extra work locally, that would not guarantee that the whole 
> theorem would use a minimal subset of hypotheses.
>
> Best regards,
>
> Guillaume

Yes, the set of tactics used includes various automation tactics - so it 
is not surprising that the dependencies are formed.

The other issues with section variables being discussed make it unlikely 
that using Section in the way I described (turning a goal into a 
separate definition) would work anyway.

But, if that other bug was fixed - it might be possible to create a 
Section from a goal, prove the consequent in that section as a 
definition, and then automatically one at a time delete the variables to 
see which ones can be removed without altering the proof...

-- Jonathan