## 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



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!

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