integral rats

Stream: general

[Johan Commelin]

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]

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

[Johan Commelin]

Thanks!

[Johan Commelin]

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]

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]

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

[Johan Commelin]

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]

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]

I am using the lemma backwards though...

[Patrick Massot]

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

[Paul-Nicolas Madelaine]

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]

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]

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]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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