Zulip Chat Archive

Stream: new members

Topic: Silly disjunction resulting from simp


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

view this post on Zulip Kevin Buzzard (Jan 11 2021 at 18:23):

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

view this post on Zulip Sandy Maguire (Jan 11 2021 at 18:23):

d k : Nat

view this post on Zulip Kevin Buzzard (Jan 11 2021 at 18:24):

Maybe if you add a proof of 202\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.

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

view this post on Zulip Sandy Maguire (Jan 11 2021 at 18:27):

currently

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

view this post on Zulip Sandy Maguire (Jan 11 2021 at 18:27):

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

view this post on Zulip Kevin Buzzard (Jan 11 2021 at 18:28):

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

view this post on Zulip Sandy Maguire (Jan 11 2021 at 18:28):

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

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

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

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

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

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

view this post on Zulip Sandy Maguire (Jan 11 2021 at 18:33):

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

view this post on Zulip Kevin Buzzard (Jan 11 2021 at 18:34):

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

view this post on Zulip Yakov Pechersky (Jan 11 2021 at 18:34):

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

view this post on Zulip Yakov Pechersky (Jan 11 2021 at 18:34):

and being explicit

view this post on Zulip Sandy Maguire (Jan 11 2021 at 18:35):

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

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

view this post on Zulip Yakov Pechersky (Jan 11 2021 at 18:38):

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

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

view this post on Zulip Sandy Maguire (Jan 11 2021 at 18:38):

sorry, i meant simp rather than rw

view this post on Zulip Mario Carneiro (Jan 11 2021 at 18:38):

which should have the same effect as yakov's version

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

view this post on Zulip Yakov Pechersky (Jan 11 2021 at 18:40):

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

view this post on Zulip Mario Carneiro (Jan 11 2021 at 18:40):

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

view this post on Zulip Sandy Maguire (Jan 11 2021 at 18:40):

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

view this post on Zulip Sandy Maguire (Jan 11 2021 at 18:40):

okay, marking this as resolved. thanks everyone!


Last updated: May 15 2021 at 23:13 UTC