zmodp

Stream: maths

[Reid Barton]

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

[Mario Carneiro]

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

[Reid Barton]

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

[Mario Carneiro]

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

[Johan Commelin]

See also #1648

[Mario Carneiro]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Mario Carneiro]

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

[Yury G. Kudryashov]

Of which idea?

[Mario Carneiro]

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

[Mario Carneiro]

the idea to merge the two definitions

[Mario Carneiro]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Mario Carneiro]

Why does nat.prime need list.perm?

[Yury G. Kudryashov]

For factors_unique

[Mario Carneiro]

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

[Yury G. Kudryashov]

Why nat/prime should care about dependencies?

[Mario Carneiro]

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

[Mario Carneiro]

also it's needed by norm_num

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Mario Carneiro]

Having a fancy definition for a simple concept is also confusing

[Yury G. Kudryashov]

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

[Mario Carneiro]

see filters

[Mario Carneiro]

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

[Yury G. Kudryashov]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Yury G. Kudryashov]

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.

[Mario Carneiro]

open nat causes a lot of confusion

[Johan Commelin]

Is _root_.prime really that complicated?

[Yury G. Kudryashov]

/-- 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)

[Johan Commelin]

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

[Mario Carneiro]

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

[Johan Commelin]

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

[Yury G. Kudryashov]

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

[Johan Commelin]

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

[Mario Carneiro]

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

[Yury G. Kudryashov]

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

[Mario Carneiro]

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

[Mario Carneiro]

group_power is hard to avoid when talking about prime numbers

[Mario Carneiro]

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

[Mario Carneiro]

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

[Patrick Massot]

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:

[Yury G. Kudryashov]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Yury G. Kudryashov]

What information about nat.prime is important for norm_num?

[Mario Carneiro]

The computation of min_fac

[Patrick Massot]

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.

[Patrick Massot]

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.

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Patrick Massot]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

Nooo!

[Mario Carneiro]

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

[Johan Commelin]

Which sounds like a useful thing to have.

[Johan Commelin]

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.

[Mario Carneiro]

We already did this kind of thing for pi day

[Mario Carneiro]

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

[Mario Carneiro]

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

[Yury G. Kudryashov]

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

[Mario Carneiro]

Yes, with the current implementation

[Yury G. Kudryashov]

Which implementation has computable functions and is a field?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Patrick Massot]

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.

[Mario Carneiro]

I think it would be nice to have both

[Mario Carneiro]

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

[Mario Carneiro]

it can be a field and everything else

[Johan Commelin]

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

[Johan Commelin]

I've never read any of their treatment of analyisis

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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.

[Yury G. Kudryashov]

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

[Mario Carneiro]

(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

[Yury G. Kudryashov]

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

[Mario Carneiro]

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

[Yury G. Kudryashov]

No, I prescribe the rate of convergence.

[Mario Carneiro]

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

[Yury G. Kudryashov]

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

[Mario Carneiro]

right

[Yury G. Kudryashov]

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

[Mario Carneiro]

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

[Yury G. Kudryashov]

Yes.

[Mario Carneiro]

i.e. x is apart from 0

[Mario Carneiro]

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