## Stream: new members

### Topic: If natural number n ≠ 0 then it is not 0 as a ℚ

#### Lars Ericson (Jan 16 2021 at 02:47):

I'm having trouble proving this:

lemma ne_zero_lift (n : ℕ) (h: n ≠ 0) : rat.of_int (int.of_nat n) ≠ 0 :=
sorry


#### Hanting Zhang (Jan 16 2021 at 03:05):

What is the context here? Explicitly writing out rat.of_int (int.of_nat n) seems unnatural. If you're trying to show that natural number n \neq 0 implies rational n \neq 0 in a proof, that should be done with norm_cast, or exact_mod_cast, these kind of tactics.

#### Alex J. Best (Jan 16 2021 at 03:05):

You probably shouldn't be using casts by explicitly using those functions, if your goal is more like this

import tactic
lemma ne_zero_lift (n : ℕ) (h: n ≠ 0) :  (( n : ℤ) : ℚ) ≠ 0 :=
by {norm_cast, exact h}


tactic#norm_cast will handle it

#### David Renshaw (Jan 16 2021 at 03:12):

Here's a (probably not very idiomatic) proof for the original lemma:

lemma ne_zero_lift (n : ℕ) (h: n ≠ 0) : rat.of_int (int.of_nat n) ≠ 0 :=
begin
rw [←(rat.coe_int_eq_of_int (int.of_nat n)), ←(int.coe_nat_eq n), (int.cast_coe_nat n)],
exact nat.cast_ne_zero.mpr h,
end


#### Lars Ericson (Jan 16 2021 at 04:04):

I am trying to prove a theorem I call plus_injective which looks like this:

import data.rat.basic
import tactic
open rat

lemma pow_two_ne_zero (n : ℕ): 2^n ≠ 0 :=
begin
induction n with d hd,
simp,
rw (succ_def d),
rw (pow_succ 2 d),
simp,
intro h,
finish,
end

lemma plus_injective
{a b : ℚ}
{n m : ℕ}
(ha : a.denom = 2 ^ n)
(hb : b.denom = 2 ^ m):
∃ k : ℕ, (a + b).denom = 2 ^ k :=
begin
by_cases h : m ≤ n,
use m,
have n20 := pow_two_ne_zero n,
have m20 := pow_two_ne_zero m,
sorry
end


At the point of the sorry, my tactic state is:

ab: ℚ
nm: ℕ
ha: a.denom = 2 ^ n
hb: b.denom = 2 ^ m
h: m ≤ n
n20: 2 ^ n ≠ 0
m20: 2 ^ m ≠ 0
h: ?m_1 ≠ 0 → ?m_2 ≠ 0 → mk ?m_3 ?m_1 + mk ?m_4 ?m_2 = mk (?m_3 * ?m_2 + ?m_4 * ?m_1) (?m_1 * ?m_2)
⊢ (a + b).denom = 2 ^ m


The point of the rat.add_def is to expand the definition of rational addition so that I can pick it apart and get the value of (a+b).denom explicitly so that I can prove that it equals 2^m. Note that m ≤ n. My reasoning is that

a + b = (2^n *a.num + 2^m * b.num)/(2^m*2^n) = (2^(n-m)*a + b)/2^m

However I can't get there if I can't apply rat_add and for that I need to make four rational numbers out of pieces of a and b, namely

• a.num as rational
• b.num as rational
• 2^n as rational
• 2^m as rational

I know this may look like the long way around, but I don't know the short way.

#### Alex J. Best (Jan 16 2021 at 04:25):

I would approach this this way:

lemma plus_injective
{a b : ℚ}
{n m : ℕ}
(ha : a.denom = 2 ^ n)
(hb : b.denom = 2 ^ m):
∃ k : ℕ, (a + b).denom = 2 ^ k :=
begin
revert ha hb a b, -- prep for next line
wlog h : m ≤ n, -- only want to worry about the m ≤ n case using WLOG without loss of generality
{ intros a b ha hb,
use m,
cases a,
cases b,
simp [(+)],
rw rat.mk_pnat_denom,
simp at *,
rw [ha, hb],
sorry },
{ specialize this hb ha, -- getting the n ≤ m case from the other
exact this, }
end


