Zulip Chat Archive

Hello,
I would like to know if you plan to implement the following tactics (and how difficult it would be).

a) glob_quote t idt would take a Coq term t and an identifier (a atring) idt declares Definition idt = ... where the dots ... represents the quote of the term t (what we currently obtain when we print idt after writing MetaCoq Quote Definition idt := t

).
The tactic fails if MetaCoq is for some reason unable to reify

t```.

c) and d) glob/loc_quote type t id: the same thing, but declaring the reification of the type of t instead of t itself.

a) glob_unquote t idt would take a reified term t (i.e. t : term) and declares Definition idt = ... where the dots ...represents what we we usually obtain by doing "MetaCoq Unquote Definition idt = t. The tactic fails for instance if *Coq* is unable to infer the type of the preterm idt``.

Basically, this would allow doing meta-operations on the formulae of Coq.
For instance, we could easily write tactics that take a goal G, reifies it into G' (of type term), transform G' into H' (also of type term), then declare H, the unquote of H.
Then, since H should be a type(*), we should be able to write assert H and prove H, perhaps automatically.
Actually, the transformation from G' to H' should be a function of type term to term or using the typeprogram or global_env etc since it's seems relevant to quote the environment as well when passing from G (Coq) to G' (MetaCoq)

I would actually be interested in implementing such a tool, although I'm not quite sure to be quick enough right now :)

(*): one could also imagine creating from G' a function (which would only be definable in the metalanguage), instead of a another formula, but I fail to see in which case this would be desirable.

Yannick Forster (Oct 02 2020 at 14:54):

I tried several of the things you suggest a while ago, but unsuccessfully :) First, let me mention that there is the possibility to run template programs in tactics, so it's really just about writing the right program and then calling it in a tactic

Yannick Forster (Oct 02 2020 at 14:57):

Now the big list of "but"s: For 1 a), if I remember correctly tactics should not manipulate the global environment, and maybe even can not anymore. 1 b) should be the semantics of tmDefinition when called in a tactic. I tried to implement it, but failed. At the moment we just print an error in this case, but that should be doable with some help of a Coq developer (e.g. as project at the CUDW workshop?). 1 c) has the same issue as 1 a), 1 d) can be implemented on top of 1 b)

Yannick Forster (Oct 02 2020 at 14:59):

For 2 the main obstacle is that we currently do not treat evars properly I think. I might have a student to work on this and at least fix the support in quoting / unquoting for evars. In particular, this would then allow to define a goal type in MetaCoq, which would be very useful to write tactics in MetaCoq

Pierre Vial (Oct 02 2020 at 15:06):

Ok, thanks @Yannick Forster for the detailled answer.
I'm a bit surprised for number 2, because, when you write MetaCoq Unquote Definition, you do define a term (and Coq infers its type afterwards, right ?), so what would be the exact problem with the evars if they are handled by Coq and not Metacoq? Or there are cases of failures of MetaCoq Unquote I'm not aware of? (for me, it works just fine)

Yannick Forster (Oct 02 2020 at 15:09):

I think you can not unquote things containing evars. For instance

MetaCoq Unquote Definition test := (tLambda (nNamed "x") (tEvar 0 []) (tRel 0)).

produces Error: inspect_term: cannot recognize (tEvar 0 []) (maybe you forgot to reduce it?) (that's also not supposed to work probably, but no term that contains tEvar can ever be succesfully unquoted in any setting at the moment I think)

Pierre Vial (Oct 02 2020 at 15:29):

Yes, but in that case, I usually disable implicit argument with @. I don't know if it works in all the cases, but I would be fine with this solution for the moment :)
Anyway, that would be great to use MetaCoq the way you describe!

Yannick Forster (Oct 02 2020 at 15:31):

By mixing a bit of Ltac and MetaCoq, 1) b, d) and 2 b, d) should be easy to implement at the moment. It seems that would already help you?

Pierre Vial (Oct 02 2020 at 16:05):

Pierre Vial (Nov 30 2020 at 15:02):

Ltac quote_term_in_local_env c idn :=
  let X :=  c in
  quote_term X ltac:(fun Xast => pose Xast as idn).

Goal False.
  quote_term_in_local_env nat nat_reif.
Abort.

nat_reif := tInd
                {|
                inductive_mind := (MPfile ["Datatypes"; "Init"; "Coq"], "nat");
                inductive_ind := 0 |} [] : term
  ============================
  False

So, just to be sure, because I would like to open a pull requet: there is no an equivalent unquote_term ml function in current state of the project yet?

Stream: MetaCoq

Topic: Adding a un/quoted term (or its type) in the environment

Pierre Vial (Oct 02 2020 at 14:52):