## Stream: new members

### Topic: Is the denominator LCD in rational addition?

#### Lars Ericson (Jan 10 2021 at 18:40):

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 (Jan 10 2021 at 18:58):

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.

1/3 + 1/6 = 1/2

#### Lars Ericson (Jan 10 2021 at 20:24):

@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 (Jan 10 2021 at 20:25):

you need to look at the definition of +

#### Kenny Lau (Jan 10 2021 at 20:25):

or /.

#### Kenny Lau (Jan 10 2021 at 20:26):

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 (Jan 10 2021 at 20:27):

the simplest evidence is this

#### Lars Ericson (Jan 10 2021 at 20:27):

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 (Jan 10 2021 at 20:27):

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 (Jan 10 2021 at 20:27):

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

#### Lars Ericson (Jan 10 2021 at 20:27):

Thanks that gives me a short cut to proving

(q+r).denom = 2^m


in my example.

great

#### Lars Ericson (Jan 10 2021 at 20:28):

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 (Jan 10 2021 at 20:28):

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 (Jan 10 2021 at 20:28):

this is the right way to think about it

#### Kenny Lau (Jan 10 2021 at 20:29):

is to extract lemma

#### Kenny Lau (Jan 10 2021 at 20:29):

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

#### Kenny Lau (Jan 10 2021 at 20:29):

also, move the arrows to the left of colon

#### Kenny Lau (Jan 10 2021 at 20:29):

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 (Jan 10 2021 at 20:30):

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

#### Kenny Lau (Jan 10 2021 at 20:30):

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 (Jan 10 2021 at 20:31):

Thanks! Anyway I have to rethink the lemma.

#### Kenny Lau (Jan 10 2021 at 20:32):

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

#### Lars Ericson (Jan 10 2021 at 20:32):

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 (Jan 10 2021 at 20:32):

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

#### Kenny Lau (Jan 10 2021 at 20:32):

what is exercise 6f?

#### Lars Ericson (Jan 10 2021 at 20:33):

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

#### Kenny Lau (Jan 10 2021 at 20:34):

well what is your mathematical proof?

#### Kenny Lau (Jan 10 2021 at 20:34):

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

#### Lars Ericson (Jan 10 2021 at 20:34):

That it's closed under multiplication and addition.

#### Kenny Lau (Jan 10 2021 at 20:35):

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

#### Kenny Lau (Jan 10 2021 at 20:35):

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

#### Kenny Lau (Jan 10 2021 at 20:35):

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

#### Kenny Lau (Jan 10 2021 at 20:35):

everything else is secondary

#### Kenny Lau (Jan 10 2021 at 20:36):

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

#### Kenny Lau (Jan 10 2021 at 20:36):

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

#### Kenny Lau (Jan 10 2021 at 20:36):

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

i.e. the RHS

#### Lars Ericson (Jan 10 2021 at 20:37):

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 (Jan 10 2021 at 20:37):

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

#### Kenny Lau (Jan 10 2021 at 20:38):

is 3/6 in that ring?

#### Lars Ericson (Jan 10 2021 at 20:38):

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

#### Kenny Lau (Jan 10 2021 at 20:38):

but 6 isn't a power of 2

#### Kenny Lau (Jan 10 2021 at 20:38):

you see the issue here

#### Kenny Lau (Jan 10 2021 at 20:39):

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

#### Kenny Lau (Jan 10 2021 at 20:39):

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

#### Kenny Lau (Jan 10 2021 at 20:39):

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

#### Kenny Lau (Jan 10 2021 at 20:39):

therefore what I said is the correct lemma to extract

#### Kenny Lau (Jan 10 2021 at 20:39):

that any k/2^N satisfies the predicate

#### Lars Ericson (Jan 10 2021 at 20:41):

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 (Jan 10 2021 at 20:41):

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

#### Lars Ericson (Jan 10 2021 at 20:42):

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 (Jan 10 2021 at 20:42):

where k is any integer

#### Kenny Lau (Jan 10 2021 at 20:42):

and N is any natural number

#### Kenny Lau (Jan 10 2021 at 20:42):

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

#### Lars Ericson (Jan 10 2021 at 20:44):

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 (Jan 10 2021 at 20:45):

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

#### Kenny Lau (Jan 10 2021 at 20:46):

they won't be coprime at birth

#### Lars Ericson (Jan 10 2021 at 20:46):

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 (Jan 10 2021 at 20:47):

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 (Jan 10 2021 at 20:48):

import data.rat.basic

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


#### Kenny Lau (Jan 10 2021 at 20:48):

this is what I mean

#### Kenny Lau (Jan 10 2021 at 20:51):

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 (Jan 10 2021 at 20:52):

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 (Jan 10 2021 at 20:52):

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

#### Lars Ericson (Jan 10 2021 at 20:56):

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 (Jan 10 2021 at 20:58):

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

#### Kenny Lau (Jan 10 2021 at 20:58):

but what I wrote in Lean code should be correct

Thanks!

#### Kenny Lau (Jan 10 2021 at 21:00):

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 (Jan 10 2021 at 21:00):

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

#### Kenny Lau (Jan 10 2021 at 21:00):

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

#### Kenny Lau (Jan 10 2021 at 21:01):

there is no point following a definition verbatim

#### Lars Ericson (Jan 11 2021 at 00:48):

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


Last updated: May 13 2021 at 23:16 UTC