The Coq mailing list

[Randy Pollack <rap AT inf.ed.ac.uk>]

On Thu, Jul 03, 2003 at 02:17:15PM +0100, Randy Pollack wrote:
>
> Why can't we have hypothetical modules at top level?

Jacek Chrzaszcz writes (in reply):
 > 
 > Well, I think my vision of things is that everything allowed to be entered
 > in the toplevel should be "closed". It is not so right now, there are
 > axioms, but I would say that this is the way to go.
 > 
 > OK, it would be hard to impose this right now, when there are no
 > multi-file functors, but I think this is the way to go. Then we can
 > think of separate development of parts of big proofs (using
 > signatures and modules), followed by a final "linking" phase,
 > verifying that all module interfaces are implemented indeed...

I see what you're getting at, but if Axioms are natural in a type
theory without modules, aren't hypothetical modules natural in a type
theory with modules?  Surely you have hypothetical modules in the
process of typechecking functors.  So you are only arguing to prevent
users from having a natural feature of the underlying concepts.

(Here, other Coq users/theorists may have an opinion.)

 > Otherwise how do you know, that in the middle of your 150kb Coq development
 > there is no Axiom a:False, out of which you prove anything you want?

You have a tactic that examines the context and tells you any
outstanding hypotheses.  (LEGO has this tactic.)

 > On the other hand I can see no technical difficulties. So if you insist and
 > I find some time, I can add this feature.

Yes, please.

Best,
Randy