Zulip Chat Archive

Stream: general

Topic: cast


view this post on Zulip Kenny Lau (Jun 10 2019 at 15:23):

theorem cast_eq_of_heq :  {α β : Sort u} {a : α} {b : β} (H : a == b), cast (type_eq_of_heq H) a = b
| α _ a _ heq.rfl := rfl

view this post on Zulip Kenny Lau (Jun 10 2019 at 15:23):

I feel like cast isn't used enough

view this post on Zulip Kenny Lau (Jun 10 2019 at 15:23):

here's a theorem I proved with cast

view this post on Zulip Mario Carneiro (Jun 10 2019 at 15:25):

cast is used exactly as often as it should be, which is almost never

view this post on Zulip Mario Carneiro (Jun 10 2019 at 15:25):

it's also not much different from eq.rec

view this post on Zulip Wojciech Nawrocki (Jun 11 2019 at 16:55):

@Mario Carneiro I run into casts all the time, but I would like to not use them, in accordance with your "almost never". However, I don't see any way to do that. For example, as soon as I define a few simple things, casts seem to become necessary really quickly:

variable vector:   Type
variable mk_vec: Π n: , vector n
variable consume_vec: Π x y, vector (x+y)  

-- Of course, I could just swap the x,y arguments to consume_vec here but this
-- doesn't seem to be possible very often with more complicated types.
def something_useful := λ x y, consume_vec x y $ cast (by simp) (mk_vec (y + x))

-- At what point does this go wrong? To me, it seems like
-- it goes wrong as soon as `vector` is defined the way it is here.

view this post on Zulip Mario Carneiro (Jun 11 2019 at 20:10):

you are right... it goes wrong as soon as you state the problem like that


Last updated: May 16 2021 at 05:21 UTC