squeeze_simp differs from simp

Stream: new members

[Riccardo Brasca]

Hi, I have a proof of the following small lemma

import algebra.big_operators.basic
import field_theory.splitting_field

variables {α : Type*} [field α]

namespace polynomial

lemma test (p : polynomial α) :
(multiset.map (λ (a : α), X - C a) p.roots).prod.nat_degree = p.roots.card :=
begin
  rw [nat_degree_multiset_prod],
  simp,
  intros x h,
  simp [multiset.mem_map] at h,
  cases h with a ha,
  replace ha := ha.2,
  rw ← ha,
  exact X_sub_C_ne_zero a
end

end polynomial

That works (it can surely proved in a better way, but at least it works). Then I decided to replace the first simp with simp only, so I run squeeze_simp instead of the first simp. It proposes the following: simp only [mul_one, nat_degree_X_sub_C, nat.cast_id, multiset.sum_repeat, multiset.map_const, nsmul_eq_mul, eq_self_iff_true, function.comp_app, multiset.map_map] but if I use it the proof doesn't work (it even adds one goal, some multiset stuff I used simp to avoid).

My question is what I am supposed to do in this situation. I can for sure prove what I want but I am more interested in the general strategy when squeeze_simp behaves like this. Thank you!

[Damiano Testa]

I just want to say that I have had a similar experience at times with simp and squeeze_simp giving incompatible outputs. I am very curious to read about the answers!

[Johan Commelin]

squeeze_simp is unfortunately a bit hacky. We need a lean/tactic/c++ expert to give us something better (-;

[Johan Commelin]

One option is to write

set_option trace.simplify.rewrite true

on an empty line above the lemma, and look at the output. It will mention all lemmas that simp is using. But the output can be intimidating.

[Riccardo Brasca]

OK, i tried trace.simplify.rewrite true. The simp gives

0. [simplify.rewrite] [multiset.map_map]: multiset.map nat_degree (multiset.map (λ (a : α), X - ⇑C a) p.roots) ==> multiset.map (nat_degree ∘ λ (a : α), X - ⇑C a) p.roots
0. [simplify.rewrite] [function.comp_app]: (nat_degree ∘ λ (a : α), X - ⇑C a) x ==> (X - ⇑C x).nat_degree
0. [simplify.rewrite] [polynomial.nat_degree_X_sub_C]: (X - ⇑C x).nat_degree ==> 1
0. [simplify.rewrite] [multiset.map_const]: multiset.map (λ (x : α), 1) p.roots ==> multiset.repeat 1 p.roots.card
0. [simplify.rewrite] [multiset.sum_repeat]: (multiset.repeat 1 p.roots.card).sum ==> p.roots.card •ℕ 1
0. [simplify.rewrite] [nsmul_eq_mul]: p.roots.card •ℕ 1 ==> ↑(p.roots.card) * 1
0. [simplify.rewrite] [nat.cast_id]: ↑(p.roots.card) ==> p.roots.card
0. [simplify.rewrite] [mul_one]: p.roots.card * 1 ==> p.roots.card
0. [simplify.rewrite] [eq_self_iff_true]: p.roots.card = p.roots.card ==> true

I do not understand exactly what it means, but if I use the line given by squeeze_simp it only says

0. [simplify.rewrite] [multiset.map_map]: multiset.map nat_degree (multiset.map (λ (a : α), X - ⇑C a) p.roots) ==> multiset.map (nat_degree ∘ λ (a : α), X - ⇑C a) p.roots

So it seems it is doing the first line but not the others.

[Johan Commelin]

Well, each line of that output gives you a lemma that you can pass to simp only. Just copy-paste the name between the second set of [..]s

[Riccardo Brasca]

Yes, but that's what simp only proposes, with a small difference in the order, but the result is the same.

I tried to write the simp only one by one. The first line simp only [multiset.map_map] seems ok (trace.simplify.rewrite true gives the correct output), but then simp only [function.comp_app] says simplify tactic failed to simplify. If I understand what simp only is doing here, it wants to do rw function.comp_app, but I have the impressione that a simple rw doesn't work inside a ( ).sum.

[Johan Commelin]

Weird...

[Riccardo Brasca]

I guess I will just keep my simp, but if someone is interested here is the code that does not work and should work if one just copy/paste the output of set_option trace.simplify.rewrite true (I put a sorry after the error instead of the rest of the output).

import algebra.big_operators.basic
import field_theory.splitting_field

variables {α : Type*} [field α]

namespace polynomial

lemma test (p : polynomial α) :
(multiset.map (λ (a : α), X - C a) p.roots).prod.nat_degree = p.roots.card :=
begin
rw [nat_degree_multiset_prod],
  simp only [multiset.map_map],
  simp only [function.comp_app],
  sorry
end

end polynomial

It fails with simplify tactic failed to simplify.

[Johan Commelin]

As a hack, maybe you can pass it function.comp instead of function.comp_app

[Riccardo Brasca]

That magically works!