The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 06/25/2014 03:51 AM, Cedric Auger wrote:
> I cannot test here, but isn’t there any distinction on whether or not the
> term defined in section is opaque?

I tried both Qed and Defined - the results are the same.  And, yes, 
printing the proof term (which is enormous, in comparison to the proof 
script and the extracted OCaml code) does show the "mistaken" 
dependencies.  I think they may be due to use of inversion tactics. The 
type of one of the problematic section variables doesn't (and can't) 
come up at any point during the proof - so it can't be used by 
assumption or auto - but it shows up in the proof term as actual 
arguments to the many nested levels of anonymous functions that I think 
are generated by inversion.

Those nested anonymous functions in the proof term are the artifact of 
inversion automating the "convoy" pattern, correct? I am glad I am not 
doing that by hand.  I read about the convoy pattern in Adam Chlipala's 
book, and would not have attempted further use of Coq had I not found 
the inversion tactic to use in place of hand-coding convoy patterns.

-- Jonathan

> 2014-06-25 8:29 GMT+02:00 Guillaume Melquiond 
> <guillaume.melquiond AT inria.fr>
> :
>
> > 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