Stream: new members

Topic: Multiple applies/exacts/haves in tactic mode

ZainAK283 (Nov 29 2019 at 17:27):

In tactic mode, you can combine "intro a" and "intro b" into "intros a b"
Is there a way to do this with apply, exact, and/or have?

Yury G. Kudryashov (Nov 29 2019 at 17:28):

exact closes the current goal, so what should do multiple exacts?

Yury G. Kudryashov (Nov 29 2019 at 17:29):

You can use refine instead of multiple applys

Yury G. Kudryashov (Nov 29 2019 at 17:31):

With mathlib you can write obtain ⟨a, b, c⟩ := (pa, pb, pc) where pa : a, pb : b, pc : c instead of have a := pa, have b := pb, have c := pc but I don't think that this is a good coding style.

Yury G. Kudryashov (Nov 29 2019 at 17:31):

obtain is have combined with rcases.

Yury G. Kudryashov (Nov 29 2019 at 17:32):

E.g., it's useful for obtain ⟨N, hN⟩ : ∃ N, ∀ n ≥ N, ... := ...

Patrick Massot (Nov 30 2019 at 10:06):

@ZainAK283 We would need a more specific question to help you. In a sense you can have "multiple exact" by providing a composite term in one exact. For instance, if your goal is a conjunction P ∧ Q and you
have hP : P and hQ : Q in your context, you can use split, exact hP, exact hQ but you can also use  exact ⟨hP, hQ⟩.

Patrick Massot (Nov 30 2019 at 10:07):

That being said, SSReflect make heavy use of a "multiple apply" that we don't have when they want to chain applications of lemmas, leaving hypotheses as side goals.

Mario Carneiro (Nov 30 2019 at 10:23):

exacts is actually a tactic

Last updated: May 11 2021 at 22:14 UTC