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: Apr 20 2024 at 00:02 UTC