## Stream: general

### Topic: integral rats

#### Johan Commelin (Jun 18 2019 at 02:20):

This proof is certainly becoming too long and annoying:

lemma rat.coe_num_eq_iff (r : ℚ) : (r.num : ℚ) = r ↔ r.denom = 1 :=
begin
split,
{ intro h,
rw [rat.coe_int_eq_mk, rat.num_denom r, rat.mk_eq] at h,
{ cases r with n d p c, show d = 1,
change (rat.mk n d).num * d = n * 1 at h,
sorry },
{ exact one_ne_zero },
{ apply ne_of_gt, exact_mod_cast r.pos } },
{ intro h,
rw [← rat.cast_of_int, rat.num_denom r, h, ← rat.mk_nat_eq],
norm_cast, delta rat.of_int rat.mk_nat, congr,
simp only [nat.gcd_one_right, int.nat_abs, nat.div_one] },
end


Can someone unsorry and/or golf this?

#### Floris van Doorn (Jun 18 2019 at 03:31):

import data.rat tactic.norm_num

lemma mul_eq_mul_left {α} [integral_domain α] {a b c : α} (ha : a ≠ 0) :
a * b = a * c ↔ b = c :=
⟨eq_of_mul_eq_mul_left ha, λ h, by rw h⟩

open rat
lemma rat.coe_num_eq_iff (r : ℚ) : (r.num : ℚ) = r ↔ r.denom = 1 :=
begin
rw [coe_int_eq_mk r.num], conv_lhs { to_rhs, rw [num_denom r] },
by_cases h : r.num = 0,
{ simpa [h] using r.cop },
{ rw [mk_eq, mul_eq_mul_left h], norm_cast, norm_num, simpa using denom_ne_zero r }
end


edit: further golfing

Thanks!

#### Johan Commelin (Jun 18 2019 at 05:13):

I really need to learn these skills... Although I guess I'm already a lot better at them than one year ago :expressionless:

#### Johan Commelin (Jun 18 2019 at 05:56):

Hmmm, sleep also seems to help. I now have my attempt down to:

lemma rat.coe_num_eq_iff (r : ℚ) : (r.num : ℚ) = r ↔ r.denom = 1 :=
begin
split; intro h,
{ rw ← h, apply rat.coe_int_denom },
{ rw [← rat.cast_of_int, rat.num_denom r, h, ← rat.mk_nat_eq],
norm_cast, delta rat.of_int rat.mk_nat, congr,
simp only [nat.gcd_one_right, int.nat_abs, nat.div_one] },
end


#### Paul-Nicolas Madelaine (Jun 18 2019 at 13:40):

@Johan Commelin you can also close you first subgoal with norm_cast instead of applying coe_int_denom directly

#### Johan Commelin (Jun 18 2019 at 14:09):

Thanks! :smiley:

lemma rat.coe_num_eq_iff (r : ℚ) : (r.num : ℚ) = r ↔ r.denom = 1 :=
begin
split; intro h,
{ rw_mod_cast ← h, refl },
{ rw_mod_cast [← rat.cast_of_int, rat.of_int], cases r with n d p c, congr, exact h.symm },
end


#### Patrick Massot (Jun 18 2019 at 14:10):

Isn't it weird that rw_mod_cast need a lemma whose name includes "cast"? Should this lemma be marked for norm_cast use?

#### Johan Commelin (Jun 18 2019 at 14:11):

I am using the lemma backwards though...

#### Patrick Massot (Jun 18 2019 at 14:13):

norm_cast handles this. You need to state it in the direction indicated by documentation and then never care again

#### Paul-Nicolas Madelaine (Jun 18 2019 at 16:59):

norm_cast can't handle this, rat.cast_of_int is not a norm_cast lemma.
the reason is that norm_cast never tries to unfold coercions.

I tried to make a simplier version of the proof, but I get a weird error when trying to rewrite h:

lemma rat.coe_num_eq_iff (r : ℚ) : (r.num : ℚ) = r ↔ r.denom = 1 :=
begin
split; intro h,
{ rw ← h, norm_cast },
{ cases r with r d,
simp only [] at h ⊢,
simp only [h], --error when I try to use rw
rw ← rat.cast_of_int, norm_cast }
end


#### Kevin Buzzard (Jun 18 2019 at 18:56):

You are trying to rewrite the term {num := r, denom := d, pos := r_pos, cop := r_cop}. Here r_cop is a proof that r and d are coprime. Your h is a proof of d=1 so if you do the naive rewrite then denom will become 1 but r_cop will still be a proof that r and d are coprime, so this term is no longer meaningful.

#### Kevin Buzzard (Jun 18 2019 at 18:58):

The two standard tricks to fix this issue are erw h and simp only [h], each of which may or may not work. Here erw does not but simp only does. Another cool trick, which works if h is of the form variable = term, is subst h; this also works in your case.

#### Kevin Buzzard (Jun 18 2019 at 18:59):

subst is very cool, it rewrites every occurrence of d in everything.

#### Kevin Buzzard (Jun 18 2019 at 19:01):

This phenomenon is somehow the achilles heel of dependent type theory.

#### Mario Carneiro (Jun 18 2019 at 20:24):

This is why you should use rat.mk' and the num_denom_cases_on functions instead of straight cases

#### Kevin Buzzard (Jun 18 2019 at 20:33):

Aah yes, for some reason the default constructor for rat is a bit bonkers, probably because it is the only one which avoids quotients

Last updated: May 11 2021 at 23:11 UTC