Zulip Chat Archive

Stream: general

Topic: Fighting cast


view this post on Zulip Eric Wieser (Mar 23 2021 at 13:09):

I know that I probably don't want to be at this goal state in the first place, but is this true?

example {ι : Type*} [add_monoid ι] {A : ι  Type*} [ i, has_zero (A i)] :
  cast (congr_arg A (zero_add (0 : ι))) 0 = 0 :=
begin
  apply eq_of_heq,
  apply cast_heq _ _, -- fails, for reasons I don't understand
end

docs#cast_heq doesn't seem to apply properly

view this post on Zulip Kevin Buzzard (Mar 23 2021 at 13:11):

import tactic

example {ι : Type*} [add_monoid ι] {A : ι  Type*} [ i, has_zero (A i)] :
  cast (congr_arg A (zero_add (0 : ι))) 0 = 0 :=
begin
  apply eq_of_heq,
  convert cast_heq _ _;
  simp,
end

view this post on Zulip Kevin Buzzard (Mar 23 2021 at 13:12):

cast_heqwants the a's in cast h a == a to have the same type, but yours don't

view this post on Zulip Eric Wieser (Mar 23 2021 at 13:21):

Thanks!

view this post on Zulip Eric Wieser (Mar 23 2021 at 13:22):

Now why doesn't my attempt to generalize this work...

lemma cast_pi {ι : Sort*} {A : ι  Sort*} (f : Π i, A i) {i j : ι} (h : i = j) :
  cast (congr_arg A h) (f i) = f j :=
begin
  convert cast_eq _ _,
  refl,
end

example {ι : Type*} [add_monoid ι] {A : ι  Type*} [ i, has_zero (A i)] :
  cast (congr_arg A (zero_add (0 : ι))) 0 = 0 :=
begin
  -- exact cast_pi (λ i, (0 : A i)) _, -- works
  apply cast_pi, --fails
  -- refine cast_pi _ _, --fails
end

view this post on Zulip Kevin Buzzard (Mar 23 2021 at 14:42):

mumble mumble apply bug?

view this post on Zulip Kevin Buzzard (Mar 23 2021 at 14:45):

mumble mumble higher order unification problem? Actually that might be it, guessing a function is hard,

view this post on Zulip Eric Wieser (Mar 23 2021 at 15:05):

I guess I'm surprised that it doesn't just give me a goal filled with metavariables

view this post on Zulip Eric Wieser (Mar 23 2021 at 15:06):

I created #6834 which hopefully eliminates some of the pain I'm feeling, but it doesn't help the case I presented here.

view this post on Zulip Eric Wieser (Mar 23 2021 at 18:30):

And #6837 has some gross solutions to nasty versions of the one I started this thread with


Last updated: May 15 2021 at 02:11 UTC