can't seem to `rw` bidirectional lemma in both directions

Stream: new members

[rzeta0]

The following are two very minimal proofs using the bidirectional lemma mul_eq_zero to rewrite the hypothesis.

For referene, here is the signature of the lemma confirming it is bidirectional:
mul_eq_zero.{u_1} {M₀ : Type u_1} [MulZeroClass M₀] [NoZeroDivisors M₀] {a b : M₀} : a * b = 0 ↔ a = 0 ∨ b = 0

The following proof works fine, pretty much replicates the signature.

example {a b : ℚ} (h: a * b = 0): a = 0 ∨ b = 0 := by
  rw [mul_eq_zero] at h
  exact h

However, in the other direction it fails.

example {a b : ℚ} (h: a = 0 ∨ b = 0): a * b = 0 := by
  rw [mul_eq_zero] at h -- < ---------- fails
  exact h

I am puzzled as I had recently learned that rw only works with lemmas stating equivalence, = or ⇔.

That suggests they work in both directions, including for rw.

What am I misunderstanding?

[Daniel Weber]

You can use rw [← mul_eq_zero] at h to rewrite in the other direction

[rzeta0]

Daniel Weber said:

You can use rw [← mul_eq_zero] at h to rewrite in the other direction

aargh! this is ugly.

I thought we avoided directions eg mpr and mpbecause rw insisted on only working with bidirectional relations.

[Daniel Weber]

← is special rw notation for "write in the other direction", it's unrelated to mp and mpr

[rzeta0]

Thanks. I'm just commenting that this is ugly language design because if rw asserts the lemma must work in both directions (unlike apply) then it should try to match the pattern in both directions.

[rzeta0]

---

The following examples use apply and require mpr and mp - which is reasonable because apply doesn't demand the lemma is bidirectional.

example {a b : ℚ} (h: a * b = 0): a = 0 ∨ b = 0 := by
  apply mul_eq_zero.mp at h
  exact h

example {a b : ℚ} (h: a = 0 ∨ b = 0): a * b = 0 := by
  apply mul_eq_zero.mpr at h
  exact h

[rzeta0]

---

So i guess, setting aside my aesthetic concerns, is there any benefit in using rw over apply in this scenario?

I'm thinking about difference between apply and exact whereexact is stricter and the benefits include highlighting errors / misunderstandings sooner than apply.

I'm thinking that because rw is stricter on the lemmas it will allow, there might be a benefit.

[Kyle Miller]

When you're using rw, you often want surgical control over what's being rewritten. If it tried both directions, it could make some rewrites very hard to accomplish.

[Kyle Miller]

With rw, the only rule you need to know is "left-hand sides get transformed into right-hand sides"

[Kyle Miller]

(plus there are a number of other limitations that everyone eventually runs into)

[rzeta0]

Thanks @Kyle Miller - so should I conclude that rw is almost lexical pattern matching and replacement, whereas apply might do other things and the replaced expressions may not be the RHS of the applied lemma?

That would be a valid reason, in my beginner brain, to entertain the existence of both.

[Kyle Miller]

Lean is extensible though, so here is your version of rw:

