Zulip Chat Archive

Stream: maths

Topic: zmodp


view this post on Zulip Reid Barton (Mar 02 2020 at 04:19):

Would it make sense for zmodp to take a primes, rather than a pair?

view this post on Zulip Mario Carneiro (Mar 02 2020 at 04:36):

it's probably fine? there will be a lot of coercions

view this post on Zulip Reid Barton (Mar 02 2020 at 04:41):

it seems potentially a lot more convenient in a situation where some prime is fixed for a long time, since the prime will probably be inferrable from everything while a separate hp : prime p will not

view this post on Zulip Mario Carneiro (Mar 02 2020 at 04:45):

prime is a typeclass, so you can have variables (p : nat) [prime p] and it will be inferred

view this post on Zulip Johan Commelin (Mar 02 2020 at 05:44):

See also #1648

view this post on Zulip Mario Carneiro (Mar 02 2020 at 06:04):

Oh, I just noticed that you changed the definition of prime in that PR. I thought it was just @[class] def prime := ...

view this post on Zulip Yury G. Kudryashov (Mar 02 2020 at 07:23):

BTW, does it make sense to have nat.prime defined differently from prime in algebra/associated?

view this post on Zulip Yury G. Kudryashov (Mar 02 2020 at 07:24):

I think that a better approach would be to reuse the general definition, and prove equivalence to the current version of nat.prime.

view this post on Zulip Mario Carneiro (Mar 02 2020 at 07:25):

I have an innate dislike of this idea but maybe it's not well grounded

view this post on Zulip Yury G. Kudryashov (Mar 02 2020 at 07:25):

Of which idea?

view this post on Zulip Mario Carneiro (Mar 02 2020 at 07:25):

I think it should be okay but we need to be careful to keep the dependencies down

view this post on Zulip Mario Carneiro (Mar 02 2020 at 07:25):

the idea to merge the two definitions

view this post on Zulip Mario Carneiro (Mar 02 2020 at 07:26):

I don't think _root_.prime was defined in an area that was being conscientious about dependencies

view this post on Zulip Yury G. Kudryashov (Mar 02 2020 at 07:28):

OK, algebra/associated depends on multiset, and nat.prime uses list.perm relation instead of equality in multiset.

view this post on Zulip Yury G. Kudryashov (Mar 02 2020 at 07:29):

Moving definition of _root_.prime with some properties to a file not importing multiset should be easy.

view this post on Zulip Mario Carneiro (Mar 02 2020 at 07:30):

Why does nat.prime need list.perm?

view this post on Zulip Yury G. Kudryashov (Mar 02 2020 at 07:30):

For factors_unique

view this post on Zulip Mario Carneiro (Mar 02 2020 at 07:30):

I think we could split the file into two parts, with the second part dealing with complete factorizations and the unique factorization theorem

view this post on Zulip Yury G. Kudryashov (Mar 02 2020 at 07:31):

Why nat/prime should care about dependencies?

view this post on Zulip Mario Carneiro (Mar 02 2020 at 07:31):

Sometimes you just want to be able to say 5 is prime and maybe evaluate some primes

view this post on Zulip Mario Carneiro (Mar 02 2020 at 07:31):

also it's needed by norm_num

view this post on Zulip Yury G. Kudryashov (Mar 02 2020 at 07:33):

I think that we can move multisets out of algebra/associated.

view this post on Zulip Yury G. Kudryashov (Mar 02 2020 at 07:34):

About merging definitions: for a newcomer, having two definitions for the same notion is really confusing.

view this post on Zulip Mario Carneiro (Mar 02 2020 at 07:34):

Having a fancy definition for a simple concept is also confusing

view this post on Zulip Yury G. Kudryashov (Mar 02 2020 at 07:34):

E.g., it took me a lot of time to understand the situation with cau_seq and cauchy.

view this post on Zulip Mario Carneiro (Mar 02 2020 at 07:34):

see filters

view this post on Zulip Mario Carneiro (Mar 02 2020 at 07:35):

