Zulip Chat Archive

Stream: maths

Topic: norm_cast questions


view this post on Zulip Kevin Buzzard (Nov 12 2019 at 23:47):

Talking through a sqrt(2) irrational proof with @Jason KY. I realise I can't do these efficiently:

example (n : ) (d : ) (h : (2 : ) * (d * d : ) = ((n * n : ) : )) :
  2 * ((d : ) * (d : )) = n * n :=
begin
  -- one tactic?
  sorry
end

example (d : ) (h : d * d  0) : ((d * d : ) : )  0 :=
begin
  -- one tactic?
  sorry
end

I am just naively typing norm_cast and that's the only trick I know. Can these be done quickly? They are two goals we ended up with when trying to reduce an irrationality of sqrt(2) proof to an assertion about the only solutions in integers to a2=2b2a^2=2b^2 being the obvious ones.

import data.rat.basic

open rat

example : ¬ ( q : , q ^ 2 = 2) :=
begin
  -- intro
  rintro q, hq,
  -- notation for num and denom
  have h := q.pos,
  rw pow_two at hq, -- q*q easier than q^2
  rw @num_denom q at hq,
  rw mul_def at hq, -- otherwise you get (a/b)*(a/b) and I want to tidy denominators
  rw mk_eq_div at hq, -- finally there
  replace hq := hq.symm, -- `symmetry' at hq` should work here but I have an old mathlib apparently
  rw eq_div_iff_mul_eq at hq,
  -- now pick up some of the pieces
  swap 3,
  exact int.coe_nat_ne_zero_iff_pos.2 h,
  swap 3,
  exact int.coe_nat_ne_zero_iff_pos.2 h,
  sorry, sorry -- what's left is the above
end

view this post on Zulip Kevin Buzzard (Nov 13 2019 at 00:00):

I'm still struggling to do the rational bit of sqrt(2) being irrational. I always hope that some day it will just look like the maths proof :-/

import data.rat.basic

open rat

theorem T1 (n : ) (d : ) (h : (2 : ) * (d * d : ) = ((n * n : ) : )) :
  2 * ((d : ) * (d : )) = n * n :=
begin
  -- one tactic?
  sorry
end

theorem T2 (d : ) (h : d * d  0) : ((d * d : ) : )  0 :=
begin
  -- one tactic?
  sorry
end

example : ( a b : , 2 * (a * a) = b * b  a = 0)  ¬ ( q : , q ^ 2 = 2) :=
begin
  -- intro
  rintro h0 q, hq,
  -- notation for num and denom
  have h := q.pos,
  rw pow_two at hq, -- q*q easier than q^2
  rw @num_denom q at hq,
  rw mul_def at hq, -- otherwise you get (a/b)*(a/b) and I want to tidy denominators
  rw mk_eq_div at hq, -- finally there
  replace hq := hq.symm, -- `symmetry' at hq` should work here but I have an old mathlib apparently
  rw eq_div_iff_mul_eq at hq,
  swap 3,
  exact int.coe_nat_ne_zero_iff_pos.2 h,
  swap 3,
  exact int.coe_nat_ne_zero_iff_pos.2 h,
  replace hq := T1 _ _ hq,
  replace hq := h0 _ _ hq,
  norm_cast at hq,
  rw hq at h, cases h,
  apply T2,
  apply nat.mul_ne_zero,
  repeat {intro h2, rw h2 at h, cases h},
end

view this post on Zulip Alex J. Best (Nov 13 2019 at 00:37):

After import data.rat.cast both T1 and T2 are exact_mod_cast h,

view this post on Zulip Kevin Buzzard (Nov 13 2019 at 07:34):

Thanks! I just don't know how to use the tools. Are there some docs other than the tactic.md file?


Last updated: May 10 2021 at 06:13 UTC