# Zulip Chat Archive

## 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,
have h := rat.add_def,
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.add,
rw rat.mk_pnat_denom,
simp at *,
rw [ha, hb],
sorry },
{ specialize this hb ha, -- getting the n ≤ m case from the other
rw add_comm at this,
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),
rw [rat.add_num_denom, ← int.coe_nat_mul, ha, hb, ← pow_add, ← int.coe_nat_dvd],
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 the`plus_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),
rw [rat.add_num_denom, ← int.coe_nat_mul, ha, hb, ← pow_add, ← int.coe_nat_dvd],
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 :=
add_denom_two_pow ha hb
```

#### 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
rw pow_add2 m n,
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.add,
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
rw add_comm at this,
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
rw pow_add2 m n,
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.add,
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
rw add_comm at this,
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