norm_cast questions

Stream: maths

[Kevin Buzzard]

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 $a^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

[Kevin Buzzard]

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

[Alex J. Best]

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

[Kevin Buzzard]

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