Is the denominator LCD in rational addition?

Stream: new members

[Lars Ericson]

We have this theorem in mathlib:

lemma add_num_denom (q r : ℚ) : q + r =
  ((q.num * r.denom + q.denom * r.num : ℤ)) /. (↑q.denom * ↑r.denom : ℤ) :=

Now suppose

import data.rat.basic

variables a b : ℤ
variables m n : ℕ
def q : ℚ := a / 2^n
def r : ℚ := b / 2^m

Question: Does (q+r).denom actually look like (↑q.denom * ↑r.denom : ℤ) , or something else? If it's that, can I rely on it in a proof?

I'm asking because somewhere in the code it says that Lean likes to keep the size of the denominator down to avoid space crunches in proofs. In the above case, suppose m ≥ n. Then

q * r = (a*2^m + b*2^n)/2^(n+m)
         = (a*2^(m-n)*2^n+b*2^n)/(2^n * 2^m)
         = (a*2^(m-n) + b)/2^m

in which case

(q+r).denom = 2^m

Or is it really

(q+r).denom = 2^(m+n)

I need to know which way Lean behaves for a proof.

This is an interesting (to me) edge case where the proof might depend on an implementation detail which is not strictly a mathematical truth.

[Alex J. Best]

Denom is a function on rationals so if two rationals are equal they must have equal denominators, hence it cannot depend om what you added together to get that rational.

[Kenny Lau]

1/3 + 1/6 = 1/2

[Lars Ericson]

@Kenny Lau I'm trying to figure out if, under the hood, 1/3 + 1/6 = 1/2 as you say, or 9/18. If I just looked at

lemma add_num_denom (q r : ℚ) : q + r =
  ((q.num * r.denom + q.denom * r.num : ℤ)) /. (↑q.denom * ↑r.denom : ℤ) :=

I might think it was 9/18. What patch of code in Lean makes it 1/2?

[Kenny Lau]

you need to look at the definition of +

[Kenny Lau]

or /.

[Kenny Lau]

https://github.com/leanprover-community/mathlib/blob/3e7efd4ecd5d379932a89212eebd362beb01309e/src/data/rat/basic.lean
L254:

instance : has_add ℚ := ⟨rat.add⟩

LL251-252:

protected def add : ℚ → ℚ → ℚ
| ⟨n₁, d₁, h₁, c₁⟩ ⟨n₂, d₂, h₂, c₂⟩ := mk_pnat (n₁ * d₂ + n₂ * d₁) ⟨d₁ * d₂, mul_pos h₁ h₂⟩

LL73-86:

/-- Form the quotient `n / d` where `n:ℤ` and `d:ℕ+` (not necessarily coprime) -/
def mk_pnat (n : ℤ) : ℕ+ → ℚ | ⟨d, dpos⟩ :=
let n' := n.nat_abs, g := n'.gcd d in
⟨n / g, d / g, begin
  apply (nat.le_div_iff_mul_le _ _ (nat.gcd_pos_of_pos_right _ dpos)).2,
  simp, exact nat.le_of_dvd dpos (nat.gcd_dvd_right _ _)
end, begin
  have : int.nat_abs (n / ↑g) = n' / g,
  { cases int.nat_abs_eq n with e e; rw e, { refl },
    rw [int.neg_div_of_dvd, int.nat_abs_neg], { refl },
    exact int.coe_nat_dvd.2 (nat.gcd_dvd_left _ _) },
  rw this,
  exact nat.coprime_div_gcd_div_gcd (nat.gcd_pos_of_pos_right _ dpos)
end⟩

[Kenny Lau]

the simplest evidence is this

[Lars Ericson]

OK here it is

/-- Form the quotient `n / d` where `n:ℤ` and `d:ℕ+` (not necessarily coprime) -/
def mk_pnat (n : ℤ) : ℕ+ → ℚ | ⟨d, dpos⟩ :=
let n' := n.nat_abs, g := n'.gcd d in
⟨n / g, d / g, begin
  apply (nat.le_div_iff_mul_le _ _ (nat.gcd_pos_of_pos_right _ dpos)).2,
  simp, exact nat.le_of_dvd dpos (nat.gcd_dvd_right _ _)
