Zulip Chat Archive

Stream: general

Topic: casts


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

view this post on Zulip Reid Barton (Jun 27 2019 at 01:26):

is it not refl?

view this post on Zulip Scott Morrison (Jun 27 2019 at 01:26):

Unfortunately not

view this post on Zulip Mario Carneiro (Jun 27 2019 at 01:27):

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

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

view this post on Zulip Scott Morrison (Jun 27 2019 at 01:27):

But they don't feel like the right lemmas!

view this post on Zulip Mario Carneiro (Jun 27 2019 at 01:28):

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

view this post on Zulip Scott Morrison (Jun 27 2019 at 01:28):

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

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

view this post on Zulip Scott Morrison (Jun 27 2019 at 01:29):

Can it be generalised in some useful way?

view this post on Zulip Mario Carneiro (Jun 27 2019 at 01:29):

that looks already maximally generalized

view this post on Zulip Scott Morrison (Jun 27 2019 at 01:30):

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

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

view this post on Zulip Mario Carneiro (Jun 27 2019 at 01:32):

and more likely to trigger with other stuff

view this post on Zulip Scott Morrison (Jun 27 2019 at 01:33):

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

view this post on Zulip Mario Carneiro (Jun 27 2019 at 01:33):

is nat.cast in scope there?

view this post on Zulip Scott Morrison (Jun 27 2019 at 01:34):

no...

view this post on Zulip Mario Carneiro (Jun 27 2019 at 01:35):

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

view this post on Zulip Scott Morrison (Jun 27 2019 at 01:36):

Seems to work.

view this post on Zulip Scott Morrison (Jun 27 2019 at 01:36):

am I meant to mark this with squash_cast?

view this post on Zulip Scott Morrison (Jun 27 2019 at 01:36):

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

view this post on Zulip Scott Morrison (Jun 27 2019 at 01:42):

#1155

view this post on Zulip Scott Morrison (Jun 27 2019 at 01:42):

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

view this post on Zulip Kenny Lau (Jun 27 2019 at 08:52):

I remember having talked about this before...

view this post on Zulip Kevin Buzzard (Jun 27 2019 at 08:55):

link or it didn't happen

view this post on Zulip Kenny Lau (Jun 27 2019 at 08:59):

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

view this post on Zulip Kevin Buzzard (Jun 27 2019 at 09:03):

Thanks

view this post on Zulip Scott Morrison (Jun 27 2019 at 10:16):

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

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

view this post on Zulip Mario Carneiro (Jun 27 2019 at 10:52):

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

view this post on Zulip Kenny Lau (Jun 27 2019 at 10:55):

@Kevin Buzzard someone verified your canonical criterion!

view this post on Zulip Kevin Buzzard (Jun 27 2019 at 12:07):

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

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

view this post on Zulip Kevin Buzzard (Jun 27 2019 at 12:13):

:-)


Last updated: May 11 2021 at 13:22 UTC