Zulip Chat Archive

Stream: new members

Topic: Calclulational proofs


Daniel (Aug 13 2019 at 09:35):

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 (Aug 13 2019 at 09:53):

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 (Aug 13 2019 at 09:56):

Actually it probably rewrited both occurrences

Patrick Massot (Aug 13 2019 at 09:59):

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 (Aug 13 2019 at 10:02):

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 (Aug 13 2019 at 10:02):

This will get rid of eq.symm everywhere

Daniel (Aug 13 2019 at 11:40):

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 (Aug 13 2019 at 11:44):

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 (Aug 13 2019 at 11:54):

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 (Aug 13 2019 at 14:01):

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 (Aug 13 2019 at 14:19):

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 (Aug 13 2019 at 14:23):

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.


Last updated: Dec 20 2023 at 11:08 UTC