macro "rzeta0_rw " "[" t:term "]" loc?:(Lean.Parser.Tactic.location)? : tactic =>
  `(tactic| first | rw [$t:term] $[$loc?]? | rw [← $t:term] $[$loc?]?)

example {a b : ℚ} (h: a = 0 ∨ b = 0): a * b = 0 := by
  rzeta0_rw [mul_eq_zero] at h -- < ---------- succeeds
  exact h

I only made it support a single rw lemma for simplicity. You can't do rzeta0_rw [lem1, lem2] for example.

rzeta0_rw [mul_eq_zero] at h is equivalent to first | rw [mul_eq_zero] at h | rw [← mul_eq_zero] at h. The first combinator goes with the first of its subtactics that succeed.

[Kyle Miller]

Yes, rw operates using pattern matching.

[Kyle Miller]

I'm fearing that you're thinking apply does something fancy. It's also using a simple rule, probably simpler.

[rzeta0]

Kyle Miller said:

I'm fearing that you're thinking apply does something fancy. It's also using a simple rule, probably simpler.

So what are the relative benefits of rw and apply in this simple example?

The answer might be "none", and that the benefits only appear in more complicated examples.

[Kyle Miller]

I'd say "none". There are probably second-order or third-order reasons why someone might reach for one or the other in a particular moment, but in a code review I'd accept either.

[Kyle Miller]

Some people like forward reasoning, some people like backward reasoning. With rw you can either rw at h, or rw the goal. With apply, you can only modify the goal.

[rzeta0]

Kyle Miller said:

With apply, you can only modify the goal.

isn't this an example of apply at a hypothesis, from the above fully working code?

apply mul_eq_zero.mp at h

[Kyle Miller]

apply .. at is a different tactic from apply

[Kyle Miller]

It's defined in mathlib: https://github.com/leanprover-community/mathlib4/blob/7f0670510ccf43e0e595357e31b7b8212cc02c45/Mathlib/Tactic/ApplyAt.lean#L19-L40

[rzeta0]

That is a surprise to me.

So when you say different tactic, the rules they use to manipulate the goal / hypothesis are different?

[Kyle Miller]

Completely different

[Kyle Miller]

apply thm at h looks for an argument to thm for which h is applicable, and the remaining arguments become new goals. In the original goal, h is modified to the result of thm.

[rzeta0]

Thanks - that is very useful, I will need take some time to think about this.

[Kyle Miller]

apply thm checks that the result of thm proves the current goal, and all the arguments to thm become new goals. (That's slightly simplified, but for most cases it's true. The complexity comes from the fact it figures out how many arguments thm actually needs to prove the goal.)

[Kyle Miller]

This is the extent of the smarts of apply:

example {p q r : Prop} (h : p → q → r) : r := by
  apply h
  -- two goals: ⊢ p and ⊢ q

example {p q r : Prop} (h : p → q → r) : q → r := by
  apply h
  -- one goal: ⊢ p

Recall that p → q → r is the same as p → (q → r).

(For completeness reasons, I feel compelled to mention that it still has a couple other tricks up its sleeve, though they're not the sorts of things you'd notice unless you really understand some details about higher-order unification — I was using Lean for years before noticing, and only because I was working on internals.)

[rzeta0]

So in this super-simple example, let me test my understanding:

example {n : ℕ} (h: n < 5): n ≠ 5 := by
  apply ne_of_lt
  exact h

• the theorem signature is ne_of_lt.{u_1} {α : Type u_1} [Preorder α] {a b : α} (h : a < b) : a ≠ b
• Here apply checks that the result of ne_of_lt proves the current goal.
• that result is a ≠ b which does indeed match the current goal
• the arguments to the theorem are a < b and they become the current goal - which is indeed the case in infoview

I think I'm correct here. I will try the same with apply at next.

PS - this looks like:

• goal is $Q$
• theorem is $P \implies Q$
• apply theorem so new goal is $P$

[Kyle Miller]

Yes, that looks right.

[rzeta0]

(deleted)

[Dan Velleman]

rzeta0 said:

Thanks. I'm just commenting that this is ugly language design because if rw asserts the lemma must work in both directions (unlike apply) then it should try to match the pattern in both directions.

I think you're mixing up two things. The purpose of rw is to change a statement (either a hypothesis or the goal) into an equivalent statement. The reason for requiring that you use a biconditional statement in rw, rather than just a conditional, is to ensure that the result of the rewriting will be equivalent to the original (and not just something that implies, or is implied by, the original). For example, if you have h : P ↔ Q, then P and Q are equivalent, so replacing one with the other inside any statement will give you an equivalent statement. The question of which way the replacement goes--whether P is replaced with Q or Q is replace with P--is an entirely different matter. That's something the user probably wants to have control over, so there is a way to specify: rw [h] means that P should be replaced with Q, and rw [←h] means that Q should be replaced by P. Notice that the replacement can be made inside a more complicated statement. For example, if the goal is (P ∨ R) ∧ (¬P ∨ S), then rw [h] will change the goal to (Q ∨ R) ∧ (¬Q ∨ S).

The purpose of apply is entirely different. apply is about inference, not equivalence. apply thm asks Lean to determine if thm can be used to infer the goal from some other statement (or perhaps several statements). If so, Lean sets the other statement to be the new goal. This new goal is not necessarily equivalent to the original goal; rather, the original goal can be inferred from the new goal.

[rzeta0]

@Dan Velleman thank you - "inference vs equivalence" is a very helpful way to see the difference.