end, begin
  have : int.nat_abs (n / ↑g) = n' / g,
  { cases int.nat_abs_eq n with e e; rw e, { refl },
    rw [int.neg_div_of_dvd, int.nat_abs_neg], { refl },
    exact int.coe_nat_dvd.2 (nat.gcd_dvd_left _ _) },
  rw this,
  exact nat.coprime_div_gcd_div_gcd (nat.gcd_pos_of_pos_right _ dpos)
end⟩

and this would support my 2nd interpretation of my original problem, namely that

(q+r).denom = 2^m

in the case that I set up. Which means potentially I need to expand the proof of rat.add to establish that.

[Kenny Lau]

LL39-49:

/-- `rat`, or `ℚ`, is the type of rational numbers. It is defined
  as the set of pairs ⟨n, d⟩ of integers such that `d` is positive and `n` and
  `d` are coprime. This representation is preferred to the quotient
  because without periodic reduction, the numerator and denominator can grow
  exponentially (for example, adding 1/2 to itself repeatedly). -/
structure rat := mk' ::
(num : ℤ)
(denom : ℕ)
(pos : 0 < denom)
(cop : num.nat_abs.coprime denom)
notation `ℚ` := rat

[Kenny Lau]

so a rational number is defined to have coprime numerator and denominator

[Lars Ericson]

Thanks that gives me a short cut to proving

(q+r).denom = 2^m

in my example.

[Kenny Lau]

great

[Lars Ericson]

I think. I'm trying to prove this:

lemma rat_pow2_denom_sum (a b : ℚ) (n m : ℕ):
  m ≥ n →
  a.denom = 2 ^ n →
  b.denom = 2 ^ m →
  (a + b).denom = 2 ^ m :=
begin
  intro h1,
  intro h2,
  intro h3,
  sorry
end

[Kenny Lau]

I mean you can probably prove (or maybe even find) that if n and d are coprime then (n / d : \Q).denom = d

[Kenny Lau]

this is the right way to think about it

[Kenny Lau]

is to extract lemma

[Kenny Lau]

your lemma is false btw, 1/2 + 1/2 = 1/1

[Kenny Lau]

also, move the arrows to the left of colon

[Kenny Lau]

there's no point to put them to the right of colon and then spend 3 lines to intro them one by one

[Lars Ericson]

I don't know how to put equations and inequalities on the left, just slide them over in parentheses?

[Kenny Lau]

lemma rat_pow2_denom_sum (a b : ℚ) (n m : ℕ)
  (h1 : m ≥ n)
  (h2 : a.denom = 2 ^ n)
  (h3 : b.denom = 2 ^ m) :
  (a + b).denom = 2 ^ m :=
begin
  sorry
end

[Lars Ericson]

Thanks! Anyway I have to rethink the lemma.

[Kenny Lau]

well you can (and you probably already did) phrase it in terms of the 2-adic valuation

[Lars Ericson]

I'm on the trail of Exercise 6F, this is where I'm at (with the lemma wrong):

import ring_theory.subring
import data.rat.basic
import tactic
open rat
open nat

lemma rat_pow2_denom_sum (a b : ℚ) (n m : ℕ):
  m ≥ n →
  a.denom = 2 ^ n →
  b.denom = 2 ^ m →
  (a + b).denom = 2 ^ m :=
begin
  intro h1,
  intro h2,
  intro h3,

end

lemma gcd_a_vs_2n_to_dvd (a n : ℕ ) : gcd a (2^n) = 1 ↔ ¬ (2 ∣ a) :=
begin
  split,
  intro h,
  refine not_dvd_of_pos_of_lt _ _,
  by_cases h1 : a > 0,
  assumption,
  sorry,
  sorry,
  sorry,
end

lemma gcd_ab_vs_2nm (a b n m : ℕ) :
  gcd a (2^n) = 1 →
  gcd b (2^m) = 1 →
  gcd (a*b) (2^(n+m)) = 1 :=
begin
  intro h1,
  intro h2,
  have h3 := gcd_a_vs_2n_to_dvd a n,
  have h4 := gcd_a_vs_2n_to_dvd b m,
  have h5 := gcd_a_vs_2n_to_dvd (a*b) (n+m),
  have h6 := h3.1 h1,
  have h7 := h4.1 h2,
  sorry,
end

