YoungJu Song (Mar 01 2021 at 11:59): 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):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: Oct 03 2023 at 19:01 UTC