## Stream: general

### Topic: removing decidability instances from polynomials

#### Scott Morrison (Jul 22 2019 at 01:34):

Hi @Johan Commelin, I noticed you've been doing some work recently on power series, so thought I'd ask you about this --- shall we make polynomials completely classical, and remove all the decidability instances?

I made a start on doing this, but it was quickly bit-rotting with all your changes. I think I've managed to merge back to master, at https://github.com/leanprover-community/mathlib/compare/decidable_eq

#### Scott Morrison (Jul 22 2019 at 01:34):

It's not quite done yet --- there are still problems in mv_polynomial.

#### Scott Morrison (Jul 22 2019 at 01:34):

Any chance you could take a look at it, and see if it's worth proceeding?

#### Johan Commelin (Jul 22 2019 at 01:43):

I think Mario said this was a good idea. I don't have a strong opinion. Will take a look now.

#### Mario Carneiro (Jul 22 2019 at 01:43):

What I can see looks good

#### Johan Commelin (Jul 22 2019 at 01:44):

Yep, it certainly didn't become less readable :stuck_out_tongue_wink:

#### Johan Commelin (Jul 22 2019 at 01:44):

If it also speeds up things, I would rather have this merged sooner than later.

#### Johan Commelin (Jul 22 2019 at 01:45):

Now I need to go back to bed. See you guys later today.

#### Scott Morrison (Jul 22 2019 at 01:45):

I think there is still one broken file. I'm building now to try to find it.

(deleted)

(deleted)

#### Scott Morrison (Jul 22 2019 at 02:05):

I'm getting strange errors like

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
finset.has_union
inferred
finset.has_union


#### Scott Morrison (Jul 22 2019 at 02:05):

which expands with pp.all to

synthesized type class instance is not definitionally equal to expression inferred by typing rules, synthesized
@finset.has_union.{0} nat (λ (a b : nat), nat.decidable_eq a b)
inferred
@finset.has_union.{0} nat (λ (a b : nat), classical.prop_decidable (@eq.{1} nat a b))


#### Scott Morrison (Jul 22 2019 at 02:06):

But I don't know how to diagnose where nat.decidable_eq instances are creeping in.

#### Mario Carneiro (Jul 22 2019 at 02:13):

I think convert will fix those issues

Last updated: May 14 2021 at 23:14 UTC