# Zulip Chat Archive

## Stream: new members

### Topic: Introduction and review request

#### Pim Otte (Aug 02 2022 at 13:16):

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:

- 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?
- 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?
- 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 (Aug 02 2022 at 14:04):

- 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). - Do you mean the statement is verbose, or the proof?
- I'm not sure yet, I think I would need to somehow normalize them into something more familiar (to me).

#### Pim Otte (Aug 02 2022 at 14:11):

@Jireh Loreaux The squeeze_simp worked wonderfully, thanks!

- The proof, mostly.
- 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 (alpha
*X+beta*Y)^2 to this form, and coefficient_equal simply says that the polynomials are equal if their coefficients are equal.

#### Yakov Pechersky (Aug 02 2022 at 14:16):

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

#### Jireh Loreaux (Aug 02 2022 at 14:17):

`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 (Aug 02 2022 at 14:18):

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 (Aug 02 2022 at 14:23):

docs#mv_polynomial.is_homogeneous

#### Jireh Loreaux (Aug 02 2022 at 14:29):

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 (Aug 02 2022 at 14:37):

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 (Aug 02 2022 at 14:41):

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

Last updated: Dec 20 2023 at 11:08 UTC