Zulip Chat Archive

Stream: new members

Topic: goal with multiple ands


view this post on Zulip Nicolò Cavalleri (Jun 22 2020 at 14:32):

Is it possible to split a goal of the form A∧B∧C∧...∧H in subgoals A, B, ..., H with a single tactic?

view this post on Zulip Johan Commelin (Jun 22 2020 at 14:32):

refine \< _, _, _, _ \>

view this post on Zulip Johan Commelin (Jun 22 2020 at 14:33):

Or maybe repeat { split }?

view this post on Zulip Nicolò Cavalleri (Jun 22 2020 at 14:39):

Johan Commelin said:

Or maybe repeat { split }?

This looks cool as it does not require me to count subgoals but is a bit aggressive as it splits not only but also other goals (like the ones with \exists). Do you know if there is a way to only make it split the s?

view this post on Zulip Patrick Massot (Jun 22 2020 at 14:40):

This would be a very nice exercise after reading the tactic writing tutorial.

view this post on Zulip Patrick Massot (Jun 22 2020 at 14:41):

I promise you'll enjoy doing it, and you'll be happy with what you'll have learned.

view this post on Zulip Nicolò Cavalleri (Jun 22 2020 at 14:41):

Patrick Massot said:

This would be a very nice exercise after reading the tactic writing tutorial.

You mean the one in the natural numbers game or in the book?

view this post on Zulip Patrick Massot (Jun 22 2020 at 14:41):

https://leanprover-community.github.io/extras/tactic_writing.html

view this post on Zulip Nicolò Cavalleri (Jun 22 2020 at 14:42):

Ok thanks

view this post on Zulip Patrick Massot (Jun 22 2020 at 14:47):

Don't hesitate to ask questions if you get stuck. Simon will answer them.


Last updated: May 13 2021 at 18:26 UTC