# Zulip Chat Archive

## Stream: new members

### Topic: TPIL 4.6.6

#### Eduardo Cavazos (Nov 09 2019 at 04:03):

In TPIL 4.6.6 we're given the following:

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 include log_exp_eq exp_log_eq exp_pos exp_add

as well as a couple of examples:

example (x y z : real) : exp (x + y + z) = exp x * exp y * exp z := by rw [exp_add, exp_add] example (y : real) (h : y > 0) : exp (log y) = y := exp_log_eq h

The exercise requests a calculational proof of `log_mul`

. So I'm assuming it'll look something like this:

theorem log_mul {x y : real} (hx : x > 0) (hy : y > 0) : log (x * y) = log x + log y := calc log (x * y) = EXPR1 : TRANSFORM1 ... = EXPR2 : TRANSFORM2 ... = log x + log y

However, from what we're given in the exercise, it isn't clear what I should apply as TRANSFORM1 to move `log(x * y)`

into some other form that's a step closer to `log x + log y`

.

Should I be looking at some of the other identities mentioned in 4.2?

Thanks for any suggestions!

#### Eduardo Cavazos (Nov 09 2019 at 04:10):

We're given `hx`

and `hy`

so I thought about using something like this:

have h1 : exp (log x) = x, from exp_log_eq hx, have h2 : exp (log y) = y, from exp_log_eq hy,

#### Eduardo Cavazos (Nov 09 2019 at 04:27):

Then maybe I could expand

log (x * y)

into

log(exp (log x) * exp (log y))

#### Eduardo Cavazos (Nov 09 2019 at 04:31):

So maybe something like this:

theorem log_mul {x y : real} (hx : x > 0) (hy : y > 0) : log (x * y) = log x + log y := have h1 : exp (log x) = x, from exp_log_eq hx, have h3 : x = exp (log x), from eq.symm h1, have h2 : exp (log y) = y, from exp_log_eq hy, have h4 : y = exp (log y), from eq.symm h2, calc log (x * y) = log (exp (log x) * y) : TRANSFORM1 ... = log (exp (log x) * exp (log y)) : TRANSFORM2

But I'm not sure what to put at TRASNFORM1 and TRANSFORM2.

#### Eduardo Cavazos (Nov 09 2019 at 04:44):

Or maybe something like this:

theorem log_mul {x y : real} (hx : x > 0) (hy : y > 0) : log (x * y) = log x + log y := have h1 : exp (log x) = x, from exp_log_eq hx, have h3 : x = exp (log x), from eq.symm h1, have h2 : exp (log y) = y, from exp_log_eq hy, have h4 : y = exp (log y), from eq.symm h2, have h5 : exp (log x + log y) = exp (log x) * exp (log y), from exp_add (log x) (log y), have h6 : exp (log x) * exp (log y) = exp (log x + log y), from eq.symm h5, have h7 : log (exp (log x + log y)) = log x + log y, from log_exp_eq (log x + log y), calc log (x * y) = log (exp (log x) * exp (log y)) : by rw [h3, h4] ... = log (exp (log x + log y)) : by rw [h6] ... = log x + log y : by rw [h7]

But I get an error with that expression.

Trying something...

#### Bryan Gin-ge Chen (Nov 09 2019 at 05:05):

The details of the error messages give a pretty big hint here. For the first rewrite (involving `rw [h3, h4]`

) I see this:

tactic failed, there are unsolved goals state: ... ⊢ log (exp (log x) * exp (log y)) = log (exp (log (exp (log x))) * exp (log (exp (log y))))

The goal in the error message shows what happened. The rewrite you attempted changed stuff on the right hand side into more complicated stuff, whereas I think you probably wanted to transform the left hand side. You might want to look at your other hypotheses to see if they work better.

(Spoiler)

#### Eduardo Cavazos (Nov 09 2019 at 05:07):

Thank you @Bryan Gin-ge Chen!

I used your hint about other hypotheses. This seems to work:

theorem log_mul {x y : real} (hx : x > 0) (hy : y > 0) : log (x * y) = log x + log y := have h1 : exp (log x) = x, from exp_log_eq hx, have h3 : x = exp (log x), from eq.symm h1, have h2 : exp (log y) = y, from exp_log_eq hy, have h4 : y = exp (log y), from eq.symm h2, have h5 : exp (log x + log y) = exp (log x) * exp (log y), from exp_add (log x) (log y), have h6 : exp (log x) * exp (log y) = exp (log x + log y), from eq.symm h5, have h7 : log (exp (log x + log y)) = log x + log y, from log_exp_eq (log x + log y), calc log (x * y) = log (exp (log x) * exp (log y)) : by rw [h1, h2] ... = log (exp (log x + log y)) : by rw [h6] ... = log x + log y : by rw [h7]

#### Eduardo Cavazos (Nov 09 2019 at 05:34):

I was wondering what it would look like without using `rw`

:

