Complete Algebra.exists_dvd_nonzero_if_isIntegral #157
Conversation
There was a problem hiding this comment.
Sorry it's taken me a while to get to this. FLT is supposed to be my full-time job right now but in practice there are some teething troubles whilst I get other aspects of my life under control (e.g. getting to inbox 0, which I've not had now for several months but am nearly achieving). My instinct is that this proof is too long. I think your idea of breaking it into two pieces is great. My instinct is that both pieces are too long right now but I'm happy to work with you to make it shorter.
| obtain ⟨p, p_monic, p_eval⟩ := (@Algebra.isIntegral_def R S).mp inferInstance s | ||
| have p_neq_zero := ne_zero_of_ne_zero_of_monic X_ne_zero p_monic | ||
| let d := p.natTrailingDegree | ||
| use ∑ n ∈ p.support, monomial (n - d) (p.coeff n) |
There was a problem hiding this comment.
I knew this proof was going to be fiddly but I hadn't appreciated that it would be this long. Do you think that using Polynomial.divByMonic would be easier than this approach?
| . apply monic_of_degree_le_of_coeff_eq_one (p.natDegree - d) this | ||
| rw [finset_sum_coeff] | ||
| rw [Finset.sum_eq_single_of_mem p.natDegree] | ||
| . simp |
There was a problem hiding this comment.
Can you fix this non-terminal simp (if you don't refactor the proof?), maybe using simpa using Monic.leadingCoeff p_monic?
| rw [natTrailingDegree_eq_support_min' p_neq_zero] | ||
| exact Finset.min'_le p.support b b_support | ||
| have this2 : d ≤ p.natDegree := by | ||
| exact Polynomial.natTrailingDegree_le_natDegree p |
There was a problem hiding this comment.
Probably you don't need this2, you can just use Polynomial.natTrailingDegree_le_natDegree p.
| . rw [finset_sum_coeff] | ||
| rw [Finset.sum_eq_single_of_mem d] |
There was a problem hiding this comment.
Just do them both in one rewrite?
| . rw [finset_sum_coeff] | ||
| rw [Finset.sum_eq_single_of_mem d] | ||
| . rw [coeff_monomial] | ||
| simp [d, p_neq_zero] |
There was a problem hiding this comment.
Again, nonterminal simps are brittle so I'd like to avoid them in the project.
There was a problem hiding this comment.
Can you explain why nonterminal simps are bad? Is there a better way to let Lean help simplify things?
| rw [Nat.sub_eq_iff_eq_add this] at h | ||
| simp [h, this] | ||
| . rw [eval₂_finset_sum] | ||
| simp |
There was a problem hiding this comment.
Ditto here and in other places.
|
I can certainly help you in golfing this proof if you want. I'll have more time tonight. |
|
I have also removed the |
Co-authored-by: Pietro Monticone <[email protected]>
Co-authored-by: Pietro Monticone <[email protected]>
|
I added the two suggestions. I'll check out |
|
I was able to get it down to ~30 lines total using |
|
This looks much better now! Many thanks! |
No description provided.