Some easy rat lemmas

Stream: new members

[Way Yan]

The following results don't seem to be in mathlib. Is this ok to PR?

import data.rat.defs
import algebra.big_operators.fin

namespace rat
@[simp] theorem mk_num_denom_eq (r : ℚ) : rat.mk r.num ↑r.denom = r :=
 rat.mk_pnat_eq r.num r.denom r.pos ▸ rat.mk_pnat_pnat_denom_eq r

@[simp] theorem div_mk_div_cancel_right {a b c : ℤ} (c0 : c ≠ 0) :
  rat.mk (c * a) (c * b) = rat.mk a b :=
by rw [mul_comm c a, mul_comm c b, rat.div_mk_div_cancel_left c0]

@[simp] theorem pow_def {a b : ℤ} {n : ℕ} (b0 : b ≠ 0) :
  (rat.mk a b) ^ n = rat.mk (a ^ n) (b ^ n) :=
begin
  induction n with i hi,
  { simp },
  repeat {rw pow_succ},
  rwa [hi, rat.mul_def],
  exact pow_ne_zero i b0
end

theorem sum_same_denom {n : ℕ} {num : fin (n + 1) → ℤ} {denom : ℤ} :
  finset.univ.sum (λ x : fin (n + 1), rat.mk (num x) denom) =
  rat.mk (finset.univ.sum (λ x : fin (n + 1), num x)) denom := by {
  induction n with i hi,
  { repeat {rw fin.sum_univ_one} },
  repeat {rw @fin.sum_univ_succ _ _ i.succ _},
  repeat {rw rat.add_mk},
  congr,
  apply hi,
}
end rat

[Alex J. Best]

These results seem fairly useful, you should PR them! Did you look at the #style guide yet? You should try and follow that advice where possible.
Some comments:

