Calclulational proofs

Stream: new members

[Daniel]

Hey, I currently trying to learn Lean by reading the – very nice – “Theorem Proving in Lean” book.
While doing the exercises, I found something confusing;

variables (real : Type) [ordered_ring real]
variables (log exp : real → real)

variable  log_exp_eq : ∀ x, log (exp x) = x
variable  exp_log_eq : ∀ {x}, x > 0 → exp (log x) = x
variable  exp_pos    : ∀ x, exp x > 0
variable  exp_add    : ∀ x y, exp (x + y) = exp x * exp y

-- this ensures the assumptions are available in tactic proofs
include log_exp_eq exp_log_eq exp_pos exp_add

theorem log_mul {x y : real} (hx : x > 0) (hy : y > 0) :
  log (x * y) = log x + log y :=
  calc
    /- the relevant line follows: -/
    -- log(x * y) = log(exp (log x) * exp (log y)) : by rw [eq.symm (exp_log_eq hx), eq.symm (exp_log_eq hy)]
    /- this works: -/
    log(x * y) = log(exp (log x) * exp (log y)) : by rw [exp_log_eq hx, exp_log_eq hy]
           ... = log(exp (log x + log y))       : by rw [eq.symm (exp_add (log x) (log y))]
           ... = log x + log y                  : by rw [log_exp_eq]

For some reason the proof / tactic fails, if I include the eq.symms in the first line of the calculational proof, although the argument seems “the other way around”.
In the second line however, Lean does not seem to care about the order of equal terms, I can remove the eq.symm without problems.
Why is that? Is there a rule-of-thumb for when I can omit eq.symm and when I do need it?

[Patrick Massot]

You need to understand each line is a separate small lemma. The first line prove one equality. Then rw rewrites at the first place it finds, which is probably in the right hand side.

[Patrick Massot]

Actually it probably rewrited both occurrences

[Patrick Massot]

Indeed rewriting using exp_log_eq hx from right to left is a bad idea since it will complexify any formula involving x.

[Patrick Massot]

Also note from the section about rewrite: The notation ←t can be used to instruct the tactic to use the equality t in the reverse direction.

[Patrick Massot]

This will get rid of eq.symm everywhere

[Daniel]

This is clear to me, but I don't see, why rw rewrites the statement as it did.
Maybe the following (failing example) makes my question clearer:

example {x y : real} (hx : x > 0) (hy : y > 0) :
    log (x * y) = log(exp (log x) * exp (log y)) :=
    have ha : x = exp (log x), from eq.symm (exp_log_eq hx),
    have hb : y = exp (log y), from eq.symm (exp_log_eq hy),
    by rw [ha, hb]

Why doesn't rw replace the x on the left side of the equality with exp (log x)? (and similarly y with exp (log y)) Even though there is only a single x to be encountered (and replaced) on the left side of the expression log (x * y)?

[Daniel]

My expectation would be that log(x * y) = log(exp(log x) * exp (log y)) just by applying the equalities x = exp (log x) and y = exp (log y), since applying exp to equal arguments must result in equal results.

[Reid Barton]

It does replace that x, it just also replaces the x on the right hand side of the equation as well, leaving you no closer to being finished

[Floris van Doorn]

As was said before, the rw tactic rewrites both the left hand side and the right hand side of an equation.

If you want to rewrite only the left-hand side, you can use the following tactic: (which is a proof of your first calc-step)

by conv_lhs { rw [← exp_log_eq hx, ← exp_log_eq hy] }

[Daniel]

Nice. So I can just use ← and it works as I expect it to :)
Replacing in both sides seemed a bit counterintuitive to me, since I want to show a particular equality in this step, namely that the left / previous term is equal to the current lines' term.
But I guess it is more useful when combining multiple steps in one rw command.

[Kevin Buzzard]

The way it works by default is that lean finds the first match, and then replaces every occurrence of the thing that matched exactly. There is a file called conv.md in mathlib which is a write-up of how to do more sophisticated rewrites.