Zulip Chat Archive

Stream: general

Topic: removing decidability instances from polynomials


view this post on Zulip 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

view this post on Zulip Scott Morrison (Jul 22 2019 at 01:34):

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

view this post on Zulip Scott Morrison (Jul 22 2019 at 01:34):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Jul 22 2019 at 01:43):

What I can see looks good

view this post on Zulip Johan Commelin (Jul 22 2019 at 01:44):

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

view this post on Zulip Johan Commelin (Jul 22 2019 at 01:44):

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

view this post on Zulip Johan Commelin (Jul 22 2019 at 01:45):

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

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Jul 22 2019 at 01:59):

(deleted)

view this post on Zulip Scott Morrison (Jul 22 2019 at 02:00):

(deleted)

view this post on Zulip 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

view this post on Zulip 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))

view this post on Zulip Scott Morrison (Jul 22 2019 at 02:06):

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

view this post on Zulip Mario Carneiro (Jul 22 2019 at 02:13):

I think convert will fix those issues


Last updated: May 14 2021 at 23:14 UTC