#### Alex J. Best (Jan 16 2021 at 04:27):

The key point here is that that definition of addition of two rationals is defined via the numerator and denominator, by doing cases a we split the rat into its components, numerator, denominator and proofs that it is well formed (coprime and positive denom).

#### Alex J. Best (Jan 16 2021 at 04:27):

Then we can rewrite the definition of rational addition directly, rather than using a have

#### Alex J. Best (Jan 16 2021 at 04:48):

Probably the key lemma you then need to prove is then (a_num * ↑2 ^ m + b_num * ↑2 ^ n).gcd (↑2 ^ n * ↑2 ^ m) = 2 ^ n given m \le n and b_num.nat_abs.coprime (2 ^ m) and a_num.nat_abs.coprime (2 ^ n), buuut that might not be true !

#### Alex J. Best (Jan 16 2021 at 04:48):

Also

lemma gcd_nat_abs (a : ℤ) (b : ℕ) : a.nat_abs.gcd b = a.gcd b := sorry


seems useful here, but doesn't seem to be in the library

#### Mario Carneiro (Jan 16 2021 at 05:15):

What I would go for is a proof that (\u a / \u b).denom | b, or alternatively (a /. b).denom | b. Then by definition of addition on rat (a + b).denom = (... /. a.denom * b.denom).denom so by the theorem and your equalities, (a + b).denom | 2 ^ n * 2 ^ m. Finally, use a theorem which says a | 2 ^ i -> \exists j, a = 2 ^ j and you are done

#### Mario Carneiro (Jan 16 2021 at 05:30):

lemma eq_two_pow_of_dvd_two_pow {a n : ℕ} : a ∣ 2 ^ n → ∃ m : ℕ, a = 2 ^ m := sorry

lemma add_denom_two_pow {a b : ℚ} {n m : ℕ} (ha : a.denom = 2 ^ n) (hb : b.denom = 2 ^ m) :
∃ k : ℕ, (a + b).denom = 2 ^ k :=
begin
apply @eq_two_pow_of_dvd_two_pow _ (n + m),
apply rat.denom_dvd
end


I've saved the best for last for you

#### Kevin Buzzard (Jan 16 2021 at 09:14):

Denominator of a+b divides product of denominators of a and b. Is that in mathlib? That should be a clean route to this goal

#### Mario Carneiro (Jan 16 2021 at 09:59):

I don't think that exact theorem is stated, but it is about half of the proof of add_denom_two_pow just above, basically a combination of rat.add_num_denom and rat.denom_dvd

#### Damiano Testa (Jan 16 2021 at 15:38):

Lars, this is somewhat besides the point, however, use m in your partial proof of plus_injective does not appear right: there could be further cancelling, if m=n. In fact, the case a+b=0 shows this clearly (when 1<n).

#### Lars Ericson (Jan 16 2021 at 17:32):

Thank you very much for all of these suggestions. @Alex J. Best , one of these is quick:

lemma gcd_nat_abs (a : ℤ) (b : ℕ) : a.nat_abs.gcd b = a.gcd b :=
begin
exact rfl,
end


#### Lars Ericson (Jan 16 2021 at 20:51):

On this lemma by @Mario Carneiro

lemma eq_two_pow_of_dvd_two_pow {a n : ℕ} : a ∣ 2 ^ n → ∃ m : ℕ, a = 2 ^ m :=
begin
intro h1,
unfold has_dvd.dvd at h1,
sorry,
end


with tactic state

an: ℕ
h1: ∃ (c : ℕ), 2 ^ n = a * c
⊢ ∃ (m : ℕ), a = 2 ^ m


Then

• "by inspection", since 2^n only contains prime factor 2, I want to
• Suppose that there is a k≤n such that c = 2^k
• Solve 2^n = a * 2^k as a = 2^n/2^k = 2^(n-k)
• Use m=n-k to solve the goal