def B : subring ℚ :=
{
  carrier := {x : ℚ | ∃ n : ℕ, x.denom = 2 ^ n },
  one_mem' /- (1 : M) ∈ carrier) -/ :=
  begin
    rw set.mem_set_of_eq,
    use 0,
    simp,
  end,
  mul_mem' /- {a b} : a ∈ carrier → b ∈ carrier → a * b ∈ carrier) -/ :=
  begin
    intro a,
    intro b,
    intro h1,
    intro h2,
    rw set.mem_set_of_eq at h1,
    rw set.mem_set_of_eq at h2,
    cases h1 with n hn,
    cases h2 with m hm,
    rw set.mem_set_of_eq,
    have h3 := rat.mul_num a b, -- just for context
    have h4 := rat.mul_denom a b,
    rw h4,
    rw hn,
    rw hm,
    use (n+m),
    have h5 := pow_add 2 n m,
    have h6 := a.cop,
    unfold coprime at h6,
    have h8 := b.cop,
    unfold coprime at h8,
    rw hn at h6,
    rw hm at h8,
    have h12 := gcd_ab_vs_2nm a.num.nat_abs b.num.nat_abs n m,
    have h13 := h12 h6,
    have h14 := h13 h8,
    rw ← h5,
    have h15 := int.nat_abs_mul a.num b.num,
    rw ← h15 at h14,
    rw h14,
    simp,
  end,
  zero_mem' /- (0 : M) ∈ carrier -/ :=
  begin
    rw set.mem_set_of_eq,
    use 0,
    simp,
    exact rfl,
  end,
  add_mem' /- {a b} : a ∈ carrier → b ∈ carrier → a + b ∈ carrier -/:=
  begin
    intro a,
    intro b,
    intro h1,
    intro h2,
    rw set.mem_set_of_eq at h1,
    rw set.mem_set_of_eq at h2,
    cases h1 with n hn,
    cases h2 with m hm,
    rw set.mem_set_of_eq,
    by_cases h3 : m ≥ n,
    {
      use m,
      have h4 := rat_pow2_denom_sum a b n m,
      exact h4 h3 hn hm,
    },
    {
      use n,
      have h5 := rat_pow2_denom_sum b a m n,
      have h6 := le_of_not_ge h3,
      have h7 := h5 h6 hm hn,
      rw (add_comm b a) at h7,
      assumption,
    },
  end,
  neg_mem' /- {x} : x ∈ carrier →d -x ∈ carrier -/:=
  begin
    intro x,
    intro h1,
    rw set.mem_set_of_eq at h1,
    cases h1 with n hn,
    rw set.mem_set_of_eq,
    use n,
    simp,
    exact hn,
  end,
 }

abbreviation is_an_integral_domain {α : Type*} [ring α] (s : set α) :=
  ∃ (sr : subring α) [integral_domain sr], s = sr

theorem ex6f : is_an_integral_domain {x : ℚ | ∃ n : ℕ, x.denom = 2 ^ n }  :=
⟨B, infer_instance, rfl⟩

[Kenny Lau]

this is just saying that |x| < |y| implies |x+y| = |y|

[Kenny Lau]

what is exercise 6f?

[Lars Ericson]

The last one here:
Screenshot-from-2021-01-10-15-33-13.png

[Kenny Lau]

well what is your mathematical proof?

[Kenny Lau]

you need to know which lemma to extract to make this most efficient

[Lars Ericson]

That it's closed under multiplication and addition.

[Kenny Lau]

the correct lemma is that (a / 2^n) has denominator a power of 2

[Kenny Lau]

i.e. "denominator being a power of 2" doesn't depend on the representation

[Kenny Lau]

I would say that the most crucial skill in formalization is knowing the right lemmas

[Kenny Lau]

everything else is secondary

[Kenny Lau]

you need to know how to convert from mathematical proof to a rigorous proof

[Kenny Lau]

your proof is probably (a/2^m) + (b/2^n) = (a x 2^n + b x 2^m) / 2^(m+n)

[Kenny Lau]

but you're implicitly using the fact that k / 2^p has denominator a power of 2

[Kenny Lau]

i.e. the RHS

[Lars Ericson]

At the top level it's easy, if p=a/2^n and q=b/2^m then p * q = (a*b)/2^(n+m). However in Lean I think I need to deal with the factor that numerator and denominator are coprime.

[Kenny Lau]

I would say that you don't actually understand the predicate "whose denominator is a power of 2"

[Kenny Lau]

is 3/6 in that ring?

[Lars Ericson]

Yes because 3/6 = 3 / (2*3) = 1/2.

[Kenny Lau]

but 6 isn't a power of 2

[Kenny Lau]

you see the issue here

[Kenny Lau]

