Stream: Coq users

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


view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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: Feb 08 2023 at 22:03 UTC