removing decidability instances from polynomials

Stream: general

[Scott Morrison]

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]

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

[Scott Morrison]

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

[Johan Commelin]

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

[Mario Carneiro]

What I can see looks good

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Scott Morrison]

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

[Scott Morrison]

(deleted)

[Scott Morrison]

(deleted)

[Scott Morrison]

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]

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]

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

[Mario Carneiro]

I think convert will fix those issues