does lemma in `rw[lemma]` need to be = or iff only?

Stream: new members

[rzeta0]

I'm exploring this example proof again.

This time I'm asking myself why the rw [mul_eq_zero] can't be replaced by rw [mul_eq_zero.mp].

The error tells me it expects an = or iff proof:

tactic 'rewrite' failed, equality or iff proof expected

---

Here is the full example:

import Mathlib.Tactic

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

[Damiano Testa]

It seems to me that the error is being very precise about what the issue is...

[Julian Berman]

Damiano gave you the short version -- I'll answer your question with a question, (which hopefully you don't find annoying, my sense from your previous questions is this is ok with you).
Why or "how" do you think rewrite works? In other words what justification is there in a proof to be able to "rewrite" something, what logically makes it an ok operation to do?
Below is the (as usual, informal) way I think about it.

Spoiler

Rewriting x to y is saying "these things are the same, so let me replace one with the other".
In order to do this, you need a proof that x is the same as y.
Equality is the most obvious of such "sameness" notions.
An if-and-only-if is a second - x iff y is saying "if I have x then I have y, and if I don't have x, I don't have y", so that means they're "the same".
.mp is not such a relationship. .mp you should recall means "given a proof of x I can give you y". It's one direction of an iff, not both.
You cannot then use it in a rewrite, because rewrite is a tactic that expresses "replace same with same".

I'll go one step further and guess maybe your intuition tells you "yes but .mp is something I got out of an iff, so Lean could see that and rewrite knowing the iff is true", and here the answer is simply "it does not do that, it rewrites with what you tell it to, and you're telling it to rewrite with something that isn't a sameness relationship."

[rzeta0]

Hi @Julian Berman - thanks, helpful as always.

Your reply goes to the core of what was on my mind - what makes rewrite work.

Imagine we are given, as a hypothesis, that $A \implies B$. Then, in paper and pen maths, I can replace $A$ with $B$. I know I can't replace $B$ with $A$.

So this suggests Lean should be able to use iff_lemma.mp to rewrite A with B, and it would be valid.

Is your reply saying that it just doesn't, even if it were valid. The rewrite rules just look for bidirectional same-ness?

[Julian Berman]

Then, in paper and pen maths, I can replace A with B.

No you cannot do this in either direction (B's with A's nor A's with B's)! Given $A \implies B$ if you could use this to replace A's with B's, even in paper mathematics, you'd be able to prove $B \implies A$ by simply replacing the A with B, giving you $B \implies B$. But this is nonsense -- implication is not the same as "being the same". An implication requires you to input something, namely the proof of A. Rewrite does "replace same thing" and only that.

[rzeta0]

I'm confused - having a bad day!

Given $A \implies B$, replacing $A$ with $B$[+] gives me $B \implies B$ which is trivially true.

But using that rewrite rule, I can never get to $B \implies A$.

Am I horribly mistaken?

[+] because whenever $A$ is true, so is $B$, from the definition of implication

[Edward van de Meent]

i think the confusion here is between replacing a goal and replacing a hypothesis.

[Edward van de Meent]

(sort of)

[Edward van de Meent]

when you have an assumption A and the implication A -> B, indeed you can add B to your context. However, when your goal is A, you don't get to substitute it with with a goal B.

[Edward van de Meent]

making this more formal, you get to talk about co- and contra-variance, i think...

[Edward van de Meent]

when you have A -> B, you can replace A with B when it is in a covariant position, and B with A when it is in a contravariant position.

[Edward van de Meent]

i'm not sure, but i think co and contravariant positions swap depending on if you're looking at a hypothesis or a goal

[Philippe Duchon]

Or, to phrase it in another way: if you have the equivalence A <=> B, you can replace A by B anywhere (in the goal, or in a hypothesis), even as a subformula; thus, for instance, rewrite a second hypothesis (B /\ C) => D into (A /\ C) => D (hence the name of the tactic). But you cannot do this blindly if all you have is an implication instead of an equivalence.

And since rw lets you do this type of surgical rewriting, it really needs an equivalence (or an equality) and not an implication.

[Kyle Miller]

Here's @Julian Berman's example in Lean terms. The problem is that if you have an implication, your statement might depend on the implication in a number of ways that depend on the precise details of the statement. In the following, I've defined a simple predicate (the definition doesn't matter — just pay attention that given two propositions, the result is a proposition), and in the first argument it's contravariant with respect to implication, and the second it's covariant with respect to implication.

def MyPredicate (p q : Prop) : Prop := p → q

-- Contravaries in the first argument.
example (p p' q : Prop) (h : p → p') : MyPredicate p' q → MyPredicate p q :=
  (· ∘ h)

