The Coq mailing list

[Damien Pous <Damien.Pous AT inria.fr>]

We have got exactly the same problem in our ATBR library...
We found no solution yet, except using functors everywhere, which is
impractical.

Damien (and think Thomas would agree...)


Le 7 juillet 2010 08:51, Pierre-Marie Pédrot
<pierremarie.pedrot AT ens-lyon.fr>
 a écrit :
> 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
>
>