There should be a theorem that relates cau_seq and cauchy. That's how I prefer to resolve these situations

view this post on Zulip Yury G. Kudryashov (Mar 02 2020 at 07:37):

In the first place there should be a clear documentation (and for cau_seq vs cauchy, I'd use cauchy everywhere).

view this post on Zulip Mario Carneiro (Mar 02 2020 at 07:38):

I agree you should use cauchy preferentially if you are doing anything using or depending on topology

view this post on Zulip Mario Carneiro (Mar 02 2020 at 07:38):

cau_seq is mostly an implementation detail for the construction of the reals

view this post on Zulip Mario Carneiro (Mar 02 2020 at 07:38):

which escaped a bit in order to help with building the p-adic numbers

view this post on Zulip Yury G. Kudryashov (Mar 02 2020 at 07:39):

If I have h : prime p in the context and I want to apply a theorem taking prime p, then I expect it to work.

view this post on Zulip Mario Carneiro (Mar 02 2020 at 07:39):

open nat causes a lot of confusion

view this post on Zulip Johan Commelin (Mar 02 2020 at 07:40):

Is _root_.prime really that complicated?

view this post on Zulip Yury G. Kudryashov (Mar 02 2020 at 07:40):

/-- prime element of a semiring -/
def prime [comm_semiring α] (p : α) : Prop :=
p  0  ¬ is_unit p  (a b, p  a * b  p  a  p  b)

view this post on Zulip Johan Commelin (Mar 02 2020 at 07:40):

What are the dependencies of that definition that you would like to avoid?

view this post on Zulip Mario Carneiro (Mar 02 2020 at 07:41):

The definition itself is not complicated, but it's embedded in a file with many dependencies last I checked

view this post on Zulip Johan Commelin (Mar 02 2020 at 07:41):

So... merge the definitions and maybe split the file to avoid deps

view this post on Zulip Yury G. Kudryashov (Mar 02 2020 at 07:41):

import algebra.group algebra.group.is_unit data.multiset

view this post on Zulip Johan Commelin (Mar 02 2020 at 07:42):

If is_unit is too complicated because it depends on units then we could even spell it out.

view this post on Zulip Mario Carneiro (Mar 02 2020 at 07:42):

actually my memory is faulty or else I missed the refactor because it's in the algebra directory now and the imports are not as bad as I thought

view this post on Zulip Yury G. Kudryashov (Mar 02 2020 at 07:42):

Actually data.multiset depends on lots of things, including group_power.

view this post on Zulip Mario Carneiro (Mar 02 2020 at 07:43):

yeah, that's definitely the biggest dependency in the list

view this post on Zulip Mario Carneiro (Mar 02 2020 at 07:43):

group_power is hard to avoid when talking about prime numbers

view this post on Zulip Mario Carneiro (Mar 02 2020 at 07:45):

but actually there are a lot of imports in data.multiset that have creeped in about algebra that are surprising

view this post on Zulip Mario Carneiro (Mar 02 2020 at 07:45):

that's kind of the whole reason algebra.big_operators exists, to act as the join of data.finset and algebra.*

view this post on Zulip Patrick Massot (Mar 02 2020 at 07:46):

See https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Contribution.20to.20mathlib.20with.20the.20Ostrowski.20theorem/near/187592253 for the last time someone tried to convince Mario to drop _root_.prime. Maybe we can ask once per month and I'll get tired at some point :wink:

view this post on Zulip Yury G. Kudryashov (Mar 02 2020 at 07:47):

Now I'm trying to convince Mario to drop nat.prime, and use _root_.prime as the only definition ;)

view this post on Zulip Mario Carneiro (Mar 02 2020 at 07:47):

Any thoughts on my suggestion to have two files, one about prime (and applied to nat) and one about factorization and unique factorization

view this post on Zulip Mario Carneiro (Mar 02 2020 at 07:48):

Or should there still be a separate file for @prime nat?

view this post on Zulip Yury G. Kudryashov (Mar 02 2020 at 07:50):

What information about nat.prime is important for norm_num?

view this post on Zulip Mario Carneiro (Mar 02 2020 at 07:50):

The computation of min_fac

view this post on Zulip Patrick Massot (Mar 02 2020 at 07:51):

cau_seq is mostly an implementation detail for the construction of the reals

Yury, if you really have too much time and energy, you can try to revert the change that introduced cau_seq. This was motivated mostly by mysterious performance issues. We used to have a construction of reals (by Johannes Hölzl) which was half-way between the Cauchy sequence construction and Bourbaki construction (using completion of general topological rings). But it caused many time-outs. This was probably because some definition should have been marked as irreducible but wasn't. But nobody could figure out a solution before Mario's desire to stick to low-tech maths kicked in. I'm very grateful to see real numbers that work, but I wouldn't mind getting rid of cau_seq.

view this post on Zulip Patrick Massot (Mar 02 2020 at 07:52):

Now I'm trying to convince Mario to drop nat.prime, and use _root_.prime as the only definition ;)

Sorry, I meant dropping nat.prime.

view this post on Zulip Mario Carneiro (Mar 02 2020 at 07:53):

Please don't remove cau_seq. For some reason Kevin loves to use data.real.basic in examples, and I have the luxury of a compiled mathlib at most 60% of the time

view this post on Zulip Mario Carneiro (Mar 02 2020 at 07:55):

If you can make the definition of cauchy and relevant properties similarly speedy I would be okay with it but we have done nothing to improve this situation since I wrote cau_seq AFAIK

view this post on Zulip Mario Carneiro (Mar 02 2020 at 07:56):

I want the real numbers to be something that can be considered part of the core library

view this post on Zulip Patrick Massot (Mar 02 2020 at 07:56):

Filters and uniform spaces can be considered part of the core library, right?

view this post on Zulip Mario Carneiro (Mar 02 2020 at 07:57):

Like I said, if that library got slimmer and faster it might be possible to do away with cau_seq. But it needs a big cleanup / refactor for that

view this post on Zulip Mario Carneiro (Mar 02 2020 at 08:00):

One way to solve the problem is to use dedekind cuts for the construction instead :D

view this post on Zulip Kevin Buzzard (Mar 02 2020 at 08:01):

Nooo!

view this post on Zulip Mario Carneiro (Mar 02 2020 at 08:02):

Also cau_seq is "computable". I was discouraged at the time from using explicit moduli but without it the actual computable content is pretty useless, but with it we could conceivably have an exact real arithmetic library built on real

view this post on Zulip Johan Commelin (Mar 02 2020 at 08:03):

Which sounds like a useful thing to have.

view this post on Zulip Johan Commelin (Mar 02 2020 at 08:04):

At some point we want to know that e > 2.71 for some reason or other. So we'll need tactics and a library that can "compute" with real numbers.

view this post on Zulip Mario Carneiro (Mar 02 2020 at 08:04):

We already did this kind of thing for pi day

view this post on Zulip Mario Carneiro (Mar 02 2020 at 08:05):

For the proof producing version we will need a norm_num style prover, but a computable function would be useful for computations with real numbers in #eval

view this post on Zulip Mario Carneiro (Mar 02 2020 at 08:06):

which, by the way, would probably be used in the prover itself

view this post on Zulip Yury G. Kudryashov (Mar 02 2020 at 08:07):

Do I remember correctly that there are no computable well-defined non-constant functions from real to nat?

view this post on Zulip Mario Carneiro (Mar 02 2020 at 08:08):

Yes, with the current implementation

view this post on Zulip Yury G. Kudryashov (Mar 02 2020 at 08:09):

Which implementation has computable functions and is a field?

view this post on Zulip Mario Carneiro (Mar 02 2020 at 08:09):

You can, however, inhabit trunc (psum (r < 1) (0 < r))

view this post on Zulip Mario Carneiro (Mar 02 2020 at 08:10):

It will not be a computable field, but it will have an inv function that requires a proof that the argument is nonzero

view this post on Zulip Patrick Massot (Mar 02 2020 at 08:10):

You guys are really not fun. I was talking about Bourbaki reals and you managed to drift to computable reals... I'm going back to normal maths in my geometry class.

view this post on Zulip Mario Carneiro (Mar 02 2020 at 08:10):

I think it would be nice to have both

view this post on Zulip Mario Carneiro (Mar 02 2020 at 08:11):

Once you go in mathematician mode, all the distinctions fade away and you've clearly constructed the actual real numbers

view this post on Zulip Mario Carneiro (Mar 02 2020 at 08:11):

it can be a field and everything else

view this post on Zulip Johan Commelin (Mar 02 2020 at 08:13):

@Patrick Massot Did Boubaki ever need an approximation of a transcendental real number?

view this post on Zulip Johan Commelin (Mar 02 2020 at 08:14):

I've never read any of their treatment of analyisis

view this post on Zulip Yury G. Kudryashov (Mar 02 2020 at 08:17):

I'm not sure that we can make sufficiently flexible computable (in the sense of eval) real numbers.

view this post on Zulip Yury G. Kudryashov (Mar 02 2020 at 08:19):

More or less, a computable real number is a (trunc of) a function λ n, {r : rat | abs (x - r) ≤ 1/n (or (1/2)^n).

view this post on Zulip Yury G. Kudryashov (Mar 02 2020 at 08:19):

If you want to define, e.g., a + b, then you need to decide how to distribute the error.

view this post on Zulip Yury G. Kudryashov (Mar 02 2020 at 08:21):

Splitting in halves is not a way to go because in a + b + c + d + e + f you'll need to know a with a very high accuracy.

view this post on Zulip Yury G. Kudryashov (Mar 02 2020 at 08:23):

So we either need a definition that automatically distributes error margins, or a definition that asks the user how to distribute them.

view this post on Zulip Mario Carneiro (Mar 02 2020 at 08:26):

(1) You can always have more fancy functions that allow you to distribute the error more precisely (2) Dividing the error in half isn't so bad. Usually you use 1/2^n for the modulus, and most of the basic operations generate bits in linear time, so asking for one more bit is not unreasonable

view this post on Zulip Yury G. Kudryashov (Mar 02 2020 at 08:26):

I think that a possible way to go is to have classical noncomputable reals and something like approximates (x : real) (f : nat → rat) : Prop := ∀ n, abs (x - f n) < (1 / 2)^n. Then we can have theorems like approximates x f → approximates y g → approximates (x + y) (λ n, f n + g n).

view this post on Zulip Mario Carneiro (Mar 02 2020 at 08:27):

but isn't that just a cau_seq and its representative real?

view this post on Zulip Yury G. Kudryashov (Mar 02 2020 at 08:27):

No, I prescribe the rate of convergence.

view this post on Zulip Mario Carneiro (Mar 02 2020 at 08:28):

I'm talking here about a hypothetical change to the definition of cau_seq to add a modulus so that you can use real for computation

view this post on Zulip Yury G. Kudryashov (Mar 02 2020 at 08:30):

Ah, so the new cau_seq will converge at a prescribed rate (e.g., (1/2)^n)?

view this post on Zulip Mario Carneiro (Mar 02 2020 at 08:30):

right

view this post on Zulip Yury G. Kudryashov (Mar 02 2020 at 08:31):

Then inv x will require psum (x < 0) (0 < x), not just x ≠ 0.

view this post on Zulip Mario Carneiro (Mar 02 2020 at 08:33):

actually it will need more than that, it will need |x| > 1/n

view this post on Zulip Yury G. Kudryashov (Mar 02 2020 at 08:33):

Yes.

view this post on Zulip Mario Carneiro (Mar 02 2020 at 08:33):

i.e. x is apart from 0

view this post on Zulip Mario Carneiro (Mar 02 2020 at 08:34):

My point being, it will have some funny intuitionistic constraints on it and the mathematicians won't need to touch it but it's there if you want to actually compute


Last updated: May 18 2021 at 08:14 UTC