This seems correct but I don't know how to implement the "by inspection" step and the "suppose there is a k≤n" step.

#### Hanting Zhang (Jan 16 2021 at 21:00):

There's probably something like dvd_prime_pow that gives you c = 2^k for some k \le n.

#### Hanting Zhang (Jan 16 2021 at 21:01):

Ah, here, docs#nat.dvd_prime_pow.

#### Mario Carneiro (Jan 17 2021 at 02:50):

Actually your second step is the same as the theorem you are proving! But nat.dvd_prime_pow implies the theorem pretty easily.

#### Lars Ericson (Jan 17 2021 at 18:55):

Thanks @Hanting Zhang and @Mario Carneiro . I was able to finish this lemma. Lean did most of the work at the end:

import data.nat.prime

-- Mario Carneiro, Hanting Zhang
lemma eq_two_pow_of_dvd_two_pow {a n : ℕ} : a ∣ 2 ^ n → ∃ m : ℕ, a = 2 ^ m :=
begin
intro h1,
have h2 := (@nat.dvd_prime_pow 2 nat.prime_two n a).1 h1,
cases h2 with m hm,
cases hm with H hH,
finish,
end


#### Lars Ericson (Jan 17 2021 at 19:52):

That finishes theplus_injective goal:

import data.rat.basic
import data.nat.prime
import tactic
import tactic.slim_check
open rat

-- Mario Carneiro, Hanting Zhang
lemma eq_two_pow_of_dvd_two_pow {a n : ℕ} : a ∣ 2 ^ n → ∃ m : ℕ, a = 2 ^ m :=
begin
intro h1,
have h2 := (@nat.dvd_prime_pow 2 nat.prime_two n a).1 h1,
cases h2 with m hm,
cases hm with H hH,
finish,
end

lemma succ_def (m: ℕ) : m.succ = m + 1 := rfl

lemma pow_two_ne_zero (n : ℕ): 2^n ≠ 0 :=
begin
induction n with d hd,
simp,
rw (succ_def d),
rw (pow_succ 2 d),
simp,
intro h,
finish,
end

-- Mario Carneiro
lemma add_denom_two_pow {a b : ℚ} {n m : ℕ} (ha : a.denom = 2 ^ n) (hb : b.denom = 2 ^ m) :
∃ k : ℕ, (a + b).denom = 2 ^ k :=
begin
apply @eq_two_pow_of_dvd_two_pow _ (n + m),
apply rat.denom_dvd,
end

lemma plus_injective
{a b : ℚ}
{n m : ℕ}
(ha : a.denom = 2 ^ n)
(hb : b.denom = 2 ^ m):
∃ k : ℕ, (a + b).denom = 2 ^ k :=


#### Lars Ericson (Jan 17 2021 at 21:18):

@Alex J. Best I worked on your approach but I can't make it go through. I get stuck on a lemma expr_eq_pow2n which only seems true with a=0 or a is a multiple of 2^(m-n):

import data.rat.basic
import data.nat.gcd
import tactic
import tactic.slim_check
open rat

lemma nat_gcd_gt_0 {n : ℕ} (hn: n > 0) (m : ℕ): m.gcd(n) > 0 :=
nat.gcd_pos_of_pos_right m hn

lemma pow_add2 (m n : ℕ): 2^n * 2^m = 2^(n+m) := tactic.ring.pow_add_rev 2 n m

lemma succ_def (m: ℕ) : m.succ = m + 1 := rfl

lemma pow_two_ne_zero (n : ℕ): 2^n ≠ 0 :=
begin
induction n with d hd,
simp,
rw (succ_def d),
rw (pow_succ 2 d),
simp,
intro h,
finish,
end

lemma pow_two_gt_zero (n : ℕ): 2^n > 0 :=
begin
have h1 := pow_two_ne_zero n,
finish,
end

