Applying iff theorem statements

Stream: new members

[Thomas Laraia]

There is an example where an iff statement, hqr: Q ↔ R is used using apply hqr.1. I've been across several problems been trying to use iff theorem statements and failing so continuing without them. How do you actually apply one direction of an iff statement?

[David Renshaw]

.1 is the same as .mp, which means the left to right direction.
.2 would be the same as .mpr, which means the right to left direction.
See https://leanprover-community.github.io/mathlib_docs/init/logic.html#iff

[David Renshaw]

I think mp stands for "modus ponens" and mpr stands for ... "modus ponens reversed" (?)

[Ruben Van de Velde]

Or "iMPlies" / "iMPlies Reverse" if you forget what the modus ponens is :)

[Thomas Laraia]

In the context of mul_left_cancel theorem mul_left_cancel (a b c : mynat) (ha : a ≠ 0) : a * b = a * c → b = c :=, is there a reason this wouldn't work?

revert b,
induction c with d hd,
rw mul_zero,
intro h,
intro g,
have j := mul_eq_zero_iff.mp a h g,
...

[Thomas Laraia]

And additionally, easier to leave it here, but what is acceptable usage of exfalso or is there another good way to get rid of the or in a hypothesis?

revert b,
induction c with d hd,
rw mul_zero,
intro h,
intro g,
have j := eq_zero_or_eq_zero_of_mul_eq_zero a h g,

I am left with an or hypothesis in j where a = 0 is clearly false thus the other must be true, so I considered using cases j and exfalso to show that it cannot be a = 0 of the two options.

Basically, my idea would be

revert b,
induction c with d hd,
rw mul_zero,
intro h,
intro g,
have j := eq_zero_or_eq_zero_of_mul_eq_zero a h g,
cases j,
exfalso,
apply ha j,
exact j,

[Huỳnh Trần Khanh]

(deleted)

[Huỳnh Trần Khanh]

Hmm... I don't know what you mean by "acceptable usage". Exfalso is certainly a perfectly fine way to get rid of that goal.

[Huỳnh Trần Khanh]

is there a reason this wouldn't work?

Well, this works: have j := (mul_eq_zero_iff a h).mp g,.

[Huỳnh Trần Khanh]

You have to read the theorem statement carefully: (a b : mynat): a * b = 0 ↔ a = 0 ∨ b = 0 means you have to supply a and b to get the iff hypothesis.

[Huỳnh Trần Khanh]

And an iff hypothesis is just a bundle of two functions: A -> B and B -> A. The first one is called mp and the second one is called mpr.

[Huỳnh Trần Khanh]

As a computer programmer, I am not fluent in Latin unfortunately. Just remember that the r in mpr means "reverse".

[Mario Carneiro]

Huỳnh Trần Khanh said:

As a computer programmer, I am not fluent in Latin unfortunately. Just remember that the r in mpr means "reverse".

That's why I call them .1 and .2

[Thomas Laraia]

theorem mul_left_cancel (a b c : mynat) (ha : a ≠ 0) : a * b = a * c → b = c :=
begin
revert b,
induction c with d hd,
rw mul_zero,
intro h,
intro g,
have f := (mul_eq_zero_iff a h).mp g,
cases f,
exfalso,
apply ha f,
exact f,
intro n,
intro g,

end

Is there a good way to isolate d to use hd?

[Huỳnh Trần Khanh]

I don't understand what you mean.

[Huỳnh Trần Khanh]

Spoiler: you have to cases on a mynat variable.