Zulip Chat Archive

Stream: general

Topic: tactic for proving iff

Bernd Losert (Jan 19 2022 at 23:41):

Is there a tactic that will "split" an iff goal into two goals, the mp direction and the mpr direction?

Eric Wieser (Jan 19 2022 at 23:42):

tactic#split

Bernd Losert (Jan 19 2022 at 23:42):

I thought that only works for conjuctions.

Bernd Losert (Jan 19 2022 at 23:43):

It works though. Nice.

Eric Wieser (Jan 19 2022 at 23:44):

(also this probably fits better in #Is there code for X?, for future reference)

Bernd Losert (Jan 19 2022 at 23:45):

By the way, is there a way of chaining iffs? Do I use transitivity?

Alex J. Best (Jan 19 2022 at 23:46):

Most transitivity tactics should work, as will manually applying docs#iff.trans. You can also use calc mode quite effectively for iffs sometimes https://leanprover-community.github.io/extras/calc.html

Eric Wieser (Jan 19 2022 at 23:47):

I think if your goal is A ↔ C then transitivity B (tactic#transitivity) will split the goal into A ↔ B and `B ↔ C|

Bernd Losert (Jan 19 2022 at 23:48):

I think I'll use iff.trans. Thanks!

Bernd Losert (Jan 19 2022 at 23:52):

I need a version of funext_iff, but for two argument functions. Is there such a thing?

Bernd Losert (Jan 19 2022 at 23:53):

Hmm... or maybe I need to apply funext_iff twice.

Bernd Losert (Jan 19 2022 at 23:55):

Ah, using simp did the trick.

Last updated: Dec 20 2023 at 11:08 UTC