TPIL 4.6.7

Stream: new members

[Eduardo Cavazos]

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?)

[Eduardo Cavazos]

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

[Bryan Gin-ge Chen]

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

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

(Spoiler)

[Eduardo Cavazos]

@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!!!

[Bryan Gin-ge Chen]

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

[Eduardo Cavazos]

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

[Eduardo Cavazos]

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

[Eduardo Cavazos]

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

[Bryan Gin-ge Chen]

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

[Eduardo Cavazos]

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 !