Zulip Chat Archive

Stream: new members

Topic: Multiple applies/exacts/haves in tactic mode


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

view this post on Zulip Yury G. Kudryashov (Nov 29 2019 at 17:28):

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

view this post on Zulip Yury G. Kudryashov (Nov 29 2019 at 17:29):

You can use refine instead of multiple applys

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

view this post on Zulip Yury G. Kudryashov (Nov 29 2019 at 17:31):

obtain is have combined with rcases.

view this post on Zulip Yury G. Kudryashov (Nov 29 2019 at 17:32):

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

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

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

view this post on Zulip Mario Carneiro (Nov 30 2019 at 10:23):

exacts is actually a tactic


Last updated: May 11 2021 at 22:14 UTC