## Stream: general

### Topic: Fighting cast

#### 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

#### 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


#### 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

Thanks!

#### 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


#### Kevin Buzzard (Mar 23 2021 at 14:42):

mumble mumble apply bug?

#### Kevin Buzzard (Mar 23 2021 at 14:45):

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

#### 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

#### 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.

#### 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