what you wrote is not a proof that the denominator of p+q is a power of 2

[Kenny Lau]

you proved that p+q = (a x 2^n + b x 2^m) / 2^(m+n)

[Kenny Lau]

but you need to prove that any fraction of that form satisfies the predicate

[Kenny Lau]

therefore what I said is the correct lemma to extract

[Kenny Lau]

that any k/2^N satisfies the predicate

[Lars Ericson]

Thanks, I will work on that direction. I was trying to normalize the result in the proof to be coprime and then prove that the normalized form had the form a/2^m where 2 did not divide a and m was an natural number.

[Kenny Lau]

do you understand why the denominator of k/2^N is always a power of 2?

[Lars Ericson]

Yes, I understand how rationals multiply and add and what the result of adding or multiplying two forms of shape a/2^m and b/2^n is.

[Kenny Lau]

I'm talking about just k/2^N

[Kenny Lau]

where k is any integer

[Kenny Lau]

and N is any natural number

[Kenny Lau]

why is the denominator of k/2^N a power of 2?

[Lars Ericson]

By construction of rat in Lean, k and 2^N will be coprime at birth. If that's not the case, and k has a power of 2 in it, then you can just subtract that from N. In any event, k as an integer will have a factorization into primes of which 2 may or may not be present. Am I missing something?

[Kenny Lau]

you can just form (k / 2^N : \Q)

[Kenny Lau]

they won't be coprime at birth

[Lars Ericson]

In this case, by construction of the problem, the denominator is a power of 2 to begin with, for all the starting numbers.

[Lars Ericson]

But I guess the construction is not specific enough and k could have a power of 2 in it, which you can just subtract from N to normalize.

[Kenny Lau]

import data.rat.basic

lemma denom_div_two_pow (k : ℤ) (N : ℕ) :
  ∃ n : ℕ, (k / 2 ^ N : ℚ).denom = 2 ^ n :=
begin
  sorry
end

[Kenny Lau]

this is what I mean

[Kenny Lau]

import data.rat.basic

lemma denom_div_two_pow (k : ℤ) (N : ℕ) :
  ∃ n : ℕ, (k / 2 ^ N : ℚ).denom = 2 ^ n :=
begin
  sorry
end

lemma denom_two_pow_iff (q : ℚ) :
  (∃ n : ℕ, q.denom = 2 ^ n) ↔ (∃ (k : ℤ) (n : ℕ), (k / 2 ^ n : ℚ) = q) :=
begin
  sorry
end

[Kenny Lau]

then the second lemma will help you a lot

[Kenny Lau]

or you can "cheat" and just claim that the RHS of my lemma is what they mean by "whose denominators are 1 or a power of 2"

[Kenny Lau]

then you won't have to go through all these denom shenanigans

[Lars Ericson]

Thanks, I will rethink it with your advice.

My confusion is that you noted 9/18=3/6=1/2 so there are multiple representatives of a single rational with different denominators in the same sense that 0=5=10=15 mod 5. So to say that denominator being a power of 2 doesn't depend on the representation assumes a canonical representation. In the Lean case the canonical representation is that in rational a/m, a and m are coprime. So it seems safer to say that in the canonical representation, a/2^n has a denominator which is a power of 2, because we aren't seeing other possible representations like (3*a)/(3*2^n).

[Kenny Lau]

Indeed, I was wrong when I said that it doesn't depend on the representation

[Kenny Lau]

but what I wrote in Lean code should be correct

[Lars Ericson]

Thanks!

[Kenny Lau]

Kenny Lau said:

or you can "cheat" and just claim that the RHS of my lemma is what they mean by "whose denominators are 1 or a power of 2"

this brings an important point: what they write in mathematics doesn't necessarily correspond to the same notation in Lean

[Kenny Lau]

3 - 5 and $3 - 5$ don't mean the same thing

[Kenny Lau]

(one is 0, the other one is $-2$)

[Kenny Lau]

there is no point following a definition verbatim

[Lars Ericson]

I think this reflects your advice and eliminates the dependency on the canonical representation, and also doesn't cause slim_check to produce a counterexample:

import tactic
import tactic.slim_check

lemma mul_injective
        {a b : ℚ}
        {n m : ℕ}
        (ha : a.denom = 2 ^ n)
        (hb : b.denom = 2 ^ m):
        ∃ k : ℕ, (a * b).denom = 2 ^ k :=
begin
  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
  sorry,
end