## Stream: general

### Topic: Import impacts simp?

#### Kunhao Zheng (Jul 21 2021 at 12:49):

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.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 (Jul 21 2021 at 12:54):

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 (Jul 21 2021 at 12:59):

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 (Jul 21 2021 at 12:59):

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

#### Oliver Nash (Jul 21 2021 at 13:01):

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 (Jul 21 2021 at 13:06):

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 (Jul 21 2021 at 13:11):

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

#### Oliver Nash (Jul 21 2021 at 13:12):

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 (Jul 21 2021 at 13:13):

Definitely the lemmas mentioning bit need some thought.

#### Alex J. Best (Jul 22 2021 at 11:22):

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.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 (Jul 22 2021 at 11:37):

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

#### Eric Wieser (Jul 22 2021 at 11:38):

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

#### Eric Wieser (Jul 22 2021 at 11:38):

Yeah, your lemma definitely looks better

#### Alex J. Best (Jul 22 2021 at 11:39):

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 (Jul 22 2021 at 11:41):

That does look a lot better, thanks for investigating!

#### Eric Wieser (Jul 22 2021 at 11:43):

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

#### Eric Wieser (Jul 22 2021 at 11:45):

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

#### Alex J. Best (Jul 22 2021 at 11:50):

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 (Jul 22 2021 at 11:54):

This is now #8394

Last updated: Dec 20 2023 at 11:08 UTC