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.
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
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)
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
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)
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)
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!
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?
Actually, it would!
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?
I think you're right
Last updated: Feb 09 2023 at 03:06 UTC