## Stream: Coq users

### Topic: ltac : intros followed by exists (beginner question)

#### Pierre Vial (Dec 10 2020 at 09:31):

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?

#### Théo Winterhalter (Dec 10 2020 at 09:34):

Again, use `lazymatch` if you want the real error message.

#### Théo Winterhalter (Dec 10 2020 at 09:37):

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

#### Théo Winterhalter (Dec 10 2020 at 09:41):

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

#### Pierre Vial (Dec 10 2020 at 09:51):

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

#### Théo Winterhalter (Dec 10 2020 at 09:52):

My tactic does

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

isn't that what you want?

#### Théo Winterhalter (Dec 10 2020 at 09:53):

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

#### Pierre Vial (Dec 10 2020 at 10:17):

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

#### Théo Winterhalter (Dec 10 2020 at 10:20):

Ah now I see what's wrong.

#### Théo Winterhalter (Dec 10 2020 at 10:20):

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

#### Théo Winterhalter (Dec 10 2020 at 10:21):

But since you do the `intro`after all the `fresh`, `x` is always fresh, so you get three times `x`.

#### Pierre Vial (Dec 10 2020 at 10:24):

Huh, I guess that's because the ltac `let in` is not a real `let in`

#### Théo Winterhalter (Dec 10 2020 at 10:33):

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