Zulip Chat Archive

Stream: new members

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


view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip Alex J. Best (Jan 16 2021 at 04:27):

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

view this post on Zulip 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 !

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Hanting Zhang (Jan 16 2021 at 21:01):

Ah, here, docs#nat.dvd_prime_pow.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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),
  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

view this post on Zulip 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

view this post on Zulip Alex J. Best (Jan 17 2021 at 21:49):

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

view this post on Zulip 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

view this post on Zulip Alex J. Best (Jan 17 2021 at 22:22):

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

view this post on Zulip Lars Ericson (Jan 17 2021 at 22:26):

Thanks, I'll try it now.

view this post on Zulip 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 : mn,

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.

view this post on Zulip 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.

view this post on Zulip 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