Introduction and review request

Stream: new members

[Pim Otte]

Hi all! I'm Pim. I'm a software developer, but dipping my toe back in to math just for fun and learning lean along with that. (Graduated with an MSc in applied math).

I've proven some smaller results I want to use elsewhere, but I'm guessing there's a lot to be improved. A couple of questions about the sample below:

1. the simp call in simple_identity takes about 2.5~3 seconds for me, is that normal? Can I do something to speed that up/should I be using something else?
2. The coeficient_equal lemma seems very verbose. (I've tried refactoring it a little bit for the a=d part, but not with much result) Is there an easier way to prove the finsupp.single s to be not equal?
3. Could I get either result directly from mathlib?

Thanks in advance:)

import data.mv_polynomial.basic
import data.complex.basic

-- set_option profiler true

noncomputable def simple_polynomial (a b c : ℂ) : (mv_polynomial ℕ ℂ)  := (mv_polynomial.monomial (finsupp.single 0 2) a) + (mv_polynomial.monomial (finsupp.single 0 1 + finsupp.single 1 1) b) + (mv_polynomial.monomial (finsupp.single 1 2) c)

lemma simple_identity (α β : ℂ) : (mv_polynomial.monomial (finsupp.single 0 1) α + mv_polynomial.monomial (finsupp.single 1 1) β)^2 = simple_polynomial (α^2) (2*α*β) (β^2) :=
begin
    unfold simple_polynomial,
    ring_nf SOP {recursive := ff},
    simp [mv_polynomial.monomial_eq_C_mul_X, mv_polynomial.monomial_single_add, mv_polynomial.C_pow],
    ring,
end

lemma coefficient_equal (a b c d e f : ℂ) : simple_polynomial a b c = simple_polynomial d e f ↔ a = d ∧ b = e ∧ c = f :=
begin
    split,
    {
        unfold simple_polynomial,
        intros h,
        rw mv_polynomial.ext_iff at h,
        have help₁ : ¬ (finsupp.single 1 2 = finsupp.single 0 2),
        {
            intro h,
            rw fun_like.ext_iff at h,
            specialize h 0,
            simp at h,
            exact h,
        },
        have help₂ : ¬ (finsupp.single 0 1 + finsupp.single 1 1 = finsupp.single 0 2),
        {
            intro h,
            rw fun_like.ext_iff at h,
            specialize h 0,
            simp at h,
            exact h,
        },
        have fact₁ : a = d,
        {
            specialize h (finsupp.single 0 2),
            simp [mv_polynomial.coeff_X_pow, mv_polynomial.coeff_mul_X', mv_polynomial.coeff_C_mul] at h,

            split_ifs at h,
            {
                simp at h,
                exact h,
            },
        },
        have fact₂ : b = e,
        {
            specialize h (finsupp.single 0 1 + finsupp.single 1 1),
            simp [mv_polynomial.coeff_X_pow, mv_polynomial.coeff_mul_X', mv_polynomial.coeff_C_mul] at h,

            split_ifs at h,
            {
                exfalso,
                rw fun_like.ext_iff at h_1,
                specialize h_1 0,
                simp at h_1,
                exact h_1,
            },
            {
                exfalso,
                rw fun_like.ext_iff at h_1,
                specialize h_1 0,
                simp at h_1,
                exact h_1,
            },
            {
                exfalso,
                rw fun_like.ext_iff at h_2,
                specialize h_2 0,
                simp at h_2,
                exact h_2,
            },
            {
                simp at h,
                exact h,
            },
        },
        have fact₃ : c = f,
        {
            specialize h (finsupp.single 1 2),
            simp [mv_polynomial.coeff_X_pow, mv_polynomial.coeff_mul_X', mv_polynomial.coeff_C_mul] at h,

            split_ifs at h,
            {
                exfalso,
                rw fun_like.ext_iff at h_1,
                specialize h_1 0,
                simp at h_1,
                exact h_1,
            },
            {
                exfalso,
                rw fun_like.ext_iff at h_1,
                specialize h_1 0,
                simp at h_1,
                exact h_1,
            },
            {
                exfalso,
                rw fun_like.ext_iff at h_2,
                specialize h_2 0,
                simp at h_2,
                exact h_2,
            },
            {
                simp at h,
                exact h,
            },
        },
        exact ⟨fact₁, fact₂, fact₃⟩
    },
    {
        intro h,
        cases h with ha h',
        cases h' with hb hc,
        rw ha,
        rw hb,
        rw hc,
    },

end

[Jireh Loreaux]

1. You can speed up simps by squeezing them (i.e., replacing it with squeeze_simp). When this runs, it will give you, in VS code's widget panel: "Try this: simp only [...]", which you can then click and it will replace the squeeze_simp with the simp only [...]. This makes it so that it is only doing simp with the collection of lemmas in brackets, as opposed to all the simp lemmas currently imported. (In addition, I think simp should be significantly faster in Lean 4, once we manage to make that switch).
2. Do you mean the statement is verbose, or the proof?
3. I'm not sure yet, I think I would need to somehow normalize them into something more familiar (to me).

[Pim Otte]

@Jireh Loreaux The squeeze_simp worked wonderfully, thanks!

2. The proof, mostly.
3. So to be a little bit more specific, I'm trying to prove a statement about multivariate polynomials of the form aX^2+bXY+cY^2, simple_identity is the expansion of (alphaX+betaY)^2 to this form, and coefficient_equal simply says that the polynomials are equal if their coefficients are equal.

[Yakov Pechersky]

example : ¬ (finsupp.single 1 2 = finsupp.single 0 2) :=
(finsupp.single_left_injective (two_ne_zero)).ne one_ne_zero

[Jireh Loreaux]

coefficient_equal should be an @[ext] lemma, so maybe docs#mv_polynomial.ext or maybe docs#mv_polynomial.ext_iff. As for simplifying the proof, the answer is certainly yes, but it should be unnecessary given the above lemma.

[Jireh Loreaux]

I'm not sure if we have stuff about homogeneous polynomials in mathlib, but I would be a bit surprised if not. Someone familiar with this part of the library will be able to answer better.

[Jireh Loreaux]

docs#mv_polynomial.is_homogeneous

[Jireh Loreaux]

That is the unbundled predicate which just says that a poynomial is homogeneous, but we also have it bundled as a submodule with docs#mv_polynomial.homogeneous_submodule. So I think you could get a "simple polynomial" as p : mv_polynomial.homogeneous_submodule (fin 2) ℂ 2.

[Pim Otte]

Yakov Pechersky said:

example : ¬ (finsupp.single 1 2 = finsupp.single 0 2) :=
(finsupp.single_left_injective (two_ne_zero)).ne one_ne_zero

Though this broke my brain a little bit, I think I understand now. This is very helpful to learn how I should be thinking about this stuff:)

@Jireh Loreaux Great references! I think I came across the ext lemma's at some point but failed to get them to work at that time, I'll give that another shot now that I have more of a clue. Perhaps with your references on the homogeneous stuff, I might not even need it. Thanks a lot :)

[Jireh Loreaux]

Even with the homogeneous submodule, you will still need the ext lemmas in order to move between equality of polynomials and equality of coefficients.