## Stream: general

### Topic: simp tactic fails resulting in weird coercions

#### Aditya Agarwal (Feb 08 2019 at 05:36):

Trying to prove lemma minimal (n : ℕ) : degree (X^n : polynomial α) = n := by simp fails with the error

tactic failed, there are unsolved goals
state:
α : Type u,
_inst_1 : decidable_eq α,
_inst_2 : integral_domain α,
n : ℕ
⊢ ↑n = ↑n


Because of slightly different coercions

set_option pp.all true


Produces

tactic failed, there are unsolved goals
state:
α : Type u,
_inst_1 : decidable_eq.{u+1} α,
_inst_2 : integral_domain.{u} α,
n : nat
⊢ @eq.{1} (with_bot.{0} nat)
(@coe.{1 1} nat (with_bot.{0} nat)
(@coe_to_lift.{1 1} nat (with_bot.{0} nat)
(@coe_base.{1 1} nat (with_bot.{0} nat)
(@nat.cast_coe.{0} (with_bot.{0} nat)
(@with_bot.has_one.{0} nat nat.has_one)
n)
(@coe.{1 1} nat (with_bot.{0} nat) (@coe_to_lift.{1 1} nat (with_bot.{0} nat) (@with_bot.has_coe_t.{0} nat)) n)


#### Aditya Agarwal (Feb 08 2019 at 05:38):

I have written a minimal example here https://github.com/chocolatier/theoremproving/blob/master/src/coe_mwe.lean

#### Aditya Agarwal (Feb 08 2019 at 05:39):

Lean should be able to identify that these two coercions are identical.

#### Aditya Agarwal (Feb 08 2019 at 05:42):

In a somewhat related point, the lemma is basically degree_X_pow, which is a simp lemma in data.polynomial. Using the simp tactic with that specified explicitly works.

#### Aditya Agarwal (Feb 08 2019 at 05:51):

Our goal is to show lemma deg_c_times_x_to_n_eq_n (n : ℕ) {c : α} (hc : c ≠ 0) : degree (C c * X^n) = n, which should ideally just be a simp, but currently requires the proof in the linked example.
It breaks if we replace

 ... = 0 + n : by rw [degree_X_pow] -- simp [degree_X_pow] also works fine.


with

  ... = 0 + n : by simp


Producing the same error as the mwe above.

#### Mario Carneiro (Feb 08 2019 at 06:16):

there is actually a theorem to prove there. Because with_bot nat is a semiring (because nat is), it has a cast from nat. The value of cast n should be some n though, that needs to be proved

#### Scott Morrison (Feb 08 2019 at 23:19):

What is the actual lemma we need here? We can prove

@[simp] lemma nat.cast_with_bot (n : ℕ) : @eq.{1} (with_bot.{0} nat)
(@coe.{1 1} nat (with_bot.{0} nat)
(@coe_to_lift.{1 1} nat (with_bot.{0} nat)
(@coe_base.{1 1} nat (with_bot.{0} nat)
(@nat.cast_coe.{0} (with_bot.{0} nat)
(@with_bot.has_one.{0} nat nat.has_one)
n)
(@coe.{1 1} nat (with_bot.{0} nat) (@coe_to_lift.{1 1} nat (with_bot.{0} nat) (@with_bot.has_coe_t.{0} nat)) n) :=
begin
unfold_coes,
induction n,
{ simp, refl },
{ dsimp [nat.cast],
rw n_ih,
refl }
end


and all is well (i.e. lemma minimal (n : ℕ) : degree (X^n : polynomial α) = n := by simp works), but that's a really messed up theorem statement...

#### Scott Morrison (Feb 08 2019 at 23:19):

One can prove @[simp] lemma nat.foo (n : ℕ) : ((nat.cast n) : with_bot ℕ) = some n := but it doesn't seem to help.

#### Mario Carneiro (Feb 08 2019 at 23:39):

that is indeed the lemma we need. I would write it like so:

lemma nat.cast_with_bot' : ∀ n : ℕ, (nat.cast n : with_bot ℕ) = some n
| 0 := rfl
| (n+1) := by simp [nat.cast, nat.cast_with_bot' n]; refl

@[simp] lemma nat.cast_with_bot : ∀ n : ℕ,
@coe _ (with_bot ℕ) (@coe_to_lift _ _ (@coe_base _ _ nat.cast_coe)) n = n :=
nat.cast_with_bot'


#### Kenny Lau (Feb 08 2019 at 23:40):

hasn't some similar issue been raised before?

#### Kenny Lau (Feb 08 2019 at 23:46):

lemma deg_c_times_x_to_n_eq_n (n : ℕ) {c : α} (hc : c ≠ 0) : degree (C c * X^n) = n :=
by rw [← single_eq_C_mul_X, degree, finsupp.support_single_ne_zero hc, finset.sup_singleton]; refl


#### Scott Morrison (Feb 08 2019 at 23:50):

It gives me a bad feeling that we need these additional cast_with_bot lemmas. We really want some insurance that no one ever defines a coercion nat \to α, and at the same time defines instances of [has_zero α] [has_one α] [has_add α], making the two coercions incompatible.

#### Mario Carneiro (Feb 08 2019 at 23:53):

no, this is part of the contract of writing an additional coercion - you want to show that it commutes with all the other coercions that can be applied with it

#### Mario Carneiro (Feb 08 2019 at 23:54):

There is a more general lemma here, namely (coe (n : nat) : with_bot A) = coe (coe n : A)

#### Mario Carneiro (Feb 09 2019 at 00:00):

ah yes, this is even easier:

@[simp] lemma nat.cast_with_bot_cast {α} [add_monoid α] [has_one α] : ∀ n : ℕ,
(n : with_bot α) = (n : α)
| 0 := rfl
| (n+1) := by simp [nat.cast_with_bot_cast n]

@[simp] lemma nat.cast_with_bot : ∀ n : ℕ,
@coe _ (with_bot ℕ) (@coe_to_lift _ _ (@coe_base _ _ nat.cast_coe)) n = n :=
by simp


#### Scott Morrison (Feb 09 2019 at 00:02):

Awesome, thanks, that solves the problem nicely.

#### Kenny Lau (Feb 09 2019 at 00:04):

@[simp] lemma nat.cast_with_bot_cast {α} [add_monoid α] [has_one α] : ∀ n : ℕ,
(n : with_bot α) = (n : α)
| 0 := rfl
| (n+1) := show ↑n + _ = ↑(↑n+_), by rw [n.cast_with_bot_cast]; refl


#### Scott Morrison (Feb 09 2019 at 00:05):

@Kenny Lau, why do you prefer that one? It just seems more complicated.

it's faster

#### Scott Morrison (Feb 09 2019 at 00:09):

We really need to buy you a new computer. :-)

Last updated: May 11 2021 at 23:11 UTC