I'm trying to implement a (very simple tactic)
intros_exist n (with
n : nat) is equivalent to:
intro x1 ; intro x2 ; ... ; intro xn ; exists x1 ; ... ; exists xn
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?
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
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
introafter all the
x is always fresh, so you get three times
Huh, I guess that's because the ltac
let in is not a real
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: Oct 04 2023 at 23:01 UTC