## Stream: new members

### Topic: Silly disjunction resulting from simp

#### Sandy Maguire (Jan 11 2021 at 18:22):

I have a hypothesis h : 2 * d ^ 2 = 2 * (2 * k * k), and if i then simp at h, I get the result d ^ 2 = 2 * k * k ∨ 2 = 0. But 2 /= 0 --- do i really need to prove this is an inl myself?

#### Kevin Buzzard (Jan 11 2021 at 18:23):

I know some types which have 2 = 0. Which type are you using?

#### Sandy Maguire (Jan 11 2021 at 18:23):

d k : Nat

#### Kevin Buzzard (Jan 11 2021 at 18:24):

Maybe if you add a proof of $2\not=0$ for nats as a hypothesis h and prove it with e.g. norm_num, and tell simp about h. it will do it for you. But it's not true that every tactic knows every obvious thing.

#### Sandy Maguire (Jan 11 2021 at 18:27):

that does it, thanks. is there a more concise way than have-binding the 2/=0 proof and then giving it to simp?

#### Sandy Maguire (Jan 11 2021 at 18:27):

currently

have two_neq_zero : 2 ≠ 0 := by norm_num,
simp [two_neq_zero] at h,


#### Sandy Maguire (Jan 11 2021 at 18:27):

i'd prefer to put it directly in the simp list

#### Kevin Buzzard (Jan 11 2021 at 18:28):

simp at h is an antipattern anyway. Maybe you should just apply the relevant lemma?

#### Sandy Maguire (Jan 11 2021 at 18:28):

sorry, i'm not sure what you mean by applying the relevant lemma here

#### Kevin Buzzard (Jan 11 2021 at 18:29):

There will be a lemma in the library saying a \ne 0 -> a * b = a * c -> b = c and you could just apply that.

#### Rob Lewis (Jan 11 2021 at 18:30):

norm_num at h is a much of an antipattern as simp at h but it will do what you want here.

#### Damiano Testa (Jan 11 2021 at 18:31):

There should also be a zero_lt_two, which you can combine with ne_of_gt(or ne_of_lt, I am not at my computer...)

#### Sandy Maguire (Jan 11 2021 at 18:33):

some more context; i'm trying to show sqrt2 is irrational. my context:

h': n ^ 2 = 2 * d ^ 2
even_pow_n_2: even (n ^ 2)
k: ℕ
hk: n = 2 * k


now I want to show d^2 is even, so i want to show there exists m st 2 * m = d^2. my current way of doing that is via a calc, but syntactically i don't know how to make it give me what i want, thus this at shenanigans

have h :=
calc
2 * d^2 = n^2               : h'.symm
... = (2 * k)^2         : by rw hk
... = (2 * k) * (2 * k) : by rw pow_two
... = 4 * k * k         : by linarith
... = 2 * (2 * k * k)   : by linarith,
have two_neq_zero : 2 ≠ 0 := by norm_num,
simp [two_neq_zero] at h,


#### Kevin Buzzard (Jan 11 2021 at 18:33):

import tactic

example (d k : ℕ) : 2 ≠ 0 → 2 * d ^ 2 = 2 * (2 * k * k) → d ^ 2 = 2 * k * k := by library_search -- mul_right_inj'

example (d k : ℕ) (h : 2 * d ^ 2 = 2 * (2 * k * k)) : d ^ 2 = 2 * k * k :=
begin
exact (mul_right_inj' (by norm_num)).1 h,
end


#### Sandy Maguire (Jan 11 2021 at 18:33):

the result is h : d ^ 2 = 2 * k * k which is actually what i want

#### Kevin Buzzard (Jan 11 2021 at 18:34):

You could do replace h := (mul_right_inj' (by norm_num)).1 h

#### Yakov Pechersky (Jan 11 2021 at 18:34):

You can always do (show 2 ≠ 0, by norm_num) as a way of inlining

#### Yakov Pechersky (Jan 11 2021 at 18:34):

and being explicit

#### Sandy Maguire (Jan 11 2021 at 18:35):

thanks kevin and yakov --- both the things i didn't know i was looking for

#### Sandy Maguire (Jan 11 2021 at 18:37):

i had tried rw [(by norm_num) : 2 \neq 0] at h, but syntactically it didnt work. happy to see that the show construct does

#### Yakov Pechersky (Jan 11 2021 at 18:38):

even if that worked, you can't rw using an inequality, only using equalities and iffs

#### Mario Carneiro (Jan 11 2021 at 18:38):

the correct way to write what you wrote is rw (by norm_num : 2 \neq 0) at h

#### Sandy Maguire (Jan 11 2021 at 18:38):

sorry, i meant simp rather than rw

#### Mario Carneiro (Jan 11 2021 at 18:38):

which should have the same effect as yakov's version

#### Sandy Maguire (Jan 11 2021 at 18:39):

ahh. simp [by norm_num : 2 ≠ 0] at h, doesn't parse, but simp [(by norm_num : 2 ≠ 0)] at h, does :upside_down:

#### Yakov Pechersky (Jan 11 2021 at 18:40):

yes, because type ascription to any term always has to be of the syntax ( term : type )`

#### Mario Carneiro (Jan 11 2021 at 18:40):

parentheses are mandatory around type ascription, they are part of the syntax

#### Sandy Maguire (Jan 11 2021 at 18:40):

that's helpful to know. i'm coming from haskell where the parens are optional

#### Sandy Maguire (Jan 11 2021 at 18:40):

okay, marking this as resolved. thanks everyone!

Last updated: May 15 2021 at 23:13 UTC