Apply contrapostive

Stream: new members

[Trevor Fancher]

How can I apply the contrapositive of a theorem? I guess I'm looking for something like apply theorem_name.contrapositive. Something similar to how we can use apply iff_theoerem.mp or apply iff_theoerem.mpr. Just to be clear, I know about the contrapose tactic, but I can't seem to make it work for theorems.

[Kyle Miller]

docs#mt is modus tollens. Rather than using dot notation (since implications can't use dot notation), you'd do apply mt theorem_name

[Kyle Miller]

Incidentally, it would be nice if iffs could be contraposed as well. These seem not to be present in mathlib:

lemma iff.mt {a b : Prop} (h : a ↔ b) : ¬b → ¬a := mt h.mp
lemma iff.mtr {a b : Prop} (h : a ↔ b) : ¬a → ¬b := mt h.mpr

Then, in addition to apply iff_theorem.mp you could do apply iff_theorem.mt.

[Trevor Fancher]

Perfect. What I needed to do was apply mt filter.ext_iff.mp which works exactly how I wanted.

[Trevor Fancher]

Yes. because there is iff.mp and iff.mpr I would expect an iff.mt.

[Trevor Fancher]

Perhaps versions that do push_neg would be convenient as well.

[Kyle Miller]

I just learned about docs#not_congr, but it's not in the iff namespace so it can't be used with dot notation.

[Eric Wieser]

Perhaps we should alias not_congr in the iff namespace somewhere

[Kyle Miller]

I'd suggest iff.mtr for it, and iff.mt for its reverse.

It would also be nice to have the reverse versions of these, that strip off the nots. I don't know if these have a name in logic... maybe they could be rmt for "reverse modus tollens" and rmtr for "reverse modus tollens reverse".

[Johan Commelin]

Now we only need rmp and rmpr...

[Yaël Dillies]

Kyle Miller said:

Incidentally, it would be nice if iffs could be contraposed as well. These seem not to be present in mathlib:

lemma iff.mt {a b : Prop} (h : a ↔ b) : ¬b → ¬a := mt h.mp
lemma iff.mtr {a b : Prop} (h : a ↔ b) : ¬a → ¬b := mt h.mpr

Then, in addition to apply iff_theorem.mp you could do apply iff_theorem.mt.

Yes please! I really wanted those at one point.

[Eric Wieser]

If we had iff.not as (h : a ↔ b) : ¬a ↔ ¬b then you could use h.not.mpr and h.not.mp for those, which might be more discoverable

[Eric Wieser]

I suppose we could do something similar for docs#and_congr too