and_iff_and_of_iff_and_iff

Stream: general

[Johan Commelin]

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

[Mario Carneiro]

This looks like and_congr

[Johan Commelin]

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

[Sean Leather]

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

[Sean Leather]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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)

[Mario Carneiro]

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