The Coq mailing list

["jonikelee AT gmail.com" <jonikelee AT gmail.com>]

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.