-- Covaries in the second argument.
example (p q q' : Prop) (h : q → q') : MyPredicate p q → MyPredicate p q' :=
  (h ∘ ·)

[Kyle Miller]

Only equality/iff lets you guarantee "equivariance" without knowing anything about the definition of MyPredicate.

[Derek Rhodes]

btw, as an aside, instead of rw the line of interest can use apply

example {p q : ℚ} (h: (p - 1)*(q - 2) = 0): p = 1 ∨ q = 2 := by
  apply mul_eq_zero.mp at h -- line of interest
  obtain hp | hq := h
  · left
    linarith
  · right
    linarith

[Eric Paul]

Another way to think of it is that rw only rewrites using equality.
Now the only reason we can use can use ↔ is because it is the same as equality as shown here:

theorem eq (P Q : Prop) : (P ↔ Q) = (P = Q) := Lean.Grind.iff_eq P Q

Now we can use rw and this theorem to replace your ↔ with = and then use rw again. Both of these steps rw can do because they are just rewriting with =.

theorem eq (P Q : Prop) : (P ↔ Q) = (P = Q) := Lean.Grind.iff_eq P Q

theorem test (P Q H : Prop) (q : Q) (h : H) (h1 : P ↔ H) : P ∧ Q := by
  -- this turns h1 into `P = H` by using the equality from `eq`
  rw [eq] at h1
  -- then we use the equality we have to replace `P` with `H`
  rw [h1]
  -- now we can easily handle the goal
  sorry

So really rw can only rewrite with equality. But since replacing your ↔ with = every time is inconvenient, rw just does those steps for you and lets you rewrite with ↔.

[Kyle Miller]

(It's a bit odd seeing Lean.Grind.iff_eq — that's a lemma for a tactic implementation. I gather you used exact? ? :smile:)

[Eric Paul]

Yes, I agree it's quite odd. I found a more normal looking lemma in Mathlib, but I have the issue that I can't figure out what namespace it's in so I can't use it. Is there an easy way to do that?

[Kyle Miller]

Small note: that's a stronger reason than the reason we can use iff in rw. The reason is simply propext, which converts iffs to equalities

#check propext
-- propext {a b : Prop} : (a ↔ b) → a = b

[Kyle Miller]

Here's the part of the rewrite tactic that applies propext if the lemma is an iff: https://github.com/leanprover/lean4/blob/9157c1f2792ddcf792b2b212185a2449078356b5/src/Lean/Meta/Tactic/Rewrite.lean#L70-L74

[Kyle Miller]

Eric Paul said:

I have the issue that I can't figure out what namespace it's in

Yeah, this can be frustrating sometimes, since the hover in the Infoview doesn't show the fully qualified name if you have the namespaces open. Best I can say is to "go to definition" and then hover over the theorem name in the source. That seems to give fully-qualified names.

[rzeta0]

Thanks everyone for the replies.

Interesting point made earlier that @Edward van de Meent made about replacing a goal vs a hypothesis.

I had not been aware of this consciously so let me try to elaborate on that below.

If there is an error below, I believe I would find it educational, as it seems I am carrying incorrect understanding.

---

Replacing the Hypothesis

Given the following hypotheses: $a=1 \implies b=2$, $(a-1)=0$, and $a, b \in \mathbb{Z}$, the goal is to prove $b=2$.

Steps:

• we can use algebra on $(a-1)=0$ to arrive at $a=1$
• we can use $a=1 \implies b=2$ to "rewrite" $a=1$ as $b=2$, reaching the goal

I believe this is a valid use of $A \implies B$ to rewrite $A$ as $B$.

---

Replacing the Goal

Given the following hypotheses: $b=1 \implies c=1$, $b=1$, and $b , c\in \mathbb{Z}$, the goal is to prove $c=1$.

Steps:

• I can use the hypotheses $$b=1 \implies c=1$$to rewrite the goal as $b=1$
• then I can use the other hypothesis $b=1$ to close the proof

I believe this is a valid rewriting of a goal with a hypothesis that is an implication.

---

[Ruben Van de Velde]

Those are valid logical arguments, but it's perhaps confusing to call them "rewriting", especially in the lean context

[Derek Rhodes]

it looks like applying to me :smile:

example (a b: ℤ) (h₁ : a = 1 → b = 2) (h₂: a - 1 = 0) : b = 2 := by
  have h₃ : a = 1 := by linarith
  apply h₁ h₃

[rzeta0]

I think I may let this question go and hope that by continuing the Mechanics of Proof course I'll eventually understand this more.

Thanks everyone for trying to help! :)