# Zulip Chat Archive

## 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

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

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