Zulip Chat Archive

Stream: general

Topic: simp tactic fails resulting in weird coercions


view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Aditya Agarwal (Feb 08 2019 at 05:39):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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'

view this post on Zulip Kenny Lau (Feb 08 2019 at 23:40):

hasn't some similar issue been raised before?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Scott Morrison (Feb 09 2019 at 00:02):

Awesome, thanks, that solves the problem nicely.

view this post on Zulip 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

view this post on Zulip Scott Morrison (Feb 09 2019 at 00:05):

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

view this post on Zulip Kenny Lau (Feb 09 2019 at 00:05):

it's faster

view this post on Zulip 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