Hi everyone,

I am new to zulip so I hope I use it right :-)

I currently start to work on my master thesis where I want to work with the congruence tactic in Coq. I have seen that there is no Ltac2 version of congruence and I tried to wrap my head around defining new tactics with Ltac and Ltac2 but I'm not shure if understand it right.

My understanding is that in order to define a new Ltac tactic one has to write OCaml code and then provide a mlg file that specifies the syntax how this OCaml code is called in Proof mode or in Ltac definitions, or the tactic gets implemented in the Ltac language directly right?

In Ltac2 on the other hand it is recommended to write the tactic itself in the Ltac2 language if possible right? So if one wants to use congruence in Ltac2 it would be necessary to do one of the following:

- reimplement it in the Ltac2 language directly
- write some Ltac2 Notation that calls the Ltac version of it possibly through ltac1:(...)
- write an mlg file suitable for Ltac2 (But here I don't understand how they work and if I understand it correctly the Ltac2 Notations approach should be preferred)

Is this right and are there other ways to do this?

Do Ltac1 and Ltac2 tactics that are implemented with OCaml differ only in how they are exposed to the User? So the ml and mli files for congruence would also work for Ltac2 but at the moment there is no exposed syntax for them in Ltac2 right?

using mlg to expose ltac2 tactics is not the right way to do it

ltac2 tactics implemented in ocaml go through the "external" system: ocaml registers them with a name and ltac2 picks up the registration

eg for `progress`

ocaml side https://github.com/coq/coq/blob/f91306fb6ee06ba42d4d17ef0effd9b0efae7748/plugins/ltac2/tac2core.ml#L1149-L1151 and ltac2 side https://github.com/coq/coq/blob/f91306fb6ee06ba42d4d17ef0effd9b0efae7748/user-contrib/Ltac2/Control.v#L52 with a little wrapper notation https://github.com/coq/coq/blob/f91306fb6ee06ba42d4d17ef0effd9b0efae7748/user-contrib/Ltac2/Notations.v#L101-L103

for congruence I would do

write some Ltac2 Notation that calls the Ltac version of it possibly through ltac1:(...)

since there are no arguments so no serious interaction with the ltac2 type system

Thank you very much. That helped a lot.

There are arguments for congruence. An numeral and a list of terms. I tried

```
Local Ltac2 congruence0 (n: constr) (terms: constr) :=
ltac1:(n terms |- congruence n with terms) (Ltac1.of_constr n) (Ltac1.of_constr terms).
```

but then I get:

**Error:** `Syntax error: ')' expected after [ltac1_expr_in_env] (in [ltac2_atom]).`

I think there still is something with the Ltac2 types not right. But

```
From Ltac2 Require Import Ltac2.
Lemma foo' {A B} (f: A -> B -> A) a b: f a b = a -> f (f a b) b = a.
Fail congruence.
ltac1:(congruence 10 with true false tt).
Qed.
```

works (the arguments given to congruence make no sense, I just wanted to try if they get accepted).

it looks like the ltac1 syntax expects a literal integer for the `n`

argument ie doesn't support variables

so if you want to support it in ltac2 you do need your own external

@Gaëtan Gilbert thank you for all your help. I will try to write such an external and make a PR once I'm ready :-)

Last updated: Oct 13 2024 at 01:02 UTC