## Stream: maths

### Topic: norm_cast questions

#### 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 $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 (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


#### Alex J. Best (Nov 13 2019 at 00:37):

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

#### 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