Modern term reification library? (replacement for Quote) · Coq users

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...)

Kazuhiko Sakaguchi (May 15 2024 at 14:48):

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).

William Spencer (May 15 2024 at 15:12):

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.

Kazuhiko Sakaguchi (May 15 2024 at 15:18):

Kazuhiko Sakaguchi (May 15 2024 at 15:24):

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.

Enrico Tassi (May 15 2024 at 15:25):

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.

Kazuhiko Sakaguchi (May 15 2024 at 15:29):

Enrico Tassi (May 15 2024 at 17:17):

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.

Joomy Korkut (May 15 2024 at 19:13):

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.

Stream: Coq users

Topic: Modern term reification library? (replacement for Quote)

William Spencer (May 15 2024 at 14:33):