example {x y : real} (hx : x > 0) (hy : y > 0) : log (x * y) = log x + log y := have h1 : exp (log x) = x, from exp_log_eq hx, have h3 : x = exp (log x), from eq.symm h1, have h2 : exp (log y) = y, from exp_log_eq hy, have h4 : y = exp (log y), from eq.symm h2, have h5 : exp (log x + log y) = exp (log x) * exp (log y), from exp_add (log x) (log y), have h6 : exp (log x) * exp (log y) = exp (log x + log y), from eq.symm h5, have h7 : log (exp (log x + log y)) = log x + log y, from log_exp_eq (log x + log y), have h8 : x * y = exp (log x) * y, from congr_arg _ h3, have h9 : exp (log x) * y = exp (log x) * exp (log y), from congr_arg _ h4, calc log (x * y) = log (exp (log x) * y) : congr_arg _ h8 ... = log (exp (log x) * exp (log y)) : congr_arg _ h9 ... = log (exp (log x + log y)) : congr_arg _ h6 ... = log x + log y : h7

#### Eduardo Cavazos (Nov 09 2019 at 05:35):

And finally, without `rw`

and everything inlined:

example {x y : real} (hx : x > 0) (hy : y > 0) : log (x * y) = log x + log y := calc log (x * y) = log (exp (log x) * y) : congr_arg _ (congr_arg _ (eq.symm (exp_log_eq hx))) ... = log (exp (log x) * exp (log y)) : congr_arg _ (congr_arg _ (eq.symm (exp_log_eq hy))) ... = log (exp (log x + log y)) : congr_arg _ (eq.symm (exp_add (log x) (log y))) ... = log x + log y : log_exp_eq (log x + log y)

#### Eduardo Cavazos (Nov 09 2019 at 05:44):

Given that this works:

example {x y : real} (hx : x > 0) (hy : y > 0) : log (x * y) = log x + log y := calc 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 exp_add ... = log x + log y : by rw log_exp_eq

I'm kinda wondering why this doesn't work:

example {x y : real} (hx : x > 0) (hy : y > 0) : log (x * y) = log x + log y := by rw [exp_log_eq hx, exp_log_eq hy, exp_add, log_exp_eq]

The end of section 4.3 shows an example that simplifies down to just a `by rw [...]`

expression.

#### Bryan Gin-ge Chen (Nov 09 2019 at 05:50):

I think the behavior of `rw`

might be a little different depending on what the local goal is. This works:

example {x y : real} (hx : x > 0) (hy : y > 0) : log (x * y) = log x + log y := by rw [←exp_log_eq hx, ←exp_log_eq hy, ←exp_add, log_exp_eq, log_exp_eq, log_exp_eq]

#### Eduardo Cavazos (Nov 09 2019 at 05:52):

Hmm... OK, that's interesting.

#### Bryan Gin-ge Chen (Nov 09 2019 at 05:52):

It's not quite the same proof though. The issue is that the goal for the rewrite in the example is:

⊢ log (x * y) = log x + log y

whereas that in the first step of the `calc`

block is:

⊢ log (x * y) = log (exp (log x) * exp (log y))

In the former, there's no `exp (log x)`

visible in the goal, so the forwards rewrite fails.

#### Bryan Gin-ge Chen (Nov 09 2019 at 05:53):

That's what the error message says, too.

#### Bryan Gin-ge Chen (Nov 09 2019 at 05:53):

rewrite tactic failed, did not find instance of the pattern in the target expression exp (log x) state: ... ⊢ log (x * y) = log x + log y

#### Eduardo Cavazos (Nov 09 2019 at 05:58):

Given that this works as you show above:

example {x y : real} (hx : x > 0) (hy : y > 0) : log (x * y) = log x + log y := by rw [← exp_log_eq hx, ← exp_log_eq hy, ← exp_add, log_exp_eq, log_exp_eq, log_exp_eq]

I tried the naive conversion to `simp`

:

example {x y : real} (hx : x > 0) (hy : y > 0) : log (x * y) = log x + log y := by simp [← exp_log_eq hx, ← exp_log_eq hy, ← exp_add, log_exp_eq]

but it doesn't like the `←`

.

#### Bryan Gin-ge Chen (Nov 09 2019 at 05:59):

Yes, that's not valid syntax in `simp`

.

#### Kevin Buzzard (Nov 09 2019 at 07:18):

Just remove the arrows and hope

#### Eduardo Cavazos (Nov 09 2019 at 07:39):

Removing the arrows doesn't seem to go through either:

example {x y : real} (hx : x > 0) (hy : y > 0) : log (x * y) = log x + log y := by simp [exp_log_eq hx, exp_log_eq hy, exp_add, log_exp_eq]

#### Kevin Buzzard (Nov 09 2019 at 08:45):

I don't know anything about how `simp`

actually does its thing, there will be a heuristic I guess

Last updated: May 13 2021 at 19:20 UTC