The Coq mailing list

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

Thanks - "repeat fold op" works, but "Parameter Inline" does not.
Furthermore "repeat fold op" only works if op is not defined using
"Parameter Inline".


On Thu, 22 Oct 2020 16:01:42 -0400
Joshua Gancher <jrg358 AT cornell.edu> wrote:

> For this simple example, you can also fold the op:
> 
> Ltac reify :=
>   repeat fold op; match goal with
>   | [ |- op _ _ ] => ..
>   end.
> 
> I am not sure if it is better to fold anop into op or unfold op into
> anop, however.
> 
> On Thu, Oct 22, 2020 at 3:57 PM Gaëtan Gilbert <
> gaetan.gilbert AT skyskimmer.net> wrote:  
> 
> > 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.
> > >  
> >