simp tactic fails resulting in weird coercions

Stream: general

[Aditya Agarwal]

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]

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

[Aditya Agarwal]

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

[Aditya Agarwal]

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]

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]

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]

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]

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

[Mario Carneiro]

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]

hasn't some similar issue been raised before?

[Kenny Lau]

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]

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]

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]

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

[Mario Carneiro]

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]

Awesome, thanks, that solves the problem nicely.

[Kenny Lau]

@[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]

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

[Kenny Lau]

it's faster

[Scott Morrison]

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