## Stream: maths

### Topic: zmodp

#### Reid Barton (Mar 02 2020 at 04:19):

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

#### Mario Carneiro (Mar 02 2020 at 04:36):

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

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

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

#### 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 := ...

#### 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?

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

#### Mario Carneiro (Mar 02 2020 at 07:25):

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

Of which idea?

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

#### Mario Carneiro (Mar 02 2020 at 07:25):

the idea to merge the two definitions

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

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

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

#### Mario Carneiro (Mar 02 2020 at 07:30):

Why does nat.prime need list.perm?

#### Yury G. Kudryashov (Mar 02 2020 at 07:30):

For factors_unique

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

#### Yury G. Kudryashov (Mar 02 2020 at 07:31):

Why nat/prime should care about dependencies?

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

#### Mario Carneiro (Mar 02 2020 at 07:31):

also it's needed by norm_num

#### Yury G. Kudryashov (Mar 02 2020 at 07:33):

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

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

#### Mario Carneiro (Mar 02 2020 at 07:34):

Having a fancy definition for a simple concept is also confusing

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

see filters

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

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

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

#### Mario Carneiro (Mar 02 2020 at 07:38):

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

#### Mario Carneiro (Mar 02 2020 at 07:38):

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

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

#### Mario Carneiro (Mar 02 2020 at 07:39):

open nat causes a lot of confusion

#### Johan Commelin (Mar 02 2020 at 07:40):

Is _root_.prime really that complicated?

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


#### Johan Commelin (Mar 02 2020 at 07:40):

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

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

#### Johan Commelin (Mar 02 2020 at 07:41):

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

#### Yury G. Kudryashov (Mar 02 2020 at 07:41):

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


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

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

#### Yury G. Kudryashov (Mar 02 2020 at 07:42):

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

#### Mario Carneiro (Mar 02 2020 at 07:43):

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

#### Mario Carneiro (Mar 02 2020 at 07:43):

group_power is hard to avoid when talking about prime numbers

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

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

#### 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:

#### 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 ;)

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

#### Mario Carneiro (Mar 02 2020 at 07:48):

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

#### Yury G. Kudryashov (Mar 02 2020 at 07:50):

What information about nat.prime is important for norm_num?

#### Mario Carneiro (Mar 02 2020 at 07:50):

The computation of min_fac

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

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

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

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

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

#### Patrick Massot (Mar 02 2020 at 07:56):

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

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

#### Mario Carneiro (Mar 02 2020 at 08:00):

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

Nooo!

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

#### Johan Commelin (Mar 02 2020 at 08:03):

Which sounds like a useful thing to have.

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

#### Mario Carneiro (Mar 02 2020 at 08:04):

We already did this kind of thing for pi day

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

#### Mario Carneiro (Mar 02 2020 at 08:06):

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

#### 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?

#### Mario Carneiro (Mar 02 2020 at 08:08):

Yes, with the current implementation

#### Yury G. Kudryashov (Mar 02 2020 at 08:09):

Which implementation has computable functions and is a field?

#### Mario Carneiro (Mar 02 2020 at 08:09):

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

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

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

#### Mario Carneiro (Mar 02 2020 at 08:10):

I think it would be nice to have both

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

#### Mario Carneiro (Mar 02 2020 at 08:11):

it can be a field and everything else

#### Johan Commelin (Mar 02 2020 at 08:13):

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

#### Johan Commelin (Mar 02 2020 at 08:14):

I've never read any of their treatment of analyisis

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

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

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

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

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

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

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

#### Mario Carneiro (Mar 02 2020 at 08:27):

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

#### Yury G. Kudryashov (Mar 02 2020 at 08:27):

No, I prescribe the rate of convergence.

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

#### 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)?

right

#### Yury G. Kudryashov (Mar 02 2020 at 08:31):

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

#### Mario Carneiro (Mar 02 2020 at 08:33):

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

Yes.

#### Mario Carneiro (Mar 02 2020 at 08:33):

i.e. x is apart from 0

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