Stream: Coq users

Topic: How to define small tactics inside a proof?


view this post on Zulip Daniel Hilst Selli (Jul 25 2022 at 17:58):

Is it possible to define some small tactic script and then reuse it during the proof but not letting it go out of the scope of the proof. I'm looking for something like

Lemma foo x : y.
Proof.
   let _easy := match goal with ... end in
   destruct v; try _easy.
  { blablabla; _easy. }
  { otherblablaba; _easy. }
Qed.

The let _easy := ... in works until I put a {, is there any alternative for that?

view this post on Zulip Paolo Giarrusso (Jul 25 2022 at 20:23):

  1. I don't think Qed. clears any tactics, but a section's End does — so you can wrap your lemma into Section foo. .... End foo.
  2. FWIW, I think let works until ., not {.

view this post on Zulip Daniel Hilst Selli (Jul 26 2022 at 21:47):

Yeah but I have to add . before {, so ... I can use [foo|bar] but is not as convenient as {...}

view this post on Zulip Paolo Giarrusso (Jul 27 2022 at 02:55):

ah I was unclear: I agree, I do mean that let lasts even less


Last updated: Jan 27 2023 at 01:03 UTC