TPIL 4.6.6

Stream: new members

[Eduardo Cavazos]

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]

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]

Then maybe I could expand

log (x * y)

into

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

[Eduardo Cavazos]

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]

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]

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]

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]

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]

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]

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]

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]

Hmm... OK, that's interesting.

[Bryan Gin-ge Chen]

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]

That's what the error message says, too.

[Bryan Gin-ge Chen]

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]

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]

Yes, that's not valid syntax in simp.

[Kevin Buzzard]

Just remove the arrows and hope

[Eduardo Cavazos]

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]

I don't know anything about how simp actually does its thing, there will be a heuristic I guess