Use of is_coprime in rat.basic

Stream: general

[Ender Doe]

Hello :wave:

I have been working on a small contribution to the rat api. And I have a question about dependencies .

For context here is the MWE

import data.rat.basic
import ring_theory.int.basic

@[simp]
theorem rat.denom_add_int (z: ℤ) (q : ℚ) : (q + z).denom = q.denom :=
begin
  rw rat.add_num_denom,
  simp only [mul_one, rat.coe_int_denom, int.coe_nat_zero, rat.coe_int_num,
    int.coe_nat_succ, zero_add],
  exact_mod_cast (rat.denom_div_eq_of_coprime
    (show (q.denom : ℤ) > 0, by exact_mod_cast q.pos)
    $ int.coprime_iff_nat_coprime.mp $ is_coprime.add_mul_left_left
    (int.coprime_iff_nat_coprime.mpr $ by exact_mod_cast q.cop ) _),
end

I have run into the following issue. The is_coprime api is under ring_theory and not accessible in rat.data.basic. Presumably this is due to the dependency order of the lean files. There seem to be 2 ways to resolve this problem.

1. Create a new file in the rat folder with this dependency .
2. Find a way to show the same thing using nat.gcd .

I tried 2 for a bit and it felt like reinventing the wheel, however based on the theorem statement alone, I would expect this sort of thing to live in the basic file. The is_coprime api seems really useful for proving these sort of things, I think the lemmas about rationals could benefit a lot from it.

Is there consensus on how to resolve these chicken or egg type problems?

[Yaël Dillies]

Have you tried induction on z? This seems like a low-powered of proving this specific lemma. Else, importing more files about abstract theory in files about concrete structures (which is what you're doing here) is often fine.

[Yaël Dillies]

But also adding new files is cheap. In that case, data.rat.basic is of medium size and I can't see an obvious split.

[Eric Wieser]

Can't you put it in the same file as docs#rat.denom_div_eq_of_coprime?

[Eric Wieser]

Or is the problem that docs#is_coprime exists but not its API?

[Ender Doe]

I believe rat.basic uses nat.coprime which is a smaller nat specific thing, with fewer available lemmas. The file
ring_theory.coprime defines the proper relationship here. Which is not available in rat.basic.

[Eric Wieser]

ring_theory.coprime looks like it should benefit from a split

[Eric Wieser]

ring_theory.coprime looks like it should benefit from a split

[Yaël Dillies]

I'll have a look. I love cutting stuff in half.

[Eric Rodriguez]

Where are you proposing a split Eric? It seems all fairly elementary

[Eric Wieser]

Avoiding the fintype or big_operator imports might be sensible

[Ender Doe]

I am also happy to help contribute here.

However the effort to split the file will be much larger than directly proving the denom lemma surely.

[Eric Wieser]

#9403