chore(data/mv_polynomial): adding decidable_eq assumptions#18791
chore(data/mv_polynomial): adding decidable_eq assumptions#18791
Conversation
joelriou
commented
Apr 11, 2023
eric-wieser
left a comment
There was a problem hiding this comment.
I think this PR has grown out of control(already!).
Can you split off a PR that edits only the mv_polynomial directory, and doesn't attempt to remove any other classicals?
| def frange [decidable_eq R] (p : R[X]) : finset R := | ||
| finset.image (λ n, p.coeff n) p.support |
There was a problem hiding this comment.
I think it's probably best to make this noncomputable for now.
| noncomputable def roots [decidable_eq R] (p : R[X]) : multiset R := | ||
| if h : p = 0 then ∅ else classical.some (exists_multiset_roots h) |
There was a problem hiding this comment.
This change is unhelpful; the definition is already very non-computable, so there's no point adding this argument,
| noncomputable def roots [decidable_eq R] (p : R[X]) : multiset R := | |
| if h : p = 0 then ∅ else classical.some (exists_multiset_roots h) | |
| noncomputable def roots (p : R[X]) : multiset R := | |
| by haveI := classical.dec_eq R; exact | |
| if h : p = 0 then ∅ else classical.some (exists_multiset_roots h) |
There was a problem hiding this comment.
I've pushed a fix to that effect
There was a problem hiding this comment.
Thanks. I think that all the definitions on polynomials which require a decidable_eq instance should be obtained from classical.dec_eq as above, including for example mv_polynomial.vars in data/mv_polynomial/variables.lean. Otherwise, it escalates quickly... If you agree, I may restart this PR from scratch. (And eventually, the same could be done on the mathlib4 side.)
There was a problem hiding this comment.
I'm not sure I agree that they should be, but at any rate they are already define that way. So the minimal fix is to add classical.dec_eq to all the relevant existing defs, and only add decidable_eq when need by theorem statements.
|
Please don't merge this without careful discussion on zulip! Several years ago we went to great effort to remove decidability instances from the polynomial library, and intentionally made everything noncomputable and classical. I don't think these sort of changes are going to be viable. |
|
@semorrison, the idea here is to add the missing instances to lemmas, which I think is widely agreed as sensible. You're right though that in it's current form it also adds them to defs which we don't want to do (at least not mid-port) |
I've done this in #18848 |