Enzo Crance (Nov 30 2020 at 16:41): Enzo Crance (Nov 30 2020 at 16:41):Hello everyone. I am here to ask the question as to whether MetaCoq is a good choice of meta-language for what I am planning to develop. One of the tasks I want to complete is a contribution to SMTCoq, a Coq library that connects the proof assistant to SMT solvers.
I would like to write a new preprocessing tactic, inspired by other existing tools. This operates on goals at a meta level, though I do not know which meta-language is the best pick for this purpose (MetaCoq, Ltac2, Mtac2, etc). Maybe I can get some advice from you. I can illustrate my needs with an example of Coq goal.
Goal forall (x y : int) (n : nat) (t v : T) (f : int -> nat) (g : T -> nat),
(forall (u : T), g u = g v) -> f (x + y) + S (S n) + g t = 2 + f (y + x) + g v + n.
Here the goal contains uninterpreted functions f and g, various variables in integer types that are user-defined (like int) or "built-in" (like nat), constants such as 2, constructors like S, a universal quantifier, an unknown type T, as well as an implication and equalities expressed in Prop.
I would like to make all the integer types converge to Z and the logic to boolean operators, whenever it is possible, going under uninterpreted functions and quantifiers. Here is what I want the output to look like after preprocessing the previous goal:
(forall (u : T), Z.eqb (g' u) (g' v) = true) ->
Z.eqb (f' (x' + y') + (n' + 2) + g' t)%Z (2 + f' (y' + x') + g' v + n')%Z = true
with
f' : Z -> Z
g' : T -> Z
x' y' n' : Z
and some constraints on the previously nat values (like 0 <= n') in the hypotheses, as nat is not in bijection with Z, so that we do not lose information. The user will have to declare some knowledge about the types, functions, binary relations, etc. This idea is similar to the work done by Frédéric Besson in the zify tactic. The difference is that the knowledge is at the meta level too. Indeed, note that the two stacked S constructors have been processed into + 2. We need to allow the user to define specific behaviours for each known constructor, thus probably a struct with a field containing a meta function operating on the proof state (a "tactic").
Thanks for reading so far. Do you think MetaCoq is a good option for such a job, or should I use a particular alternative for my needs? I look forward to reading your answers and pieces of advice.
Pierre Vial (Dec 01 2020 at 09:56):Hello Enzo,
My two cents on this issue. If I'm not wrong, SMTcoq should soon most convert most implementations of Z into the native integers.
However, in the particular case of nat, if you want to pass the information that 0 <= n, this is possible with MetaCoq: you may write (in MetaCoq) that scans your goal, check whether the type nat appears in it (such a thing is not possible if you are not on the meta-level).
Then, it seems to me that you have several possibilities:
1) using a coq tactic or library, you just assert that 0 <= n in the local context for any nat variable that you meet (not need to be on the metalevel anymore I think). But I guess this possibility is too simple, since you may have quantified nat variables inside complicated statements
2) you translate your initial Coq goal G into a new one G' where every quantification on nat has been transformed appropriately. That is, forall (n : nat), foo should be transformed into something like forall (n: Z), 0 <= n -> fooand exists (n : nat), foo into exists (n : Z), 0 <= n /\ foo.
The transformation from G to G' should be written in the metalangague. However, you would also need a proof in Coq (produced by a tactic for instance) that G' *implies G, and I think that this proof/tactic should be easy to write in Coq (not on the meta-level) I think.
3) More generally, if you need to feed SMTCoq with some ad hoc information on some types, you can proceed this way.
Thus, yes, MetaCoq is a good meta-language to do some of the things you describe. Theoretically, you can write all the meta-things directly in OCaml but you should ask an expert whether this would improve performance that much. I think it more convenient to work with MetaCoq: it is quicker and easier to see whether your code works or not.
In the case of nat, you should also try to see whether there is already a tactic which eliminates nat into Z in Coq goals.
Enrico Tassi (Dec 01 2020 at 10:04):Hi @Enzo Crance I think Coq-Elpi could work fine as well, I'll make a POC for you.
Enzo Crance (Dec 01 2020 at 10:21):Thanks @Pierre Vial. About OCaml, I had it on my list too, but it is also probably much harder to implement the procedure in OCaml than in MetaCoq.
Enzo Crance (Dec 01 2020 at 10:26):@Enrico Tassi Thank you for the advice, I did not know about Coq-Elpi.
Enrico Tassi (Dec 01 2020 at 10:27):To get a flavor of it, you can find a few example here https://github.com/LPCIC/coq-elpi/ . When I'll have a proof of concept "zify" in elpi, I'll add it there among the other examples and ping you.
Kazuhiko Sakaguchi (Dec 01 2020 at 10:45):@Enrico Tassi FTR, my idea to make it possible to apply zify for MathComp was inspired by ssrmatching (indexing Z-ification rules by head symbols such as addn and GRing.add, but then match them using conversion to support overloaded operators). So it would be really nice if you reimplement this in Coq-Elpi.
Enrico Tassi (Dec 01 2020 at 13:10):@Enzo Crance this is my POC. It may be too simplistic... comments are welcome on the PR: https://github.com/LPCIC/coq-elpi/pull/199
@Kazuhiko Sakaguchi I don't know how the current zify is coded, so maybe my POC is also pointing in the wrong direction. If so, please comment.
Enzo Crance (Dec 01 2020 at 13:36):@Enrico Tassi I am trying to know whether Coq-Elpi suits my needs. I would like to ask you a few more questions that are specific to the tool, but this goes beyond the scope of the MetaCoq stream, so I will probably switch to the Elpi stream.
Matthieu Sozeau (Dec 03 2020 at 13:16):For the record, I think like Pierre that both Coq-elpi and MetaCoq would fit (assuming you can prove the equivalence of the original and translated goal using some tactic). It will probably be faster to prototype in Coq-elpi, and I don't know if performance-wise there would be a big difference between the two. It would have to be benchmarked.
Enzo Crance (Dec 03 2020 at 16:10):Thanks for your opinion. Performance will definitely be a parameter for the final state of my work, but at the moment this is more about ease of use and checking the meta-languages are powerful enough for my needs, which should be the case. I will probably try both and work in an incremental mode.
Last updated: Apr 18 2024 at 17:02 UTC