## 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_existsuch 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 intros 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 introafter 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