where should these lemmas go

Stream: general

[Kevin Kappelmann]

Can someone please advise me where the following lemmas should live in mathlib and if the naming/tagging is correct (proofs omitted):

@[simp]
lemma rat.div_num_denom_eq_div_nat_int (n : ℤ) (d : ℕ) :
  (rat.mk n d).num / (rat.mk n d).denom = n / d := sorry

@[simp]
lemma rat.floor_eq_num_div_denom (n : ℤ) (d : ℕ) : ⌊rat.mk n d⌋ = n / d := sorry

lemma mod_eq_sub_mul_floor_rat (n : ℤ) (d : ℕ) : n % d = n - d * ⌊rat.mk n d⌋ := sorry

lemma coprime_sub_mul_floor {n d : ℕ} (n_coprime_d : n.coprime d) :
  ((n : ℤ) - d * ⌊rat.mk n d⌋).nat_abs.coprime d := sorry

Thank you :)

[Kevin Buzzard]

So let me say first that I have had very little experience of PR'ing to mathlib and you will want to get some more experienced voices before doing anything. But here's my two cents:

I would instinctively say "put stuff like this in data.rat.basic" but that file is already over 1000 lines long. Maybe it's time to split it into more than one file? We have the directory data/rat now.

Actually, looking at it a bit closer, maybe it should be reformulated a bit. My instinct is that one should prove ⌊ q ⌋ = q.num / q.denom (which seems like a cleaner statement, there are no n's and d's involved, and library_search doesn't seem to find this) and then the first lemma follows from this and the second lemma, which makes me wonder whether the first lemma is needed at all. I'm wondering whether it's best to include just the second lemma and this ⌊ q ⌋ = q.num / q.denom statement because they are both quite succinct, and I could imagine that they could both go in data.rat.basic or data.rat.basic2 if it gets split.

The third lemma is an easy consequence of the second lemma and int.mod_add_div I guess, so my instinct is that the natural results are there and the user can put them together if they want the 3rd result. Similarly the 4th result is not really a result about rationals, if you use the second statement then it becomes an assertion about integers which could go in data.int.gcd or something, if it's not already there.

PS while writing this answer I discovered that data.int.basic imports algebra.field. Not what I would have guessed.

[Kevin Buzzard]

Hmm, I see that I suggested that some lemmas involving floors could go in data.rat.basic but that's no good because the floor stuff is defined in algebra/archimedean.lean which imports data.rat.basic. So the floor rational stuff would have go to in there I guess.

[Kevin Kappelmann]

Alright, thanks for the pointers. I'll pick my best guess from the mentioned folders then and be prepared for some PR discussion :p

rat.floor is actually defined as q.num / q.denom, so that's pretty simple:

example {q : ℚ} : ⌊q⌋ = q.num / q.denom := by { cases q, refl }

however, it does not hold that (rat.mk n d).num = n (and similar for .denom) since rat.mk has to create a coprime pair (num : int , denom : nat). But it still holds that (rat.mk n d).num / (rat.mk n d).denom = n / d, which is my first lemma.

[Mario Carneiro]

You can still simplify the first lemma using Kevin's lemma, to ⌊rat.mk n d⌋ = n / d

[Mario Carneiro]

which makes it the same as the second lemma, hence why Kevin says it's not necessary

[Mario Carneiro]

You should swap the order to q.num / q.denom = ⌊q⌋ if you want these to be simp lemmas though

[Kevin Kappelmann]

You should swap the order to q.num / q.denom = ⌊q⌋ if you want these to be simp lemmas though

Should ⌊rat.mk n d⌋ = n / d or n / d = ⌊rat.mk n d⌋ or neither be a simp lemma? I would have picked the first one since it seems easier for me to deal with the division rather than rat.mk combined with floor

[Mario Carneiro]

I agree. Notice that if ⌊rat.mk n d⌋ = n / d and q.num / q.denom = ⌊q⌋ are both simp lemmas, then (rat.mk n d).num / (rat.mk n d).denom = n / d is proven by simp

[Kevin Kappelmann]

I would instinctively say "put stuff like this in data.rat.basic" but that file is already over 1000 lines long. Maybe it's time to split it into more than one file? We have the directory data/rat now.

I think it is time. I made a PR to split it.

[Johan Commelin]

You can use default.lean to export a "default" set of files. (Which can then be imported using import data.rat.)

[Johan Commelin]

I guess a next (and tedious) step, is to minimize the import data.rat.* in the rest of the library. But olean-rs might be able to help with that.

[Kevin Kappelmann]

Yeah, I was a bit afraid of changing basic.lean to default.lean since every rat.basic import then needs to be changed. Should I create default.lean that just imports basic.lean for now?

[Chris Hughes]

I would at least import basic and order.

[Johan Commelin]

@Kevin Kappelmann I find it hard to say, atm. I think you said there was some sort of (almost) import loop? What was it exactly?

[Johan Commelin]

Because that might help in determining how to structure things.

[Kevin Kappelmann]

Imports where OK; just Kevin B. noticed:

PS while writing this answer I discovered that data.int.basic imports algebra.field. Not what I would have guessed.

Hmm, I see that I suggested that some lemmas involving floors could go in data.rat.basic but that's no good because the floor stuff is defined in algebra/archimedean.lean which imports data.rat.basic. So the floor rational stuff would have go to in there I guess.

My idea was:
- data.rat.field defines the field structure
- data.rat.order defines the order and related functions
- data.rat.cast defines the casts
- data.rat.floor_ceil defines floor and ceil functions
- data.rat.basic imports the previous four.

If we want to have data.rat.default, my proposal is to just import data.rat.basic from data.rat.default for now and in a different PR update the data.rat.basic and data.rat.* imports.

[Chris Hughes]

If you don't want to break anything, isn't it best to import all of them from default at the moment, and change imports from data.rat.basic to data.rat.default and then minimise the imports in a separate PR.

[Kevin Kappelmann]

OK, doing some quick search, I think fixing the imports shouldn't be difficult. Gimme a few mins.

[Johan Commelin]

Does this help removing algebra.field as import from data.int.basic?

[Kevin Kappelmann]

Nope, that's unrelated to this PR

[Johan Commelin]

Ok, I see.

[Kevin Kappelmann]

I changed basic to default and floor_ceil to floor now in the new version.

[Johan Commelin]

@Kevin Kappelmann We're still in the process of figuring out what exactly we want to document. We just had a change in policy. My apologies for confusing questions/remarks on your PR. It's a bit of a playground/testing ground.

[Mario Carneiro]

I don't see why we need to remove the algebra.field import. That's basically the definition of field as a structure (or would be if it wasn't in core already)

[Mario Carneiro]

and obviously rat is a field and that's pretty integral to the definition. We aren't so bootstrapped that we need to separate the type rat from the field rat

[Chris Hughes]

That's why I suggested data/rat/field should be called data/rat/basic. Just looking, this hasn't actually been done yet.

[Chris Hughes]

Especially since that file also contains the definition of rat

[Kevin Kappelmann]

So everyone agrees I should rename rat.field to rat.basic - is that right?

[Chris Hughes]

I think so.

[Mario Carneiro]

I am not sure I see the argument for splitting the file, but the name suggestions seem alright

[Chris Hughes]

I think the argument is that floor will be able to import algebra.archimedean

[Chris Hughes]

Personally I would actually state the lemma @[simp] lemma rat.floor_eq_num_div_denom (n : ℤ) (d : ℕ) : ⌊rat.mk n d⌋ = n / d := sorry differently. I would just add a simp lemma turning rat.mk n d into (n : rat) / d and then a lemma turning ⌊n / d⌋ = (n : int) / d in any ordered field. I'm not sure why you'd want to use rat.mk instead of division.

[Kevin Kappelmann]

So everyone agrees I should rename rat.field to rat.basic - is that right?

updated the PR with this

[Kevin Kappelmann]

I am not sure I see the argument for splitting the file, but the name suggestions seem alright

I was about to add lemmas to data.rat.basic and the sequence of statements in data.rat.basic made it non-trivial to integrate them. Making smaller, coherent files makes adding changes way easier + it is easier to find and document things.

[Mario Carneiro]

the current file is stated in a logical order, with subheadings. Could you be more specific?

[Mario Carneiro]

It predates the new doc requirements though

[Mario Carneiro]

My point is mostly that making more files with the same content does not on its own make anything better. It's just trading one organizational scheme for another, and you can be equally convoluted either way

[Mario Carneiro]

The biggest thing you lose with moving to mini files is the explicit dependency order. Filesystems just show the files in alphabetical order, and you can't see what comes first anymore

[Kevin Kappelmann]

For example, things like

lemma num_denom_mk {q : ℚ} {n d : ℤ} (hn : n ≠ 0) (hd : d ≠ 0) (qdf : q = n /. d) :
      ∃ c : ℤ, n = c * q.num ∧ d = c * q.denom :=

were not stated at the top where rat.mk is defined, but somewhere at the bottom, sections of coercions, floor functions, etc in-between, making it really difficult to find the lemma.
Another example: there was a section about coercions randomly appearing between the ceil and nat_ceil section, obfuscating the connection.

[Kevin Kappelmann]

The biggest thing you lose with moving to mini files is the explicit dependency order. Filesystems just show the files in alphabetical order, and you can't see what comes first anymore

My take is that If that's the main thing you miss, then that should be fixed by, e.g. a tactic outputting dependency graphs rather than giving up on easier maintenance of smaller files.

[Mario Carneiro]

I agree; those last theorems involving num and denom look tacked on, perhaps the author didn't know where to put them

[Mario Carneiro]

When I originally wrote the file I didn't say much about rat.mk beyond the basics because it's supposed to be an implementation detail. I'm not sure why all these lemmas are exposing it

[Kevin Kappelmann]

I finally came back to fix these lemmas and ran into the following rewriting issue:

lemma floor_div_eq_div {n : ℤ} {d : ℕ} : ⌊(n : ℚ) / d⌋ = n / d :=
begin
  -- rw [rat.floor_def], -- this fails
  rw [(show ⌊(n : ℚ) / d⌋ = _, from rat.floor_def)], -- this works
  sorry
end

Maybe this is also related to this issue that Patrick and I ran into a few weeks ago. Any idea what's going on here?

[Floris van Doorn]

The problem here is that ⌊ ... ⌋ means floor_ring.floor, but rat.floor_def is defined using rat.floor. These two functions are definitionally equal, but you will have to unfold some instances (namely, floor_ring ℚ) to figure that out.
rw will do (almost) no unfolding of definitions, so on the first line, it cannot match rat.floor with floor_ring.floor. On the second line, you proof an equality involving floor_ring.floor (the proof works, since the two definitions are definitionally equal), and then rewrite is happy, because the equality you're rewriting with now only involves floor_ring.floor.

This issue is avoided in other situations by defining the instance floor_ring.floor as quickly as possible after rat.floor, and from then on only using floor_ring.floor and never rat.floor. An uglier work-around is to reprove rat.floor_def after the instance is declared using floor_ring.floor.

[Kevin Kappelmann]

Thanks, that does make a lot of sense! :)

[Kevin Kappelmann]

So now I have these three lemmas:

lemma inv_def' {q : ℚ} : q⁻¹ = (q.denom : ℚ) / q.num := sorry

lemma div_lt_div_iff_mul_lt_mul {a b c d : ℤ} (b_pos : 0 < b) (d_pos : 0 < d) :
  (a : ℚ) / b < c / d ↔ a * d < c * b := sorry

@[simp] lemma mul_own_denom_eq_num {q : ℚ} : q * q.denom = q.num := sorry

All the proofs are quite simple if one imports data.rat.cast. Semantically, however, they obviously should not live in data.rat.cast. Are these lemmas good candidates for data.rat.default or should that file stay completely empty besides a list of imports?

[Floris van Doorn]

I would suggest moving properties about coercions into rat (from int and nat) to rat.basic and then just add these lemmas there. Then rat.cast is only about the cast from the rationals to other types. I would expect these kind of lemmas, which are basic equational rules, to be in rat.basic.

[Kevin Kappelmann]

That sounds sensible. I'll give it a shot. Cheers :)