Zulip Chat Archive

Stream: new members

Topic: nat.rfl.dvd


view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Apr 09 2021 at 09:42):

anyway the lemma should be called nat.dvd_refl

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 09 2021 at 09:44):

(unless it happens to come up during bootstrapping)

view this post on Zulip Kevin Buzzard (Apr 09 2021 at 09:44):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 09 2021 at 09:44):

prelude?

view this post on Zulip Mario Carneiro (Apr 09 2021 at 09:44):

what file are you working on?

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 09 2021 at 09:44):

There aren't any prelude files in mathlib

view this post on Zulip Mario Carneiro (Apr 09 2021 at 09:45):

Oh this is init.data.nat.lemmas

view this post on Zulip Kevin Buzzard (Apr 09 2021 at 09:45):

That's core Lean!

view this post on Zulip Damiano Testa (Apr 09 2021 at 09:45):

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

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip Mario Carneiro (Apr 09 2021 at 09:46):

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

view this post on Zulip Mario Carneiro (Apr 09 2021 at 09:46):

and you should already have dvd_refl available in that file

view this post on Zulip Mario Carneiro (Apr 09 2021 at 09:47):

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

view this post on Zulip 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!

view this post on Zulip 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)

view this post on Zulip Damiano Testa (Apr 09 2021 at 09:49):

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

view this post on Zulip Damiano Testa (Apr 09 2021 at 09:50):

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

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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 (-;

view this post on Zulip Damiano Testa (Apr 09 2021 at 10:01):

What do you need to do to upgrade elan?

view this post on Zulip Johan Commelin (Apr 09 2021 at 10:02):

elan update

view this post on Zulip Damiano Testa (Apr 09 2021 at 10:03):

Also, PR #7132!

view this post on Zulip 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:

view this post on Zulip 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...

view this post on Zulip Mario Carneiro (Apr 09 2021 at 10:07):

Isn't that just a monoid?

view this post on Zulip Johan Commelin (Apr 09 2021 at 10:08):

@Mario Carneiro I mean that units M has cardinality 1

view this post on Zulip Kevin Buzzard (Apr 09 2021 at 10:08):

Maybe it's a distrib-monoid

view this post on Zulip Mario Carneiro (Apr 09 2021 at 10:08):

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

view this post on Zulip Johan Commelin (Apr 09 2021 at 10:08):

But I guess semiring can be weakened to div_monoid.

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Apr 09 2021 at 10:10):

We should make a type alias for that

view this post on Zulip Johan Commelin (Apr 09 2021 at 10:10):

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

view this post on Zulip Damiano Testa (Apr 09 2021 at 10:10):

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

view this post on Zulip Johan Commelin (Apr 09 2021 at 10:10):

And polynomial (zmod 2), I guess

view this post on Zulip Kevin Buzzard (Apr 09 2021 at 10:10):

mv_polynomial S nat

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Apr 09 2021 at 10:11):

The nat_dvd_iff_eq lemma is just true in all partial orders

view this post on Zulip Mario Carneiro (Apr 09 2021 at 10:11):

you don't need inf/sup for that

view this post on Zulip Johan Commelin (Apr 09 2021 at 10:12):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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...

view this post on Zulip Damiano Testa (Apr 09 2021 at 10:13):

partial orders can have loops?

view this post on Zulip Mario Carneiro (Apr 09 2021 at 10:13):

Oh, good point about the preorder issue

view this post on Zulip Damiano Testa (Apr 09 2021 at 10:13):

I am worried about non-cancellative stuff.

view this post on Zulip 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

view this post on Zulip Damiano Testa (Apr 09 2021 at 10:14):

maybe no_zero_divisors is good enough?

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 09 2021 at 10:16):

which would be the case for nat, for instance

view this post on Zulip 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