## Stream: Coq users

### Topic: Ltac to check if a term is existential or not

#### YoungJu Song (Mar 01 2021 at 11:59):

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!

#### MackieLoeffel (Mar 02 2021 at 07:28):

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

#### YoungJu Song (Mar 04 2021 at 10:32):

That `has_evar` keyword is exactly the one I was looking for.