# Zulip Chat Archive

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

#### Johan Commelin (Mar 02 2020 at 05:44):

See also #1648

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

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

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 `import`

ing `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`

.

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

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

#### Kevin Buzzard (Mar 02 2020 at 08:01):

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 `real`

s 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`

)?

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

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`

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

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