# Zulip Chat Archive

## 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) (@add_monoid.to_has_zero.{0} (with_bot.{0} nat) (@with_bot.add_monoid.{0} nat nat.add_monoid)) (@with_bot.has_one.{0} nat nat.has_one) (@add_semigroup.to_has_add.{0} (with_bot.{0} nat) (@add_monoid.to_add_semigroup.{0} (with_bot.{0} nat) (@with_bot.add_monoid.{0} nat nat.add_monoid)))))) 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) (@add_monoid.to_has_zero.{0} (with_bot.{0} nat) (@with_bot.add_monoid.{0} nat nat.add_monoid)) (@with_bot.has_one.{0} nat nat.has_one) (@add_semigroup.to_has_add.{0} (with_bot.{0} nat) (@add_monoid.to_add_semigroup.{0} (with_bot.{0} nat) (@with_bot.add_monoid.{0} nat nat.add_monoid)))))) 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.

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

it's faster

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

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

Last updated: Aug 03 2023 at 10:10 UTC