Fighting cast

Stream: general

[Eric Wieser]

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]

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]

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

[Eric Wieser]

Thanks!

[Eric Wieser]

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]

mumble mumble apply bug?

[Kevin Buzzard]

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

[Eric Wieser]

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

[Eric Wieser]

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]

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