I'm working on a project which will require term reification similar to that of the `ring`

tactic. In looking online, I came across the old `quote`

library, which seems like it might be able to help, though it's deprecated. Is there a currently-supported library that provides similar tactics for reification?

I saw in an old github thread the recommendation to use template-coq (I suppose now MetaCoq?). I looked at that briefly, but couldn't figure out where to start, so if that's the answer, I'd appreciate direction as to how to begin. (Specifically, I want to reify terms to a particular inductive type, as in CPDT's Reflection chapter, not reify coq terms in general... though to be honest I'm not so sure what the latter does / doesn't do.)

For bonus points, I'd like advice on the following: I'll also need to reify with respect to typeclass instance fields, i.e. the term reification will depend on definitions within a typeclass instance. I can add specifics if helpful, but it's broadly similar to how `ring`

needs to reify with respect to user-defined addition and multiplication functions, but more parametrized. (Specifically, I'm reifying terms in a monoidal category, so similar to `ring`

with two binary operations such that 1) each operation is parametrized by object and 2) we have certain "constants", also parametrized by constants [these are the associator and unitors]. Much of my concern / difficulty with just bodging this together in Ltac is because the ways I've found to deal with the typeclass side of things are all very hacky: for example, to iterate over all declared typeclass instances in context, I have to pose them as hypotheses to the context, then revert all of them, then repeatedly introduce them...)

In my experience, Coq-Elpi allows me to concisely write a reification procedure. My ITP'22 paper explains how to implement a ring tactic that supports overloaded algebraic operators (but we use canonical structures rather than type classes).

That looks promising, thank you! Did you find that the quotation was robust, or did it run into issues? For instance, would it be able to reify `Z.plus 1 2`

by unifying `Z.plus`

with a canonical `GRing.add`

instance?

Also, do you foresee an issue with adapting this type of method to work with parametrized objects and operators? I don't have an intuition for how strong the unification in this Elpi script is.

The actual reification *rules* for addition look like this. Our discipline is to have one rule for each constant (like `GRing.add`

, `addn`

, `N.add`

, and `Z.add`

) to avoid performance issues: https://github.com/math-comp/algebra-tactics/blob/9308c54787b246ed3310940fe9710dc6b2a6cb87/theories/common.elpi#L400-L425

Well, that's probably the difference between canonical structures (packed classes) and unbundled type classes. In MathComp, the addition of a ring, in principle, should always appear as `GRing.add`

. But, that would not be the case in unbundled type classes. You can still write a program in Elpi that translates type class instances to reification rules, but that's quite an advanced use of Coq-Elpi.

William Spencer said:

Also, do you foresee an issue with adapting this type of method to work with parametrized objects and operators? I don't have an intuition for how strong the unification in this Elpi script is.

The unification of the programming language Elpi honors alpha-equivalence for Coq terms, nothing more.

But Coq-Elpi comes with many APIs, including `coq.unify-eq`

, that is the unification of Coq.

Yes, and we extensively use `coq.unify-eq`

in Algebra Tactics.

About type classes, you do have APIs to crawl instances in Elpi, or you can also call the elaborator to see if it can find an instance on a given search key.

Since you said you couldn't figure out where to start with MetaCoq, here's an interpretation of the reflection chapter from CPDT using MetaCoq:

```
Require Import List.
Import ListNotations.
Require Import MetaCoq.Template.All.
Import MCMonadNotation.
Inductive taut : Set :=
| TautTrue : taut
| TautAnd : taut -> taut -> taut
| TautOr : taut -> taut -> taut
| TautImp : taut -> taut -> taut.
Fixpoint tautReify (t : term) : TemplateMonad taut :=
match t with
| tInd {| inductive_mind := (MPfile _, "True"%bs); inductive_ind := _ |} _ =>
ret TautTrue
| tProd _ a b =>
a' <- tautReify a ;;
b' <- tautReify b ;;
ret (TautImp a' b')
| tApp (tInd {| inductive_mind := (MPfile _, "and"%bs); inductive_ind := _ |} _) [a ; b] =>
a' <- tautReify a ;;
b' <- tautReify b ;;
ret (TautAnd a' b')
| tApp (tInd {| inductive_mind := (MPfile _, "or"%bs); inductive_ind := _ |} _) [a ; b] =>
a' <- tautReify a ;;
b' <- tautReify b ;;
ret (TautOr a' b')
| _ => tmFail "No match for term"%bs
end.
Fixpoint tautDenote (t : taut) : Prop :=
match t with
| TautTrue => True
| TautAnd t1 t2 => tautDenote t1 /\ tautDenote t2
| TautOr t1 t2 => tautDenote t1 \/ tautDenote t2
| TautImp t1 t2 => tautDenote t1 -> tautDenote t2
end.
Theorem tautTrue : forall t, tautDenote t.
induction t; simpl; intuition.
Qed.
Ltac obvious :=
match goal with
| [ |- ?P ] => run_template_program (tmQuote P >>= tmEval all >>= tautReify)
(fun p => exact (tautTrue p))
end.
Goal True /\ (True \/ True).
obvious.
Qed.
```

You can look at the definition of `TemplateMonad`

to see what other actions are available to you (though the ones that create definitions won't run in a tactic). If you need to looks up type class instances, `tmInferInstance`

might be particularly helpful.

Last updated: Jun 23 2024 at 05:02 UTC