5

I am considering writing tactics which will look at multiple goals and make decision based on that. However, when I use match goal with and stare at a goal, how do I say "please find another goal that looks like this"?

Or rather, a more general question is, how can I switch between goals in Ltac?

Jason Hu
  • 6,239
  • 1
  • 20
  • 41
  • Can you maybe give a minimal example where you would like to "switch" goals? After using a tactic like `destruct ..` or `induction ...` you usually see all the goals that are available and can focus them using `Focus n` for the nth goal. – Heiko Becker Apr 11 '18 at 14:25
  • @nesreka one straightforward case is, when you do `dependent induction` on certain term, the inductive hypothesis might generate a `_ = _` condition, which pretty much constraints what the term should be. after `eapply` the hypothesis, there isn't too many choice left due to this if it generates an existential var, while `auto/eauto` are not smart enough to figure this out. – Jason Hu Apr 11 '18 at 20:22
  • Would tacticals like `all:` then maybe be sufficient? After doing `dependent induction` you could run `; subst` to get rid of the equalities in all your subgoals. There is more than the `all:` tactical which are defined in https://coq.inria.fr/distrib/current/refman/ltac.html#sec469 Let me know if this is an appropriate answer for you and I will convert it to one. – Heiko Becker Apr 13 '18 at 06:40
  • @nesreka `subst` won't work, neither goal selector, as it does not participate into auto proof flow. `dependent induction` often involve into more complex structural equality and evars, which isn't quite helpful here. a human knows what to fill in, and eauto sometimes can fill in correctly if the proof searching __by chance__ performed in the right order. but it's not a deterministic solution here. – Jason Hu Apr 13 '18 at 18:41
  • Can you explain what you mean with "not participating into auto proof flow? – Heiko Becker Apr 16 '18 at 06:39
  • @nesreka try to use goal selector in tactic and you will see. in fact, goal selector is quite useless, if the proof is automated from the beginning; and its use also doesn't make sense, because a tactic cares more about the form of a goal rather than its position. i don't think this discussion is fruitful here as it's already clear to me the answer is no, and what you said does not give a workaround for that. – Jason Hu Apr 16 '18 at 14:16
  • Ok, can you then please put this as the accepted answer that it is currently not possible? Or may I answer? – Heiko Becker Apr 17 '18 at 09:28
  • @nesreka, as no one gives the answer i want and I was reading through the whole refman, i don't think at this state it's possible in ltac alone. – Jason Hu Apr 17 '18 at 14:33

1 Answers1

0

As we discussed in the comments, it is the case that achieving this kind of inspection of the current proof goal is currently not possible in Ltac.

However, it may be possible to program such a tactic on the ocaml level or in one of the newer tactic languages like ltac2 or mtac.

Heiko Becker
  • 556
  • 3
  • 16