Question about namespace

Stream: new members

[Alfredo]

Hi all, i am very new to lean so trying to do some easy cleanup task, however as a begginier, i have some problems that i can't figure out. I made a draft PR to ask a question: https://github.com/leanprover-community/mathlib/pull/11805
Any input will be great, thanks in advance.

[Eric Rodriguez]

hiya Alfredo, you should try move this to another thread!

[Riccardo Brasca]

I've moved the message to a new thread.

[Riccardo Brasca]

(feel free to modify the title)

[Alfredo]

ops, sorry about that. thanks for the move, title looks good.

[Riccardo Brasca]

What is the error you are getting?

[Alfredo]

forgot to post that:

type mismatch at application
  has_mul.mul X
term
  X
has type
  polynomial ?m_1 : Type ?
but is expected to have type
  power_series A : Type u_1

[Johan Commelin]

It looks like lean thinks you are trying to multiply polynomials whereas it expects you to multiply power series.

[Johan Commelin]

Does writing power_series.X instead of X help?

[Alfredo]

i think i tried, the error change to a lower line if we do that

[Alfredo]

it will fial in the rw line:

  rw [coeff_succ_X_mul, coeff_rescale, coeff_exp, coeff_mul,
    nat.sum_antidiagonal_eq_sum_range_succ_mk, sum_range_succ],

with error:

error: rewrite tactic failed, did not find instance of the pattern in the target expression
  (?m_3 * ?m_4).coeff ?m_5
state:
A : Type u_1,
_inst_1 : comm_ring A,
_inst_2 : algebra ℚ A,
t : A,
n : ℕ
⊢ ⇑(power_series.coeff A n.succ)
      (mk (λ (n : ℕ), ⇑(aeval t) ((1 / ↑n!) • bernoulli_poly n)) * (exp A - 1)) =
    t ^ n * ⇑(algebra_map ℚ A) (1 / ↑n!)
external command exited with status 1

[Johan Commelin]

Did you move things from the power_series namespace to a place working inside the polynomial namespace?

[Alfredo]

i dont think i did that
can you explain more ?

[Riccardo Brasca]

I suggested to work in the polynomial namespace (since the file is about Bernoulli polynomials). Let me check what's going on.

[Alfredo]

yea, that is what i am trying to do, i can add everything to the polynomial namespace without issues but the second theorem is the one that fails when we do that

[Riccardo Brasca]

Here is what is going on: writing namespace polynomial means that all the lemma will have polynomial in the name, so for example lemma foo will be called polynomial.foo (this answer your first comment about collision with another name).

[Riccardo Brasca]

It also means that if a lemma is called polynomial.bar you can use it just writing bar (so namespace polynomial implies open polynomial, and this line can be deleted).

[Riccardo Brasca]

In the file there is also open power_series, to avoid writing power_series.exp and similar stuff.

[Alfredo]

yes

[Riccardo Brasca]

Now, there is polynomial.X and power_series.X in mathlib, and this confuses Lean, since now both are called X. This is why you got the first error: Lean tried to use polynomial.X, but there one should use power_series.X. You can help it writing power_series.X in that location.

[Alfredo]

right

[Riccardo Brasca]

The second error is similar: it says

rewrite tactic failed, did not find instance of the pattern in the target expression
  (?m_3 * ?m_4).coeff ?m_5

In the line

  rw [coeff_succ_X_mul, coeff_rescale, coeff_exp, coeff_mul,
    nat.sum_antidiagonal_eq_sum_range_succ_mk, sum_range_succ],

Looking at the error one can guess that it's something related to coeff_mul (you can also delete one lemma after the other to see which one creates problems).

[Riccardo Brasca]

And indeed we have both polynomial.coeff_mul and power_series.coeff_mul.

[Riccardo Brasca]

Here again the correct one is the latter, so with power_series.coeff_mul the error goes away.

[Alfredo]

cool, you are the best, thank you!

[Alfredo]

i made an additional comment about the first question

[Riccardo Brasca]

The same error occurs again later, but it's a little trickier to understand: it says that it cannot use apply congr_arg to make progress, but this is because the previous line, the one with simp only changed it's effect and it has become less efficient. You should replace coeff_one with power_series.coeff_one and then everything works.

[Alfredo]

awsome

[Riccardo Brasca]

Concerning your new comment: I don't understand what you mean, I don't have any error.

[Riccardo Brasca]

Can I push a commit to your branch?

[Alfredo]

sure

[Riccardo Brasca]

Ah sorry, now I got what you mean. Yes, if you want to use bernoulli you can write _root_.bernoulli.

[Riccardo Brasca]

/-- The Bernoulli polynomials are defined in terms of the negative Bernoulli numbers. -/
def bernoulli (n : ℕ) : polynomial ℚ :=
  ∑ i in range (n + 1), polynomial.monomial (n - i) ((bernoulli i) * (choose n i))

lemma bernoulli_def (n : ℕ) : bernoulli n =
  ∑ i in range (n + 1), polynomial.monomial i ((_root_.bernoulli (n - i)) * (choose n i)) :=
begin
  rw [←sum_range_reflect, add_succ_sub_one, add_zero, bernoulli],
  apply sum_congr rfl,
  rintros x hx,
  rw mem_range_succ_iff at hx, rw [choose_symm hx, tsub_tsub_cancel_of_le hx],
end

This works. (There are other changes to be done later in the file.)

[Alfredo]

apologies, had to go out for a bit

[Alfredo]

thank you for the help , i will try to do the other changes suggested, i think there are just lemma name changes left