Zulip Chat Archive

Stream: new members

Topic: TPIL 4.6.6


view this post on Zulip 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!

view this post on Zulip 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,

view this post on Zulip Eduardo Cavazos (Nov 09 2019 at 04:27):

Then maybe I could expand

log (x * y)

into

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

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip 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)

view this post on Zulip 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]

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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.

view this post on Zulip 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]

view this post on Zulip Eduardo Cavazos (Nov 09 2019 at 05:52):

Hmm... OK, that's interesting.

view this post on Zulip 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.

view this post on Zulip Bryan Gin-ge Chen (Nov 09 2019 at 05:53):

That's what the error message says, too.

view this post on Zulip 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

view this post on Zulip 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 .

view this post on Zulip Bryan Gin-ge Chen (Nov 09 2019 at 05:59):

Yes, that's not valid syntax in simp.

view this post on Zulip Kevin Buzzard (Nov 09 2019 at 07:18):

Just remove the arrows and hope

view this post on Zulip 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]

view this post on Zulip 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