The Coq mailing list

[Pierre-Marie P�drot <pierremarie.pedrot AT ens-lyon.fr>]

Dear Coq users,

I am currently facing a quite serious problem by trying to mix modules
with reflexive tactics.

Actually, I would like to use modules in order to:

1. Have a nice abstract layer for proof and hide the implementation in
further proofs;

2. Prevent cluttering of the namespace with irrelevant intermediary lemmas.

That means, I do use declarations

Module X : T := ...

and NOT

Module X <: T := ....

Yet at the same time, I would like to be able to build up reflexive
tactics operating on the contents of the module. Alas, it does not work
precisely because of the opaque nature of the content of the module
(which is something I want...). I have tested a lot of combinations, and
they are all more or less flawed.

1. What does not work:

Defining reflexive tactics in the module body: they are not exported.

Defining reflexive tactics in the module type, instead of in the module
body; terms are still opaque, so it does not reduce. (Maybe one day when
we have abstract tactics in module types?)

2. What does partly work:

Do not use either abstraction of reflexivity: relatively useless...

Mix computational reflexivity with ltac rewriting: hell on earth (slow,
unsecure, unmaintainable).

And the best I came with, which is in my opinion an UGLY hack, by doing
as follows:

Module X <: T :=

(* definitions *) ...

(* HACK-a-tron *)

Global Opaque ... all_transparent_defs ...

End X.

Module Tactics. Import X.

Transparent ... relevant_defs ...

(* tactics *) ...

End Tactics.

This is not totally satisfactory because while partially abstracting
definitions, we still have a cluttered namespace.

3. What should work:

Have a semi-transparent flag stating that this term is transparent for
reduction but not for unfolding in proofs (I don't think this is possible).

Have a way to define in-module abstract tactics that can work on the
transparent term while hiding the inner parts of the module.

...

So did you encounter this problem, and did you find a partial workaround
(I assume there is no way to do so)? Actually, the more I use the module
system, the more I find it useless because while providing a VITAL way
to abstract things, it does conflict with a lot of other parts of Coq.

PMP

Attachment: signature.asc
Description: OpenPGP digital signature