Stream: MetaCoq

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


view this post on Zulip Pierre Vial (Oct 02 2020 at 14:52):

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

1) Quote tactics:

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

b) loc_quote t idt the same thing, but declaring idt in the local environment

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.

2) Unquote tactics

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

b) local version

c) and d): same thing, but with the infered type of 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 gave an example of possible application related to SMTSolver in https://coq.zulipchat.com/#narrow/stream/237658-MetaCoq/topic/Proving.20a.20reified.20proposition.20with.20Program/near/211615565 where we would like to do exactly this.

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.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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)

view this post on Zulip 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!

view this post on Zulip 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?

view this post on Zulip Pierre Vial (Oct 02 2020 at 16:05):

Actually, it would!

view this post on Zulip Pierre Vial (Nov 30 2020 at 15:02):

A late follow-up.
We have this nice quoting function in
https://github.com/MetaCoq/metacoq/blob/a23b7c9e8aa2735f2209059b7594beb1f7a939b2/template-coq/src/quoter.ml#L369
I may thus write such a function quote_term_in_local_env below, which just adds in the local environment the reification of a Coq term c with the identifier idn:

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.

which gives me:

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?

view this post on Zulip Matthieu Sozeau (Nov 30 2020 at 15:44):

I think you're right


Last updated: Aug 11 2022 at 03:02 UTC