Silly disjunction resulting from simp

Stream: new members

[Sandy Maguire]

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]

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

[Sandy Maguire]

d k : Nat

[Kevin Buzzard]

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]

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]

currently

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

[Sandy Maguire]

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

[Kevin Buzzard]

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

[Sandy Maguire]

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

[Kevin Buzzard]

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]

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

[Damiano Testa]

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]

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]

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]

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

[Kevin Buzzard]

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

[Yakov Pechersky]

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

[Yakov Pechersky]

and being explicit

[Sandy Maguire]

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

[Sandy Maguire]

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]

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

[Mario Carneiro]

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

[Sandy Maguire]

sorry, i meant simp rather than rw

[Mario Carneiro]

which should have the same effect as yakov's version

[Sandy Maguire]

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]

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

[Mario Carneiro]

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

[Sandy Maguire]

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

[Sandy Maguire]

okay, marking this as resolved. thanks everyone!