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

Stream: new members

[Lars Ericson]

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]

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]

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]

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]

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]

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]

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]

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

[Alex J. Best]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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

[Hanting Zhang]

Ah, here, docs#nat.dvd_prime_pow.

[Mario Carneiro]

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]

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]

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),
  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]

@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]

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

[Lars Ericson]

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]

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

[Lars Ericson]

Thanks, I'll try it now.

[Lars Ericson]

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]

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]

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