bye `decidable_linear_order`

Stream: general

[Yury G. Kudryashov]

In lean#484 I merge linear_order with decidable_linear_order. In #4762 I'm trying to fix mathlib build. I could definitely use some help in this task. The PR already touches 100 files.

[Heather Macbeth]

Sure, what can I do? Do you want to give me some files to fix?

[Johan Commelin]

I can also help. I guess it's good to make sure that we don't step on each others toes...

[Yury G. Kudryashov]

Pushed

[Yury G. Kudryashov]

I'm fixing filter_product. You're free to fix any other file.

[Yury G. Kudryashov]

Main API changes:

• remove decidable_linear_order;
• remove all decidable_linear_* groups etc, including discrete_*field

[Yury G. Kudryashov]

I did some search&replace, so should be no more decidable_linear* in the repository

[Yury G. Kudryashov]

Once you choose a file, tell the others here, please.

[Yury G. Kudryashov]

I'm done with filter_product, moving to data/real/basic

[Johan Commelin]

Note: 24daef0aff0716188b82300b2d629ca04696057e has cached oleans available

[Yury G. Kudryashov]

I'm not sure what should we do with real.ordered_ring etc. Currently proofs rely on linear_order which is going to become noncomputable. @Mario Carneiro Do you want to rewrite some proofs, or should I just make more instances noncomputable?

[Yury G. Kudryashov]

Note that some failures are because of https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/conv.20in.20lean.20master

[Johan Commelin]

It's about the reals, right? Aren't those already noncomputable in every sense?

[Yury G. Kudryashov]

And possibly we should skip them and hope that @Gabriel Ebner and @Eric Wieser will fix it in lean.

[Yury G. Kudryashov]

(+) and (*) are formally "computable"

[Yury G. Kudryashov]

But I see no practical value in this "computable".

[Yury G. Kudryashov]

They're computable in the following sense: given sequences approximating a and b, you can write down a sequence approximating a + b.

[Johan Commelin]

So maybe real.comm_ring can be computable, and then real.ordered_ring is not?

[Mario Carneiro]

@Yury G. Kudryashov real.linear_ordered_comm_ring was chosen to be the strongest class which can be derived on real that is computable

[Yury G. Kudryashov]

But linear_order now includes decidable_*

[Mario Carneiro]

I would suggest proving all the maximal elements of the poset of instances that are computable

[Yury G. Kudryashov]

So it can't be computable anymore

[Mario Carneiro]

right, you've pushed the frontier down a bit

[Yury G. Kudryashov]

Can you adjust the proofs?

[Mario Carneiro]

so we need a partial_order real instance now, and possibly some partial_order based ring proof

[Mario Carneiro]

It's just a subset of fields

[Yury G. Kudryashov]

I would prefer to avoid dealing with cau_seq and the definition of real if possible.

[Mario Carneiro]

Basically, the idea is to have all the same instances as we do currently, but ensure that nothing is noncomputable unless it has to be

[Mario Carneiro]

so the question comes down to which instances are noncomputable

[Yury G. Kudryashov]

E.g., the proof of add_le_add_left relies on linear_order.

[Yury G. Kudryashov]

So it has to be adjusted.

[Mario Carneiro]

what instance is that part of?

[Johan Commelin]

I will attempt topology/algebra/ordered.lean

[Yury G. Kudryashov]

E.g., ordered_add_comm_group or ordered_ring

[Yury G. Kudryashov]

I know how to fix it.

[Mario Carneiro]

Actually you can probably prove it using linear_order real

[Mario Carneiro]

because it's in a proof

[Yury G. Kudryashov]

@Mario Carneiro Could you please have a look at https://github.com/leanprover-community/mathlib/pull/4762/files#diff-6abf6bbce2c44f1e6e6680b121362215a4139aaeebe1c010f364b253eebbc5e9 ?

[Yury G. Kudryashov]

I'm going to fix data/complex/exponential

[Mario Carneiro]

I have some other stuff to attend to right now but I will be back in a few hours

[Yury G. Kudryashov]

Actually, data/complex/exponential is about conv+find

[Johan Commelin]

data/padics/padic_numbers.lean

[Yury G. Kudryashov]

real/hyperreal

[Johan Commelin]

padics/ring_homs

[Johan Commelin]

I think we're almost done!

[Heather Macbeth]

Indeed, I was just trying to find something to work on (I am slower than you!) and couldn't.

[Yury G. Kudryashov]

My computer already compiles manifold.times_cont_mdiff, and so far conv+find is the only remaining error.

[Yury G. Kudryashov]

@Heather Macbeth Then you can start reviewing the PR!

[Johan Commelin]

I've fixed complex/exponential

[Johan Commelin]

Didn't want to wait on the conv fix

[Heather Macbeth]

@Yury G. Kudryashov OK, but I am not qualified to review this computability-of-real.linear_ordered_comm_ring issue which you were discussing with Mario.

[Yury G. Kudryashov]

I hope, Mario will review this part.

[Johan Commelin]

I have a version that compiles without errors

[Yury G. Kudryashov]

Now we need someone to make a new release of Lean before this PR rots.

[Johan Commelin]

@Yury G. Kudryashov This is how you make a new release: https://github.com/leanprover-community/lean/commit/cc729642c39f9a5d66e45c1c92066bd8bec7d282

[Bryan Gin-ge Chen]

Do you mind writing a few sentences on the motivation for this for the commit message of lean#484? I'd be happy to merge it and make a new release of Lean after Mario gives his OK.

[Yury G. Kudryashov]

I think that the new release should wait for https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/conv.20in.20lean.20master

[Yury G. Kudryashov]

After lean#482 some of conv in ... in mathlib started to fail.

[Mario Carneiro]

what am I supposed to be reviewing again?

[Johan Commelin]

Yury G. Kudryashov said:

Mario Carneiro Could you please have a look at https://github.com/leanprover-community/mathlib/pull/4762/files#diff-6abf6bbce2c44f1e6e6680b121362215a4139aaeebe1c010f364b253eebbc5e9 ?

:up:

[Mario Carneiro]

I looked at it

[Mario Carneiro]

it looks like it's working

[Bryan Gin-ge Chen]

I approved lean#484. In the end I just added a link to this thread in the PR comment.

I don't feel qualified to figure out how to fix the issues related to lean#482.

[Eric Wieser]

Regarding lean#482, I think basically the contents of this discussion turned out to be a mistake:

https://github.com/leanprover-community/lean/pull/476#discussion_r503264366

[Bryan Gin-ge Chen]

Can you make a PR that resolves things? (Sorry, I haven't been following the discussion there or in the other thread in detail.)

[Eric Wieser]

Done in lean#485. Can someone else commit a test to that branch that demonstrates the behavior that broke?

[Yury G. Kudryashov]

I don't understand what exactly went wrong, so I guess I can't help creating a test that doesn't depend on mathlib.

[Eric Wieser]

I think even basic writing under binders broke

[Yury G. Kudryashov]

@Bryan Gin-ge Chen @Gabriel Ebner Are we ready for a new release?

[Bryan Gin-ge Chen]

I can make one this evening if Gabriel doesn't get to it before then.

[Yury G. Kudryashov]

In the meantime I made a tag in my repo and switched mathlib branch to this tag.

[Yury G. Kudryashov]

@maintainers #4762 is ready for review. It touches 103 files, so I'd love to see it merged soon (but no sooner than we actually have the corresponding lean release).