lemma expr_ne_0 (a_num b_num : ℤ) (m n: ℕ): (a_num * ↑(2 ^ m) + b_num * ↑(2 ^ n)).nat_abs.gcd (2 ^ n * 2 ^ m) > 0 :=
begin
have h1 := pow_two_gt_zero (n+m),
exact nat_gcd_gt_0 h1 (a_num * ↑(2 ^ m) + b_num * ↑(2 ^ n)).nat_abs,
end

lemma mul_inj_right(a b c : ℕ) (h: b = c) : b * a = c * a := congr_fun (congr_arg has_mul.mul h) a

lemma mul_to_left_div (a b c : ℕ ) (c0: c > 0) (h: a * b = c * b): a * b / c = b :=
nat.div_eq_of_eq_mul_right c0 h

lemma expr_eq_pow2n {n m: ℕ} {a b: ℤ} (h: m ≤ n)
(b_cop: b.nat_abs.coprime (2 ^ m))
(a_cop: a.nat_abs.coprime (2 ^ n)):
2 ^ n = (a * ↑(2 ^ m) + b * ↑(2 ^ n)).nat_abs.gcd (2 ^ n * 2 ^ m) :=
begin
have a_pos := pow_two_gt_zero n,
have b_pos := pow_two_gt_zero m,
sorry,
end

lemma plus_injective {a b : ℚ} {n m : ℕ} (ha : a.denom = 2 ^ n) (hb : b.denom = 2 ^ m):
∃ k : ℕ, (a + b).denom = 2 ^ k :=
begin
revert ha hb a b, -- prep for next line
wlog h : m ≤ n, -- only want to worry about the m ≤ n case using WLOG without loss of generality
{ intros a b ha hb,
use m,
cases a,
cases b,
simp only [(+)],
rw rat.mk_pnat_denom,
simp at *,
rw [ha, hb] at *,
have h1 := expr_ne_0 a_num b_num m n,
have h2 := mul_to_left_div (2^n) (2^m) ((a_num * ↑(2 ^ m) + b_num * ↑(2 ^ n)).nat_abs.gcd (2 ^ n * 2 ^ m)) h1,
apply h2,
clear h1 h2,
rw hb at b_pos,
have h3 := mul_inj_right (2^m) (2^n) (((a_num * ↑(2 ^ m) + b_num * ↑(2 ^ n)).nat_abs.gcd (2 ^ n * 2 ^ m))),
apply h3,
clear h3,
rw hb at b_cop,
exact (expr_eq_pow2n h b_cop a_cop),
},
{ specialize this hb ha, -- getting the n ≤ m case from the other
exact this, },
end


#### Alex J. Best (Jan 17 2021 at 21:49):

Right the correct version has $m \ge n$.

#### Lars Ericson (Jan 17 2021 at 22:17):

If I switch it around to n ≤ m, the goal becomes to show

2 ^ n = (a * ↑(2 ^ m) + b * ↑(2 ^ n)).nat_abs.gcd (2 ^ n * 2 ^ m)
= (a * ↑(2 ^ (m-n)) * (2 ^ n) + b * ↑(2 ^ n)).nat_abs.gcd (2 ^ n * 2 ^ m)
= ((2 ^ n) *(a * ↑(2 ^ (m-n)) + b)).nat_abs.gcd (2 ^ n * 2 ^ m)


or

1 = (a * ↑(2 ^ (m-n)) + b)).nat_abs.gcd (2 ^ m)


but for a=b=1, n=m, this seems to become 1=2. This seems false. Am I switching the n ≤ m in the wrong place? Here is what I am looking at:

import data.rat.basic
import data.nat.gcd
import tactic
import tactic.slim_check
open rat

lemma nat_gcd_gt_0 {n : ℕ} (hn: n > 0) (m : ℕ): m.gcd(n) > 0 :=
nat.gcd_pos_of_pos_right m hn

lemma pow_add2 (m n : ℕ): 2^n * 2^m = 2^(n+m) := tactic.ring.pow_add_rev 2 n m

lemma succ_def (m: ℕ) : m.succ = m + 1 := rfl

