Hello,

I'm trying to implement a (very simple tactic) `intros_exist`

such that `intros_exist n`

(with `n : nat`

) is equivalent to:

`intro x1 ; intro x2 ; ... ; intro xn ; exists x1 ; ... ; exists xn`

where `x1`

, ... `xn`

are fresh ident generated by Coq.

Here is a first approximation of this tactic:

```
Ltac intros_exist_aux n i0 e0 :=
match n with
| O => idtac "match 0" ; i0 (* this line should be | O => i0 ; e0 *)
| S ?n => let x := fresh "x" in let i1 := (intro x ; idtac "let i1 :=" ; i0) in let e1 := (exists x ; idtac "let i2 :=" ; e0) in let i2 := intros_exist_aux n i1 e1 in i2
end.
```

Basically, I'm trying to store the `intro`

s in i0 and the `exists`

in e0. Right now, in the base case, I just drop `e0`

, because, as seen below, I have an error before I can reach that and begin the `exists`

sequence. With the above code, if I write:

```
Goal forall (n m k: nat), exists (x y z: nat), x = n /\ y = m /\ z = k .
Proof.
intros_exist_aux 1 ltac:(idtac "foo") ltac:(idtac "bar").
intros_exist_aux 1 ltac:(idtac "foo") ltac:(idtac "bar").
```

every thing goes fines: I obtain two new variables `x, x0 : nat`

in the goal `forall k : nat, exists x1 y z : nat, x1 = x /\ y = x0 /\ z = k`

as expected.

However, if I replace, the two `intros_exist 1 ...`

with (one) `intros_exist_aux 2 ltac:(idtac "foo") ltac:(idtac "bar")`

which should do the same job, I get the following error:

`Error: No matching clauses for match`

Thus, the tactic does not seem currently able to store more than one recursive call. What is going wrong with the match?

Again, use `lazymatch`

if you want the real error message.

But basically you are giving a continuation that you are building as you intro right.

Then I think we can do simpler just like this:

```
Ltac foo n e :=
lazymatch n with
| 0 => e
| S ?n =>
let h := fresh "x" in
intro h ;
let e' := e ; exists h in
foo n e'
end.
Ltac bar n :=
let e := idtac "ok" in
foo n e.
```

`lazymatch`

is indeed more precise and tells me that `x is already used`

.

However, I cannot quite adapt your syntax, because as you do it, you will have the `exist`

in the reverse order as the one I'm expecting.

Still, I'm a bit surprised by the error I get: shouldn't ltac be able to handle alpha-conversion of bound variables on its own, or I'm missing something?

My tactic does

```
intro x ; intro y ; intro z ; exist x ; exist y ; exist z
```

isn't that what you want?

It's indeed weird that a variable gets bound twice since you are using `fresh`

…

Mmh, yes, you are totally right! Still, I would like to undersand why there is a problem

Ah now I see what's wrong.

What you are doing is `fresh ; fresh ; fresh ; intro ; intro ; intro ; exist ; exist ; exsit`

.

But since you do the `intro`

after all the `fresh`

, `x`

is always fresh, so you get three times `x`

.

Huh, I guess that's because the ltac `let in`

is not a real `let in`

Well I'm not sure because this works:

```
let x := fresh "x" in
let y := fresh "x" in
intros x y.
```

so it might be some sort of weird evaluation thing.

Last updated: Jan 29 2023 at 03:28 UTC