Zulip Chat Archive

Stream: new members

Topic: Is the denominator LCD in rational addition?


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

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

view this post on Zulip Kenny Lau (Jan 10 2021 at 19:23):

1/3 + 1/6 = 1/2

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

view this post on Zulip Kenny Lau (Jan 10 2021 at 20:25):

you need to look at the definition of +

view this post on Zulip Kenny Lau (Jan 10 2021 at 20:25):

or /.

view this post on Zulip Kenny Lau (Jan 10 2021 at 20:26):

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

view this post on Zulip Kenny Lau (Jan 10 2021 at 20:27):

the simplest evidence is this

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

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

view this post on Zulip Kenny Lau (Jan 10 2021 at 20:27):

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

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

view this post on Zulip Kenny Lau (Jan 10 2021 at 20:28):

great

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

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

view this post on Zulip Kenny Lau (Jan 10 2021 at 20:28):

this is the right way to think about it

view this post on Zulip Kenny Lau (Jan 10 2021 at 20:29):

is to extract lemma

view this post on Zulip Kenny Lau (Jan 10 2021 at 20:29):

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

view this post on Zulip Kenny Lau (Jan 10 2021 at 20:29):

also, move the arrows to the left of colon

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

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

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

view this post on Zulip Lars Ericson (Jan 10 2021 at 20:31):

Thanks! Anyway I have to rethink the lemma.

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

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

view this post on Zulip Kenny Lau (Jan 10 2021 at 20:32):

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

view this post on Zulip Kenny Lau (Jan 10 2021 at 20:32):

what is exercise 6f?

view this post on Zulip Lars Ericson (Jan 10 2021 at 20:33):

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

view this post on Zulip Kenny Lau (Jan 10 2021 at 20:34):

well what is your mathematical proof?

view this post on Zulip Kenny Lau (Jan 10 2021 at 20:34):

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

view this post on Zulip Lars Ericson (Jan 10 2021 at 20:34):

That it's closed under multiplication and addition.

view this post on Zulip Kenny Lau (Jan 10 2021 at 20:35):

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

view this post on Zulip Kenny Lau (Jan 10 2021 at 20:35):

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

view this post on Zulip Kenny Lau (Jan 10 2021 at 20:35):

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

view this post on Zulip Kenny Lau (Jan 10 2021 at 20:35):

everything else is secondary

view this post on Zulip Kenny Lau (Jan 10 2021 at 20:36):

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

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

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

view this post on Zulip Kenny Lau (Jan 10 2021 at 20:37):

i.e. the RHS

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

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

view this post on Zulip Kenny Lau (Jan 10 2021 at 20:38):

is 3/6 in that ring?

view this post on Zulip Lars Ericson (Jan 10 2021 at 20:38):

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

view this post on Zulip Kenny Lau (Jan 10 2021 at 20:38):

but 6 isn't a power of 2

view this post on Zulip Kenny Lau (Jan 10 2021 at 20:38):

you see the issue here

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

view this post on Zulip Kenny Lau (Jan 10 2021 at 20:39):

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

view this post on Zulip Kenny Lau (Jan 10 2021 at 20:39):

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

view this post on Zulip Kenny Lau (Jan 10 2021 at 20:39):

therefore what I said is the correct lemma to extract

view this post on Zulip Kenny Lau (Jan 10 2021 at 20:39):

that any k/2^N satisfies the predicate

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

view this post on Zulip Kenny Lau (Jan 10 2021 at 20:41):

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

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

view this post on Zulip Kenny Lau (Jan 10 2021 at 20:42):

I'm talking about just k/2^N

view this post on Zulip Kenny Lau (Jan 10 2021 at 20:42):

where k is any integer

view this post on Zulip Kenny Lau (Jan 10 2021 at 20:42):

and N is any natural number

view this post on Zulip Kenny Lau (Jan 10 2021 at 20:42):

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

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

view this post on Zulip Kenny Lau (Jan 10 2021 at 20:45):

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

view this post on Zulip Kenny Lau (Jan 10 2021 at 20:46):

they won't be coprime at birth

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

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

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

view this post on Zulip Kenny Lau (Jan 10 2021 at 20:48):

this is what I mean

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

view this post on Zulip Kenny Lau (Jan 10 2021 at 20:51):

then the second lemma will help you a lot

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

view this post on Zulip Kenny Lau (Jan 10 2021 at 20:52):

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

view this post on Zulip Lars Ericson (Jan 10 2021 at 20:56):

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).

view this post on Zulip Kenny Lau (Jan 10 2021 at 20:58):

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

view this post on Zulip Kenny Lau (Jan 10 2021 at 20:58):

but what I wrote in Lean code should be correct

view this post on Zulip Lars Ericson (Jan 10 2021 at 20:58):

Thanks!

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

view this post on Zulip Kenny Lau (Jan 10 2021 at 21:00):

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

view this post on Zulip Kenny Lau (Jan 10 2021 at 21:00):

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

view this post on Zulip Kenny Lau (Jan 10 2021 at 21:01):

there is no point following a definition verbatim

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