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.

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

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

Hi @Enzo Crance I think Coq-Elpi could work fine as well, I'll make a POC for you.

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.

@Enrico Tassi Thank you for the advice, I did not know about Coq-Elpi.

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.

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

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

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

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.

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: Jul 13 2024 at 03:01 UTC