Zulip Chat Archive

Stream: new members

Topic: 4 | 2 → false


view this post on Zulip Jia Ming (Oct 13 2020 at 10:07):

Hello, may I have some hints as to how to solve these simple questions? I've tried many powerful tactics but all seem to fail :(

example : (4  2)  false := sorry
example : ( i : , (1/2 : ) = i)  false := sorry

view this post on Zulip Kenny Lau (Oct 13 2020 at 10:10):

the first one decidable, so dec_trivial

view this post on Zulip Kenny Lau (Oct 13 2020 at 10:11):

... and the second one can be reduced to the first one :P

view this post on Zulip Jia Ming (Oct 13 2020 at 10:19):

Ooo wow thank you!!!

view this post on Zulip Jia Ming (Oct 13 2020 at 10:23):

Umm huh, what exactly do u mean by reduced to the first one?

view this post on Zulip Kenny Lau (Oct 13 2020 at 10:28):

well you can prove that 2 * i = 1 given the assumption

view this post on Zulip Kenny Lau (Oct 13 2020 at 10:28):

which will allow you to deduce 2 \| 1

view this post on Zulip Kenny Lau (Oct 13 2020 at 10:28):

so it reduces to the first one

view this post on Zulip Jia Ming (Oct 13 2020 at 10:29):

Ooh rightt

view this post on Zulip Mario Carneiro (Oct 13 2020 at 10:35):

Hm, this didn't go as smoothly as I would hope

example : ( i : , (1/2 : ) = i)  false :=
begin
  rintro i, h⟩,
  have : (1/2 : ) = i,
  { rw  @rat.cast_inj ,
    simpa using h },
  have := congr_arg rat.denom this,
  simp at this,
  cases this
end

view this post on Zulip Mario Carneiro (Oct 13 2020 at 10:37):

Kenny's proof goes a little better

example : ( i : , (1/2 : ) = i)  false :=
begin
  rintro i, h⟩,
  field_simp at h,
  norm_cast at h,
  have : (2:)  1 := i, by simpa [mul_comm] using h⟩,
  exact absurd this dec_trivial
end

view this post on Zulip Jia Ming (Oct 13 2020 at 10:46):

Awesome! Thanks

view this post on Zulip Shing Tak Lam (Oct 13 2020 at 12:01):

slightly different approach, I showed if there was such an integer, it'd be between 0 and 1.

example : ( i : , (1/2 : ) = i)  false :=
begin
  rintro x, hx⟩,
  have h1 : (0 : ) < x, linarith,
  have h2 : (x : ) < 1, linarith,
  norm_cast at h1 h2,
  linarith,
end

Last updated: May 14 2021 at 23:14 UTC