• mk_num_denom_eq is the same as docs#rat.num_denom apart from the implicitness of r
• div_mk_div_cancel_right likely won't work well as a simp lemma as the condition c \ne 0 likely isn't provable by simp (you can check this sort of thing by typing #simp (rat.mk 1 2) ^ 2 to see that your simp lemma pow_def is also not working)
• pow_def doesn't need b \ne 0 as an extra condition, you can prove it in both cases with

  by_cases b0 : b = 0,
  { cases n; simp [b0], },

at the start of the proof

• div_mk_div_cancel_right should be called rat.mk_mul_mul_cancel maybe?
• sum_same_denom should use begin... end rather than by {} as the proof is long.
• sum_same_denom should be called something like rat.sum_mk_left_eq
• sum_same_denom should probably be generalised to more general finsets than just univ in fin (n+1) (I guess any finset is fine?)

theorem sum_mk_left_eq {M : Type*} {num : M → ℤ} {S : finset M} {denom : ℤ} :
  S.sum (λ x : M, rat.mk (num x) denom) =
  rat.mk (S.sum (λ x, num x)) denom :=
begin
  classical,
  induction S using finset.induction with a S ha ih,
  { simp },
  { rw [finset.sum_insert ha, finset.sum_insert ha, ih, rat.add_mk], }
end

[Way Yan]

Thanks for the feedback! I'll take a look at the #style guide

[Way Yan]

Wow I somehow missed rat.num_denom even though I combed through that page multiple times

[Alex J. Best]

I used tactic#library_search to find it, as I had a feeling it should already exist

[Way Yan]

btw regarding div_mk_div_cancel_right, I named it as such to be consistent with the existing result rat.div_mk_div_cancel_left

[Way Yan]

also, I'm not sure how to get induction to work for arbitrary finsets (I'm guessing you're supposed to use finset.card)

[Damiano Testa]

Or maybe docs#finset.induction_on?

[Alex J. Best]

Did you see I put a proof at the end of the message?

[Way Yan]

oops, I missed that part

[Way Yan]

So this is what I have now:

import data.rat.defs
import algebra.big_operators.fin

open_locale rat
open_locale big_operators

namespace rat
theorem div_mk_div_cancel_right {a b c : ℤ} (c0 : c ≠ 0) :
  (c * a) /. (c * b) = a /. b :=
by rw [mul_comm c a, mul_comm c b, rat.div_mk_div_cancel_left c0]

theorem pow_def {a b : ℤ} {n : ℕ} : (a /. b) ^ n = (a ^ n) /. (b ^ n) :=
begin
  by_cases b0 : b = 0,
  { cases n; simp [b0] },
  induction n with i hi,
  { simp },
  repeat {rw pow_succ},
  rwa [hi, rat.mul_def],
  exact pow_ne_zero i b0
end

theorem sum_mk_left_eq {M : Type*} {num : M → ℤ} {S : finset M} {denom : ℤ} :
  ∑ x in S, (num x) /. denom = (∑ x in S, num x) /. denom :=
begin
  classical,
  induction S using finset.induction with a S ha ih,
  { simp },
  { rw [finset.sum_insert ha, finset.sum_insert ha, ih, rat.add_mk], }
end
end rat

[Reid Barton]

What's the motivation for these lemmas? I would say you should basically never use /. (prefer /)

[Way Yan]

/. is the notation used for rat.mk (as mentioned here)

[Way Yan]

I needed those lemmas while formalising a simple theorem

[Mario Carneiro]

That doesn't really answer the question. /. is an implementation detail of rat, you shouldn't need to use it directly

[Way Yan]

I'm a little confused now. What should I use then, given that I also used rat.mk earlier on?

[Mario Carneiro]

Why are you using rat.mk / /. at all?

[Mario Carneiro]

all your theorems make direct reference to it so it's not clear what lead you down this path

[Way Yan]

For context, I was trying to prove that if some rational $r=p/q$ (with $p,q$ coprime) is a root of a degree $n$ monic polynomial $p$ with integer coefficients, then $q=1$. I wanted to perform the computation $p(r) = \sum_i a_i(p/q)^i = \sum_i a_i(p^i/q^i) = \sum_i a_ip^iq^{n-i}/q^n = (\sum_i a_ip^iq^{n-i})/q^n$, and for that I needed all three lemmas.

[Mario Carneiro]

What happens if you just use / instead of /.?

[Mario Carneiro]

all those steps seem like they wouldn't care if it was /

[Way Yan]

The proof breaks sadly

[Damiano Testa]

Besides the question about /., docs#denoms_clearable_nat_degree might be useful.

[Mario Carneiro]

Use docs#rat.num_div_denom instead of docs#rat.num_denom

[Mario Carneiro]

Way Yan said:

The proof breaks sadly

be more specific

[Way Yan]

Ok I'll try that

[Way Yan]

Mario Carneiro said:

Way Yan said:

The proof breaks sadly

be more specific

For example in the proof of rat.div_mk_div_cancel_right, the call to rat.div_mk_div_cancel_left breaks. But I guess I could fix that

[Mario Carneiro]

of course you won't be using exactly the same lemmas; the question is whether analogous lemmas do or should exist

[Damiano Testa]

I suspect that what Mario is hinting at is that you should go to the first time that /. appeared in your argument and make it not appear instead.

[Way Yan]

Ok will try that

[Damiano Testa]

(and then keep making it not appear! :smile: )

[Way Yan]

Can I ask what's the difference between / and /. then?

[Kyle Miller]

/. is used in the implementation of rationals, but you're meant to interact with rationals using /, at least that's my understanding

[Kyle Miller]

For example, (num x / denom : ℚ) will give you a rational

[Kevin Buzzard]

@Way Yan there might be lots of ways to state one mathematical theorem in Lean. But there will probably be a "preferred" way, and the reason to use the preferred way is that this will use the functions about which there will be lots of useful lemmas. It's a bit of an art figuring out the "preferred" way, often people do it by reading the source code to find out eg simp normal forms and so on (or just by asking and learning from example). This sort of way of thinking completely passed me by when I was learning lean and it only all dawned on me later. For example nat.succ is really important for early development of naturals, but the moment you've got things going you'd be much better off using x+1 because then the ring tactic will work. rat.mk falls into the same category.

[Reid Barton]

Ideally, they could find out from the documentation, too