## Stream: general

### Topic: where should these lemmas go

#### Kevin Kappelmann (Jul 29 2019 at 16:27):

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 (Jul 29 2019 at 17:23):

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 (Jul 29 2019 at 17:27):

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 (Jul 29 2019 at 20:16):

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 (Jul 29 2019 at 22:56):

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

#### Mario Carneiro (Jul 29 2019 at 22:58):

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

#### Mario Carneiro (Jul 29 2019 at 22:59):

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

#### Kevin Kappelmann (Jul 30 2019 at 08:41):

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 (Jul 30 2019 at 09:01):

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 (Jul 30 2019 at 11:36):

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 (Jul 30 2019 at 11:43):

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

#### Johan Commelin (Jul 30 2019 at 11:44):

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 (Jul 30 2019 at 11:45):

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 (Jul 30 2019 at 11:46):

I would at least import basic and order.

#### Johan Commelin (Jul 30 2019 at 11:50):

@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 (Jul 30 2019 at 11:51):

Because that might help in determining how to structure things.

#### Kevin Kappelmann (Jul 30 2019 at 11:55):

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 (Jul 30 2019 at 11:58):

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 (Jul 30 2019 at 12:01):

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

#### Johan Commelin (Jul 30 2019 at 12:02):

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

#### Kevin Kappelmann (Jul 30 2019 at 12:08):

Nope, that's unrelated to this PR

Ok, I see.

#### Kevin Kappelmann (Jul 30 2019 at 12:18):

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

#### Johan Commelin (Jul 30 2019 at 12:35):

@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 (Jul 30 2019 at 12:57):

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 (Jul 30 2019 at 12:58):

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 (Jul 30 2019 at 13:00):

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 (Jul 30 2019 at 13:01):

Especially since that file also contains the definition of rat

#### Kevin Kappelmann (Jul 30 2019 at 13:03):

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

I think so.

#### Mario Carneiro (Jul 30 2019 at 13:04):

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

#### Chris Hughes (Jul 30 2019 at 13:05):

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

#### Chris Hughes (Jul 30 2019 at 13:08):

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 (Jul 30 2019 at 13:09):

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

updated the PR with this

#### Kevin Kappelmann (Jul 30 2019 at 13:10):

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 (Jul 30 2019 at 13:13):

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

#### Mario Carneiro (Jul 30 2019 at 13:14):

It predates the new doc requirements though

#### Mario Carneiro (Jul 30 2019 at 13:15):

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 (Jul 30 2019 at 13:17):

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 (Jul 30 2019 at 13:21):

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 (Jul 30 2019 at 13:24):

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 (Jul 30 2019 at 23:02):

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

#### Mario Carneiro (Jul 30 2019 at 23:03):

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 (Aug 14 2019 at 14:05):

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 (Aug 14 2019 at 18:13):

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 (Aug 14 2019 at 19:53):

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

#### Kevin Kappelmann (Aug 19 2019 at 14:22):

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 (Aug 19 2019 at 14:39):

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 (Aug 19 2019 at 14:51):

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

Last updated: May 08 2021 at 04:14 UTC