Stream: Coq users

Topic: Backtracking and assumption (without using Ltac)


view this post on Zulip Thomas Lamiaux (Mar 17 2024 at 00:06):

Hi, suppose you have two goals depending on each other and that there is two choice for the first goal as in the following.
Is it possible to write a tactic without using Ltac that use assumption for all goals, and backtracks if it chose wrong in the first goal ?
(Similarly to how one could use constructor)

Definition foo A B (a1 a2 : A) (f : forall (x : A), x = a1 -> B) : B.
Proof.
  unshelve eapply f; eassumption.
Admitted.

view this post on Zulip Pierre-Marie Pédrot (Mar 17 2024 at 11:31):

What's the problem with Ltac? The very fact you're saying "a tactic" without further ado means you're already using Ltac...

view this post on Zulip Thomas Lamiaux (Mar 17 2024 at 12:14):

It seems like a basic issue that must arise regularly, so I was hoping that there would be either

that wouldn't require a user to learn Ltac


Last updated: Jun 13 2024 at 19:02 UTC