Zulip Chat Archive

Stream: general

Topic: integral rats


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

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

view this post on Zulip Johan Commelin (Jun 18 2019 at 05:11):

Thanks!

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

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

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

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

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

view this post on Zulip Johan Commelin (Jun 18 2019 at 14:11):

I am using the lemma backwards though...

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

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

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

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

view this post on Zulip Kevin Buzzard (Jun 18 2019 at 18:59):

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

view this post on Zulip Kevin Buzzard (Jun 18 2019 at 19:01):

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

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

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