Hi all,

I would like to have a tactic (my_tactic) that returns 0 if there is an existential variable in LHS, 1 if in RHS, and 2 if in both.

For instance, the below program should print "Left" and then "Right".

```
Goal exists (a: unit), a = tt.
eexists.
let tmp := my_tactic in
match tmp with | 0 => idtac "Left" | 1 => idtac "Right" | 2 => idtac "Both" end.
symmetry.
let tmp := my_tactic in
match tmp with | 0 => idtac "Left" | 1 => idtac "Right" | 2 => idtac "Both" end.
Qed.
```

Is there a way to do this?

Thanks!

Hi Youngju,

the following tactic should do the trick:

```
Ltac my_tactic :=
match goal with
| |- ?a = ?b => let _ := match a with | _ => has_evar a end in
let _ := match a with | _ => has_evar b end in constr:(2)
| |- ?a = ?b => let _ := match a with | _ => has_evar a end in constr:(0)
| |- ?a = ?b => let _ := match a with | _ => has_evar b end in constr:(1)
end.
Goal exists (a1 a2: unit), a1 = tt ∧ a2 = a2.
eexists _, _.
split.
- let tmp := my_tactic in
match tmp with | 0 => idtac "Left" | 1 => idtac "Right" | 2 => idtac "Both" end. (* Left *)
symmetry.
let tmp := my_tactic in
match tmp with | 0 => idtac "Left" | 1 => idtac "Right" | 2 => idtac "Both" end. (* Right *)
reflexivity.
- let tmp := my_tactic in
match tmp with | 0 => idtac "Left" | 1 => idtac "Right" | 2 => idtac "Both" end. (* Both *)
Abort.
```

This uses the trick that Jason explained here: https://stackoverflow.com/questions/45949064/check-for-evars-in-a-tactic-that-returns-a-value/46178884#46178884

Thanks a lot for your answer, @MackieLoeffel!

That `has_evar`

keyword is exactly the one I was looking for.

Also, the trick you used to change tactic success/failure into constr is very helpful.

Last updated: Jun 23 2024 at 23:01 UTC