Zulip Chat Archive

Stream: general

Topic: and_iff_and_of_iff_and_iff


view this post on Zulip Johan Commelin (Oct 03 2018 at 08:04):

Would this be a useful lemma for mathlib? If so, where should it go? I currently solve this by split; intros; split, but that is a bit of a hack, and creates 4 goals where usually 2 should suffice.

theorem and_iff_and_of_iff_and_iff {P1 P2 Q1 Q2 : Prop} (H : (P1 \iff Q1) \and (P2 \iff Q2)) :
(P1 \and P2) \iff (Q1 \and Q2) := sorry

view this post on Zulip Mario Carneiro (Oct 03 2018 at 08:06):

This looks like and_congr

view this post on Zulip Johan Commelin (Oct 03 2018 at 08:08):

Cool, I'll use that! Is there a way that I could have discovered that name myself?

view this post on Zulip Sean Leather (Oct 03 2018 at 08:09):

I also had trouble finding that. Like me, Johan may have been look for something iff-named instead of and- and congr-named.

view this post on Zulip Sean Leather (Oct 03 2018 at 08:11):

I probably tried git grep 'and.*iff' and git grep 'iff.*and'.

view this post on Zulip Mario Carneiro (Oct 03 2018 at 08:11):

That's true. This is a special pattern, like ext. congr lemmas mean if the inputs are equal then a function applied to those inputs is equal

view this post on Zulip Mario Carneiro (Oct 03 2018 at 08:13):

There are similar theorems for all the propositional functions, and for regular functions congr the tactic will often generate these on the fly

view this post on Zulip Mario Carneiro (Oct 03 2018 at 08:16):

You will also find custom congr lemmas for things like list.map_congr, where we want to insert an additional assumption into the hypothesis (if \all x \in l, f x = g x then map f l = map g l)

view this post on Zulip Mario Carneiro (Oct 03 2018 at 08:17):

so many higher order functions have some kind of altered congr lemma


Last updated: May 10 2021 at 23:11 UTC