## Stream: general

### Topic: casts

#### Scott Morrison (Jun 27 2019 at 01:25):

What is the canonical solution to:

import data.polynomial

open polynomial

universe u

variables {α : Type u} [integral_domain α] [decidable_eq α]

example (n : ℕ) : degree (X^n : polynomial α) = n :=
begin
simp,
-- We're left with ↑n = ↑n
sorry
end


Are we missing some lemmas? Should norm_cast be able to help here (it currently doesn't).

#### Reid Barton (Jun 27 2019 at 01:26):

is it not refl?

#### Scott Morrison (Jun 27 2019 at 01:26):

Unfortunately not

#### Mario Carneiro (Jun 27 2019 at 01:27):

There is clearly a missing lemma. What are the coe instances involved?

#### Scott Morrison (Jun 27 2019 at 01:27):

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

example (n : ℕ) : degree (X^n : polynomial α) = n :=
by simp


works

#### Scott Morrison (Jun 27 2019 at 01:27):

But they don't feel like the right lemmas!

#### Mario Carneiro (Jun 27 2019 at 01:28):

That looks right to me... I recall Johan mentioning this lemma

#### Scott Morrison (Jun 27 2019 at 01:28):

Oh, actually the second one isn't necessary. (removed it)

#### Mario Carneiro (Jun 27 2019 at 01:29):

I'm not sure about the direction of the simp though. Isn't the RHS two up arrows?

#### Scott Morrison (Jun 27 2019 at 01:29):

Can it be generalised in some useful way?

#### Scott Morrison (Jun 27 2019 at 01:30):

Okay. If I reverse the direction of the simp lemma, it no longer fixes my problem.

#### Mario Carneiro (Jun 27 2019 at 01:31):

Eh, I guess it's fine the way you wrote it... There are more coes but they are simpler

#### Mario Carneiro (Jun 27 2019 at 01:32):

and more likely to trigger with other stuff

#### Scott Morrison (Jun 27 2019 at 01:33):

Okay. And this belongs in src/order/bounded_lattice.lean, right after the coercion is introduced?

#### Mario Carneiro (Jun 27 2019 at 01:33):

is nat.cast in scope there?

no...

#### Mario Carneiro (Jun 27 2019 at 01:35):

what about the other way around, putting it in data.nat.cast

Seems to work.

#### Scott Morrison (Jun 27 2019 at 01:36):

am I meant to mark this with squash_cast?

#### Scott Morrison (Jun 27 2019 at 01:36):

even though it's actually unsquashing a cast? :-)

#1155

#### Scott Morrison (Jun 27 2019 at 01:42):

(Going through abandoned pieces of students' work salvaging useful bits. :-)

#### Kenny Lau (Jun 27 2019 at 08:59):

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/simp.20tactic.20fails.20resulting.20in.20weird.20coercions

Thanks

#### Scott Morrison (Jun 27 2019 at 10:16):

Thanks Kenny, I've switched over to using your faster proof.

#### Kenny Lau (Jun 27 2019 at 10:20):

did you and Mario come up with the exact same lemma and proof across 4 months :o

#### Mario Carneiro (Jun 27 2019 at 10:52):

that's when you know it's a good interface

#### Kenny Lau (Jun 27 2019 at 10:55):

@Kevin Buzzard someone verified your canonical criterion!

#### Kevin Buzzard (Jun 27 2019 at 12:07):

Yeah, that's a proof that it's the canonical interface.

#### Scott Morrison (Jun 27 2019 at 12:13):

No, I found that in a student's old repo that I was looking at for other reasons; I suspect he got it from Mario to begin with.

#### Kevin Buzzard (Jun 27 2019 at 12:13):

:-)

Last updated: May 11 2021 at 13:22 UTC