The Coq mailing list

[Gaëtan Gilbert <gaetan.gilbert AT skyskimmer.net>]

try Parameter Inline op ... in the module type.
If that doesn't work then maybe unfolding in the tactic works:

  Ltac reifier := ...
     let opv := eval cbv [op] in op in
     match ...
     | opv ?X ?y => ...

Gaëtan Gilbert

On 22/10/2020 21:46, jonikelee AT gmail.com wrote:
> I'm trying to make a particular reflection procedure I have into an
> abstract module, and have hit a problem with its reifier. The
> problem is that the reifier, being a tactic, doesn't recognize that a
> abstract (module parameter) operation is equivalent to an instatiation
> of that operation.  The reifier is of course a tactic defined using a
> match on the abstract operation, and since the instantiation is not
> syntactically the same, it can't reify terms that use the instantiation
> operation instead of the abstract one.
>
> I mean something like:
>
> Module Type XT.
>    ...
>    Parameter op : A -> A -> Prop.
>    ...
> End XT.
> Module R(Import X: XT).
>    ....
>    Ltac reifier := ...
>       match ...
>       | op ?X ?y => ...
> End R.
> Module X <: XT.
>    ...
>    Definition op := anop.
>    ...
> End X.
> Module Import MyR := R X.
> ...
> (* attempt to call reifier on some code containing: *)
> anop a b
>
> The reifier tactic will not see that "anop" is convertible with "op",
> and so will not reify "anop a b".  It will reify "op a b", but clients
> of module R will be using "anop" instead of "op".
>
> Is there a way around this?  I am contemplating defining "op" to be
> overloaded using canonical structures.  But is there any way to make it
> work with a purely module-style abstraction?  I guess I'm looking for a
> way to make "op" be syntactically the same as "anop", as if defined by
> Notation instead of Definition.
>
> Perhaps another way is to force the reifier to notice convertibility by
> doing something like this:
>
>    Ltac reifier := ...
>      match ...
>      | ?OP ?X ?Y => unify OP op; ...
>
> But that seems like it could slow down the reifier dramatically.