nat.rfl.dvd

Stream: new members

[Damiano Testa]

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]

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]

anyway the lemma should be called nat.dvd_refl

[Mario Carneiro]

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

[Mario Carneiro]

(unless it happens to come up during bootstrapping)

[Kevin Buzzard]

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

[Damiano Testa]

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

[Mario Carneiro]

prelude?

[Mario Carneiro]

what file are you working on?

[Damiano Testa]

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]

There aren't any prelude files in mathlib

[Mario Carneiro]

Oh this is init.data.nat.lemmas

[Kevin Buzzard]

That's core Lean!

[Damiano Testa]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

and you should already have dvd_refl available in that file

[Mario Carneiro]

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

[Damiano Testa]

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]

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]

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

[Damiano Testa]

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

[Kevin Buzzard]

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]

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]

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

[Damiano Testa]

What do you need to do to upgrade elan?

[Johan Commelin]

elan update

[Damiano Testa]

Also, PR #7132!

[Johan Commelin]

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

[Damiano Testa]

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]

Isn't that just a monoid?

[Johan Commelin]

@Mario Carneiro I mean that units M has cardinality 1

[Kevin Buzzard]

Maybe it's a distrib-monoid

[Mario Carneiro]

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

[Johan Commelin]

But I guess semiring can be weakened to div_monoid.

[Damiano Testa]

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]

We should make a type alias for that

[Johan Commelin]

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

[Damiano Testa]

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

[Johan Commelin]

And polynomial (zmod 2), I guess

[Kevin Buzzard]

mv_polynomial S nat

[Damiano Testa]

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

[Mario Carneiro]

The nat_dvd_iff_eq lemma is just true in all partial orders

[Mario Carneiro]

you don't need inf/sup for that

[Johan Commelin]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Damiano Testa]

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]

partial orders can have loops?

[Mario Carneiro]

Oh, good point about the preorder issue

[Damiano Testa]

I am worried about non-cancellative stuff.

[Mario Carneiro]

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]

maybe no_zero_divisors is good enough?

[Johan Commelin]

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]

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

[Damiano Testa]

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]

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

[Mario Carneiro]

which would be the case for nat, for instance

[Damiano Testa]

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