Zulip Chat Archive

Stream: new members

Topic: TPIL 4.6.7


view this post on Zulip Eduardo Cavazos (Nov 09 2019 at 14:54):

In TPIL 4.6.7 we're asked to prove the following:

example (x : ℤ) : x * 0 = 0 := sorry

It's suggested that we use #check sub_self as well as the identities in section 4.2.

It looks like I can get:

x * 0 = x * 0 + 0

using

eq.symm (add_zero (x * 0))

And I can get:

x * 0 - x * 0 = 0

using

sub_self (x * 0)

So I have these two:

x*0 = x*0 + 0

x*0 - x*0 = 0

and it seems like I just need an intermediary step (move the x*0 to the left of the = in the first expression to get the second?)

view this post on Zulip Eduardo Cavazos (Nov 09 2019 at 14:58):

I did enumerate the various applications of the identities with x * 0:

#check add_zero     (x * 0) -- x * 0 + 0 = x * 0
#check zero_add     (x * 0) -- 0 + x * 0 = x * 0
#check mul_one      (x * 0) -- x * 0 * 1 = x * 0
#check one_mul      (x * 0) -- 1 * (x * 0) = x * 0
#check neg_add_self (x * 0) -- -(x * 0) + x * 0 = 0
#check add_neg_self (x * 0) -- x * 0 + -(x * 0) = 0
#check sub_self     (x * 0) -- x * 0 - x * 0 = 0
#check mul_comm     x 0     -- x * 0 = 0 * x

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

It might be easier to start from something like this instead:

example (x : ) : x * 0 = 0 :=
calc x * 0 = x * (1 - 1) : sorry
...

(Spoiler)

view this post on Zulip Eduardo Cavazos (Nov 09 2019 at 15:21):

@Bryan Gin-ge Chen Ah! OK... This seems to work:

example (x : ) : x * 0 = 0 :=
    calc
        x * 0   = x * (1 - 1)   : by rw sub_self
        ...     = x * 1 - x * 1 : by rw mul_sub
        ...     = 0             : by rw sub_self

Thank you again!!!

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

Nice work! (and it looks like I had an unnecessary mul_one step in my "Spoiler", whoops)

view this post on Zulip Eduardo Cavazos (Nov 09 2019 at 15:34):

Here's a version which doesn't use rewrite:

example (x : ) : x * 0 = 0 :=
    have h1 : (0 : ) = 1 - 1,              from eq.refl _,
    have h2 : x * (1 - 1) = x * 1 - x * 1,  from mul_sub x 1 1,
    have h3 : x * 1 - x * 1 = 0,            from sub_self (x * 1),
    calc
        x * 0   = x * (1 - 1)   : congr_arg _ h1
        ...     = x * 1 - x * 1 : h2
        ...     = 0             : h3

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

As an aside, when I open your spoiler link to view your approach, I see errors in the Lean Web Editor:

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

Do I need to do something to get it to execute properly in there?

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

Try clicking the (?) icon and then scroll down and click "Clear JS / wasm cache and refresh".

view this post on Zulip Eduardo Cavazos (Nov 09 2019 at 16:55):

I needed to click the 'Clear library cache and refresh' button as well as that one. Now it's loading fine. Thanks @Bryan Gin-ge Chen !


Last updated: May 06 2021 at 20:13 UTC