lemma pow_two_ne_zero (n : ℕ): 2^n ≠ 0 :=
begin
induction n with d hd,
simp,
rw (succ_def d),
rw (pow_succ 2 d),
simp,
intro h,
finish,
end

lemma pow_two_gt_zero (n : ℕ): 2^n > 0 :=
begin
have h1 := pow_two_ne_zero n,
finish,
end

lemma expr_ne_0 (a_num b_num : ℤ) (m n: ℕ): (a_num * ↑(2 ^ m) + b_num * ↑(2 ^ n)).nat_abs.gcd (2 ^ n * 2 ^ m) > 0 :=
begin
have h1 := pow_two_gt_zero (n+m),
exact nat_gcd_gt_0 h1 (a_num * ↑(2 ^ m) + b_num * ↑(2 ^ n)).nat_abs,
end

lemma mul_inj_right(a b c : ℕ) (h: b = c) : b * a = c * a := congr_fun (congr_arg has_mul.mul h) a

lemma mul_to_left_div (a b c : ℕ ) (c0: c > 0) (h: a * b = c * b): a * b / c = b :=
nat.div_eq_of_eq_mul_right c0 h

lemma expr_eq_pow2n {n m: ℕ} {a b: ℤ} (h: n ≤ m)
(b_cop: b.nat_abs.coprime (2 ^ m))
(a_cop: a.nat_abs.coprime (2 ^ n)):
2 ^ n = (a * ↑(2 ^ m) + b * ↑(2 ^ n)).nat_abs.gcd (2 ^ n * 2 ^ m) :=
by
begin
have a_pos := pow_two_gt_zero n,
have b_pos := pow_two_gt_zero m,

end

lemma plus_injective {a b : ℚ} {n m : ℕ} (ha : a.denom = 2 ^ n) (hb : b.denom = 2 ^ m):
∃ k : ℕ, (a + b).denom = 2 ^ k :=
begin
revert ha hb a b, -- prep for next line
wlog h : n ≤ m, -- only want to worry about the m ≤ n case using WLOG without loss of generality
{ intros a b ha hb,
use m,
cases a,
cases b,
simp only [(+)],
rw rat.mk_pnat_denom,
simp at *,
rw [ha, hb] at *,
have h1 := expr_ne_0 a_num b_num m n,
have h2 := mul_to_left_div (2^n) (2^m) ((a_num * ↑(2 ^ m) + b_num * ↑(2 ^ n)).nat_abs.gcd (2 ^ n * 2 ^ m)) h1,
apply h2,
clear h1 h2,
rw hb at b_pos,
have h3 := mul_inj_right (2^m) (2^n) (((a_num * ↑(2 ^ m) + b_num * ↑(2 ^ n)).nat_abs.gcd (2 ^ n * 2 ^ m))),
apply h3,
clear h3,
rw hb at b_cop,
exact (expr_eq_pow2n h b_cop a_cop),
},
{ specialize this hb ha, -- getting the n ≤ m case from the other
exact this, },
end


#### Alex J. Best (Jan 17 2021 at 22:22):

Yeah that seems right, I guess you need $m > n$ then

#### Lars Ericson (Jan 17 2021 at 22:26):

Thanks, I'll try it now.

#### Lars Ericson (Jan 17 2021 at 22:38):

Saying n<m is very different in its effect on Lean than saying n≤m. In this case:

wlog h : m≤n,


two goals are produced, one with h and one with it's negation. In case

wlog h: n<m,


3 goals are produced. The first is

nm: ℕ
⊢ n < m ∨ m < n


This appears to be false for n=m. So the proof can't be fixed with this change.

#### Alex J. Best (Jan 17 2021 at 23:41):

Agreed, the proof will not work in its current form, the outline isn't true, after all 1/2 + 1/2 = 1/4 so in the case of n = m = 1 we have k = 2 so the use m line must be changed in that case at the very least.

#### Alex J. Best (Jan 17 2021 at 23:42):

You can do a case split inside the n \le m branch on m = n or  n < m` though

Last updated: May 09 2021 at 19:11 UTC