how to apply a lemma to a hypothesis

Stream: new members

[rzeta0]

I have two versions of a short proof.

In the second version I want to create an intermediate hypothesis h2 by applying the lemma mul_eq_zero to h.

I am failing, probably because of syntax.

So my question is (1) how do I apply it, and more importantly (2) how do I read the signature of the lemma to tell me how to apply it?

I've tried variations such as

• := by mul_eq_zero h
• := by rw [mul_eq_zero] h
• := mul_eq_zero h

import Mathlib.Tactic

example {p q : ℚ} (h: (p - 1) * (q - 2) = 0): p = 1 ∨ q = 2 := by
  rw [mul_eq_zero] at h
  obtain hp | hq := h
  · left
    linarith
  · right
    linarith

---

example {p q : ℚ} (h: (p - 1) * (q - 2) = 0): p = 1 ∨ q = 2 := by
  have h2:  p - 1 = 0 ∨ q - 2 =0 :=  mul_eq_zero  h -- < ---------------- fails -------------
  obtain hp | hq := h2
  · left
    linarith
  · right
    linarith

[Julian Berman]

Hover over the lemma in your editor and it will tell you what its type is -- what do you see?

[Dan Velleman]

mul_eq_zero is a biconditional statement: a * b = 0 ↔ a = 0 ∨ b = 0. That's why you were able to use it in rw, which can be used with equations and biconditional statements. In your second proof, you're trying to use the logical rule modus ponens, which applies to conditional statement, not biconditional statements. Modus ponens is the rule that says that from P → Q and P you can infer Q. So what you need to use is the left-to-right direction of the theorem. You can do that by using mul_eq_zero.mp instead of mul_eq_zero. (The right-to-left direction would be mul_eq_zero.mpr.)

[rzeta0]

Julian Berman said:

Hover over the lemma in your editor and it will tell you what its type is -- what do you see?

I see

mul_eq_zero.{u_1} {M₀ : Type u_1} [MulZeroClass M₀] [NoZeroDivisors M₀] {a b : M₀} : a * b = 0 ↔ a = 0 ∨ b = 0

I can work out what the correct syntax form I should use just by looking at the signature, the point about mp and mpr aside.

[Julian Berman]

Cool. To be sure, "can" is not a typo (for "can't") there right? Meaning the piece you were missing is the mp bit? Because it's an important skill to be able to look at that line and know what it means in terms of how you use mul_eq_zero (specifically it says mul_eq_zero takes 0 arguments, so you should immediately see from it that you can never do mul_eq_zero h for any h).

[rzeta0]

Thanks Julian - so no arguments means I don't supply parameters in the usual sense.

In the code above that works it is applied at h .. so what's going on here? Is it the case that rw is pointed at h and the rewriting is done by the lemma.

Regarding the mp, the following all fail:

• := mul_eq_zero.mp
• := by mul_eq_zero.mp
• := by apply mul_eq_zero.mp

So I'm back to the syntax question. Or maybe my misunderstanding is more fundamental?

[Ruben Van de Velde]

Please show your full code again - by mul_eq_zero.mp can't work because mul_eq_zero.mp is not a tactic but a term

[Dan Velleman]

In your second example, this works:

have h2:  p - 1 = 0 ∨ q - 2 =0 :=  mul_eq_zero.mp  h

[Julian Berman]

I can answer your question, and you should answer Ruben's, but in the interest of repeating the point I made about this being an important skill to read the term and see what arguments it takes -- you should now mouse over mul_eq_zero.mp -- this is a new term, separate from mul_eq_zero -- what does it say its type is? That skill above now is needed to know whether it's something you can use as-is or whether you need to give it an argument!

[rzeta0]

@Ruben Van de Velde here is the full code for the second (previously non-working) example:

import Mathlib.Tactic

example {p q : ℚ} (h: (p - 1) * (q - 2) = 0): p = 1 ∨ q = 2 := by
  have h2:  p - 1 = 0 ∨ q - 2 =0 := mul_eq_zero.mp h -- < -------- discussion is about this line
  obtain hp | hq := h2
  · left
    linarith
  · right
    linarith

[rzeta0]

@Julian Berman

If I hover over mul_eq_zero.mp my editor (VSC) still shows the signature for mul_eq_zero

mul_eq_zero.{u_1} {M₀ : Type u_1} [MulZeroClass M₀] [NoZeroDivisors M₀] {a b : M₀} : a * b = 0 ↔ a = 0 ∨ b = 0

If I hover over just the mp I get

Iff.mp {a b : Prop} (self : a ↔ b) : a → b

---

Update - I just checked in live.lean-lang.org and it also gives the same signatures.

[Kyle Miller]

This is a bit subtle, but you need to hover over the .

[Kyle Miller]

When you hover over things in VS Code, there should be an almost-imperceptible highlight. Many people don't notice it. It highlights everything that is part of that term.

[Kyle Miller]

Hovering over mul_eq_zero highlights just that, hovering over mp highlights just that, but hovering over . highlights the whole composite.

[rzeta0]

aha!

hovering over the dot shows me

p - 1 = 0 ∨ q - 2 = 0

but if I didn't include the h, that is, only had := mul_eq_zero.mp then it shows

type mismatch
  mul_eq_zero.mp
has type
  ?m.2307 * ?m.2308 = 0 → ?m.2307 = 0 ∨ ?m.2308 = 0 : Prop
but is expected to have type
  p - 1 = 0 ∨ q - 2 = 0 : Prop

How can I read this and know that I need to provide a parameter h?

Here is my guess:

• ?m.2307 * ?m.2308 = 0 suggests these elements are missing / uninstantiated.
• therefore I need to find something that fills them in by matching the pattern
• which is h
• but this is not as obvious as the message telling me it needs a parameter.

[Kyle Miller]

The → is a hint that mul_eq_zero.mp expects one more parameter

[Kyle Miller]

(This error message could be smarter and figure out you are missing a parameter automatically, but it is not (yet?) smart in that way.)

[Kyle Miller]

What you can see is that in the "has type" line the return type is ?m.2307 = 0 ∨ ?m.2308 = 0, and the expected type is p - 1 = 0 ∨ q - 2 = 0. These line up with ?m.2307 = p - 1 and ?m.2308 = q - 2.

[Alex Mobius]

I agree the UX here has room for improvement - hovering over the dot is bothersome, and synthetic hole names are, to use a flowery term, sinfully unreadable :( If that said (?a.1 * ?b.1) = 0 -> ?a.1 = 0 \/ ?b.1 = 0 or somesuch, perhaps eyes wouldn't gloss right over the term structure.

[Mario Carneiro]

I have advocated a few times for using "alphanumbering" ?a†, ?b†, ... ?z†, ?aa†, ... instead of showing unique IDs, because I find them significantly easier to differentiate as a human. (The daggers are needed to differentiate them from named metavariables, since you should not be able to refer to them by these names.) The other important improvement, which could be done at the same time, is to renumber them sequentially based on appearance in the goal state (but with a numbering that is globally coherent across the display of all goals), instead of using globally unique numbers, which is the main reason they have such eye-crossingly large but similar numbers like ?m.2307, ?m.2308. This is actually what lean 3 did (it used names like ?m_1, ?m_2...) but this got lost in the upgrade for whatever reason.