Import impacts simp?

Stream: general

[Kunhao Zheng]

Hi all! I just encountered a phenomenon that I don't understand quite well. Don't know if you have any clue?
(the mathlib I used is based on the commit "9a8dcb9be408e7ae8af9f6832c08c021007f40ec", maybe not the latest but it's quite new)

Let's start from an example:

import data.nat.basic
import data.finset.basic
import algebra.big_operators.basic
import tactic.linarith
open_locale big_operators

example : ∑ (x : ℕ) in finset.range 49, (1:ℚ) = 49 :=
begin
  simp,
end

This one should look good and we have goal accomplished. But if I add more imports to the file, like the following one:

import algebra.algebra.basic
import algebra.big_operators.basic
import algebra.floor
import algebra.group_power.basic
import algebra.quadratic_discriminant
import algebra.ring.basic
import analysis.asymptotics.asymptotic_equivalent
import analysis.mean_inequalities
import analysis.normed_space.basic
import analysis.normed_space.inner_product
import analysis.normed_space.pi_Lp
import analysis.special_functions.exp_log
import analysis.special_functions.pow
import analysis.special_functions.trigonometric
import data.complex.basic
import data.complex.exponential
import data.equiv.basic
import data.finset.basic
import data.int.basic
import data.int.gcd
import data.int.modeq
import data.multiset.basic
import data.nat.basic
import data.nat.factorial
import data.nat.modeq
import data.nat.parity
import data.nat.prime
import data.pnat.basic
import data.polynomial
import data.polynomial.basic
import data.polynomial.eval
import data.rat.basic
import data.real.basic
import data.real.ennreal
import data.real.irrational
import data.real.nnreal
import data.real.sqrt
import data.zmod.basic
import geometry.euclidean.basic
import geometry.euclidean.circumcenter
import init.data.nat.gcd
import linear_algebra.affine_space.affine_map
import linear_algebra.affine_space.independent
import linear_algebra.finite_dimensional
import number_theory.divisors
import order.bounds
import order.filter.basic
import topology.basic
import topology.instances.nnreal
open_locale big_operators

example : ∑ (x : ℕ) in finset.range 49, (1:ℚ) = 49 :=
begin
  simp,
end

It became

tactic failed, there are unsolved goals
state:
⊢ 32 + 16 + 1 = 49

So I would like to know if this is a bug or it's reasonable? And different imports do impact the performance of simp? Any clue is welcome!

[David Wärn]

It looks like one of your imports contains a simp lemma that rewrote 49 to it's binary representation 32+16+1. You can use squeeze_simp to get a better idea of what happened (it tells you what lemmas were used by simp)

[Kunhao Zheng]

Thanks! So the simp tactic will search through the lemma with @simp among all the files that I import. As I import more files, the search space is larger and there is more chance that it applies the lemma that is not really desirable. Is it correct?

[Oliver Nash]

Yes though in theory there should be no such thing as a simp lemma that is not really desirable.

[Oliver Nash]

So this is a good opportunity to compare the results of the two squeeze_simps and see if there are some simp tags that need rethinking.

[Kunhao Zheng]

Cool! Thank you for the hint. This is a very good practice!

The first one implies

simp only [mul_one, nat.cast_bit0, finset.sum_const, nsmul_eq_mul, nat.cast_bit1, finset.card_range, nat.cast_one]

and the second one

simp only [one_mul, finset.sum_const, nsmul_eq_mul, algebra.bit1_smul_one, finset.card_range, nat.cast_one,
  algebra.bit0_smul_bit0, algebra.bit1_smul_bit0],

[Yakov Pechersky]

The offending one is the one that mentions bit1. As a stopgap, you can include [bit1] in your simp call.

[Oliver Nash]

I don't have time to dig into this at the moment but the two lists are:

 * mul_one
 * finset.sum_const
 * finset.card_range
 * nsmul_eq_mul
 * nat.cast_one
 * nat.cast_bit0
 * nat.cast_bit1

and

 * one_mul
 * finset.sum_const
 * finset.card_range
 * nsmul_eq_mul
 * nat.cast_one
 * algebra.bit0_smul_bit0
 * algebra.bit1_smul_bit0
 * algebra.bit1_smul_one

[Oliver Nash]

Definitely the lemmas mentioning bit need some thought.

[Alex J. Best]

The following versions of the lemmas algebra.bit1_smul_one and algebra.bit0_smul_one seem to work a bit better, I'll try and run CI on them and see what happens

import algebra.algebra.basic
import algebra.big_operators.basic
import algebra.floor
import algebra.group_power.basic
import algebra.quadratic_discriminant
import algebra.ring.basic
import analysis.asymptotics.asymptotic_equivalent
import analysis.mean_inequalities
import analysis.normed_space.basic
import analysis.normed_space.inner_product
import analysis.normed_space.pi_Lp
import analysis.special_functions.exp_log
import analysis.special_functions.pow
import analysis.special_functions.trigonometric
import data.complex.basic
import data.complex.exponential
import data.equiv.basic
import data.finset.basic
import data.int.basic
import data.int.gcd
import data.int.modeq
import data.multiset.basic
import data.nat.basic
import data.nat.factorial
import data.nat.modeq
import data.nat.parity
import data.nat.prime
import data.pnat.basic
import data.polynomial
import data.polynomial.basic
import data.polynomial.eval
import data.rat.basic
import data.real.basic
import data.real.ennreal
import data.real.irrational
import data.real.nnreal
import data.real.sqrt
import data.zmod.basic
import geometry.euclidean.basic
import geometry.euclidean.circumcenter
import init.data.nat.gcd
import linear_algebra.affine_space.affine_map
import linear_algebra.affine_space.independent
import linear_algebra.finite_dimensional
import number_theory.divisors
import order.bounds
import order.filter.basic
import topology.basic
import topology.instances.nnreal
open_locale big_operators
@[simp]
theorem algebra.bit0_smul_one' {R : Type*} {A : Type*} [comm_semiring R] [semiring A] [algebra R A] {r : R} :
bit0 r • (1:A) = bit0 (r • (1:A)) := by simp [bit0, add_smul]
@[simp]
theorem algebra.bit1_smul_one' {R : Type*} {A : Type*} [comm_semiring R] [semiring A] [algebra R A] {r : R} :
bit1 r • (1:A) = bit1 (r • (1: A)) := by simp [bit1, add_smul]
example : ∑ (x : ℕ) in finset.range 49, (1:ℚ) = 49 :=
begin
simp [-algebra.bit1_smul_one, algebra.bit1_smul_one',
      -algebra.bit0_smul_one, algebra.bit0_smul_one'],
end

[Eric Wieser]

What's the difference between your lemma and docs#algebra.bit1_smul_one?

[Eric Wieser]

Oh, I see - bit1 (r • 1 : A) vs (r • 2 + 1 : A) on the RHS

[Eric Wieser]

Yeah, your lemma definitely looks better

[Alex J. Best]

Yeah it looks like the originals aren't used anywhere by name, so the only potential issues would be in simp calls, hopefully CI will find them :grinning:

[Anne Baanen]

That does look a lot better, thanks for investigating!

[Eric Wieser]

Although actually - would bit1 r • (1 : A) = r • bit1 (1 : A) be a better simp lemma?

[Eric Wieser]

Since that ensures the bit1 gets placed on the 1 which is likely to introduce a numeral in a helpful place

[Alex J. Best]

This one isn't true right? (2 + 2 + 1) • (1 : A) \ne 2 • (1 + 1 + 1 : A) the bit0 version works, but I would think keeping both bit0/1 on the same side is best?

[Alex J. Best]

This is now #8394