Zulip Chat Archive
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):
adding the lemma
@[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?
Mario Carneiro (Jun 27 2019 at 01:29):
that looks already maximally generalized
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?
Scott Morrison (Jun 27 2019 at 01:34):
no...
Mario Carneiro (Jun 27 2019 at 01:35):
what about the other way around, putting it in data.nat.cast
Scott Morrison (Jun 27 2019 at 01:36):
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? :-)
Scott Morrison (Jun 27 2019 at 01:42):
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:52):
I remember having talked about this before...
Kevin Buzzard (Jun 27 2019 at 08:55):
link or it didn't happen
Kenny Lau (Jun 27 2019 at 08:59):
Kevin Buzzard (Jun 27 2019 at 09:03):
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: Dec 20 2023 at 11:08 UTC