## Stream: new members

### Topic: nat.rfl.dvd

#### Damiano Testa (Apr 09 2021 at 09:35):

Dear All,

I wanted to extract the lemma below about natural numbers from PR #7082. The natural place would seem to be data/nat/lemmas. As you can see, the proof uses dvd_refl which is the statement n | n. However, this lemma appears in larger generality and is not imported by data/nat/lemmas. Should the nat-version of rfl.dvd be also added? Is there a reason that it is not there?

Thanks!

-- lemma to be extracted from PR
lemma nat_dvd_iff_eq {m n : ℕ} : (∀ a : ℕ, m ∣ a ↔ n ∣ a) ↔ m = n :=
⟨λ h, nat.dvd_antisymm ((h _).mpr (dvd_refl _)) ((h _).mp (dvd_refl _)), λ h n, by rw h⟩

-- auxiliary lemma?
lemma rfl.dvd (n : ℕ) : n ∣ n := ⟨1, (mul_one _).symm⟩


#### Mario Carneiro (Apr 09 2021 at 09:42):

How could it not import dvd_refl? I would assume it is in the same file that defines dvd, so how are you getting dvd on nat in that case?

#### Mario Carneiro (Apr 09 2021 at 09:42):

anyway the lemma should be called nat.dvd_refl

#### Mario Carneiro (Apr 09 2021 at 09:43):

We don't usually prove the nat version of a lemma if it is an application of the generic lemma

#### Mario Carneiro (Apr 09 2021 at 09:44):

(unless it happens to come up during bootstrapping)

#### Kevin Buzzard (Apr 09 2021 at 09:44):

There's a root namespace dvd_refl in algebra.divisibility which applies to all monoids.

#### Damiano Testa (Apr 09 2021 at 09:44):

I must have messed something up, but this is the beginning of the file that VSCode opens, when I tell it to open data/nat/lemmas:

prelude
import init.data.nat.basic init.data.nat.div init.meta init.algebra.functions


prelude?

#### Mario Carneiro (Apr 09 2021 at 09:44):

what file are you working on?

#### Damiano Testa (Apr 09 2021 at 09:44):

Hoewever, if I look at the path of the file, I see this:
/home/damiano/.elan/toolchains/leanprover-community-lean-3.28.0/lib/lean/library/init/data/nat/lemmas.lean

#### Mario Carneiro (Apr 09 2021 at 09:44):

There aren't any prelude files in mathlib

#### Mario Carneiro (Apr 09 2021 at 09:45):

Oh this is init.data.nat.lemmas

#### Kevin Buzzard (Apr 09 2021 at 09:45):

That's core Lean!

#### Damiano Testa (Apr 09 2021 at 09:45):

But I opened it by browsing to src/data/nat/lemmas.lean: something is weird...

#### Mario Carneiro (Apr 09 2021 at 09:45):

Core lean doesn't have any lemmas about nat unless they are absolutely necessary for setting up some part of the tactic framework or other core stuff

#### Damiano Testa (Apr 09 2021 at 09:46):

Ok, then I would like to add this to the non-core file, but I do not know how to open it...

#### Mario Carneiro (Apr 09 2021 at 09:46):

The main initial mathlib file about nat is data.nat.basic

#### Mario Carneiro (Apr 09 2021 at 09:46):

and you should already have dvd_refl available in that file

#### Mario Carneiro (Apr 09 2021 at 09:47):

I don't think there is a mathlib file called data.nat.lemmas

#### Damiano Testa (Apr 09 2021 at 09:49):

Ok, I think that what happened is that I clicked on "go to def" and it went to the preludefile, and, after that, I was navigating already in the wrong path. I think that I found the correct file now!

No wonder I could not use library_search!

#### Kevin Buzzard (Apr 09 2021 at 09:49):

PS Damiano, if you edited a core Lean file then be super-careful to change it back to exactly how it was, or you'll break your entire set-up (in a way which leanproject will not be able to fix)

#### Damiano Testa (Apr 09 2021 at 09:49):

I will try to be careful: I had no idea that this was a potential pitfall!

#### Damiano Testa (Apr 09 2021 at 09:50):

In fact, I do not intend to change these files: this was a mistake!

#### Kevin Buzzard (Apr 09 2021 at 09:51):

If later on you find yourself not being able to get rid of orange bars whatever you try, then come and ask for help in re-downloading Lean 3.28.0 on your system.

#### Damiano Testa (Apr 09 2021 at 09:53):

Ok, thanks! I have had difficulty working with those files, so I think that I did all my experimenting in a git.ignored file, so I am hoping that I will not have problems!

#### Johan Commelin (Apr 09 2021 at 09:59):

