Polynomial.degree_toFinsupp

Stream: Is there code for X?

[Siddharth Bhat]

Does the following exist?

theorem Polynomial.degree_toFinsupp [Semiring M] [DecidableEq M]
  (xs : List M) :
  degree { toFinsupp := List.toFinsupp (l := xs) } ≤ List.length xs

[Yakov Pechersky]

I had something like it in here https://github.com/leanprover-community/mathlib/pull/15477/files

[Yakov Pechersky]

https://github.com/leanprover-community/mathlib/pull/15476/files#diff-fae6d434339c03bb00dae13fc68db6fad33f196335665c91f06aad5d4f52eaf6R150

[Siddharth Bhat]

Aha, now I need to understand how we work on stuff together in mathlib. If I need the result for a different result, do I copy-paste, wait for your PR to be merged, and then rework my code to use your PR?

[Ruben Van de Velde]

Well, Yakov's result is in a mathlib 3 PR that will never be merged, so you could translate it to lean 4 and add it yourself

[Yakov Pechersky]

15476 should be easy to rewrite in lean4, it is only a single file, and getD instead of nthd

[Ruben Van de Velde]

Alternatively, this is a lean 4 proof:

import Mathlib

theorem Polynomial.degree_toFinsupp [Semiring M] [DecidableEq M]
  (xs : List M) :
  degree { toFinsupp := List.toFinsupp (l := xs) } ≤ List.length xs := by
  simp [degree]
  refine Finset.max_le fun x hx => ?st
  contrapose! hx
  simp
  have : List.length xs < x := by
    rw [Nat.cast_withBot] at hx
    norm_cast at hx
  exact List.getD_eq_default xs 0 this.le

[Ruben Van de Velde]

But Yakov has probably thought more about the best way to state those results

[Siddharth Bhat]

Is there a place one can ask for code review to get better at mathlibing? Here's the proof I came up with, which is clearly way more verbose:

import Mathlib.RingTheory.Polynomial.Basic
import Mathlib.Data.List.ToFinsupp

theorem Polynomial.degree_toFinsupp [Semiring M] [DecidableEq M]
  (xs : List M) :
  degree { toFinsupp := List.toFinsupp (l := xs) } ≤ List.length xs := by
    cases xs
    case nil =>
      simp[degree]
    case cons x xs =>
      simp[degree]
      simp[List.toFinsupp]
      simp[Finset.range_succ]
      apply Finset.max_le
      intros a ha
      obtain ⟨ha₁, ha₂⟩ := Finset.mem_filter.mp ha
      have ha₃ := Finset.mem_insert.mp ha₁
      cases' ha₃ with ha₄ ha₅
      . subst ha₄
        norm_cast
        apply WithBot.coe_le_coe.mpr
        simp[Nat.cast]
      . have ha₆ := Finset.mem_range.mp ha₅
        norm_cast
        apply WithBot.coe_le_coe.mpr
        norm_cast
        simp at ha₆ ⊢
        simp[Nat.le_add_one_iff, ha₆]
        left
        apply Nat.le_of_lt ha₆

[Ruben Van de Velde]

Generally, by making a PR to mathlib

[Siddharth Bhat]

In this particular proof, I struggled to deal with WithBot, and to repeatedly destruct the proof witness a ∈ Finset.filter (fun i => ¬List.getD (x :: xs) i 0 = 0) (insert (List.length xs) (Finset.range (List.length xs)))

[Siddharth Bhat]

Ruben Van de Velde said:

Generally, by making a PR to mathlib

Would it be impolite to ask for review here to get better at mathlib, without making a PR, since I presume your version would be far more preferable? :smile:

[Ruben Van de Velde]

I think (looking at my proof), you went off in an inefficient direction at cases xs - if you hadn't started that way, you probably wouldn't have ended up much more verbose than I did

[Ruben Van de Velde]

So sometimes it's just luck in getting the "right" start

[Yakov Pechersky]

I shared the PR because I think having an API layer between lists and polynomial that doesn't rely on a direct piercing through the API layers would be better

[Yakov Pechersky]

It's not about the length / style of this one proof, but the collection of proofs / gadgets you might want about such constructions.

[Yakov Pechersky]

and in building that collection, one finds proof patterns

[Yakov Pechersky]

If you're having to unfold API via tactics like simp [degree], simp [List.toFinsupp], sure, you'll be able to get a proof that compiles. But it won't create for a nice API microecosystem