The latest version of elan should make those files read-only on your system. So upgrade your elans (-;

#### Damiano Testa (Apr 09 2021 at 10:01):

What do you need to do to upgrade elan?

#### Johan Commelin (Apr 09 2021 at 10:02):

elan update

Also, PR #7132!

#### Johan Commelin (Apr 09 2021 at 10:06):

@Damiano Testa Your PR is true more generally in an arbitrary semiring_with_one_unit :stuck_out_tongue_wink:

#### Damiano Testa (Apr 09 2021 at 10:07):

I actually wanted it to be a formulation of Yoneda's lemma for the category associated to the divisibility lattice on nat, but decided against the alternate proof...

#### Mario Carneiro (Apr 09 2021 at 10:07):

Isn't that just a monoid?

#### Johan Commelin (Apr 09 2021 at 10:08):

@Mario Carneiro I mean that units M has cardinality 1

#### Kevin Buzzard (Apr 09 2021 at 10:08):

Maybe it's a distrib-monoid

#### Mario Carneiro (Apr 09 2021 at 10:08):

I believe there is already a version of this lemma stated for partial orders with le

#### Johan Commelin (Apr 09 2021 at 10:08):

But I guess semiring can be weakened to div_monoid.

#### Damiano Testa (Apr 09 2021 at 10:09):

I remember that there was a discussion about putting the order structure on nat given by divisibility, but I was scared of working with a "non-standard" ordering on nat and decided not following this route.

#### Mario Carneiro (Apr 09 2021 at 10:10):

We should make a type alias for that

#### Johan Commelin (Apr 09 2021 at 10:10):

How many other such monoid are there? I guess polynomial nat is a useful one.

#### Damiano Testa (Apr 09 2021 at 10:10):

Once you have this, the lemma is a statement about existence of inf/sups, essentially.

#### Johan Commelin (Apr 09 2021 at 10:10):

And polynomial (zmod 2), I guess

#### Kevin Buzzard (Apr 09 2021 at 10:10):

mv_polynomial S nat

#### Damiano Testa (Apr 09 2021 at 10:11):

you could prove that elements that divide the same elements are associated and then get more mileage out of this.

#### Mario Carneiro (Apr 09 2021 at 10:11):

The nat_dvd_iff_eq lemma is just true in all partial orders

#### Mario Carneiro (Apr 09 2021 at 10:11):

you don't need inf/sup for that

#### Johan Commelin (Apr 09 2021 at 10:12):

Right so we need associated_iff_eq for a couple of rings (-;

#### Mario Carneiro (Apr 09 2021 at 10:12):

Any ring can be usefully turned into a partial order and a semilattice using the divisibility order

#### Johan Commelin (Apr 09 2021 at 10:12):

Marios type alias could possibly be a quotient by associated, and then we can use it for arbitrary monoids.

#### Damiano Testa (Apr 09 2021 at 10:12):

Ok, this is motivating to pull up my sleeves and actually prove this with for partial orders and using the dvd-lattice. I would like to have a hint at a start for this, though...

#### Damiano Testa (Apr 09 2021 at 10:13):

partial orders can have loops?

#### Mario Carneiro (Apr 09 2021 at 10:13):

Oh, good point about the preorder issue

#### Damiano Testa (Apr 09 2021 at 10:13):

I am worried about non-cancellative stuff.

#### Mario Carneiro (Apr 09 2021 at 10:14):

I would do it in two stages: make a preorder from the divisibility, and then make an arbitrary preorder into a partial order by quotienting

#### Damiano Testa (Apr 09 2021 at 10:14):

maybe no_zero_divisors is good enough?

#### Johan Commelin (Apr 09 2021 at 10:14):

Mario Carneiro said:

I would do it in two stages: make a preorder from the divisibility, and then make an arbitrary preorder into a partial order by quotienting

But we still need glue with associated, right?

#### Mario Carneiro (Apr 09 2021 at 10:15):

I guess you can prove that associated is either equivalent to or defeq with the equivalence on a preorder

#### Damiano Testa (Apr 09 2021 at 10:15):

ah, I was going via the route of assuming enough to avoid pathologies, but I also like the approach of getting pathological stuff and "making it work" by quotienting! Assuming that I understood Mario's approach.

#### Mario Carneiro (Apr 09 2021 at 10:15):

You can also prove that the preorder quotient is an isomorphism if the preorder is already a partial order

#### Mario Carneiro (Apr 09 2021 at 10:16):

which would be the case for nat, for instance

#### Damiano Testa (Apr 09 2021 at 10:16):

Can I suggest moving this conversation to a new topic: "semilattice, dvd, associated"? I still think that the lemma on naturals could work fine as is...

Last updated: May 13 2021 at 21:12 UTC